(** 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
  | Ref of string  (** [#Name], a relation reference *)
  | 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