parsing terms!

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

@@ -0,0 +1,6 @@
+signature PARSER =
+sig
+  type result
+  type state
+  val parse : state -> result ParseUtils.p
+end

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

@@ -0,0 +1,2 @@
+structure ParseUtils =
+  Parse (type token = Scanner.token val pp_token = Scanner.pp_token)

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

@@ -0,0 +1,44 @@
+structure TermParser: PARSER =
+struct
+  type result = Term.t
+
+  structure StringSet = Utils.StringSet
+  structure ArityMap = Utils.ArityMap
+
+  type state =
+    {binders: string list, constants: StringSet.t, functions: ArityMap.t}
+
+  open ParseUtils
+  infix >>> ->> >>- ?? ??? || oo oor ??*
+
+  open Term
+  open Scanner
+
+  fun parse {binders = binders, constants = constants, functions = functions} =
+    let
+      fun term_p nil =
+            NO (Region.botloc, fn () =>
+              "expecting identifier but reached the end")
+        | term_p ((Scanner.IDENT id, r) :: rest) =
+            (case Utils.findIndex (id, binders) of
+               SOME i => OK (Var i, r, rest)
+             | NONE =>
+                 if StringSet.member (constants, id) then
+                   OK (Const id, r, rest)
+                 else if ArityMap.member (functions, id) then
+                   (args_p oo (fn args => Function (id, rev args))) rest
+                 else
+                   OK (Free id, r, rest))
+        | term_p ((t, r) :: rest) =
+            NO (#1 r, fn () =>
+              "expecting variable but found token " ^ pp_token t)
+
+      and args_p ts =
+        (eat LPAREN
+         ->>
+         ((term_p oo (fn x => [x])) ??* (eat COMMA ->> term_p))
+           (Utils.flip op::) >>- eat RPAREN) ts
+    in
+      term_p
+    end
+end

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

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

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

@@ -1,16 +1,39 @@
 open Scanner
 
-fun scan_repl s = scan {srcname = "repl", input = s}
+structure TermTesting:
+sig
+  val parse_repl: string -> unit
+end =
+struct
+  open TermParser
+  open Utils
+  open ParseUtils
+  open Scanner
 
