New code-position variants: ^()<-, and ^(x)<- to match tuple assignme…

…nts.

src/ecMatching.ml

@@ -19,6 +19,7 @@ module Position = struct
     | `If
     | `While
     | `Assign of lvmatch
+    | `AssignTuple of lvmatch
     | `Sample of lvmatch
     | `Call   of lvmatch
     | `Match
@@ -122,6 +123,14 @@ module Zipper = struct
               -> i-1
             | _ -> i
           end
+        | Sasgn (lv, _), `AssignTuple lvm -> begin
+            match lv, lvm with
+            | LvTuple _, `LvmNone -> i-1
+            | LvTuple pvs, `LvmVar pvm
+                  when List.exists (fun (pv, _) -> EcReduction.EqTest.for_pv env pv pvm) pvs
+              -> i-1
+            | _ -> i
+          end
 
         | _ -> i
 

src/ecMatching.mli

@@ -16,6 +16,7 @@ module Position : sig
     | `While
     | `Match
     | `Assign of lvmatch
+    | `AssignTuple of lvmatch
     | `Sample of lvmatch
     | `Call   of lvmatch
   ]

src/ecParser.mly

@@ -1462,9 +1462,9 @@ update_cond:
 | MINUS bs=branch_select { Pupc_del bs }
 
 fun_update:
-| cp=loc(codepos) sup=update_stmt 
+| cp=loc(codepos) sup=update_stmt
   { List.map (fun v -> (cp, Pup_stmt v)) sup }
-| cp=loc(codepos) cup=update_cond 
+| cp=loc(codepos) cup=update_cond
   { [(cp, Pup_cond cup)] }
 
 (* -------------------------------------------------------------------- *)
@@ -2486,6 +2486,7 @@ icodepos_r:
 | lvm=lvmatch LESAMPLE { (`Sample lvm :> pcp_match) }
 | lvm=lvmatch LEAT { (`Call lvm :> pcp_match) }
 | lvm=lvmatch LARROW { (`Assign lvm :> pcp_match) }
+| lvm=paren(lvmatch)  LARROW { (`AssignTuple lvm :> pcp_match) }
 
 lvmatch:
 | empty        { (`LvmNone  :> plvmatch) }
@@ -3703,7 +3704,7 @@ hintoption:
 | x=lident {
     match unloc x with
     | "rigid" -> `Rigid
-    | _ -> 
+    | _ ->
         parse_error x.pl_loc
             (Some ("invalid option: " ^ (unloc x)))
   }
@@ -3716,7 +3717,7 @@ hint:
     { { ht_local   = local;
         ht_prio    = prio;
         ht_base    = base ;
-        ht_names   = l; 
+        ht_names   = l;
         ht_options = odfl [] opts; } }
 
 (* -------------------------------------------------------------------- *)

src/ecParsetree.ml

@@ -41,6 +41,7 @@ type pcp_match = [
   | `While
   | `Match
   | `Assign of plvmatch
+  | `AssignTuple of plvmatch
   | `Sample of plvmatch
   | `Call of plvmatch
 ]

src/ecPrinting.ml

@@ -452,8 +452,8 @@ let pp_shorten_path (cond : P.path -> qsymbol -> bool) (fmt : Format.formatter)
   | None ->
     Format.fprintf fmt "%a" EcSymbols.pp_qsymbol plong
   | Some pshort ->
-    Format.fprintf fmt "%a (shorten name: %a)" 
-    EcSymbols.pp_qsymbol plong 
+    Format.fprintf fmt "%a (shorten name: %a)"
+    EcSymbols.pp_qsymbol plong
     EcSymbols.pp_qsymbol pshort
 
 (* -------------------------------------------------------------------- *)
@@ -940,7 +940,7 @@ let pp_tuple (type v)
 
 let pp_proji (type v)
   (ppe    : PPEnv.t)
-  (pp_sub : PPEnv.t -> opprec * iassoc -> v pp) 
+  (pp_sub : PPEnv.t -> opprec * iassoc -> v pp)
   (fmt    : Format.formatter)
   ((e, i) : v * int)
 =
@@ -1601,7 +1601,7 @@ and try_pp_chained_orderings
       let sb  = EcMatching.MEV.assubst ue ev ppe.ppe_env in
       let i1  = Fsubst.f_subst sb i1 in
       let i2  = Fsubst.f_subst sb i2 in
-  
+
       (op, tvi), (i1, i2)
     end
 
@@ -1626,7 +1626,7 @@ and try_pp_chained_orderings
       le;
 
     let acc = (op, tvi, i2) :: acc in
-    
+
     Option.fold ~none:(i1, acc) ~some:(collect acc (Some i1)) f1
   in
     match collect [] None f with
@@ -1720,8 +1720,8 @@ and match_pp_notations
   let nts = EcEnv.Op.get_notations ~head ppe.PPEnv.ppe_env in
 
   List.find_map_opt try_notation nts
-          
-            
+
+
 and try_pp_notations
   (ppe   : PPEnv.t)
   (outer : opprec * iassoc)
@@ -2269,6 +2269,8 @@ let pp_codepos1 (ppe : PPEnv.t) (fmt : Format.formatter) ((off, cp) : CP.codepos
             | `Call (`LvmVar pv) -> Format.asprintf "%a<@" (pp_pv ppe) pv
             | `Assign `LvmNone -> "<-"
             | `Assign (`LvmVar pv) -> Format.asprintf "%a<-" (pp_pv ppe) pv
