blob: 61ca7872b822527d750b7a1f3556bdeeed3aadca (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
(** 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
| Not of node * node
(** [u :not d]: within the universe [u], deny [d]. *)
(** 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
|
