mostly? done with parsing formulas

lib/forgejo.ballcloud.cc/wball/proof-checker/parser/FormulaParser.sml

@@ -0,0 +1,131 @@
+structure FormulaParser: PARSER =
+struct
+  type result = Formula.t
+
+  structure StringSet = Utils.StringSet
+  structure ArityMap = Utils.ArityMap
+
+  type state =
+    { binders: string list
+    , constants: StringSet.t
+    , functions: ArityMap.t
+    , relations: ArityMap.t
+    }
+
+  open ParseUtils
+  infix >>> ->> >>- ?? ??? || oo oor ??* >>=
+
+  fun ((p: 'a p) >>= (q: 'a -> 'b p)) ts =
+    case p ts of
+      OK (v, r, ts') => q v ts'
+    | NO e => NO e
+
+  open Formula
+  open Scanner
+
+  val prec =
+    fn AND => (6, 7)
+     | OR => (4, 5)
+     | RARROW => (3, 2)
+     | LRARROW => (1, 2)
+     | _ => (~1, ~1)
+
+  exception NotOperator
+
+  val comb_func =
+    fn AND => Conj
+     | OR => Disj
+     | RARROW => Impl
+     | LRARROW => Iff
+     | _ => fn (_, _) => raise NotOperator
+
+  fun parse
+    (state as
+       { binders = binders
+       , constants = constants
+       , functions = functions
+       , relations = relations
+       }) =
+    let
+      val termState =
+        {binders = binders, constants = constants, functions = functions}
+
+      val term_p = TermParser.parse termState
+
+      fun formula_p ts = parse state ts
+
+      fun equal_p ts =
+        ((term_p >>- eat EQ >>> term_p) oo Equal) ts
+
+      fun ident_p nil =
+            NO (Region.botloc, fn () =>
+              "expecting identifier but reached the end")
+        | ident_p ((Scanner.IDENT id, r) :: rest) = OK (id, r, rest)
+        | ident_p ((t, r) :: rest) =
+            NO (#1 r, fn () =>
+              "expecting identifier but found token " ^ pp_token t)
+
+      val bottom_p = eat HASH oo (fn () => Bottom)
+
+      fun forall_p ts =
+        ((eat FORALL ->> ident_p >>- eat DOT)
+         >>=
+         (fn id =>
+            parse
+              { binders = id :: binders
+              , constants = constants
+              , functions = functions
+              , relations = relations
+              } oo Forall)) ts
+
+      fun exists_p ts =
+        ((eat EXISTS ->> ident_p >>- eat DOT)
+         >>=
+         (fn id =>
+            parse
+              { binders = id :: binders
+              , constants = constants
+              , functions = functions
+              , relations = relations
+              } oo Exists)) ts
+
+      fun args_p ts =
+        (eat LPAREN
+         ->>
+         ((term_p oo (fn x => [x])) ??* (eat COMMA ->> term_p))
+           (Utils.flip op::) >>- eat RPAREN) ts
+
+      fun relation_p ((Scanner.IDENT id, r) :: rest) =
+            if ArityMap.member (relations, id) then
+              (args_p oo (fn args => Relation (id, rev args))) rest
+            else
+              NO (#1 r, fn () => "identifier '" ^ id ^ "' is not a relation")
+        | relation_p ((t, r) :: _) =
+            NO (#1 r, fn () =>
+              "expected identifier but found token " ^ pp_token t)
+        | relation_p [] =
+            NO (Region.botloc, fn () =>
+              "expecting identifier but reached the end")
+
+      val atomic_p =
+        bottom_p || equal_p || forall_p || exists_p || relation_p
+        || (eat LPAREN ->> formula_p >>- eat RPAREN)
+
+      fun comb_p mprec [] =
+            NO (Region.botloc, fn () => "expecting formula but reached the end")
+        | comb_p mprec ts =
+            case atomic_p ts of
+              NO e => NO e
+            | OK (v, r, []) => OK (v, r, [])
+            | OK (v, r1, ts as (t, r) :: rest) =>
+                let
+                  val (lprec, rprec) = prec t
+                  val comb = comb_func t
+                in
+                  if lprec < mprec then OK (v, r1, ts)
+                  else ((comb_p rprec) oo (fn res => comb (v, res))) rest
+                end
+    in
+      comb_p 0
+    end
+end

lib/forgejo.ballcloud.cc/wball/proof-checker/parser/SCANNER.sig

@@ -10,6 +10,7 @@ sig
   | LRARROW
   | DOT
   | COMMA
+  | HASH
   | FORALL
   | EXISTS
   | IDENT of string

lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Scanner.sml

@@ -12,6 +12,7 @@ struct
   | LRARROW
   | DOT
   | COMMA
+  | HASH
   | FORALL
   | EXISTS
   | IDENT of string
@@ -21,6 +22,7 @@ struct
     | map_token (Symb ")") = RPAREN
     | map_token (Symb ".") = DOT
     | map_token (Symb ",") = COMMA
+    | map_token (Symb "#") = HASH
     | map_token (Symb "&") = AND
     | map_token (Symb "|") = OR
     | map_token (Symb "=") = EQ
@@ -38,7 +40,7 @@ struct
     map (fn (t, r) => (map_token t, r))
     o
     tokenise
-      { sep_chars = "(),&|."
+      { sep_chars = "(),&|.#"
       , symb_chars = "<=>"
       , is_id = (List.all Char.isAlphaNum) o String.explode
       , is_num = const false
@@ -57,5 +59,6 @@ struct
      | FORALL => "forall"
      | EXISTS => "exists"
      | ERR => "unk"
+     | HASH => "#"
      | IDENT s => s
 end

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

@@ -8,4 +8,5 @@ Scanner.sml
 ParseUtils.sml
 PARSER.sig
 TermParser.sml
+FormulaParser.sml
 repl.sml

lib/forgejo.ballcloud.cc/wball/proof-checker/parser/repl.sml

@@ -1,29 +1,34 @@
 open Scanner
 
-structure TermTesting:
+structure Testing:
 sig
   val parse_repl: string -> unit
 end =
 struct
-  open TermParser
+  open FormulaParser
   open Utils
   open ParseUtils
   open Scanner
 
-  val binders = ["y", "x"]
   val functions = ArityMap.fromList [("S", 1), ("plus", 2)]
   val constants = StringSet.fromList ["zero"]
-  val state = {binders = binders, functions = functions, constants = constants}
+  val relations = ArityMap.fromList [("lt", 2)]
+  val state =
+    { binders = []
+    , functions = functions
+    , constants = constants
+    , relations = relations
+    }
 
   fun parse_repl s =
     let
       val toks = scan {input = s, srcname = "repl"}
     in
       case parse state toks of
-        OK (t, _, []) => print ("Parsed successfully: " ^ Term.ppd 2 t ^ "\n")
+        OK (t, _, []) => print ("Parsed successfully: " ^ Formula.pp t ^ "\n")
       | OK (t, r, rest) =>
           print
-            ("Parsed '" ^ Term.ppd 2 t ^ "' up to " ^ Region.pp r ^ ", but "
+            ("Parsed '" ^ Formula.pp t ^ "' up to " ^ Region.pp r ^ ", but "
              ^ Int.toString (length rest) ^ " tokens remain unparsed\n")
       | NO (r, err) => print ("ERROR: " ^ Region.ppLoc r ^ ", " ^ err () ^ "\n")
     end
@@ -32,7 +37,7 @@ end
 fun repl () =
   ( print "> "
   ; case (TextIO.inputLine TextIO.stdIn) of
-      SOME s => (TermTesting.parse_repl s; repl ())
+      SOME s => (Testing.parse_repl s; repl ())
     | NONE => ()
   )