scanner works

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

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

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

@@ -0,0 +1,61 @@
+structure Scanner: SCANNER =
+struct
+  open SimpleToken
+
+  datatype token =
+    LPAREN
+  | RPAREN
+  | AND
+  | OR
+  | EQ
+  | RARROW
+  | LRARROW
+  | DOT
+  | COMMA
+  | FORALL
+  | EXISTS
+  | IDENT of string
+  | ERR
+
+  fun map_token (Symb "(") = LPAREN
+    | map_token (Symb ")") = RPAREN
+    | map_token (Symb ".") = DOT
+    | map_token (Symb ",") = COMMA
+    | map_token (Symb "&") = AND
+    | map_token (Symb "|") = OR
+    | map_token (Symb "=") = EQ
+    | map_token (Symb "=>") = RARROW
+    | map_token (Symb "<=>") = LRARROW
+    | map_token (Symb _) = ERR
+    | map_token (Id "forall") = FORALL
+    | map_token (Id "exists") = EXISTS
+    | map_token (Id id) = IDENT id
+    | map_token (Num _) = ERR
+
+  fun const k _ = k
+
+  val scan =
+    map (fn (t, r) => (map_token t, r))
+    o
+    tokenise
+      { sep_chars = "(),&|."
+      , symb_chars = "<=>"
+      , is_id = (List.all Char.isAlphaNum) o String.explode
+      , is_num = const false
+      }
+
+  val pp_token =
+    fn LPAREN => "("
+     | RPAREN => ")"
+     | AND => "&"
+     | OR => "|"
+     | EQ => "="
+     | RARROW => "=>"
+     | LRARROW => "<=>"
+     | DOT => "."
+     | COMMA => ","
+     | FORALL => "forall"
+     | EXISTS => "exists"
+     | ERR => "unk"
+     | IDENT s => s
+end

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

@@ -1,3 +1,8 @@
 $(SML_LIB)/basis/basis.mlb
+../kernel/kernel.mlb
 ../../../../github.com/diku-dk/sml-parse/parse.mlb
 ../../../../github.com/diku-dk/sml-parse/simple_token.mlb
+SCANNER.sig
+Scanner.sml
+
+repl.sml

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

@@ -0,0 +1,16 @@
+open Scanner
+
+fun scan_repl s = scan {srcname = "repl", input = s}
+
+fun report_scan s = print ((String.concatWith ", " (map (pp_token o #1) (scan_repl s))) ^ "\n")
+
+fun repl () =
+  ( print "> "
+  ; case (TextIO.inputLine TextIO.stdIn) of
+      SOME s => (report_scan s; repl ())
+    | NONE => ()
+  )
+
+fun main () = repl ()
+
+(* val () = main () *)