diff --git a/src/format/formulas.rs b/src/format/formulas.rs index 631f21b..680bfdc 100644 --- a/src/format/formulas.rs +++ b/src/format/formulas.rs @@ -29,7 +29,7 @@ impl std::fmt::Display for crate::PredicateDeclaration } #[derive(Clone, Copy, Eq, PartialEq)] -enum ChildPosition +enum FormulaChildPosition { Any, ImpliesAntecedent, @@ -39,7 +39,7 @@ struct FormulaDisplay<'formula> { formula: &'formula crate::Formula, parent_formula: Option<&'formula crate::Formula>, - position: ChildPosition, + position: FormulaChildPosition, } impl<'formula> FormulaDisplay<'formula> @@ -97,7 +97,7 @@ impl<'formula> FormulaDisplay<'formula> { // Implications with the same direction nested on the antecedent side // require parentheses because implication is considered right-associative - self.position == ChildPosition::ImpliesAntecedent + self.position == FormulaChildPosition::ImpliesAntecedent } else { @@ -113,7 +113,7 @@ impl<'formula> FormulaDisplay<'formula> } fn display_formula<'formula>(formula: &'formula crate::Formula, - parent_formula: Option<&'formula crate::Formula>, position: ChildPosition) + parent_formula: Option<&'formula crate::Formula>, position: FormulaChildPosition) -> FormulaDisplay<'formula> { FormulaDisplay @@ -158,7 +158,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> } write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula), - ChildPosition::Any))?; + FormulaChildPosition::Any))?; } }, crate::Formula::ForAll(for_all) => @@ -182,11 +182,11 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> } write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula), - ChildPosition::Any))?; + FormulaChildPosition::Any))?; } }, crate::Formula::Not(argument) => write!(format, "not {:?}", - display_formula(argument, Some(self.formula), ChildPosition::Any))?, + display_formula(argument, Some(self.formula), FormulaChildPosition::Any))?, crate::Formula::And(arguments) => { if arguments.is_empty() @@ -198,7 +198,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> let (parent_formula, position) = match arguments.len() { 1 => (self.parent_formula, self.position), - _ => (Some(self.formula), ChildPosition::Any), + _ => (Some(self.formula), FormulaChildPosition::Any), }; let mut separator = ""; @@ -223,7 +223,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> let (parent_formula, position) = match arguments.len() { 1 => (self.parent_formula, self.position), - _ => (Some(self.formula), ChildPosition::Any), + _ => (Some(self.formula), FormulaChildPosition::Any), }; let mut separator = ""; @@ -243,13 +243,13 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> { write!(format, "{:?}", display_formula(antecedent, Some(self.formula), - ChildPosition::ImpliesAntecedent)) + FormulaChildPosition::ImpliesAntecedent)) }; let format_implication = |format: &mut std::fmt::Formatter| -> Result<_, _> { write!(format, "{:?}", - display_formula(implication, Some(self.formula), ChildPosition::Any)) + display_formula(implication, Some(self.formula), FormulaChildPosition::Any)) }; match direction @@ -279,7 +279,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> let (parent_formula, position) = match arguments.len() { 1 => (self.parent_formula, self.position), - _ => (Some(self.formula), ChildPosition::Any), + _ => (Some(self.formula), FormulaChildPosition::Any), }; let mut separator = ""; @@ -293,37 +293,23 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> } } }, - // TODO: refactor - crate::Formula::Compare( - crate::Compare{operator: crate::ComparisonOperator::Less, left, right}) - => write!(format, "{:?} < {:?}", - display_term(left, None, crate::format::terms::ChildPosition::Any), - display_term(right, None, crate::format::terms::ChildPosition::Any))?, - crate::Formula::Compare( - crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right}) - => write!(format, "{:?} <= {:?}", - display_term(left, None, crate::format::terms::ChildPosition::Any), - display_term(right, None, crate::format::terms::ChildPosition::Any))?, - crate::Formula::Compare( - crate::Compare{operator: crate::ComparisonOperator::Greater, left, right}) - => write!(format, "{:?} > {:?}", - display_term(left, None, crate::format::terms::ChildPosition::Any), - display_term(right, None, crate::format::terms::ChildPosition::Any))?, - crate::Formula::Compare( - crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right}) - => write!(format, "{:?} >= {:?}", - display_term(left, None, crate::format::terms::ChildPosition::Any), - display_term(right, None, crate::format::terms::ChildPosition::Any))?, - crate::Formula::Compare( - crate::Compare{operator: crate::ComparisonOperator::Equal, left, right}) - => write!(format, "{:?} = {:?}", - display_term(left, None, crate::format::terms::ChildPosition::Any), - display_term(right, None, crate::format::terms::ChildPosition::Any))?, - crate::Formula::Compare( - crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right}) - => write!(format, "{:?} != {:?}", - display_term(left, None, crate::format::terms::ChildPosition::Any), - display_term(right, None, crate::format::terms::ChildPosition::Any))?, + crate::Formula::Compare(compare) => + { + let operator_string = match compare.operator + { + crate::ComparisonOperator::Less => "<", + crate::ComparisonOperator::LessOrEqual => "<=", + crate::ComparisonOperator::Greater => ">", + crate::ComparisonOperator::GreaterOrEqual => ">=", + crate::ComparisonOperator::Equal => "=", + crate::ComparisonOperator::NotEqual => "!=", + }; + + write!(format, "{:?} {} {:?}", + display_term(&compare.left, None, TermChildPosition::Any), + operator_string, + display_term(&compare.right, None, TermChildPosition::Any))? + }, crate::Formula::Boolean(true) => write!(format, "true")?, crate::Formula::Boolean(false) => write!(format, "false")?, crate::Formula::Predicate(predicate) => @@ -339,7 +325,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> for argument in &predicate.arguments { write!(format, "{}{:?}", separator, display_term(argument, None, - crate::format::terms::ChildPosition::Any))?; + TermChildPosition::Any))?; separator = ", " } @@ -370,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, None, ChildPosition::Any)) + write!(format, "{:?}", display_formula(&self, None, FormulaChildPosition::Any)) } } @@ -378,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, None, ChildPosition::Any)) + write!(format, "{}", display_formula(&self, None, FormulaChildPosition::Any)) } } diff --git a/src/format/terms.rs b/src/format/terms.rs index 319d4cd..d378164 100644 --- a/src/format/terms.rs +++ b/src/format/terms.rs @@ -1,5 +1,5 @@ #[derive(Clone, Copy, Eq, PartialEq)] -pub(crate) enum ChildPosition +pub(crate) enum TermChildPosition { Any, Left, @@ -62,7 +62,7 @@ pub(crate) struct TermDisplay<'term> { term: &'term crate::Term, parent_term: Option<&'term crate::Term>, - position: ChildPosition, + position: TermChildPosition, } impl<'term> TermDisplay<'term> @@ -110,7 +110,7 @@ impl<'term> TermDisplay<'term> { crate::BinaryOperator::Exponentiate => parent_binary_operation.operator == crate::BinaryOperator::Exponentiate - && self.position == ChildPosition::Left, + && self.position == TermChildPosition::Left, crate::BinaryOperator::Multiply | crate::BinaryOperator::Divide => match parent_binary_operation.operator @@ -118,7 +118,7 @@ impl<'term> TermDisplay<'term> crate::BinaryOperator::Exponentiate => true, crate::BinaryOperator::Divide | crate::BinaryOperator::Modulo - => self.position == ChildPosition::Right, + => self.position == TermChildPosition::Right, _ => false, }, crate::BinaryOperator::Modulo => match parent_binary_operation.operator @@ -127,7 +127,7 @@ impl<'term> TermDisplay<'term> crate::BinaryOperator::Multiply | crate::BinaryOperator::Divide | crate::BinaryOperator::Modulo - => self.position == ChildPosition::Right, + => self.position == TermChildPosition::Right, _ => false, }, crate::BinaryOperator::Add @@ -140,7 +140,7 @@ impl<'term> TermDisplay<'term> | crate::BinaryOperator::Modulo => true, crate::BinaryOperator::Subtract - => self.position == ChildPosition::Right, + => self.position == TermChildPosition::Right, _ => false, }, } @@ -150,7 +150,7 @@ impl<'term> TermDisplay<'term> } pub(crate) fn display_term<'term>(term: &'term crate::Term, parent_term: Option<&'term crate::Term>, - position: ChildPosition) + position: TermChildPosition) -> TermDisplay<'term> { TermDisplay @@ -198,7 +198,7 @@ impl<'term> std::fmt::Debug for TermDisplay<'term> for argument in &function.arguments { write!(format, "{}{:?}", separator, - display_term(&argument, Some(self.term), ChildPosition::Any))?; + display_term(&argument, Some(self.term), TermChildPosition::Any))?; separator = ", "; } @@ -221,18 +221,18 @@ impl<'term> std::fmt::Debug for TermDisplay<'term> }; write!(format, "{:?} {} {:?}", - display_term(&binary_operation.left, Some(self.term), ChildPosition::Left), + display_term(&binary_operation.left, Some(self.term), TermChildPosition::Left), operator_string, - display_term(&binary_operation.right, Some(self.term), ChildPosition::Right)) + display_term(&binary_operation.right, Some(self.term), TermChildPosition::Right)) }, crate::Term::UnaryOperation( crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument}) => write!(format, "-{:?}", - display_term(argument, Some(self.term), ChildPosition::Any)), + display_term(argument, Some(self.term), TermChildPosition::Any)), crate::Term::UnaryOperation( crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument}) => write!(format, "|{:?}|", - display_term(argument, Some(self.term), ChildPosition::Any)), + display_term(argument, Some(self.term), TermChildPosition::Any)), }?; if requires_parentheses @@ -256,7 +256,7 @@ impl std::fmt::Debug for crate::Term { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(format, "{:?}", display_term(&self, None, ChildPosition::Any)) + write!(format, "{:?}", display_term(&self, None, TermChildPosition::Any)) } } @@ -264,7 +264,7 @@ impl std::fmt::Display for crate::Term { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(format, "{}", display_term(&self, None, ChildPosition::Any)) + write!(format, "{}", display_term(&self, None, TermChildPosition::Any)) } }