[internal] introduce general code position ranges for selecting code blocks.

src/ecMatching.ml

@@ -35,6 +35,7 @@ module Position = struct
   type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol]
   type codepos1      = int * cp_base
   type codepos       = (codepos1 * codepos_brsel) list * codepos1
+  type codepos_range = codepos * [`Base of codepos | `Offset of codepos1]
   type codeoffset1   = [`ByOffset of int | `ByPosition of codepos1]
 
   let shift1 ~(offset : int) ((o, p) : codepos1) : codepos1 =
@@ -60,8 +61,8 @@ module Zipper = struct
   type ('a, 'state) folder =
     env -> 'a -> 'state -> instr -> 'state * instr list
 
-  type ('a, 'state) folder_tl =
-    env -> 'a -> 'state -> instr -> instr list -> 'state * instr list
+  type ('a, 'state) folder_l =
+    env -> 'a -> 'state -> instr list -> 'state * instr list
 
   type spath_match_ctxt = {
     locals : (EcIdent.t * ty) list;
@@ -249,6 +250,17 @@ module Zipper = struct
   let zipper_of_cpos (env : EcEnv.env) (cp : codepos) (s : stmt) =
     fst (zipper_of_cpos_r env cp s)
 
+  let zipper_of_cpos_range env cpr s =
+    let top, bot = cpr in
+    let zpr = zipper_of_cpos env top s in
+    match bot with
+    | `Base cp ->
+      let path = (zipper_of_cpos env cp s).z_path in
+      if path <> zpr.z_path then
+        raise InvalidCPos;
+      zpr, snd cp
+    | `Offset cp1 -> zpr, cp1
+
   let split_at_cpos1 env cpos1 s =
     split_at_cpos1 ~after:`Auto env cpos1 s
 
@@ -288,23 +300,22 @@ module Zipper = struct
     in
       List.rev after
 
-  let fold_tl env cenv cpos f state s =
-    let zpr = zipper_of_cpos env cpos s in
-
-      match zpr.z_tail with
-      | []      -> raise InvalidCPos
-      | i :: tl -> begin
-          match f (odfl env zpr.z_env) cenv state i tl with
-          | (state', [i']) when i == i' && state == state' -> (state, s)
-          | (state', si  ) -> (state', zip { zpr with z_tail = si })
-      end
-
-  let fold env cenv cpos f state s =
-    let f e ce st i tl =
-      let state', si = f e ce st i in
-      state', si @ tl
-    in
-    fold_tl env cenv cpos f state s
+  let fold_range env cenv cpr f state s =
+    let zpr, cp = zipper_of_cpos_range env cpr s in
+    match zpr.z_tail with
+    | []      -> raise InvalidCPos
+    | i :: tl ->
+      let s, tl = split_at_cpos1 env cp (stmt tl) in
+      let env = odfl env zpr.z_env in
+      let state', si' = f env cenv state (i :: s) in
+      state', zip { zpr with z_tail = si' @ tl }
+
+  let map_range env cpr f s =
+    snd (fold_range env () cpr (fun env () _ si -> (), f env si) () s)
+
+  let fold env cenv cp f state s =
+    let f env cenv state si = f env cenv state (List.hd si) in
+    fold_range env cenv (cp, `Offset (cpos 0)) f state s
 
   let map env cpos f s =
     fst_map

src/ecMatching.mli

@@ -31,6 +31,7 @@ module Position : sig
   type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol]
   type codepos1      = int * cp_base
   type codepos       = (codepos1 * codepos_brsel) list * codepos1
+  type codepos_range = codepos * [`Base of codepos | `Offset of codepos1]
   type codeoffset1   = [`ByOffset of int | `ByPosition of codepos1]
 
   val shift1 : offset:int -> codepos1 -> codepos1
@@ -92,6 +93,13 @@ module Zipper : sig
   val zipper_of_cpos_r : env -> codepos -> stmt -> zipper * codepos
   val zipper_of_cpos : env -> codepos -> stmt -> zipper
 
+  (* Return the zipper for the stmt [stmt] from the start of the code position
+   * range [codepos_range]. It also returns a code position relative to
+   * the zipper that represents the final position in the range.
+   * Raise [InvalidCPos] if [codepos_range] is not a valid range for [stmt].
+   *)
+  val zipper_of_cpos_range : env -> codepos_range -> stmt -> zipper * codepos1
+
   (* Zip the zipper, returning the corresponding statement *)
   val zip : zipper -> stmt
 
@@ -104,7 +112,7 @@ module Zipper : sig
   val after : strict:bool -> zipper -> instr list list
 
   type ('a, 'state) folder = env -> 'a -> 'state -> instr -> 'state * instr list
-  type ('a, 'state) folder_tl = env -> 'a -> 'state -> instr -> instr list -> 'state * instr list
+  type ('a, 'state) folder_l = env -> 'a -> 'state -> instr list -> 'state * instr list
 
   (* [fold env v cpos f state s] create the zipper for [s] at [cpos], and apply
    * [f] to it, along with [v] and the state [state]. [f] must return the
@@ -115,14 +123,16 @@ module Zipper : sig
    *)
   val fold : env -> 'a -> codepos -> ('a, 'state) folder -> 'state -> stmt -> 'state * stmt
 
-  (* Same as above but using [folder_tl]. *)
-  val fold_tl : env -> 'a -> codepos -> ('a, 'state) folder_tl -> 'state -> stmt -> 'state * stmt
-
   (* [map cpos env f s] is a special case of [fold] where the state and the
    * out-of-band data are absent
    *)
   val map : env -> codepos -> (instr -> 'a * instr list) -> stmt -> 'a * stmt
 
+  (* Variants of the above but using code position ranges *)
+  val fold_range : env -> 'a -> codepos_range -> ('a, 'state) folder_l -> 'state -> stmt -> 'state * stmt
+  val map_range : env -> codepos_range -> (env -> instr list -> instr list) -> stmt -> stmt
+
+
 end
 
 (* -------------------------------------------------------------------- *)

src/ecTyping.ml

@@ -2194,7 +2194,11 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
         List.fold_right (fun (cp, up) bd ->
           let {pl_desc = cp; pl_loc = loc} = cp in
           let cp = trans_codepos env cp in
-          let change env _ _ i tl = (),
+          let change env si =
+            (* NOTE: There will always be a head element *)
+            let i, tl = List.takedrop 1 si in
+            let i = List.hd i in
+
             match up with
             | Pup_stmt sup ->
               eval_supdate env sup i @ tl
@@ -2203,8 +2207,7 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
           in
           let env = EcEnv.Memory.push_active !memenv env in
           try
-            let _, s = EcMatching.Zipper.fold_tl env () cp change () bd in
-            s
+            EcMatching.Zipper.map_range env (cp, `Offset (EcMatching.Zipper.cpos (-1))) change bd
           with
             | EcMatching.Zipper.InvalidCPos ->
               tyerror loc env (InvalidModUpdate MUE_InvalidCodePos);