From 9b425616c6a82fe6510f7fc72070d3bd1410ff3f Mon Sep 17 00:00:00 2001 From: Jay Lee Date: Tue, 2 Jul 2024 15:41:12 +0900 Subject: [PATCH] :tada: Functioning interpreter --- bin/main.ml | 40 +------------------------- lib/domains.ml | 6 ++-- lib/interp.ml | 77 ++++++++++++++++++++++++++------------------------ lib/logger.ml | 7 +++++ 4 files changed, 50 insertions(+), 80 deletions(-) diff --git a/bin/main.ml b/bin/main.ml index 665e572..5492952 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -1,44 +1,6 @@ open! Base open React_trace -(*let test_prog =*) -(* let open Syntax in*) -(* Prog.Expr Expr.(View [ Const Unit ])*) - -(*let test_prog =*) -(* let open Syntax in*) -(* Prog.( *) -(* Comp*) -(* ( { name = "C"; param = "x"; body = Expr.(View [ Const Unit ]) },*) -(* Expr Expr.(View [ App { fn = Var "C"; arg = Const Unit } ]) ))*) - -(*let test_prog =*) -(* let open Syntax in*) -(* Prog.( *) -(* Comp*) -(* ( {*) -(* name = "C";*) -(* param = "x";*) -(* body =*) -(* Expr.( *) -(* Stt*) -(* {*) -(* label = 0;*) -(* stt = "s";*) -(* set = "setS";*) -(* init = Fn { param = "s"; body = Const (Int 42) };*) -(* body =*) -(* Seq*) -(* ( App*) -(* {*) -(* fn = Var "setS";*) -(* arg = Fn { param = "s"; body = Const (Int 42) };*) -(* },*) -(* View [ Const Unit ] );*) -(* });*) -(* },*) -(* Expr Expr.(View [ App { fn = Var "C"; arg = Const Unit } ]) ))*) - let test_prog = let open Syntax in Prog.( @@ -53,7 +15,7 @@ let test_prog = label = 0; stt = "s"; set = "setS"; - init = Fn { param = "s"; body = Const (Int 42) }; + init = Const (Int 42); body = Seq ( Eff diff --git a/lib/domains.ml b/lib/domains.ml index 29e07a9..ce862d9 100644 --- a/lib/domains.ml +++ b/lib/domains.ml @@ -18,7 +18,7 @@ module rec T : sig 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 + type phase = P_init | P_update | P_retry | P_effect type decision = Idle | Retry | Update type part_view = @@ -138,7 +138,6 @@ end = struct | P_update -> a "P_update" | P_retry -> a "P_retry" | P_effect -> a "P_effect" - | P_top -> a "P_top" and sexp_of_decision = let open Sexp_helper in @@ -297,8 +296,7 @@ module Phase = struct | P_init, P_init | P_update, P_update | P_retry, P_retry - | P_effect, P_effect - | P_top, P_top -> + | P_effect, P_effect -> true | _, _ -> false diff --git a/lib/interp.ml b/lib/interp.ml index b65b20b..659e1c8 100644 --- a/lib/interp.ml +++ b/lib/interp.ml @@ -142,7 +142,6 @@ let rec eval : type a. a Expr.t -> value = let self_pt = perform Rd_pt in let phase = perform Rd_ph in - if Phase.(phase = P_top) then assert false; let dec = if Int.(path = self_pt) && Phase.(phase <> P_effect) then Retry @@ -188,12 +187,12 @@ let rec eval : type a. a Expr.t -> value = 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 | P_top -> raise Invalid_phase) + | P_effect -> raise Invalid_phase) | Eff e -> 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 | _ -> ()); + (match phase with P_effect -> raise Invalid_phase | _ -> ()); perform (Enq_eff (path, { param = Id.unit; body = e; env })); Unit | Seq (e1, e2) -> @@ -265,6 +264,7 @@ let rec update (path : Path.t) : bool = | Idle -> Snoc_list.fold children ~init:false ~f:(fun acc t -> acc || update1 t) | Update -> + perform (Set_dec (path, Idle)); let env = Env.extend env ~id:param ~value:arg in let vss = (eval_mult |> env_h ~env |> ptph_h ~ptph:(path, P_update)) body @@ -282,45 +282,47 @@ let rec update (path : Path.t) : bool = verify this behavior. *) let ent = perform (Lookup_ent path) in perform (Update_ent (path, { ent with children = [] })); - reconcile path old_trees vss) + reconcile path old_trees vss; + true) and update1 (t : tree) : bool = Logger.update1 t; match t with Leaf_null | Leaf_int _ -> false | Path path -> update path and reconcile (path : Path.t) (old_trees : tree option list) - (vss : view_spec list) : bool = + (vss : view_spec list) : unit = Logger.reconcile path old_trees vss; - List.fold2_exn old_trees vss ~init:false ~f:(fun updated old_tree new_vs -> - let t, updated' = - match (old_tree, new_vs) with - | Some (Leaf_null as t), Vs_null -> (t, false) - | Some (Leaf_int i as t), Vs_int j when i = j -> (t, false) - | Some (Path pt as t), (Vs_comp { comp = { name; _ }; arg; _ } as vs) - -> ( - let { part_view; _ } = perform (Lookup_ent pt) in - match part_view with - | Root -> assert false - | Node - { comp_spec = { comp = { name = name'; _ }; arg = arg'; _ }; _ } - -> - if Id.(name = name') && Value.(arg = arg') then (t, update1 t) - else (render1 vs, true)) - | _, vs -> (render1 vs, true) - in + List.iter2_exn old_trees vss ~f:(fun old_tree vs -> + let t = reconcile1 old_tree vs in let ({ children; _ } as ent) = perform (Lookup_ent path) in perform - (Update_ent (path, { ent with children = Snoc_list.(children ||> t) })); - updated || updated') + (Update_ent (path, { ent with children = Snoc_list.(children ||> t) }))) + +and reconcile1 (old_tree : tree option) (vs : view_spec) : tree = + Logger.reconcile1 old_tree vs; + match (old_tree, 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; _ } = perform (Lookup_ent pt) in + match part_view with + | Root -> assert false + | Node { comp_spec = { comp = { name = name'; _ }; arg = arg'; _ }; _ } -> + if Id.(name = name') && Value.(arg = arg') then t else render1 vs) + | _, vs -> render1 vs let rec commit_effs (path : Path.t) : unit = Logger.commit_effs path; - let { part_view; children } = perform (Lookup_ent path) in + let ({ part_view; children } as ent) = perform (Lookup_ent path) in (match part_view with | Root -> () - | Node { eff_q; _ } -> + | Node ({ eff_q; _ } as node) -> Job_q.iter eff_q ~f:(fun { body; env; _ } -> - (eval |> env_h ~env |> ptph_h ~ptph:(path, P_effect)) body |> ignore)); + (eval |> env_h ~env |> ptph_h ~ptph:(path, P_effect)) body |> ignore); + perform + (Update_ent + ( path, + { ent with part_view = Node { node with eff_q = Job_q.empty } } ))); Snoc_list.iter children ~f:commit_effs1 @@ -352,16 +354,17 @@ let step_path (path : Path.t) : bool = if has_updates then commit_effs path; has_updates -let run (prog : Prog.t) : unit = +let run ?(step : int option) (prog : Prog.t) : unit = Logger.run prog; - let cnt = ref 0 in - let rec loop () = + let driver () = + let cnt = ref 1 in let path = step_prog prog in - if step_path path then ( - Logs.info (fun m -> - m "Step %d" - (Int.incr cnt; - !cnt)); - loop ()) + let rec loop () = + Int.incr cnt; + Logs.info (fun m -> m "Step %d" !cnt); + if step_path path then + match step with Some n when !cnt >= n -> () | _ -> loop () + in + loop () in - mem_h loop () ~mem:Tree_mem.empty |> ignore + mem_h driver () ~mem:Tree_mem.empty |> ignore diff --git a/lib/logger.ml b/lib/logger.ml index dfdb0a4..0096576 100644 --- a/lib/logger.ml +++ b/lib/logger.ml @@ -100,6 +100,13 @@ let reconcile path old_trees vss = Sexp.pp (List.sexp_of_t Value.sexp_of_view_spec vss)) +let reconcile1 old_tree vs = + Logs.debug (fun m -> + m "reconcile1 [old_tree: %a, vs: %a]" Sexp.pp + ((Option.sexp_of_t Value.sexp_of_tree) old_tree) + Sexp.pp + (Value.sexp_of_view_spec vs)) + let commit_effs path = Logs.debug (fun m -> m "commit_effs [path: %a]" Sexp.pp (Path.sexp_of_t path))