branch world: state scoped reads, insert transitions, tip commit

5 files changed, 291 insertions, 9 deletions

diff --git a/lib/branch.ml b/lib/branch.ml
new file mode 100644
index 0000000..a1382c6
--- /dev/null
+++ b/lib/branch.ml
@@ -0,0 +1,162 @@
+module String_map = Map.Make (String)
+
+type state = Term.t Label.Map.t list String_map.t
+(* relation name -> stored tuples, the whole tree of one state *)
+
+type t = {
+  schemas : (Label.t * World.primitive) list String_map.t;
+  states : (string, state) Hashtbl.t;  (* digest -> state; append-only *)
+  mutable tips : (string * string) list;  (* branch -> digest; the one mutable place *)
+}
+
+let forced_label name =
+  match Label.of_string name with Ok l -> l | Error _ -> assert false
+
+let relation_l = forced_label "relation"
+let tuple_l = forced_label "tuple"
+let before_l = forced_label "before"
+let after_l = forced_label "after"
+
+(* Canonical serialization: relations in name order (the map gives
+   it), tuples in term order, printed in canonical notation. Equal
+   states digest equally because terms are canonical by
+   construction. *)
+let digest_of_state (state : state) =
+  let buffer = Buffer.create 256 in
+  String_map.iter
+    (fun name tuples ->
+      Buffer.add_string buffer name;
+      let terms =
+        List.map (fun tuple -> Term.record (Label.Map.bindings tuple)) tuples
+        |> List.filter_map Result.to_option
+        |> List.sort Term.compare
+      in
+      List.iter
+        (fun term -> Buffer.add_string buffer (Format.asprintf "|%a" Term.pp term))
+        terms;
+      Buffer.add_char buffer '\n')
+    state;
+  Digest.to_hex (Digest.string (Buffer.contents buffer))
+
+let store world state =
+  let digest = digest_of_state state in
+  if not (Hashtbl.mem world.states digest) then
+    Hashtbl.add world.states digest state;
+  digest
+
+let create ~schemas =
+  let catalog =
+    List.fold_left
+      (fun acc (name, schema) -> String_map.add name schema acc)
+      String_map.empty schemas
+  in
+  let root : state =
+    String_map.map (fun _ -> []) catalog
+  in
+  let world = { schemas = catalog; states = Hashtbl.create 16; tips = [] } in
+  let root_digest = store world root in
+  world.tips <- [ ("main", root_digest) ];
+  world
+
+let state_at world = function
+  | Some (Term.String digest) -> Hashtbl.find_opt world.states digest
+  | Some _ -> None
+  | None -> (
+      match List.assoc_opt "main" world.tips with
+      | Some digest -> Hashtbl.find_opt world.states digest
+      | None -> None)
+
+let find world ?at name =
+  match (String_map.find_opt name world.schemas, state_at world at) with
+  | Some schema, Some state ->
+      let facts = Option.value ~default:[] (String_map.find_opt name state) in
+      let schema = List.map (fun (l, p) -> (l, World.Primitive p)) schema in
+      Some (World.Table { schema; facts })
+  | _ -> None
+
+(* [Insert]: the transition relation between states (decision 3).
+   Ground relation name, ground tuple, ground predecessor state;
+   the tuple must match the schema exactly and satisfy its
+   primitive domains, or there is no such transition. *)
+let insert world bindings =
+  let ground label =
+    Option.bind (Label.Map.find_opt label bindings) Pattern.to_term
+  in
+  match (ground relation_l, ground tuple_l, ground before_l) with
+  | Some (Term.String relation), Some (Term.Record tuple), Some (Term.String before)
+    -> (
+      match
+        (String_map.find_opt relation world.schemas, Hashtbl.find_opt world.states before)
+      with
+      | Some schema, Some state ->
+          let conforms =
+            List.length schema = Label.Map.cardinal tuple
+            && List.for_all
+                 (fun (label, domain) ->
+                   match Label.Map.find_opt label tuple with
+                   | Some value -> World.member_of_primitive value domain
+                   | None -> false)
+                 schema
+          in
+          if not conforms then World.T_fail
+          else
+            let facts = Option.value ~default:[] (String_map.find_opt relation state) in
+            let successor = String_map.add relation (facts @ [ tuple ]) state in
+            World.T_state (Term.string (store world successor))
+      | _ -> World.T_fail)
+  | Some _, Some _, Some _ -> World.T_fail
+  | _ ->
+      (* Something essential is not ground yet: wait for the chain. *)
+      World.T_stuck
+
+let transition world name bindings =
+  match name with "Insert" -> Some (insert world bindings) | _ -> None
+
+let tip world branch =
+  Option.map Term.string (List.assoc_opt branch world.tips)
+
+(* The single effect: compare-and-swap on the tip (decision 8). *)
+let commit world ~branch ~expect ~next =
+  match (expect, next, List.assoc_opt branch world.tips) with
+  | Term.String expected, Term.String next_digest, Some current
+    when String.equal current expected && Hashtbl.mem world.states next_digest ->
+      world.tips <-
+        (branch, next_digest) :: List.remove_assoc branch world.tips;
+      Ok ()
+  | _ -> Error `Conflict
+
+(* Linearity (decision 6): within one expression, a state variable
+   is consumed at most once as [before:] and produced at most once
+   as [after:]. Sequencing comes from the chain, and the chain must
+   be a chain. *)
+let linear expr =
+  let rec applications = function
+    | World.Apply (name, bindings) -> [ (name, bindings) ]
+    | World.And (a, b) | World.Or (a, b) | World.Not (a, b) | World.Forall (a, b)
+      ->
+        applications a @ applications b
+  in
+  let uses label =
+    applications expr
+    |> List.filter (fun (name, _) -> String.equal name "Insert")
+    |> List.filter_map (fun (_, bindings) ->
+           match Label.Map.find_opt label bindings with
+           | Some (Pattern.Var v) -> Some v
+           | _ -> None)
+  in
+  let duplicate vars =
+    let sorted = List.sort String.compare vars in
+    let rec scan = function
+      | a :: b :: _ when String.equal a b -> Some a
+      | _ :: rest -> scan rest
+      | [] -> None
+    in
+    scan sorted
+  in
+  match (duplicate (uses before_l), duplicate (uses after_l)) with
+  | Some v, _ ->
+      Error
+        (Printf.sprintf
+           "state %s consumed twice: a fork inside one expression is not a chain" v)
+  | _, Some v -> Error (Printf.sprintf "state %s produced twice" v)
+  | None, None -> Ok ()
diff --git a/lib/branch.mli b/lib/branch.mli
new file mode 100644
index 0000000..a60d91e
--- /dev/null
+++ b/lib/branch.mli
@@ -0,0 +1,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. *)
diff --git a/lib/vm.ml b/lib/vm.ml
index 4a11c4d..67efc56 100644
--- a/lib/vm.ml
+++ b/lib/vm.ml
@@ -23,6 +23,12 @@ type solution = {
 module Make (W : World.WORLD) = struct
   exception Stuck of string list
 
+  let forced_label name =
+    match Label.of_string name with Ok l -> l | Error _ -> assert false
+
+  let at_label = forced_label "at"
+  let after_label = forced_label "after"
+
   (* A goal is a proposition to establish or a denial to refute.
      Conjunction flattens; [u :not d] contributes the universe
      positively and the denial negatively. *)
@@ -547,7 +553,22 @@ module Make (W : World.WORLD) = struct
               else if List.mem `Unknown statuses then
                 Wait { residuatable = false }
               else Run [ (subst, []) ])
