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

1 files changed, 25 insertions, 0 deletions

diff --git a/lib/ast.ml b/lib/ast.ml
new file mode 100644
index 0000000..9674664
--- /dev/null
+++ b/lib/ast.ml
@@ -0,0 +1,25 @@
+(** Surface syntax tree.
+
+    The parser produces one uniform node category. Atoms and
+    variables share a spelling in Sol and are distinguished by
+    context, so classification (proposition or term, relation or
+    variable) belongs to the loader, not the grammar. *)
+
+type node =
+  | Name of string  (** identifier; variable or relation, by context *)
+  | Int of Z.t
+  | Rat of Z.t * Z.t  (** one token, [1/4]; normalized at loading *)
+  | Str of string
+  | Record of (string * node) list  (** [{l: n ...}], source order *)
+  | Seq of node list * node option  (** [#(a b)], optional [| tail] *)
+  | Block of string * (string * node) list  (** [[Rel l: n ...]] *)
+  | And of node * node
+  | Or of node * node
+
+(** A program is a list of statements. A bare block asserts a fact;
+    a directive is a top-level message send such as
+    [Relation named: ... schema: ...], [Rule name: ... head: ...
+    body: ...], or [Query expression: ...]. *)
+type statement =
+  | Directive of string * (string * node) list
+  | Assert of node