From a206812d803c772496a67c991ef0930073b2f7d8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 7 Nov 2019 00:53:50 -0600 Subject: [PATCH] Implement forward and backward proofs with all new directives correctly --- src/format.rs | 20 ++++++ src/format_tptp.rs | 115 +++++++++++++++++++++++----------- src/main.rs | 149 +++++++++++++++++++++++++++++---------------- src/parse.rs | 2 + src/project.rs | 1 + 5 files changed, 198 insertions(+), 89 deletions(-) diff --git a/src/format.rs b/src/format.rs index 8cf3991..aabcc37 100644 --- a/src/format.rs +++ b/src/format.rs @@ -1,3 +1,23 @@ +impl std::fmt::Debug for crate::project::ProofDirection +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + match &self + { + crate::project::ProofDirection::Forward => write!(format, "forward"), + crate::project::ProofDirection::Backward => write!(format, "backward"), + } + } +} + +impl std::fmt::Display for crate::project::ProofDirection +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(format, "{:?}", &self) + } +} + impl std::fmt::Debug for crate::project::StatementKind { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result diff --git a/src/format_tptp.rs b/src/format_tptp.rs index 54715c0..cdf34da 100644 --- a/src/format_tptp.rs +++ b/src/format_tptp.rs @@ -4,15 +4,52 @@ pub trait DisplayTPTP<'a, DisplayType> fn display_tptp(&'a self) -> DisplayType; } -pub fn is_statement_kind_conjecture(statement_kind: &crate::project::StatementKind, +pub fn is_statement_axiom(statement: &crate::project::Statement, proof_direction: crate::project::ProofDirection) -> bool { - match (proof_direction, statement_kind) + if statement.proven + { + return true; + } + + match (proof_direction, &statement.kind) + { + (_, crate::project::StatementKind::Axiom) => true, + (_, crate::project::StatementKind::Assumption) => true, + (crate::project::ProofDirection::Forward, crate::project::StatementKind::Completion(_)) => true, + (crate::project::ProofDirection::Backward, crate::project::StatementKind::Assertion) => true, + _ => false, + } +} + +pub fn is_statement_lemma(statement: &crate::project::Statement, + proof_direction: crate::project::ProofDirection) -> bool +{ + if statement.proven + { + return false; + } + + match (proof_direction, &statement.kind) + { + (_, crate::project::StatementKind::Lemma(None)) => true, + (proof_direction, crate::project::StatementKind::Lemma(Some(proof_direction_lemma))) => proof_direction == *proof_direction_lemma, + _ => false, + } +} + +pub fn is_statement_theorem(statement: &crate::project::Statement, + proof_direction: crate::project::ProofDirection) -> bool +{ + if statement.proven + { + return false; + } + + match (proof_direction, &statement.kind) { (crate::project::ProofDirection::Forward, crate::project::StatementKind::Assertion) => true, (crate::project::ProofDirection::Backward, crate::project::StatementKind::Completion(_)) => true, - (_, crate::project::StatementKind::Lemma(None)) => true, - (proof_direction, crate::project::StatementKind::Lemma(Some(proof_direction_lemma))) => proof_direction == *proof_direction_lemma, _ => false, } } @@ -234,9 +271,9 @@ struct VariableDeclarationDisplay<'a>(&'a foliage::VariableDeclaration); struct PredicateDeclarationDisplay<'a>(&'a foliage::PredicateDeclaration); struct TermDisplay<'a>(&'a foliage::Term); struct FormulaDisplay<'a>(&'a foliage::Formula); -struct StatementKindDisplay<'a> +struct StatementDisplay<'a> { - statement_kind: &'a crate::project::StatementKind, + statement: &'a crate::project::Statement, proof_direction: crate::project::ProofDirection, } pub struct ProjectDisplay<'a> @@ -278,13 +315,13 @@ impl<'a> DisplayTPTP<'a, FormulaDisplay<'a>> for foliage::Formula } } -fn display_statement_kind_tptp<'a>(statement_kind: &'a crate::project::StatementKind, +fn display_statement_tptp<'a>(statement: &'a crate::project::Statement, proof_direction: crate::project::ProofDirection) - -> StatementKindDisplay<'a> + -> StatementDisplay<'a> { - StatementKindDisplay + StatementDisplay { - statement_kind, + statement, proof_direction, } } @@ -575,30 +612,42 @@ impl<'a> std::fmt::Display for FormulaDisplay<'a> } } -impl<'a> std::fmt::Debug for StatementKindDisplay<'a> +impl<'a> std::fmt::Debug for StatementDisplay<'a> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - match (&self.statement_kind, self.proof_direction) + write!(format, "\ntff(")?; + + let identifier = match &self.statement.kind { - (crate::project::StatementKind::Axiom, _) => write!(format, "axiom, axiom"), - (crate::project::StatementKind::Assumption, _) => write!(format, "assumption, axiom"), - (crate::project::StatementKind::Completion(_), crate::project::ProofDirection::Forward) => write!(format, "completion, axiom"), - (crate::project::StatementKind::Completion(_), crate::project::ProofDirection::Backward) => write!(format, "completion, conjecture"), - (crate::project::StatementKind::Assertion, crate::project::ProofDirection::Forward) => write!(format, "assertion, conjecture"), - (crate::project::StatementKind::Assertion, crate::project::ProofDirection::Backward) => write!(format, "assertion, axiom"), - (crate::project::StatementKind::Lemma(None), _) => write!(format, "lemma, conjecture"), - (crate::project::StatementKind::Lemma(Some(proof_direction_lemma)), proof_direction) => - match proof_direction == *proof_direction_lemma - { - true => write!(format, "lemma, conjecture"), - false => Ok(()), - }, + crate::project::StatementKind::Axiom => "axiom", + crate::project::StatementKind::Assumption => "assumption", + crate::project::StatementKind::Completion(_) => "completion", + crate::project::StatementKind::Assertion => "assertion", + crate::project::StatementKind::Lemma(_) => "lemma", + }; + + write!(format, "{}, ", identifier)?; + + if is_statement_theorem(&self.statement, self.proof_direction) + || is_statement_lemma(&self.statement, self.proof_direction) + { + write!(format, "conjecture")?; } + else if is_statement_axiom(&self.statement, self.proof_direction) + { + write!(format, "axiom")?; + } + else + { + panic!("expected statement to be either theorem, lemma, or axiom, please report to bug tracker"); + } + + write!(format, ", {:?}).", self.statement.formula.display_tptp()) } } -impl<'a> std::fmt::Display for StatementKindDisplay<'a> +impl<'a> std::fmt::Display for StatementDisplay<'a> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -652,25 +701,21 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a> { crate::project::Block::Whitespace(_) => None, crate::project::Block::Statement(ref statement) => - match is_statement_kind_conjecture(&statement.kind, self.proof_direction) + match is_statement_axiom(&statement, self.proof_direction) { - false => Some(statement), - true => None, + true => Some(statement), + false => None, } }); for axiom in axioms { - write!(format, "\ntff({:?}, {:?}).", - display_statement_kind_tptp(&axiom.kind, self.proof_direction), axiom.formula.display_tptp())?; + write!(format, "\n{}", display_statement_tptp(&axiom, self.proof_direction))?; } write_title(format, "\n\n", "assertion")?; - write!(format, "\ntff({:?}, {:?}).", - display_statement_kind_tptp(&self.conjecture.kind, self.proof_direction), self.conjecture.formula.display_tptp())?; - - Ok(()) + write!(format, "\n{}", display_statement_tptp(&self.conjecture, self.proof_direction)) } } diff --git a/src/main.rs b/src/main.rs index 432ebc1..671bd9f 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,39 +1,3 @@ -fn find_conjecture<'a>(project: &'a ask_dracula::Project, - proof_direction: ask_dracula::project::ProofDirection) - -> Option<&'a ask_dracula::project::Statement> -{ - for block in &project.blocks - { - if let ask_dracula::project::Block::Statement(ref statement) = block - { - if ask_dracula::format_tptp::is_statement_kind_conjecture(&statement.kind, proof_direction) - { - return Some(statement) - } - } - } - - None -} - -fn find_conjecture_mut<'a>(project: &'a mut ask_dracula::Project, - proof_direction: ask_dracula::project::ProofDirection) - -> Option<&'a mut ask_dracula::project::Statement> -{ - for block in &mut project.blocks - { - if let ask_dracula::project::Block::Statement(ref mut statement) = block - { - if ask_dracula::format_tptp::is_statement_kind_conjecture(&statement.kind, proof_direction) - { - return Some(statement) - } - } - } - - None -} - enum ProofResult { ProofNotFound, @@ -41,6 +5,18 @@ enum ProofResult Satisfiable, } +fn reset_proof_results<'a>(project: &'a mut ask_dracula::Project) +{ + for block in &mut project.blocks + { + match block + { + ask_dracula::project::Block::Whitespace(_) => (), + ask_dracula::project::Block::Statement(ref mut statement) => statement.proven = false, + } + } +} + fn run_vampire(input: &str, arguments: Option) -> Result<(ProofResult, Option), ask_dracula::Error> where I: IntoIterator, S: AsRef @@ -132,30 +108,61 @@ fn main() -> Result<(), Box> proof_direction => panic!("unrecognized proof direction “{}”", proof_direction), }; + let mut section_separator = ""; + let mut was_proof_attempted = false; + for proof_direction in proof_directions { + println!("{}performing {} proof", section_separator, proof_direction); + + section_separator = "\n"; + + reset_proof_results(&mut project); + loop { - let conjecture = find_conjecture(&project, proof_direction); + let conjecture = project.blocks.iter() + .filter_map + ( + |block| + match block + { + ask_dracula::project::Block::Whitespace(_) => None, + ask_dracula::project::Block::Statement(ref statement) => Some(statement), + } + ) + .find(|statement| ask_dracula::format_tptp::is_statement_lemma(&statement, proof_direction)); - let (vampire_result, proof_time) = match conjecture + let conjecture = match conjecture { - None => - { - eprintln!("nothing to prove, exiting"); - return Ok(()); - }, - Some(ref conjecture) => - { - eprintln!("verifying {}: {}", &conjecture.kind, conjecture.formula); - - let tptp_content = format!("{}", ask_dracula::format_tptp::display_project_with_conjecture_tptp(&project, conjecture, proof_direction)); - - run_vampire(&tptp_content, matches.values_of("vampire_arguments").map(|value| value))? - }, + Some(conjecture) => Some(conjecture), + None => project.blocks.iter() + .filter_map + ( + |block| + match block + { + ask_dracula::project::Block::Whitespace(_) => None, + ask_dracula::project::Block::Statement(ref statement) => Some(statement), + } + ) + .find(|statement| ask_dracula::format_tptp::is_statement_theorem(&statement, proof_direction)), }; - let conjecture = find_conjecture_mut(&mut project, proof_direction).unwrap(); + let conjecture = match conjecture + { + Some(ref conjecture) => conjecture, + None => break, + }; + + was_proof_attempted = true; + + eprintln!("verifying {}: {}", &conjecture.kind, conjecture.formula); + + let tptp_content = format!("{}", ask_dracula::format_tptp::display_project_with_conjecture_tptp(&project, conjecture, proof_direction)); + + let (vampire_result, proof_time) + = run_vampire(&tptp_content, matches.values_of("vampire_arguments").map(|value| value))?; match vampire_result { @@ -175,8 +182,36 @@ fn main() -> Result<(), Box> println!("assertion proven"); } - conjecture.kind = ask_dracula::project::StatementKind::Axiom; - conjecture.original_text = replace_statement_kind_regex.replace(&conjecture.original_text, "axiom").to_string(); + // TODO: refactor + let conjecture = project.blocks.iter_mut() + .filter_map + ( + |block| + match block + { + ask_dracula::project::Block::Whitespace(_) => None, + ask_dracula::project::Block::Statement(ref mut statement) => Some(statement), + } + ) + .find(|statement| ask_dracula::format_tptp::is_statement_lemma(&statement, proof_direction)); + + let mut conjecture = match conjecture + { + Some(conjecture) => Some(conjecture), + None => project.blocks.iter_mut() + .filter_map + ( + |block| + match block + { + ask_dracula::project::Block::Whitespace(_) => None, + ask_dracula::project::Block::Statement(ref mut statement) => Some(statement), + } + ) + .find(|statement| ask_dracula::format_tptp::is_statement_theorem(&statement, proof_direction)), + }.unwrap(); + + conjecture.proven = true; }, ProofResult::Satisfiable => { @@ -187,5 +222,11 @@ fn main() -> Result<(), Box> } } + match was_proof_attempted + { + true => println!("finished all proofs"), + false => println!("nothing to verify, exiting"), + } + Ok(()) } diff --git a/src/parse.rs b/src/parse.rs index 34573c9..3d75a3b 100644 --- a/src/parse.rs +++ b/src/parse.rs @@ -161,6 +161,7 @@ pub fn project(i: &str) -> IResult<&str, crate::Project> kind: statement_kind, original_text: statement_original_text.to_string(), formula, + proven: false, }; blocks.push(crate::project::Block::Statement(statement)); @@ -182,6 +183,7 @@ pub fn project(i: &str) -> IResult<&str, crate::Project> // Verify that the whole file has been parsed if i != "" { + eprintln!("parsing error at:\n{}", i); return Err(nom::Err::Error(nom::error::ParseError::from_error_kind(statement_input, nom::error::ErrorKind::Many0))); } diff --git a/src/project.rs b/src/project.rs index 54f2e68..ffeec19 100644 --- a/src/project.rs +++ b/src/project.rs @@ -27,6 +27,7 @@ pub struct Statement pub kind: StatementKind, pub original_text: String, pub formula: foliage::Formula, + pub proven: bool, } pub enum Block