diff --git a/src/format.rs b/src/format.rs index e517a7f..9a281c1 100644 --- a/src/format.rs +++ b/src/format.rs @@ -1,30 +1,30 @@ -struct TermDisplay<'term> +struct TermDisplay<'parent> { - parent_precedence: u64, - term: &'term crate::Term, + parent: Option<&'parent crate::Term>, + term: &'parent crate::Term, } -struct FormulaDisplay<'formula> +struct FormulaDisplay<'parent> { - parent_precedence: u64, - formula: &'formula crate::Formula, + parent: Option<&'parent crate::Formula>, + formula: &'parent crate::Formula, } -fn display_term<'term>(term: &'term crate::Term, parent_precedence: u64) -> TermDisplay<'term> +fn display_term<'parent>(term: &'parent crate::Term, parent: Option<&'parent crate::Term>) -> TermDisplay<'parent> { TermDisplay { - parent_precedence, + parent, term, } } -fn display_formula<'formula>(formula: &'formula crate::Formula, parent_precedence: u64) - -> FormulaDisplay<'formula> +fn display_formula<'parent>(formula: &'parent crate::Formula, parent: Option<&'parent crate::Formula>) + -> FormulaDisplay<'parent> { FormulaDisplay { - parent_precedence, + parent, formula, } } @@ -40,6 +40,32 @@ fn term_precedence(term: &crate::Term) -> u64 } } +fn term_requires_parentheses(child: &crate::Term, parent: Option<&crate::Term>) -> bool +{ + match parent + { + None => false, + Some(parent) => + { + let child_precedence = term_precedence(child); + let parent_precedence = term_precedence(parent); + + if child_precedence != parent_precedence + { + return child_precedence > parent_precedence; + } + + // Subtraction isn’t associative, so handle them separately + // TODO: only do this for right-hand side of subtractions + match parent + { + crate::Term::Subtract(_, _) => true, + _ => false, + } + }, + } +} + fn formula_precedence(formula: &crate::Formula) -> u64 { match formula @@ -54,6 +80,31 @@ fn formula_precedence(formula: &crate::Formula) -> u64 } } +fn formula_requires_parentheses(child: &crate::Formula, parent: Option<&crate::Formula>) -> bool +{ + match parent + { + None => false, + Some(parent) => + { + let child_precedence = formula_precedence(child); + let parent_precedence = formula_precedence(parent); + + if child_precedence != parent_precedence + { + return child_precedence > parent_precedence; + } + + // Implications aren’t associative, so handle them separately + match parent + { + crate::Formula::Implies(_, _) => true, + _ => false, + } + }, + } +} + impl std::fmt::Debug for crate::VariableDeclaration { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result @@ -74,8 +125,7 @@ impl<'term> std::fmt::Debug for TermDisplay<'term> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - let precedence = term_precedence(self.term); - let requires_parentheses = precedence > self.parent_precedence; + let requires_parentheses = term_requires_parentheses(self.term, self.parent); if requires_parentheses { @@ -90,10 +140,10 @@ impl<'term> std::fmt::Debug for TermDisplay<'term> crate::Term::Symbolic(ref value) => write!(format, "{}", value), crate::Term::String(ref value) => write!(format, "\"{}\"", value), crate::Term::Variable(ref declaration) => write!(format, "{:?}", declaration), - crate::Term::Add(ref left, ref right) => write!(format, "{:?} + {:?}", display_term(left, precedence), display_term(right, precedence)), - crate::Term::Subtract(ref left, ref right) => write!(format, "{:?} - {:?}", display_term(left, precedence), display_term(right, precedence)), - crate::Term::Multiply(ref left, ref right) => write!(format, "{:?} * {:?}", display_term(left, precedence), display_term(right, precedence)), - crate::Term::Negative(ref argument) => write!(format, "-{:?}", display_term(argument, precedence)), + crate::Term::Add(ref left, ref right) => write!(format, "{:?} + {:?}", display_term(left, Some(self.term)), display_term(right, Some(self.term))), + crate::Term::Subtract(ref left, ref right) => write!(format, "{:?} - {:?}", display_term(left, Some(self.term)), display_term(right, Some(self.term))), + crate::Term::Multiply(ref left, ref right) => write!(format, "{:?} * {:?}", display_term(left, Some(self.term)), display_term(right, Some(self.term))), + crate::Term::Negative(ref argument) => write!(format, "-{:?}", display_term(argument, Some(self.term))), }?; if requires_parentheses @@ -117,8 +167,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - let precedence = formula_precedence(self.formula); - let requires_parentheses = precedence > self.parent_precedence; + let requires_parentheses = formula_requires_parentheses(self.formula, self.parent); if requires_parentheses { @@ -140,7 +189,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> separator = ", " } - write!(format, " {:?}", display_formula(&exists.argument, precedence))?; + write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula)))?; }, crate::Formula::ForAll(ref for_all) => { @@ -155,16 +204,16 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> separator = ", " } - write!(format, " {:?}", display_formula(&for_all.argument, precedence))?; + write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula)))?; }, - crate::Formula::Not(ref argument) => write!(format, "not {:?}", display_formula(argument, precedence))?, + crate::Formula::Not(ref argument) => write!(format, "not {:?}", display_formula(argument, Some(self.formula)))?, crate::Formula::And(ref arguments) => { let mut separator = ""; for argument in arguments { - write!(format, "{}{:?}", separator, display_formula(argument, precedence))?; + write!(format, "{}{:?}", separator, display_formula(argument, Some(self.formula)))?; separator = " and " } @@ -175,19 +224,19 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> for argument in arguments { - write!(format, "{}{:?}", separator, display_formula(argument, precedence))?; + write!(format, "{}{:?}", separator, display_formula(argument, Some(self.formula)))?; separator = " or " } }, - crate::Formula::Implies(ref left, ref right) => write!(format, "{:?} -> {:?}", display_formula(left, precedence), display_formula(right, precedence))?, - crate::Formula::Biconditional(ref left, ref right) => write!(format, "{:?} <-> {:?}", display_formula(left, precedence), display_formula(right, precedence))?, - crate::Formula::Less(ref left, ref right) => write!(format, "{:?} < {:?}", display_term(left, 1000), display_term(right, 1000))?, - crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "{:?} <= {:?}", display_term(left, 1000), display_term(right, 1000))?, - crate::Formula::Greater(ref left, ref right) => write!(format, "{:?} > {:?}", display_term(left, 1000), display_term(right, 1000))?, - crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "{:?} >= {:?}", display_term(left, 1000), display_term(right, 1000))?, - crate::Formula::Equal(ref left, ref right) => write!(format, "{:?} = {:?}", display_term(left, 1000), display_term(right, 1000))?, - crate::Formula::NotEqual(ref left, ref right) => write!(format, "{:?} != {:?}", display_term(left, 1000), display_term(right, 1000))?, + crate::Formula::Implies(ref left, ref right) => write!(format, "{:?} -> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?, + crate::Formula::Biconditional(ref left, ref right) => write!(format, "{:?} <-> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?, + crate::Formula::Less(ref left, ref right) => write!(format, "{:?} < {:?}", display_term(left, None), display_term(right, None))?, + crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "{:?} <= {:?}", display_term(left, None), display_term(right, None))?, + crate::Formula::Greater(ref left, ref right) => write!(format, "{:?} > {:?}", display_term(left, None), display_term(right, None))?, + crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "{:?} >= {:?}", display_term(left, None), display_term(right, None))?, + crate::Formula::Equal(ref left, ref right) => write!(format, "{:?} = {:?}", display_term(left, None), display_term(right, None))?, + crate::Formula::NotEqual(ref left, ref right) => write!(format, "{:?} != {:?}", display_term(left, None), display_term(right, None))?, crate::Formula::Boolean(value) => match value { @@ -206,7 +255,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> for argument in &predicate.arguments { - write!(format, "{}{:?}", separator, display_term(argument, 1000))?; + write!(format, "{}{:?}", separator, display_term(argument, None))?; separator = ", " } @@ -237,7 +286,7 @@ impl std::fmt::Debug for crate::Formula { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(format, "{:?}", display_formula(&self, 1000)) + write!(format, "{:?}", display_formula(&self, None)) } } @@ -245,7 +294,7 @@ impl std::fmt::Display for crate::Formula { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(format, "{}", display_formula(&self, 1000)) + write!(format, "{}", display_formula(&self, None)) } } @@ -253,7 +302,7 @@ impl std::fmt::Debug for crate::Term { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(format, "{:?}", display_term(&self, 1000)) + write!(format, "{:?}", display_term(&self, None)) } } @@ -261,6 +310,6 @@ impl std::fmt::Display for crate::Term { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(format, "{}", display_term(&self, 1000)) + write!(format, "{}", display_term(&self, None)) } }