Add option to bind new local variables with proc change

src/ecHiTacticals.ml

@@ -231,7 +231,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Prepl_stmt infos          -> EcPhlTrans.process_equiv_trans infos
     | Pprocrewrite (s, p, f)    -> EcPhlRewrite.process_rewrite s p f
     | Pprocrewriteat (x, f)     -> EcPhlRewrite.process_rewrite_at x f
-    | Pchangestmt (s, p, c)     -> EcPhlRewrite.process_change_stmt s p c
+    | Pchangestmt (s, b, p, c)  -> EcPhlRewrite.process_change_stmt s b p c 
     | Prwprgm infos             -> EcPhlRwPrgm.process_rw_prgm infos
     | Phoaresplit               -> EcPhlHoare.process_hoaresplit
   in

src/ecParser.mly

@@ -3261,11 +3261,11 @@ interleave_info:
 | LOSSLESS
     { Plossless }
 
-| PROC CHANGE side=side? pos=codepos_or_range COLON s=brace(stmt)
-    { Pchangestmt (side, PosOrRange pos, s) }
+| PROC CHANGE side=side? pos=codepos_or_range COLON b=option(bracket(ptybindings)) s=brace(stmt)
+    { Pchangestmt (side, b, PosOrRange pos, s) }
 
-| PROC CHANGE side=side? pos=codegap COLON s=brace(stmt)
-    { Pchangestmt (side, Gap pos, s) }
+| PROC CHANGE side=side? pos=codegap COLON b=option(bracket(ptybindings)) s=brace(stmt)
+    { Pchangestmt (side, b, Gap pos, s) }
 
 | PROC REWRITE side=side? pos=codepos f=pterm
     { Pprocrewrite (side, pos, `Rw f) }

src/ecParsetree.ml

@@ -824,7 +824,7 @@ type phltactic =
   | Prwprgm of rwprgm
   | Pprocrewrite   of side option * pcodepos * prrewrite
   | Pprocrewriteat of psymbol * ppterm
-  | Pchangestmt    of side option * prange1_or_insert * pstmt
+  | Pchangestmt    of side option * ptybindings option * prange1_or_insert * pstmt
   | Phoaresplit
 
     (* Eager *)

src/phl/ecPhlRewrite.ml

@@ -238,11 +238,12 @@ let process_rewrite_at
 let t_change_stmt
   (side : side option)
   (pos : EcMatching.Position.codegap_range)
+  (me : memenv)
   (s : stmt)
   (tc : tcenv1)
 =
   let env = FApi.tc1_env tc in
-  let me, stmt = EcLowPhlGoal.tc1_get_stmt side tc in
+  let _, stmt = EcLowPhlGoal.tc1_get_stmt side tc in 
 
   let zpr, (_,stmt, epilog), _nmr =
     EcMatching.Zipper.zipper_and_split_of_cgap_range env pos stmt in
@@ -342,10 +343,12 @@ let t_change_stmt
 (* -------------------------------------------------------------------- *)
 let process_change_stmt
   (side   : side option)
+  (binds  : ptybindings option)
   (pos    : prange1_or_insert)
   (s      : pstmt)
   (tc     : tcenv1)
 =
+  let hyps = FApi.tc1_hyps tc in
   let env = FApi.tc1_env tc in
 
   begin match side, (FApi.tc1_goal tc).f_node with
@@ -366,14 +369,41 @@ let process_change_stmt
 
   let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
 
-  let pos =
+  let pos = 
     let env = EcEnv.Memory.push_active_ss me env in
     EcTyping.trans_range1_or_insert ~memory:(fst me) env pos
   in
 
-  let s = match side with
-  | Some side -> EcProofTyping.tc1_process_prhl_stmt tc side s
-  | None -> EcProofTyping.tc1_process_Xhl_stmt tc s
+  (* Add the new variables *)
+  let bindings = 
+     binds
+  |> odfl []
+  |> List.map (fun (xs, ty) -> List.map (fun x -> (x, ty)) xs)
+  |> List.flatten 
+  |> List.map (fun (x, ty) ->
+      let ue = EcUnify.UniEnv.create (Some (EcEnv.LDecl.tohyps hyps).h_tvar) in
+      let ty = EcTyping.transty EcTyping.tp_tydecl env ue ty in
+      assert (EcUnify.UniEnv.closed ue);
+      let ty =
+        let subst = EcCoreSubst.Tuni.subst (EcUnify.UniEnv.close ue) in
+        EcCoreSubst.ty_subst subst ty in
+      let x = Option.map EcLocation.unloc (EcLocation.unloc x) in
+      let vr = EcAst.{ ov_name = x; ov_type = ty; } in
+      vr
+    )
+  in
+  let me, _ = EcMemory.bindall_fresh bindings me in
+
+  (* Process the given statement using the new bound variables *)
+  let env = EcEnv.Memory.push_active_ss me env in
+  let s = 
+    let ue = EcProofTyping.unienv_of_hyps hyps in
+    let s = EcTyping.transstmt env ue s in
+
+    assert (EcUnify.UniEnv.closed ue);
+
+    let sb = EcCoreSubst.Tuni.subst (EcUnify.UniEnv.close ue) in
+    EcCoreSubst.s_subst sb s 
   in
 
-  t_change_stmt side pos s tc
+  t_change_stmt side pos me s tc

src/phl/ecPhlRewrite.mli

@@ -8,4 +8,4 @@ val process_rewrite_rw    : side option -> pcodepos -> ppterm -> backward
 val process_rewrite_simpl : side option -> pcodepos -> backward
 val process_rewrite       : side option -> pcodepos -> prrewrite -> backward
 val process_rewrite_at    : psymbol -> ppterm -> backward
-val process_change_stmt   : side option -> prange1_or_insert -> pstmt -> backward
+val process_change_stmt   : side option -> ptybindings option -> prange1_or_insert -> pstmt -> backward

tests/procchange.ec

@@ -30,8 +30,7 @@ theory ProcChangeAssignEquiv.
   lemma L : equiv[M.f ~ M.f: true ==> true].
   proof.
   proc.
-    proc change {1} [1..3] : { x <- 3; }.
-
+    proc change {1} [1..3] : [y : int] { y <- 3; x <- y; }.
     wp. skip. smt().
   abort.
 end ProcChangeAssignEquiv.