From 33c5245b80cc5b1c20167ced26301247aedc4413 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 7 Nov 2019 02:17:49 -0600 Subject: [PATCH] Skip input predicates in completion --- src/format.rs | 2 + src/format_tptp.rs | 32 +++++++++-- src/main.rs | 23 ++++---- src/parse.rs | 136 +++++++++++++++++++++++++++++++++++++++------ src/project.rs | 14 +++++ 5 files changed, 175 insertions(+), 32 deletions(-) diff --git a/src/format.rs b/src/format.rs index 372480c..4fe67b2 100644 --- a/src/format.rs +++ b/src/format.rs @@ -58,6 +58,8 @@ impl std::fmt::Debug for crate::Project crate::project::Block::Whitespace(ref text) => write!(format, "{}", text)?, crate::project::Block::FormulaStatement(ref formula_statement) => write!(format, "{}", formula_statement.original_text)?, + crate::project::Block::InputStatement(ref input_statement) => + write!(format, "{}", input_statement.original_text)?, } } diff --git a/src/format_tptp.rs b/src/format_tptp.rs index 499eef3..38d64b1 100644 --- a/src/format_tptp.rs +++ b/src/format_tptp.rs @@ -54,6 +54,18 @@ pub fn is_formula_statement_theorem(formula_statement: &crate::project::FormulaS } } +pub fn is_formula_statement_ignored(formula_statement: &crate::project::FormulaStatement, + input_predicates: &std::collections::HashSet) -> bool +{ + // Hide completed definitions of input predicates + if let crate::project::FormulaStatementKind::Completion(crate::project::CompletionTarget::Predicate(ref predicate_declaration)) = formula_statement.kind + { + return input_predicates.contains(predicate_declaration); + } + + false +} + fn is_arithmetic_term(term: &foliage::Term) -> bool { match term @@ -129,6 +141,7 @@ fn collect_predicate_declarations_in_project<'a>(project: &'a crate::Project) { crate::project::Block::Whitespace(_) => None, crate::project::Block::FormulaStatement(ref formula_statement) => Some(&formula_statement.formula), + crate::project::Block::InputStatement(_) => None, }); for formula in formulas @@ -253,11 +266,12 @@ fn collect_symbolic_constants_in_project<'a>(project: &'a crate::Project) let formulas = project.blocks.iter() .filter_map( |block| - match block - { - crate::project::Block::Whitespace(_) => None, - crate::project::Block::FormulaStatement(ref formula_statement) => Some(&formula_statement.formula), - }); + match block + { + crate::project::Block::Whitespace(_) => None, + crate::project::Block::FormulaStatement(ref formula_statement) => Some(&formula_statement.formula), + crate::project::Block::InputStatement(_) => None, + }); for formula in formulas { @@ -701,11 +715,19 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a> { crate::project::Block::Whitespace(_) => None, crate::project::Block::FormulaStatement(ref formula_statement) => + { + if is_formula_statement_ignored(formula_statement, &self.project.input_predicates) + { + return None; + } + match is_formula_statement_axiom(&formula_statement, self.proof_direction) { true => Some(formula_statement), false => None, } + }, + crate::project::Block::InputStatement(_) => None, }); for axiom in axioms diff --git a/src/main.rs b/src/main.rs index 4fcbbf6..bc7dad6 100644 --- a/src/main.rs +++ b/src/main.rs @@ -9,10 +9,9 @@ fn reset_proof_results<'a>(project: &'a mut ask_dracula::Project) { for block in &mut project.blocks { - match block + if let ask_dracula::project::Block::FormulaStatement(ref mut formula_statement) = block { - ask_dracula::project::Block::Whitespace(_) => (), - ask_dracula::project::Block::FormulaStatement(ref mut formula_statement) => formula_statement.proven = false, + formula_statement.proven = false; } } } @@ -119,6 +118,8 @@ fn main() -> Result<(), Box> reset_proof_results(&mut project); + let input_predicates = &project.input_predicates; + loop { let conjecture = project.blocks.iter() @@ -127,11 +128,11 @@ fn main() -> Result<(), Box> |block| match block { - ask_dracula::project::Block::Whitespace(_) => None, ask_dracula::project::Block::FormulaStatement(ref formula_statement) => Some(formula_statement), + _ => None, } ) - .find(|formula_statement| ask_dracula::format_tptp::is_formula_statement_lemma(&formula_statement, proof_direction)); + .find(|formula_statement| !ask_dracula::format_tptp::is_formula_statement_ignored(&formula_statement, &input_predicates) && ask_dracula::format_tptp::is_formula_statement_lemma(&formula_statement, proof_direction)); let conjecture = match conjecture { @@ -142,11 +143,11 @@ fn main() -> Result<(), Box> |block| match block { - ask_dracula::project::Block::Whitespace(_) => None, ask_dracula::project::Block::FormulaStatement(ref formula_statement) => Some(formula_statement), + _ => None, } ) - .find(|formula_statement| ask_dracula::format_tptp::is_formula_statement_theorem(&formula_statement, proof_direction)), + .find(|formula_statement| !ask_dracula::format_tptp::is_formula_statement_ignored(&formula_statement, &input_predicates) && ask_dracula::format_tptp::is_formula_statement_theorem(&formula_statement, proof_direction)), }; let conjecture = match conjecture @@ -189,11 +190,11 @@ fn main() -> Result<(), Box> |block| match block { - ask_dracula::project::Block::Whitespace(_) => None, ask_dracula::project::Block::FormulaStatement(ref mut formula_statement) => Some(formula_statement), + _ => None, } ) - .find(|formula_statement| ask_dracula::format_tptp::is_formula_statement_lemma(&formula_statement, proof_direction)); + .find(|formula_statement| !ask_dracula::format_tptp::is_formula_statement_ignored(&formula_statement, &input_predicates) && ask_dracula::format_tptp::is_formula_statement_lemma(&formula_statement, proof_direction)); let mut conjecture = match conjecture { @@ -204,11 +205,11 @@ fn main() -> Result<(), Box> |block| match block { - ask_dracula::project::Block::Whitespace(_) => None, ask_dracula::project::Block::FormulaStatement(ref mut formula_statement) => Some(formula_statement), + _ => None, } ) - .find(|formula_statement| ask_dracula::format_tptp::is_formula_statement_theorem(&formula_statement, proof_direction)), + .find(|formula_statement| !ask_dracula::format_tptp::is_formula_statement_ignored(&formula_statement, &input_predicates) && 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 974da76..6d108d9 100644 --- a/src/parse.rs +++ b/src/parse.rs @@ -6,6 +6,7 @@ use nom:: character::complete::digit1, branch::alt, bytes::complete::tag, + multi::separated_list, }; use foliage::parse::whitespace0; @@ -31,7 +32,7 @@ where fn formula_statement_kind(i: &str) -> IResult<&str, crate::project::FormulaStatementKind> { - let foo = delimited + delimited ( whitespace0, alt @@ -101,9 +102,7 @@ fn formula_statement_kind(i: &str) -> IResult<&str, crate::project::FormulaState ), )), whitespace0, - )(i); - - foo + )(i) } fn formula_statement(i: &str) -> IResult<&str, (crate::project::FormulaStatementKind, foliage::Formula)> @@ -123,13 +122,84 @@ fn formula_statement(i: &str) -> IResult<&str, (crate::project::FormulaStatement )(i) } -fn formula_statement_enclosed_by_whitespace(i: &str) - -> IResult<&str, (&str, (&str, (crate::project::FormulaStatementKind, foliage::Formula)), &str)> +fn input_statement(i: &str) -> IResult<&str, Vec> +{ + delimited + ( + whitespace0, + preceded + ( + pair + ( + tag("input:"), + whitespace0, + ), + separated_list + ( + tag(","), + delimited + ( + whitespace0, + alt + (( + map + ( + pair + ( + terminated + ( + foliage::parse::symbolic_identifier, + tag("/"), + ), + digit1, + ), + |(name, arity)| + crate::project::InputSymbol::Predicate( + foliage::PredicateDeclaration + { + name: name.to_string(), + arity: arity.parse::().expect("invalid arity"), + }) + ), + map + ( + foliage::parse::symbolic_identifier, + |name| + crate::project::InputSymbol::Constant(name.to_string()) + ), + )), + whitespace0, + ) + ) + ), + preceded + ( + whitespace0, + tag("."), + ), + )(i) +} + +pub enum Statement +{ + Formula(crate::project::FormulaStatementKind, foliage::Formula), + Input(Vec), +} + +fn statement_enclosed_by_whitespace(i: &str) + -> IResult<&str, (&str, (&str, Statement), &str)> { tuple (( recognize(whitespace0), - recognize_and_keep(formula_statement), + recognize_and_keep + ( + alt + (( + map(formula_statement, |(formula_statement_kind, formula)| Statement::Formula(formula_statement_kind, formula)), + map(input_statement, |input_symbols| Statement::Input(input_symbols)), + )) + ), recognize(whitespace0), ))(i) } @@ -138,13 +208,15 @@ pub fn project(i: &str) -> IResult<&str, crate::Project> { let mut statement_input = i.clone(); let mut blocks = Vec::new(); + let mut input_constants = std::collections::HashSet::new(); + let mut input_predicates = std::collections::HashSet::new(); loop { let i_ = statement_input.clone(); - match formula_statement_enclosed_by_whitespace(i_) + match statement_enclosed_by_whitespace(i_) { - Ok((i, (whitespace_before, (formula_statement_original_text, (formula_statement_kind, formula)), whitespace_after))) => + Ok((i, (whitespace_before, (statement_original_text, statement), whitespace_after))) => { // Iteration must always consume input (to prevent infinite loops) if i == statement_input @@ -157,15 +229,45 @@ pub fn project(i: &str) -> IResult<&str, crate::Project> blocks.push(crate::project::Block::Whitespace(whitespace_before.to_string())); } - let formula_statement = crate::project::FormulaStatement + match statement { - kind: formula_statement_kind, - original_text: formula_statement_original_text.to_string(), - formula, - proven: false, - }; + Statement::Formula(formula_statement_kind, formula) => + { + let formula_statement = crate::project::FormulaStatement + { + kind: formula_statement_kind, + original_text: statement_original_text.to_string(), + formula, + proven: false, + }; - blocks.push(crate::project::Block::FormulaStatement(formula_statement)); + blocks.push(crate::project::Block::FormulaStatement(formula_statement)); + }, + Statement::Input(input_symbols) => + { + for input_symbol in input_symbols + { + match input_symbol + { + crate::project::InputSymbol::Constant(name) => + { + input_constants.insert(name); + }, + crate::project::InputSymbol::Predicate(declaration) => + { + input_predicates.insert(declaration); + }, + } + } + + let input_statement = crate::project::InputStatement + { + original_text: statement_original_text.to_string(), + }; + + blocks.push(crate::project::Block::InputStatement(input_statement)); + }, + } if !whitespace_after.is_empty() { @@ -191,6 +293,8 @@ pub fn project(i: &str) -> IResult<&str, crate::Project> let project = crate::Project { blocks, + input_constants, + input_predicates, }; Ok((i, project)) diff --git a/src/project.rs b/src/project.rs index a30a8dd..fd05992 100644 --- a/src/project.rs +++ b/src/project.rs @@ -30,13 +30,27 @@ pub struct FormulaStatement pub proven: bool, } +pub struct InputStatement +{ + pub original_text: String, +} + +pub enum InputSymbol +{ + Constant(String), + Predicate(foliage::PredicateDeclaration), +} + pub enum Block { FormulaStatement(FormulaStatement), + InputStatement(InputStatement), Whitespace(String), } pub struct Project { pub blocks: Vec, + pub input_constants: std::collections::HashSet, + pub input_predicates: std::collections::HashSet, }