✨ Implement update & reconcile logic

lib/domains.ml

@@ -10,27 +10,25 @@ module rec T : sig
     | Clos of clos
     | Set_clos of set_clos
     | Comp_clos of comp_clos
-    | Comp_thunk of comp_thunk
+    | Comp_spec of comp_spec
 
   and clos = { param : Id.t; body : hook_free Expr.t; env : Env.t }
   and set_clos = { label : Label.t; path : Path.t }
   and comp_clos = { comp : Prog.comp; env : Env.t }
-  and comp_thunk = { comp : Prog.comp; env : Env.t; arg : value }
-  and view_spec = Vs_null | Vs_int of int | Vs_comp of comp_thunk
+  and comp_spec = { comp : Prog.comp; env : Env.t; arg : value }
+  and view_spec = Vs_null | Vs_int of int | Vs_comp of comp_spec
 
   type phase = P_init | P_update | P_retry | P_effect | P_top
   and decision = Idle | Retry | Update
   and st_store = St_store.t
   and job_q = Job_q.t
 
-  and part_view =
-    | Root
-    | Node of {
-        view_spec : view_spec;
-        dec : decision;
-        st_store : St_store.t;
-        eff_q : Job_q.t;
-      }
+  and part_view = {
+    comp_spec : comp_spec;
+    dec : decision;
+    st_store : St_store.t;
+    eff_q : Job_q.t;
+  }
 
   and tree = Leaf_null | Leaf_int of int | Path of Path.t
   and entry = { part_view : part_view; children : tree Snoc_list.t }
@@ -90,41 +88,28 @@ end = struct
 
   let lookup_st tree_mem ~path ~label =
     let { part_view; _ } = Map.find_exn tree_mem path in
-    match part_view with
-    | Root -> failwith "lookup_st: Root"
-    | Node { st_store; _ } -> St_store.lookup st_store ~label
+    St_store.lookup part_view.st_store ~label
 
   let update_st tree_mem ~path ~label (v, q) =
     let ({ part_view; _ } as entry) = Map.find_exn tree_mem path in
-    match part_view with
-    | Root -> failwith "update_st: Root"
-    | Node ({ st_store; _ } as node) ->
-        let st_store = St_store.update st_store ~label ~value:(v, q) in
-        Map.set tree_mem ~key:path
-          ~data:{ entry with part_view = Node { node with st_store } }
+    let st_store = St_store.update part_view.st_store ~label ~value:(v, q) in
+    Map.set tree_mem ~key:path
+      ~data:{ entry with part_view = { part_view with st_store } }
 
   let get_dec tree_mem ~path =
     let { part_view; _ } = Map.find_exn tree_mem path in
-    match part_view with
-    | Root -> failwith "set_dec: Root"
-    | Node { dec; _ } -> dec
+    part_view.dec
 
   let set_dec tree_mem ~path dec =
     let ({ part_view; _ } as entry) = Map.find_exn tree_mem path in
-    match part_view with
-    | Root -> failwith "set_dec: Root"
-    | Node node ->
-        Map.set tree_mem ~key:path
-          ~data:{ entry with part_view = Node { node with dec } }
+    Map.set tree_mem ~key:path
+      ~data:{ entry with part_view = { part_view with dec } }
 
   let enq_eff tree_mem ~path clos =
     let ({ part_view; _ } as entry) = Map.find_exn tree_mem path in
-    match part_view with
-    | Root -> failwith "enq_eff: Root"
-    | Node ({ eff_q; _ } as node) ->
-        let eff_q = Job_q.enqueue eff_q clos in
-        Map.set tree_mem ~key:path
-          ~data:{ entry with part_view = Node { node with eff_q } }
+    let eff_q = Job_q.enqueue part_view.eff_q clos in
+    Map.set tree_mem ~key:path
+      ~data:{ entry with part_view = { part_view with eff_q } }
 
   let alloc_pt = Map.length
   let lookup_ent tree_mem ~path = Map.find_exn tree_mem path
@@ -147,7 +132,7 @@ module Value = struct
   let to_vs = function
     | Unit -> Some Vs_null
     | Int i -> Some (Vs_int i)
