From 7026242e2d7580b4c32a7a8ba50099ac829fbba9 Mon Sep 17 00:00:00 2001 From: Jay Lee Date: Tue, 25 Jun 2024 10:10:46 +0900 Subject: [PATCH] :sparkles: Implement initial render pass --- .ocamlformat | 1 - lib/batched_queue.ml | 59 +++++++---- lib/domains.ml | 219 +++++++++++++++++++++++++++++------------ lib/interp.ml | 228 ++++++++++++++++++++++++++++++------------- lib/snoc_list.ml | 12 +++ lib/syntax.ml | 10 +- lib/util.ml | 18 ++++ 7 files changed, 384 insertions(+), 163 deletions(-) create mode 100644 lib/snoc_list.ml create mode 100644 lib/util.ml diff --git a/.ocamlformat b/.ocamlformat index 87c1145..f805ba7 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,3 +1,2 @@ profile = default -version = 0.26.2 wrap-comments = true diff --git a/lib/batched_queue.ml b/lib/batched_queue.ml index 0552437..6f6d5c5 100644 --- a/lib/batched_queue.ml +++ b/lib/batched_queue.ml @@ -1,26 +1,49 @@ open! Base -type 'a t = { f : 'a list; r : 'a list } +module type S = sig + type t + type elt -exception Empty_queue + exception Empty_queue -let empty = { f = []; r = [] } -let is_empty = function { f = []; _ } -> true | _ -> false + val empty : t + val is_empty : t -> bool + val enqueue : t -> elt -> t + val front : t -> elt + val dequeue : t -> t + val size : t -> int + val to_list : t -> elt list + val fold : t -> init:'acc -> f:('acc -> elt -> 'acc) -> 'acc + val iter : t -> f:(elt -> unit) -> unit +end -let enqueue q x = - match q with - | { f = []; _ } -> { f = [ x ]; r = [] } - | { f; r } -> { f; r = x :: r } +module M (T : sig + type t +end) : S with type elt := T.t = struct + type elt = T.t + type t = { f : elt list; r : elt list } -let front = function - | { f = []; _ } -> raise Empty_queue - | { f = h :: _; _ } -> h + exception Empty_queue -let dequeue = function - | { f = []; _ } -> raise Empty_queue - | { f = [ _ ]; r } -> { f = List.rev r; r = [] } - | { f = _ :: t; r } -> { f = t; r } + let empty = { f = []; r = [] } + let is_empty = function { f = []; _ } -> true | _ -> false -let size { f; r } = List.(length f + length r) -let to_list { f; r } = f @ List.rev r -let fold q = List.fold (to_list q) + let enqueue q x = + match q with + | { f = []; _ } -> { f = [ x ]; r = [] } + | { f; r } -> { f; r = x :: r } + + let front = function + | { f = []; _ } -> raise Empty_queue + | { f = h :: _; _ } -> h + + let dequeue = function + | { f = []; _ } -> raise Empty_queue + | { f = [ _ ]; r } -> { f = List.rev r; r = [] } + | { f = _ :: t; r } -> { f = t; r } + + let size { f; r } = List.(length f + length r) + let to_list { f; r } = f @ List.rev r + let fold q = List.fold (to_list q) + let iter q = List.iter (to_list q) +end diff --git a/lib/domains.ml b/lib/domains.ml index 512abde..6ba4b38 100644 --- a/lib/domains.ml +++ b/lib/domains.ml @@ -1,83 +1,172 @@ open! Base open Syntax - -module Env = struct - type 'a t = 'a Id.Map.t +module Path = Util.Map_key (Int) + +module rec T : sig + type value = + | Unit + | Int of int + | View_spec of view_spec list + | Clos of clos + | Set_clos of set_clos + | Comp_clos of comp_clos + | Comp_thunk of comp_thunk + + 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 + + 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 tree = Leaf_null | Leaf_int of int | Path of Path.t + and entry = { part_view : part_view; children : tree Snoc_list.t } +end = + T + +and Env : sig + type t + + val empty : t + val lookup : t -> id:Id.t -> T.value option + val extend : t -> id:Id.t -> value:T.value -> t +end = struct + type t = T.value Id.Map.t let empty = Id.Map.empty let lookup env ~id = Map.find env id let extend env ~id ~value = Map.set env ~key:id ~data:value end -module Store = struct - type 'a t = 'a Label.Map.t +and St_store : sig + type t + + val empty : t + val lookup : t -> label:Label.t -> T.value * Job_q.t + val update : t -> label:Label.t -> value:T.value * Job_q.t -> t +end = struct + type t = (T.value * Job_q.t) Label.Map.t let empty = Label.Map.empty let lookup store ~label = Map.find_exn store label let update store ~label ~value = Map.set store ~key:label ~data:value end -module Tree_path = struct - module T = Int - include T +and Job_q : (Batched_queue.S with type elt := T.clos) = Batched_queue.M (struct + type t = T.clos +end) + +include T + +module Tree_mem : sig + type t + + val empty : t + val lookup_st : t -> path:Path.t -> label:Label.t -> value * Job_q.t + val update_st : t -> path:Path.t -> label:Label.t -> value * Job_q.t -> t + val get_dec : t -> path:Path.t -> decision + val set_dec : t -> path:Path.t -> decision -> t + val enq_eff : t -> path:Path.t -> clos -> t + val alloc_pt : t -> Path.t + val lookup_ent : t -> path:Path.t -> entry + val update_ent : t -> path:Path.t -> entry -> t +end = struct + type t = entry Path.Map.t + + let empty = Path.Map.empty + + 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 + + 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 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 + + 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 } } + + 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 alloc_pt = Map.length + let lookup_ent tree_mem ~path = Map.find_exn tree_mem path + let update_ent tree_mem ~path ent = Map.set tree_mem ~key:path ~data:ent +end + +module Value = struct + type t = value - module Map = struct - open Map - include M (T) + let equal v1 v2 = + match (v1, v2) with + | Unit, Unit -> true + | Int i1, Int i2 -> i1 = i2 + | _, _ -> false - let empty = empty (module T) - end + let ( = ) = equal + let ( <> ) v1 v2 = not (v1 = v2) + let to_int = function Int i -> Some i | _ -> None + + let to_vs = function + | Unit -> Some Vs_null + | Int i -> Some (Vs_int i) + | Comp_thunk t -> Some (Vs_comp t) + | _ -> None + + let to_vss = function View_spec vss -> Some vss | _ -> None + let to_clos = function Clos c -> Some c | _ -> None end -module Job_q = Batched_queue - -type value = - | Unit - | Int of int - | View_spec of view_spec list - | Clos of clos - | Set_clos of set_clos - | Comp_clos of comp_clos - | Comp_thunk of comp_thunk - -and clos = { param : Id.t; body : hook_free Expr.t; env : env } -and set_clos = { label : Label.t; path : path } -and comp_clos = { comp : Prog.comp; env : env } -and comp_thunk = { comp : Prog.comp; env : env; arg : value } -and view_spec = Vs_null | Vs_int of int | Vs_comp of comp_thunk -and env = value Env.t -and phase = P_init | P_update | P_retry | P_effect -and node_ctx = { decision : decision; st_store : st_store; tree_mem : tree_mem } -and decision = Idle | Retry | Update -and st_store = (value * job_q) Store.t -and job_q = clos Job_q.t - -and part_view = { - view_spec : view_spec; - decision : decision; - st_store : st_store; - eff_q : job_q; -} - -and tree = - | Leaf of tree_val - | Node of { part_view : part_view; children : path list } - -and tree_val = Leaf_null | Leaf_int of int -and tree_mem = tree option Tree_path.Map.t -and path = Tree_path.t - -let empty_env : env = Env.empty -let empty_st_store : st_store = Store.empty -let empty_tree_mem : tree_mem = Tree_path.Map.empty -let empty_setq : job_q = Job_q.empty -let empty_effq : job_q = Job_q.empty - -let equal v1 v2 = - match (v1, v2) with - | Unit, Unit -> true - | Int i1, Int i2 -> i1 = i2 - | _, _ -> false - -let ( = ) = equal -let ( <> ) v1 v2 = not (equal v1 v2) +module Phase = struct + type t = phase + + let equal p1 p2 = + match (p1, p2) with + | P_init, P_init + | P_update, P_update + | P_retry, P_retry + | P_effect, P_effect + | P_top, P_top -> + true + | _, _ -> false + + let ( = ) = equal + let ( <> ) p1 p2 = not (p1 = p2) +end diff --git a/lib/interp.ml b/lib/interp.ml index 3591582..ce10fdd 100644 --- a/lib/interp.ml +++ b/lib/interp.ml @@ -4,49 +4,91 @@ open Stdlib.Effect.Deep open Syntax open Domains -type _ eff += Rd_env : env eff | In_env : env -> (('b -> 'a) -> 'b -> 'a) eff +exception Unbound_var of string +exception Type_error +exception Invalid_phase + +(* path and phase effects *) +type _ eff += Rd_pt : Path.t eff | Rd_ph : phase eff +(* environmental effects *) type _ eff += - | Lookup_st : Label.t -> (value * job_q) eff - | Update_st : (Label.t * (value * job_q)) -> unit eff + | Rd_env : Env.t eff + | In_env : Env.t -> (('b -> 'a) -> 'b -> 'a) eff +(* memory effects in eval/eval_mult *) type _ eff += - | Part_view_set_dec : path * Label.t * decision -> unit eff - | Part_view_enq_set : path * Label.t * clos -> unit eff + | Lookup_st : Path.t * Label.t -> (value * Job_q.t) eff + | Update_st : (Path.t * Label.t * (value * Job_q.t)) -> unit eff + | Get_dec : Path.t -> decision eff + | Set_dec : Path.t * decision -> unit eff + | Enq_eff : Path.t * clos -> unit eff -type _ eff += Set_dec : decision -> unit eff -type _ eff += Rd_phase : phase eff -type _ eff += Rd_path : path eff -type _ eff += Enq_eff : clos -> unit eff +(* memory effects in render *) +type _ eff += + | Alloc_pt : Path.t eff + | Lookup_ent : Path.t -> entry eff + | Update_ent : Path.t * entry -> unit eff -exception Unbound_var of string -exception Type_error -exception Invalid_phase +let ptph_h (type a b) (f : b -> a) (x : b) : ptph:Path.t * phase -> a = + match f x with + | v -> fun ~ptph:_ -> v + | effect Rd_pt, k -> fun ~ptph -> continue k (fst ptph) ~ptph + | effect Rd_ph, k -> fun ~ptph -> continue k (snd ptph) ~ptph + +let rec env_h : type a b. (b -> a) -> b -> env:Env.t -> a = + fun f x -> + match f x with + | v -> fun ~env:_ -> v + | effect Rd_env, k -> fun ~env -> continue k env ~env + | effect In_env env', k -> fun ~env -> continue k (env_h ~env:env') ~env + +let mem_h (type a b) (f : b -> a) (x : b) : mem:Tree_mem.t -> a * Tree_mem.t = + match f x with + | v -> fun ~mem -> (v, mem) + (* in eval *) + | effect Lookup_st (path, label), k -> + fun ~mem -> continue k (Tree_mem.lookup_st mem ~path ~label) ~mem + | effect Update_st (path, label, (v, q)), k -> + fun ~mem -> + continue k () ~mem:(Tree_mem.update_st mem ~path ~label (v, q)) + | effect Get_dec path, k -> + fun ~mem -> continue k (Tree_mem.get_dec mem ~path) ~mem + | effect Set_dec (path, dec), k -> + fun ~mem -> continue k () ~mem:(Tree_mem.set_dec mem ~path dec) + | effect Enq_eff (path, clos), k -> + fun ~mem -> continue k () ~mem:(Tree_mem.enq_eff mem ~path clos) + (* in render *) + | effect Alloc_pt, k -> fun ~mem -> continue k (Tree_mem.alloc_pt mem) ~mem + | effect Lookup_ent path, k -> + fun ~mem -> continue k (Tree_mem.lookup_ent mem ~path) ~mem + | effect Update_ent (path, ent), k -> + fun ~mem -> continue k () ~mem:(Tree_mem.update_ent mem ~path ent) + +let value_exn exn v = + Option.value_exn v ~error:(Error.of_exn exn ~backtrace:`Get) + +let int_of_value_exn v = v |> Value.to_int |> value_exn Type_error +let vs_of_value_exn v = v |> Value.to_vs |> value_exn Type_error +let vss_of_value_exn v = v |> Value.to_vss |> value_exn Type_error +let clos_of_value_exn v = v |> Value.to_clos |> value_exn Type_error + +module Env = struct + include Env + + let lookup_exn env ~id = lookup env ~id |> value_exn (Unbound_var id) +end let rec eval : type a. a Expr.t -> value = function | Const (Unit ()) -> Unit | Const (Int i) -> Int i - | Var x -> ( + | Var id -> let env = perform Rd_env in - match Map.find env x with Some v -> v | None -> raise (Unbound_var x)) - | View es -> - let vss = - List.fold es ~init:[] ~f:(fun vss e -> - let vs = - match eval e with - | Unit -> Vs_null - | Int i -> Vs_int i - | Comp_thunk t -> Vs_comp t - | _ -> raise Type_error - in - vs :: vss) - in - View_spec vss - | Cond { pred; con; alt } -> ( - match eval pred with - | Int 0 -> eval alt - | Int _ -> eval con - | _ -> raise Type_error) + Env.lookup_exn env ~id + | View es -> View_spec (List.map es ~f:(fun e -> eval e |> vs_of_value_exn)) + | Cond { pred; con; alt } -> + let p = eval pred |> int_of_value_exn in + if Int.(p <> 0) then eval con else eval alt | Fn { param; body } -> Clos { param; body; env = perform Rd_env } | App { fn; arg } -> ( match eval fn with @@ -55,66 +97,65 @@ let rec eval : type a. a Expr.t -> value = function perform (In_env env) eval body | Comp_clos { comp; env } -> Comp_thunk { comp; env; arg = eval arg } | Set_clos { label; path } -> - let clos = - (* Argument to the setter should be a setting thunk *) - match eval arg with Clos c -> c | _ -> raise Type_error + (* 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; + + let dec = + if Int.(path = self_pt) && Phase.(phase <> P_effect) then Retry + else Update in + perform (Set_dec (path, dec)); + + let v, q = perform (Lookup_st (path, label)) in + perform (Update_st (path, label, (v, Job_q.enqueue q clos))); - let self_path = perform Rd_path in - if Tree_path.(path = self_path) then ( - (* Set self's state *) - perform - (Set_dec - (match perform Rd_phase with P_effect -> Update | _ -> Retry)); - - let v, q = perform (Lookup_st label) in - perform (Update_st (label, (v, Job_q.enqueue q clos))); - Unit) - else ( - (* Set other's state *) - perform (Part_view_set_dec (path, label, Update)); - perform (Part_view_enq_set (path, label, clos)); - Unit) + Unit | _ -> raise Type_error) | Let { id; bound; body } -> let value = eval bound in let env = Env.extend (perform Rd_env) ~id ~value in perform (In_env env) eval body | Stt { label; stt; set; init; body } -> ( - let path = perform Rd_path in - match perform Rd_phase with + let path = perform Rd_pt in + match perform Rd_ph with | P_init -> let v = eval init in - perform (Update_st (label, (v, empty_setq))); let env = perform Rd_env |> Env.extend ~id:stt ~value:v |> Env.extend ~id:set ~value:(Set_clos { label; path }) in + perform (Update_st (path, label, (v, Job_q.empty))); perform (In_env env) eval body | P_update | P_retry -> - let v_prev, q = perform (Lookup_st label) in + let v_old, q = perform (Lookup_st (path, label)) in (* Run the setting thunks in the set queue *) - let v_curr = - Job_q.fold q ~init:v_prev ~f:(fun value { param; body; env } -> + let v = + Job_q.fold q ~init:v_old ~f:(fun value { param; body; env } -> let env = Env.extend env ~id:param ~value in perform (In_env env) eval body) in - if v_prev <> v_curr then perform (Set_dec Update); - perform (Update_st (label, (v_curr, Job_q.empty))); + let env = perform Rd_env - |> Env.extend ~id:stt ~value:v_curr + |> Env.extend ~id:stt ~value:v |> Env.extend ~id:set ~value:(Set_clos { label; path }) in + if Value.(v_old <> v) then perform (Set_dec (path, Update)); + perform (Update_st (path, label, (v, Job_q.empty))); perform (In_env env) eval body - | P_effect -> raise Invalid_phase) - | Eff e -> ( - match perform Rd_phase with - | P_effect -> raise Invalid_phase - | _ -> - perform (Enq_eff { param = Id.unit; body = e; env = perform Rd_env }); - Unit) + | P_effect | P_top -> raise Invalid_phase) + | Eff e -> + let path = perform Rd_pt in + let phase = perform Rd_ph in + (match phase with P_effect | P_top -> raise Invalid_phase | _ -> ()); + perform + (Enq_eff (path, { param = Id.unit; body = e; env = perform Rd_env })); + Unit | Seq (e1, e2) -> eval e1 |> ignore; eval e2 @@ -129,7 +170,54 @@ let rec eval : type a. a Expr.t -> value = function let rec eval_mult : type a. a Expr.t -> value = fun expr -> - (match eval expr with - | v -> ( function Idle | Update -> v | Retry -> eval_mult expr) - | effect Set_dec d, k -> fun _d -> continue k () d) - Idle + let v = eval expr in + let path = perform Rd_pt in + match perform (Get_dec path) with + | Retry -> eval_mult expr + | 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 + 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 -> + 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; + } + in + perform (Update_ent (path, { part_view; children = [] })); + + let vss = + (eval_mult |> env_h ~env |> ptph_h ~ptph:(path, P_init)) body + |> vss_of_value_exn + in + render path vss; + + Path path + +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)); + + Snoc_list.iter children ~f:commit_effs1 + +and commit_effs1 : tree -> unit = function + | Leaf_null | Leaf_int _ -> () + | Path path -> commit_effs path diff --git a/lib/snoc_list.ml b/lib/snoc_list.ml new file mode 100644 index 0000000..9536d47 --- /dev/null +++ b/lib/snoc_list.ml @@ -0,0 +1,12 @@ +open! Base + +type 'a t = [] | Snoc of 'a t * 'a + +let ( ||> ) l a = Snoc (l, a) + +let rec iter t ~(f : 'a -> unit) : unit = + match t with + | [] -> () + | Snoc (l, a) -> + f a; + iter l ~f diff --git a/lib/syntax.ml b/lib/syntax.ml index 3fe87b7..e5a5da6 100644 --- a/lib/syntax.ml +++ b/lib/syntax.ml @@ -1,15 +1,7 @@ open! Base module Id = struct - module T = String - include T - - module Map = struct - open Map - include M (T) - - let empty = empty (module T) - end + include Util.Map_key (String) let unit = "()" end diff --git a/lib/util.ml b/lib/util.ml new file mode 100644 index 0000000..10265a6 --- /dev/null +++ b/lib/util.ml @@ -0,0 +1,18 @@ +open! Base + +module Map_key (T : sig + type t + type comparator_witness + + val comparator : (t, comparator_witness) Comparator.t +end) = +struct + include T + + module Map = struct + open Map + include M (T) + + let empty = empty (module T) + end +end