Compare commits
No commits in common. "master" and "prepare-0.1.0" have entirely different histories.
master
...
prepare-0.
|
@ -1,4 +1,4 @@
|
|||
# foliage [![crates.io](https://img.shields.io/crates/v/foliage.svg?maxAge=3600)](https://crates.io/crates/foliage)
|
||||
# foliage [![GitHub release](https://img.shields.io/github/release/potassco/foliage.svg?maxAge=3600)](https://github.com/potassco/foliage/releases) [![crates.io](https://img.shields.io/crates/v/foliage.svg?maxAge=3600)](https://crates.io/crates/foliage)
|
||||
|
||||
> First-order logic with integer arithmetics in Rust
|
||||
|
||||
|
|
|
@ -379,8 +379,7 @@ impl Term
|
|||
Self::boolean(false)
|
||||
}
|
||||
|
||||
pub fn function(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>)
|
||||
-> Self
|
||||
pub fn function(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
|
||||
{
|
||||
Self::Function(Function::new(declaration, arguments))
|
||||
}
|
||||
|
@ -552,8 +551,7 @@ impl Formula
|
|||
Self::Or(arguments)
|
||||
}
|
||||
|
||||
pub fn predicate(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>)
|
||||
-> Self
|
||||
pub fn predicate(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
|
||||
{
|
||||
Self::Predicate(Predicate::new(declaration, arguments))
|
||||
}
|
||||
|
|
143
src/format.rs
143
src/format.rs
|
@ -16,25 +16,18 @@ impl Precedence for crate::Term
|
|||
| Self::String(_)
|
||||
| Self::Variable(_)
|
||||
=> 0,
|
||||
Self::UnaryOperation(
|
||||
crate::UnaryOperation{operator: crate::UnaryOperator::Negative, ..})
|
||||
Self::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::Negative, ..})
|
||||
=> 1,
|
||||
Self::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, ..})
|
||||
Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, ..})
|
||||
=> 2,
|
||||
Self::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, ..})
|
||||
| Self::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Divide, ..})
|
||||
| Self::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..})
|
||||
Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, ..})
|
||||
| Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Divide, ..})
|
||||
| Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..})
|
||||
=> 3,
|
||||
Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Add, ..})
|
||||
| Self::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, ..})
|
||||
| Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, ..})
|
||||
=> 4,
|
||||
Self::UnaryOperation(
|
||||
crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..})
|
||||
Self::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..})
|
||||
=> 5,
|
||||
}
|
||||
}
|
||||
|
@ -67,26 +60,6 @@ impl Precedence for crate::Formula
|
|||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Debug for crate::SpecialInteger
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
match &self
|
||||
{
|
||||
crate::SpecialInteger::Infimum => write!(format, "#inf"),
|
||||
crate::SpecialInteger::Supremum => write!(format, "#sup"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Display for crate::SpecialInteger
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{:?}", &self)
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Debug for crate::FunctionDeclaration
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
|
@ -141,7 +114,8 @@ struct TermDisplay<'term>
|
|||
term: &'term crate::Term,
|
||||
}
|
||||
|
||||
fn display_term(term: &crate::Term, parent_precedence: Option<i32>) -> TermDisplay
|
||||
fn display_term<'term>(term: &'term crate::Term, parent_precedence: Option<i32>)
|
||||
-> TermDisplay<'term>
|
||||
{
|
||||
TermDisplay
|
||||
{
|
||||
|
@ -171,7 +145,8 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
|
|||
{
|
||||
crate::Term::Boolean(true) => write!(format, "true"),
|
||||
crate::Term::Boolean(false) => write!(format, "false"),
|
||||
crate::Term::SpecialInteger(value) => write!(format, "{:?}", value),
|
||||
crate::Term::SpecialInteger(crate::SpecialInteger::Infimum) => write!(format, "#inf"),
|
||||
crate::Term::SpecialInteger(crate::SpecialInteger::Supremum) => write!(format, "#sup"),
|
||||
crate::Term::Integer(value) => write!(format, "{}", value),
|
||||
crate::Term::String(value) => write!(format, "\"{}\"", value),
|
||||
crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration),
|
||||
|
@ -180,12 +155,12 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
|
|||
write!(format, "{}", function.declaration.name)?;
|
||||
|
||||
assert!(function.declaration.arity == function.arguments.len(),
|
||||
"number of function arguments differs from declaration (expected {}, got {})",
|
||||
"function has a different number of arguments than declared (expected {}, got {})",
|
||||
function.declaration.arity, function.arguments.len());
|
||||
|
||||
if !function.arguments.is_empty()
|
||||
if function.arguments.len() > 0
|
||||
{
|
||||
write!(format, "(")?;
|
||||
write!(format, "{}(", function.declaration.name)?;
|
||||
|
||||
let mut separator = "";
|
||||
|
||||
|
@ -201,35 +176,21 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
|
|||
|
||||
Ok(())
|
||||
},
|
||||
crate::Term::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Add, left, right})
|
||||
=> write!(format, "{:?} + {:?}", display_term(left, precedence),
|
||||
display_term(right, precedence)),
|
||||
crate::Term::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, left, right})
|
||||
=> write!(format, "{:?} - {:?}", display_term(left, precedence),
|
||||
display_term(right, precedence)),
|
||||
crate::Term::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, left, right})
|
||||
=> write!(format, "{:?} * {:?}", display_term(left, precedence),
|
||||
display_term(right, precedence)),
|
||||
crate::Term::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Divide, left, right})
|
||||
=> write!(format, "{:?} / {:?}", display_term(left, precedence),
|
||||
display_term(right, precedence)),
|
||||
crate::Term::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, left, right})
|
||||
=> write!(format, "{:?} % {:?}", display_term(left, precedence),
|
||||
display_term(right, precedence)),
|
||||
crate::Term::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, left, right})
|
||||
=> write!(format, "{:?} ** {:?}", display_term(left, precedence),
|
||||
display_term(right, precedence)),
|
||||
crate::Term::UnaryOperation(
|
||||
crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
|
||||
crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Add, left, right})
|
||||
=> write!(format, "{:?} + {:?}", display_term(left, precedence), display_term(right, precedence)),
|
||||
crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, left, right})
|
||||
=> write!(format, "{:?} - {:?}", display_term(left, precedence), display_term(right, precedence)),
|
||||
crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, left, right})
|
||||
=> write!(format, "{:?} * {:?}", display_term(left, precedence), display_term(right, precedence)),
|
||||
crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Divide, left, right})
|
||||
=> write!(format, "{:?} / {:?}", display_term(left, precedence), display_term(right, precedence)),
|
||||
crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, left, right})
|
||||
=> write!(format, "{:?} % {:?}", display_term(left, precedence), display_term(right, precedence)),
|
||||
crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, left, right})
|
||||
=> write!(format, "{:?} ** {:?}", display_term(left, precedence), display_term(right, precedence)),
|
||||
crate::Term::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
|
||||
=> write!(format, "-{:?}", display_term(argument, precedence)),
|
||||
crate::Term::UnaryOperation(
|
||||
crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
|
||||
crate::Term::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
|
||||
=> write!(format, "|{:?}|", display_term(argument, precedence)),
|
||||
}?;
|
||||
|
||||
|
@ -256,7 +217,8 @@ struct FormulaDisplay<'formula>
|
|||
formula: &'formula crate::Formula,
|
||||
}
|
||||
|
||||
fn display_formula(formula: &crate::Formula, parent_precedence: Option<i32>) -> FormulaDisplay
|
||||
fn display_formula<'formula>(formula: &'formula crate::Formula, parent_precedence: Option<i32>)
|
||||
-> FormulaDisplay<'formula>
|
||||
{
|
||||
FormulaDisplay
|
||||
{
|
||||
|
@ -318,8 +280,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|||
|
||||
write!(format, " {:?}", display_formula(&for_all.argument, precedence))?;
|
||||
},
|
||||
crate::Formula::Not(argument) => write!(format, "not {:?}",
|
||||
display_formula(argument, precedence))?,
|
||||
crate::Formula::Not(argument) => write!(format, "not {:?}", display_formula(argument, precedence))?,
|
||||
crate::Formula::And(arguments) =>
|
||||
{
|
||||
let mut separator = "";
|
||||
|
@ -347,35 +308,21 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|||
}
|
||||
},
|
||||
crate::Formula::Implies(crate::Implies{antecedent, implication})
|
||||
=> write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence),
|
||||
display_formula(implication, precedence))?,
|
||||
=> write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence), display_formula(implication, precedence))?,
|
||||
crate::Formula::IfAndOnlyIf(crate::IfAndOnlyIf{left, right})
|
||||
=> write!(format, "{:?} <-> {:?}", display_formula(left, precedence),
|
||||
display_formula(right, precedence))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
|
||||
=> write!(format, "{:?} < {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
|
||||
=> write!(format, "{:?} <= {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
|
||||
=> write!(format, "{:?} > {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
|
||||
=> write!(format, "{:?} >= {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::Equal, left, right})
|
||||
=> write!(format, "{:?} = {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right})
|
||||
=> write!(format, "{:?} != {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
=> write!(format, "{:?} <-> {:?}", display_formula(left, precedence), display_formula(right, precedence))?,
|
||||
crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
|
||||
=> write!(format, "{:?} < {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
|
||||
=> write!(format, "{:?} <= {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
|
||||
=> write!(format, "{:?} > {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
|
||||
=> write!(format, "{:?} >= {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::Equal, left, right})
|
||||
=> write!(format, "{:?} = {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right})
|
||||
=> write!(format, "{:?} != {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::Boolean(true) => write!(format, "#true")?,
|
||||
crate::Formula::Boolean(false) => write!(format, "#false")?,
|
||||
crate::Formula::Predicate(predicate) =>
|
||||
|
|
Loading…
Reference in New Issue