Merge branch 'master' into jan/translate_format

potassco · Nov 21, 2024 · 2ff66f4 · 2ff66f4
2 parents 02148e2 + 24b2f32
commit 2ff66f4
Show file tree

Hide file tree

Showing 3 changed files with 54 additions and 36 deletions.
diff --git a/res/manual/src/contributors.md b/res/manual/src/contributors.md
@@ -10,3 +10,4 @@ We would like to thank the past and current contributors of the Anthem project!
 * Patrick Luhne
 * Torsten Schaub
 * Tobias Stolzmann
+* Nathan Temple
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(())

diff --git a/src/syntax_tree/fol.rs b/src/syntax_tree/fol.rs
@@ -377,6 +377,36 @@ pub struct Comparison {
 impl_node!(Comparison, Format, ComparisonParser);
 
 impl Comparison {
+    pub fn individuals(&self) -> impl Iterator<Item = (&GeneralTerm, &Relation, &GeneralTerm)> {
+        struct Individuals<'a> {
+            lhs: &'a GeneralTerm,
+            guards_iter: std::slice::Iter<'a, Guard>,
+        }
+
+        impl<'a> Iterator for Individuals<'a> {
+            type Item = (&'a GeneralTerm, &'a Relation, &'a GeneralTerm);
+
+            fn next(&mut self) -> Option<Self::Item> {
+                if let Some(Guard {
+                    relation,
+                    term: rhs,
+                }) = self.guards_iter.next()
+                {
+                    let result = Some((self.lhs, relation, rhs));
+                    self.lhs = rhs;
+                    result
+                } else {
+                    None
+                }
+            }
+        }
+
+        Individuals {
+            lhs: &self.term,
+            guards_iter: self.guards.iter(),
+        }
+    }
+
     pub fn substitute(self, var: Variable, term: GeneralTerm) -> Self {
         let lhs = self.term.substitute(var.clone(), term.clone());