reorganization in preparation for ProofParser

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

@@ -15,25 +15,20 @@ struct
   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
 
-  exception NotOperator of token
+  exception NotOperator of Token.t
 
   val infix_table =
-    fn AND => (40, 41, Conj)
+    fn Token.AND => (40, 41, Conj)
-     | OR => (30, 31, Disj)
+     | Token.OR => (30, 31, Disj)
-     | RARROW => (21, 20, Impl)
+     | Token.RARROW => (21, 20, Impl)
-     | LRARROW => (10, 10, Iff)
+     | Token.LRARROW => (10, 10, Iff)
      | t => (100, 100, fn _ => raise NotOperator t)
 
   val prefix_table =
-    fn NEG => ((), 50, Neg) | t => ((), 100, fn _ => raise NotOperator t)
+    fn Token.NEG => ((), 50, Neg) | t => ((), 100, fn _ => raise NotOperator t)
 
   exception NotOperator
 
@@ -53,20 +48,20 @@ struct
       fun parse_full ts = parse state ts
 
       fun equal_p ts =
-        ((term_p >>- eat EQ >>> term_p) oo Equal) ts
+        ((term_p >>- eat Token.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 ((Token.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)
+              "expecting identifier but found token " ^ Token.pp_token t)
 
-      val bottom_p = eat HASH oo (fn () => Bottom)
+      val bottom_p = eat Token.HASH oo (fn () => Bottom)
 
       fun forall_p ts =
-        ((eat FORALL ->> ident_p >>- eat DOT)
+        ((eat (Token.KEYWORD Token.Forall) ->> ident_p >>- eat Token.DOT)
          >>=
          (fn id =>
             parse
@@ -77,7 +72,7 @@ struct
               } oo Forall)) ts
 
       fun exists_p ts =
-        ((eat EXISTS ->> ident_p >>- eat DOT)
+        ((eat (Token.KEYWORD Token.Exists) ->> ident_p >>- eat Token.DOT)
          >>=
          (fn id =>
             parse
@@ -88,19 +83,19 @@ struct
               } oo Exists)) ts
 
       fun args_p ts =
-        (eat LPAREN
+        (eat Token.LPAREN
          ->>
-         ((term_p oo (fn x => [x])) ??* (eat COMMA ->> term_p))
+         ((term_p oo (fn x => [x])) ??* (eat Token.COMMA ->> term_p))
-           (Utils.flip op::) >>- eat RPAREN) ts
+           (Utils.flip op::) >>- eat Token.RPAREN) ts
 
-      fun relation_p ((Scanner.IDENT id, r) :: rest) =
+      fun relation_p ((Token.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)
+              "expected identifier but found token " ^ Token.pp_token t)
         | relation_p [] =
             NO (Region.botloc, fn () =>
               "expecting identifier but reached the end")
@@ -112,7 +107,7 @@ struct
 
       fun atomic_p ts =
         (equal_p || bottom_p || relation_p || forall_p || exists_p
-         || (eat LPAREN ->> formula_p 0 >>- eat RPAREN)) ts
+         || (eat Token.LPAREN ->> formula_p 0 >>- eat Token.RPAREN)) ts
 
       and formula_p mprec [] =
             NO (Region.botloc, fn () => "expecting formula but reached the end")
@@ -120,7 +115,7 @@ struct
             let
               (* get first term atomic or prefix *)
               val (lhs, r, rest') = unwrap
-                (if prefix_connective t then
+                (if Token.prefix_connective t then
                    let val ((), rp, comb) = prefix_table t
                    in (formula_p rp oo comb) rest
                    end
@@ -130,7 +125,7 @@ struct
               (* loop through the rest while the precedence is high enough *)
               fun loop (lhs, r, []) = OK (lhs, r, [])
                 | loop (lhs, r, ts as (t, _) :: rest) =
-                    if infix_connective t then
+                    if Token.infix_connective t then
                       let
                         val (lp, rp, comb) = infix_table t
                       in

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

@@ -1,2 +1,19 @@
-structure ParseUtils =
+signature PARSEUTILS =
-  Parse (type token = Scanner.token val pp_token = Scanner.pp_token)
+sig
+  include PARSE
+  val >>= : 'a p * ('a -> 'b p) -> 'b p
+end
+
+structure ParseUtils: PARSEUTILS =
+struct
+  structure ParseUtilsTemp =
+    Parse (type token = Token.t val pp_token = Token.pp_token)
+  open ParseUtilsTemp
+
+  infix >>=
+
+  fun (p >>= q) ts =
+    case p ts of
+      OK (v, r, ts') => q v ts'
+    | NO e => NO e
+end

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

@@ -1,25 +1,4 @@
 signature SCANNER =
 sig
-  datatype token =
+  val scan: {srcname: string, input: string} -> (Token.t * Region.reg) list
-    LPAREN
-  | RPAREN
-  | NEG
-  | AND
-  | OR
-  | EQ
-  | RARROW
-  | LRARROW
-  | DOT
-  | COMMA
-  | HASH
-  | FORALL
-  | EXISTS
-  | IDENT of string
-  | ERR
-
-  val scan: {srcname: string, input: string} -> (token * Region.reg) list
-  val pp_token: token -> string
-
-  val infix_connective: token -> bool
-  val prefix_connective: token -> bool
 end

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

@@ -1,23 +1,7 @@
 structure Scanner: SCANNER =
 struct
   open SimpleToken
-
+  open Token
-  datatype token =
-    LPAREN
-  | RPAREN
-  | NEG
-  | AND
-  | OR
-  | EQ
-  | RARROW
-  | LRARROW
-  | DOT
-  | COMMA
-  | HASH
-  | FORALL
-  | EXISTS
-  | IDENT of string
-  | ERR
 
   fun map_token (Symb "(") = LPAREN
     | map_token (Symb ")") = RPAREN
@@ -31,9 +15,10 @@ struct
     | map_token (Symb "=>") = RARROW
     | map_token (Symb "<=>") = LRARROW
     | map_token (Symb _) = ERR
-    | map_token (Id "forall") = FORALL
+    | map_token (Id id) =
-    | map_token (Id "exists") = EXISTS
+        (case KeywordMap.get (keywordMap, id) of
-    | map_token (Id id) = IDENT id
+           SOME keyword => KEYWORD keyword
+         | NONE => IDENT id)
     | map_token (Num _) = ERR
 
   fun const k _ = k
@@ -47,26 +32,4 @@ struct
       , is_id = (List.all Char.isAlphaNum) o String.explode
       , is_num = const false
       }
-
-  val pp_token =
-    fn LPAREN => "("
-     | RPAREN => ")"
-     | NEG => "~"
-     | AND => "&"
-     | OR => "|"
-     | EQ => "="
-     | RARROW => "=>"
-     | LRARROW => "<=>"
-     | DOT => "."
-     | COMMA => ","
-     | FORALL => "forall"
-     | EXISTS => "exists"
-     | ERR => "unk"
-     | HASH => "#"
-     | IDENT s => s
-
-  val infix_connective =
-    fn AND => true | OR => true | RARROW => true | LRARROW => true | _ => false
-
-  val prefix_connective = fn NEG => true | _ => false
 end

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

@@ -0,0 +1,51 @@
+signature TOKEN =
+sig
+  datatype keyword =
+  (* labels *)
+    Axiom
+  | AndI
+  | AndE
+  | OrI
+  | OrE
+  | ArrI
+  | ArrE
+  | NegI
+  | NegE
+  | RAA
+  | IffI
+  | IffE
+  | EqI
+  | EqE
+  | ForallI
+  | ForallE
+  | ExistsI
+  | ExistsE
+
+  (* formulas *)
+  | Forall
+  | Exists
+
+  structure KeywordMap: MAP where type key = string and type value = keyword
+  val keywordMap: KeywordMap.t
+
+  datatype t =
+    LPAREN
+  | RPAREN
+  | NEG
+  | AND
+  | OR
+  | EQ
+  | RARROW
+  | LRARROW
+  | DOT
+  | COMMA
+  | HASH
+  | KEYWORD of keyword
+  | IDENT of string
+  | ERR
+
+  val pp_token: t -> string
+
+  val infix_connective: t -> bool
+  val prefix_connective: t -> bool
+end

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

@@ -19,7 +19,7 @@ struct
       fun term_p nil =
             NO (Region.botloc, fn () =>
               "expecting identifier but reached the end")
-        | term_p ((Scanner.IDENT id, r) :: rest) =
+        | term_p ((Token.IDENT id, r) :: rest) =
             (case Utils.findIndex (id, binders) of
                SOME i => OK (Var i, r, rest)
              | NONE =>
@@ -31,13 +31,13 @@ struct
                    OK (Free id, r, rest))
         | term_p ((t, r) :: rest) =
             NO (#1 r, fn () =>
-              "expecting variable but found token " ^ pp_token t)
+              "expecting variable but found token " ^ Token.pp_token t)
 
       and args_p ts =
-        (eat LPAREN
+        (eat Token.LPAREN
          ->>
-         ((term_p oo (fn x => [x])) ??* (eat COMMA ->> term_p))
+         ((term_p oo (fn x => [x])) ??* (eat Token.COMMA ->> term_p))
-           (Utils.flip op::) >>- eat RPAREN) ts
+           (Utils.flip op::) >>- eat Token.RPAREN) ts
     in
       term_p
     end

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

@@ -0,0 +1,86 @@
+structure Token: TOKEN =
+struct
+  datatype keyword =
+    Axiom
+  | AndI
+  | AndE
+  | OrI
+  | OrE
+  | ArrI
+  | ArrE
+  | NegI
+  | NegE
+  | RAA
+  | IffI
+  | IffE
+  | EqI
+  | EqE
+  | ForallI
+  | ForallE
+  | ExistsI
+  | ExistsE
+  | Forall
+  | Exists
+
+  datatype t =
+    LPAREN
+  | RPAREN
+  | NEG
+  | AND
+  | OR
+  | EQ
+  | RARROW
+  | LRARROW
+  | DOT
+  | COMMA
+  | HASH
+  | KEYWORD of keyword
+  | IDENT of string
+  | ERR
+
+  structure KeywordMap = Map (structure Ord = StringOrd type value = keyword)
+  val keywordMap = KeywordMap.fromList
+    [ ("Axiom", Axiom)
+    , ("AndI", AndI)
+    , ("AndE", AndE)
+    , ("OrI", OrI)
+    , ("OrE", OrE)
+    , ("ArrI", ArrI)
+    , ("ArrE", ArrE)
+    , ("NegI", NegI)
+    , ("NegE", NegE)
+    , ("RAA", RAA)
+    , ("IffI", IffI)
+    , ("IffE", IffE)
+    , ("EqI", EqI)
+    , ("EqE", EqE)
+    , ("ForallI", ForallI)
+    , ("ForallE", ForallE)
+    , ("ExistsI", ExistsI)
+    , ("ExistsE", ExistsE)
+    , ("Forall", Forall)
+    , ("Exists", Exists)
+    ]
+
+  val pp_token =
+    fn LPAREN => "("
+     | RPAREN => ")"
+     | NEG => "~"
+     | AND => "&"
+     | OR => "|"
+     | EQ => "="
+     | RARROW => "=>"
+     | LRARROW => "<=>"
+     | DOT => "."
+     | COMMA => ","
+     | FORALL => "forall"
+     | EXISTS => "exists"
+     | ERR => "unk"
+     | HASH => "#"
+     | IDENT s => s
+
+  val infix_connective =
+    fn AND => true | OR => true | RARROW => true | LRARROW => true | _ => false
+
+  val prefix_connective = fn NEG => true | _ => false
+end

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

@@ -3,6 +3,8 @@ $(SML_LIB)/basis/basis.mlb
 ../utils/utils.mlb
 ../../../../github.com/diku-dk/sml-parse/parse.mlb
 ../../../../github.com/diku-dk/sml-parse/simple_token.mlb
+TOKEN.sig
+Token.sml
 SCANNER.sig
 Scanner.sml
 ParseUtils.sml