diff --git a/lib/domains.ml b/lib/domains.ml index 6ba4b38..f594d8d 100644 --- a/lib/domains.ml +++ b/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 diff --git a/lib/interp.ml b/lib/interp.ml index ce10fdd..bf2e0c0 100644 --- a/lib/interp.ml +++ b/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,12 +173,13 @@ 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) }))) @@ -186,17 +187,16 @@ let rec render (path : Path.t) (vss : view_spec list) : unit = 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 diff --git a/lib/snoc_list.ml b/lib/snoc_list.ml index 9536d47..1bf073f 100644 --- a/lib/snoc_list.ml +++ b/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) diff --git a/lib/util.ml b/lib/util.ml index 10265a6..138169c 100644 --- a/lib/util.ml +++ b/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