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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
(** 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
|
