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
|
(** The branch world: the reference stateful host.
This is the RNT-shaped world of decisions 3, 5, 7 and 8, in
miniature: states are whole content-addressed trees, a state
value is its digest, reads are state-scoped, [Insert] is a
transition relation between states, and the single effect is
compare-and-swap on a branch tip. The store is append-only;
everything else is pure value manipulation.
The digest is a canonical-serialization hash (a placeholder for
RNT's SHA256 content addressing; same shape, weaker hash). *)
type t
val create : schemas:(string * (Label.t * World.primitive) list) list -> t
(** A world with the given catalog, an empty root state, and one
branch, ["main"], whose tip is the root. The catalog is fixed at
creation; DDL-as-transition comes with the full catalog work. *)
val find : t -> ?at:Term.t -> string -> World.def option
(** State-scoped read. [at:] is the state digest (as a string
term); omitted, the read sees the ["main"] tip, which is the
REPL elaboration rule of decision 7. *)
val transition : t -> string -> Pattern.t Label.Map.t -> World.transition_result option
(** [Insert relation: "R" tuple: {...} before: S after: S']: checks
the tuple against the relation's schema (integrity at the
transition, decision 3), stores the successor state, and
returns its digest for the VM to unify with [after:]. Stuck
until [relation:], [tuple:] and [before:] are ground. *)
val tip : t -> string -> Term.t option
(** The branch's current state digest. *)
val commit :
t -> branch:string -> expect:Term.t -> next:Term.t -> (unit, [ `Conflict ]) result
(** The single effect (decisions 3 and 8): install [next] as the
tip iff the tip still equals [expect]. Everything above this
primitive is DCL's business. *)
val linear : World.expr -> (unit, string) result
(** The linearity discipline of decision 6, checked before running:
no state variable is consumed twice (two [before:] uses) or
produced twice (two [after:] uses) across the expression's
transition applications. Forks are DCL's to express, not a
query's. *)
|
