Implement integer comparison operators in Aura

aura_lang/interpreter.py

@@ -162,6 +162,8 @@ def eval_infix_expression(op, left, right):
         if op == '-': return Integer(l - r)
         if op == '*': return Integer(l * r)
         if op == '/': return Integer(l // r)
+        if op == '>': return Object(l > r)
+        if op == '<': return Object(l < r)
         return Object(False) # Unsupported operator for integers
 
     return Object(False) # Unsupported operator for the given types

lfi_ill/__init__.py

@@ -2,4 +2,4 @@
 from .token import *
 from .lexer import *
 from .parser import *
-from .interpreter import *
+from .prover import *

lfi_ill/ast.py

@@ -1,90 +1,189 @@
-# AST Node classes
+from __future__ import annotations
+from dataclasses import dataclass
+
+# Base class for all formulas
 class Formula:
-    pass
+    def neg(self) -> Formula:
+        raise NotImplementedError
 
+# Atoms and their linear negations
+@dataclass(frozen=True, eq=True)
 class Atom(Formula):
-    def __init__(self, name, negated=False):
-        self.name = name
-        self.negated = negated
-    def __repr__(self):
-        return f"Atom({self.name}{'`' if self.negated else ''})"
+    name: str
+    negated: bool = False
+
+    def __repr__(self) -> str:
+        return f"{self.name}{'⊥' if self.negated else ''}"
+
+    def neg(self) -> Atom:
+        return Atom(self.name, not self.negated)
 
+# Multiplicative Connectives
+@dataclass(frozen=True, eq=True)
 class Tensor(Formula):
-    def __init__(self, left, right):
-        self.left = left
-        self.right = right
-    def __repr__(self):
-        return f"Tensor({self.left}, {self.right})"
+    left: Formula
+    right: Formula
 
+    def __repr__(self) -> str:
+        return f"({self.left} ⊗ {self.right})"
+
+    def neg(self) -> Par:
+        return Par(self.left.neg(), self.right.neg())
+
+@dataclass(frozen=True, eq=True)
 class Par(Formula):
-    def __init__(self, left, right):
-        self.left = left
-        self.right = right
-    def __repr__(self):
-        return f"Par({self.left}, {self.right})"
+    left: Formula
+    right: Formula
 
-class Plus(Formula):
-    def __init__(self, left, right):
-        self.left = left
-        self.right = right
-    def __repr__(self):
-        return f"Plus({self.left}, {self.right})"
+    def __repr__(self) -> str:
+        return f"({self.left} ⅋ {self.right})"
+
+    def neg(self) -> Tensor:
+        return Tensor(self.left.neg(), self.right.neg())
+
+@dataclass(frozen=True, eq=True)
+class One(Formula):
+    def __repr__(self) -> str:
+        return "1"
+
+    def neg(self) -> Bottom:
+        return Bottom()
+
+@dataclass(frozen=True, eq=True)
+class Bottom(Formula):
+    def __repr__(self) -> str:
+        return "⊥"
 
+    def neg(self) -> One:
+        return One()
+
+# Additive Connectives
+@dataclass(frozen=True, eq=True)
 class With(Formula):
-    def __init__(self, left, right):
-        self.left = left
-        self.right = right
-    def __repr__(self):
-        return f"With({self.left}, {self.right})"
+    left: Formula
+    right: Formula
+
+    def __repr__(self) -> str:
+        return f"({self.left} & {self.right})"
+
+    def neg(self) -> Plus:
+        return Plus(self.left.neg(), self.right.neg())
+
+@dataclass(frozen=True, eq=True)
+class Plus(Formula):
+    left: Formula
+    right: Formula
+
+    def __repr__(self) -> str:
+        return f"({self.left} ⊕ {self.right})"
+
+    def neg(self) -> With:
+        return With(self.left.neg(), self.right.neg())
+
+@dataclass(frozen=True, eq=True)
+class Top(Formula):
+    def __repr__(self) -> str:
+        return "⊤"
+
+    def neg(self) -> Zero:
+        return Zero()
+
+@dataclass(frozen=True, eq=True)
+class Zero(Formula):
+    def __repr__(self) -> str:
+        return "0"
+
+    def neg(self) -> Top:
+        return Top()
 
+# Modal Operators
+@dataclass(frozen=True, eq=True)
 class OfCourse(Formula):
-    def __init__(self, formula):
-        self.formula = formula
-    def __repr__(self):
-        return f"OfCourse({self.formula})"
+    formula: Formula
+
+    def __repr__(self) -> str:
+        return f"!{self.formula}"
 
+    def neg(self) -> WhyNot:
+        return WhyNot(self.formula.neg())
+
+@dataclass(frozen=True, eq=True)
 class WhyNot(Formula):
-    def __init__(self, formula):
-        self.formula = formula
-    def __repr__(self):
-        return f"WhyNot({self.formula})"
+    formula: Formula
+
+    def __repr__(self) -> str:
+        return f"?{self.formula}"
+
+    def neg(self) -> OfCourse:
+        return OfCourse(self.formula.neg())
 
+@dataclass(frozen=True, eq=True)
 class Section(Formula):
-    def __init__(self, formula):
-        self.formula = formula
-    def __repr__(self):
-        return f"Section({self.formula})"
+    formula: Formula
 
+    def __repr__(self) -> str:
+        return f"§{self.formula}"
+
+    def neg(self) -> Section:
+        return Section(self.formula.neg())
+
+# Paraconsistent and Other Operators
+@dataclass(frozen=True, eq=True)
 class Negation(Formula):
-    def __init__(self, formula):
-        self.formula = formula
-    def __repr__(self):
-        return f"Negation({self.formula})"
+    formula: Formula
+
+    def __repr__(self) -> str:
+        return f"¬{self.formula}"
+
+    def neg(self) -> NegationPerp:
+        return NegationPerp(self)
+
+@dataclass(frozen=True, eq=True)
+class NegationPerp(Formula):
+    formula: Formula # Should be a Negation instance
+
+    def __repr__(self) -> str:
+        return f"({self.formula})⊥"
 
+    def neg(self) -> Formula:
+        return self.formula
+
+@dataclass(frozen=True, eq=True)
 class Consistency(Formula):
-    def __init__(self, formula):
-        self.formula = formula
-    def __repr__(self):
-        return f"Consistency({self.formula})"
+    formula: Formula
+
+    def __repr__(self) -> str:
+        return f"∘{self.formula}"
+
+    def neg(self) -> Inconsistency:
+        return Inconsistency(self)
+
+@dataclass(frozen=True, eq=True)
+class Inconsistency(Formula):
+    formula: Formula # Should be a Consistency instance
+
+    def __repr__(self) -> str:
+        return f"({self.formula})⊥"
+
+    def neg(self) -> Formula:
+        return self.formula
 
+@dataclass(frozen=True, eq=True)
 class Completeness(Formula):
-    def __init__(self, formula):
-        self.formula = formula
-    def __repr__(self):
-        return f"Completeness({self.formula})"
+    formula: Formula
 
-class One(Formula):
-    def __repr__(self):
-        return "One"
+    def __repr__(self) -> str:
+        return f"~{self.formula}"
 
-class Bottom(Formula):
-    def __repr__(self):
-        return "Bottom"
+    def neg(self) -> NonCompleteness:
+        return NonCompleteness(self)
 
-class Zero(Formula):
-    def __repr__(self):
-        return "Zero"
+@dataclass(frozen=True, eq=True)
+class NonCompleteness(Formula):
+    formula: Formula # Should be a Completeness instance
 
-class Top(Formula):
-    def __repr__(self):
-        return "Top"
+    def __repr__(self) -> str:
+        return f"({self.formula})⊥"
+
+    def neg(self) -> Formula:
+        return self.formula