Propagate extended code positions to more tactics

Nearly all program tactics (`wp`, `sp`, ...) can now take extended
code positions as arguments.

Moreover, extended code positions have been extended s.t. they
can now target a assignment with a specific variable. The syntax is
`^x<-` where `x` is the program variable name.

src/ecCorePrinting.ml

@@ -24,7 +24,7 @@ module type PrinterAPI = sig
 
   (* ------------------------------------------------------------------ *)
   val string_of_hcmp : EcFol.hoarecmp -> string
-  val string_of_cpos1 : EcParsetree.codepos1 -> string
+  val string_of_cpos1 : EcMatching.Position.codepos1 -> string
 
   (* ------------------------------------------------------------------ *)
   type 'a pp = Format.formatter -> 'a -> unit

src/ecHiTacticals.ml

@@ -174,9 +174,9 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pskip                     -> EcPhlSkip.t_skip
     | Papp info                 -> EcPhlApp.process_app info
     | Pwp wp                    -> EcPhlWp.process_wp wp
-    | Psp sp                    -> EcPhlSp.t_sp sp
+    | Psp sp                    -> EcPhlSp.process_sp sp
     | Prcond (side, b, i)       -> EcPhlRCond.process_rcond side b i
-    | Prmatch (side, c, i)      -> EcPhlRCond.t_rcond_match side c i
+    | Prmatch (side, c, i)      -> EcPhlRCond.process_rcond_match side c i
     | Pcond info                -> EcPhlHiCond.process_cond info
     | Pmatch infos              -> EcPhlHiCond.process_match infos
     | Pwhile (side, info)       -> EcPhlWhile.process_while side info

src/ecLowPhlGoal.ml

@@ -9,6 +9,7 @@ open EcFol
 open EcEnv
 open EcPV
 open EcCoreGoal
+open EcMatching.Position
 
 module Zpr = EcMatching.Zipper
 
@@ -266,19 +267,19 @@ let set_pre ~pre f =
 (* -------------------------------------------------------------------- *)
 exception InvalidSplit of codepos1
 
-let s_split i s =
+let s_split env i s =
   let module Zpr = EcMatching.Zipper in
-  try  Zpr.split_at_cpos1 i s
+  try  Zpr.split_at_cpos1 env i s
   with Zpr.InvalidCPos -> raise (InvalidSplit i)
 
-let s_split_i i s =
+let s_split_i env i s =
   let module Zpr = EcMatching.Zipper in
-  try  Zpr.find_by_cpos1 ~rev:false i s
+  try  Zpr.find_by_cpos1 ~rev:false env i s
   with Zpr.InvalidCPos -> raise (InvalidSplit i)
 
-let o_split ?rev i s =
+let o_split ?rev env i s =
   let module Zpr = EcMatching.Zipper in
-  try  Zpr.may_split_at_cpos1 ?rev i s
+  try  Zpr.may_split_at_cpos1 ?rev env i s
   with Zpr.InvalidCPos -> raise (InvalidSplit (oget i))
 
 (* -------------------------------------------------------------------- *)
@@ -576,13 +577,15 @@ type 'a zip_t =
 
 let t_fold f (cenv : code_txenv) (cpos : codepos) (_ : form * form) (state, s) =
   try
-    let (me, f) = Zpr.fold cenv cpos f state s in
+    let env = EcEnv.LDecl.toenv (snd cenv) in
+    let (me, f) = Zpr.fold env cenv cpos f state s in
       ((me, f, []) : memenv * _ * form list)
   with Zpr.InvalidCPos -> tc_error (fst cenv) "invalid code position"
 
 let t_zip f (cenv : code_txenv) (cpos : codepos) (prpo : form * form) (state, s) =
   try
-    let (me, zpr, gs) = f cenv prpo state (Zpr.zipper_of_cpos cpos s) in
+    let env = EcEnv.LDecl.toenv (snd cenv) in
+    let (me, zpr, gs) = f cenv prpo state (Zpr.zipper_of_cpos env cpos s) in
       ((me, Zpr.zip zpr, gs) : memenv * _ * form list)
   with Zpr.InvalidCPos -> tc_error (fst cenv) "invalid code position"
 

src/ecMatching.ml

