Refactor parenthesis requirement check
This commit is contained in:
parent
80d7460ec1
commit
e0dbb8b75f
@ -1,77 +1,5 @@
|
|||||||
use super::*;
|
use super::*;
|
||||||
|
|
||||||
fn requires_parentheses<'formula>(formula: &'formula crate::Formula,
|
|
||||||
parent_formula: &'formula crate::Formula)
|
|
||||||
-> bool
|
|
||||||
{
|
|
||||||
use crate::Formula;
|
|
||||||
|
|
||||||
match formula
|
|
||||||
{
|
|
||||||
Formula::Predicate(_)
|
|
||||||
| Formula::Boolean(_)
|
|
||||||
| Formula::Compare(_)
|
|
||||||
| Formula::Not(_)
|
|
||||||
| Formula::Exists(_)
|
|
||||||
| Formula::ForAll(_)
|
|
||||||
=> false,
|
|
||||||
Formula::And(formulas)
|
|
||||||
| Formula::Or(formulas)
|
|
||||||
| Formula::IfAndOnlyIf(formulas) if formulas.len() <= 1
|
|
||||||
=> false,
|
|
||||||
Formula::And(_) => match *parent_formula
|
|
||||||
{
|
|
||||||
Formula::Not(_)
|
|
||||||
| Formula::Exists(_)
|
|
||||||
| Formula::ForAll(_)
|
|
||||||
=> true,
|
|
||||||
_ => false,
|
|
||||||
},
|
|
||||||
Formula::Or(_) => match *parent_formula
|
|
||||||
{
|
|
||||||
Formula::Not(_)
|
|
||||||
| Formula::Exists(_)
|
|
||||||
| Formula::ForAll(_)
|
|
||||||
| Formula::And(_)
|
|
||||||
=> true,
|
|
||||||
_ => false,
|
|
||||||
},
|
|
||||||
Formula::Implies(crate::Implies{direction, ..}) => match &*parent_formula
|
|
||||||
{
|
|
||||||
Formula::Not(_)
|
|
||||||
| Formula::Exists(_)
|
|
||||||
| Formula::ForAll(_)
|
|
||||||
| Formula::And(_)
|
|
||||||
| Formula::Or(_)
|
|
||||||
=> true,
|
|
||||||
Formula::Implies(
|
|
||||||
crate::Implies{direction: parent_direction, antecedent: parent_antecedent, ..}) =>
|
|
||||||
if direction == parent_direction
|
|
||||||
{
|
|
||||||
// Implications with the same direction nested on the antecedent side require
|
|
||||||
// parentheses because implication is considered right-associative
|
|
||||||
std::ptr::eq(formula, &**parent_antecedent)
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
true
|
|
||||||
},
|
|
||||||
_ => false,
|
|
||||||
},
|
|
||||||
Formula::IfAndOnlyIf(_) => match *parent_formula
|
|
||||||
{
|
|
||||||
Formula::Not(_)
|
|
||||||
| Formula::Exists(_)
|
|
||||||
| Formula::ForAll(_)
|
|
||||||
| Formula::And(_)
|
|
||||||
| Formula::Or(_)
|
|
||||||
| Formula::Implies(_)
|
|
||||||
=> true,
|
|
||||||
_ => false,
|
|
||||||
},
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl std::fmt::Debug for crate::ImplicationDirection
|
impl std::fmt::Debug for crate::ImplicationDirection
|
||||||
{
|
{
|
||||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||||
@ -106,6 +34,85 @@ struct FormulaDisplay<'formula>
|
|||||||
parent_formula: Option<&'formula crate::Formula>,
|
parent_formula: Option<&'formula crate::Formula>,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
impl<'formula> FormulaDisplay<'formula>
|
||||||
|
{
|
||||||
|
fn requires_parentheses(&self) -> bool
|
||||||
|
{
|
||||||
|
use crate::Formula;
|
||||||
|
|
||||||
|
let parent_formula = match self.parent_formula
|
||||||
|
{
|
||||||
|
Some(parent_formula) => parent_formula,
|
||||||
|
None => return false,
|
||||||
|
};
|
||||||
|
|
||||||
|
match self.formula
|
||||||
|
{
|
||||||
|
Formula::Predicate(_)
|
||||||
|
| Formula::Boolean(_)
|
||||||
|
| Formula::Compare(_)
|
||||||
|
| Formula::Not(_)
|
||||||
|
| Formula::Exists(_)
|
||||||
|
| Formula::ForAll(_)
|
||||||
|
=> false,
|
||||||
|
Formula::And(formulas)
|
||||||
|
| Formula::Or(formulas)
|
||||||
|
| Formula::IfAndOnlyIf(formulas) if formulas.len() <= 1
|
||||||
|
=> false,
|
||||||
|
Formula::And(_) => match *parent_formula
|
||||||
|
{
|
||||||
|
Formula::Not(_)
|
||||||
|
| Formula::Exists(_)
|
||||||
|
| Formula::ForAll(_)
|
||||||
|
=> true,
|
||||||
|
_ => false,
|
||||||
|
},
|
||||||
|
Formula::Or(_) => match *parent_formula
|
||||||
|
{
|
||||||
|
Formula::Not(_)
|
||||||
|
| Formula::Exists(_)
|
||||||
|
| Formula::ForAll(_)
|
||||||
|
| Formula::And(_)
|
||||||
|
=> true,
|
||||||
|
_ => false,
|
||||||
|
},
|
||||||
|
Formula::Implies(crate::Implies{direction, ..}) => match &*parent_formula
|
||||||
|
{
|
||||||
|
Formula::Not(_)
|
||||||
|
| Formula::Exists(_)
|
||||||
|
| Formula::ForAll(_)
|
||||||
|
| Formula::And(_)
|
||||||
|
| Formula::Or(_)
|
||||||
|
=> true,
|
||||||
|
Formula::Implies(crate::Implies{direction: parent_direction,
|
||||||
|
antecedent: parent_antecedent, ..}) =>
|
||||||
|
if direction == parent_direction
|
||||||
|
{
|
||||||
|
// Implications with the same direction nested on the antecedent side require
|
||||||
|
// parentheses because implication is considered right-associative
|
||||||
|
std::ptr::eq(self.formula, &**parent_antecedent)
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
true
|
||||||
|
},
|
||||||
|
_ => false,
|
||||||
|
},
|
||||||
|
Formula::IfAndOnlyIf(_) => match *parent_formula
|
||||||
|
{
|
||||||
|
Formula::Not(_)
|
||||||
|
| Formula::Exists(_)
|
||||||
|
| Formula::ForAll(_)
|
||||||
|
| Formula::And(_)
|
||||||
|
| Formula::Or(_)
|
||||||
|
| Formula::Implies(_)
|
||||||
|
=> true,
|
||||||
|
_ => false,
|
||||||
|
},
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
fn display_formula<'formula>(formula: &'formula crate::Formula,
|
fn display_formula<'formula>(formula: &'formula crate::Formula,
|
||||||
parent_formula: Option<&'formula crate::Formula>)
|
parent_formula: Option<&'formula crate::Formula>)
|
||||||
-> FormulaDisplay<'formula>
|
-> FormulaDisplay<'formula>
|
||||||
@ -121,11 +128,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|||||||
{
|
{
|
||||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||||
{
|
{
|
||||||
let requires_parentheses = match self.parent_formula
|
let requires_parentheses = self.requires_parentheses();
|
||||||
{
|
|
||||||
Some(ref parent_formula) => requires_parentheses(self.formula, parent_formula),
|
|
||||||
None => false,
|
|
||||||
};
|
|
||||||
|
|
||||||
if requires_parentheses
|
if requires_parentheses
|
||||||
{
|
{
|
||||||
|
Loading…
Reference in New Issue
Block a user