|
|
|
@ -1,24 +1,3 @@
|
|
|
|
|
fn backup_file_path(file_path: &std::path::Path) -> Result<std::path::PathBuf, ask_dracula::Error> |
|
|
|
|
{ |
|
|
|
|
let file_name = file_path.file_name() |
|
|
|
|
.ok_or(ask_dracula::Error::new_not_a_file(file_path.to_owned()))?; |
|
|
|
|
|
|
|
|
|
let mut i = 0; |
|
|
|
|
|
|
|
|
|
loop |
|
|
|
|
{ |
|
|
|
|
i += 1; |
|
|
|
|
|
|
|
|
|
let backup_file_name = format!("{}.{}~", file_name.to_string_lossy(), i); |
|
|
|
|
let backup_file_path = file_path.with_file_name(backup_file_name); |
|
|
|
|
|
|
|
|
|
if !backup_file_path.exists() |
|
|
|
|
{ |
|
|
|
|
return Ok(backup_file_path); |
|
|
|
|
} |
|
|
|
|
} |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
fn find_conjecture<'a>(project: &'a ask_dracula::Project, |
|
|
|
|
proof_direction: ask_dracula::project::ProofDirection) |
|
|
|
|
-> Option<&'a ask_dracula::project::Statement> |
|
|
|
@ -145,8 +124,6 @@ fn main() -> Result<(), Box<dyn std::error::Error>>
|
|
|
|
|
let (_, mut project) = ask_dracula::parse::project(&file_content) |
|
|
|
|
.map_err(|_| "couldn’t parse input file")?; |
|
|
|
|
|
|
|
|
|
let replace_statement_kind_regex = regex::Regex::new(r"(assertion)").unwrap(); |
|
|
|
|
|
|
|
|
|
let proof_directions = match matches.value_of("proof-direction").unwrap() |
|
|
|
|
{ |
|
|
|
|
"forward" => vec![ask_dracula::project::ProofDirection::Forward], |
|
|
|
@ -200,17 +177,6 @@ fn main() -> Result<(), Box<dyn std::error::Error>>
|
|
|
|
|
|
|
|
|
|
conjecture.kind = ask_dracula::project::StatementKind::Axiom; |
|
|
|
|
conjecture.original_text = replace_statement_kind_regex.replace(&conjecture.original_text, "axiom").to_string(); |
|
|
|
|
|
|
|
|
|
let backup_file_path = backup_file_path(file_path)?; |
|
|
|
|
|
|
|
|
|
// Make backup of old file
|
|
|
|
|
std::fs::rename(file_path, backup_file_path) |
|
|
|
|
.map_err(|error| ask_dracula::Error::new_write_file(file_path.to_owned(), error))?; |
|
|
|
|
|
|
|
|
|
// Write updated version of the file
|
|
|
|
|
let file_content = format!("{}", project); |
|
|
|
|
std::fs::write(file_path, &file_content) |
|
|
|
|
.map_err(|error| ask_dracula::Error::new_write_file(file_path.to_owned(), error))?; |
|
|
|
|
}, |
|
|
|
|
ProofResult::Satisfiable => |
|
|
|
|
{ |
|
|
|
|