From 79258acdda7853b4c7b0f0474eab6a9e53201e71 Mon Sep 17 00:00:00 2001
From: ZachJHansen <zachhansen@unomaha.edu>
Date: Tue, 10 Dec 2024 11:11:26 -0600
Subject: [PATCH] adding double negation elim to classical simplifications

---
 src/simplifying/fol/classic.rs | 68 +++++++++++++++++++++++++++++++++-
 1 file changed, 66 insertions(+), 2 deletions(-)

diff --git a/src/simplifying/fol/classic.rs b/src/simplifying/fol/classic.rs
index 51bd44c9..b6f1d733 100644
--- a/src/simplifying/fol/classic.rs
+++ b/src/simplifying/fol/classic.rs
@@ -1,6 +1,70 @@
-use crate::syntax_tree::fol::Theory;
+use crate::{
+    convenience::{
+        apply::Apply as _,
+        unbox::{fol::UnboxedFormula, Unbox},
+    },
+    syntax_tree::fol::{Formula, Theory, UnaryConnective},
+};
 
 pub fn simplify(theory: Theory) -> Theory {
-    crate::simplifying::fol::ht::simplify(theory)
+    simplify_classic(crate::simplifying::fol::ht::simplify(theory))
     // TODO: Add classic simplifications
 }
+
+pub fn simplify_classic(theory: Theory) -> Theory {
+    Theory {
+        formulas: theory.formulas.into_iter().map(simplify_formula).collect(),
+    }
+}
+
+fn simplify_formula(formula: Formula) -> Formula {
+    formula.apply_all(&mut vec![Box::new(eliminate_double_negation)])
+}
+
+fn eliminate_double_negation(formula: Formula) -> Formula {
+    // Remove double negation
+    // e.g. not not F => F
+
+    match formula.unbox() {
+        UnboxedFormula::UnaryFormula {
+            connective: UnaryConnective::Negation,
+            formula:
+                Formula::UnaryFormula {
+                    connective: UnaryConnective::Negation,
+                    formula: inner,
+                },
+        } => *inner,
+
+        x => x.rebox(),
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use {
+        super::{eliminate_double_negation, simplify_formula},
+        crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula},
+    };
+
+    #[test]
+    fn test_simplify() {
+        for (src, target) in [("not not forall X p(X)", "forall X p(X)")] {
+            assert_eq!(
+                simplify_formula(src.parse().unwrap()),
+                target.parse().unwrap()
+            )
+        }
+    }
+
+    #[test]
+    fn test_eliminate_double_negation() {
+        for (src, target) in [("not not a", "a")] {
+            assert_eq!(
+                src.parse::<Formula>()
+                    .unwrap()
+                    .apply(&mut eliminate_double_negation),
+                target.parse().unwrap()
+            )
+        }
+    }
+}