Implement forward and backward proofs with all new directives correctly

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

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::Axiom => "axiom",
-			(crate::project::StatementKind::Assumption, _) => write!(format, "assumption, axiom"),
+			crate::project::StatementKind::Assumption => "assumption",
-			(crate::project::StatementKind::Completion(_), crate::project::ProofDirection::Forward) => write!(format, "completion, axiom"),
+			crate::project::StatementKind::Completion(_) => "completion",
-			(crate::project::StatementKind::Completion(_), crate::project::ProofDirection::Backward) => write!(format, "completion, conjecture"),
+			crate::project::StatementKind::Assertion => "assertion",
-			(crate::project::StatementKind::Assertion, crate::project::ProofDirection::Forward) => write!(format, "assertion, conjecture"),
+			crate::project::StatementKind::Lemma(_) => "lemma",
-			(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) =>
+		write!(format, "{}, ", identifier)?;
-				match proof_direction == *proof_direction_lemma
+
-				{
+		if is_statement_theorem(&self.statement, self.proof_direction)
-					true => write!(format, "lemma, conjecture"),
+			|| is_statement_lemma(&self.statement, self.proof_direction)
-					false => Ok(()),
+		{
-				},
+			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 => Some(statement),
-							true => None,
+							false => None,
 						}
 				});
 
 		for axiom in axioms
 		{
-			write!(format, "\ntff({:?}, {:?}).",
+			write!(format, "\n{}", display_statement_tptp(&axiom, self.proof_direction))?;
-				display_statement_kind_tptp(&axiom.kind, self.proof_direction), axiom.formula.display_tptp())?;
 		}
 
 		write_title(format, "\n\n", "assertion")?;
 
-		write!(format, "\ntff({:?}, {:?}).",
+		write!(format, "\n{}", display_statement_tptp(&self.conjecture, self.proof_direction))
-			display_statement_kind_tptp(&self.conjecture.kind, self.proof_direction), self.conjecture.formula.display_tptp())?;
-
-		Ok(())
 	}
 }
 

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<I, S>(input: &str, arguments: Option<I>)
 	-> Result<(ProofResult, Option<f32>), ask_dracula::Error>
 	where I: IntoIterator<Item = S>, S: AsRef<std::ffi::OsStr>
@@ -132,30 +108,61 @@ fn main() -> Result<(), Box<dyn std::error::Error>>
 		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 =>
+				Some(conjecture) => Some(conjecture),
-				{
+				None => project.blocks.iter()
-					eprintln!("nothing to prove, exiting");
+					.filter_map
-					return Ok(());
+					(
-				},
+						|block|
-				Some(ref conjecture) =>
+						match block
-				{
+						{
-					eprintln!("verifying {}: {}", &conjecture.kind, conjecture.formula);
+							ask_dracula::project::Block::Whitespace(_) => None,
-
+							ask_dracula::project::Block::Statement(ref statement) => Some(statement),
-					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))?
+					.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<dyn std::error::Error>>
 						println!("assertion proven");
 					}
 
-					conjecture.kind = ask_dracula::project::StatementKind::Axiom;
+					// TODO: refactor
-					conjecture.original_text = replace_statement_kind_regex.replace(&conjecture.original_text, "axiom").to_string();
+					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<dyn std::error::Error>>
 		}
 	}
 
+	match was_proof_attempted
+	{
+		true => println!("finished all proofs"),
+		false => println!("nothing to verify, exiting"),
+	}
+
 	Ok(())
 }

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)));
 	}
 

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