diff --git a/Cargo.toml b/Cargo.toml index 0033c16..a0b7709 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -10,3 +10,4 @@ edition = "2018" clap = "2.33" foliage = {path = "foliage"} nom = "5.0" +regex = "1.3" diff --git a/src/error.rs b/src/error.rs new file mode 100644 index 0000000..3b75349 --- /dev/null +++ b/src/error.rs @@ -0,0 +1,101 @@ +pub type Source = Box; + +pub enum Kind +{ + ParseProject, + NotAFile(std::path::PathBuf), + WriteFile(std::path::PathBuf), + RunVampire, + InterpretVampireOutput(String, String), +} + +pub struct Error +{ + pub kind: Kind, + pub source: Option, +} + +impl Error +{ + pub fn new(kind: Kind) -> Self + { + Self + { + kind, + source: None, + } + } + + pub fn with>(mut self, source: S) -> Self + { + self.source = Some(source.into()); + self + } + + pub fn new_parse_project>(source: S) -> Self + { + Self::new(Kind::ParseProject).with(source) + } + + pub fn new_not_a_file(path: std::path::PathBuf) -> Self + { + Self::new(Kind::NotAFile(path)) + } + + pub fn new_write_file>(path: std::path::PathBuf, source: S) -> Self + { + Self::new(Kind::WriteFile(path)).with(source) + } + + pub fn new_run_vampire>(source: S) -> Self + { + Self::new(Kind::RunVampire).with(source) + } + + pub fn new_interpret_vampire_output(stdout: String, stderr: String) -> Self + { + Self::new(Kind::InterpretVampireOutput(stdout, stderr)) + } +} + +impl std::fmt::Debug for Error +{ + fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result + { + match self.kind + { + Kind::ParseProject => write!(formatter, "could not parse project file")?, + Kind::NotAFile(ref file_path) => write!(formatter, "specified path is not a file ({})", file_path.display())?, + Kind::WriteFile(ref file_path) => write!(formatter, "could not write file ({})", file_path.display())?, + Kind::RunVampire => write!(formatter, "could not run Vampire")?, + Kind::InterpretVampireOutput(ref stdout, ref stderr) => write!(formatter, "could not interpret Vampire output\n\n======== stdout =========\n{}\n\n======== stderr =========\n{}", stdout, stderr)?, + } + + if let Some(source) = &self.source + { + write!(formatter, "\nerror source: {}", source)?; + } + + Ok(()) + } +} + +impl std::fmt::Display for Error +{ + fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(formatter, "{:?}", self) + } +} + +impl std::error::Error for Error +{ + fn source(&self) -> Option<&(dyn std::error::Error + 'static)> + { + match &self.source + { + Some(source) => Some(source.as_ref()), + None => None, + } + } +} diff --git a/src/format_tptp.rs b/src/format_tptp.rs index 9a20808..9b056e4 100644 --- a/src/format_tptp.rs +++ b/src/format_tptp.rs @@ -209,7 +209,11 @@ struct PredicateDeclarationDisplay<'a>(&'a foliage::PredicateDeclaration); struct TermDisplay<'a>(&'a foliage::Term); struct FormulaDisplay<'a>(&'a foliage::Formula); struct StatementKindDisplay<'a>(&'a crate::project::StatementKind); -pub struct ProjectDisplay<'a>(&'a crate::project::Project); +pub struct ProjectDisplay<'a> +{ + project: &'a crate::project::Project, + conjecture: (crate::project::StatementKind, &'a foliage::Formula), +} impl<'a> DisplayTPTP<'a, VariableDeclarationDisplay<'a>> for foliage::VariableDeclaration { @@ -251,11 +255,13 @@ impl<'a> DisplayTPTP<'a, StatementKindDisplay<'a>> for crate::project::Statement } } -impl<'a> DisplayTPTP<'a, ProjectDisplay<'a>> for crate::project::Project +pub fn display_project_with_conjecture_tptp<'a>(project: &'a crate::Project, + conjecture: (crate::project::StatementKind, &'a foliage::Formula)) -> ProjectDisplay<'a> { - fn display_tptp(&'a self) -> ProjectDisplay<'a> + ProjectDisplay { - ProjectDisplay(self) + project, + conjecture, } } @@ -569,8 +575,8 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a> let tptp_preamble_anthem_axioms = include_str!("tptp_preamble_anthem_axioms.tptp").trim_end(); write!(format, "\n{}", tptp_preamble_anthem_axioms)?; - let predicate_declarations = collect_predicate_declarations_in_project(self.0); - let symbolic_constants = collect_symbolic_constants_in_project(self.0); + let predicate_declarations = collect_predicate_declarations_in_project(self.project); + let symbolic_constants = collect_symbolic_constants_in_project(self.project); if !predicate_declarations.is_empty() || !symbolic_constants.is_empty() { @@ -587,7 +593,7 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a> } } - if let Some(axioms) = self.0.statements.get(&crate::project::StatementKind::Axiom) + if let Some(axioms) = self.project.statements.get(&crate::project::StatementKind::Axiom) { write_title(format, "\n\n", "axioms")?; @@ -597,27 +603,26 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a> } } - if let Some(lemmas) = self.0.statements.get(&crate::project::StatementKind::Lemma) + match self.conjecture { - write_title(format, "\n\n", "lemmas")?; - - for lemma in lemmas + (crate::project::StatementKind::Lemma, ref lemma) => { + write_title(format, "\n\n", "lemma")?; + write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Lemma.display_tptp(), lemma.display_tptp())?; - } - } - if let Some(conjectures) = self.0.statements.get(&crate::project::StatementKind::Conjecture) - { - write_title(format, "\n\n", "conjectures")?; - - for conjecture in conjectures + Ok(()) + }, + (crate::project::StatementKind::Conjecture, ref conjecture) => { - write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Conjecture.display_tptp(), conjecture.display_tptp())?; - } - } + write_title(format, "\n\n", "conjecture")?; - Ok(()) + write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Conjecture.display_tptp(), conjecture.display_tptp())?; + + Ok(()) + }, + (crate::project::StatementKind::Axiom, _) => panic!("unexpected axiom"), + } } } diff --git a/src/lib.rs b/src/lib.rs index 552dd13..1c57b8b 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,6 +1,8 @@ +mod error; pub mod format; pub mod format_tptp; pub mod parse; -mod project; +pub mod project; +pub use error::Error; pub use project::Project; diff --git a/src/main.rs b/src/main.rs index 8d91b84..ddfb38b 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,22 +1,172 @@ -use ask_dracula::format_tptp::DisplayTPTP; +fn backup_file_path(file_path: &std::path::Path) -> Result +{ + 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) -> Option<(ask_dracula::project::StatementKind, &'a foliage::Formula)> +{ + if let Some(lemmas) = project.statements.get(&ask_dracula::project::StatementKind::Lemma) + { + if let Some(lemma) = lemmas.first() + { + return Some((ask_dracula::project::StatementKind::Lemma, lemma)); + } + } + + if let Some(conjectures) = project.statements.get(&ask_dracula::project::StatementKind::Conjecture) + { + if let Some(conjecture) = conjectures.first() + { + return Some((ask_dracula::project::StatementKind::Conjecture, conjecture)); + } + } + + None +} + +enum VampireResult +{ + ProofNotFound, + Refutation, + Satisfiable, +} + +fn run_vampire(input: &str, arguments: Option) + -> Result + where I: IntoIterator, S: AsRef +{ + let mut vampire = std::process::Command::new("vampire"); + + let vampire = match arguments + { + Some(arguments) => vampire.args(arguments), + None => &mut vampire, + }; + + let mut vampire = vampire + .stdin(std::process::Stdio::piped()) + .stdout(std::process::Stdio::piped()) + .stderr(std::process::Stdio::piped()) + .spawn() + .map_err(|error| ask_dracula::Error::new_run_vampire(error))?; + + { + use std::io::Write; + + let vampire_stdin = vampire.stdin.as_mut().unwrap(); + vampire_stdin.write_all(input.as_bytes()) + .map_err(|error| ask_dracula::Error::new_run_vampire(error))?; + } + + let output = vampire.wait_with_output() + .map_err(|error| ask_dracula::Error::new_run_vampire(error))?; + + let stdout = std::str::from_utf8(&output.stdout) + .map_err(|error| ask_dracula::Error::new_run_vampire(error))?; + + let stderr = std::str::from_utf8(&output.stderr) + .map_err(|error| ask_dracula::Error::new_run_vampire(error))?; + + if !output.status.success() + { + let proof_not_found_regex = regex::Regex::new(r"% \(\d+\)Proof not found in time").unwrap(); + + if proof_not_found_regex.is_match(stdout) + { + return Ok(VampireResult::ProofNotFound); + } + + return Err(ask_dracula::Error::new_run_vampire( + format!("Vampire returned unsuccessful exit code ({})\n\n======== stderr ========\n{}", output.status, std::str::from_utf8(&output.stdout).unwrap_or("(not valid UTF-8)").trim()))); + } + + let refutation_regex = regex::Regex::new(r"% \(\d+\)Termination reason: Refutation").unwrap(); + + if refutation_regex.is_match(stdout) + { + return Ok(VampireResult::Refutation); + } + + Err(ask_dracula::Error::new_interpret_vampire_output(stdout.to_string(), stderr.to_string())) +} fn main() -> Result<(), Box> { let matches = clap::App::new("Ask Dracula: Using Vampire as an interactive theorem prover") - .arg(clap::Arg::with_name("file").long("file").short("f").takes_value(true).required(true)) - .after_help("example: ask_dracula -f program") + .arg(clap::Arg::with_name("file").takes_value(true).required(true)) + .arg(clap::Arg::with_name("vampire_arguments").multiple(true)) + .after_help("example: ask_dracula -- --mode casc --cores 8") .get_matches(); let file = matches.value_of("file").unwrap().to_string(); let file_path = std::path::Path::new(&file); let file_content = std::fs::read_to_string(&file_path)?; - let (_, project) = ask_dracula::parse::project(&file_content) + let (_, mut project) = ask_dracula::parse::project(&file_content) .map_err(|_| "couldn’t parse input file")?; - eprintln!("{}", project); + match find_conjecture(&project) + { + None => + { + eprintln!("no lemma or conjecture found, nothing to do"); + Ok(()) + }, + Some((ref statement_kind, ref conjecture)) => + { + eprintln!("verifying conjecture: {}", conjecture); - println!("{}", project.display_tptp()); + let tptp_content = format!("{}", ask_dracula::format_tptp::display_project_with_conjecture_tptp(&project, (statement_kind.clone(), conjecture))); - Ok(()) + match run_vampire(&tptp_content, matches.values_of("vampire_arguments").map(|value| value))? + { + VampireResult::ProofNotFound => + { + println!("proof not found"); + Ok(()) + }, + VampireResult::Refutation => + { + println!("conjecture proven"); + + let axiom = project.statements.get_mut(statement_kind).unwrap().remove(0); + project.statements.entry(ask_dracula::project::StatementKind::Axiom).or_insert_with(Vec::new).push(axiom); + + 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))?; + + Ok(()) + }, + VampireResult::Satisfiable => + { + println!("conjecture disproven"); + Ok(()) + }, + } + }, + } } diff --git a/src/project.rs b/src/project.rs index c4df427..38a9bdb 100644 --- a/src/project.rs +++ b/src/project.rs @@ -8,5 +8,5 @@ pub enum StatementKind pub struct Project { - pub(crate) statements: std::collections::HashMap>, + pub statements: std::collections::HashMap>, }