feat(unroll-for): propagate constants after unrolling

Refactor unroll-for and add a variant that runs constant folding
immediately after unrolling to propagate constants introduced
by the transformation.

Co-Authored-By: Gustavo Delerue <gxdelerue@proton.me>
Co-Authored-By: Pierre-Yves Strub <pierre-yves@strub.nu>

Author: strub

src/ecParser.mly

@@ -3019,8 +3019,11 @@ interleave_info:
 | FUSION s=side? o=codepos NOT i=word AT d1=word COMMA d2=word
     { Pfusion (s, o, (i, (d1, d2))) }
 
-| UNROLL b=boption(FOR) s=side? o=codepos
-    { Punroll (s, o, b) }
+| UNROLL s=side? o=codepos
+    { Punroll (s, o, `While) }
+
+| UNROLL FOR b=boption(STAR) s=side? o=codepos
+    { Punroll (s, o, `For (not b)) }
 
 | SPLITWHILE s=side? o=codepos COLON c=expr %prec prec_tactic
     { Psplitwhile (c, s, o) }

src/ecParsetree.ml

@@ -731,7 +731,7 @@ type phltactic =
   | Pasyncwhile    of async_while_info
   | Pfission       of (oside * pcodepos * (int * (int * int)))
   | Pfusion        of (oside * pcodepos * (int * (int * int)))
-  | Punroll        of (oside * pcodepos * bool)
+  | Punroll        of (oside * pcodepos * [`While | `For of bool])
   | Psplitwhile    of (pexpr * oside * pcodepos)
   | Pcall          of oside * call_info gppterm
   | Pcallconcave   of (pformula * call_info gppterm)

src/phl/ecPhlLoopTx.ml

@@ -20,7 +20,7 @@ module TTC = EcProofTyping
 (* -------------------------------------------------------------------- *)
 type fission_t    = oside * pcodepos * (int * (int * int))
 type fusion_t     = oside * pcodepos * (int * (int * int))
-type unroll_t     = oside * pcodepos * bool
+type unroll_t     = oside * pcodepos * [`While | `For of bool]
 type splitwhile_t = pexpr * oside * pcodepos
 
 (* -------------------------------------------------------------------- *)
@@ -220,7 +220,7 @@ let process_splitwhile (b, side, cpos) tc =
   t_splitwhile b side cpos tc
 
 (* -------------------------------------------------------------------- *)
-let process_unroll_for side cpos tc =
+let process_unroll_for ~cfold side cpos tc =
   let env  = FApi.tc1_env tc in
   let hyps = FApi.tc1_hyps tc in
   let (goal_m, _), c = EcLowPhlGoal.tc1_get_stmt side tc in
@@ -327,16 +327,19 @@ let process_unroll_for side cpos tc =
   let tcenv = t_doit 0 pos zs tc in
   let tcenv = FApi.t_onalli doi tcenv in
 
-  let cpos = EcMatching.Position.shift ~offset:(-1) cpos in
-  let clen = blen * (List.length zs - 1) in
+  if cfold then begin
+    let cpos = EcMatching.Position.shift ~offset:(-1) cpos in
+    let clen = blen * (List.length zs - 1) in
 
-  FApi.t_last (EcPhlCodeTx.t_cfold side cpos (Some clen)) tcenv
+    FApi.t_last (EcPhlCodeTx.t_cfold side cpos (Some clen)) tcenv
+  end else tcenv
 
 (* -------------------------------------------------------------------- *)
 let process_unroll (side, cpos, for_) tc =
-  if for_ then
-    process_unroll_for side cpos tc
-  else begin
+  match for_ with
+  | `While ->
     let cpos = EcLowPhlGoal.tc1_process_codepos tc (side, cpos) in
     t_unroll side cpos tc
-  end
+
+  | `For cfold ->
+    process_unroll_for ~cfold side cpos tc

src/phl/ecPhlLoopTx.mli

@@ -13,10 +13,10 @@ val t_splitwhile : expr -> oside -> codepos -> backward
 (* -------------------------------------------------------------------- *)
 type fission_t    = oside * pcodepos * (int * (int * int))
 type fusion_t     = oside * pcodepos * (int * (int * int))
-type unroll_t     = oside * pcodepos * bool
+type unroll_t     = oside * pcodepos * [`While | `For of bool]
 type splitwhile_t = pexpr * oside * pcodepos
 
-val process_unroll_for : oside -> pcodepos -> backward
+val process_unroll_for : cfold:bool -> oside -> pcodepos -> backward
 val process_fission    : fission_t -> backward
 val process_fusion     : fusion_t -> backward
 val process_unroll     : unroll_t -> backward