From 46b81dd3fc3581a77c8a2d4ec13ed51845ccf266 Mon Sep 17 00:00:00 2001
From: Tobias Stolzmann <tobias.stolzmann@gmail.com>
Date: Fri, 1 Dec 2023 14:19:23 +0100
Subject: [PATCH] Apply Apply to simplify ;-)

---
 src/simplifying/fol/ht.rs | 35 +++++------------------------------
 1 file changed, 5 insertions(+), 30 deletions(-)

diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs
index 2f48be4d..abd1e9f8 100644
--- a/src/simplifying/fol/ht.rs
+++ b/src/simplifying/fol/ht.rs
@@ -1,38 +1,13 @@
 use crate::{
-    convenience::unbox::{fol::UnboxedFormula, Unbox as _},
+    convenience::{
+        apply::Apply as _,
+        unbox::{fol::UnboxedFormula, Unbox as _},
+    },
     syntax_tree::fol::{AtomicFormula, BinaryConnective, Formula},
 };
 
 pub fn simplify(formula: Formula) -> Formula {
-    simplify_outer(match formula {
-        x @ Formula::AtomicFormula(_) => x,
-
-        Formula::UnaryFormula {
-            connective,
-            formula,
-        } => Formula::UnaryFormula {
-            connective,
-            formula: Box::new(simplify(*formula)),
-        },
-
-        Formula::BinaryFormula {
-            connective,
-            lhs,
-            rhs,
-        } => Formula::BinaryFormula {
-            connective,
-            lhs: Box::new(simplify(*lhs)),
-            rhs: Box::new(simplify(*rhs)),
-        },
-
-        Formula::QuantifiedFormula {
-            quantification,
-            formula,
-        } => Formula::QuantifiedFormula {
-            quantification,
-            formula: Box::new(simplify(*formula)),
-        },
-    })
+    formula.apply(&mut simplify_outer)
 }
 
 pub fn simplify_outer(formula: Formula) -> Formula {