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

1 files changed, 162 insertions, 0 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 ()