-fun report_scan s = print ((String.concatWith ", " (map (pp_token o #1) (scan_repl s))) ^ "\n")
+  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}
+
+  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, r, rest) =>
+          print
+            ("Parsed '" ^ Term.ppd 2 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
+end
 
 fun repl () =
   ( print "> "
   ; case (TextIO.inputLine TextIO.stdIn) of
-      SOME s => (report_scan s; repl ())
+      SOME s => (TermTesting.parse_repl s; repl ())
     | NONE => ()
   )
 
-fun main () = repl ()
+fun main () = repl () (* val () = main () *)
-
-(* val () = main () *)

lib/forgejo.ballcloud.cc/wball/proof-checker/utils/MAP.sig

@@ -0,0 +1,13 @@
+signature MAP =
+sig
+  type key
+  type value
+  type t
+
+  val empty: t
+  val insert: t * key * value -> t
+  val member: t * key -> bool
+  val get: t * key -> value option
+  val fromList: (key * value) list -> t
+  val toList: t -> (key * value) list
+end

lib/forgejo.ballcloud.cc/wball/proof-checker/utils/Map.sml

@@ -0,0 +1,39 @@
+functor Map (structure Ord: ORD type value) :> MAP
+                                               where type key = Ord.t
+                                               and type value = value =
+struct
+  type key = Ord.t
+  type value = value
+  datatype t = Leaf | Node of t * key * value * t
+
+  val empty = Leaf
+
+  fun insert (Leaf, x, v) = Node (Leaf, x, v, Leaf)
+    | insert (s as Node (left, y, u, right), x, v) =
+        case Ord.compare (x, y) of
+          LESS => Node (insert (left, x, v), y, u, right)
+        | EQUAL => s
+        | GREATER => Node (left, y, u, insert (right, x, v))
+
+  fun member (Leaf, _) = false
+    | member (Node (left, y, _, right), x) =
+        case Ord.compare (x, y) of
+          LESS => member (left, x)
+        | EQUAL => true
+        | GREATER => member (right, x)
+
+  fun get (Leaf, _) = NONE
+    | get (Node (left, y, v, right), x) =
+        case Ord.compare (x, y) of
+          LESS => get (left, x)
+        | EQUAL => SOME v
+        | GREATER => get (right, x)
+
+  fun fromList [] = Leaf
+    | fromList ((x, v) :: xs) =
+        insert (fromList xs, x, v)
+
+  fun toList Leaf = []
+    | toList (Node (left, x, v, right)) =
+        toList left @ ((x, v) :: toList right)
+end

lib/forgejo.ballcloud.cc/wball/proof-checker/utils/ORD.sig

@@ -0,0 +1,5 @@
+signature ORD =
+sig
+  type t
+  val compare: t * t -> order
+end

lib/forgejo.ballcloud.cc/wball/proof-checker/utils/Ord.sml

@@ -0,0 +1,4 @@
+structure IntOrd: ORD = struct type t = int val compare = Int.compare end
+
+structure StringOrd: ORD =
+struct type t = string val compare = String.compare end

lib/forgejo.ballcloud.cc/wball/proof-checker/utils/SET.sig

@@ -0,0 +1,11 @@
+signature SET =
+sig
+  type elem
+  type t
+
+  val empty: t
+  val insert: t * elem -> t
+  val member: t * elem -> bool
+  val fromList: elem list -> t
+  val toList: t -> elem list
+end

lib/forgejo.ballcloud.cc/wball/proof-checker/utils/Set.sml

@@ -0,0 +1,29 @@
+functor Set(Ord: ORD) :> SET where type elem = Ord.t =
+struct
+  type elem = Ord.t
+  datatype t = Leaf | Node of t * elem * t
+
+  val empty = Leaf
+
+  fun insert (Leaf, x) = Node (Leaf, x, Leaf)
+    | insert (s as Node (left, y, right), x) =
+        case Ord.compare (x, y) of
+          LESS => Node (insert (left, x), y, right)
+        | EQUAL => s
+        | GREATER => Node (left, y, insert (right, x))
+
+  fun member (Leaf, _) = false
+    | member (Node (left, y, right), x) =
+        case Ord.compare (x, y) of
+          LESS => member (left, x)
+        | EQUAL => true
+        | GREATER => member (right, x)
+
+  fun fromList [] = Leaf
+    | fromList (x :: xs) =
+        insert (fromList xs, x)
+
+  fun toList Leaf = []
+    | toList (Node (left, x, right)) =
+        toList left @ (x :: toList right)
+end

lib/forgejo.ballcloud.cc/wball/proof-checker/utils/UTILS.sig

@@ -0,0 +1,9 @@
+signature UTILS =
+sig
+  val const: 'a -> 'b -> 'a
+  val flip: ('a * 'b -> 'c) -> ('b * 'a -> 'c)
+  val findIndex: ''a * ''a list -> int option
+
+  structure StringSet: SET where type elem = string
+  structure ArityMap: MAP where type key = string and type value = int
+end

lib/forgejo.ballcloud.cc/wball/proof-checker/utils/Utils.sml

@@ -0,0 +1,16 @@
+structure Utils: UTILS =
+struct
+  fun const k _ = k
+
+  fun flip f =
+    fn (b, a) => f (a, b)
+
+  fun findIndex' (_, [], _) = NONE
+    | findIndex' (y, (x :: xs), acc) =
+        if x = y then SOME acc else findIndex' (y, xs, acc + 1)
+
+  fun findIndex (x, xs) = findIndex' (x, xs, 0)
+
+  structure StringSet = Set(StringOrd)
+  structure ArityMap = Map (structure Ord = StringOrd type value = int)
+end

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

@@ -0,0 +1,9 @@
+$(SML_LIB)/basis/basis.mlb
+ORD.sig
+Ord.sml
+SET.sig
+Set.sml
+MAP.sig
+Map.sml
+UTILS.sig
+Utils.sml