Bugfix / implement tests for formulas and grammars

README.md

@@ -95,7 +95,7 @@ pip install mathesis
 
 ## Roadmap
 
-- [ ] Add tests
+- [ ] Add tests (WIP)
 - [ ] Hilbert systems
 - [x] Natural deduction
 - [ ] Boolean algebra

mathesis/forms.py

@@ -46,7 +46,7 @@ def free_terms(self):
         return self.terms
 
     def replace_term(self, replaced_term, replacing_term):
-        fml = self
+        fml = self.clone()
         fml.terms = [
             replacing_term if term == replaced_term else term for term in self.terms
         ]
@@ -132,7 +132,7 @@ def free_terms(self):
         return self.sub.free_terms
 
     def replace_term(self, replaced_term, replacing_term):
-        fml = self
+        fml = self.clone()
         fml.sub = self.sub.replace_term(replaced_term, replacing_term)
         return fml
 
@@ -187,9 +187,9 @@ def free_terms(self):
 
     def replace_term(self, replaced_term, replacing_term):
         # fml = copy(self)
-        fml = self
+        fml = self.clone()
         subs = []
-        for subfml in self.subs:
+        for subfml in deepcopy(self.subs):
             subs.append(subfml.replace_term(replaced_term, replacing_term))
         fml.subs = subs
         return fml
@@ -205,7 +205,7 @@ def latex(self):
     def __str__(self) -> str:
         # print(self.subs)
         # return f"{self.connective}".join(map(lambda x: f"({x})", self.subs))