-    | Comp_thunk t -> Some (Vs_comp t)
+    | Comp_spec t -> Some (Vs_comp t)
     | _ -> None
 
   let to_vss = function View_spec vss -> Some vss | _ -> None

lib/interp.ml

@@ -95,14 +95,14 @@ let rec eval : type a. a Expr.t -> value = function
       | Clos { param; body; env } ->
           let env = Env.extend env ~id:param ~value:(eval arg) in
           perform (In_env env) eval body
-      | Comp_clos { comp; env } -> Comp_thunk { comp; env; arg = eval arg }
+      | Comp_clos { comp; env } -> Comp_spec { comp; env; arg = eval arg }
       | Set_clos { label; path } ->
           (* Argument to the setter should be a setting thunk *)
           let clos = eval arg |> clos_of_value_exn in
 
           let self_pt = perform Rd_pt in
           let phase = perform Rd_ph in
-          if Phase.(phase = P_top) then raise Invalid_phase;
+          if Phase.(phase = P_top) then assert false;
 
           let dec =
             if Int.(path = self_pt) && Phase.(phase <> P_effect) then Retry
@@ -150,11 +150,11 @@ let rec eval : type a. a Expr.t -> value = function
           perform (In_env env) eval body
       | P_effect | P_top -> raise Invalid_phase)
   | Eff e ->
-      let path = perform Rd_pt in
-      let phase = perform Rd_ph in
+      let path = perform Rd_pt
+      and phase = perform Rd_ph
+      and env = perform Rd_env in
       (match phase with P_effect | P_top -> raise Invalid_phase | _ -> ());
-      perform
-        (Enq_eff (path, { param = Id.unit; body = e; env = perform Rd_env }));
+      perform (Enq_eff (path, { param = Id.unit; body = e; env }));
       Unit
   | Seq (e1, e2) ->
       eval e1 |> ignore;
@@ -173,30 +173,30 @@ let rec eval_mult : type a. a Expr.t -> value =
   let v = eval expr in
   let path = perform Rd_pt in
   match perform (Get_dec path) with
-  | Retry -> eval_mult expr
+  | Retry -> ptph_h eval_mult expr ~ptph:(path, P_retry)
   | Idle | Update -> v
 
 let rec render (path : Path.t) (vss : view_spec list) : unit =
   List.iter vss ~f:(fun vs ->
       let t = render1 vs in
+      (* refetch the whole entry, as the children may have updated the parent *)
       let ({ children; _ } as ent) = perform (Lookup_ent path) in
       perform
         (Update_ent (path, { ent with children = Snoc_list.(children ||> t) })))
 
 and render1 : view_spec -> tree = function
   | Vs_null -> Leaf_null
   | Vs_int i -> Leaf_int i
-  | Vs_comp { comp = { param; body; _ }; env; arg } as view_spec ->
+  | Vs_comp ({ comp = { param; body; _ }; env; arg } as comp_spec) ->
       let path = perform Alloc_pt
       and env = Env.extend env ~id:param ~value:arg
       and part_view =
-        Node
-          {
-            view_spec;
-            dec = Idle;
-            st_store = St_store.empty;
-            eff_q = Job_q.empty;
-          }
+        {
+          comp_spec;
+          dec = Idle;
+          st_store = St_store.empty;
+          eff_q = Job_q.empty;
+        }
       in
       perform (Update_ent (path, { part_view; children = [] }));
 
@@ -208,13 +208,69 @@ and render1 : view_spec -> tree = function
 
       Path path
 
