complete #367

src/gen_decompile.ml

@@ -644,17 +644,17 @@ end = struct
     | _ ->
       ty
 
-  let rec unify (uf : uf) (effect : effect_) : uf =
-    pump (unify_r uf effect)
+  let rec unify (uf : uf) (effect_ : effect_) : uf =
+    pump (unify_r uf effect_)
 
   and pump ((uf, effects) : uf * effect_ list) : uf =
     unify_all uf effects
 
   and unify_all (uf : uf) (effects : effect_ list) : uf =
     List.fold_left unify uf effects
 
-  and unify_r (uf : uf) (effect : effect_) : uf * effect_ list =
-    match effect with
+  and unify_r (uf : uf) (effect_ : effect_) : uf * effect_ list =
+    match effect_ with
     | `TyUnify (ty1, ty2) ->
       unify_type_r uf ty1 ty2
 

src/model.ml

@@ -4193,7 +4193,7 @@ let extract_list (mt : mterm) (e : mterm) =
 
 (* -------------------------------------------------------------------- *)
 
-type effect = Eadded of ident | Eremoved of ident | Eupdated of ident
+type effect_ = Eadded of ident | Eremoved of ident | Eupdated of ident
 [@@deriving show {with_path = false}]
 module Utils : sig
 

src/printer_pt.ml

@@ -932,11 +932,11 @@ and pp_field fmt { pldesc = f; _ } =
 and pp_simple_expr fmt e = (pp_expr e_simple PNone) fmt e
 
 (* -------------------------------------------------------------------------- *)
-let pp_to fmt ((to_, when_, effect) : (lident * expr option * expr option)) =
+let pp_to fmt ((to_, when_, effect_) : (lident * expr option * expr option)) =
   Format.fprintf fmt " to %a@\n%a%a"
     pp_id to_
     (pp_option (pp_enclose " when {" "}@\n" (pp_expr e_default PNone))) when_
-    (pp_option (pp_enclose " with effect {" "}@\n" (pp_expr e_default PNone))) effect
+    (pp_option (pp_enclose " with effect {" "}@\n" (pp_expr e_default PNone))) effect_
 
 let pp_specification_variable fmt (sv : (lident * type_t * expr option) loced) =
   match sv with
@@ -1104,16 +1104,16 @@ let pp_entry_properties fmt (props : entry_properties) =
   pp_option (pp_rf "fail if" "with") fmt props.failif;
   (pp_list "@\n" pp_function) fmt (List.map unloc props.functions)
 
-let pp_transition fmt (to_, conditions, effect) =
+let pp_transition fmt (to_, conditions, effect_) =
   Format.fprintf fmt "to %a%a%a@\n"
     pp_id to_
     (pp_option (
         fun fmt e ->
           Format.fprintf fmt " when { %a }"
             (pp_expr e_default PNone) e)) conditions
     (pp_option (fun fmt e ->
-         Format.fprintf fmt "@\nwith effect {@\n  @[%a@]@\n}"
-           pp_simple_expr e)) effect
+         Format.fprintf fmt "@\nwith effect_ {@\n  @[%a@]@\n}"
+           pp_simple_expr e)) effect_
 
 let pp_parameter fmt (id, ty, dv, c) =
   Format.fprintf fmt "%a%a : %a%a"

src/typing.ml

@@ -6229,9 +6229,9 @@ and for_instruction ~(ret : A.type_ option) (kind : ekind) (env : env) (i : PT.e
   Env.inscope env (fun env -> for_instruction_r ~ret kind env i)
 
 (* -------------------------------------------------------------------- *)
-let for_effect ~(ret : A.type_ option) (kind : ekind) (env : env) (effect : PT.expr) =
+let for_effect ~(ret : A.type_ option) (kind : ekind) (env : env) (effect_ : PT.expr) =
   Env.inscope env (fun env ->
-      let env, i = for_instruction kind env effect ~ret in (env, (env, i)))
+      let env, i = for_instruction kind env effect_ ~ret in (env, (env, i)))
 
 (* -------------------------------------------------------------------- *)
 let for_named_state (locc : Location.t) ?enum (env : env) (x : PT.lident) =
@@ -6346,16 +6346,16 @@ let for_entry (env : env) (act : PT.entry_properties) i (ret : PT.type_t option)
   let env, fai  = Option.foldmap (for_rfs `Entry) env act.failif in
   let ret = Option.bind (for_type env) ret in
   let env, poeffect = Option.foldmap (for_effect ~ret:ret (if Option.is_some ret then `Entry else `Getter)) env i in
-  let effect = Option.map snd poeffect in
+  let effect_ = Option.map snd poeffect in
   let env, funs = List.fold_left_map for_function env act.functions in
-  (env, (ret, sourcedby, calledby, stateis, actfs, cst, req, fai, funs, effect))
+  (env, (ret, sourcedby, calledby, stateis, actfs, cst, req, fai, funs, effect_))
 
 (* -------------------------------------------------------------------- *)
-let for_transition ?enum (env : env) (state, when_, effect) =
+let for_transition ?enum (env : env) (state, when_, effect_) =
   let tx_state  = for_named_state Location.dummy ?enum env state in
   let tx_when   = Option.map (for_expr ~ety:(A.Tbuiltin A.VTbool) `Function env) when_ in
   let env, tx_effect = snd_map (Option.map snd)
-      (Option.foldmap (for_effect ~ret:None `Entry) env effect) in
+      (Option.foldmap (for_effect ~ret:None `Entry) env effect_) in
 
   env, { tx_state; tx_when; tx_effect; }
 
@@ -7009,7 +7009,7 @@ let for_acttx_decl (env : env) (decl : acttx loced)
       let env, decl =
         Env.inscope env (fun env ->
             let env, args = for_args_decl env args in
-            let env, (ret, srcby, callby, stateis, actfs, csts, reqs, fais, funs, effect) =
+            let env, (ret, srcby, callby, stateis, actfs, csts, reqs, fais, funs, effect_) =
               for_entry env pt i None in
 
             let decl =
@@ -7020,7 +7020,7 @@ let for_acttx_decl (env : env) (decl : acttx loced)
                 ad_srcby  = for_csby srcby;
                 ad_callby = for_csby callby;
                 ad_stateis= stateis;
-                ad_effect = Option.map (fun x -> `Raw x) effect;
+                ad_effect = Option.map (fun x -> `Raw x) effect_;
                 ad_funs   = funs;
                 ad_csts   = Option.get_dfl [] csts;
                 ad_reqs   = Option.get_dfl [] reqs;
@@ -7041,7 +7041,7 @@ let for_acttx_decl (env : env) (decl : acttx loced)
       let env, decl =
         Env.inscope env (fun env ->
             let env, args = for_args_decl env args in
-            let env, (ret, srcby, callby, stateis, actfs, csts, reqs, fais, funs, effect) =
+            let env, (ret, srcby, callby, stateis, actfs, csts, reqs, fais, funs, effect_) =
               for_entry env entry_properties (Some body) (Some ret_t) in
 
             let decl =
@@ -7052,7 +7052,7 @@ let for_acttx_decl (env : env) (decl : acttx loced)
                 ad_srcby  = for_csby srcby;
                 ad_callby = for_csby callby;
                 ad_stateis= stateis;
-                ad_effect = Option.map (fun x -> `Raw x) effect;
+                ad_effect = Option.map (fun x -> `Raw x) effect_;
                 ad_funs   = funs;
                 ad_csts   = Option.get_dfl [] csts;
                 ad_reqs   = Option.get_dfl [] reqs;