Refactor cfold propagation and add eager mode

src/ecCoreModules.ml

@@ -55,6 +55,16 @@ let lv_of_expr e =
      LvTuple (List.map (fun e -> EcTypes.destr_var e, e_ty e) pvs)
   | _ -> failwith "failed to construct lv from expr"
 
+let explode_assgn (lv : lvalue) (e : expr) : ((prog_var * ty) * expr) list =
+  match lv, e with
+  | LvVar lv, e ->
+    [(lv, e)]
+  | LvTuple lvs, { e_node = Etuple es } ->
+    List.combine lvs es
+  | LvTuple lvs, e ->
+    List.mapi (fun i (pv, ty) ->
+      ((pv, ty), e_proj_simpl e i ty)) lvs
+
 (* -------------------------------------------------------------------- *)
 type instr = EcAst.instr
 
@@ -161,6 +171,14 @@ let is_while  = _is_of_get get_while
 let is_match  = _is_of_get get_match
 let is_raise  = _is_of_get get_raise
 
+(* -------------------------------------------------------------------- *)
+let i_asgn_of_pve (pve : ((prog_var * ty) * expr) list) : instr option = 
+  let lvs, es = List.split pve in
+
+  lvs
+  |> lv_of_list
+  |> omap (fun lvs -> i_asgn (lvs, e_tuple es))
+
 (* -------------------------------------------------------------------- *)
 let i_iter (f : instr -> unit) =
   let rec i_iter (i : instr) =
@@ -181,6 +199,24 @@ let i_iter (f : instr -> unit) =
 
   in fun (i : instr) -> i_iter i
 
+(* -------------------------------------------------------------------- *)
+let i_map_expr (tx : expr -> expr) =
+  let rec doit (i : instr) =
+    match i.i_node with
+    | Sasgn (lv, e) -> i_asgn (lv, (tx e))
+    | Sif (c, t, f) -> i_if (tx c, doit_s t, doit_s f)
+    | Smatch (e, cs) -> i_match (tx e, List.map (snd_map doit_s) cs)
+    | Swhile (c, bd) -> i_while (tx c, doit_s bd)
+    | Srnd (lv, e) -> i_rnd (lv, tx e)
+    | Sraise e -> i_raise (tx e)
+    | Sabstract (_ : memory) -> i
+    | Scall (lv, f, args) -> i_call (lv, f, List.map tx args)
+
+  and doit_s (s : stmt) =
+    stmt (List.map doit s.s_node) in
+
+  fun i -> doit i
+
 (* -------------------------------------------------------------------- *)
 module Uninit = struct    (* FIXME: generalize this for use in ecPV *)
   let e_pv e =

src/ecCoreModules.mli

@@ -15,6 +15,7 @@ val lv_to_list      : lvalue -> prog_var list
 val lv_to_ty_list   : lvalue -> (prog_var * ty) list
 val name_of_lv      : lvalue -> string
 val lv_of_expr      : expr -> lvalue
+val explode_assgn   : lvalue -> expr -> ((prog_var * ty) * expr) list
 
 (* --------------------------------------------------------------------- *)
 type instr = EcAst.instr
@@ -76,8 +77,12 @@ val is_while  : instr -> bool
 val is_match  : instr -> bool
 val is_raise  : instr -> bool
 
+(* -------------------------------------------------------------------- *)
+val i_asgn_of_pve : ((prog_var * ty) * expr) list -> instr option
+
 (* -------------------------------------------------------------------- *)
 val i_iter : (instr -> unit) -> instr -> unit
+val i_map_expr : (expr -> expr) -> instr -> instr
 
 (* -------------------------------------------------------------------- *)
 val get_uninit_read : stmt -> Sx.t

src/ecParser.mly

@@ -2990,8 +2990,8 @@ interleave_info:
 | INTERLEAVE info=loc(interleave_info)
     { Pinterleave info }
 
-| CFOLD s=side? c=codepos n=word?
-    { Pcfold (s, c, n) }
+| CFOLD eager=boption(STAR) side=side? start=codepos length=word?
+    { Pcfold { side; start; length; eager; } }
 
 | RND s=side? info=rnd_info c=prefix(COLON, semrndpos)?
     { Prnd (s, c, info) }

src/ecParsetree.ml

@@ -757,7 +757,7 @@ type phltactic =
   | Pcond          of pcond_info
   | Pmatch         of matchmode
   | Pswap          of ((oside * pswap_kind) located list)
-  | Pcfold         of (oside * pcodepos * int option)
+  | Pcfold         of pcfold
   | Pinline        of inline_info
   | Poutline       of outline_info
   | Pinterleave    of interleave_info located
@@ -812,6 +812,12 @@ and rwprgm = [
   | `IdAssign of pcodepos * pqsymbol
 ]
 
+and pcfold =
+  { side   : oside
+  ; start  : pcodepos
+  ; length : int option
+  ; eager : bool }
+
 (* -------------------------------------------------------------------- *)
 type include_exclude = [ `Include | `Exclude ]
 type pdbmap1 = {