(** 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 list;
      (** For a recursive rule, the lexicographic measure of its
          call-graph component: at some position the recursive
          argument strictly decreases, all earlier positions staying
          equal. The VM requires every position ground before
          unfolding, which is what turns the admission proof into
          runtime termination. Empty 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. *)

val member_of_primitive : Term.t -> primitive -> bool
(** Host-decided membership in a primitive domain, with the literal
    inclusions of decision 12. Exposed so stateful worlds check
    schemas with exactly the loader's judgment. *)

(** What a transition relation says when consulted (decision 3:
    transitions are relations over states, provided by the world,
    never by the engine). *)
type transition_result =
  | T_state of Term.t
      (** The successor state; the VM unifies it with [after:]. *)
  | T_fail  (** No such transition: integrity violation and kin. *)
  | T_stuck  (** Arguments not ground yet; the planner defers. *)

(** What a host must answer for the VM to run: which relation lives
    under a name, optionally at a state ([at:] reads, decision 7),
    and which names are transition relations. Builtins are the VM's
    own and are not consulted here. The standalone world has one
    implicit state and no transitions (decision 5). *)
module type WORLD = sig
  type t

  val find : t -> ?at:Term.t -> string -> def option

  val transition :
    t -> string -> Pattern.t Label.Map.t -> transition_result option
  (** [None] when the name is not a transition relation of this
      world. Bindings arrive resolved. *)
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 -> ?at:Term.t -> string -> def option
  (** [at:] is accepted and ignored: the standalone world is its own
      single, eternal state. *)

  val transition : t -> string -> Pattern.t Label.Map.t -> transition_result option
  (** Always [None]: no branches, no transitions, the pure
      fragment. *)

  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