Simplify the TPTP formatter for Comparisons as a proof of concept

potassco · Nov 21, 2024 · 24b2f32 · 24b2f32
1 parent a2c43eb
commit 24b2f32
Showing 1 changed file with 23 additions and 36 deletions.
diff --git a/src/formatting/fol/tptp.rs b/src/formatting/fol/tptp.rs
@@ -138,55 +138,42 @@ impl Display for Format<'_, Relation> {
 
 impl Display for Format<'_, Comparison> {
     fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
-        let guards = &self.0.guards;
-
-        let mut previous_term = &self.0.term;
-        for (counter, g) in guards.iter().enumerate() {
+        for (counter, (lhs, relation, rhs)) in self.0.individuals().enumerate() {
             if counter > 0 {
                 write!(f, " & ")?;
             }
 
-            match (previous_term, &g.term) {
-                (GeneralTerm::IntegerTerm(lhs), GeneralTerm::IntegerTerm(rhs)) => {
-                    match g.relation {
-                        Relation::Equal | Relation::NotEqual => write!(
-                            f,
-                            "{} {} {}",
-                            Format(lhs),
-                            Format(&g.relation).repr_integer(),
-                            Format(rhs)
-                        ),
-                        _ => write!(
-                            f,
-                            "{}({}, {})",
-                            Format(&g.relation).repr_integer(),
-                            Format(lhs),
-                            Format(rhs)
-                        ),
-                    }
-                }
+            match (lhs, rhs) {
+                (GeneralTerm::IntegerTerm(lhs), GeneralTerm::IntegerTerm(rhs)) => match relation {
+                    Relation::Equal | Relation::NotEqual => write!(
+                        f,
+                        "{} {} {}",
+                        Format(lhs),
+                        Format(relation).repr_integer(),
+                        Format(rhs)
+                    ),
+                    _ => write!(
+                        f,
+                        "{}({}, {})",
+                        Format(relation).repr_integer(),
+                        Format(lhs),
+                        Format(rhs)
+                    ),
+                },
 
                 (GeneralTerm::SymbolicTerm(lhs), GeneralTerm::SymbolicTerm(rhs))
-                    if matches!(g.relation, Relation::Equal | Relation::NotEqual) =>
+                    if matches!(relation, Relation::Equal | Relation::NotEqual) =>
                 {
-                    write!(f, "{} {} {}", Format(lhs), Format(&g.relation), Format(rhs))
+                    write!(f, "{} {} {}", Format(lhs), Format(relation), Format(rhs))
                 }
 
-                (lhs, rhs) => match g.relation {
+                (lhs, rhs) => match relation {
                     Relation::Equal | Relation::NotEqual => {
-                        write!(f, "{} {} {}", Format(lhs), Format(&g.relation), Format(rhs))
+                        write!(f, "{} {} {}", Format(lhs), Format(relation), Format(rhs))
                     }
-                    _ => write!(
-                        f,
-                        "{}({}, {})",
-                        Format(&g.relation),
-                        Format(lhs),
-                        Format(rhs)
-                    ),
+                    _ => write!(f, "{}({}, {})", Format(relation), Format(lhs), Format(rhs)),
                 },
             }?;
-
-            previous_term = &g.term;
         }
 
         Ok(())