@@ -6,16 +6,38 @@
 open EcUtils
 open EcMaps
 open EcIdent
-open EcParsetree
 open EcEnv
 open EcAst
 open EcTypes
 open EcModules
 open EcFol
 open EcGenRegexp
 
+(* -------------------------------------------------------------------- *)
+module Position = struct
+  type cp_match = [
+    | `If
+    | `While
+    | `Assign of lvmatch
+    | `Sample
+    | `Call
+  ]
+
+  and lvmatch = [ `LvmNone | `LvmVar of EcTypes.prog_var ]
+
+  type cp_base = [
+    | `ByPos of int
+    | `ByMatch of int option * cp_match
+  ]
+
+  type codepos1   = int * cp_base
+  type codepos    = (codepos1 * int) list * codepos1
+end
+
 (* -------------------------------------------------------------------- *)
 module Zipper = struct
+  open Position
+
   exception InvalidCPos
 
   module P = EcPath
@@ -41,7 +63,11 @@ module Zipper = struct
 
   let zipper hd tl zpr = { z_head = hd; z_tail = tl; z_path = zpr; }
 
-  let find_by_cp_match ((i, cm) : int option * cp_match) (s : stmt) =
+  let find_by_cp_match
+    (env     : EcEnv.env)
+    ((i, cm) : int option * cp_match)
+    (s       : stmt)
+  =
     let rec progress (acc : instr list) (s : instr list) (i : int) =
       if i <= 0 then
         let shd = oget (List.Exceptionless.hd acc) in
@@ -57,10 +83,19 @@ module Zipper = struct
         match ir.i_node, cm with
         | Swhile _, `While  -> i-1
         | Sif    _, `If     -> i-1
-        | Sasgn  _, `Assign -> i-1
         | Srnd   _, `Sample -> i-1
         | Scall  _, `Call   -> i-1
-        | _       , _       -> i
+
+        | Sasgn  (lv, _), `Assign lvm -> begin
+            match lv, lvm with
+            | _, `LvmNone -> i-1
+            | LvVar (pv, _), `LvmVar pvm
+                 when EcReduction.EqTest.for_pv env pv pvm
+              -> i-1
+            | _ -> i
+          end
+
+        | _ -> i
 
       in progress (ir :: acc) s i
 
@@ -76,7 +111,7 @@ module Zipper = struct
     | false -> (s1, ir, s2)
     | true  -> (s2, ir, s1)
 
-  let split_at_cp_base ~after (cb : cp_base) (s : stmt) =
+  let split_at_cp_base ~after (env : EcEnv.env) (cb : cp_base) (s : stmt) =
     match cb with
     | `ByPos i -> begin
         let i = if i < 0 then List.length s.s_node + i else i in
@@ -85,14 +120,14 @@ module Zipper = struct
       end
 
     | `ByMatch (i, cm) ->
-        let (s1, i, s2) = find_by_cp_match (i, cm) s in
+        let (s1, i, s2) = find_by_cp_match env (i, cm) s in
 
         match after with
         | false -> (List.rev s1, i :: s2)
         | true  -> (List.rev_append s1 [i], s2)
 
-  let split_at_cpos1 ~after ((ipos, cb) : codepos1) s =
-    let (s1, s2) = split_at_cp_base ~after cb s in
+  let split_at_cpos1 ~after (env : EcEnv.env) ((ipos, cb) : codepos1) s =
+    let (s1, s2) = split_at_cp_base ~after env cb s in
 
     let (s1, s2) =
       match ipos with
@@ -112,13 +147,13 @@ module Zipper = struct
 
     in (s1, s2)
 
-  let find_by_cpos1 ?(rev = true) (cpos1 : codepos1) s =
-    match split_at_cpos1 ~after:false cpos1 s with
+  let find_by_cpos1 ?(rev = true) (env : EcEnv.env) (cpos1 : codepos1) s =
+    match split_at_cpos1 ~after:false env cpos1 s with
     | (s1, i :: s2) -> ((if rev then List.rev s1 else s1), i, s2)
     | _ -> raise InvalidCPos
 
-  let zipper_at_nm_cpos1 ((cp1, sub) : codepos1 * int) s zpr =
-    let (s1, i, s2) = find_by_cpos1 cp1 s in
+  let zipper_at_nm_cpos1 (env : EcEnv.env) ((cp1, sub) : codepos1 * int) s zpr =
+    let (s1, i, s2) = find_by_cpos1 env cp1 s in
 
     match i.i_node, sub with
     | Swhile (e, sw), 0 ->
@@ -132,23 +167,23 @@ module Zipper = struct
 
     | _ -> raise InvalidCPos
 
-  let zipper_of_cpos ((nm, cp1) : codepos) s =
+  let zipper_of_cpos (env : EcEnv.env) ((nm, cp1) : codepos) s =
     let zpr, s =
       List.fold_left
-        (fun (zpr, s) nm1 -> zipper_at_nm_cpos1 nm1 s zpr)
+        (fun (zpr, s) nm1 -> zipper_at_nm_cpos1 env nm1 s zpr)
         (ZTop, s) nm in
 
-    let s1, i, s2 = find_by_cpos1 cp1 s in
+    let s1, i, s2 = find_by_cpos1 env cp1 s in
 
     zipper s1 (i :: s2) zpr
 
-  let split_at_cpos1 cpos1 s =
-    split_at_cpos1 ~after:true cpos1 s
+  let split_at_cpos1 env cpos1 s =
+    split_at_cpos1 ~after:true env cpos1 s
 
-  let may_split_at_cpos1 ?(rev = false) cpos1 s =
+  let may_split_at_cpos1 ?(rev = false) env cpos1 s =
     ofdfl
       (fun () -> if rev then (s.s_node, []) else ([], s.s_node))
-      (omap (split_at_cpos1^~ s) cpos1)
+      (omap ((split_at_cpos1 env)^~ s) cpos1)
 
   let rec zip i ((hd, tl), ip) =
     let s = stmt (List.rev_append hd (List.ocons i tl)) in
@@ -178,21 +213,21 @@ module Zipper = struct
     in
       List.rev after
 
-  let fold env cpos f state s =
-    let zpr = zipper_of_cpos cpos s in
+  let fold 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 env state i with
+          match f cenv state i with
           | (state', [i']) when i == i' && state == state' -> (state, s)
           | (state', si  ) -> (state', zip { zpr with z_tail = si @ tl })
       end
 
-  let map cpos f s =
+  let map env cpos f s =
     fst_map
       Option.get
-      (fold () cpos (fun () _ i -> fst_map some (f i)) None s)
+      (fold env () cpos (fun () _ i -> fst_map some (f i)) None s)
 end
 
 (* -------------------------------------------------------------------- *)

src/ecMatching.mli

@@ -1,7 +1,6 @@
 (* -------------------------------------------------------------------- *)
 open EcMaps
 open EcUid
-open EcParsetree
 open EcIdent
 open EcTypes
 open EcModules
@@ -10,8 +9,31 @@ open EcUnify
 open EcEnv
 open EcGenRegexp
 
+(* -------------------------------------------------------------------- *)
+module Position : sig
+  type cp_match = [
+    | `If
+    | `While
+    | `Assign of lvmatch
+    | `Sample
+    | `Call
+  ]
+
+  and lvmatch = [ `LvmNone | `LvmVar of EcTypes.prog_var ]
+
+  type cp_base = [
+    | `ByPos of int
+    | `ByMatch of int option * cp_match
+  ]
+
+  type codepos1   = int * cp_base
+  type codepos    = (codepos1 * int) list * codepos1
+end
+
 (* -------------------------------------------------------------------- *)
 module Zipper : sig
