fix "unroll for" failure (InvalidCPos)

Keep a resolved version of the position so that it can be safely
reused later.

Author: strub

src/ecCorePrinting.ml

@@ -66,6 +66,8 @@ module type PrinterAPI = sig
   val pp_codepos1    : PPEnv.t -> EcMatching.Position.codepos1 pp
   val pp_codeoffset1 : PPEnv.t -> EcMatching.Position.codeoffset1 pp
 
+  val pp_codepos     : PPEnv.t -> EcMatching.Position.codepos pp
+
   (* ------------------------------------------------------------------ *)
   val pp_typedecl    : PPEnv.t -> (path * tydecl                  ) pp
   val pp_opdecl      : ?long:bool -> PPEnv.t -> (path * operator  ) pp

src/ecMatching.ml

@@ -30,8 +30,8 @@ module Position = struct
     | `ByMatch of int option * cp_match
   ]
 
-  type codepos1   = int * cp_base
-  type codepos    = (codepos1 * int) list * codepos1
+  type codepos1    = int * cp_base
+  type codepos     = (codepos1 * int) list * codepos1
   type codeoffset1 = [`ByOffset of int | `ByPosition of codepos1]
 
   let shift1 ~(offset : int) ((o, p) : codepos1) : codepos1 =
@@ -176,30 +176,41 @@ module Zipper = struct
     let (s, _) = split_at_cpos1 ~after:`No env cpos s in
     1 + List.length s
 
-  let zipper_at_nm_cpos1 (env : EcEnv.env) ((cp1, sub) : codepos1 * int) s zpr =
+  let zipper_at_nm_cpos1
+    (env        : EcEnv.env)
+    ((cp1, sub) : codepos1 * int)
+    (s          : stmt)
+    (zpr        : ipath)
+  : (ipath * stmt) * (codepos1 * int)
+  =
     let (s1, i, s2) = find_by_cpos1 env cp1 s in
+    let zpr =
+      match i.i_node, sub with
+      | Swhile (e, sw), 0 ->
+          (ZWhile (e, ((s1, s2), zpr)), sw)
 
-    match i.i_node, sub with
-    | Swhile (e, sw), 0 ->
-        (ZWhile (e, ((s1, s2), zpr)), sw)
-
-    | Sif (e, ifs1, ifs2), 0 ->
-        (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1)
+      | Sif (e, ifs1, ifs2), 0 ->
+          (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1)
 
-    | Sif (e, ifs1, ifs2), 1 ->
-        (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2)
+      | Sif (e, ifs1, ifs2), 1 ->
+          (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2)
 
-    | _ -> raise InvalidCPos
+      | _ -> raise InvalidCPos
+    in zpr, ((0, `ByPos (1 + List.length s1)), sub)
 
-  let zipper_of_cpos (env : EcEnv.env) ((nm, cp1) : codepos) s =
-    let zpr, s =
-      List.fold_left
+  let zipper_of_cpos_r (env : EcEnv.env) ((nm, cp1) : codepos) (s : stmt) =
+    let (zpr, s), nm =
+      List.fold_left_map
         (fun (zpr, s) nm1 -> zipper_at_nm_cpos1 env nm1 s zpr)
         (ZTop, s) nm in
 
     let s1, i, s2 = find_by_cpos1 env cp1 s in
+    let zpr = zipper s1 (i :: s2) zpr in
+
+    (zpr, (nm, (0, `ByPos (1 + List.length s1))))
 
