357 lines
9.6 KiB
Rust
357 lines
9.6 KiB
Rust
pub trait DisplayTPTP<'a, DisplayType>
|
|
where DisplayType: 'a + std::fmt::Debug + std::fmt::Display
|
|
{
|
|
fn display_tptp(&'a self) -> DisplayType;
|
|
}
|
|
|
|
fn is_arithmetic_term(term: &foliage::Term) -> bool
|
|
{
|
|
match term
|
|
{
|
|
foliage::Term::Infimum => false,
|
|
foliage::Term::Supremum => false,
|
|
foliage::Term::Integer(_) => true,
|
|
foliage::Term::Symbolic(_) => false,
|
|
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),
|
|
}
|
|
}
|
|
|
|
struct VariableDeclarationDisplay<'a>(&'a foliage::VariableDeclaration);
|
|
struct TermDisplay<'a>(&'a foliage::Term);
|
|
struct FormulaDisplay<'a>(&'a foliage::Formula);
|
|
struct StatementKindDisplay<'a>(&'a crate::project::StatementKind);
|
|
pub struct ProjectDisplay<'a>(&'a crate::project::Project);
|
|
|
|
impl<'a> DisplayTPTP<'a, VariableDeclarationDisplay<'a>> for foliage::VariableDeclaration
|
|
{
|
|
fn display_tptp(&'a self) -> VariableDeclarationDisplay<'a>
|
|
{
|
|
VariableDeclarationDisplay(self)
|
|
}
|
|
}
|
|
|
|
impl<'a> DisplayTPTP<'a, TermDisplay<'a>> for foliage::Term
|
|
{
|
|
fn display_tptp(&'a self) -> TermDisplay<'a>
|
|
{
|
|
TermDisplay(self)
|
|
}
|
|
}
|
|
|
|
impl<'a> DisplayTPTP<'a, FormulaDisplay<'a>> for foliage::Formula
|
|
{
|
|
fn display_tptp(&'a self) -> FormulaDisplay<'a>
|
|
{
|
|
FormulaDisplay(self)
|
|
}
|
|
}
|
|
|
|
impl<'a> DisplayTPTP<'a, StatementKindDisplay<'a>> for crate::project::StatementKind
|
|
{
|
|
fn display_tptp(&'a self) -> StatementKindDisplay<'a>
|
|
{
|
|
StatementKindDisplay(self)
|
|
}
|
|
}
|
|
|
|
impl<'a> DisplayTPTP<'a, ProjectDisplay<'a>> for crate::project::Project
|
|
{
|
|
fn display_tptp(&'a self) -> ProjectDisplay<'a>
|
|
{
|
|
ProjectDisplay(self)
|
|
}
|
|
}
|
|
|
|
impl<'a> std::fmt::Debug for VariableDeclarationDisplay<'a>
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
match &self.0.domain
|
|
{
|
|
foliage::Domain::Program => write!(format, "X{}: object", self.0.name),
|
|
foliage::Domain::Integer => write!(format, "N{}: $int", self.0.name),
|
|
}
|
|
}
|
|
}
|
|
|
|
impl<'a> std::fmt::Display for VariableDeclarationDisplay<'a>
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
write!(format, "{:?}", &self)
|
|
}
|
|
}
|
|
|
|
impl<'a> std::fmt::Debug for TermDisplay<'a>
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
match self.0
|
|
{
|
|
foliage::Term::Infimum => write!(format, "#inf"),
|
|
foliage::Term::Supremum => write!(format, "#sup"),
|
|
foliage::Term::Integer(value) => write!(format, "{}", value),
|
|
foliage::Term::Symbolic(ref value) => write!(format, "{}", value),
|
|
foliage::Term::String(ref value) => write!(format, "\"{}\"", value),
|
|
foliage::Term::Variable(ref declaration) => match declaration.domain
|
|
{
|
|
foliage::Domain::Program => write!(format, "X{}", declaration.name),
|
|
foliage::Domain::Integer => write!(format, "N{}", declaration.name),
|
|
},
|
|
foliage::Term::Add(ref left, ref right) => write!(format, "$sum({:?}, {:?})", (&**left).display_tptp(), right.display_tptp()),
|
|
foliage::Term::Subtract(ref left, ref right) => write!(format, "$difference({:?} - {:?})", left.display_tptp(), right.display_tptp()),
|
|
foliage::Term::Multiply(ref left, ref right) => write!(format, "$product({:?} * {:?})", left.display_tptp(), right.display_tptp()),
|
|
foliage::Term::Negative(ref argument) => write!(format, "$uminus({:?})", argument.display_tptp()),
|
|
}
|
|
}
|
|
}
|
|
|
|
impl<'a> std::fmt::Display for TermDisplay<'a>
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
write!(format, "{:?}", self)
|
|
}
|
|
}
|
|
|
|
impl<'a> std::fmt::Debug for FormulaDisplay<'a>
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
#[derive(Eq, PartialEq)]
|
|
enum Notation
|
|
{
|
|
Prefix,
|
|
Infix,
|
|
}
|
|
|
|
let mut display_comparison = |notation, operator_identifier: &str, left, right| -> Result<(), std::fmt::Error>
|
|
{
|
|
if notation == Notation::Prefix
|
|
{
|
|
write!(format, "{}(", operator_identifier)?;
|
|
}
|
|
|
|
if is_arithmetic_term(left) && !is_arithmetic_term(right)
|
|
{
|
|
write!(format, "f__integer__({})", left.display_tptp())?;
|
|
}
|
|
else
|
|
{
|
|
write!(format, "{}", left.display_tptp())?;
|
|
}
|
|
|
|
match notation
|
|
{
|
|
Notation::Prefix => write!(format, ", ")?,
|
|
Notation::Infix => write!(format, " {} ", operator_identifier)?,
|
|
}
|
|
|
|
if is_arithmetic_term(right) && !is_arithmetic_term(left)
|
|
{
|
|
write!(format, "f__integer__({})", right.display_tptp())?;
|
|
}
|
|
else
|
|
{
|
|
write!(format, "{}", right.display_tptp())?;
|
|
}
|
|
|
|
if notation == Notation::Prefix
|
|
{
|
|
write!(format, ")")?;
|
|
}
|
|
|
|
Ok(())
|
|
};
|
|
|
|
match self.0
|
|
{
|
|
foliage::Formula::Exists(ref exists) =>
|
|
{
|
|
write!(format, "?[")?;
|
|
|
|
let mut separator = "";
|
|
|
|
for parameter in &exists.parameters
|
|
{
|
|
write!(format, "{}{:?}", separator, parameter.display_tptp())?;
|
|
|
|
separator = ", "
|
|
}
|
|
|
|
write!(format, "]: ({:?})", exists.argument.display_tptp())
|
|
},
|
|
foliage::Formula::ForAll(ref for_all) =>
|
|
{
|
|
write!(format, "![")?;
|
|
|
|
let mut separator = "";
|
|
|
|
for parameter in &for_all.parameters
|
|
{
|
|
write!(format, "{}{:?}", separator, parameter.display_tptp())?;
|
|
|
|
separator = ", "
|
|
}
|
|
|
|
write!(format, "]: ({:?})", for_all.argument.display_tptp())
|
|
},
|
|
foliage::Formula::Not(ref argument) => write!(format, "~({:?})", argument.display_tptp()),
|
|
foliage::Formula::And(ref arguments) =>
|
|
{
|
|
let mut separator = "";
|
|
|
|
for argument in arguments
|
|
{
|
|
write!(format, "{}{:?}", separator, argument.display_tptp())?;
|
|
|
|
separator = " & "
|
|
}
|
|
|
|
Ok(())
|
|
},
|
|
foliage::Formula::Or(ref arguments) =>
|
|
{
|
|
let mut separator = "";
|
|
|
|
for argument in arguments
|
|
{
|
|
write!(format, "{}{:?}", separator, argument.display_tptp())?;
|
|
|
|
separator = " | "
|
|
}
|
|
|
|
Ok(())
|
|
},
|
|
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::Boolean(value) =>
|
|
match value
|
|
{
|
|
true => write!(format, "$true"),
|
|
false => write!(format, "$false"),
|
|
},
|
|
foliage::Formula::Predicate(ref predicate) =>
|
|
{
|
|
write!(format, "{}", predicate.declaration.name)?;
|
|
|
|
if !predicate.arguments.is_empty()
|
|
{
|
|
write!(format, "(")?;
|
|
|
|
let mut separator = "";
|
|
|
|
for argument in &predicate.arguments
|
|
{
|
|
write!(format, "{}{:?}", separator, argument.display_tptp())?;
|
|
|
|
separator = ", "
|
|
}
|
|
|
|
write!(format, ")")?;
|
|
}
|
|
|
|
Ok(())
|
|
},
|
|
}
|
|
}
|
|
}
|
|
|
|
impl<'a> std::fmt::Display for FormulaDisplay<'a>
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
write!(format, "{:?}", self)
|
|
}
|
|
}
|
|
|
|
impl<'a> std::fmt::Debug for StatementKindDisplay<'a>
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
match &self.0
|
|
{
|
|
crate::project::StatementKind::Axiom => write!(format, "axiom, axiom"),
|
|
crate::project::StatementKind::Lemma => write!(format, "conjecture, lemma"),
|
|
crate::project::StatementKind::Conjecture => write!(format, "conjecture, conjecture"),
|
|
}
|
|
}
|
|
}
|
|
|
|
impl<'a> std::fmt::Display for StatementKindDisplay<'a>
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
write!(format, "{:?}", &self)
|
|
}
|
|
}
|
|
|
|
impl<'a> std::fmt::Debug for ProjectDisplay<'a>
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
let mut line_separator = "";
|
|
let mut section_separator = "";
|
|
|
|
if let Some(axioms) = self.0.statements.get(&crate::project::StatementKind::Axiom)
|
|
{
|
|
for axiom in axioms
|
|
{
|
|
write!(format, "{}tff({:?}, {:?}).", line_separator, crate::project::StatementKind::Axiom.display_tptp(), axiom.display_tptp())?;
|
|
line_separator = "\n";
|
|
}
|
|
|
|
section_separator = "\n";
|
|
}
|
|
|
|
if let Some(lemmas) = self.0.statements.get(&crate::project::StatementKind::Lemma)
|
|
{
|
|
write!(format, "{}", section_separator)?;
|
|
|
|
for lemma in lemmas
|
|
{
|
|
write!(format, "{}tff({:?}, {:?}).", line_separator, crate::project::StatementKind::Lemma.display_tptp(), lemma.display_tptp())?;
|
|
line_separator = "\n";
|
|
}
|
|
|
|
section_separator = "\n";
|
|
}
|
|
|
|
if let Some(conjectures) = self.0.statements.get(&crate::project::StatementKind::Conjecture)
|
|
{
|
|
write!(format, "{}", section_separator)?;
|
|
|
|
for conjecture in conjectures
|
|
{
|
|
write!(format, "{}tff({:?}, {:?}).", line_separator, crate::project::StatementKind::Conjecture.display_tptp(), conjecture.display_tptp())?;
|
|
line_separator = "\n";
|
|
}
|
|
}
|
|
|
|
Ok(())
|
|
}
|
|
}
|
|
|
|
impl<'a> std::fmt::Display for ProjectDisplay<'a>
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
write!(format, "{:?}", &self)
|
|
}
|
|
}
|