unroll for: constant-propagate the counter

Author: strub

src/ecMatching.ml

@@ -34,9 +34,12 @@ module Position = struct
   type codepos    = (codepos1 * int) list * codepos1
   type codeoffset1 = [`ByOffset of int | `ByPosition of codepos1]
 
-  let shift ~(offset : int) ((o, p) : codepos1) : codepos1 =
+  let shift1 ~(offset : int) ((o, p) : codepos1) : codepos1 =
     (o + offset, p)
 
+  let shift ~(offset : int) ((outp, p) : codepos) : codepos =
+    (outp, shift1 ~offset p)
+
   let resolve_offset ~(base : codepos1) ~(offset : codeoffset1) : codepos1 =
     match offset with
     | `ByPosition pos -> pos

src/ecMatching.mli

@@ -30,7 +30,9 @@ module Position : sig
   type codepos     = (codepos1 * int) list * codepos1
   type codeoffset1 = [`ByOffset of int | `ByPosition of codepos1]
 
-  val shift : offset:int -> codepos1 -> codepos1
+  val shift1 : offset:int -> codepos1 -> codepos1
+  val shift  : offset:int -> codepos  -> codepos
+
   val resolve_offset : base:codepos1 -> offset:codeoffset1 -> codepos1
 end
 

src/phl/ecPhlLoopTx.ml

@@ -317,7 +317,14 @@ let process_unroll_for side cpos tc =
         [t_apply_hd h'; t_conseq_nm] ] tc
   in
 
-  let tcenv = t_doit 0 pos zs tc in FApi.t_onalli doi tcenv
+  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
+
+  Format.eprintf "[W]%d %d@." blen (List.length zs);
+  FApi.t_last (EcPhlCodeTx.t_cfold side cpos (Some clen)) tcenv
 
 (* -------------------------------------------------------------------- *)
 let process_unroll (side, cpos, for_) tc =

tests/cfold.ec

@@ -108,7 +108,6 @@ theory CfoldWhileUnroll.
   proc.
   cfold 1.
   unroll for 2.
-  cfold 1.
   by auto => />.
   qed.
 end CfoldWhileUnroll.