From cafec44616ed2bc470f4ce1e9dfe89a2b26a2d7b Mon Sep 17 00:00:00 2001
From: Tobias Stolzmann <tobias.stolzmann@gmail.com>
Date: Thu, 7 Dec 2023 14:44:34 +0100
Subject: [PATCH] Add tests for the gamma translation

---
 src/translating/gamma.rs | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/src/translating/gamma.rs b/src/translating/gamma.rs
index dbcae012..ed08bd17 100644
--- a/src/translating/gamma.rs
+++ b/src/translating/gamma.rs
@@ -54,6 +54,7 @@ pub fn gamma(formula: Formula) -> Formula {
             formula: gamma(*formula).into(),
         },
 
+        // TODO: Support reverse implication and equivalence
         _ => todo!(),
     }
 }
@@ -75,3 +76,25 @@ fn prepend_predicate(formula: Formula, prefix: &'static str) -> Formula {
         x => x,
     })
 }
+
+#[cfg(test)]
+mod tests {
+    use super::gamma;
+
+    #[test]
+    fn test_simplify() {
+        for (src, target) in [
+            ("#true", "#true"),
+            ("a", "ha"),
+            ("X > 1", "X > 1"), // TODO: Is this correct?
+            ("not a", "not ta"),
+            ("a and not b", "ha and not tb"),
+            ("a or not b", "ha or not tb"),
+            ("a -> b", "(ha -> hb) and (ta -> tb)"),
+            ("forall X p(X)", "forall X hp(X)"),
+            ("exists X p(X)", "exists X hp(X)"),
+        ] {
+            assert_eq!(gamma(src.parse().unwrap()), target.parse().unwrap())
+        }
+    }
+}