proc change: support binding fresh local variables

Allow `proc change` to introduce new local memory variables via an
optional `[x : ty, ...]` annotation. The replacement statement can
then reference these freshly bound variables.

Author: Gustavo2622

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/ecProofTyping.ml

@@ -50,6 +50,17 @@ let process_dformula ?mv hyps pf =
     let f = process_xreal ?mv hyps pf in
     Double(p,f)
 
+let process_type hyps pty =
+  let env = LDecl.toenv hyps in
+  let ue  = unienv_of_hyps hyps in
+  let ty  = EcTyping.transty EcTyping.tp_tydecl env ue pty in
+
+  if not (EcUnify.UniEnv.closed ue) then
+    EcTyping.tyerror (EcLocation.loc pty) env EcTyping.FreeTypeVariables;
+
+  let ts = Tuni.subst (EcUnify.UniEnv.close ue) in
+  EcCoreSubst.ty_subst ts ty
+
 let process_exp hyps mode oty e =
   let env = LDecl.toenv hyps in
   let ue  = unienv_of_hyps hyps in

src/ecProofTyping.mli

@@ -21,6 +21,7 @@ val pf_check_tvi   : proofenv -> ty_params -> EcUnify.tvi -> unit
 val process_form_opt : ?mv:metavs -> LDecl.hyps -> pformula -> ty option -> form
 val process_form     : ?mv:metavs -> LDecl.hyps -> pformula -> ty -> form
 val process_formula  : ?mv:metavs -> LDecl.hyps -> pformula -> form
+val process_type     : LDecl.hyps -> pty -> ty
 val process_exp      : LDecl.hyps -> [`InProc|`InOp] -> ty option -> pexpr -> expr
 val process_pattern  : LDecl.hyps -> pformula -> ptnenv * form
 

src/phl/ecPhlRewrite.ml

@@ -236,13 +236,18 @@ let process_rewrite_at
      and produce the same values for everything observable afterwards;
    - the original program-logic goal with the selected range rewritten. *)
 let t_change_stmt
-  (side : side option)
-  (pos : EcMatching.Position.codegap_range)
-  (s : stmt)
-  (tc : tcenv1)
+   (side : side option)
+   (pos  : EcMatching.Position.codegap_range)
+  ?(me   : memenv option)
+   (s    : stmt)
+   (tc   : tcenv1)
 =
   let env = FApi.tc1_env tc in
-  let me, stmt = EcLowPhlGoal.tc1_get_stmt side tc in
+
+  let me, stmt =
+    let metc, stmt = EcLowPhlGoal.tc1_get_stmt side tc in
+    (odfl metc me, stmt)
+  in
 
   let zpr, (_,stmt, epilog), _nmr =
     EcMatching.Zipper.zipper_and_split_of_cgap_range env pos stmt in
@@ -342,10 +347,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 +373,35 @@ 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 ty = EcProofTyping.process_type hyps ty in
+      let x = Option.map EcLocation.unloc (EcLocation.unloc x) in
+      EcAst.{ ov_name = x; ov_type = ty; }
+    )
+  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.