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

@@ -33,15 +33,19 @@ let process_form_opt ?mv hyps pf oty =
     EcTyping.tyerror pf.EcLocation.pl_loc
       (LDecl.toenv hyps) EcTyping.FreeTypeVariables
 
+(* ------------------------------------------------------------------ *)
 let process_form ?mv hyps pf ty =
   process_form_opt ?mv hyps pf (Some ty)
 
+(* ------------------------------------------------------------------ *)
 let process_formula ?mv hyps pf =
   process_form hyps ?mv pf tbool
 
+(* ------------------------------------------------------------------ *)
 let process_xreal ?mv hyps pf =
   process_form hyps ?mv pf txreal
 
+(* ------------------------------------------------------------------ *)
 let process_dformula ?mv hyps pf =
   match pf with
   | Single pf -> Single(process_formula ?mv hyps pf)
@@ -50,13 +54,39 @@ 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_stmt hyps s =
+  let env = LDecl.toenv hyps in
+  let ue  = unienv_of_hyps hyps in
+  let s   = EcTyping.transstmt env ue s in
+
+  try
+    let ts = Tuni.subst (EcUnify.UniEnv.close ue) in
+    s_subst ts s
+  with EcUnify.UninstantiateUni ->
+    EcTyping.tyerror EcLocation._dummy env EcTyping.FreeTypeVariables
+
+(* ------------------------------------------------------------------ *)
 let process_exp hyps mode oty e =
   let env = LDecl.toenv hyps in
   let ue  = unienv_of_hyps hyps in
   let e   = EcTyping.transexpcast_opt env mode ue oty e in
   let ts  = Tuni.subst (EcUnify.UniEnv.close ue)  in
   e_subst ts e
 
+(* ------------------------------------------------------------------ *)
 let process_pattern hyps fp =
   let ps = ref Mid.empty in
   let ue = unienv_of_hyps hyps in

src/ecProofTyping.mli

@@ -21,6 +21,8 @@ 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_stmt     : LDecl.hyps -> pstmt -> EcAst.stmt
 val process_exp      : LDecl.hyps -> [`InProc|`InOp] -> ty option -> pexpr -> expr
 val process_pattern  : LDecl.hyps -> pformula -> ptnenv * form
 

src/phl/ecPhlRewrite.ml

@@ -230,19 +230,29 @@ let process_rewrite_at
   |> FApi.t_sub [t_pre; t_post; EcLowGoal.t_id]
 
 (* -------------------------------------------------------------------- *)
-(* [change] replaces a code range with [s] by generating:
+(* [t_change_stmt side pos ?me s] replaces a code range with [s] by
+   generating:
    - a local equivalence goal showing that the original fragment and [s]
      agree under the framed precondition on the variables they both read,
      and produce the same values for everything observable afterwards;
-   - the original program-logic goal with the selected range rewritten. *)
+   - the original program-logic goal with the selected range rewritten.
+
+   If [me] is provided, it is used as the memory environment (e.g. when
+   fresh local variables have been bound); otherwise, the memory
+   environment is taken from the goal. *)
 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 +352,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 +378,27 @@ 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 hyps = EcEnv.LDecl.push_active_ss me hyps in
+  let s = EcProofTyping.process_stmt hyps 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.