|
|
(** 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. *)
(** 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
|
