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

1 files changed, 52 insertions, 0 deletions

diff --git a/lib/parser.mly b/lib/parser.mly
new file mode 100644
index 0000000..c85eccc
--- /dev/null
+++ b/lib/parser.mly
@@ -0,0 +1,52 @@
+%{
+open Ast
+%}
+
+%token <Z.t> INT
+%token <Z.t * Z.t> RAT
+%token <string> STR
+%token <string> NAME
+%token <string> LABEL
+%token LBRACKET RBRACKET LBRACE RBRACE LPAREN RPAREN HASH_LPAREN
+%token BAR AND OR EOF
+
+%start <Ast.statement list> program
+
+%%
+
+program:
+  | statements = list(statement); EOF { statements }
+
+statement:
+  | head = NAME; args = nonempty_list(binding) { Directive (head, args) }
+  | b = block                                  { Assert b }
+
+binding:
+  | label = LABEL; value = node { (label, value) }
+
+(* :or binds looser than :and; both associate to the left. The
+   grouping form is ordinary parentheses. *)
+node:
+  | left = node; OR; right = conjunction { Or (left, right) }
+  | conj = conjunction                   { conj }
+
+conjunction:
+  | left = conjunction; AND; right = operand { And (left, right) }
+  | operand = operand                        { operand }
+
+operand:
+  | b = block                     { b }
+  | name = NAME                   { Name name }
+  | n = INT                       { Int n }
+  | r = RAT                       { Rat (fst r, snd r) }
+  | s = STR                       { Str s }
+  | LBRACE; fields = nonempty_list(binding); RBRACE { Record fields }
+  | HASH_LPAREN; items = list(operand); tail = option(seq_tail); RPAREN
+      { Seq (items, tail) }
+  | LPAREN; n = node; RPAREN      { n }
+
+seq_tail:
+  | BAR; tail = operand { tail }
+
+block:
+  | LBRACKET; head = NAME; args = list(binding); RBRACKET { Block (head, args) }