PR: Cfold refactoring

src/ecPV.ml

@@ -47,6 +47,8 @@ module PVMap = struct
     Mnpv.find_opt (pvm m.pvm_env k) m.pvm_map
 
   let raw m = m.pvm_map
+
+
 end
 
 (* -------------------------------------------------------------------- *)

src/ecParser.mly

@@ -2991,7 +2991,10 @@ interleave_info:
     { Pinterleave info }
 
 | CFOLD s=side? c=codepos n=word?
-    { Pcfold (s, c, n) }
+    { Pcfold (s, c, n, false) }
+
+| CFOLD STAR s=side? c=codepos n=word?
+    { Pcfold (s, c, n, true) }
 
 | 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 (oside * pcodepos * int option * bool) (* side + 1st inst + n lines + eager? *)
   | Pinline        of inline_info
   | Poutline       of outline_info
   | Pinterleave    of interleave_info located

src/ecUtils.ml

@@ -626,6 +626,19 @@ module List = struct
       end
 
     in fun state xs -> aux state [] xs
+
+  (* FIXME: REMOVE *)
+  let fold_left_map_filter_while (f: 'a -> 'b -> ('a * ('c option)) interruptible) =
+    let rec aux (state: 'a) (acc: 'c list) (xs : 'b list) =
+      match xs with
+      | [] -> (state, List.rev acc, [])
+      | y :: ys -> begin
+        match f state y with
+        | `Continue (state, Some y) -> aux state (y :: acc) ys
+        | `Continue (state, None)   -> aux state acc ys
+        | `Interrupt                -> (state, List.rev acc, xs)
+      end
+    in fun state xs -> aux state [] xs
 end
 
 (* -------------------------------------------------------------------- *)

src/ecUtils.mli

@@ -309,6 +309,10 @@ module List : sig
        ('a -> 'b -> [`Interrupt | `Continue of 'a * 'c])
     -> 'a -> 'b list -> 'a * 'c list * 'b list
 
+  val fold_left_map_filter_while :
+       ('a -> 'b -> [`Interrupt | `Continue of 'a * ('c option)])
+    -> 'a -> 'b list -> 'a * 'c list * 'b list
+
   (* ------------------------------------------------------------------ *)
   val ksort:
         ?stable:bool -> ?rev:bool