Simplify abstract type structuring

proof.py

@@ -15,45 +15,51 @@ class App(Term):
     f : Term
     x : Term
 
+A0 = lambda fn : Const(fn)
+A1 = lambda fn, a : App(f=A0(fn), x=a)
+A2 = lambda fn, a, b : App(f=A1(fn, a), x=b)
+A3 = lambda fn, a, b, c : App(f=A2(fn, a, b), x=c)
+A4 = lambda fn, a, b, c, d : App(f=A3(fn, a, b, c), x=d)
+A5 = lambda fn, a, b, c, d, e : App(f=A4(fn, a, b, c, d), x=e)
+A6 = lambda fn, a, b, c, d, e, f : App(f=A5(fn, a, b, c, d, e), x=f)
+A7 = lambda fn, a, b, c, d, e, f, g : App(f=A6(fn, a, b, c, d, e, f), x=g)
+A8 = lambda fn, a, b, c, d, e, f, g, h : App(f=A7(fn, a, b, c, d, e, f, g), x=h)
+
 @dataclass(frozen=True)
 class Const(Term):
     name : str
 
-@dataclass(frozen=True)
-class Var(Term):
-    name : str
-
 # --- Bool constructors ---
 
-Bool = Union["Truth", "Contradiction"]
+def Truth() -> Term:
+    return A0("Bool.Truth")
 
-@dataclass(frozen=True)
+def Contradiction() -> Term:
-class Truth(Term):
+    return A0("Bool.Contradiction")
-    pass
 
-@dataclass(frozen=True)
+# --- List constructors ---
-class Contradiction(Term):
+
-    pass
+def Nil() -> Term:
+    return A0("List.Nil")
+
+def Cons(head : Term, tail : Term) -> Term:
+    return A2("List.Cons", head, tail)
 
 # --- Nat constructors ---
 
-Nat = Union["Zero", "Succ"]
+def Zero() -> Term:
+    return A0("Nat.Zero")
 
-@dataclass(frozen=True)
+def Succ(n : Term) -> Term:
-class Zero(Term):
+    return A1("Nat.Succ", n)
-    pass
 
-@dataclass(frozen=True)
+def kernel_from_int(n : int) -> Term:
-class Succ(Term):
-    n : Term
-
-def kernel_from_int(n : int) -> Nat:
     if n == 0:
         return Zero()
     elif n < 0:
         raise ValueError("Int is not Nat")
     else:
-        return Succ(n=kernel_from_int(n=n-1))
+        return Succ(kernel_from_int(n-1))
 
 # -----------------------------------------------------------------------------
 # Propositions
@@ -87,40 +93,44 @@ class F:
     arity : int
     func : Callable[..., Term | None]
 
+F_ = lambda a : lambda f : F(arity=a, func=f)
+F0, F1, F2, F3 = F_(0), F_(1), F_(2), F_(3)
+F4, F5, F6, F7 = F_(4), F_(5), F_(6), F_(7)
+
 def apply_rules() -> dict[str, F]:
     def __bool_not(x : Term) -> Term | None:
         match x:
-            case Truth():
+            case Const("Bool.Truth"):
                 return Contradiction()
             
-            case Contradiction():
+            case Const("Bool.Contradiction"):
                 return Truth()
     
     def __nat_add(x : Term, y : Term) -> Term | None:
         match x:
-            case Zero():
+            case Const("Nat.Zero"):
                 return y
             
-            case Succ():
+            case App(f=Const("Nat.Succ"), x=x_):
                 return Succ(
-                    n=normalize(App(
+                    App(
-                        f=App(Const("Nat.add"), x=x.n),
+                        f=App(Const("Nat.add"), x_),
                         x=y,
-                    ))
+                    )
                 )
     
     def __nat_iszero(x : Term) -> Term | None:
         match x:
-            case Zero():
+            case Const("Nat.Zero"):
                 return Truth()
             
-            case Succ():
+            case App(f=Const("Nat.Succ")):
                 return Contradiction()
     
     return {
-        "Bool.not": F(arity=1, func=__bool_not),
+        "Bool.not": F1(__bool_not),
-        "Nat.add" : F(arity=2, func=__nat_add),
+        "Nat.add" : F2(__nat_add),
-        "Nat.isZero" : F(arity=1, func=__nat_iszero),
+        "Nat.isZero" : F1(__nat_iszero),
     }
                 
 
@@ -154,39 +164,14 @@ def normalize(term : Term) -> Term:
                         
                         out = rule.func(*reversed([i.x for i in items]))
 
-                        return out if out is not None else App(f, x)
+                        return normalize(out) if out is not None else App(f, x)
-
-                    case Contradiction():
-                        if len(items) != 2:
-                            # Either evaluating too early or too late
-                            return term
-                        
-                        # Return the "second" item
-                        return x
-
-                    case Truth():
-                        if len(items) != 2:
-                            # Either evaluating too early or too late
-                            return App(f, x)
-                        
-                        # Return the "first" item
-                        return cursor.x
 
         case Const():
             return term
 
-        case Succ():
-            return Succ(n=normalize(term.n))
-        
         case Term():
             return term
 
-        case Var():
-            return term
-        
-        case Zero():
-            return term
-
 # -----------------------------------------------------------------------------
 # Proof checker
 # -----------------------------------------------------------------------------
@@ -207,7 +192,7 @@ if __name__ == "__main__":
     # 2 + 3 == 5
     print(check(
         Eq(
-            lhs=App(f=App(f=Const("Nat.add"), x=kernel_from_int(2)), x=kernel_from_int(3)),
+            lhs=A2("Nat.add", kernel_from_int(2), kernel_from_int(3)),
             rhs=kernel_from_int(5),
         ),
         Refl(),
@@ -216,8 +201,8 @@ if __name__ == "__main__":
     # 0 + x == x
     print(check(
         Eq(
-            lhs=App(f=App(f=Const("Nat.add"), x=Zero()), x=Var("x")),
+            lhs=A2("Nat.add", Zero(), Const("x")),
-            rhs=Var("x")
+            rhs=Const("x")
         ),
         Refl(),
     ))
@@ -225,8 +210,8 @@ if __name__ == "__main__":
     # x + 0 == x
     print(check(
         Eq(
-            lhs=App(f=App(f=Const("Nat.add"), x=Var("x")), x=Zero()),
+            lhs=A2("Nat.add", Const("x"), Zero()),
-            rhs=Var("x")
+            rhs=Const("x")
         ),
         Refl(),
     ))