-    | Positive (World.Apply (name, bindings)) -> (
+    | Positive (World.Apply (name, all_bindings)) -> (
+        (* State-scoped reads (decision 7): the reserved [at:] label
+           names the state a stored relation is read from. It is
+           stripped before unification, since it is not an attribute
+           of any tuple, and must be ground before the read runs. *)
+        let at_pattern =
+          Option.map
+            (Pattern.Subst.resolve subst)
+            (Label.Map.find_opt at_label all_bindings)
+        in
+        let bindings = Label.Map.remove at_label all_bindings in
+        match at_pattern with
+        | Some p when not (Pattern.is_ground p) ->
+            Wait { residuatable = false }
+        | _ -> (
+        let at = Option.bind at_pattern Pattern.to_term in
         match Builtin.run subst name bindings with
         | Some (Builtin.Solved substs) ->
             Run (List.map (fun s -> (s, [])) substs)
@@ -556,7 +577,27 @@ module Make (W : World.WORLD) = struct
                case. Constraining is not searching. *)
             Wait { residuatable = true }
         | None -> (
-            match W.find world name with
+            (* Transitions before stored relations: a world that
+               declares [Insert] answers for it here (decision 3).
+               The successor state unifies with [after:]. *)
+            match
+              W.transition world name
+                (Label.Map.map (Pattern.Subst.resolve subst) bindings)
+            with
+            | Some (World.T_state successor) -> (
+                match Label.Map.find_opt after_label bindings with
+                | None -> Run [ (subst, []) ]
+                | Some pattern -> (
+                    match
+                      Pattern.Subst.unify subst pattern
+                        (Pattern.of_term successor)
+                    with
+                    | Some subst -> Run [ (subst, []) ]
+                    | None -> Run []))
+            | Some World.T_fail -> Run []
+            | Some World.T_stuck -> Wait { residuatable = false }
+            | None -> (
+            match W.find world ?at name with
             | Some (World.Table { facts; _ }) ->
                 Run
                   (List.filter_map
@@ -591,7 +632,7 @@ module Make (W : World.WORLD) = struct
                    checks references. An embedded host that lies
                    about its catalog surfaces here as a stuck goal
                    rather than a crash. *)
-                Wait { residuatable = false }))
+                Wait { residuatable = false }))))
 
   (* Search yields substitutions with the goals they left
      residuated. A state where every remaining goal is residuatable
diff --git a/lib/world.ml b/lib/world.ml
index a053c2c..94fa0a9 100644
--- a/lib/world.ml
+++ b/lib/world.ml
@@ -22,10 +22,15 @@ type def =
   | Table of { schema : (Label.t * domain) list; facts : Term.t Label.Map.t list }
   | Rules of rule list
 
+type transition_result = T_state of Term.t | T_fail | T_stuck
+
 module type WORLD = sig
   type t
 
-  val find : t -> string -> def option
+  val find : t -> ?at:Term.t -> string -> def option
+
+  val transition :
+    t -> string -> Pattern.t Label.Map.t -> transition_result option
 end
 
 type error =
@@ -227,7 +232,8 @@ module String_map = Map.Make (String)
 module Standalone = struct
   type t = def String_map.t
 
-  let find world name = String_map.find_opt name world
+  let find world ?at:_ name = String_map.find_opt name world
+  let transition _ _ _ = None
 
   let schema_of_node ~relation = function
     | Ast.Seq (entries, None) ->
diff --git a/lib/world.mli b/lib/world.mli
index 14f82d3..3868261 100644
--- a/lib/world.mli
+++ b/lib/world.mli
@@ -56,13 +56,34 @@ type def =
       (** 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. Builtins are the VM's own and are not consulted
-    here. *)
+    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 -> string -> def option
+  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
@@ -94,7 +115,13 @@ val expr_of_node : Ast.node -> (expr, error) result
 module Standalone : sig
   type t
 
-  val find : t -> string -> def option
+  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