From caed24a58792b1d943d8c31d0fd1db5d8a9a7e94 Mon Sep 17 00:00:00 2001
From: Tobias Stolzmann <tobias.stolzmann@gmail.com>
Date: Fri, 1 Dec 2023 15:11:48 +0100
Subject: [PATCH] Implement the gamma translation

---
 src/main.rs              |  1 +
 src/translating/gamma.rs | 77 ++++++++++++++++++++++++++++++++++++++++
 src/translating/mod.rs   |  1 +
 3 files changed, 79 insertions(+)
 create mode 100644 src/translating/gamma.rs
 create mode 100644 src/translating/mod.rs

diff --git a/src/main.rs b/src/main.rs
index 800eca80..17c9d418 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -3,6 +3,7 @@ pub mod formatting;
 pub mod parsing;
 pub mod simplifying;
 pub mod syntax_tree;
+pub mod translating;
 
 fn main() {
     // TODO
diff --git a/src/translating/gamma.rs b/src/translating/gamma.rs
new file mode 100644
index 00000000..dbcae012
--- /dev/null
+++ b/src/translating/gamma.rs
@@ -0,0 +1,77 @@
+use crate::{
+    convenience::apply::Apply as _,
+    syntax_tree::fol::{AtomicFormula, BinaryConnective, Formula, UnaryConnective},
+};
+
+pub fn gamma(formula: Formula) -> Formula {
+    match formula {
+        x @ Formula::AtomicFormula(_) => here(x),
+
+        Formula::UnaryFormula {
+            connective: connective @ UnaryConnective::Negation,
+            formula,
+        } => Formula::UnaryFormula {
+            connective,
+            formula: there(*formula).into(),
+        },
+
+        Formula::BinaryFormula {
+            connective:
+                connective @ BinaryConnective::Conjunction | connective @ BinaryConnective::Disjunction,
+            lhs,
+            rhs,
+        } => Formula::BinaryFormula {
+            connective,
+            lhs: gamma(*lhs).into(),
+            rhs: gamma(*rhs).into(),
+        },
+
+        Formula::BinaryFormula {
+            connective: BinaryConnective::Implication,
+            lhs,
+            rhs,
+        } => Formula::BinaryFormula {
+            connective: BinaryConnective::Conjunction,
+            lhs: Formula::BinaryFormula {
+                connective: BinaryConnective::Implication,
+                lhs: gamma(*lhs.clone()).into(),
+                rhs: gamma(*rhs.clone()).into(),
+            }
+            .into(),
+            rhs: Formula::BinaryFormula {
+                connective: BinaryConnective::Implication,
+                lhs: there(*lhs).into(),
+                rhs: there(*rhs).into(),
+            }
+            .into(),
+        },
+
+        Formula::QuantifiedFormula {
+            quantification,
+            formula,
+        } => Formula::QuantifiedFormula {
+            quantification,
+            formula: gamma(*formula).into(),
+        },
+
+        _ => todo!(),
+    }
+}
+
+fn here(formula: Formula) -> Formula {
+    prepend_predicate(formula, "h")
+}
+
+fn there(formula: Formula) -> Formula {
+    prepend_predicate(formula, "t")
+}
+
+fn prepend_predicate(formula: Formula, prefix: &'static str) -> Formula {
+    formula.apply(&mut |formula| match formula {
+        Formula::AtomicFormula(AtomicFormula::Atom(mut a)) => {
+            a.predicate.insert_str(0, prefix);
+            Formula::AtomicFormula(AtomicFormula::Atom(a))
+        }
+        x => x,
+    })
+}
diff --git a/src/translating/mod.rs b/src/translating/mod.rs
new file mode 100644
index 00000000..2cd64b3e
--- /dev/null
+++ b/src/translating/mod.rs
@@ -0,0 +1 @@
+pub mod gamma;