From 2e44e19adb19b9aefd0fb4629653b83192cffe76 Mon Sep 17 00:00:00 2001 From: Jay Lee Date: Sat, 21 Dec 2024 15:45:03 +0900 Subject: [PATCH] :recycle: The effect syntax strikes back --- bin/js/dune | 4 +- bin/js/main.ml | 4 +- bin/js/string_recorder.ml | 69 ----- bin/js/string_recorder/dune | 3 + bin/js/string_recorder/string_recorder.ml | 57 ++++ .../{ => string_recorder}/string_recorder.mli | 0 bin/native/dune | 6 +- bin/native/report_box_recorder/dune | 3 + .../report_box_recorder.ml | 24 +- .../report_box_recorder.mli | 0 lib/default_recorder.ml | 54 ++-- lib/interp.ml | 259 +++++++----------- lib/recorder_intf.ml | 3 +- 13 files changed, 202 insertions(+), 284 deletions(-) delete mode 100644 bin/js/string_recorder.ml create mode 100644 bin/js/string_recorder/dune create mode 100644 bin/js/string_recorder/string_recorder.ml rename bin/js/{ => string_recorder}/string_recorder.mli (100%) create mode 100644 bin/native/report_box_recorder/dune rename bin/native/{ => report_box_recorder}/report_box_recorder.ml (83%) rename bin/native/{ => report_box_recorder}/report_box_recorder.mli (100%) diff --git a/bin/js/dune b/bin/js/dune index 8a81576..9b4b8c3 100644 --- a/bin/js/dune +++ b/bin/js/dune @@ -2,5 +2,5 @@ (name main) (modes js) (preprocess - (pps ppx_jane js_of_ocaml-ppx)) - (libraries react_trace base logs logs.fmt fmt fmt.tty js_of_ocaml)) + (pps js_of_ocaml-ppx)) + (libraries react_trace string_recorder base logs.fmt fmt.tty js_of_ocaml)) diff --git a/bin/js/main.ml b/bin/js/main.ml index b9b5f2d..e3a2b12 100644 --- a/bin/js/main.ml +++ b/bin/js/main.ml @@ -28,8 +28,8 @@ let () = Js.export_all (object%js method run (fuel : int) program_str = - (let open Result.Let_syntax in - let%bind prog = parse_program_str program_str in + (let ( let* ) x f = Result.bind x ~f in + let* prog = parse_program_str program_str in let Interp.{ recording; _ } = Interp.run ?fuel:(if fuel < 1 then None else Some fuel) diff --git a/bin/js/string_recorder.ml b/bin/js/string_recorder.ml deleted file mode 100644 index dc39c2b..0000000 --- a/bin/js/string_recorder.ml +++ /dev/null @@ -1,69 +0,0 @@ -open! Base -open Stdlib.Effect -open Stdlib.Effect.Deep -open React_trace -open Lib_domains -open Concrete_domains -open Interp_effects -include Recorder_intf - -type recording = string - -let emp_recording = "= Recording =\n" - -let event_h = - { - retc = (fun v ~recording -> (v, recording)); - exnc = raise; - effc = - (fun (type a) (eff : a t) -> - match eff with - | Update_st (path, label, (v, q)) -> - Some - (fun (k : (a, _) continuation) ~(recording : recording) -> - let () = perform (Update_st (path, label, (v, q))) in - let recording = - recording - ^ Printf.sprintf "[path %s] Update state %d -> %s\n" - (Sexp.to_string (Path.sexp_of_t path)) - label - (Sexp.to_string (sexp_of_value v)) - in - continue k () ~recording) - | Set_dec (path, dec) -> - Some - (fun (k : (a, _) continuation) ~(recording : recording) -> - let () = perform (Set_dec (path, dec)) in - let recording = - recording - ^ Printf.sprintf "[path %s] Set decision %s\n" - (Sexp.to_string (Path.sexp_of_t path)) - (Sexp.to_string (sexp_of_decision dec)) - in - continue k () ~recording) - | Enq_eff (path, clos) -> - Some - (fun (k : (a, _) continuation) ~(recording : recording) -> - let () = perform (Enq_eff (path, clos)) in - let recording = - recording - ^ Printf.sprintf "[path %s] Enqueue effect\n" - (Sexp.to_string (Path.sexp_of_t path)) - in - continue k () ~recording) - | Alloc_pt -> - Some - (fun (k : (a, _) continuation) ~(recording : recording) -> - let path = perform Alloc_pt in - let recording = - recording - ^ Printf.sprintf "Allocate path %s\n" - (Sexp.to_string (Path.sexp_of_t path)) - in - continue k path ~recording) - | Checkpoint _ -> - Some - (fun (k : (a, _) continuation) ~(recording : recording) -> - continue k () ~recording) - | _ -> None); - } diff --git a/bin/js/string_recorder/dune b/bin/js/string_recorder/dune new file mode 100644 index 0000000..f8b893c --- /dev/null +++ b/bin/js/string_recorder/dune @@ -0,0 +1,3 @@ +(library + (name string_recorder) + (libraries react_trace base)) diff --git a/bin/js/string_recorder/string_recorder.ml b/bin/js/string_recorder/string_recorder.ml new file mode 100644 index 0000000..c81f93a --- /dev/null +++ b/bin/js/string_recorder/string_recorder.ml @@ -0,0 +1,57 @@ +open! Base +open Stdlib.Effect +open Stdlib.Effect.Deep +open React_trace +open Lib_domains +open Concrete_domains +open Interp_effects +include Recorder_intf + +type recording = string + +let emp_recording = "= Recording =\n" + +let event_h (type a b) (f : a -> b) (x : a) : + recording:recording -> b * recording = + match f x with + | v -> fun ~recording -> (v, recording) + | effect Update_st (path, label, (v, q)), k -> + fun ~recording -> + let () = perform (Update_st (path, label, (v, q))) in + let recording = + recording + ^ Printf.sprintf "[path %s] Update state %d -> %s\n" + (Sexp.to_string (Path.sexp_of_t path)) + label + (Sexp.to_string (sexp_of_value v)) + in + continue k () ~recording + | effect Set_dec (path, dec), k -> + fun ~recording -> + let () = perform (Set_dec (path, dec)) in + let recording = + recording + ^ Printf.sprintf "[path %s] Set decision %s\n" + (Sexp.to_string (Path.sexp_of_t path)) + (Sexp.to_string (sexp_of_decision dec)) + in + continue k () ~recording + | effect Enq_eff (path, clos), k -> + fun ~recording -> + let () = perform (Enq_eff (path, clos)) in + let recording = + recording + ^ Printf.sprintf "[path %s] Enqueue effect\n" + (Sexp.to_string (Path.sexp_of_t path)) + in + continue k () ~recording + | effect Alloc_pt, k -> + fun ~recording -> + let path = perform Alloc_pt in + let recording = + recording + ^ Printf.sprintf "Allocate path %s\n" + (Sexp.to_string (Path.sexp_of_t path)) + in + continue k path ~recording + | effect Checkpoint _, k -> fun ~recording -> continue k () ~recording diff --git a/bin/js/string_recorder.mli b/bin/js/string_recorder/string_recorder.mli similarity index 100% rename from bin/js/string_recorder.mli rename to bin/js/string_recorder/string_recorder.mli diff --git a/bin/native/dune b/bin/native/dune index 499ba5e..2588521 100644 --- a/bin/native/dune +++ b/bin/native/dune @@ -1,14 +1,10 @@ (executable (public_name react_trace) (name main) - (preprocess - (pps ppx_jane)) (libraries react_trace + report_box_recorder base - logs logs.fmt - fmt fmt.tty - printbox printbox-text)) diff --git a/bin/native/report_box_recorder/dune b/bin/native/report_box_recorder/dune new file mode 100644 index 0000000..8315ad2 --- /dev/null +++ b/bin/native/report_box_recorder/dune @@ -0,0 +1,3 @@ +(library + (name report_box_recorder) + (libraries react_trace base printbox)) diff --git a/bin/native/report_box_recorder.ml b/bin/native/report_box_recorder/report_box_recorder.ml similarity index 83% rename from bin/native/report_box_recorder.ml rename to bin/native/report_box_recorder/report_box_recorder.ml index 54a3e94..7e263d2 100644 --- a/bin/native/report_box_recorder.ml +++ b/bin/native/report_box_recorder/report_box_recorder.ml @@ -75,18 +75,12 @@ let get_path_from_checkpoint = function let emp_recording = [] -let event_h = - { - retc = (fun v ~recording -> (v, recording)); - exnc = raise; - effc = - (fun (type a) (eff : a t) -> - match eff with - | Checkpoint { msg; checkpoint } -> - Some - (fun (k : (a, _) continuation) ~(recording : recording) -> - let pt = get_path_from_checkpoint checkpoint in - let box = path pt in - continue k () ~recording:((msg, box) :: recording)) - | _ -> None); - } +let event_h (type a b) (f : a -> b) (x : a) : + recording:recording -> b * recording = + match f x with + | v -> fun ~recording -> (v, recording) + | effect Checkpoint { msg; checkpoint }, k -> + fun ~recording -> + let pt = get_path_from_checkpoint checkpoint in + let box = path pt in + continue k () ~recording:((msg, box) :: recording) diff --git a/bin/native/report_box_recorder.mli b/bin/native/report_box_recorder/report_box_recorder.mli similarity index 100% rename from bin/native/report_box_recorder.mli rename to bin/native/report_box_recorder/report_box_recorder.mli diff --git a/lib/default_recorder.ml b/lib/default_recorder.ml index a8517c6..7d0ee7a 100644 --- a/lib/default_recorder.ml +++ b/lib/default_recorder.ml @@ -7,36 +7,24 @@ type recording = unit let emp_recording = () -let event_h = - { - retc = (fun v ~recording -> (v, recording)); - exnc = raise; - effc = - (fun (type a) (eff : a t) -> - match eff with - | Update_st (path, label, (v, q)) -> - Some - (fun (k : (a, _) continuation) ~(recording : recording) -> - let () = perform (Update_st (path, label, (v, q))) in - continue k () ~recording) - | Set_dec (path, dec) -> - Some - (fun (k : (a, _) continuation) ~(recording : recording) -> - let () = perform (Set_dec (path, dec)) in - continue k () ~recording) - | Enq_eff (path, clos) -> - Some - (fun (k : (a, _) continuation) ~(recording : recording) -> - let () = perform (Enq_eff (path, clos)) in - continue k () ~recording) - | Alloc_pt -> - Some - (fun (k : (a, _) continuation) ~(recording : recording) -> - let path = perform Alloc_pt in - continue k path ~recording) - | Checkpoint _ -> - Some - (fun (k : (a, _) continuation) ~(recording : recording) -> - continue k () ~recording) - | _ -> None); - } +let event_h (type a b) (f : a -> b) (x : a) : + recording:recording -> b * recording = + match f x with + | v -> fun ~recording -> (v, recording) + | effect Update_st (path, label, (v, q)), k -> + fun ~recording -> + let () = perform (Update_st (path, label, (v, q))) in + continue k () ~recording + | effect Set_dec (path, dec), k -> + fun ~recording -> + let () = perform (Set_dec (path, dec)) in + continue k () ~recording + | effect Enq_eff (path, clos), k -> + fun ~recording -> + let () = perform (Enq_eff (path, clos)) in + continue k () ~recording + | effect Alloc_pt, k -> + fun ~recording -> + let path = perform Alloc_pt in + continue k path ~recording + | effect Checkpoint _, k -> fun ~recording -> continue k () ~recording diff --git a/lib/interp.ml b/lib/interp.ml index e7dfb76..ffe960b 100644 --- a/lib/interp.ml +++ b/lib/interp.ml @@ -6,151 +6,105 @@ open Syntax open Concrete_domains open Interp_effects -let re_render_limit_h : 'a. ('a, re_render_limit:int -> 'a) handler = - { - retc = (fun v ~re_render_limit:_ -> v); - exnc = raise; - effc = - (fun (type b) (eff : b t) -> - match eff with - | Re_render_limit -> - Some - (fun (k : (b, _) continuation) ~(re_render_limit : int) -> - continue k re_render_limit ~re_render_limit) - | _ -> None); - } - -let ptph_h = - { - retc = - (fun v ~ptph -> +let re_render_limit_h (type a b) (f : a -> b) (x : a) : re_render_limit:int -> b + = + match f x with + | v -> fun ~re_render_limit:_ -> v + | effect Re_render_limit, k -> + fun ~re_render_limit -> continue k re_render_limit ~re_render_limit + +let ptph_h (type a b) (f : a -> b) (x : a) : ptph:Path.t * phase -> b = + match f x with + | v -> + fun ~ptph -> Logger.ptph ptph `Ret; - v); - exnc = raise; - effc = - (fun (type a) (eff : a t) -> - match eff with - | Rd_pt -> - Some - (fun (k : (a, _) continuation) ~(ptph : Path.t * phase) -> - Logger.ptph ptph `Rd_pt; - continue k (fst ptph) ~ptph) - | Rd_ph -> - Some - (fun (k : (a, _) continuation) ~(ptph : Path.t * phase) -> - Logger.ptph ptph `Rd_ph; - continue k (snd ptph) ~ptph) - | _ -> None); - } - -let rec env_h : 'a. ('a, env:Env.t -> 'a) handler = - { - retc = - (fun v ~env -> + v + | effect Rd_pt, k -> + fun ~ptph -> + Logger.ptph ptph `Rd_pt; + continue k (fst ptph) ~ptph + | effect Rd_ph, k -> + fun ~ptph -> + Logger.ptph ptph `Rd_ph; + continue k (snd ptph) ~ptph + +let rec env_h : type a b. (a -> b) -> a -> env:Env.t -> b = + fun f x -> + match f x with + | v -> + fun ~env -> Logger.env env `Ret; - v); - exnc = raise; - effc = - (fun (type a) (eff : a t) -> - match eff with - | Rd_env -> - Some - (fun (k : (a, _) continuation) ~(env : Env.t) -> - Logger.env env `Rd_env; - continue k env ~env) - | In_env env' -> - Some - (fun (k : (a, _) continuation) ~(env : Env.t) -> - Logger.env env (`In_env env'); - continue k (fun f x -> match_with f x env_h ~env:env') ~env) - | _ -> None); - } - -let mem_h = - { - retc = - (fun v ~mem -> + v + | effect Rd_env, k -> + fun ~env -> + Logger.env env `Rd_env; + continue k env ~env + | effect In_env env', k -> + fun ~env -> + Logger.env env (`In_env env'); + continue k (env_h ~env:env') ~env + +let mem_h (type a b) (f : a -> b) (x : a) : mem:Memory.t -> b * Memory.t = + match f x with + | v -> + fun ~mem -> Logger.mem mem `Ret; - (v, mem)); - exnc = raise; - effc = - (fun (type a) (eff : a t) -> - match eff with - | Alloc_addr obj -> - Some - (fun (k : (a, _) continuation) ~(mem : Memory.t) -> - Logger.mem mem `Alloc_addr; - let addr = Memory.alloc mem in - let mem = Memory.update mem ~addr ~obj in - continue k addr ~mem) - | Lookup_addr addr -> - Some - (fun (k : (a, _) continuation) ~(mem : Memory.t) -> - Logger.mem mem (`Lookup_addr addr); - continue k (Memory.lookup mem ~addr) ~mem) - | Update_addr (addr, v) -> - Some - (fun (k : (a, _) continuation) ~(mem : Memory.t) -> - Logger.mem mem (`Update_addr (addr, v)); - continue k () ~mem:(Memory.update mem ~addr ~obj:v)) - | _ -> None); - } - -let treemem_h = - { - retc = - (fun v ~treemem -> + (v, mem) + | effect Alloc_addr obj, k -> + fun ~mem -> + Logger.mem mem `Alloc_addr; + let addr = Memory.alloc mem in + let mem = Memory.update mem ~addr ~obj in + continue k addr ~mem + | effect Lookup_addr addr, k -> + fun ~mem -> + Logger.mem mem (`Lookup_addr addr); + continue k (Memory.lookup mem ~addr) ~mem + | effect Update_addr (addr, v), k -> + fun ~mem -> + Logger.mem mem (`Update_addr (addr, v)); + continue k () ~mem:(Memory.update mem ~addr ~obj:v) + +let treemem_h (type a b) (f : a -> b) (x : a) : + treemem:Tree_mem.t -> b * Tree_mem.t = + match f x with + | v -> + fun ~treemem -> Logger.treemem treemem `Ret; - (v, treemem)); - exnc = raise; - effc = - (fun (type a) (eff : a t) -> - match eff with - (* in eval *) - | Lookup_st (path, label) -> - Some - (fun (k : (a, _) continuation) ~(treemem : Tree_mem.t) -> - Logger.treemem treemem (`Lookup_st (path, label)); - continue k (Tree_mem.lookup_st treemem ~path ~label) ~treemem) - | Update_st (path, label, (v, q)) -> - Some - (fun (k : (a, _) continuation) ~(treemem : Tree_mem.t) -> - Logger.treemem treemem (`Update_st (path, label, (v, q))); - continue k () - ~treemem:(Tree_mem.update_st treemem ~path ~label (v, q))) - | Get_dec path -> - Some - (fun (k : (a, _) continuation) ~(treemem : Tree_mem.t) -> - Logger.treemem treemem (`Get_dec path); - continue k (Tree_mem.get_dec treemem ~path) ~treemem) - | Set_dec (path, dec) -> - Some - (fun (k : (a, _) continuation) ~(treemem : Tree_mem.t) -> - Logger.treemem treemem (`Set_dec (path, dec)); - continue k () ~treemem:(Tree_mem.set_dec treemem ~path dec)) - | Enq_eff (path, clos) -> - Some - (fun (k : (a, _) continuation) ~(treemem : Tree_mem.t) -> - Logger.treemem treemem (`Enq_eff (path, clos)); - continue k () ~treemem:(Tree_mem.enq_eff treemem ~path clos)) - (* in render *) - | Alloc_pt -> - Some - (fun (k : (a, _) continuation) ~(treemem : Tree_mem.t) -> - Logger.treemem treemem `Alloc_pt; - continue k (Tree_mem.alloc_pt treemem) ~treemem) - | Lookup_ent path -> - Some - (fun (k : (a, _) continuation) ~(treemem : Tree_mem.t) -> - Logger.treemem treemem (`Lookup_ent path); - continue k (Tree_mem.lookup_ent treemem ~path) ~treemem) - | Update_ent (path, ent) -> - Some - (fun (k : (a, _) continuation) ~(treemem : Tree_mem.t) -> - Logger.treemem treemem (`Update_ent (path, ent)); - continue k () ~treemem:(Tree_mem.update_ent treemem ~path ent)) - | _ -> None); - } + (v, treemem) + | effect Lookup_st (path, label), k -> + fun ~treemem -> + Logger.treemem treemem (`Lookup_st (path, label)); + continue k (Tree_mem.lookup_st treemem ~path ~label) ~treemem + | effect Update_st (path, label, (v, q)), k -> + fun ~treemem -> + Logger.treemem treemem (`Update_st (path, label, (v, q))); + continue k () ~treemem:(Tree_mem.update_st treemem ~path ~label (v, q)) + | effect Get_dec path, k -> + fun ~treemem -> + Logger.treemem treemem (`Get_dec path); + continue k (Tree_mem.get_dec treemem ~path) ~treemem + | effect Set_dec (path, dec), k -> + fun ~treemem -> + Logger.treemem treemem (`Set_dec (path, dec)); + continue k () ~treemem:(Tree_mem.set_dec treemem ~path dec) + | effect Enq_eff (path, clos), k -> + fun ~treemem -> + Logger.treemem treemem (`Enq_eff (path, clos)); + continue k () ~treemem:(Tree_mem.enq_eff treemem ~path clos) + (* NOTE: in render *) + | effect Alloc_pt, k -> + fun ~treemem -> + Logger.treemem treemem `Alloc_pt; + continue k (Tree_mem.alloc_pt treemem) ~treemem + | effect Lookup_ent path, k -> + fun ~treemem -> + Logger.treemem treemem (`Lookup_ent path); + continue k (Tree_mem.lookup_ent treemem ~path) ~treemem + | effect Update_ent (path, ent), k -> + fun ~treemem -> + Logger.treemem treemem (`Update_ent (path, ent)); + continue k () ~treemem:(Tree_mem.update_ent treemem ~path ent) let value_exn exn v = Option.value_exn v ~error:(Error.of_exn exn ~backtrace:`Get) @@ -315,7 +269,7 @@ let rec eval_mult : type a. ?re_render:int -> a Expr.t -> value = perform (Checkpoint { msg = "Will retry"; checkpoint = Retry_start (re_render, path) }); - match_with (eval_mult ~re_render) expr ptph_h ~ptph:(path, P_retry) + ptph_h ~ptph:(path, P_retry) (eval_mult ~re_render) expr | Idle | Update -> v let rec render (path : Path.t) (vss : view_spec list) : unit = @@ -347,9 +301,7 @@ and render1 (vs : view_spec) : tree = perform (Update_ent (path, { part_view; children = [] })); let vss = - ( (eval_mult |> fun f x -> match_with f x env_h ~env) |> fun f x -> - match_with f x ptph_h ~ptph:(path, P_init) ) - body + (eval_mult |> env_h ~env |> ptph_h ~ptph:(path, P_init)) body |> vss_of_value_exn in render path vss; @@ -373,9 +325,7 @@ let rec update (path : Path.t) (arg : value option) : bool = Env.extend env ~id:param ~value:(Option.value arg ~default:arg') in let vss = - ( (eval_mult |> fun f x -> match_with f x env_h ~env) |> fun f x -> - match_with f x ptph_h ~ptph:(path, P_update) ) - body + (eval_mult |> env_h ~env |> ptph_h ~ptph:(path, P_update)) body |> vss_of_value_exn in @@ -433,10 +383,7 @@ let rec commit_effs (path : Path.t) : unit = | Root -> () | Node { eff_q; _ } -> ( Job_q.iter eff_q ~f:(fun { body; env; _ } -> - ( (eval |> fun f x -> match_with f x env_h ~env) |> fun f x -> - match_with f x ptph_h ~ptph:(path, P_effect) ) - body - |> ignore); + (eval |> env_h ~env |> ptph_h ~ptph:(path, P_effect)) body |> ignore); (* Refetch the entry, as committing effects may change the entry *) let ent = perform (Lookup_ent path) in @@ -465,7 +412,7 @@ let rec eval_top (prog : Prog.t) : view_spec list = let step_prog (prog : Prog.t) : Path.t = Logger.step_prog prog; - let vss = match_with eval_top prog env_h ~env:Env.empty in + let vss = env_h ~env:Env.empty eval_top prog in let path = perform Alloc_pt in perform (Update_ent (path, { part_view = Root; children = [] })); @@ -521,9 +468,9 @@ let run (type recording) ?(fuel : int option) let driver () = let open (val recorder) in - match_with driver () event_h ~recording:emp_recording + event_h ~recording:emp_recording driver () in - let driver () = match_with driver () treemem_h ~treemem:Tree_mem.empty in - let driver () = match_with driver () mem_h ~mem:Memory.empty in + let driver () = treemem_h ~treemem:Tree_mem.empty driver () in + let driver () = mem_h ~mem:Memory.empty driver () in let ((steps, recording), treemem), mem = driver () in { steps; mem; treemem; recording } diff --git a/lib/recorder_intf.ml b/lib/recorder_intf.ml index 999c4ef..b037aeb 100644 --- a/lib/recorder_intf.ml +++ b/lib/recorder_intf.ml @@ -1,9 +1,8 @@ open! Base -open Stdlib.Effect.Deep module type Intf = sig type recording val emp_recording : recording - val event_h : 'a. ('a, recording:recording -> 'a * recording) handler + val event_h : ('a -> 'b) -> 'a -> recording:recording -> 'b * recording end