-        return f"{self.connective}".join(
+        return f" {self.connective} ".join(
             map(
                 lambda x: f"({x})" if isinstance(x, Binary) else f"{x}",
                 self.subs,

mathesis/semantics/truth_table/base.py

@@ -4,7 +4,7 @@
 from itertools import product
 
 from anytree import NodeMixin, PostOrderIter
-from prettytable import PLAIN_COLUMNS, PrettyTable
+from prettytable import TableStyle, PrettyTable
 
 from mathesis import forms
 
@@ -47,7 +47,7 @@ def to_table(self):
 
         return table
 
-    def to_string(self, style=PLAIN_COLUMNS):
+    def to_string(self, style=TableStyle.PLAIN_COLUMNS):
         table = self.to_table()
         table.set_style(style)
         return str(table)
@@ -405,7 +405,7 @@ def to_table(self):
 
         return table
 
-    def to_string(self, style=PLAIN_COLUMNS):
+    def to_string(self, style=TableStyle.PLAIN_COLUMNS):
         table = self.to_table()
         table.set_style(style)
         return str(table)

tests/test_forms.py

@@ -0,0 +1,130 @@
+from mathesis.forms import (
+    Formula,
+    Atom,
+    Top,
+    Bottom,
+    Negation,
+    Disjunction,
+    Conjunction,
+    Conditional,
+    Universal,
+    Particular
+)
+
+
+# ⊤ ∨ (¬Q ∨ R)
+propositional_formula_1 = Disjunction(
+    Top(),
+    Disjunction(
+        Negation(Atom("Q")),
+        Atom("R")
+    )
+)
+
+# (P ∧ ¬P) → ⊥
+propositional_formula_2 = Conditional(
+    Conjunction(
+        Atom("P"),
+        Negation(Atom("P"))
+    ),
+    Bottom()
+)
+
+# ∀x(P(x) → (Q(x) ∨ R(x)))
+quantified_formula_1 = Universal(
+    "x",
+    Conditional(
+        Atom("P", terms=["x"]),
+        Disjunction(
+            Atom("Q", terms=["x"]),
+            Atom("R", terms=["x"])
+        )
+    )
+)
+
+# ∃y(¬Q(y) ∧ ¬R(a, b, y))
+quantified_formula_2 = Particular(
+    "y",
+    Conjunction(
+        Negation(Atom("Q", terms=["y"])),
+        Negation(Atom("R", terms=["a", "b", "y"]))
+    )
+)
+
+
+def test_repr():
+    assert repr(propositional_formula_1) == "Disj[Top, Disj[Neg[Atom[Q]], Atom[R]]]"
+    assert repr(propositional_formula_2) == "Cond[Conj[Atom[P], Neg[Atom[P]]], Bottom]"
+    assert repr(quantified_formula_1) == "Forall<x>[Cond[Atom[P(x)], Disj[Atom[Q(x)], Atom[R(x)]]]]"
+    assert repr(quantified_formula_2) == "Exists<y>[Conj[Neg[Atom[Q(y)]], Neg[Atom[R(a, b, y)]]]]"
+
+
+def test_str():
+    assert str(propositional_formula_1) == "⊤ ∨ (¬Q ∨ R)"
+    assert str(propositional_formula_2) == "(P ∧ ¬P) → ⊥"
+    assert str(quantified_formula_1) == "∀x(P(x) → (Q(x) ∨ R(x)))"
+    assert str(quantified_formula_2) == "∃y(¬Q(y) ∧ ¬R(a, b, y))"
+
+
+def test_latex():
+    assert propositional_formula_1.latex() == r"\top \lor (\neg Q \lor R)"
+    assert propositional_formula_2.latex() == r"(P \land \neg P) \to \bot"
+    assert quantified_formula_1.latex() == r"\forall x (P(x) \to (Q(x) \lor R(x)))"
+    assert quantified_formula_2.latex() == r"\exists y (\neg Q(y) \land \neg R(a, b, y))"
+
+
+def test_atoms():
+    assert propositional_formula_1.atoms == {
+        "Q": [Atom("Q")],
+        "R": [Atom("R")]
+    }
+    assert propositional_formula_2.atoms == {
+        "P": [Atom("P"), Atom("P")]
+    }
+    assert quantified_formula_1.atoms == {
+        "P(x)": [Atom("P", terms=["x"])],
+        "Q(x)": [Atom("Q", terms=["x"])],
+        "R(x)": [Atom("R", terms=["x"])]
+    }
+    assert quantified_formula_2.atoms == {
+        "Q(y)": [Atom("Q", terms=["y"])],
+        "R(a, b, y)": [Atom("R", terms=["a", "b", "y"])]
+    }
+
+
+def test_atom_symbols():
+    assert propositional_formula_1.atom_symbols == ["Q", "R"]
+    assert propositional_formula_2.atom_symbols == ["P"]
+    assert quantified_formula_1.atom_symbols == ["P(x)", "Q(x)", "R(x)"]
+    assert quantified_formula_2.atom_symbols == ["Q(y)", "R(a, b, y)"]
+
+
+def test_equality():
+    assert propositional_formula_1 == propositional_formula_1
+    assert propositional_formula_2 != propositional_formula_1
+    assert propositional_formula_2 != quantified_formula_1
+    assert quantified_formula_1 == quantified_formula_1
+    assert quantified_formula_2 == quantified_formula_2
+    assert quantified_formula_1 != quantified_formula_2
+
+
+def test_free_terms():
+    assert propositional_formula_1.free_terms == []
+    assert propositional_formula_2.free_terms == []
+    assert quantified_formula_1.free_terms == []
+    assert quantified_formula_2.free_terms == ["a", "b"]
+
+
+def test_replace_term():
+    assert propositional_formula_1.replace_term("Q", "R") == propositional_formula_1
+    assert quantified_formula_1.replace_term("x", "y") == Conditional(
+        Atom("P", terms=["y"]),
+        Disjunction(
+            Atom("Q", terms=["y"]),
+            Atom("R", terms=["y"])
+        )
+    )
+    assert quantified_formula_2.replace_term("a", "b") == Conjunction(
+        Negation(Atom("Q", terms=["y"])),
+        Negation(Atom("R", terms=["b", "b", "y"]))
+    )

tests/test_grammars.py

@@ -0,0 +1,85 @@
+from mathesis.grammars import (
+    BasicPropositionalGrammar,
+    BasicGrammar
+)
+from mathesis.forms import (
+    Atom,
+    Top,
+    Bottom,
+    Negation,
+    Conjunction,
+    Disjunction,
+    Conditional,
+    Universal,
+    Particular
+)
+
+
+def test_propositional_grammar():
+    grammar = BasicPropositionalGrammar()
+    assert grammar.parse("⊥ ∨ (B → C)") == Disjunction(
+        Bottom(),
+        Conditional(
+            Atom("B"),
+            Atom("C")
+        )
+    )
+    assert grammar.parse("⊤ ∧ (P_1 ∧ ¬P_2)") == Conjunction(
+        Top(),
+        Conjunction(
+            Atom("P_1"),
+            Negation(Atom("P_2"))
+        )
+    )
+
+    # Test for the order of precedence of operators
+    assert grammar.parse("P ∨ Q ∧ ¬R → T") == Conditional(
+        Disjunction(
+            Atom("P"),
+            Conjunction(
+                Atom("Q"),
+                Negation(Atom("R"))
+            )
+        ),
+        Atom("T")
+    )
+
+    # Test for symbol customization
+    grammar = BasicPropositionalGrammar(
+        symbols={"conditional": "->"}
+    )
+    assert grammar.parse("A -> B") == Conditional(Atom("A"), Atom("B"))
+
+
+def test_first_order_grammar():
+    grammar = BasicGrammar()
+    assert grammar.parse("∀x((P(x) ∧ Q(x)) → R(x, x))") == Universal(
+        "x",
+        Conditional(
+            Conjunction(
+                Atom("P", terms=["x"]),
+                Atom("Q", terms=["x"])
+            ),
+            Atom("R", terms=["x", "x"])
+        )
+    )
+
+    assert grammar.parse("∃y∀x(P123(x, y) ∨ P123(y, x))") == Particular(
+        "y",
+        Universal(
+            "x",
+            Disjunction(
+                Atom("P123", terms=["x", "y"]),
+                Atom("P123", terms=["y", "x"])
+            )
+        )
+    )
+
+    # Test with nullary predicates (propositions)
+    assert grammar.parse("⊤ ∨ (A → B)") == Disjunction(
+        Top(),
+        Conditional(
+            Atom("A"),
+            Atom("B")
+        )
+    )