From 1968ed83ee5801f4dd41ba2ffd19378fb45586d6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Mon, 6 Apr 2020 13:33:48 +0200 Subject: [PATCH] Refactor precedence rules for formulas --- src/format/formulas.rs | 149 ++++++++++++++++++++++++++++++----------- 1 file changed, 111 insertions(+), 38 deletions(-) diff --git a/src/format/formulas.rs b/src/format/formulas.rs index 098d777..a59f838 100644 --- a/src/format/formulas.rs +++ b/src/format/formulas.rs @@ -29,6 +29,85 @@ impl super::Precedence for crate::Formula } } +#[derive(Clone, Copy, Eq, PartialEq)] +enum ChildPosition +{ + Any, + Antecedent, + Implication, +} + +fn requires_parentheses<'formula>(formula: &'formula crate::Formula, position: ChildPosition, + 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) if formulas.len() <= 1 + => false, + Formula::And(formulas) => match *parent_formula + { + Formula::Not(_) + | Formula::Exists(_) + | Formula::ForAll(_) + => true, + _ => false, + }, + Formula::Or(formulas) => 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::Or(formulas) => match *parent_formula + { + Formula::Not(_) + | Formula::Exists(_) + | Formula::ForAll(_) + | Formula::And(_) + | Formula::Implies(_) + => true, + _ => false, + }, + _ => true, + } +} + impl std::fmt::Debug for crate::ImplicationDirection { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result @@ -59,16 +138,20 @@ impl std::fmt::Display for crate::PredicateDeclaration struct FormulaDisplay<'formula> { - parentheses: Parentheses, formula: &'formula crate::Formula, + parent_formula: Option<&'formula crate::Formula>, + position: ChildPosition, } -fn display_formula(formula: &crate::Formula, parentheses: Parentheses) -> FormulaDisplay +fn display_formula<'formula>(formula: &'formula crate::Formula, + parent_formula: Option<&'formula crate::Formula>, position: ChildPosition) + -> FormulaDisplay<'formula> { FormulaDisplay { - parentheses, formula, + parent_formula, + position, } } @@ -77,14 +160,11 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { let precedence_level = self.formula.precedence_level(); - let requires_parentheses = match self.parentheses + let requires_parentheses = match self.parent_formula { - Parentheses::None => false, - Parentheses::PrecedenceBased(parent_precedence_level) - => precedence_level > parent_precedence_level, - Parentheses::Required => true, + Some(ref parent_formula) => requires_parentheses(self.formula, self.position, parent_formula), + None => false, }; - let parentheses = Parentheses::PrecedenceBased(precedence_level); if requires_parentheses { @@ -108,7 +188,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> separator = ", " } - write!(format, " {:?}", display_formula(&exists.argument, parentheses))?; + write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula), ChildPosition::Any))?; }, crate::Formula::ForAll(for_all) => { @@ -125,19 +205,25 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> separator = ", " } - write!(format, " {:?}", display_formula(&for_all.argument, parentheses))?; + write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula), ChildPosition::Any))?; }, crate::Formula::Not(argument) => write!(format, "not {:?}", - display_formula(argument, parentheses))?, + display_formula(argument, Some(self.formula), ChildPosition::Any))?, crate::Formula::And(arguments) => { let mut separator = ""; assert!(!arguments.is_empty()); + let parent_formula = match arguments.len() + { + 0 | 1 => self.parent_formula, + _ => Some(self.formula), + }; + for argument in arguments { - write!(format, "{}{:?}", separator, display_formula(argument, parentheses))?; + write!(format, "{}{:?}", separator, display_formula(argument, parent_formula, ChildPosition::Any))?; separator = " and " } @@ -148,42 +234,29 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> assert!(!arguments.is_empty()); + let parent_formula = match arguments.len() + { + 0 | 1 => self.parent_formula, + _ => Some(self.formula), + }; + for argument in arguments { - write!(format, "{}{:?}", separator, display_formula(argument, parentheses))?; + write!(format, "{}{:?}", separator, display_formula(argument, parent_formula, ChildPosition::Any))?; separator = " or " } }, crate::Formula::Implies(crate::Implies{direction, antecedent, implication}) => { - let antecedent_parentheses = match **antecedent - { - // Implication is right-associative and thus requires parentheses when nested on - // the antecedent side - crate::Formula::Implies(_) => Parentheses::Required, - _ => parentheses, - }; - - let implication_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 => Parentheses::None, - // If the nested implication is in the other direction, parentheses are needed - crate::Formula::Implies(_) => Parentheses::Required, - _ => parentheses, - }; - let format_antecedent = |format: &mut std::fmt::Formatter| -> Result<_, _> { - write!(format, "{:?}", display_formula(antecedent, antecedent_parentheses)) + write!(format, "{:?}", display_formula(antecedent, Some(self.formula), ChildPosition::Antecedent)) }; let format_implication = |format: &mut std::fmt::Formatter| -> Result<_, _> { - write!(format, "{:?}", display_formula(implication, implication_parentheses)) + write!(format, "{:?}", display_formula(implication, Some(self.formula), ChildPosition::Implication)) }; match direction @@ -208,7 +281,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> for argument in arguments { - write!(format, "{}{:?}", separator, display_formula(argument, parentheses))?; + write!(format, "{}{:?}", separator, display_formula(argument, Some(self.formula), ChildPosition::Any))?; separator = " <-> "; } @@ -283,7 +356,7 @@ impl std::fmt::Debug for crate::Formula { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(format, "{:?}", display_formula(&self, Parentheses::None)) + write!(format, "{:?}", display_formula(&self, None, ChildPosition::Any)) } } @@ -291,7 +364,7 @@ impl std::fmt::Display for crate::Formula { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(format, "{}", display_formula(&self, Parentheses::None)) + write!(format, "{}", display_formula(&self, None, ChildPosition::Any)) } }