working vm: parser, admission with totality checks, solver and repl

1 files changed, 54 insertions, 0 deletions

diff --git a/lib/lexer.mll b/lib/lexer.mll
new file mode 100644
index 0000000..53ef04a
--- /dev/null
+++ b/lib/lexer.mll
@@ -0,0 +1,54 @@
+{
+open Parser
+
+exception Error of string
+
+let unescape s =
+  let buffer = Buffer.create (String.length s) in
+  let rec go i =
+    if i < String.length s then
+      match s.[i] with
+      | '\\' when i + 1 < String.length s ->
+          (match s.[i + 1] with
+           | 'n' -> Buffer.add_char buffer '\n'
+           | 't' -> Buffer.add_char buffer '\t'
+           | c -> Buffer.add_char buffer c);
+          go (i + 2)
+      | c ->
+          Buffer.add_char buffer c;
+          go (i + 1)
+  in
+  go 0;
+  Buffer.contents buffer
+}
+
+let digit = ['0'-'9']
+let ident = ['A'-'Z' 'a'-'z'] ['A'-'Z' 'a'-'z' '0'-'9' '_']*
+let string_body = ([^ '"' '\\'] | '\\' _)*
+
+rule token = parse
+  | [' ' '\t' '\r' '\n']+     { token lexbuf }
+  | '%' [^ '\n']*             { token lexbuf }
+  | "#("                      { HASH_LPAREN }
+  | '('                       { LPAREN }
+  | ')'                       { RPAREN }
+  | '['                       { LBRACKET }
+  | ']'                       { RBRACKET }
+  | '{'                       { LBRACE }
+  | '}'                       { RBRACE }
+  | '|'                       { BAR }
+  | ":and"                    { AND }
+  | ":or"                     { OR }
+  | '-'? digit+ '/' digit+ as s
+      { match String.index_opt s '/' with
+        | Some i ->
+            RAT
+              ( Z.of_string (String.sub s 0 i),
+                Z.of_string (String.sub s (i + 1) (String.length s - i - 1)) )
+        | None -> assert false }
+  | '-'? digit+ as s          { INT (Z.of_string s) }
+  | (ident as name) ':'       { LABEL name }
+  | ident as name             { NAME name }
+  | '"' (string_body as s) '"' { STR (unescape s) }
+  | eof                       { EOF }
+  | _ as c                    { raise (Error (Printf.sprintf "unexpected character %C" c)) }