Add more, hopefully rather uncontroversial 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,6 +1,58 @@
-use crate::syntax_tree::fol::Theory;
+use crate::{
+    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: Add 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
+
+    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::remove_double_negation,
+        crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula},
+    };
+
+    #[test]
+    fn test_eliminate_double_negation() {
+        assert_eq!(
+            "not not a"
+                .parse::<Formula>()
+                .unwrap()
+                .apply(&mut remove_double_negation),
+            "a".parse().unwrap()
+        )
+    }
 }

src/simplifying/fol/ht.rs

@@ -1,9 +1,7 @@
 use crate::{
-    convenience::{
-        apply::Apply as _,
-        unbox::{fol::UnboxedFormula, Unbox as _},
-    },
-    syntax_tree::fol::{AtomicFormula, BinaryConnective, Formula, Theory},
+    convenience::{apply::Apply as _, compose::Compose as _},
+    simplifying::fol::intuitionistic::INTUITIONISTIC,
+    syntax_tree::fol::{Formula, Theory},
 };
 
 pub fn simplify(theory: Theory) -> Theory {
@@ -12,232 +10,8 @@ pub fn simplify(theory: Theory) -> Theory {
     }
 }
 
-fn simplify_formula(formula: Formula) -> Formula {
-    formula.apply_all(&mut vec![
-        Box::new(remove_identities),
-        Box::new(remove_annihilations),
-        Box::new(remove_idempotences),
-        Box::new(join_nested_quantifiers),
-    ])
+pub fn simplify_formula(formula: Formula) -> Formula {
+    formula.apply(&mut INTUITIONISTIC.iter().chain(HT).compose())
 }
 
-fn remove_identities(formula: Formula) -> Formula {
-    // Remove identities
-    // e.g. F op E => F
-
-    match formula.unbox() {
-        // F and #true => F
-        UnboxedFormula::BinaryFormula {
-            connective: BinaryConnective::Conjunction,
-            lhs,
-            rhs: Formula::AtomicFormula(AtomicFormula::Truth),
-        } => lhs,
-
-        // #true and F => F
-        UnboxedFormula::BinaryFormula {
-            connective: BinaryConnective::Conjunction,
-            lhs: Formula::AtomicFormula(AtomicFormula::Truth),
-            rhs,
-        } => rhs,
-
-        // F or #false => F
-        UnboxedFormula::BinaryFormula {
-            connective: BinaryConnective::Disjunction,
-            lhs,
-            rhs: Formula::AtomicFormula(AtomicFormula::Falsity),
-        } => lhs,
-
-        // #false or F => F
-        UnboxedFormula::BinaryFormula {
-            connective: BinaryConnective::Disjunction,
-            lhs: Formula::AtomicFormula(AtomicFormula::Falsity),
-            rhs,
-        } => rhs,
-
-        x => x.rebox(),
-    }
-}
-
-fn remove_annihilations(formula: Formula) -> Formula {
-    // Remove annihilations
-    // e.g. F op E => E
-
-    match formula.unbox() {
-        // F or #true => #true
-        UnboxedFormula::BinaryFormula {
-            connective: BinaryConnective::Disjunction,
-            lhs: _,
-            rhs: rhs @ Formula::AtomicFormula(AtomicFormula::Truth),
-        } => rhs,
-
-        // #true or F => #true
-        UnboxedFormula::BinaryFormula {
-            connective: BinaryConnective::Disjunction,
-            lhs: lhs @ Formula::AtomicFormula(AtomicFormula::Truth),
-            rhs: _,
-        } => lhs,
-
-        // F and #false => false
-        UnboxedFormula::BinaryFormula {
-            connective: BinaryConnective::Conjunction,
-            lhs: _,
-            rhs: rhs @ Formula::AtomicFormula(AtomicFormula::Falsity),
-        } => rhs,
-
-        // #false and F => #false
-        UnboxedFormula::BinaryFormula {
-            connective: BinaryConnective::Conjunction,
-            lhs: lhs @ Formula::AtomicFormula(AtomicFormula::Falsity),
-            rhs: _,
-        } => lhs,
-
-        x => x.rebox(),
-    }
-}
-
-fn remove_idempotences(formula: Formula) -> Formula {
-    // Remove idempotences
-    // e.g. F op F => F
-
-    match formula.unbox() {
-        // F and F => F
-        // F or  F => F
-        UnboxedFormula::BinaryFormula {
-            connective: BinaryConnective::Conjunction | BinaryConnective::Disjunction,
-            lhs,
-            rhs,
-        } if lhs == rhs => lhs,
-
-        x => x.rebox(),
-    }
-}
-
-pub(crate) fn join_nested_quantifiers(formula: Formula) -> Formula {
-    // Remove nested quantifiers
-    // e.g. q X ( q Y F(X,Y) ) => q X Y F(X,Y)
-
-    match formula.unbox() {
-        // forall X ( forall Y F(X,Y) ) => forall X Y F(X,Y)
-        // exists X ( exists Y F(X,Y) ) => exists X Y F(X,Y)
-        UnboxedFormula::QuantifiedFormula {
-            quantification: outer_quantification,
-            formula:
-                Formula::QuantifiedFormula {
-                    quantification: mut inner_quantification,
-                    formula: inner_formula,
-                },
-        } if outer_quantification.quantifier == inner_quantification.quantifier => {
-            let mut variables = outer_quantification.variables;
-            variables.append(&mut inner_quantification.variables);
-            variables.sort();
-            variables.dedup();
-
-            inner_formula.quantify(outer_quantification.quantifier, variables)
-        }
-        x => x.rebox(),
-    }
-}
-
-#[cfg(test)]
-mod tests {
-    use {
-        super::{
-            join_nested_quantifiers, remove_annihilations, remove_idempotences, remove_identities,
-            simplify_formula,
-        },
-        crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula},
-    };
-
-    #[test]
-    fn test_simplify() {
-        for (src, target) in [
-            ("#true and #true and a", "a"),
-            ("#true and (#true and a)", "a"),
-        ] {
-            assert_eq!(
-                simplify_formula(src.parse().unwrap()),
-                target.parse().unwrap()
-            )
-        }
-    }
-
-    #[test]
-    fn test_remove_identities() {
-        for (src, target) in [
-            ("#true and a", "a"),
-            ("a and #true", "a"),
-            ("#false or a", "a"),
-            ("a or #false", "a"),
-        ] {
-            assert_eq!(
-                src.parse::<Formula>()
-                    .unwrap()
-                    .apply(&mut remove_identities),
-                target.parse().unwrap()
-            )
-        }
-    }
-
-    #[test]
-    fn test_remove_annihilations() {
-        for (src, target) in [
-            ("#true or a", "#true"),
-            ("a or #true", "#true"),
-            ("#false and a", "#false"),
-            ("a and #false", "#false"),
-        ] {
-            assert_eq!(
-                src.parse::<Formula>()
-                    .unwrap()
-                    .apply(&mut remove_annihilations),
-                target.parse().unwrap()
-            )
-        }
-    }
-
-    #[test]
-    fn test_remove_idempotences() {
-        for (src, target) in [("a and a", "a"), ("a or a", "a")] {
-            assert_eq!(
-                src.parse::<Formula>()
-                    .unwrap()
-                    .apply(&mut remove_idempotences),
-                target.parse().unwrap()
-            )
-        }
-    }
-
-    #[test]
-    fn test_join_nested_quantifiers() {
-        for (src, target) in [
-            ("exists X (exists Y (X = Y))", "exists X Y (X = Y)"),
-            (
-                "exists X Y ( exists Z ( X < Y and Y < Z ))",
-                "exists X Y Z ( X < Y and Y < Z )",
-            ),
-            (
-                "exists X (exists Y (X = Y and q(Y)))",
-                "exists X Y (X = Y and q(Y))",
-            ),
-            (
-                "exists X (exists X$i (p(X) -> X$i < 1))",
-                "exists X X$i (p(X) -> X$i < 1)",
-            ),
-            (
-                "forall X Y (forall Y Z (p(X,Y) and q(Y,Z)))",
-                "forall X Y Z (p(X,Y) and q(Y,Z))",
-            ),
-            (
-                "forall X (forall Y (forall Z (X = Y = Z)))",
-                "forall X Y Z (X = Y = Z)",
-            ),
-        ] {
-            assert_eq!(
-                src.parse::<Formula>()
-                    .unwrap()
-                    .apply(&mut join_nested_quantifiers),
-                target.parse().unwrap()
-            )
-        }
-    }
-}
+pub const HT: &[fn(Formula) -> Formula] = &[];