From d3e525e99e3590372229318bd85038bc7c3932b1 Mon Sep 17 00:00:00 2001
From: Tobias Stolzmann <tobias.stolzmann@gmail.com>
Date: Sat, 3 Feb 2024 14:44:20 +0100
Subject: [PATCH] Integrate the gamma translation into the command-line
 interface

---
 src/command_line/mod.rs  |  1 +
 src/main.rs              | 13 ++++++++++++-
 src/translating/gamma.rs | 27 ++++++++++++++++++---------
 3 files changed, 31 insertions(+), 10 deletions(-)

diff --git a/src/command_line/mod.rs b/src/command_line/mod.rs
index 939cb9de..2fd3f520 100644
--- a/src/command_line/mod.rs
+++ b/src/command_line/mod.rs
@@ -25,6 +25,7 @@ pub enum Command {
 
 #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, ValueEnum)]
 pub enum Translation {
+    Gamma,
     TauStar,
 }
 
diff --git a/src/main.rs b/src/main.rs
index 4b6ecae4..47b3144f 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -9,12 +9,13 @@ pub mod translating;
 use {
     crate::{
         command_line::{Arguments, Command, Translation},
-        syntax_tree::asp,
+        syntax_tree::{asp, fol},
         translating::tau_star::tau_star,
     },
     anyhow::{Context, Result},
     clap::Parser as _,
     std::fs::read_to_string,
+    translating::gamma::gamma,
 };
 
 fn main() -> Result<()> {
@@ -24,6 +25,16 @@ fn main() -> Result<()> {
                 .with_context(|| format!("could not read file `{}`", input.display()))?;
 
             match with {
+                Translation::Gamma => {
+                    let theory: fol::Theory = content
+                        .parse()
+                        .with_context(|| format!("could not parse file `{}`", input.display()))?;
+
+                    let theory = gamma(theory);
+
+                    println!("{theory}")
+                }
+
                 Translation::TauStar => {
                     let program: asp::Program = content
                         .parse()
diff --git a/src/translating/gamma.rs b/src/translating/gamma.rs
index a958c2dc..811045d7 100644
--- a/src/translating/gamma.rs
+++ b/src/translating/gamma.rs
@@ -1,9 +1,18 @@
 use crate::{
     convenience::apply::Apply as _,
-    syntax_tree::fol::{AtomicFormula, BinaryConnective, Formula, UnaryConnective},
+    syntax_tree::fol::{AtomicFormula, BinaryConnective, Formula, Theory, UnaryConnective},
 };
 
-pub fn gamma(formula: Formula) -> Formula {
+pub fn gamma(theory: Theory) -> Theory {
+    let mut formulas = Vec::new();
+    for formula in theory.formulas {
+        formulas.push(gamma_formula(formula));
+    }
+
+    Theory { formulas }
+}
+
+pub fn gamma_formula(formula: Formula) -> Formula {
     match formula {
         x @ Formula::AtomicFormula(_) => here(x),
 
@@ -22,8 +31,8 @@ pub fn gamma(formula: Formula) -> Formula {
             rhs,
         } => Formula::BinaryFormula {
             connective,
-            lhs: gamma(*lhs).into(),
-            rhs: gamma(*rhs).into(),
+            lhs: gamma_formula(*lhs).into(),
+            rhs: gamma_formula(*rhs).into(),
         },
 
         Formula::BinaryFormula {
@@ -37,8 +46,8 @@ pub fn gamma(formula: Formula) -> Formula {
             connective: BinaryConnective::Conjunction,
             lhs: Formula::BinaryFormula {
                 connective: connective.clone(),
-                lhs: gamma(*lhs.clone()).into(),
-                rhs: gamma(*rhs.clone()).into(),
+                lhs: gamma_formula(*lhs.clone()).into(),
+                rhs: gamma_formula(*rhs.clone()).into(),
             }
             .into(),
             rhs: Formula::BinaryFormula {
@@ -54,7 +63,7 @@ pub fn gamma(formula: Formula) -> Formula {
             formula,
         } => Formula::QuantifiedFormula {
             quantification,
-            formula: gamma(*formula).into(),
+            formula: gamma_formula(*formula).into(),
         },
     }
 }
@@ -79,7 +88,7 @@ fn prepend_predicate(formula: Formula, prefix: &'static str) -> Formula {
 
 #[cfg(test)]
 mod tests {
-    use super::gamma;
+    use super::gamma_formula;
 
     #[test]
     fn test_simplify() {
@@ -98,7 +107,7 @@ mod tests {
             ("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())
+            assert_eq!(gamma_formula(src.parse().unwrap()), target.parse().unwrap())
         }
     }
 }