diff --git a/foliage b/foliage index 5070965..8a7bd65 160000 --- a/foliage +++ b/foliage @@ -1 +1 @@ -Subproject commit 5070965bfee7ad8a0af0d4abc0f8c6d07b7ae5ec +Subproject commit 8a7bd651b217a37f6d95faaa2d4bc1221631e88b diff --git a/src/format.rs b/src/format.rs index 4419a95..5364a92 100644 --- a/src/format.rs +++ b/src/format.rs @@ -19,45 +19,17 @@ impl std::fmt::Display for crate::project::StatementKind } } -impl std::fmt::Debug for crate::Project +impl<'input> std::fmt::Debug for crate::Project<'input> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - let mut line_separator = ""; - let mut section_separator = ""; - - if let Some(axioms) = self.statements.get(&crate::project::StatementKind::Axiom) + for block in &self.blocks { - for axiom in axioms + match block { - write!(format, "{}{:?}: {:?}.", line_separator, crate::project::StatementKind::Axiom, axiom)?; - line_separator = "\n"; - } - - section_separator = "\n"; - } - - if let Some(lemmas) = self.statements.get(&crate::project::StatementKind::Lemma) - { - write!(format, "{}", section_separator)?; - - for lemma in lemmas - { - write!(format, "{}{:?}: {:?}.", line_separator, crate::project::StatementKind::Lemma, lemma)?; - line_separator = "\n"; - } - - section_separator = "\n"; - } - - if let Some(conjectures) = self.statements.get(&crate::project::StatementKind::Conjecture) - { - write!(format, "{}", section_separator)?; - - for conjecture in conjectures - { - write!(format, "{}{:?}: {:?}.", line_separator, crate::project::StatementKind::Conjecture, conjecture)?; - line_separator = "\n"; + crate::project::Block::Whitespace(ref text) => write!(format, "{}", text)?, + crate::project::Block::Statement(ref statement) => + write!(format, "{}", statement.original_text)?, } } @@ -65,7 +37,7 @@ impl std::fmt::Debug for crate::Project } } -impl std::fmt::Display for crate::Project +impl<'input> std::fmt::Display for crate::Project<'input> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { diff --git a/src/format_tptp.rs b/src/format_tptp.rs index dfc81e0..93ff55b 100644 --- a/src/format_tptp.rs +++ b/src/format_tptp.rs @@ -72,12 +72,23 @@ fn collect_predicate_declarations_in_project<'a>(project: &'a crate::Project) { let mut predicate_declarations = std::collections::HashSet::new(); - for (_, formulas) in project.statements.iter() + let formulas = project.blocks.iter() + .filter_map( + |block| + match block + { + crate::project::Block::Whitespace(_) => None, + crate::project::Block::Statement(ref statement) => + match statement.kind + { + crate::project::StatementKind::Axiom => Some(&statement.formula), + _ => None, + } + }); + + for formula in formulas { - for formula in formulas.iter() - { - collect_predicate_declarations_in_formula(&mut predicate_declarations, formula); - } + collect_predicate_declarations_in_formula(&mut predicate_declarations, formula); } predicate_declarations @@ -193,12 +204,24 @@ fn collect_symbolic_constants_in_project<'a>(project: &'a crate::Project) { let mut symbolic_constants = std::collections::HashSet::new(); - for (_, formulas) in project.statements.iter() + // TODO: avoid code duplication + let formulas = project.blocks.iter() + .filter_map( + |block| + match block + { + crate::project::Block::Whitespace(_) => None, + crate::project::Block::Statement(ref statement) => + match statement.kind + { + crate::project::StatementKind::Axiom => Some(&statement.formula), + _ => None, + } + }); + + for formula in formulas { - for formula in formulas.iter() - { - collect_symbolic_constants_in_formula(&mut symbolic_constants, formula); - } + collect_symbolic_constants_in_formula(&mut symbolic_constants, formula); } symbolic_constants @@ -209,10 +232,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> +pub struct ProjectDisplay<'a, 'input> { - project: &'a crate::project::Project, - conjecture: (crate::project::StatementKind, &'a foliage::Formula), + project: &'a crate::project::Project<'input>, + conjecture: &'a crate::project::Statement<'input>, } impl<'a> DisplayTPTP<'a, VariableDeclarationDisplay<'a>> for foliage::VariableDeclaration @@ -255,8 +278,8 @@ impl<'a> DisplayTPTP<'a, StatementKindDisplay<'a>> for crate::project::Statement } } -pub fn display_project_with_conjecture_tptp<'a>(project: &'a crate::Project, - conjecture: (crate::project::StatementKind, &'a foliage::Formula)) -> ProjectDisplay<'a> +pub fn display_project_with_conjecture_tptp<'a, 'input>(project: &'a crate::Project<'input>, + conjecture: &'a crate::project::Statement<'input>) -> ProjectDisplay<'a, 'input> { ProjectDisplay { @@ -554,7 +577,7 @@ impl<'a> std::fmt::Display for StatementKindDisplay<'a> } } -impl<'a> std::fmt::Debug for ProjectDisplay<'a> +impl<'a, 'input> std::fmt::Debug for ProjectDisplay<'a, 'input> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -593,40 +616,49 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a> } } - if let Some(axioms) = self.project.statements.get(&crate::project::StatementKind::Axiom) - { - write_title(format, "\n\n", "axioms")?; + let axioms = self.project.blocks.iter() + .filter_map( + |block| + match block + { + crate::project::Block::Whitespace(_) => None, + crate::project::Block::Statement(ref statement) => + match statement.kind + { + crate::project::StatementKind::Axiom => Some(statement), + _ => None, + } + }); - for axiom in axioms - { - write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Axiom.display_tptp(), axiom.display_tptp())?; - } + for axiom in axioms + { + write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Axiom.display_tptp(), axiom.formula.display_tptp())?; } - match self.conjecture + match self.conjecture.kind { - (crate::project::StatementKind::Lemma, ref lemma) => + crate::project::StatementKind::Lemma => { write_title(format, "\n\n", "lemma")?; - write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Lemma.display_tptp(), lemma.display_tptp())?; + write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Lemma.display_tptp(), self.conjecture.formula.display_tptp())?; Ok(()) }, - (crate::project::StatementKind::Conjecture, ref conjecture) => + crate::project::StatementKind::Conjecture => { write_title(format, "\n\n", "conjecture")?; - write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Conjecture.display_tptp(), conjecture.display_tptp())?; + 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"), } } } -impl<'a> std::fmt::Display for ProjectDisplay<'a> +impl<'a, 'input> std::fmt::Display for ProjectDisplay<'a, 'input> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { diff --git a/src/main.rs b/src/main.rs index 624f000..582d7cf 100644 --- a/src/main.rs +++ b/src/main.rs @@ -19,28 +19,41 @@ fn backup_file_path(file_path: &std::path::Path) -> Result(project: &'a ask_dracula::Project) -> Option<(ask_dracula::project::StatementKind, &'a foliage::Formula)> +fn find_conjecture<'a, 'input>(project: &'a ask_dracula::Project<'input>) -> Option<&'a ask_dracula::project::Statement<'input>> { - if let Some(lemmas) = project.statements.get(&ask_dracula::project::StatementKind::Lemma) + for block in &project.blocks { - if let Some(lemma) = lemmas.first() + if let ask_dracula::project::Block::Statement(ref statement) = block { - return Some((ask_dracula::project::StatementKind::Lemma, lemma)); - } - } - - if let Some(conjectures) = project.statements.get(&ask_dracula::project::StatementKind::Conjecture) - { - if let Some(conjecture) = conjectures.first() - { - return Some((ask_dracula::project::StatementKind::Conjecture, conjecture)); + if statement.kind == ask_dracula::project::StatementKind::Lemma + || statement.kind == ask_dracula::project::StatementKind::Conjecture + { + return Some(statement) + } } } None } -enum VampireResult +fn find_conjecture_mut<'a, 'input>(project: &'a mut ask_dracula::Project<'input>) -> Option<&'a mut ask_dracula::project::Statement<'input>> +{ + for block in &mut project.blocks + { + 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 + { + return Some(statement) + } + } + } + + None +} + +enum ProofResult { ProofNotFound, Refutation, @@ -48,7 +61,7 @@ enum VampireResult } fn run_vampire(input: &str, arguments: Option) - -> Result + -> Result where I: IntoIterator, S: AsRef { let mut vampire = std::process::Command::new("vampire"); @@ -59,6 +72,8 @@ fn run_vampire(input: &str, arguments: Option) None => &mut vampire, }; + //eprintln!("{}", input); + let mut vampire = vampire .stdin(std::process::Stdio::piped()) .stdout(std::process::Stdio::piped()) @@ -89,7 +104,7 @@ fn run_vampire(input: &str, arguments: Option) if proof_not_found_regex.is_match(stdout) { - return Ok(VampireResult::ProofNotFound); + return Ok(ProofResult::ProofNotFound); } return Err(ask_dracula::Error::new_run_vampire( @@ -100,7 +115,7 @@ fn run_vampire(input: &str, arguments: Option) if refutation_regex.is_match(stdout) { - return Ok(VampireResult::Refutation); + return Ok(ProofResult::Refutation); } Err(ask_dracula::Error::new_interpret_vampire_output(stdout.to_string(), stderr.to_string())) @@ -121,52 +136,60 @@ fn main() -> Result<(), Box> let (_, mut project) = ask_dracula::parse::project(&file_content) .map_err(|_| "couldn’t parse input file")?; - match find_conjecture(&project) + let conjecture = find_conjecture(&project); + + let vampire_result = match conjecture { None => { eprintln!("no lemma or conjecture found, nothing to do"); + return Ok(()); + }, + Some(ref conjecture) => + { + eprintln!("verifying conjecture: {}", 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 + { + ProofResult::ProofNotFound => + { + println!("proof not found"); Ok(()) }, - Some((ref statement_kind, ref conjecture)) => + ProofResult::Refutation => { - eprintln!("verifying conjecture: {}", conjecture); + println!("conjecture proven"); - let tptp_content = format!("{}", ask_dracula::format_tptp::display_project_with_conjecture_tptp(&project, (statement_kind.clone(), conjecture))); + conjecture.kind = ask_dracula::project::StatementKind::Axiom; + let replace_statement_kind_regex = regex::Regex::new(r"(conjecture|lemma)").unwrap(); + let new_text = replace_statement_kind_regex.replace(conjecture.original_text, "axiom"); + conjecture.original_text = &new_text; - match run_vampire(&tptp_content, matches.values_of("vampire_arguments").map(|value| value))? - { - VampireResult::ProofNotFound => - { - println!("proof not found"); - Ok(()) - }, - VampireResult::Refutation => - { - println!("conjecture proven"); + let backup_file_path = backup_file_path(file_path)?; - let axiom = project.statements.get_mut(statement_kind).unwrap().remove(0); - project.statements.entry(ask_dracula::project::StatementKind::Axiom).or_insert_with(Vec::new).push(axiom); + // 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))?; - let backup_file_path = backup_file_path(file_path)?; + // 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))?; - // 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(()) - }, - VampireResult::Satisfiable => - { - println!("conjecture disproven"); - Ok(()) - }, - } + Ok(()) + }, + ProofResult::Satisfiable => + { + println!("conjecture disproven"); + Ok(()) }, } } diff --git a/src/parse.rs b/src/parse.rs index bc3d47f..74eb48b 100644 --- a/src/parse.rs +++ b/src/parse.rs @@ -1,18 +1,38 @@ use nom:: { IResult, - character::complete::multispace0, - sequence::{delimited, pair, terminated}, - combinator::map, + sequence::{delimited, pair, preceded, terminated, tuple}, + combinator::{map, recognize}, branch::alt, bytes::complete::tag, }; +use foliage::parse::whitespace0; + +pub fn recognize_and_keep>, O, E: nom::error::ParseError, F>(parser: F) -> impl Fn(I) -> IResult +where + F: Fn(I) -> IResult, +{ + move |input: I| + { + let i = input.clone(); + match parser(i) + { + Ok((i, result)) => + { + let index = input.offset(&i); + Ok((i, (input.slice(..index), result))) + }, + Err(e) => Err(e), + } + } +} + fn statement_kind(i: &str) -> IResult<&str, crate::project::StatementKind> { let foo = delimited ( - multispace0, + whitespace0, alt (( map @@ -31,7 +51,7 @@ fn statement_kind(i: &str) -> IResult<&str, crate::project::StatementKind> |_| crate::project::StatementKind::Conjecture, ), )), - multispace0, + whitespace0, )(i); foo @@ -46,26 +66,35 @@ fn statement(i: &str) -> IResult<&str, (crate::project::StatementKind, foliage:: statement_kind, foliage::formula, ), - delimited + preceded ( - multispace0, + whitespace0, tag("."), - multispace0, ), )(i) } +fn statement_enclosed_by_whitespace(i: &str) -> IResult<&str, (&str, (&str, (crate::project::StatementKind, foliage::Formula)), &str)> +{ + tuple + (( + recognize(whitespace0), + recognize_and_keep(statement), + recognize(whitespace0), + ))(i) +} + pub fn project(i: &str) -> IResult<&str, crate::Project> { let mut statement_input = i.clone(); - let mut statements = std::collections::HashMap::new(); + let mut blocks = Vec::new(); loop { let i_ = statement_input.clone(); - match statement(i_) + match statement_enclosed_by_whitespace(i_) { - Ok((i, (statement_kind, formula))) => + Ok((i, (whitespace_before, (statement_original_text, (statement_kind, formula)), whitespace_after))) => { // Iteration must always consume input (to prevent infinite loops) if i == statement_input @@ -73,8 +102,24 @@ pub fn project(i: &str) -> IResult<&str, crate::Project> return Err(nom::Err::Error(nom::error::ParseError::from_error_kind(statement_input, nom::error::ErrorKind::Many0))); } - let statements = statements.entry(statement_kind).or_insert_with(Vec::new); - statements.push(formula); + if !whitespace_before.is_empty() + { + blocks.push(crate::project::Block::Whitespace(whitespace_before)); + } + + let statement = crate::project::Statement + { + kind: statement_kind, + original_text: statement_original_text, + formula, + }; + + blocks.push(crate::project::Block::Statement(statement)); + + if !whitespace_after.is_empty() + { + blocks.push(crate::project::Block::Whitespace(whitespace_after)); + } statement_input = i; }, @@ -93,7 +138,7 @@ pub fn project(i: &str) -> IResult<&str, crate::Project> let project = crate::Project { - statements, + blocks, }; Ok((i, project)) diff --git a/src/project.rs b/src/project.rs index 38a9bdb..a1e3c3d 100644 --- a/src/project.rs +++ b/src/project.rs @@ -6,7 +6,20 @@ pub enum StatementKind Conjecture, } -pub struct Project +pub struct Statement<'input> { - pub statements: std::collections::HashMap>, + pub kind: StatementKind, + pub original_text: &'input str, + pub formula: foliage::Formula, +} + +pub enum Block<'input> +{ + Statement(Statement<'input>), + Whitespace(&'input str), +} + +pub struct Project<'input> +{ + pub blocks: Vec>, }