diff --git a/foliage b/foliage index 7af51e9..9202c83 160000 --- a/foliage +++ b/foliage @@ -1 +1 @@ -Subproject commit 7af51e9e64947a16f7f9c5c7923b77a8862139b5 +Subproject commit 9202c839e2654e92a7535019924918203e89862c diff --git a/src/format_tptp.rs b/src/format_tptp.rs index 38d64b1..a39571a 100644 --- a/src/format_tptp.rs +++ b/src/format_tptp.rs @@ -66,24 +66,40 @@ pub fn is_formula_statement_ignored(formula_statement: &crate::project::FormulaS false } -fn is_arithmetic_term(term: &foliage::Term) -> bool +fn is_integer_input_constant(constant_name: &str, + input_constants: &std::collections::HashSet) -> bool +{ + let input_constant = crate::project::InputConstantDeclaration + { + // TODO: avoid unnecessary allocation + name: constant_name.to_owned(), + domain: foliage::Domain::Integer, + }; + + input_constants.contains(&input_constant) +} + +fn is_arithmetic_term(term: &foliage::Term, input_constants: &std::collections::HashSet) -> bool { match term { foliage::Term::Infimum => false, foliage::Term::Supremum => false, foliage::Term::Integer(_) => true, - foliage::Term::Symbolic(_) => false, + foliage::Term::Symbolic(ref name) => + { + is_integer_input_constant(name, input_constants) + }, foliage::Term::String(_) => false, foliage::Term::Variable(ref declaration) => match declaration.domain { foliage::Domain::Program => false, foliage::Domain::Integer => true, }, - foliage::Term::Add(ref left, ref right) => is_arithmetic_term(left) && is_arithmetic_term(right), - foliage::Term::Subtract(ref left, ref right) => is_arithmetic_term(left) && is_arithmetic_term(right), - foliage::Term::Multiply(ref left, ref right) => is_arithmetic_term(left) && is_arithmetic_term(right), - foliage::Term::Negative(ref argument) => is_arithmetic_term(argument), + foliage::Term::Add(ref left, ref right) => is_arithmetic_term(left, input_constants) && is_arithmetic_term(right, input_constants), + foliage::Term::Subtract(ref left, ref right) => is_arithmetic_term(left, input_constants) && is_arithmetic_term(right, input_constants), + foliage::Term::Multiply(ref left, ref right) => is_arithmetic_term(left, input_constants) && is_arithmetic_term(right, input_constants), + foliage::Term::Negative(ref argument) => is_arithmetic_term(argument, input_constants), } } @@ -284,11 +300,16 @@ fn collect_symbolic_constants_in_project<'a>(project: &'a crate::Project) 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 FormulaStatementDisplay<'a> +struct FormulaDisplay<'a, 'project> +{ + formula: &'a foliage::Formula, + input_constants: &'project std::collections::HashSet, +} +struct FormulaStatementDisplay<'a, 'project> { formula_statement: &'a crate::project::FormulaStatement, proof_direction: crate::project::ProofDirection, + input_constants: &'project std::collections::HashSet, } pub struct ProjectDisplay<'a> { @@ -321,22 +342,26 @@ impl<'a> DisplayTPTP<'a, TermDisplay<'a>> for foliage::Term } } -impl<'a> DisplayTPTP<'a, FormulaDisplay<'a>> for foliage::Formula +fn display_formula_tptp<'a, 'project>(formula: &'a foliage::Formula, + input_constants: &'project std::collections::HashSet) + -> FormulaDisplay<'a, 'project> { - fn display_tptp(&'a self) -> FormulaDisplay<'a> + FormulaDisplay { - FormulaDisplay(self) + formula, + input_constants, } } -fn display_formula_statement_tptp<'a>(formula_statement: &'a crate::project::FormulaStatement, - proof_direction: crate::project::ProofDirection) - -> FormulaStatementDisplay<'a> +fn display_formula_statement_tptp<'a, 'project>(formula_statement: &'a crate::project::FormulaStatement, + proof_direction: crate::project::ProofDirection, input_constants: &'project std::collections::HashSet,) + -> FormulaStatementDisplay<'a, 'project> { FormulaStatementDisplay { formula_statement, proof_direction, + input_constants, } } @@ -430,7 +455,7 @@ impl<'a> std::fmt::Display for TermDisplay<'a> } } -impl<'a> std::fmt::Debug for FormulaDisplay<'a> +impl<'a, 'project> std::fmt::Debug for FormulaDisplay<'a, 'project> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -448,8 +473,8 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> let mut notation = notation; let mut operator_identifier = operator_identifier; - let left_is_arithmetic_term = is_arithmetic_term(left); - let right_is_arithmetic_term = is_arithmetic_term(right); + let left_is_arithmetic_term = is_arithmetic_term(left, self.input_constants); + let right_is_arithmetic_term = is_arithmetic_term(right, self.input_constants); if let Some(operator_identifier_fallback) = operator_identifier_fallback { @@ -497,7 +522,7 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> write!(format, ")") }; - match self.0 + match self.formula { foliage::Formula::Exists(ref exists) => { @@ -512,7 +537,7 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> separator = ", " } - write!(format, "]: ({:?})", exists.argument.display_tptp()) + write!(format, "]: ({:?})", display_formula_tptp(&exists.argument, self.input_constants)) }, foliage::Formula::ForAll(ref for_all) => { @@ -527,9 +552,9 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> separator = ", " } - write!(format, "]: ({:?})", for_all.argument.display_tptp()) + write!(format, "]: ({:?})", display_formula_tptp(&for_all.argument, self.input_constants)) }, - foliage::Formula::Not(ref argument) => write!(format, "~({:?})", argument.display_tptp()), + foliage::Formula::Not(ref argument) => write!(format, "~({:?})", display_formula_tptp(argument, self.input_constants)), foliage::Formula::And(ref arguments) => { write!(format, "(")?; @@ -538,7 +563,7 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> for argument in arguments { - write!(format, "{}{:?}", separator, argument.display_tptp())?; + write!(format, "{}{:?}", separator, display_formula_tptp(argument, self.input_constants))?; separator = " & " } @@ -553,7 +578,7 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> for argument in arguments { - write!(format, "{}{:?}", separator, argument.display_tptp())?; + write!(format, "{}{:?}", separator, display_formula_tptp(argument, self.input_constants))?; separator = " | " } @@ -562,10 +587,10 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> }, foliage::Formula::Implies(ref left, ref right, implication_direction) => match implication_direction { - foliage::ImplicationDirection::LeftToRight => write!(format, "({:?} => {:?})", left.display_tptp(), right.display_tptp()), - foliage::ImplicationDirection::RightToLeft => write!(format, "({:?} <= {:?})", left.display_tptp(), right.display_tptp()), + foliage::ImplicationDirection::LeftToRight => write!(format, "({:?} => {:?})", display_formula_tptp(left, self.input_constants), display_formula_tptp(right, self.input_constants)), + foliage::ImplicationDirection::RightToLeft => write!(format, "({:?} <= {:?})", display_formula_tptp(left, self.input_constants), display_formula_tptp(right, self.input_constants)), }, - foliage::Formula::Biconditional(ref left, ref right) => write!(format, "({:?} <=> {:?})", left.display_tptp(), right.display_tptp()), + foliage::Formula::Biconditional(ref left, ref right) => write!(format, "({:?} <=> {:?})", display_formula_tptp(left, self.input_constants), display_formula_tptp(right, self.input_constants)), foliage::Formula::Less(ref left, ref right) => display_comparison(Notation::Prefix, "$less", Some("p__less__"), left, right), foliage::Formula::LessOrEqual(ref left, ref right) => display_comparison(Notation::Prefix, "$lesseq", Some("p__less_equal__"), left, right), foliage::Formula::Greater(ref left, ref right) => display_comparison(Notation::Prefix, "$greater", Some("p__greater__"), left, right), @@ -590,7 +615,7 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> for argument in &predicate.arguments { - let argument_is_arithmetic_term = is_arithmetic_term(argument); + let argument_is_arithmetic_term = is_arithmetic_term(argument, self.input_constants); write!(format, "{}", separator)?; @@ -618,7 +643,7 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> } } -impl<'a> std::fmt::Display for FormulaDisplay<'a> +impl<'a, 'project> std::fmt::Display for FormulaDisplay<'a, 'project> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -626,7 +651,7 @@ impl<'a> std::fmt::Display for FormulaDisplay<'a> } } -impl<'a> std::fmt::Debug for FormulaStatementDisplay<'a> +impl<'a, 'project> std::fmt::Debug for FormulaStatementDisplay<'a, 'project> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -657,11 +682,11 @@ impl<'a> std::fmt::Debug for FormulaStatementDisplay<'a> panic!("expected formula statement to be either theorem, lemma, or axiom, please report to bug tracker"); } - write!(format, ", {:?}).", self.formula_statement.formula.display_tptp()) + write!(format, ", {:?}).", display_formula_tptp(&self.formula_statement.formula, self.input_constants)) } } -impl<'a> std::fmt::Display for FormulaStatementDisplay<'a> +impl<'a, 'project> std::fmt::Display for FormulaStatementDisplay<'a, 'project> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -704,7 +729,11 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a> for symbolic_constant in symbolic_constants { - write!(format, "\ntff(type, type, {}: object).", symbolic_constant)?; + match is_integer_input_constant(symbolic_constant, &self.project.input_constants) + { + true => write!(format, "\ntff(type, type, {}: $int).", symbolic_constant)?, + false => write!(format, "\ntff(type, type, {}: object).", symbolic_constant)?, + } } } @@ -732,12 +761,12 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a> for axiom in axioms { - write!(format, "\n{}", display_formula_statement_tptp(&axiom, self.proof_direction))?; + write!(format, "\n{}", display_formula_statement_tptp(&axiom, self.proof_direction, &self.project.input_constants))?; } write_title(format, "\n\n", "assertion")?; - write!(format, "\n{}", display_formula_statement_tptp(&self.conjecture, self.proof_direction)) + write!(format, "\n{}", display_formula_statement_tptp(&self.conjecture, self.proof_direction, &self.project.input_constants)) } } diff --git a/src/parse.rs b/src/parse.rs index 6d108d9..a383671 100644 --- a/src/parse.rs +++ b/src/parse.rs @@ -2,7 +2,7 @@ use nom:: { IResult, sequence::{delimited, pair, preceded, terminated, tuple}, - combinator::{map, recognize}, + combinator::{map, recognize, opt}, character::complete::digit1, branch::alt, bytes::complete::tag, @@ -163,9 +163,40 @@ fn input_statement(i: &str) -> IResult<&str, Vec> ), map ( - foliage::parse::symbolic_identifier, - |name| - crate::project::InputSymbol::Constant(name.to_string()) + pair + ( + foliage::parse::symbolic_identifier, + opt + ( + preceded + ( + delimited + ( + whitespace0, + tag("->"), + whitespace0, + ), + tag("integer"), + ), + ), + ), + |(name, domain)| + match domain + { + None => crate::project::InputSymbol::Constant( + crate::project::InputConstantDeclaration + { + name: name.to_string(), + domain: foliage::Domain::Program, + }), + Some("integer") => crate::project::InputSymbol::Constant( + crate::project::InputConstantDeclaration + { + name: name.to_string(), + domain: foliage::Domain::Integer, + }), + Some(ref unknown_sort) => panic!("unrecognized sort “{}”", unknown_sort), + } ), )), whitespace0, diff --git a/src/project.rs b/src/project.rs index fd05992..44a5826 100644 --- a/src/project.rs +++ b/src/project.rs @@ -35,9 +35,16 @@ pub struct InputStatement pub original_text: String, } +#[derive(Eq, Hash, PartialEq)] +pub struct InputConstantDeclaration +{ + pub name: String, + pub domain: foliage::Domain, +} + pub enum InputSymbol { - Constant(String), + Constant(InputConstantDeclaration), Predicate(foliage::PredicateDeclaration), } @@ -51,6 +58,6 @@ pub enum Block pub struct Project { pub blocks: Vec, - pub input_constants: std::collections::HashSet, + pub input_constants: std::collections::HashSet, pub input_predicates: std::collections::HashSet, }