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

1 files changed, 44 insertions, 3 deletions

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