From 3bf78115cf348d7ef9647474063a2963c9a8f03e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Wed, 6 Nov 2019 00:18:30 -0600 Subject: [PATCH] Add completion, assumption, and assertion directives --- src/format.rs | 5 +++-- src/format_tptp.rs | 45 ++++++++++++++++----------------------------- src/main.rs | 12 +++++------- src/parse.rs | 13 +++++++++---- src/project.rs | 5 +++-- 5 files changed, 36 insertions(+), 44 deletions(-) diff --git a/src/format.rs b/src/format.rs index 5364a92..67bdb29 100644 --- a/src/format.rs +++ b/src/format.rs @@ -5,8 +5,9 @@ impl std::fmt::Debug for crate::project::StatementKind match &self { crate::project::StatementKind::Axiom => write!(format, "axiom"), - crate::project::StatementKind::Lemma => write!(format, "lemma"), - crate::project::StatementKind::Conjecture => write!(format, "conjecture"), + crate::project::StatementKind::Completion => write!(format, "completion"), + crate::project::StatementKind::Assumption => write!(format, "assumption"), + crate::project::StatementKind::Assertion => write!(format, "assertion"), } } } diff --git a/src/format_tptp.rs b/src/format_tptp.rs index 62dd832..aa80588 100644 --- a/src/format_tptp.rs +++ b/src/format_tptp.rs @@ -78,12 +78,7 @@ fn collect_predicate_declarations_in_project<'a>(project: &'a crate::Project) match block { crate::project::Block::Whitespace(_) => None, - crate::project::Block::Statement(ref statement) => - match statement.kind - { - crate::project::StatementKind::Axiom => Some(&statement.formula), - _ => None, - } + crate::project::Block::Statement(ref statement) => Some(&statement.formula), }); for formula in formulas @@ -211,12 +206,7 @@ fn collect_symbolic_constants_in_project<'a>(project: &'a crate::Project) match block { crate::project::Block::Whitespace(_) => None, - crate::project::Block::Statement(ref statement) => - match statement.kind - { - crate::project::StatementKind::Axiom => Some(&statement.formula), - _ => None, - } + crate::project::Block::Statement(ref statement) => Some(&statement.formula), }); for formula in formulas @@ -565,8 +555,9 @@ impl<'a> std::fmt::Debug for StatementKindDisplay<'a> match &self.0 { crate::project::StatementKind::Axiom => write!(format, "axiom, axiom"), - crate::project::StatementKind::Lemma => write!(format, "lemma, conjecture"), - crate::project::StatementKind::Conjecture => write!(format, "conjecture, conjecture"), + crate::project::StatementKind::Completion => write!(format, "completion, axiom"), + crate::project::StatementKind::Assumption => write!(format, "assumption, axiom"), + crate::project::StatementKind::Assertion => write!(format, "assertion, conjecture"), } } } @@ -627,35 +618,31 @@ impl<'a, 'input> std::fmt::Debug for ProjectDisplay<'a, 'input> crate::project::Block::Statement(ref statement) => match statement.kind { - crate::project::StatementKind::Axiom => Some(statement), - _ => None, + crate::project::StatementKind::Axiom + | crate::project::StatementKind::Completion + | crate::project::StatementKind::Assumption => Some(statement), + crate::project::StatementKind::Assertion => None, } }); for axiom in axioms { - write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Axiom.display_tptp(), axiom.formula.display_tptp())?; + write!(format, "\ntff({:?}, {:?}).", axiom.kind.display_tptp(), axiom.formula.display_tptp())?; } match self.conjecture.kind { - crate::project::StatementKind::Lemma => + crate::project::StatementKind::Assertion => { - write_title(format, "\n\n", "lemma")?; + write_title(format, "\n\n", "assertion")?; - write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Lemma.display_tptp(), self.conjecture.formula.display_tptp())?; + write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Assertion.display_tptp(), self.conjecture.formula.display_tptp())?; Ok(()) }, - crate::project::StatementKind::Conjecture => - { - write_title(format, "\n\n", "conjecture")?; - - write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Conjecture.display_tptp(), self.conjecture.formula.display_tptp())?; - - Ok(()) - }, - crate::project::StatementKind::Axiom => panic!("unexpected axiom"), + crate::project::StatementKind::Axiom => panic!("unexpected axiom statement"), + crate::project::StatementKind::Completion => panic!("unexpected completion statement"), + crate::project::StatementKind::Assumption => panic!("unexpected assumption statement"), } } } diff --git a/src/main.rs b/src/main.rs index 582d7cf..ba22167 100644 --- a/src/main.rs +++ b/src/main.rs @@ -25,8 +25,7 @@ fn find_conjecture<'a, 'input>(project: &'a ask_dracula::Project<'input>) -> Opt { if let ask_dracula::project::Block::Statement(ref statement) = block { - if statement.kind == ask_dracula::project::StatementKind::Lemma - || statement.kind == ask_dracula::project::StatementKind::Conjecture + if statement.kind == ask_dracula::project::StatementKind::Assertion { return Some(statement) } @@ -42,8 +41,7 @@ fn find_conjecture_mut<'a, 'input>(project: &'a mut ask_dracula::Project<'input> { if let ask_dracula::project::Block::Statement(ref mut statement) = block { - if statement.kind == ask_dracula::project::StatementKind::Lemma - || statement.kind == ask_dracula::project::StatementKind::Conjecture + if statement.kind == ask_dracula::project::StatementKind::Assertion { return Some(statement) } @@ -142,7 +140,7 @@ fn main() -> Result<(), Box> { None => { - eprintln!("no lemma or conjecture found, nothing to do"); + eprintln!("nothing to prove, exiting"); return Ok(()); }, Some(ref conjecture) => @@ -166,10 +164,10 @@ fn main() -> Result<(), Box> }, ProofResult::Refutation => { - println!("conjecture proven"); + println!("assertion proven"); conjecture.kind = ask_dracula::project::StatementKind::Axiom; - let replace_statement_kind_regex = regex::Regex::new(r"(conjecture|lemma)").unwrap(); + let replace_statement_kind_regex = regex::Regex::new(r"(assertion)").unwrap(); let new_text = replace_statement_kind_regex.replace(conjecture.original_text, "axiom"); conjecture.original_text = &new_text; diff --git a/src/parse.rs b/src/parse.rs index 74eb48b..259ec27 100644 --- a/src/parse.rs +++ b/src/parse.rs @@ -42,13 +42,18 @@ fn statement_kind(i: &str) -> IResult<&str, crate::project::StatementKind> ), map ( - tag("lemma:"), - |_| crate::project::StatementKind::Lemma, + tag("completion:"), + |_| crate::project::StatementKind::Completion, ), map ( - tag("conjecture:"), - |_| crate::project::StatementKind::Conjecture, + tag("assumption:"), + |_| crate::project::StatementKind::Assumption, + ), + map + ( + tag("assertion:"), + |_| crate::project::StatementKind::Assertion, ), )), whitespace0, diff --git a/src/project.rs b/src/project.rs index a1e3c3d..20ee70b 100644 --- a/src/project.rs +++ b/src/project.rs @@ -2,8 +2,9 @@ pub enum StatementKind { Axiom, - Lemma, - Conjecture, + Completion, + Assumption, + Assertion, } pub struct Statement<'input>