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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
|
(** 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. *)
}
(** 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
|
