Split Apply in twain to enable portfolios of simplifications

src/convenience/apply/mod.rs

@@ -5,23 +5,6 @@ pub trait Apply {
     fn apply(self, f: &mut impl FnMut(Self) -> Self) -> Self
     where
         Self: Sized;
-
-    /// Apply a series of operations `fs` in post-order to each node of a tree
-    ///
-    /// This function will traverse the tree only once. Whenever a node is visited, the first operation is applied first.
-    /// The remaining operations are also applied in this order.
-    fn apply_all(self, fs: &mut Vec<Box<dyn FnMut(Self) -> Self>>) -> Self
-    where
-        Self: Sized,
-    {
-        let mut f = |mut node: Self| {
-            for fi in fs.iter_mut() {
-                node = fi(node);
-            }
-            node
-        };
-        self.apply(&mut f)
-    }
 }
 
 impl Apply for Formula {

src/convenience/compose/mod.rs

@@ -0,0 +1,23 @@
+pub trait Compose<X> {
+    fn compose(self) -> impl Fn(X) -> X;
+}
+
+impl<T: Iterator + Clone + 'static, X> Compose<X> for T
+where
+    <T as Iterator>::Item: Fn(X) -> X,
+{
+    /// Composes a series of operations `f0, f1, ..., fn` into single operation `f`.
+    ///
+    /// The operations are applied left-to-right, i.e. `f(x) = fn( .. f1( f0(x) ) .. )`.
+    fn compose(self) -> impl Fn(X) -> X {
+        // CAUTION: Cloning is absolutely crucial here.
+        // self is an Iterator that is moved into the closure and therefore
+        // returned from the function. It is used whenever the closure is
+        // called. If we do not clone the iterator, it will be empty after
+        // the first call which changes the intended behavior. Besides,
+        // cloning an Iterator is cheap since it is merely a view into the
+        // underlying data structure. The data structure itself is not
+        // cloned.
+        move |x| self.clone().fold(x, |x, f| f(x))
+    }
+}

src/convenience/mod.rs

@@ -1,3 +1,4 @@
 pub mod apply;
+pub mod compose;
 pub mod unbox;
 pub mod with_warnings;

src/simplifying/fol/classic.rs

@@ -1,13 +1,25 @@
 use crate::{
-    convenience::unbox::{fol::UnboxedFormula, Unbox as _},
+    convenience::{
+        apply::Apply as _,
+        compose::Compose as _,
+        unbox::{fol::UnboxedFormula, Unbox as _},
+    },
+    simplifying::fol::{ht::HT, intuitionistic::INTUITIONISTIC},
     syntax_tree::fol::{Formula, Theory, UnaryConnective},
 };
 
 pub fn simplify(theory: Theory) -> Theory {
-    crate::simplifying::fol::ht::simplify(theory)
-    // TODO: Apply classic simplifications
+    Theory {
+        formulas: theory.formulas.into_iter().map(simplify_formula).collect(),
+    }
+}
+
+pub fn simplify_formula(formula: Formula) -> Formula {
+    formula.apply(&mut INTUITIONISTIC.iter().chain(HT).chain(CLASSIC).compose())
 }
 
+pub const CLASSIC: &[fn(Formula) -> Formula] = &[remove_double_negation];
+
 pub fn remove_double_negation(formula: Formula) -> Formula {
     // Remove double negation
     // e.g. not not F => F

src/simplifying/fol/ht.rs

@@ -1,6 +1,17 @@
-use crate::syntax_tree::fol::Theory;
+use crate::{
+    convenience::{apply::Apply as _, compose::Compose as _},
+    simplifying::fol::intuitionistic::INTUITIONISTIC,
+    syntax_tree::fol::{Formula, Theory},
+};
 
 pub fn simplify(theory: Theory) -> Theory {
-    crate::simplifying::fol::intuitionistic::simplify(theory)
-    // TODO: Add ht simplifications
+    Theory {
+        formulas: theory.formulas.into_iter().map(simplify_formula).collect(),
+    }
 }
+
+pub fn simplify_formula(formula: Formula) -> Formula {
+    formula.apply(&mut INTUITIONISTIC.iter().chain(HT).compose())
+}
+
+pub const HT: &[fn(Formula) -> Formula] = &[];

src/simplifying/fol/intuitionistic.rs

@@ -1,6 +1,7 @@
 use crate::{
     convenience::{
         apply::Apply as _,
+        compose::Compose as _,
         unbox::{fol::UnboxedFormula, Unbox as _},
     },
     syntax_tree::fol::{
@@ -16,20 +17,22 @@ pub fn simplify(theory: Theory) -> Theory {
 }
 
 pub fn simplify_formula(formula: Formula) -> Formula {
-    formula.apply_all(&mut vec![
-        Box::new(evaluate_comparisons),
-        Box::new(apply_negation_definition),
-        Box::new(apply_reverse_implication_definition),
-        Box::new(apply_equivalence_definition),
-        Box::new(remove_identities),
-        Box::new(remove_annihilations),
-        Box::new(remove_idempotences),
-        Box::new(remove_orphaned_variables),
-        Box::new(remove_empty_quantifications),
-        Box::new(join_nested_quantifiers),
-    ])
+    formula.apply(&mut INTUITIONISTIC.iter().compose())
 }
 
+pub const INTUITIONISTIC: &[fn(Formula) -> Formula] = &[
+    evaluate_comparisons,
+    apply_negation_definition,
+    apply_reverse_implication_definition,
+    apply_equivalence_definition,
+    remove_identities,
+    remove_annihilations,
+    remove_idempotences,
+    remove_orphaned_variables,
+    remove_empty_quantifications,
+    join_nested_quantifiers,
+];
+
 pub fn evaluate_comparisons(formula: Formula) -> Formula {
     // Evaluate comparisons between structurally equal terms
     // e.g. T  = T => #true