From e382058c2dba2fb868e2f7b4505151ea4f2bf79e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Sat, 2 Nov 2019 04:13:00 +0100 Subject: [PATCH] Add missing anthem axioms --- foliage | 2 +- src/format_tptp.rs | 213 +++++++++++++++++++++++++-- src/main.rs | 4 +- src/tptp_preamble_anthem_axioms.tptp | 15 ++ src/tptp_preamble_anthem_types.tptp | 11 ++ 5 files changed, 225 insertions(+), 20 deletions(-) create mode 100644 src/tptp_preamble_anthem_axioms.tptp create mode 100644 src/tptp_preamble_anthem_types.tptp diff --git a/foliage b/foliage index a6fe4b9..5070965 160000 --- a/foliage +++ b/foliage @@ -1 +1 @@ -Subproject commit a6fe4b9e0881fc1707fd6c83e419857ad8a653eb +Subproject commit 5070965bfee7ad8a0af0d4abc0f8c6d07b7ae5ec diff --git a/src/format_tptp.rs b/src/format_tptp.rs index d4f4325..9a20808 100644 --- a/src/format_tptp.rs +++ b/src/format_tptp.rs @@ -83,6 +83,127 @@ fn collect_predicate_declarations_in_project<'a>(project: &'a crate::Project) predicate_declarations } +fn collect_symbolic_constants_in_term<'a>( + symbolic_constants: &mut std::collections::HashSet<&'a str>, term: &'a foliage::Term) +{ + match term + { + foliage::Term::Infimum => (), + foliage::Term::Supremum => (), + foliage::Term::Integer(_) => (), + foliage::Term::Symbolic(ref name) => + { + symbolic_constants.insert(name); + }, + foliage::Term::String(_) => (), + foliage::Term::Variable(_) => (), + foliage::Term::Add(ref left, ref right) => + { + collect_symbolic_constants_in_term(symbolic_constants, left); + collect_symbolic_constants_in_term(symbolic_constants, right); + }, + foliage::Term::Subtract(ref left, ref right) => + { + collect_symbolic_constants_in_term(symbolic_constants, left); + collect_symbolic_constants_in_term(symbolic_constants, right); + }, + foliage::Term::Multiply(ref left, ref right) => + { + collect_symbolic_constants_in_term(symbolic_constants, left); + collect_symbolic_constants_in_term(symbolic_constants, right); + }, + foliage::Term::Negative(ref argument) => + { + collect_symbolic_constants_in_term(symbolic_constants, argument); + }, + } +} + +fn collect_symbolic_constants_in_formula<'a>( + symbolic_constants: &mut std::collections::HashSet<&'a str>, formula: &'a foliage::Formula) +{ + match formula + { + foliage::Formula::Exists(ref exists) => collect_symbolic_constants_in_formula(symbolic_constants, &exists.argument), + foliage::Formula::ForAll(ref for_all) => collect_symbolic_constants_in_formula(symbolic_constants, &for_all.argument), + foliage::Formula::Not(ref argument) => collect_symbolic_constants_in_formula(symbolic_constants, argument), + foliage::Formula::And(ref arguments) => + for argument in arguments + { + collect_symbolic_constants_in_formula(symbolic_constants, argument); + }, + foliage::Formula::Or(ref arguments) => + for argument in arguments + { + collect_symbolic_constants_in_formula(symbolic_constants, argument); + }, + foliage::Formula::Implies(ref left, ref right) => + { + collect_symbolic_constants_in_formula(symbolic_constants, left); + collect_symbolic_constants_in_formula(symbolic_constants, right); + }, + foliage::Formula::Biconditional(ref left, ref right) => + { + collect_symbolic_constants_in_formula(symbolic_constants, left); + collect_symbolic_constants_in_formula(symbolic_constants, right); + }, + foliage::Formula::Less(ref left, ref right) => + { + collect_symbolic_constants_in_term(symbolic_constants, left); + collect_symbolic_constants_in_term(symbolic_constants, right); + }, + foliage::Formula::LessOrEqual(ref left, ref right) => + { + collect_symbolic_constants_in_term(symbolic_constants, left); + collect_symbolic_constants_in_term(symbolic_constants, right); + }, + foliage::Formula::Greater(ref left, ref right) => + { + collect_symbolic_constants_in_term(symbolic_constants, left); + collect_symbolic_constants_in_term(symbolic_constants, right); + }, + foliage::Formula::GreaterOrEqual(ref left, ref right) => + { + collect_symbolic_constants_in_term(symbolic_constants, left); + collect_symbolic_constants_in_term(symbolic_constants, right); + }, + foliage::Formula::Equal(ref left, ref right) => + { + collect_symbolic_constants_in_term(symbolic_constants, left); + collect_symbolic_constants_in_term(symbolic_constants, right); + }, + foliage::Formula::NotEqual(ref left, ref right) => + { + collect_symbolic_constants_in_term(symbolic_constants, left); + collect_symbolic_constants_in_term(symbolic_constants, right); + }, + foliage::Formula::Boolean(_) => (), + foliage::Formula::Predicate(ref predicate) => + { + for argument in &predicate.arguments + { + collect_symbolic_constants_in_term(symbolic_constants, &argument); + } + }, + } +} + +fn collect_symbolic_constants_in_project<'a>(project: &'a crate::Project) + -> std::collections::HashSet<&'a str> +{ + let mut symbolic_constants = std::collections::HashSet::new(); + + for (_, formulas) in project.statements.iter() + { + for formula in formulas.iter() + { + collect_symbolic_constants_in_formula(&mut symbolic_constants, formula); + } + } + + symbolic_constants +} + struct VariableDeclarationDisplay<'a>(&'a foliage::VariableDeclaration); struct PredicateDeclarationDisplay<'a>(&'a foliage::PredicateDeclaration); struct TermDisplay<'a>(&'a foliage::Term); @@ -227,14 +348,31 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> Infix, } - let mut display_comparison = |notation, operator_identifier: &str, left, right| -> Result<(), std::fmt::Error> + let mut display_comparison = |notation, operator_identifier: &str, operator_identifier_fallback, left, right| -> Result<(), std::fmt::Error> { + write!(format, "(")?; + + 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); + + if let Some(operator_identifier_fallback) = operator_identifier_fallback + { + if !left_is_arithmetic_term || !right_is_arithmetic_term + { + notation = Notation::Prefix; + operator_identifier = operator_identifier_fallback; + } + } + if notation == Notation::Prefix { write!(format, "{}(", operator_identifier)?; } - if is_arithmetic_term(left) && !is_arithmetic_term(right) + if left_is_arithmetic_term && !right_is_arithmetic_term { write!(format, "f__integer__({})", left.display_tptp())?; } @@ -249,7 +387,7 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> Notation::Infix => write!(format, " {} ", operator_identifier)?, } - if is_arithmetic_term(right) && !is_arithmetic_term(left) + if right_is_arithmetic_term && !left_is_arithmetic_term { write!(format, "f__integer__({})", right.display_tptp())?; } @@ -263,7 +401,7 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> write!(format, ")")?; } - Ok(()) + write!(format, ")") }; match self.0 @@ -301,6 +439,8 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> foliage::Formula::Not(ref argument) => write!(format, "~({:?})", argument.display_tptp()), foliage::Formula::And(ref arguments) => { + write!(format, "(")?; + let mut separator = ""; for argument in arguments @@ -310,10 +450,12 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> separator = " & " } - Ok(()) + write!(format, ")") }, foliage::Formula::Or(ref arguments) => { + write!(format, "(")?; + let mut separator = ""; for argument in arguments @@ -323,16 +465,16 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> separator = " | " } - Ok(()) + write!(format, ")") }, foliage::Formula::Implies(ref left, ref right) => write!(format, "({:?} => {:?})", left.display_tptp(), right.display_tptp()), foliage::Formula::Biconditional(ref left, ref right) => write!(format, "({:?} <=> {:?})", left.display_tptp(), right.display_tptp()), - foliage::Formula::Less(ref left, ref right) => display_comparison(Notation::Prefix, "$less", left, right), - foliage::Formula::LessOrEqual(ref left, ref right) => display_comparison(Notation::Prefix, "$lesseq", left, right), - foliage::Formula::Greater(ref left, ref right) => display_comparison(Notation::Prefix, "$greater", left, right), - foliage::Formula::GreaterOrEqual(ref left, ref right) => display_comparison(Notation::Prefix, "$greatereq", left, right), - foliage::Formula::Equal(ref left, ref right) => display_comparison(Notation::Infix, "=", left, right), - foliage::Formula::NotEqual(ref left, ref right) => display_comparison(Notation::Infix, "~=", left, right), + 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), + foliage::Formula::GreaterOrEqual(ref left, ref right) => display_comparison(Notation::Prefix, "$greatereq", Some("p__greater_equal__"), left, right), + foliage::Formula::Equal(ref left, ref right) => display_comparison(Notation::Infix, "=", None, left, right), + foliage::Formula::NotEqual(ref left, ref right) => display_comparison(Notation::Infix, "~=", None, left, right), foliage::Formula::Boolean(value) => match value { @@ -351,8 +493,20 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> for argument in &predicate.arguments { + let argument_is_arithmetic_term = is_arithmetic_term(argument); + + if argument_is_arithmetic_term + { + write!(format, "f__integer__(")?; + } + write!(format, "{}{:?}", separator, argument.display_tptp())?; + if argument_is_arithmetic_term + { + write!(format, ")")?; + } + separator = ", " } @@ -380,7 +534,7 @@ impl<'a> std::fmt::Debug for StatementKindDisplay<'a> match &self.0 { crate::project::StatementKind::Axiom => write!(format, "axiom, axiom"), - crate::project::StatementKind::Lemma => write!(format, "conjecture, lemma"), + crate::project::StatementKind::Lemma => write!(format, "lemma, conjecture"), crate::project::StatementKind::Conjecture => write!(format, "conjecture, conjecture"), } } @@ -398,21 +552,44 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(format, "tff(types, type, object: $tType).")?; + let write_title = |format: &mut std::fmt::Formatter, line_separator, title_identifier| + { + write!(format, "{}{}", line_separator, "%".repeat(80))?; + write!(format, "\n% {}", title_identifier)?; + write!(format, "\n{}", "%".repeat(80)) + }; + + write_title(format, "", "anthem types")?; + + let tptp_preamble_anthem_types = include_str!("tptp_preamble_anthem_types.tptp").trim_end(); + write!(format, "\n{}", tptp_preamble_anthem_types)?; + + write_title(format, "\n\n", "anthem axioms")?; + + let tptp_preamble_anthem_axioms = include_str!("tptp_preamble_anthem_axioms.tptp").trim_end(); + write!(format, "\n{}", tptp_preamble_anthem_axioms)?; let predicate_declarations = collect_predicate_declarations_in_project(self.0); + let symbolic_constants = collect_symbolic_constants_in_project(self.0); - if !predicate_declarations.is_empty() + if !predicate_declarations.is_empty() || !symbolic_constants.is_empty() { + write_title(format, "\n\n", "types")?; + for predicate_declaration in predicate_declarations { write!(format, "\ntff(type, type, {:?}).", predicate_declaration.display_tptp())?; } + + for symbolic_constant in symbolic_constants + { + write!(format, "\ntff(type, type, {}: object).", symbolic_constant)?; + } } if let Some(axioms) = self.0.statements.get(&crate::project::StatementKind::Axiom) { - write!(format, "\n")?; + write_title(format, "\n\n", "axioms")?; for axiom in axioms { @@ -422,6 +599,8 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a> if let Some(lemmas) = self.0.statements.get(&crate::project::StatementKind::Lemma) { + write_title(format, "\n\n", "lemmas")?; + for lemma in lemmas { write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Lemma.display_tptp(), lemma.display_tptp())?; @@ -430,6 +609,8 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a> if let Some(conjectures) = self.0.statements.get(&crate::project::StatementKind::Conjecture) { + write_title(format, "\n\n", "conjectures")?; + for conjecture in conjectures { write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Conjecture.display_tptp(), conjecture.display_tptp())?; diff --git a/src/main.rs b/src/main.rs index 7aad92e..8d91b84 100644 --- a/src/main.rs +++ b/src/main.rs @@ -14,9 +14,7 @@ fn main() -> Result<(), Box> let (_, project) = ask_dracula::parse::project(&file_content) .map_err(|_| "couldn’t parse input file")?; - println!("{}", project); - - println!(""); + eprintln!("{}", project); println!("{}", project.display_tptp()); diff --git a/src/tptp_preamble_anthem_axioms.tptp b/src/tptp_preamble_anthem_axioms.tptp new file mode 100644 index 0000000..c4d0d09 --- /dev/null +++ b/src/tptp_preamble_anthem_axioms.tptp @@ -0,0 +1,15 @@ +tff(axiom, axiom, ![X: object]: (p__is_integer__(X) <=> (?[Y: $int]: (X = f__integer__(Y))))). +tff(axiom, axiom, ![X: object]: (p__is_symbolic__(X) <=> (?[Y: $i]: (X = f__symbolic__(Y))))). +tff(axiom, axiom, ![X: object]: ((X = c__infimum__) | p__is_integer__(X) | p__is_symbolic__(X) | (X = c__supremum__))). +tff(axiom, axiom, ![X: $int, Y: $int]: ((f__integer__(X) = f__integer__(Y)) <=> (X = Y))). +tff(axiom, axiom, ![X: $i, Y: $i]: ((f__symbolic__(X) = f__symbolic__(Y)) <=> (X = Y))). +tff(axiom, axiom, ![X1: $int, X2: $int]: (p__less_equal__(f__integer__(X1), f__integer__(X2)) <=> $lesseq(X1, X2))). +tff(axiom, axiom, ![X1: object, X2: object]: ((p__less_equal__(X1, X2) & p__less_equal__(X2, X1)) => (X1 = X2))). +tff(axiom, axiom, ![X1: object, X2: object, X3: object]: ((p__less_equal__(X1, X2) & p__less_equal__(X2, X3)) => p__less_equal__(X1, X3))). +tff(axiom, axiom, ![X1: object, X2: object]: (p__less_equal__(X1, X2) | p__less_equal__(X2, X1))). +tff(axiom, axiom, ![X1: object, X2: object]: (p__less__(X1, X2) <=> (p__less_equal__(X1, X2) & (X1 != X2)))). +tff(axiom, axiom, ![X1: object, X2: object]: (p__greater_equal__(X1, X2) <=> p__less_equal__(X2, X1))). +tff(axiom, axiom, ![X1: object, X2: object]: (p__greater__(X1, X2) <=> (p__less_equal__(X2, X1) & (X1 != X2)))). +tff(axiom, axiom, ![X: $int]: p__less__(c__infimum__, f__integer__(X))). +tff(axiom, axiom, ![X1: $int, X2: $i]: p__less__(f__integer__(X1), f__symbolic__(X2))). +tff(axiom, axiom, ![X: $i]: p__less__(f__symbolic__(X), c__supremum__)). diff --git a/src/tptp_preamble_anthem_types.tptp b/src/tptp_preamble_anthem_types.tptp new file mode 100644 index 0000000..40e6f7c --- /dev/null +++ b/src/tptp_preamble_anthem_types.tptp @@ -0,0 +1,11 @@ +tff(type, type, object: $tType). +tff(type, type, f__integer__: ($int) > object). +tff(type, type, f__symbolic__: ($i) > object). +tff(type, type, c__infimum__: object). +tff(type, type, c__supremum__: object). +tff(type, type, p__is_integer__: (object) > $o). +tff(type, type, p__is_symbolic__: (object) > $o). +tff(type, type, p__less_equal__: (object * object) > $o). +tff(type, type, p__less__: (object * object) > $o). +tff(type, type, p__greater_equal__: (object * object) > $o). +tff(type, type, p__greater__: (object * object) > $o).