+let rec update (path : Path.t) : unit =
+  let {
+    part_view = { comp_spec = { comp = { param; body; _ }; env; arg }; dec; _ };
+    children;
+  } =
+    perform (Lookup_ent path)
+  in
+  match dec with
+  | Retry -> assert false
+  | Idle -> Snoc_list.iter children ~f:update1
+  | Update ->
+      let env = Env.extend env ~id:param ~value:arg in
+      let vss =
+        (eval_mult |> env_h ~env |> ptph_h ~ptph:(path, P_update)) body
+        |> vss_of_value_exn
+      in
+
+      let old_trees =
+        children |> Snoc_list.to_list
+        |> Util.pad_or_truncate ~len:(List.length vss)
+      in
+      (* TODO: We assume that updates from a younger sibling to an older sibling
+         are not dropped, while those from an older sibling to a younger sibling
+         are. That's why we are resetting the children list and then snoc each
+         child again in the reconcile function. We should verify this
+         behavior. *)
+      let ent = perform (Lookup_ent path) in
+      perform (Update_ent (path, { ent with children = [] }));
+      reconcile path old_trees vss
+
+and update1 : tree -> unit = function
+  | Leaf_null | Leaf_int _ -> ()
+  | Path path -> update path
+
+and reconcile (path : Path.t) (old_trees : tree option list)
+    (vss : view_spec list) : unit =
+  List.iter2_exn old_trees vss ~f:(fun old_tree new_vs ->
+      let t =
+        match (old_tree, new_vs) with
+        | Some (Leaf_null as t), Vs_null -> t
+        | Some (Leaf_int i as t), Vs_int j when i = j -> t
+        | Some (Path pt as t), (Vs_comp { comp = { name; _ }; arg; _ } as vs) ->
+            let {
+              part_view =
+                { comp_spec = { comp = { name = name'; _ }; arg = arg'; _ }; _ };
+              _;
+            } =
+              perform (Lookup_ent pt)
+            in
+            if Id.(name = name') && Value.(arg = arg') then (
+              update1 t;
+              t)
+            else render1 vs
+        | _, vs -> render1 vs
+      in
+      let ({ children; _ } as ent) = perform (Lookup_ent path) in
+      perform
+        (Update_ent (path, { ent with children = Snoc_list.(children ||> t) })))
+
 let rec commit_effs (path : Path.t) : unit =
   let { part_view; children } = perform (Lookup_ent path) in
-  (match part_view with
-  | Root -> ()
-  | Node { eff_q; _ } ->
-      Job_q.iter eff_q ~f:(fun { body; env; _ } ->
-          env_h eval body ~env |> ignore));
+  Job_q.iter part_view.eff_q ~f:(fun { body; env; _ } ->
+      env_h eval body ~env |> ignore);
 
   Snoc_list.iter children ~f:commit_effs1
 

lib/snoc_list.ml

@@ -8,5 +8,13 @@ let rec iter t ~(f : 'a -> unit) : unit =
   match t with
   | [] -> ()
   | Snoc (l, a) ->
-      f a;
-      iter l ~f
+      iter l ~f;
+      f a
+
+let[@tail_mod_cons] rec to_list : 'a t -> 'a list = function
+  | [] -> []
+  | Snoc (l, a) -> a :: to_list l
+
+let[@tail_mod_cons] rec of_list : 'a list -> 'a t = function
+  | [] -> []
+  | a :: l -> Snoc (of_list l, a)

lib/util.ml

@@ -2,9 +2,31 @@ open! Base
 
 module Map_key (T : sig
   type t
+
+  val sexp_of_t : t -> Sexp.t
+  val t_of_sexp : Sexp.t -> t
+  val of_string : string -> t
+  val to_string : t -> string
+  val ( <= ) : t -> t -> bool
+  val ( >= ) : t -> t -> bool
+  val ( = ) : t -> t -> bool
+  val ( < ) : t -> t -> bool
+  val ( > ) : t -> t -> bool
+  val ( <> ) : t -> t -> bool
+  val compare : t -> t -> int
+  val min : t -> t -> t
+  val max : t -> t -> t
+  val ascending : t -> t -> int
+  val descending : t -> t -> int
+  val between : t -> low:t -> high:t -> bool
+  val clamp_exn : t -> min:t -> max:t -> t
+  val clamp : t -> min:t -> max:t -> t Or_error.t
+
   type comparator_witness
 
   val comparator : (t, comparator_witness) Comparator.t
+  val hash : t -> int
+  val equal : t -> t -> bool
 end) =
 struct
   include T
@@ -16,3 +38,10 @@ struct
     let empty = empty (module T)
   end
 end
+
+let pad_or_truncate (lst : 'a list) ~(len : int) : 'a option list =
+  let open List in
+  let l = length lst in
+  let pad = if l < len then init (len - l) ~f:(fun _ -> None) else [] in
+  let lst = take lst len in
+  map ~f:(fun x -> Some x) lst @ pad