+            | `AssignTuple `LvmNone -> "()<-"
+            | `AssignTuple (`LvmVar pv) -> Format.asprintf "(%a)<-" (pp_pv ppe) pv
           in Format.asprintf "^%s" k in
 
         match i with
@@ -2290,7 +2292,7 @@ let pp_codeoffset1 (ppe : PPEnv.t) (fmt : Format.formatter) (offset : CP.codeoff
 (* -------------------------------------------------------------------- *)
 let pp_codepos (ppe : PPEnv.t) (fmt : Format.formatter) ((nm, cp1) : CP.codepos) =
   let pp_nm (fmt : Format.formatter) ((cp, bs) : CP.codepos1 * CP.codepos_brsel) =
-    let bs = 
+    let bs =
       match bs with
       | `Cond  true  -> "."
       | `Cond  false -> "?"
@@ -3030,7 +3032,7 @@ let pp_rwbase ppe fmt (p, rws) =
 let pp_solvedb ppe fmt (db: (int * (P.path * _) list) list) =
   List.iter (fun (lvl, ps) ->
     Format.fprintf fmt "[%3d] %a\n%!"
-      lvl 
+      lvl
       (pp_list ", " (pp_axhnt ppe))
       ps)
   db;
@@ -3050,7 +3052,7 @@ let pp_solvedb ppe fmt (db: (int * (P.path * _) list) list) =
           match ir with
           | `Default -> ""
           | `Rigid -> " (rigid)" in
-        
+
         Format.fprintf fmt "%a%s\n\n%!" (pp_axiom ppe) ax ir)
       lemmas
   end
@@ -3563,7 +3565,7 @@ let pp_by_theory
   (pp   : PPEnv.t -> (EcPath.path * 'a) pp)
   (fmt  : Format.formatter)
   (xs   : (EcPath.path * 'a) list)
-= 
+=
   let tr =
     List.fold_left (fun tr ((p, _) as x) ->
       Trie.add (EcPath.tolist (oget (EcPath.prefix p))) x tr

src/ecTyping.ml

@@ -3081,7 +3081,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt =
     | PFdecimal (n, f) ->
         f_decimal (n, f)
 
-    | PFtuple pes ->        
+    | PFtuple pes ->
         let esig = List.map (fun _ -> EcUnify.UniEnv.fresh ue) pes in
         tt |> oiter (fun tt -> unify_or_fail env ue f.pl_loc  ~expct:tt (ttuple esig));
         let es = List.map2 (fun tt pe -> transf env ~tt pe) esig pes in
@@ -3608,6 +3608,8 @@ and trans_cp_match ?(memory : memory option) (env : EcEnv.env) (p : pcp_match) :
     `Call (trans_lv_match ?memory env lv)
   | `Assign lv ->
     `Assign (trans_lv_match ?memory env lv)
+  | `AssignTuple lv ->
+    `AssignTuple (trans_lv_match ?memory env lv)
 (* -------------------------------------------------------------------- *)
 and trans_cp_base ?(memory : memory option) (env : EcEnv.env) (p : pcp_base) : cp_base =
   match p with

tests/codepos-tuple-name.ec

@@ -0,0 +1,23 @@
+(* -------------------------------------------------------------------- *)
+require import AllCore.
+
+module M = {
+  proc f() = {
+    var x : int;
+    var y : int;
+    var z : int;
+
+    y <- 1;
+    (x, z) <- (0, 0);
+    return y;
+  }
+}.
+
+op p : int -> bool.
+
+lemma L : hoare[M.f : true ==> p res].
+proof.
+proc.
+swap ^()<- @ ^y<-.
+swap ^y<- @ ^(x)<-.
+abort.