344 lines
8.2 KiB
Rust
344 lines
8.2 KiB
Rust
use super::*;
|
||
|
||
impl super::Precedence for crate::Formula
|
||
{
|
||
fn precedence(&self) -> i32
|
||
{
|
||
match &self
|
||
{
|
||
Self::Predicate(_)
|
||
| Self::Boolean(_)
|
||
| Self::Compare(_)
|
||
=> 0,
|
||
Self::Exists(_)
|
||
| Self::ForAll(_)
|
||
=> 1,
|
||
Self::Not(_)
|
||
=> 2,
|
||
Self::And(_)
|
||
=> 3,
|
||
Self::Or(_)
|
||
=> 4,
|
||
Self::Implies(_)
|
||
=> 5,
|
||
Self::IfAndOnlyIf(_)
|
||
=> 6,
|
||
}
|
||
}
|
||
}
|
||
|
||
impl std::fmt::Debug for crate::ImplicationDirection
|
||
{
|
||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||
{
|
||
match &self
|
||
{
|
||
Self::LeftToRight => write!(format, "left to right"),
|
||
Self::RightToLeft => write!(format, "right to left"),
|
||
}
|
||
}
|
||
}
|
||
|
||
impl std::fmt::Debug for crate::PredicateDeclaration
|
||
{
|
||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||
{
|
||
write!(format, "{}/{}", &self.name, self.arity)
|
||
}
|
||
}
|
||
|
||
impl std::fmt::Display for crate::PredicateDeclaration
|
||
{
|
||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||
{
|
||
write!(format, "{:?}", &self)
|
||
}
|
||
}
|
||
|
||
struct FormulaDisplay<'formula>
|
||
{
|
||
parent_precedence: Option<i32>,
|
||
formula: &'formula crate::Formula,
|
||
}
|
||
|
||
fn display_formula(formula: &crate::Formula, parent_precedence: Option<i32>) -> FormulaDisplay
|
||
{
|
||
FormulaDisplay
|
||
{
|
||
parent_precedence,
|
||
formula,
|
||
}
|
||
}
|
||
|
||
impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
||
{
|
||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||
{
|
||
let precedence = self.formula.precedence();
|
||
let requires_parentheses = match self.parent_precedence
|
||
{
|
||
Some(parent_precedence) => precedence > parent_precedence,
|
||
None => false,
|
||
};
|
||
let precedence = Some(precedence);
|
||
|
||
if requires_parentheses
|
||
{
|
||
write!(format, "(")?;
|
||
}
|
||
|
||
match &self.formula
|
||
{
|
||
crate::Formula::Exists(exists) =>
|
||
{
|
||
assert!(!exists.parameters.is_empty());
|
||
|
||
write!(format, "exists")?;
|
||
|
||
let mut separator = " ";
|
||
|
||
for parameter in exists.parameters.iter()
|
||
{
|
||
write!(format, "{}{:?}", separator, parameter)?;
|
||
|
||
separator = ", "
|
||
}
|
||
|
||
write!(format, " {:?}", display_formula(&exists.argument, precedence))?;
|
||
},
|
||
crate::Formula::ForAll(for_all) =>
|
||
{
|
||
assert!(!for_all.parameters.is_empty());
|
||
|
||
write!(format, "forall")?;
|
||
|
||
let mut separator = " ";
|
||
|
||
for parameter in for_all.parameters.iter()
|
||
{
|
||
write!(format, "{}{:?}", separator, parameter)?;
|
||
|
||
separator = ", "
|
||
}
|
||
|
||
write!(format, " {:?}", display_formula(&for_all.argument, precedence))?;
|
||
},
|
||
crate::Formula::Not(argument) => write!(format, "not {:?}",
|
||
display_formula(argument, precedence))?,
|
||
crate::Formula::And(arguments) =>
|
||
{
|
||
let mut separator = "";
|
||
|
||
assert!(!arguments.is_empty());
|
||
|
||
for argument in arguments
|
||
{
|
||
write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
|
||
|
||
separator = " and "
|
||
}
|
||
},
|
||
crate::Formula::Or(arguments) =>
|
||
{
|
||
let mut separator = "";
|
||
|
||
assert!(!arguments.is_empty());
|
||
|
||
for argument in arguments
|
||
{
|
||
write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
|
||
|
||
separator = " or "
|
||
}
|
||
},
|
||
crate::Formula::Implies(crate::Implies{direction, antecedent, implication}) =>
|
||
{
|
||
let antecedent_requires_parentheses = match **antecedent
|
||
{
|
||
// Implication is right-associative and thus requires parentheses when nested on
|
||
// the antecedent side
|
||
crate::Formula::Implies(_) => true,
|
||
_ => false,
|
||
};
|
||
|
||
let implication_requires_parentheses = match **antecedent
|
||
{
|
||
// Implication is right-associative and thus doesn’t require parentheses when
|
||
// nested on the implication side with the same implication direction
|
||
crate::Formula::Implies(crate::Implies{direction: nested_direction, ..})
|
||
if nested_direction == *direction => false,
|
||
// If the nested implication is in the other direction, parentheses are needed
|
||
crate::Formula::Implies(_) => true,
|
||
_ => false,
|
||
};
|
||
|
||
let format_antecedent = |format: &mut std::fmt::Formatter| -> Result<_, _>
|
||
{
|
||
if antecedent_requires_parentheses
|
||
{
|
||
write!(format, "(")?;
|
||
}
|
||
|
||
write!(format, "{:?}", display_formula(antecedent, precedence))?;
|
||
|
||
if antecedent_requires_parentheses
|
||
{
|
||
write!(format, ")")?;
|
||
}
|
||
|
||
Ok(())
|
||
};
|
||
|
||
let format_implication = |format: &mut std::fmt::Formatter| -> Result<_, _>
|
||
{
|
||
if implication_requires_parentheses
|
||
{
|
||
write!(format, "(")?;
|
||
}
|
||
|
||
write!(format, "{:?}", display_formula(implication, precedence))?;
|
||
|
||
if implication_requires_parentheses
|
||
{
|
||
write!(format, ")")?;
|
||
}
|
||
|
||
Ok(())
|
||
};
|
||
|
||
match direction
|
||
{
|
||
crate::ImplicationDirection::LeftToRight =>
|
||
{
|
||
format_antecedent(format)?;
|
||
write!(format, " -> ")?;
|
||
format_implication(format)?;
|
||
},
|
||
crate::ImplicationDirection::RightToLeft =>
|
||
{
|
||
format_implication(format)?;
|
||
write!(format, " <- ")?;
|
||
format_antecedent(format)?;
|
||
},
|
||
}
|
||
},
|
||
crate::Formula::IfAndOnlyIf(arguments) =>
|
||
{
|
||
let mut separator = "";
|
||
|
||
for argument in arguments
|
||
{
|
||
write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
|
||
|
||
separator = " <-> ";
|
||
}
|
||
},
|
||
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) =>
|
||
{
|
||
write!(format, "{}", predicate.declaration.name)?;
|
||
|
||
if !predicate.arguments.is_empty()
|
||
{
|
||
write!(format, "(")?;
|
||
|
||
let mut separator = "";
|
||
|
||
for argument in &predicate.arguments
|
||
{
|
||
write!(format, "{}{:?}", separator, display_term(argument, None))?;
|
||
|
||
separator = ", "
|
||
}
|
||
|
||
write!(format, ")")?;
|
||
}
|
||
},
|
||
}
|
||
|
||
if requires_parentheses
|
||
{
|
||
write!(format, ")")?;
|
||
}
|
||
|
||
Ok(())
|
||
}
|
||
}
|
||
|
||
impl<'formula> std::fmt::Display for FormulaDisplay<'formula>
|
||
{
|
||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||
{
|
||
write!(format, "{:?}", self)
|
||
}
|
||
}
|
||
|
||
impl std::fmt::Debug for crate::Formula
|
||
{
|
||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||
{
|
||
write!(format, "{:?}", display_formula(&self, None))
|
||
}
|
||
}
|
||
|
||
impl std::fmt::Display for crate::Formula
|
||
{
|
||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||
{
|
||
write!(format, "{}", display_formula(&self, None))
|
||
}
|
||
}
|
||
|
||
#[cfg(test)]
|
||
mod tests
|
||
{
|
||
use crate::*;
|
||
|
||
fn format(formula: &ast::Formula) -> String
|
||
{
|
||
format!("{}", formula)
|
||
}
|
||
|
||
#[test]
|
||
fn compare()
|
||
{
|
||
let ad = std::rc::Rc::new(FunctionDeclaration::new("a".to_string(), 0));
|
||
let bd = std::rc::Rc::new(FunctionDeclaration::new("b".to_string(), 0));
|
||
|
||
let a = || Box::new(Term::function(std::rc::Rc::clone(&ad), vec![]));
|
||
let b = || Box::new(Term::function(std::rc::Rc::clone(&bd), vec![]));
|
||
|
||
assert_eq!(format(&Formula::greater(a(), b())), "a > b");
|
||
assert_eq!(format(&Formula::less(a(), b())), "a < b");
|
||
assert_eq!(format(&Formula::less_or_equal(a(), b())), "a <= b");
|
||
assert_eq!(format(&Formula::greater_or_equal(a(), b())), "a >= b");
|
||
assert_eq!(format(&Formula::equal(a(), b())), "a = b");
|
||
assert_eq!(format(&Formula::not_equal(a(), b())), "a != b");
|
||
}
|
||
}
|