diff --git a/examples/test.rs b/examples/test.rs index 7497522..fd59431 100644 --- a/examples/test.rs +++ b/examples/test.rs @@ -1,5 +1,3 @@ -use foliage::format; - fn main() -> Result<(), Box> { let formulas = "forall XV1 (p(XV1) <-> (exists XU1 (exists X1, X2 (X1 = XU1 and exists N1, N2, N3 (N1 = 0 and N2 = n and N1 <= N3 and N3 <= N2 and X2 = N3) and X1 = X2) and exists X3, X4 (exists N4, N5 (X3 = (N4 * N5) and N4 = XU1 and N5 = XU1) and X4 = n and X3 <= X4) and XV1 = XU1))) @@ -13,5 +11,16 @@ forall XV2 (q(XV2) <-> (exists XU2 (exists X5 (X5 = XU2 and p(X5)) and exists X6 println!("{}", formula); } + let formulas = "forall XV1 (p(XV1) <-> exists XU1 (exists X1, X2 (X1 = XU1 and exists N1, N2, N3 (N1 = 0 and N2 = n and N1 <= N3 and N3 <= N2 and X2 = N3) and X1 = X2) and exists X3, X4 (exists N4, N5 (X3 = N4 * N5 and N4 = XU1 and N5 = XU1) and X4 = n and X3 <= X4) and XV1 = XU1)) +forall XV2 (q(XV2) <-> exists XU2 (exists X5 (X5 = XU2 and p(X5)) and exists X6 (exists N6, N7 (X6 = N6 + N7 and N6 = XU2 and N7 = 1) and not p(X6)) and XV2 = XU2))"; + + let (i, formulas) = foliage::formulas(formulas).unwrap(); + assert_eq!(i, ""); + + for formula in formulas + { + println!("{}", formula); + } + Ok(()) } diff --git a/src/format.rs b/src/format.rs index bf6170b..69addcc 100644 --- a/src/format.rs +++ b/src/format.rs @@ -1,3 +1,34 @@ +struct TermDisplay<'term> +{ + parent_precedence: u64, + term: &'term crate::Term, +} + +struct FormulaDisplay<'formula> +{ + parent_precedence: u64, + formula: &'formula crate::Formula, +} + +fn display_term<'term>(term: &'term crate::Term, parent_precedence: u64) -> TermDisplay<'term> +{ + TermDisplay + { + parent_precedence, + term, + } +} + +fn display_formula<'formula>(formula: &'formula crate::Formula, parent_precedence: u64) + -> FormulaDisplay<'formula> +{ + FormulaDisplay + { + parent_precedence, + formula, + } +} + fn term_precedence(term: &crate::Term) -> u64 { match term @@ -51,11 +82,19 @@ impl std::fmt::Display for crate::VariableDeclaration } } -impl std::fmt::Debug for crate::Term +impl<'term> std::fmt::Debug for TermDisplay<'term> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - match *self + let precedence = term_precedence(self.term); + let requires_parentheses = precedence > self.parent_precedence; + + if requires_parentheses + { + write!(format, "(")?; + } + + match self.term { crate::Term::Infimum => write!(format, "#inf"), crate::Term::Supremum => write!(format, "#sup"), @@ -63,31 +102,146 @@ impl std::fmt::Debug for crate::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, "({:?} + {:?})", left, right), - crate::Term::Subtract(ref left, ref right) => write!(format, "({:?} - {:?})", left, right), - crate::Term::Multiply(ref left, ref right) => write!(format, "({:?} * {:?})", left, right), - crate::Term::Negative(ref argument) => write!(format, "-({:?})", argument), + 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)), + }?; + + if requires_parentheses + { + write!(format, ")")?; } + + Ok(()) } } -impl std::fmt::Display for crate::Term +impl<'term> std::fmt::Display for TermDisplay<'term> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - match *self + write!(format, "{:?}", self) + } +} + +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; + + if requires_parentheses { - crate::Term::Infimum => write!(format, "#inf"), - crate::Term::Supremum => write!(format, "#sup"), - crate::Term::Integer(value) => write!(format, "{}", value), - 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, "({} + {})", left, right), - crate::Term::Subtract(ref left, ref right) => write!(format, "({} - {})", left, right), - crate::Term::Multiply(ref left, ref right) => write!(format, "({} * {})", left, right), - crate::Term::Negative(ref argument) => write!(format, "-({})", argument), + write!(format, "(")?; } + + match self.formula + { + crate::Formula::Exists(ref exists) => + { + write!(format, "exists")?; + + let mut separator = " "; + + for parameter in &exists.parameters + { + write!(format, "{}{:?}", separator, parameter)?; + + separator = ", " + } + + write!(format, " {:?}", display_formula(&exists.argument, precedence))?; + }, + crate::Formula::ForAll(ref for_all) => + { + write!(format, "forall")?; + + let mut separator = " "; + + for parameter in &for_all.parameters + { + write!(format, "{}{:?}", separator, parameter)?; + + separator = ", " + } + + write!(format, " {:?}", display_formula(&for_all.argument, precedence))?; + }, + crate::Formula::Not(ref argument) => write!(format, "not {:?}", display_formula(argument, precedence))?, + crate::Formula::And(ref arguments) => + { + let mut separator = ""; + + for argument in arguments + { + write!(format, "{}{:?}", separator, display_formula(argument, precedence))?; + + separator = " and " + } + }, + crate::Formula::Or(ref arguments) => + { + let mut separator = ""; + + for argument in arguments + { + write!(format, "{}{:?}", separator, display_formula(argument, precedence))?; + + 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::Boolean(value) => + match value + { + true => write!(format, "#true")?, + false => write!(format, "#false")?, + }, + crate::Formula::Predicate(ref predicate) => + { + write!(format, "{}", predicate.declaration.name)?; + + if !predicate.arguments.is_empty() + { + write!(format, "(")?; + + let mut separator = ""; + + for argument in &predicate.arguments + { + write!(format, "{}{:?}", separator, display_term(argument, 1000))?; + + separator = ", " + } + + write!(format, ")")?; + } + }, + } + + if requires_parentheses + { + write!(format, ")")?; + } + + Ok(()) + } +} + +impl<'formula> std::fmt::Display for FormulaDisplay<'formula> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(format, "{:?}", self) } } @@ -95,106 +249,7 @@ impl std::fmt::Debug for crate::Formula { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - match *self - { - crate::Formula::Exists(ref exists) => - { - write!(format, "exists")?; - - let mut separator = " "; - - for parameter in &exists.parameters - { - write!(format, "{}{:?}", separator, parameter)?; - - separator = ", " - } - - write!(format, " ({:?})", exists.argument) - }, - crate::Formula::ForAll(ref for_all) => - { - write!(format, "forall")?; - - let mut separator = " "; - - for parameter in &for_all.parameters - { - write!(format, "{}{:?}", separator, parameter)?; - - separator = ", " - } - - write!(format, " ({:?})", for_all.argument) - }, - crate::Formula::Not(ref argument) => write!(format, "not {:?}", argument), - crate::Formula::And(ref arguments) => - { - write!(format, "(")?; - - let mut separator = ""; - - for argument in arguments - { - write!(format, "{}{:?}", separator, argument)?; - - separator = " and " - } - - write!(format, ")") - }, - crate::Formula::Or(ref arguments) => - { - write!(format, "(")?; - - let mut separator = ""; - - for argument in arguments - { - write!(format, "{}{:?}", separator, argument)?; - - separator = " or " - } - - write!(format, ")") - }, - crate::Formula::Implies(ref left, ref right) => write!(format, "({:?} -> {:?})", left, right), - crate::Formula::Biconditional(ref left, ref right) => write!(format, "({:?} <-> {:?})", left, right), - crate::Formula::Less(ref left, ref right) => write!(format, "({:?} < {:?})", left, right), - crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "({:?} <= {:?})", left, right), - crate::Formula::Greater(ref left, ref right) => write!(format, "({:?} > {:?})", left, right), - crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "({:?} >= {:?})", left, right), - crate::Formula::Equal(ref left, ref right) => write!(format, "({:?} = {:?})", left, right), - crate::Formula::NotEqual(ref left, ref right) => write!(format, "({:?} != {:?})", left, right), - crate::Formula::Boolean(value) => - match value - { - true => write!(format, "#true"), - false => write!(format, "#false"), - }, - crate::Formula::Predicate(ref predicate) => - { - write!(format, "{}", predicate.declaration.name)?; - - if !predicate.arguments.is_empty() - { - write!(format, "(")?; - - let mut separator = ""; - - for argument in &predicate.arguments - { - write!(format, "{}{:?}", separator, argument)?; - - separator = ", " - } - - write!(format, ")")?; - } - - Ok(()) - }, - } + write!(format, "{:?}", display_formula(&self, 1000)) } } @@ -202,105 +257,22 @@ impl std::fmt::Display for crate::Formula { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - match *self - { - crate::Formula::Exists(ref exists) => - { - write!(format, "exists")?; - - let mut separator = " "; - - for parameter in &exists.parameters - { - write!(format, "{}{}", separator, parameter)?; - - separator = ", " - } - - write!(format, " ({})", exists.argument) - }, - crate::Formula::ForAll(ref for_all) => - { - write!(format, "forall")?; - - let mut separator = " "; - - for parameter in &for_all.parameters - { - write!(format, "{}{}", separator, parameter)?; - - separator = ", " - } - - write!(format, " ({})", for_all.argument) - }, - crate::Formula::Not(ref argument) => write!(format, "not {}", argument), - crate::Formula::And(ref arguments) => - { - write!(format, "(")?; - - let mut separator = ""; - - for argument in arguments - { - write!(format, "{}{}", separator, argument)?; - - separator = " and " - } - - write!(format, ")") - }, - crate::Formula::Or(ref arguments) => - { - write!(format, "(")?; - - let mut separator = ""; - - for argument in arguments - { - write!(format, "{}{}", separator, argument)?; - - separator = " or " - } - - write!(format, ")") - }, - crate::Formula::Implies(ref left, ref right) => write!(format, "({} -> {})", left, right), - crate::Formula::Biconditional(ref left, ref right) => write!(format, "({} <-> {})", left, right), - crate::Formula::Less(ref left, ref right) => write!(format, "({} < {})", left, right), - crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "({} <= {})", left, right), - crate::Formula::Greater(ref left, ref right) => write!(format, "({} > {})", left, right), - crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "({} >= {})", left, right), - crate::Formula::Equal(ref left, ref right) => write!(format, "({} = {})", left, right), - crate::Formula::NotEqual(ref left, ref right) => write!(format, "({} != {})", left, right), - crate::Formula::Boolean(value) => - match value - { - true => write!(format, "#true"), - false => write!(format, "#false"), - }, - crate::Formula::Predicate(ref predicate) => - { - write!(format, "{}", predicate.declaration.name)?; - - if !predicate.arguments.is_empty() - { - write!(format, "(")?; - - let mut separator = ""; - - for argument in &predicate.arguments - { - write!(format, "{}{}", separator, argument)?; - - separator = ", " - } - - write!(format, ")")?; - } - - Ok(()) - }, - } + write!(format, "{}", display_formula(&self, 1000)) + } +} + +impl std::fmt::Debug for crate::Term +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(format, "{:?}", display_term(&self, 1000)) + } +} + +impl std::fmt::Display for crate::Term +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(format, "{}", display_term(&self, 1000)) } }