diff options
Diffstat (limited to '')
| -rw-r--r-- | lib/branch.ml | 162 | ||||
| -rw-r--r-- | lib/branch.mli | 46 |
2 files changed, 208 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 () 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. *) |