updated README

.gitignore

@@ -0,0 +1,3 @@
+**/*.du
+**/*.ud
+lib/github.com/*

README.md

@@ -1,3 +1,2 @@
 # proof-checker
-testing blah blah
-wow it's working!
+Proof checker based on first order logic. The eventual goal is to be as readable and natural as possible.

lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig

@@ -0,0 +1,17 @@
+signature FORMULA =
+sig
+  datatype t =
+    Named of string
+  | Relation of string * Term.t list
+  | Equal of Term.t * Term.t
+  | Bottom
+  | Neg of t
+  | Conj of t * t
+  | Disj of t * t
+  | Impl of t * t
+  | Iff of t * t
+  | Forall of t
+  | Exists of t
+
+  val eq: t * t -> bool
+end

lib/forgejo.ballcloud.cc/wball/proof-checker/Formula.sml

@@ -0,0 +1,35 @@
+structure Formula: FORMULA =
+struct
+  datatype t =
+    Named of string
+  | Relation of string * Term.t list
+  | Equal of Term.t * Term.t
+  | Bottom
+  | Neg of t
+  | Conj of t * t
+  | Disj of t * t
+  | Impl of t * t
+  | Iff of t * t
+  | Forall of t
+  | Exists of t
+
+  fun eq (Named s1, Named s2) = s1 = s2
+    | eq (Relation (r, ts), Relation (p, ss)) =
+        (r = p andalso List.all Term.eq (ListPair.zip (ts, ss))
+         handle unequalLengths => false)
+    | eq (Equal (t, s), Equal (t', s')) =
+        Term.eq (t, t') andalso Term.eq (s, s')
+    | eq (Bottom, Bottom) = true
+    | eq (Neg phi, Neg psi) = eq (phi, psi)
+    | eq (Conj (phi, psi), Conj (phi', psi')) =
+        eq (phi, phi') andalso eq (psi, psi')
+    | eq (Disj (phi, psi), Disj (phi', psi')) =
+        eq (phi, phi') andalso eq (psi, psi')
+    | eq (Impl (phi, psi), Impl (phi', psi')) =
+        eq (phi, phi') andalso eq (psi, psi')
+    | eq (Iff (phi, psi), Iff (phi', psi')) =
+        eq (phi, phi') andalso eq (psi, psi')
+    | eq (Forall phi, Forall psi) = eq (phi, psi)
+    | eq (Exists phi, Exists psi) = eq (phi, psi)
+    | eq _ = false
+end

lib/forgejo.ballcloud.cc/wball/proof-checker/PROOF.sig

@@ -0,0 +1,28 @@
+signature PROOF =
+sig
+  datatype label =
+    Axiom
+  | AndI
+  | AndE
+  | OrI
+  | OrE
+  | ArrI
+  | ArrE
+  | NegI
+  | NegE
+  | RAA
+  | IffI
+  | IffE
+  | EqI
+  | EqE
+  | ForAllI
+  | ForAllE
+  | ExistsI
+  | ExistsE
+
+  exception ProofError of int
+
+  datatype t = Proof of {children: t list, label: label, formula: Formula.t}
+
+  val valid: t * Formula.t list -> bool
+end

lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml

@@ -0,0 +1,225 @@
+structure Proof: PROOF =
+struct
+  datatype label =
+    Axiom
+  | AndI
+  | AndE
+  | OrI
+  | OrE
+  | ArrI
+  | ArrE
+  | NegI
+  | NegE
+  | RAA
+  | IffI
+  | IffE
+  | EqI
+  | EqE
+  | ForAllI
+  | ForAllE
+  | ExistsI
+  | ExistsE
+
+  exception ProofError of int
+
+  datatype t = Proof of {children: t list, label: label, formula: Formula.t}
+
+  local open Formula
+  in
+    infix eq
+    fun valid
+          ( Proof
+              { children =
+                  kids as
+                    [Proof {formula = phi, ...}, Proof {formula = psi, ...}]
+              , label = AndI
+              , formula = Conj (phi', psi')
+              }
+          , a
+          ) =
+          phi eq phi' andalso psi eq psi'
+          andalso List.all (fn k => valid (k, a)) kids
+      | valid
+          ( Proof
+              { children = [kid as Proof {formula = Conj (phi, psi), ...}]
+              , label = AndE
+              , formula = chi
+              }
+          , a
+          ) =
+          chi eq phi orelse chi eq psi andalso valid (kid, a)
+      | valid (Proof {children = [], label = Axiom, formula = phi}, a) =
+          let
+            fun mem (phi, []) = false
+              | mem (phi, x :: xs) =
+                  phi eq x orelse mem (phi, xs)
+          in
+            mem (phi, a)
+          end
+      | valid
+          ( Proof
+              { children = [kid as Proof {formula = phi, ...}]
+              , label = OrI
+              , formula = Disj (psi, chi)
+              }
+          , a
+          ) =
+          (phi eq psi orelse phi eq chi) andalso valid (kid, a)
+      | valid
+          ( Proof
+              { children =
+                  [ left as Proof {formula = Disj (phi, psi), ...}
+                  , mid as Proof {formula = chi, ...}
+                  , right as Proof {formula = chi', ...}
+                  ]
+              , label = OrE
+              , formula = chi''
+              }
+          , a
+          ) =
+          chi eq chi' andalso chi' eq chi'' andalso valid (left, a)
+          andalso valid (mid, phi :: a) andalso valid (right, psi :: a)
+      | valid
+          ( Proof
+              { children = [kid as Proof {formula = psi, ...}]
+              , label = ArrI
+              , formula = Impl (phi, psi')
+              }
+          , a
+          ) =
+          psi eq psi' andalso valid (kid, phi :: a)
+      | valid
+          ( Proof
+              { children =
+                  [ left as Proof {formula = Impl (phi, psi), ...}
+                  , right as Proof {formula = phi', ...}
+                  ]
+              , label = ArrE
+              , formula = psi'
+              }
+          , a
+          ) =
+          phi eq phi' andalso psi eq psi' andalso valid (left, a)
+          andalso valid (right, a)
+      | valid
+          ( Proof
+              { children = [kid as Proof {formula = Bottom, ...}]
+              , label = NegI
+              , formula = Neg phi
+              }
+          , a
+          ) =
+          valid (kid, phi :: a)
+      | valid
+          ( Proof
+              { children =
+                  [ left as Proof {formula = Neg phi, ...}
+                  , right as Proof {formula = phi', ...}
+                  ]
+              , label = NegE
+              , formula = Bottom
+              }
+          , a
+          ) =
+          phi eq phi' andalso valid (left, a) andalso valid (right, a)
+      | valid
+          ( Proof
+              { children = [kid as Proof {formula = Bottom, ...}]
+              , label = RAA
+              , formula = phi
+              }
+          , a
+          ) =
+          valid (kid, Neg phi :: a)
+      | valid
+          ( Proof
+              { children =
+                  [ left as Proof {formula = Impl (phi, psi), ...}
+                  , right as Proof {formula = Impl (psi', phi'), ...}
+                  ]
+              , label = IffI
+              , formula = Iff (phi'', psi'')
+              }
+          , a
+          ) =
+          phi eq phi' andalso phi' eq phi'' andalso psi eq psi'
+          andalso psi' eq psi'' andalso valid (left, a) andalso valid (right, a)
+      | valid
+          ( Proof
+              { children = [kid as Proof {formula = Iff (phi, psi), ...}]
+              , label = IffE
+              , formula = Impl (p, q)
+              }
+          , a
+          ) =
+          ((phi eq p andalso psi eq q) orelse (phi eq q andalso psi eq p))
+          andalso valid (kid, a)
+      | valid (Proof {children = [], label = EqI, formula = Equal (t, t')}, a) =
+          Term.eq (t, t')
+      (* | valid *)
+      (*     ( Proof *)
+      (*         { children = *)
+      (*             [ left as Proof {formula = Equal (t, s), ...} *)
+      (*             , right as Proof {formula = phi, ...} *)
+      (*             ] *)
+      (*         , label = EqE *)
+      (*         , formula = psi *)
+      (*         } *)
+      (*     , a *)
+      (*     ) = *)
+      (*     valid (left, a) andalso valid (right, a) *)
+      (*     andalso Formula.checkSubst (t, s) (phi, psi) *)
+      (* | valid *)
+      (*     ( Proof *)
+      (*         { children = [kid as Proof {formula = Forall (x, phi), ...}] *)
+      (*         , label = ForAllE *)
+      (*         , formula = psi *)
+      (*         } *)
+      (*     , a *)
+      (*     ) = *)
+      (*     valid (kid, a) *)
+      (*     andalso *)
+      (*     (case Formula.matchVariable x (phi, psi) of *)
+      (*        _ => true handle MatchFailure => false) *)
+      (* | valid *)
+      (*     ( Proof *)
+      (*         { children = [kid as Proof {formula = phi, ...}] *)
+      (*         , label = ExistsI *)
+      (*         , formula = Exist (x, psi) *)
+      (*         } *)
+      (*     , a *)
+      (*     ) = *)
+      (*     valid (kid, a) *)
+      (*     andalso *)
+      (*     (case Formula.matchVariable x (psi, phi) of *)
+      (*        _ => true handle MatchFailure => false) *)
+      (* | valid *)
+      (*     ( Proof *)
+      (*         { children = [kid as Proof {formula = phi, ...}] *)
+      (*         , label = ForAllI *)
+      (*         , formula = Forall (x, psi) *)
+      (*         } *)
+      (*     , a *)
+      (*     ) = *)
+      (*     valid (kid, a) *)
+      (*     andalso *)
+      (*     (case Formula.matchVariable x (psi, phi) of *)
+      (*        SOME (t as Term.Var x') => *)
+      (*          Var.eq (x, x') andalso not (List.exists (Formula.occurs t) a) *)
+      (*      | _ => false handle MatchFailure => false) *)
+      (* | valid *)
+      (*     ( Proof *)
+      (*         { children = *)
+      (*             [ left as Proof {formula = Exist (x, phi), ...} *)
+      (*             , right as Proof {formula = chi, ...} *)
+      (*             ] *)
+      (*         , label = ExistsE *)
+      (*         , formula = chi' *)
+      (*         } *)
+      (*     , a *)
+      (*     ) = *)
+      (*     valid (left, a) andalso valid (right, phi :: a) *)
+      (*     andalso not (List.exists (Formula.occurs (Term.Var x)) a) *)
+      (* | valid _ = false *)
+  end
+end

lib/forgejo.ballcloud.cc/wball/proof-checker/TERM.sig

@@ -0,0 +1,10 @@
+signature TERM =
+sig
+  datatype t =
+    Var of int (* de Bruijn index *)
+  | Const of string
+  | Free of string
+  | Function of string * t list
+
+  val eq: t * t -> bool
+end

lib/forgejo.ballcloud.cc/wball/proof-checker/Term.sml

@@ -0,0 +1,16 @@
+structure Term: TERM =
+struct
+  datatype t =
+    Var of int
+  | Const of string
+  | Free of string
+  | Function of string * t list
+
+  fun eq (Var x1, Var x2) = x1 = x2
+    | eq (Const s1, Const s2) = s1 = s2
+    | eq (Free s1, Free s2) = s1 = s2
+    | eq (Function (f1, args1), Function (f2, args2)) =
+        (f1 = f2 andalso List.all eq (ListPair.zip (args1, args2))
+         handle unequalLengths => false)
+    | eq _ = false
+end

lib/forgejo.ballcloud.cc/wball/proof-checker/proof-checker.mlb

@@ -0,0 +1,9 @@
+$(SML_LIB)/basis/basis.mlb
+../../../github.com/diku-dk/sml-parse/parse.mlb
+../../../github.com/diku-dk/sml-parse/simple_token.mlb
+TERM.sig
+Term.sml
+FORMULA.sig
+Formula.sml
+PROOF.sig
+Proof.sml

sml.pkg

@@ -0,0 +1,5 @@
+package forgejo.ballcloud.cc/wball/proof-checker
+
+require {
+  github.com/diku-dk/sml-parse 0.1.5 #5693148ec0e4cbba1a1664170d9814f3b63267d9
+}