From cb83bb5ee8b19a29a6b2b23c3382aa32efe7e45b Mon Sep 17 00:00:00 2001
From: Christopher Hampson <christopher.hampson.1989@gmail.com>
Date: Tue, 17 Mar 2026 16:25:40 +0000
Subject: [PATCH] feat: allow configurable symbols for all connectives

---
 mathesis/forms.py    | 10 ++++++
 mathesis/grammars.py | 75 +++++++++++++++++++++++++++++++-------------
 2 files changed, 63 insertions(+), 22 deletions(-)

diff --git a/mathesis/forms.py b/mathesis/forms.py
index 6b92eac..33a27a7 100644
--- a/mathesis/forms.py
+++ b/mathesis/forms.py
@@ -187,6 +187,16 @@ class Negation(Unary):
     connective = "¬"
     connective_latex = r"\neg"
 
+class Possibility(Unary):
+    signature = "Poss"
+    connective = "◇"
+    connective_latex = r"\Diamond"
+
+class Necessity(Unary):
+    signature = "Necc"
+    connective = "□"
+    connective_latex = r"\Box"
+
 
 class Binary(Formula):
     subs: tuple[Formula, Formula]
diff --git a/mathesis/grammars.py b/mathesis/grammars.py
index aae8f81..db6ec61 100644
--- a/mathesis/grammars.py
+++ b/mathesis/grammars.py
@@ -12,6 +12,8 @@
     Conjunction,
     Disjunction,
     Negation,
+    Possibility,
+    Necessity,
     Particular,
     Universal,
 )
@@ -32,6 +34,12 @@ def bottom(self, v):
 
     def negation(self, v):
         return Negation(*v)
+    
+    def possibility(self, v):
+        return Possibility(*v)
+    
+    def necessity(self, v):
+        return Necessity(*v)
 
     def universal(self, v):
         return Universal(*v)
@@ -90,11 +98,24 @@ def parse(self, text_or_list: str | list):
 class BasicPropositionalGrammar(Grammar):
     """Basic grammar for the propositional language."""
 
+    default_symbols = {
+        "top": "⊤",
+        "bottom": "⊥",
+        "negation": "¬",
+        "conjunction": "∧",
+        "disjunction": "∨",
+        "conditional": "→",
+        "necessity": "□",
+        "possibility": "◇",
+    }
+
     grammar_rules = r"""
 ?fml: conditional
     | disjunction
     | conjunction
     | negation
+    | necessity
+    | possibility
     | top
     | bottom
     | atom
@@ -103,34 +124,44 @@ class BasicPropositionalGrammar(Grammar):
 ATOM : /\w+/
 
 atom : ATOM
-top : "⊤"
-bottom : "⊥"
-negation : "¬" fml
-conjunction : (conjunction | fml) "∧" fml
-disjunction : (disjunction | fml) "∨" fml
-conditional : fml "{conditional_symbol}" fml
-necc : "□" fml
-poss : "◇" fml
+top : "{top}"
+bottom : "{bottom}"
+negation : "{negation}" fml
+conjunction : (conjunction | fml) "{conjunction}" fml
+disjunction : (disjunction | fml) "{disjunction}" fml
+conditional : fml "{conditional}" fml
+necessity : "{necessity}" fml
+possibility : "{possibility}" fml
 
 %import common.WS
 %ignore WS
 """.lstrip()
 
-    def __init__(self, symbols={"conditional": "→"}):
-        self.grammar_rules = self.grammar_rules.format(
-            conditional_symbol=symbols["conditional"]
-        )
+    def __init__(self, symbols=None):
+        merged = self.default_symbols.copy()
+        if symbols is not None:
+            merged.update(symbols)
+        self.symbols = merged
+        self.grammar_rules = self.grammar_rules.format(**merged)
         super().__init__()
 
 
 class BasicGrammar(BasicPropositionalGrammar):
     """Basic grammar for the first-order language."""
 
+    default_symbols = {
+        **BasicPropositionalGrammar.default_symbols,
+        "universal": "∀",
+        "particular": "∃",
+    }
+
     grammar_rules = r"""
 ?fml: conditional
     | disjunction
     | conjunction
     | negation
+    | necessity
+    | possibility
     | universal
     | particular
     | top
@@ -142,16 +173,16 @@ class BasicGrammar(BasicPropositionalGrammar):
 TERM: /\w+/
 
 atom : PREDICATE ("(" TERM ("," TERM)* ")")?
-top : "⊤"
-bottom : "⊥"
-negation : "¬" fml
-conjunction : fml "∧" fml
-disjunction : fml "∨" fml
-conditional : fml "{conditional_symbol}" fml
-necc : "□" fml
-poss : "◇" fml
-universal : "∀" TERM fml
-particular : "∃" TERM fml
+top : "{top}"
+bottom : "{bottom}"
+negation : "{negation}" fml
+conjunction : fml "{conjunction}" fml
+disjunction : fml "{disjunction}" fml
+conditional : fml "{conditional}" fml
+necessity : "{necessity}" fml
+possibility : "{possibility}" fml
+universal : "{universal}" TERM fml
+particular : "{particular}" TERM fml
 
 %import common.WS
 %ignore WS