From c530682030e80ee2de2c263471e5eda7a3392e84 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 03:07:56 -0300 Subject: working vm: parser, admission with totality checks, solver and repl --- lib/ast.ml | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 lib/ast.ml (limited to 'lib/ast.ml') 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 -- cgit v1.2.3