🎉 Functioning interpreter

React-Analysis · Jul 2, 2024 · 9b42561 · 9b42561
1 parent 33d9eb4
commit 9b42561
Show file tree

Hide file tree

Showing 4 changed files with 50 additions and 80 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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))