Verify all assertions one after the other

src/format.rs

@@ -20,7 +20,7 @@ impl std::fmt::Display for crate::project::StatementKind
 	}
 }
 
-impl<'input> std::fmt::Debug for crate::Project<'input>
+impl std::fmt::Debug for crate::Project
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
@@ -38,7 +38,7 @@ impl<'input> std::fmt::Debug for crate::Project<'input>
 	}
 }
 
-impl<'input> std::fmt::Display for crate::Project<'input>
+impl std::fmt::Display for crate::Project
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{

src/format_tptp.rs

@@ -222,10 +222,10 @@ 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, 'input>
+pub struct ProjectDisplay<'a>
 {
-	project: &'a crate::project::Project<'input>,
+	project: &'a crate::project::Project,
-	conjecture: &'a crate::project::Statement<'input>,
+	conjecture: &'a crate::project::Statement,
 }
 
 impl<'a> DisplayTPTP<'a, VariableDeclarationDisplay<'a>> for foliage::VariableDeclaration
@@ -268,8 +268,8 @@ impl<'a> DisplayTPTP<'a, StatementKindDisplay<'a>> for crate::project::Statement
 	}
 }
 
-pub fn display_project_with_conjecture_tptp<'a, 'input>(project: &'a crate::Project<'input>,
+pub fn display_project_with_conjecture_tptp<'a>(project: &'a crate::Project,
-	conjecture: &'a crate::project::Statement<'input>) -> ProjectDisplay<'a, 'input>
+	conjecture: &'a crate::project::Statement) -> ProjectDisplay<'a>
 {
 	ProjectDisplay
 	{
@@ -570,7 +570,7 @@ impl<'a> std::fmt::Display for StatementKindDisplay<'a>
 	}
 }
 
-impl<'a, 'input> std::fmt::Debug for ProjectDisplay<'a, 'input>
+impl<'a> std::fmt::Debug for ProjectDisplay<'a>
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
@@ -647,7 +647,7 @@ impl<'a, 'input> std::fmt::Debug for ProjectDisplay<'a, 'input>
 	}
 }
 
-impl<'a, 'input> std::fmt::Display for ProjectDisplay<'a, 'input>
+impl<'a> std::fmt::Display for ProjectDisplay<'a>
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{

src/main.rs

@@ -19,7 +19,7 @@ fn backup_file_path(file_path: &std::path::Path) -> Result<std::path::PathBuf, a
 	}
 }
 