+  open Position
+
   type ipath =
   | ZTop
   | ZWhile  of expr * spath
@@ -32,18 +54,18 @@ module Zipper : sig
   val cpos : int -> codepos1
 
   (* Split a statement from a top-level position (codepos1) *)
-  val find_by_cpos1  : ?rev:bool -> codepos1 -> stmt -> instr list * instr * instr list
-  val split_at_cpos1 : codepos1 -> stmt -> instr list * instr list
+  val find_by_cpos1  : ?rev:bool -> env -> codepos1 -> stmt -> instr list * instr * instr list
+  val split_at_cpos1 : env -> codepos1 -> stmt -> instr list * instr list
 
   (* Split a statement from an optional top-level position (codepos1) *)
-  val may_split_at_cpos1 : ?rev:bool -> codepos1 option -> stmt -> instr list * instr list
+  val may_split_at_cpos1 : ?rev:bool -> env -> codepos1 option -> stmt -> instr list * instr list
 
   (* [zipper] soft constructor *)
   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]. *)
-  val zipper_of_cpos : codepos -> stmt -> zipper
+  val zipper_of_cpos : env -> codepos -> stmt -> zipper
 
   (* Zip the zipper, returning the corresponding statement *)
   val zip : zipper -> stmt
@@ -58,19 +80,19 @@ module Zipper : sig
 
   type ('a, 'state) folder = 'a -> 'state -> instr -> 'state * instr list
 