-    zipper s1 (i :: s2) zpr
+  let zipper_of_cpos (env : EcEnv.env) (cp : codepos) (s : stmt) =
+    fst (zipper_of_cpos_r env cp s)
 
   let split_at_cpos1 env cpos1 s =
     split_at_cpos1 ~after:`Auto env cpos1 s

src/ecMatching.mli

@@ -73,7 +73,12 @@ module Zipper : sig
   val zipper : instr list -> instr list -> ipath -> zipper
 
   (* Return the zipper for the stmt [stmt] at code position [codepos].
-   * Raise [InvalidCPos] if [codepos] is not valid for [stmt]. *)
+   * Raise [InvalidCPos] if [codepos] is not valid for [stmt]. It also
+   * returns a input code-position, but fully resolved (i.e. with absolute
+   * positions only). The second variant simply throw away the second
+   * output.
+   *)
+  val zipper_of_cpos_r : env -> codepos -> stmt -> zipper * codepos
   val zipper_of_cpos : env -> codepos -> stmt -> zipper
 
   (* Zip the zipper, returning the corresponding statement *)

src/ecPrinting.ml

@@ -12,6 +12,7 @@ module P  = EcPath
 module EP = EcParser
 module BI = EcBigInt
 module EI = EcInductive
+module CP = EcMatching.Position
 
 module Ssym = EcSymbols.Ssym
 module Msym = EcSymbols.Msym
@@ -2112,7 +2113,7 @@ let pp_scvar ppe fmt vs =
   pp_list "@ " pp_grp fmt vs
 
 (* -------------------------------------------------------------------- *)
-let pp_codepos1 (ppe : PPEnv.t) (fmt : Format.formatter) ((off, cp) : EcMatching.Position.codepos1) =
+let pp_codepos1 (ppe : PPEnv.t) (fmt : Format.formatter) ((off, cp) : CP.codepos1) =
   let s : string =
     match cp with
     | `ByPos i ->
@@ -2141,11 +2142,19 @@ let pp_codepos1 (ppe : PPEnv.t) (fmt : Format.formatter) ((off, cp) : EcMatching
     Format.fprintf fmt "%s%s%d" s (if off < 0 then "-" else "+") (abs off)
 
 (* -------------------------------------------------------------------- *)
-let pp_codeoffset1 (ppe : PPEnv.t) (fmt : Format.formatter) (offset : EcMatching.Position.codeoffset1) =
+let pp_codeoffset1 (ppe : PPEnv.t) (fmt : Format.formatter) (offset : CP.codeoffset1) =
   match offset with
   | `ByPosition p -> Format.fprintf fmt "%a" (pp_codepos1 ppe) p
   | `ByOffset   o -> Format.fprintf fmt "%d" o
 
+(* -------------------------------------------------------------------- *)
+let pp_codepos (ppe : PPEnv.t) (fmt : Format.formatter) ((nm, cp1) : CP.codepos) =
+  let pp_nm (fmt : Format.formatter) ((cp, i) : CP.codepos1 * int) =
+    Format.eprintf "%a%s" (pp_codepos1 ppe) cp (if i = 0 then "." else "?")
+  in
+
+  Format.eprintf "%a%a" (pp_list "" pp_nm) nm (pp_codepos1 ppe) cp1
+
 (* -------------------------------------------------------------------- *)
 let pp_opdecl_pr (ppe : PPEnv.t) fmt (basename, ts, ty, op) =
   let ppe = PPEnv.add_locals ppe (List.map fst ts) in

src/phl/ecPhlLoopTx.ml

@@ -224,8 +224,12 @@ let process_unroll_for side cpos tc =
   let env  = FApi.tc1_env tc in
   let hyps = FApi.tc1_hyps tc in
   let _, c = EcLowPhlGoal.tc1_get_stmt side tc in
+
+  if not (List.is_empty (fst cpos)) then
+    tc_error !!tc "cannot use deep code position";
+
   let cpos = EcProofTyping.tc1_process_codepos tc (side, cpos) in
-  let z    = Zpr.zipper_of_cpos env cpos c in
+  let z, cpos = Zpr.zipper_of_cpos_r env cpos c in
   let pos  = 1 + List.length z.Zpr.z_head in
 
   (* Extract loop condition / body *)
@@ -323,7 +327,6 @@ let process_unroll_for side cpos tc =
   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
 
 (* -------------------------------------------------------------------- *)