diff --git a/src/format.rs b/src/format.rs index aabcc37..372480c 100644 --- a/src/format.rs +++ b/src/format.rs @@ -18,28 +18,28 @@ impl std::fmt::Display for crate::project::ProofDirection } } -impl std::fmt::Debug for crate::project::StatementKind +impl std::fmt::Debug for crate::project::FormulaStatementKind { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { match &self { - crate::project::StatementKind::Axiom => write!(format, "axiom"), - crate::project::StatementKind::Completion( + crate::project::FormulaStatementKind::Axiom => write!(format, "axiom"), + crate::project::FormulaStatementKind::Completion( crate::project::CompletionTarget::Predicate(predicate_declaration)) => write!(format, "completion({}/{})", predicate_declaration.name, predicate_declaration.arity), - crate::project::StatementKind::Completion(crate::project::CompletionTarget::Constraint) + crate::project::FormulaStatementKind::Completion(crate::project::CompletionTarget::Constraint) => write!(format, "completion(constraint)"), - crate::project::StatementKind::Assumption => write!(format, "assumption"), - crate::project::StatementKind::Assertion => write!(format, "assertion"), - crate::project::StatementKind::Lemma(None) => write!(format, "lemma"), - crate::project::StatementKind::Lemma(Some(crate::project::ProofDirection::Forward)) => write!(format, "lemma(forward)"), - crate::project::StatementKind::Lemma(Some(crate::project::ProofDirection::Backward)) => write!(format, "lemma(backward)"), + crate::project::FormulaStatementKind::Assumption => write!(format, "assumption"), + crate::project::FormulaStatementKind::Assertion => write!(format, "assertion"), + crate::project::FormulaStatementKind::Lemma(None) => write!(format, "lemma"), + crate::project::FormulaStatementKind::Lemma(Some(crate::project::ProofDirection::Forward)) => write!(format, "lemma(forward)"), + crate::project::FormulaStatementKind::Lemma(Some(crate::project::ProofDirection::Backward)) => write!(format, "lemma(backward)"), } } } -impl std::fmt::Display for crate::project::StatementKind +impl std::fmt::Display for crate::project::FormulaStatementKind { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -56,8 +56,8 @@ impl std::fmt::Debug for crate::Project match block { crate::project::Block::Whitespace(ref text) => write!(format, "{}", text)?, - crate::project::Block::Statement(ref statement) => - write!(format, "{}", statement.original_text)?, + crate::project::Block::FormulaStatement(ref formula_statement) => + write!(format, "{}", formula_statement.original_text)?, } } diff --git a/src/format_tptp.rs b/src/format_tptp.rs index cdf34da..499eef3 100644 --- a/src/format_tptp.rs +++ b/src/format_tptp.rs @@ -4,52 +4,52 @@ pub trait DisplayTPTP<'a, DisplayType> fn display_tptp(&'a self) -> DisplayType; } -pub fn is_statement_axiom(statement: &crate::project::Statement, +pub fn is_formula_statement_axiom(formula_statement: &crate::project::FormulaStatement, proof_direction: crate::project::ProofDirection) -> bool { - if statement.proven + if formula_statement.proven { return true; } - match (proof_direction, &statement.kind) + match (proof_direction, &formula_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, + (_, crate::project::FormulaStatementKind::Axiom) => true, + (_, crate::project::FormulaStatementKind::Assumption) => true, + (crate::project::ProofDirection::Forward, crate::project::FormulaStatementKind::Completion(_)) => true, + (crate::project::ProofDirection::Backward, crate::project::FormulaStatementKind::Assertion) => true, _ => false, } } -pub fn is_statement_lemma(statement: &crate::project::Statement, +pub fn is_formula_statement_lemma(formula_statement: &crate::project::FormulaStatement, proof_direction: crate::project::ProofDirection) -> bool { - if statement.proven + if formula_statement.proven { return false; } - match (proof_direction, &statement.kind) + match (proof_direction, &formula_statement.kind) { - (_, crate::project::StatementKind::Lemma(None)) => true, - (proof_direction, crate::project::StatementKind::Lemma(Some(proof_direction_lemma))) => proof_direction == *proof_direction_lemma, + (_, crate::project::FormulaStatementKind::Lemma(None)) => true, + (proof_direction, crate::project::FormulaStatementKind::Lemma(Some(proof_direction_lemma))) => proof_direction == *proof_direction_lemma, _ => false, } } -pub fn is_statement_theorem(statement: &crate::project::Statement, +pub fn is_formula_statement_theorem(formula_statement: &crate::project::FormulaStatement, proof_direction: crate::project::ProofDirection) -> bool { - if statement.proven + if formula_statement.proven { return false; } - match (proof_direction, &statement.kind) + match (proof_direction, &formula_statement.kind) { - (crate::project::ProofDirection::Forward, crate::project::StatementKind::Assertion) => true, - (crate::project::ProofDirection::Backward, crate::project::StatementKind::Completion(_)) => true, + (crate::project::ProofDirection::Forward, crate::project::FormulaStatementKind::Assertion) => true, + (crate::project::ProofDirection::Backward, crate::project::FormulaStatementKind::Completion(_)) => true, _ => false, } } @@ -128,7 +128,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) => Some(&statement.formula), + crate::project::Block::FormulaStatement(ref formula_statement) => Some(&formula_statement.formula), }); for formula in formulas @@ -256,7 +256,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) => Some(&statement.formula), + crate::project::Block::FormulaStatement(ref formula_statement) => Some(&formula_statement.formula), }); for formula in formulas @@ -271,15 +271,15 @@ 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 StatementDisplay<'a> +struct FormulaStatementDisplay<'a> { - statement: &'a crate::project::Statement, + formula_statement: &'a crate::project::FormulaStatement, proof_direction: crate::project::ProofDirection, } pub struct ProjectDisplay<'a> { project: &'a crate::project::Project, - conjecture: &'a crate::project::Statement, + conjecture: &'a crate::project::FormulaStatement, proof_direction: crate::project::ProofDirection, } @@ -315,19 +315,19 @@ impl<'a> DisplayTPTP<'a, FormulaDisplay<'a>> for foliage::Formula } } -fn display_statement_tptp<'a>(statement: &'a crate::project::Statement, +fn display_formula_statement_tptp<'a>(formula_statement: &'a crate::project::FormulaStatement, proof_direction: crate::project::ProofDirection) - -> StatementDisplay<'a> + -> FormulaStatementDisplay<'a> { - StatementDisplay + FormulaStatementDisplay { - statement, + formula_statement, proof_direction, } } pub fn display_project_with_conjecture_tptp<'a>(project: &'a crate::Project, - conjecture: &'a crate::project::Statement, proof_direction: crate::project::ProofDirection) + conjecture: &'a crate::project::FormulaStatement, proof_direction: crate::project::ProofDirection) -> ProjectDisplay<'a> { ProjectDisplay @@ -612,42 +612,42 @@ impl<'a> std::fmt::Display for FormulaDisplay<'a> } } -impl<'a> std::fmt::Debug for StatementDisplay<'a> +impl<'a> std::fmt::Debug for FormulaStatementDisplay<'a> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { write!(format, "\ntff(")?; - let identifier = match &self.statement.kind + let identifier = match &self.formula_statement.kind { - 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", + crate::project::FormulaStatementKind::Axiom => "axiom", + crate::project::FormulaStatementKind::Assumption => "assumption", + crate::project::FormulaStatementKind::Completion(_) => "completion", + crate::project::FormulaStatementKind::Assertion => "assertion", + crate::project::FormulaStatementKind::Lemma(_) => "lemma", }; write!(format, "{}, ", identifier)?; - if is_statement_theorem(&self.statement, self.proof_direction) - || is_statement_lemma(&self.statement, self.proof_direction) + if is_formula_statement_theorem(&self.formula_statement, self.proof_direction) + || is_formula_statement_lemma(&self.formula_statement, self.proof_direction) { write!(format, "conjecture")?; } - else if is_statement_axiom(&self.statement, self.proof_direction) + else if is_formula_statement_axiom(&self.formula_statement, self.proof_direction) { write!(format, "axiom")?; } else { - panic!("expected statement to be either theorem, lemma, or axiom, please report to bug tracker"); + panic!("expected formula statement to be either theorem, lemma, or axiom, please report to bug tracker"); } - write!(format, ", {:?}).", self.statement.formula.display_tptp()) + write!(format, ", {:?}).", self.formula_statement.formula.display_tptp()) } } -impl<'a> std::fmt::Display for StatementDisplay<'a> +impl<'a> std::fmt::Display for FormulaStatementDisplay<'a> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -700,22 +700,22 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a> match block { crate::project::Block::Whitespace(_) => None, - crate::project::Block::Statement(ref statement) => - match is_statement_axiom(&statement, self.proof_direction) + crate::project::Block::FormulaStatement(ref formula_statement) => + match is_formula_statement_axiom(&formula_statement, self.proof_direction) { - true => Some(statement), + true => Some(formula_statement), false => None, } }); for axiom in axioms { - write!(format, "\n{}", display_statement_tptp(&axiom, self.proof_direction))?; + write!(format, "\n{}", display_formula_statement_tptp(&axiom, self.proof_direction))?; } write_title(format, "\n\n", "assertion")?; - write!(format, "\n{}", display_statement_tptp(&self.conjecture, self.proof_direction)) + write!(format, "\n{}", display_formula_statement_tptp(&self.conjecture, self.proof_direction)) } } diff --git a/src/main.rs b/src/main.rs index 671bd9f..4fcbbf6 100644 --- a/src/main.rs +++ b/src/main.rs @@ -12,7 +12,7 @@ fn reset_proof_results<'a>(project: &'a mut ask_dracula::Project) match block { ask_dracula::project::Block::Whitespace(_) => (), - ask_dracula::project::Block::Statement(ref mut statement) => statement.proven = false, + ask_dracula::project::Block::FormulaStatement(ref mut formula_statement) => formula_statement.proven = false, } } } @@ -128,10 +128,10 @@ fn main() -> Result<(), Box> match block { ask_dracula::project::Block::Whitespace(_) => None, - ask_dracula::project::Block::Statement(ref statement) => Some(statement), + ask_dracula::project::Block::FormulaStatement(ref formula_statement) => Some(formula_statement), } ) - .find(|statement| ask_dracula::format_tptp::is_statement_lemma(&statement, proof_direction)); + .find(|formula_statement| ask_dracula::format_tptp::is_formula_statement_lemma(&formula_statement, proof_direction)); let conjecture = match conjecture { @@ -143,10 +143,10 @@ fn main() -> Result<(), Box> match block { ask_dracula::project::Block::Whitespace(_) => None, - ask_dracula::project::Block::Statement(ref statement) => Some(statement), + ask_dracula::project::Block::FormulaStatement(ref formula_statement) => Some(formula_statement), } ) - .find(|statement| ask_dracula::format_tptp::is_statement_theorem(&statement, proof_direction)), + .find(|formula_statement| ask_dracula::format_tptp::is_formula_statement_theorem(&formula_statement, proof_direction)), }; let conjecture = match conjecture @@ -190,10 +190,10 @@ fn main() -> Result<(), Box> match block { ask_dracula::project::Block::Whitespace(_) => None, - ask_dracula::project::Block::Statement(ref mut statement) => Some(statement), + ask_dracula::project::Block::FormulaStatement(ref mut formula_statement) => Some(formula_statement), } ) - .find(|statement| ask_dracula::format_tptp::is_statement_lemma(&statement, proof_direction)); + .find(|formula_statement| ask_dracula::format_tptp::is_formula_statement_lemma(&formula_statement, proof_direction)); let mut conjecture = match conjecture { @@ -205,10 +205,10 @@ fn main() -> Result<(), Box> match block { ask_dracula::project::Block::Whitespace(_) => None, - ask_dracula::project::Block::Statement(ref mut statement) => Some(statement), + ask_dracula::project::Block::FormulaStatement(ref mut formula_statement) => Some(formula_statement), } ) - .find(|statement| ask_dracula::format_tptp::is_statement_theorem(&statement, proof_direction)), + .find(|formula_statement| ask_dracula::format_tptp::is_formula_statement_theorem(&formula_statement, proof_direction)), }.unwrap(); conjecture.proven = true; diff --git a/src/parse.rs b/src/parse.rs index 3d75a3b..974da76 100644 --- a/src/parse.rs +++ b/src/parse.rs @@ -29,7 +29,7 @@ where } } -fn statement_kind(i: &str) -> IResult<&str, crate::project::StatementKind> +fn formula_statement_kind(i: &str) -> IResult<&str, crate::project::FormulaStatementKind> { let foo = delimited ( @@ -39,12 +39,12 @@ fn statement_kind(i: &str) -> IResult<&str, crate::project::StatementKind> map ( tag("axiom:"), - |_| crate::project::StatementKind::Axiom, + |_| crate::project::FormulaStatementKind::Axiom, ), map ( tag("completion(constraint):"), - |_| crate::project::StatementKind::Completion(crate::project::CompletionTarget::Constraint), + |_| crate::project::FormulaStatementKind::Completion(crate::project::CompletionTarget::Constraint), ), map ( @@ -69,7 +69,7 @@ fn statement_kind(i: &str) -> IResult<&str, crate::project::StatementKind> |(name, arity)| match arity.parse::() { - Ok(arity) => crate::project::StatementKind::Completion( + Ok(arity) => crate::project::FormulaStatementKind::Completion( crate::project::CompletionTarget::Predicate(foliage::PredicateDeclaration{name, arity})), Err(error) => panic!("invalid arity “{}”: {}", arity, error), } @@ -77,27 +77,27 @@ fn statement_kind(i: &str) -> IResult<&str, crate::project::StatementKind> map ( tag("assumption:"), - |_| crate::project::StatementKind::Assumption, + |_| crate::project::FormulaStatementKind::Assumption, ), map ( tag("lemma(forward):"), - |_| crate::project::StatementKind::Lemma(Some(crate::project::ProofDirection::Forward)), + |_| crate::project::FormulaStatementKind::Lemma(Some(crate::project::ProofDirection::Forward)), ), map ( tag("lemma(backward):"), - |_| crate::project::StatementKind::Lemma(Some(crate::project::ProofDirection::Backward)), + |_| crate::project::FormulaStatementKind::Lemma(Some(crate::project::ProofDirection::Backward)), ), map ( tag("lemma:"), - |_| crate::project::StatementKind::Lemma(None), + |_| crate::project::FormulaStatementKind::Lemma(None), ), map ( tag("assertion:"), - |_| crate::project::StatementKind::Assertion, + |_| crate::project::FormulaStatementKind::Assertion, ), )), whitespace0, @@ -106,13 +106,13 @@ fn statement_kind(i: &str) -> IResult<&str, crate::project::StatementKind> foo } -fn statement(i: &str) -> IResult<&str, (crate::project::StatementKind, foliage::Formula)> +fn formula_statement(i: &str) -> IResult<&str, (crate::project::FormulaStatementKind, foliage::Formula)> { terminated ( pair ( - statement_kind, + formula_statement_kind, foliage::formula, ), preceded @@ -123,12 +123,13 @@ fn statement(i: &str) -> IResult<&str, (crate::project::StatementKind, foliage:: )(i) } -fn statement_enclosed_by_whitespace(i: &str) -> IResult<&str, (&str, (&str, (crate::project::StatementKind, foliage::Formula)), &str)> +fn formula_statement_enclosed_by_whitespace(i: &str) + -> IResult<&str, (&str, (&str, (crate::project::FormulaStatementKind, foliage::Formula)), &str)> { tuple (( recognize(whitespace0), - recognize_and_keep(statement), + recognize_and_keep(formula_statement), recognize(whitespace0), ))(i) } @@ -141,9 +142,9 @@ pub fn project(i: &str) -> IResult<&str, crate::Project> loop { let i_ = statement_input.clone(); - match statement_enclosed_by_whitespace(i_) + match formula_statement_enclosed_by_whitespace(i_) { - Ok((i, (whitespace_before, (statement_original_text, (statement_kind, formula)), whitespace_after))) => + Ok((i, (whitespace_before, (formula_statement_original_text, (formula_statement_kind, formula)), whitespace_after))) => { // Iteration must always consume input (to prevent infinite loops) if i == statement_input @@ -156,15 +157,15 @@ pub fn project(i: &str) -> IResult<&str, crate::Project> blocks.push(crate::project::Block::Whitespace(whitespace_before.to_string())); } - let statement = crate::project::Statement + let formula_statement = crate::project::FormulaStatement { - kind: statement_kind, - original_text: statement_original_text.to_string(), + kind: formula_statement_kind, + original_text: formula_statement_original_text.to_string(), formula, proven: false, }; - blocks.push(crate::project::Block::Statement(statement)); + blocks.push(crate::project::Block::FormulaStatement(formula_statement)); if !whitespace_after.is_empty() { diff --git a/src/project.rs b/src/project.rs index ffeec19..a30a8dd 100644 --- a/src/project.rs +++ b/src/project.rs @@ -13,7 +13,7 @@ pub enum CompletionTarget } #[derive(Eq, Hash, PartialEq)] -pub enum StatementKind +pub enum FormulaStatementKind { Axiom, Completion(CompletionTarget), @@ -22,9 +22,9 @@ pub enum StatementKind Assertion, } -pub struct Statement +pub struct FormulaStatement { - pub kind: StatementKind, + pub kind: FormulaStatementKind, pub original_text: String, pub formula: foliage::Formula, pub proven: bool, @@ -32,7 +32,7 @@ pub struct Statement pub enum Block { - Statement(Statement), + FormulaStatement(FormulaStatement), Whitespace(String), }