(** Worlds: the store of relations, and the loader that builds the
    standalone one.

    Decision 4 of the integration document: the VM is parameterized
    over a world. This module gives the module type every host
    satisfies, the standalone in-memory world, and the loader that
    admits a parsed program into it. Admission is where totality is
    enforced: a program that gets a world is a program whose queries
    terminate. *)

(** A compiled relational expression: what rule bodies and queries
    are made of after names are resolved. [Exists] is lowered away
    at loading: its variable is renamed apart and the form becomes a
    conjunction. *)
type expr =
  | Apply of string * Pattern.t Label.Map.t
  | And of expr * expr
  | Or of expr * expr
  | Not of expr * expr
      (** [u :not d]: the universe holds and the denial has no
          solutions. Decidable negation only: the VM runs the denial
          once its variables are ground. *)
  | Forall of expr * expr
      (** Every solution of the quantifier satisfies the body. The
          VM runs it when the quantifier is decidable, which keeps
          universals off infinite domains. *)

type rule = {
  rule_name : string;
  head : Pattern.t Label.Map.t;
  body : expr;
  witness : Label.t option;
      (** For a recursive rule, the label whose argument strictly
          decreases. The VM requires it ground before unfolding,
          which is what turns the admission proof into runtime
          termination. [None] on non-recursive rules. *)
}

(** The primitive host-checked domains. *)
type primitive = D_integer | D_natural | D_rational | D_string

(** What a schema constrains an attribute by: a primitive domain, or
    a membership criterion, an arbitrary relational expression with
    exactly one free variable, the subject, bound to the attribute
    value at admission. Foreign keys are the criterion
    [([Department id: D])], nothing more special than that. *)
type domain =
  | Primitive of primitive
  | Criterion of { subject : string; body : expr }

(** How a relation is defined. *)
type def =
  | Table of { schema : (Label.t * domain) list; facts : Term.t Label.Map.t list }
      (** Extensional: a schema and finite stored tuples. *)
  | Rules of rule list  (** Intensional: defined by admitted rules. *)

(** What a host must answer for the VM to run: which relation lives
    under a name. Builtins are the VM's own and are not consulted
    here. *)
module type WORLD = sig
  type t

  val find : t -> string -> def option
end

type error

val pp_error : Format.formatter -> error -> unit

(** A fact attribute awaiting a criterion check. The loader cannot
    run the solver (the solver sits above it), so criterion
    admission is finished by {!Program}, against the fully loaded
    world. *)
type pending = {
  pending_relation : string;
  pending_label : Label.t;
  pending_body : expr;
      (** The criterion with its subject already bound to the
          attribute value; admissible iff it has a solution. *)
}

val expr_of_node : Ast.node -> (expr, error) result
(** Compiles one surface expression: names resolve by context,
    [Exists] lowers, quantified variables rename apart. This is the
    embedding hosts' way in: they compile queries themselves and
    answer for their own relations, so no standalone reference
    checking happens here. *)

(** The standalone world: an immutable catalog loaded from program
    text. This is Sol as a separate language; there are no branches,
    no transitions, only the pure fragment. *)
module Standalone : sig
  type t

  val find : t -> string -> def option

  val load : Ast.statement list -> (t * expr list * pending list, error) result
  (** Admits a program: registers relations, checks every fact
      against its schema and primitive domains, compiles rules and
      queries, and enforces totality. Rejected, not deferred: a
      recursive rule without a structural decrease witness, a mutual
      recursion cycle, an unknown relation, or an ill-typed fact is
      an [error], and no world exists. Returns the world, the query
      expressions in program order, and the criterion checks for
      {!Program} to finish. *)
end