-  (* [fold v cpos f state s] create the zipper for [s] at [cpos], and apply
+  (* [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
    * new [state] and a new [zipper]. These last are directly returned.
    *
    * Raise [InvalidCPos] if [cpos] is not valid for [s], or any exception
    * raised by [f].
    *)
-  val fold : 'a -> codepos -> ('a, 'state) folder -> 'state -> stmt -> 'state * stmt
+  val fold : env -> 'a -> codepos -> ('a, 'state) folder -> 'state -> stmt -> 'state * stmt
 
-  (* [map cpos f s] is a special case of [fold] where the state and the
+  (* [map cpos env f s] is a special case of [fold] where the state and the
    * out-of-band data are absent
    *)
-  val map : codepos -> (instr -> 'a * instr list) -> stmt -> 'a * stmt
+  val map : env -> codepos -> (instr -> 'a * instr list) -> stmt -> 'a * stmt
 
 end
 

src/ecParser.mly

@@ -1434,19 +1434,21 @@ param_decl:
 (* -------------------------------------------------------------------- *)
 (* Statements                                                           *)
 
-lvalue_u:
+lvalue_var:
 | x=loc(fident)
    { match lqident_of_fident x.pl_desc with
      | None   -> parse_error x.pl_loc None
-     | Some v -> PLvSymbol (mk_loc x.pl_loc v) }
+     | Some v -> mk_loc x.pl_loc v }
+
+lvalue_u:
+| x=lvalue_var
+   { PLvSymbol x }
 
 | LPAREN p=plist2(qident, COMMA) RPAREN
    { PLvTuple p }
 
-| x=loc(fident) DLBRACKET ti=tvars_app? es=plist1(expr, COMMA) RBRACKET
-   { match lqident_of_fident x.pl_desc with
-     | None   -> parse_error x.pl_loc None
-     | Some v -> PLvMap (mk_loc x.pl_loc v, ti, es) }
+| x=lvalue_var DLBRACKET ti=tvars_app? e=plist1(expr, COMMA) RBRACKET
+   { PLvMap (x, ti, e) }
 
 %inline lvalue:
 | x=loc(lvalue_u) { x }
@@ -2602,21 +2604,26 @@ tac_dir:
 | empty { Backs }
 
 icodepos_r:
-| IF       { (`If     :> cp_match) }
-| WHILE    { (`While  :> cp_match) }
-| LARROW   { (`Assign :> cp_match) }
-| LESAMPLE { (`Sample :> cp_match) }
-| LEAT     { (`Call   :> cp_match) }
+| IF       { (`If     :> pcp_match) }
+| WHILE    { (`While  :> pcp_match) }
+| LESAMPLE { (`Sample :> pcp_match) }
+| LEAT     { (`Call   :> pcp_match) }
+
+| lvm=lvmatch LARROW { (`Assign lvm :> pcp_match) }
+
+lvmatch:
+| empty        { (`LvmNone  :> plvmatch) }
+| x=lvalue_var { (`LvmVar x :> plvmatch) }
 
 %inline icodepos:
  | HAT x=icodepos_r { x }
 
 codepos1_wo_off:
 | i=sword
-    { (`ByPos i :> cp_base) }
+    { (`ByPos i :> pcp_base) }
 
 | k=icodepos i=option(brace(sword))
-    { (`ByMatch (i, k) :> cp_base) }
+    { (`ByMatch (i, k) :> pcp_base) }
 
 codepos1:
 | cp=codepos1_wo_off { (0, cp) }