Merge branch 'master' into tobias/default_format_and_parser

potassco · Sep 15, 2023 · b5f8830 · b5f8830
2 parents 1c0c072 + df03a0c
commit b5f8830
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 7 deletions.
diff --git a/src/formatting/fol/default.rs b/src/formatting/fol/default.rs
@@ -267,6 +267,18 @@ impl Precedence for Format<'_, Formula> {
         }
     }
 
+    fn mandatory_parentheses(&self) -> bool {
+        matches!(
+            self.0,
+            Formula::BinaryFormula {
+                connective: BinaryConnective::Equivalence
+                    | BinaryConnective::Implication
+                    | BinaryConnective::ReverseImplication,
+                ..
+            }
+        )
+    }
+
     fn fmt_operator(&self, f: &mut Formatter<'_>) -> fmt::Result {
         match self.0 {
             Formula::UnaryFormula { connective, .. } => write!(f, "{} ", Format(connective)),
@@ -515,7 +527,7 @@ mod tests {
                 .into(),
             })
             .to_string(),
-            "p <- q <- r"
+            "(p <- q) <- r"
         );
 
         assert_eq!(
@@ -596,7 +608,7 @@ mod tests {
                 .into()
             })
             .to_string(),
-            "p -> q -> r"
+            "p -> (q -> r)"
         );
 
         assert_eq!(
@@ -650,7 +662,7 @@ mod tests {
                 .into()
             })
             .to_string(),
-            "p -> q <- r"
+            "p -> (q <- r)"
         );
 
         assert_eq!(
@@ -677,7 +689,7 @@ mod tests {
                 .into(),
             })
             .to_string(),
-            "p <- q -> r"
+            "(p <- q) -> r"
         );
 
         assert_eq!(

diff --git a/src/formatting/mod.rs b/src/formatting/mod.rs
@@ -14,14 +14,18 @@ pub trait Precedence: Display {
 
     fn associativity(&self) -> Associativity;
 
+    fn mandatory_parentheses(&self) -> bool {
+        false
+    }
+
     fn fmt_operator(&self, f: &mut Formatter<'_>) -> fmt::Result;
 
     fn fmt_unary(&self, inner: impl Precedence, f: &mut Formatter<'_>) -> fmt::Result {
         if self.associativity() == Associativity::Left {
             self.fmt_operator(f)?;
         }
 
-        if self.precedence() < inner.precedence() {
+        if inner.mandatory_parentheses() || self.precedence() < inner.precedence() {
             write!(f, "({inner})")?;
         } else {
             write!(f, "{inner}")?;
@@ -40,7 +44,8 @@ pub trait Precedence: Display {
         rhs: impl Precedence,
         f: &mut Formatter<'_>,
     ) -> fmt::Result {
-        if self.precedence() < lhs.precedence()
+        if lhs.mandatory_parentheses()
+            || self.precedence() < lhs.precedence()
             || self.precedence() == lhs.precedence() && lhs.associativity() == Associativity::Right
         {
             write!(f, "({lhs})")?;
@@ -50,7 +55,8 @@ pub trait Precedence: Display {
 
         self.fmt_operator(f)?;
 
-        if self.precedence() < rhs.precedence()
+        if rhs.mandatory_parentheses()
+            || self.precedence() < rhs.precedence()
             || self.precedence() == rhs.precedence() && self.associativity() == Associativity::Left
         {
             write!(f, "({rhs})")