Refactor precedence rules for formulas

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,
+			Some(ref parent_formula) => requires_parentheses(self.formula, self.position, parent_formula),
-			Parentheses::PrecedenceBased(parent_precedence_level)
+			None => false,
-				=> precedence_level > parent_precedence_level,
-			Parentheses::Required => true,
 		};
-		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))
 	}
 }