From f52efd20120cf5ceeae28da2c04d57acc6e46f14 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sun, 12 Jul 2026 10:11:38 -0300 Subject: branch world: state scoped reads, insert transitions, tip commit --- lib/branch.ml | 162 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/branch.mli | 46 ++++++++++++++++ lib/vm.ml | 47 +++++++++++++++-- lib/world.ml | 10 +++- lib/world.mli | 35 +++++++++++-- 5 files changed, 291 insertions(+), 9 deletions(-) create mode 100644 lib/branch.ml create mode 100644 lib/branch.mli (limited to 'lib') 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 -- cgit v1.2.3