-fn find_conjecture<'a, 'input>(project: &'a ask_dracula::Project<'input>) -> Option<&'a ask_dracula::project::Statement<'input>>
+fn find_conjecture<'a>(project: &'a ask_dracula::Project) -> Option<&'a ask_dracula::project::Statement>
 {
 	for block in &project.blocks
 	{
@@ -35,7 +35,7 @@ fn find_conjecture<'a, 'input>(project: &'a ask_dracula::Project<'input>) -> Opt
 	None
 }
 
-fn find_conjecture_mut<'a, 'input>(project: &'a mut ask_dracula::Project<'input>) -> Option<&'a mut ask_dracula::project::Statement<'input>>
+fn find_conjecture_mut<'a>(project: &'a mut ask_dracula::Project) -> Option<&'a mut ask_dracula::project::Statement>
 {
 	for block in &mut project.blocks
 	{
@@ -134,60 +134,61 @@ fn main() -> Result<(), Box<dyn std::error::Error>>
 	let (_, mut project) = ask_dracula::parse::project(&file_content)
 		.map_err(|_| "couldn’t parse input file")?;
 
-	let conjecture = find_conjecture(&project);
+	let replace_statement_kind_regex = regex::Regex::new(r"(assertion)").unwrap();
 
-	let vampire_result = match conjecture
+	loop
 	{
-		None =>
+		let conjecture = find_conjecture(&project);
+
+		let vampire_result = match conjecture
 		{
-			eprintln!("nothing to prove, exiting");
+			None =>
-			return Ok(());
+			{
-		},
+				eprintln!("nothing to prove, exiting");
-		Some(ref conjecture) =>
+				return Ok(());
+			},
+			Some(ref conjecture) =>
+			{
+				eprintln!("verifying assertion: {}", conjecture.formula);
+
+				let tptp_content = format!("{}", ask_dracula::format_tptp::display_project_with_conjecture_tptp(&project, conjecture));
+
+				run_vampire(&tptp_content, matches.values_of("vampire_arguments").map(|value| value))?
+			},
+		};
+
+		let conjecture = find_conjecture_mut(&mut project).unwrap();
+
+		match vampire_result
 		{
-			eprintln!("verifying conjecture: {}", conjecture.formula);
+			ProofResult::ProofNotFound =>
+			{
+				println!("proof not found");
+				return Ok(());
+			},
+			ProofResult::Refutation =>
+			{
+				println!("assertion proven");
 
-			let tptp_content = format!("{}", ask_dracula::format_tptp::display_project_with_conjecture_tptp(&project, conjecture));
+				conjecture.kind = ask_dracula::project::StatementKind::Axiom;
+				conjecture.original_text = replace_statement_kind_regex.replace(&conjecture.original_text, "axiom").to_string();
 
-			run_vampire(&tptp_content, matches.values_of("vampire_arguments").map(|value| value))?
+				let backup_file_path = backup_file_path(file_path)?;
-		},
-	};
 
-	let conjecture = find_conjecture_mut(&mut project).unwrap();
+				// 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))?;
 
-	match vampire_result
+				// Write updated version of the file
-	{
+				let file_content = format!("{}", project);
-		ProofResult::ProofNotFound =>
+				std::fs::write(file_path, &file_content)
-		{
+					.map_err(|error| ask_dracula::Error::new_write_file(file_path.to_owned(), error))?;
-			println!("proof not found");
+			},
-			Ok(())
+			ProofResult::Satisfiable =>
-		},
+			{
-		ProofResult::Refutation =>
+				println!("assertion disproven");
-		{
+				return Ok(());
-			println!("assertion proven");
+			},
-
+		}
-			conjecture.kind = ask_dracula::project::StatementKind::Axiom;
-			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;
-
-			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(())
-		},
-		ProofResult::Satisfiable =>
-		{
-			println!("conjecture disproven");
-			Ok(())
-		},
 	}
 }

src/parse.rs

@@ -109,13 +109,13 @@ pub fn project(i: &str) -> IResult<&str, crate::Project>
 
 				if !whitespace_before.is_empty()
 				{
-					blocks.push(crate::project::Block::Whitespace(whitespace_before));
+					blocks.push(crate::project::Block::Whitespace(whitespace_before.to_string()));
 				}
 
 				let statement = crate::project::Statement
 				{
 					kind: statement_kind,
-					original_text: statement_original_text,
+					original_text: statement_original_text.to_string(),
 					formula,
 				};
 
@@ -123,7 +123,7 @@ pub fn project(i: &str) -> IResult<&str, crate::Project>
 
 				if !whitespace_after.is_empty()
 				{
-					blocks.push(crate::project::Block::Whitespace(whitespace_after));
+					blocks.push(crate::project::Block::Whitespace(whitespace_after.to_string()));
 				}
 
 				statement_input = i;

src/project.rs

@@ -7,20 +7,20 @@ pub enum StatementKind
 	Assertion,
 }
 
-pub struct Statement<'input>
+pub struct Statement
 {
 	pub kind: StatementKind,
-	pub original_text: &'input str,
+	pub original_text: String,
 	pub formula: foliage::Formula,
 }
 
-pub enum Block<'input>
+pub enum Block
 {
-	Statement(Statement<'input>),
+	Statement(Statement),
-	Whitespace(&'input str),
+	Whitespace(String),
 }
 
-pub struct Project<'input>
+pub struct Project
 {
-	pub blocks: Vec<Block<'input>>,
+	pub blocks: Vec<Block>,
 }