From 5836cbe2f4aa597e9bfb6229ce363b66b587714b Mon Sep 17 00:00:00 2001
From: William Ball <williampi103@gmail.com>
Date: Mon, 12 Aug 2024 01:03:31 -0700
Subject: [PATCH] scanner works

---
 .../wball/proof-checker/parser/SCANNER.sig    | 20 ++++++
 .../wball/proof-checker/parser/Scanner.sml    | 61 +++++++++++++++++++
 .../wball/proof-checker/parser/parser.mlb     |  5 ++
 .../wball/proof-checker/parser/repl.sml       | 16 +++++
 4 files changed, 102 insertions(+)
 create mode 100644 lib/forgejo.ballcloud.cc/wball/proof-checker/parser/SCANNER.sig
 create mode 100644 lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Scanner.sml
 create mode 100644 lib/forgejo.ballcloud.cc/wball/proof-checker/parser/repl.sml

diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/SCANNER.sig b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/SCANNER.sig
new file mode 100644
index 0000000..6532085
--- /dev/null
+++ b/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
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Scanner.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Scanner.sml
new file mode 100644
index 0000000..7ee94cb
--- /dev/null
+++ b/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
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/parser.mlb b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/parser.mlb
index 2c35957..881c0a0 100644
--- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/parser.mlb
+++ b/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
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/repl.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/repl.sml
new file mode 100644
index 0000000..3adf621
--- /dev/null
+++ b/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 () *)