patrick/ask-dracula-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Add missing anthem axioms

Browse Source
This commit is contained in:
Patrick Lühne 2019-11-02 04:13:00 +01:00
parent 306dc7d850
commit e382058c2d
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
5 changed files with 225 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
foliage

@ -1 +1 @@
Subproject commit a6fe4b9e0881fc1707fd6c83e419857ad8a653eb
Subproject commit 5070965bfee7ad8a0af0d4abc0f8c6d07b7ae5ec

213
src/format_tptp.rs
View File

@ -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())?;

4
src/main.rs
View File

@ -14,9 +14,7 @@ fn main() -> Result<(), Box<dyn std::error::Error>>
let (_, project) = ask_dracula::parse::project(&file_content)
.map_err(|_| "couldn’t parse input file")?;
println!("{}", project);
println!("");
eprintln!("{}", project);
println!("{}", project.display_tptp());

15
src/tptp_preamble_anthem_axioms.tptp Normal file
View File

@ -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__)).

11
src/tptp_preamble_anthem_types.tptp Normal file
View File

@ -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).