Skip to content

Commit

Permalink
♻️ {P_update, P_retry} = {P_succ}
Browse files Browse the repository at this point in the history
  • Loading branch information
Zeta611 committed Feb 24, 2025
1 parent c957ff1 commit 60d07a4
Show file tree
Hide file tree
Showing 3 changed files with 6 additions and 6 deletions.
4 changes: 2 additions & 2 deletions lib/domains/concrete_domains.ml
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ module M : Domains.S = struct
and view_spec = Vs_null | Vs_int of int | Vs_comp of comp_spec
[@@deriving sexp_of]

type phase = P_init | P_update | P_retry | P_effect [@@deriving sexp_of]
type phase = P_init | P_succ | P_effect [@@deriving sexp_of]
type decision = Idle | Retry | Update [@@deriving sexp_of]

type part_view =
Expand Down Expand Up @@ -227,7 +227,7 @@ module M : Domains.S = struct
end

module Phase = struct
type t = phase = P_init | P_update | P_retry | P_effect [@@deriving equal]
type t = phase = P_init | P_succ | P_effect [@@deriving equal]

let ( = ) = equal
let ( <> ) p1 p2 = not (p1 = p2)
Expand Down
2 changes: 1 addition & 1 deletion lib/domains/domains.ml
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ module type T = sig
and comp_spec = { comp : Prog.comp; env : env; 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
type phase = P_init | P_succ | P_effect
type decision = Idle | Retry | Update

type part_view =
Expand Down
6 changes: 3 additions & 3 deletions lib/interp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -213,7 +213,7 @@ let rec eval : type a. a Expr.t -> value =
in
perform (Update_st (path, label, (v, Job_q.empty)));
perform (In_env env) eval body
| P_update | P_retry ->
| P_succ ->
let v_old, q = perform (Lookup_st (path, label)) in
(* Run the setting thunks in the set queue *)
let v =
Expand Down Expand Up @@ -314,7 +314,7 @@ let rec eval_mult : type a. ?re_render:int -> a Expr.t -> value =
( path,
{ ent with part_view = Node { node with eff_q = Job_q.empty } }
)));
ptph_h ~ptph:(path, P_retry) (eval_mult ~re_render) expr
ptph_h ~ptph:(path, P_succ) (eval_mult ~re_render) expr
| Idle | Update -> v

let alloc_tree (vs : view_spec) : tree =
Expand Down Expand Up @@ -398,7 +398,7 @@ let rec update (path : Path.t) (arg : value option) : bool =
perform (Set_arg (path, arg));
let env = Env.extend env ~id:param ~value:arg in
let vss =
(eval_mult |> env_h ~env |> ptph_h ~ptph:(path, P_update)) body
(eval_mult |> env_h ~env |> ptph_h ~ptph:(path, P_succ)) body
|> vss_of_value_exn
in

Expand Down

0 comments on commit 60d07a4

Please sign in to comment.