Proc change multiline to range + deep code position

Author: Gustavo2622

src/ecMatching.ml

@@ -268,6 +268,14 @@ module Zipper = struct
     end
     | `Offset cp1 -> zpr, cp1
 
+  let zipper_and_split_of_cpos_range env cpr s =
+    let zpr, cp = zipper_of_cpos_range env cpr s in
+    match zpr.z_tail with
+    | []      -> raise InvalidCPos
+    | i :: tl ->
+      let s, tl = split_at_cpos1 ~after:`Auto env cp (stmt tl) in
+      (zpr, cp), ((i::s), tl)
+
   let split_at_cpos1 env cpos1 s =
     split_at_cpos1 ~after:`Auto env cpos1 s
 
@@ -308,14 +316,10 @@ module Zipper = struct
       List.rev after
 
   let fold_range env cenv cpr f state s =
-    let zpr, cp = zipper_of_cpos_range env cpr s in
-    match zpr.z_tail with
-    | []      -> raise InvalidCPos
-    | i :: tl ->
-      let s, tl = split_at_cpos1 env cp (stmt tl) in
-      let env = odfl env zpr.z_env in
-      let state', si' = f env cenv state (i :: s) in
-      state', zip { zpr with z_tail = si' @ tl }
+    let (zpr, _), (s, tl) = zipper_and_split_of_cpos_range env cpr s in
+    let env = odfl env zpr.z_env in
+    let state', si' = f env cenv state s in
+    state', zip { zpr with z_tail = si' @ tl }
 
   let map_range env cpr f s =
     snd (fold_range env () cpr (fun env () _ si -> (), f env si) () s)

src/ecMatching.mli

@@ -99,6 +99,7 @@ module Zipper : sig
    * Raise [InvalidCPos] if [codepos_range] is not a valid range for [stmt].
    *)
   val zipper_of_cpos_range : env -> codepos_range -> stmt -> zipper * codepos1
+  val zipper_and_split_of_cpos_range : env -> codepos_range -> stmt -> (zipper * codepos1) * (instr list * instr list)
 
   (* Zip the zipper, returning the corresponding statement *)
   val zip : zipper -> stmt

src/ecParser.mly

@@ -3194,10 +3194,8 @@ interleave_info:
 | LOSSLESS
     { Plossless }
 
-| PROC CHANGE side=side? pos=loc(codepos) offset=codeoffset1 COLON s=brace(stmt)
-   { if not (List.is_empty (fst (unloc pos))) then
-       parse_error (loc pos) (Some "only top-level positions are supported");
-     Pchangestmt (side, (snd (unloc pos), offset), s) }
+| PROC CHANGE side=side? pos=loc(codepos_or_range) COLON s=brace(stmt)
+    { Pchangestmt (side, (unloc pos), s) }
 
 | PROC REWRITE side=side? pos=codepos f=pterm
     { Pprocrewrite (side, pos, `Rw f) }

src/ecParsetree.ml

@@ -770,9 +770,9 @@ type phltactic =
   | Prw_equiv      of rw_eqv_info
   | Psymmetry
   | Pbdhoare_split of bdh_split
-  | Pchangestmt    of side option * (pcodepos1 * pcodeoffset1) * pstmt
-  | Pprocrewrite   of side option * pcodepos * prrewrite
   | Prwprgm of rwprgm
+  | Pprocrewrite   of side option * pcodepos * prrewrite
+  | Pchangestmt    of side option * pcodepos_range * pstmt
 
 
     (* Eager *)

src/phl/ecPhlRewrite.ml

@@ -172,12 +172,14 @@ let process_rewrite
 (* -------------------------------------------------------------------- *)
 let t_change_stmt
   (side : side option)
-  (hd, stmt, tl : instr list * instr list * instr list) 
+  (pos : EcMatching.Position.codepos_range) 
   (s : stmt)
   (tc : tcenv1)
 =
   let env = FApi.tc1_env tc in
-  let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in 
+  let me, stmt = EcLowPhlGoal.tc1_get_stmt side tc in 
+
+  let (zpr, _), (stmt, epilog) = EcMatching.Zipper.zipper_and_split_of_cpos_range env pos stmt in
 
   let pvs = EcPV.is_write env (stmt @ s.s_node) in
   let pvs, globs = EcPV.PV.elements pvs in
@@ -187,8 +189,8 @@ let t_change_stmt
     (EcPV.is_read env s.s_node)
   in
 
-  let mleft = EcIdent.create "1" in (* FIXME: PR: is this how we want to do this? *)
-  let mright = EcIdent.create "2" in
+  let mleft = EcIdent.create "&1" in (* FIXME: PR: is this how we want to do this? *)
+  let mright = EcIdent.create "&2" in
 
   let eq =
    List.map
@@ -217,17 +219,19 @@ let t_change_stmt
        {ml=mleft; mr=mright; inv=f_ands eq}
   in
 
+  let stmt = EcMatching.Zipper.zip { zpr with z_tail = s.s_node @ epilog } in
+
   let goal2 =
    EcLowPhlGoal.hl_set_stmt
      side (FApi.tc1_goal tc)
-     (EcAst.stmt (List.flatten [hd; s.s_node; tl])) in
+     stmt in
 
   FApi.xmutate1 tc `ProcChangeStmt [goal1; goal2]
 
 (* -------------------------------------------------------------------- *)
 let process_change_stmt
   (side   : side option)
-  ((p, o) : pcodepos1 * pcodeoffset1)
+  (pos    : pcodepos_range)
   (s      : pstmt)
   (tc     : tcenv1)
 =
@@ -249,30 +253,16 @@ let process_change_stmt
   | _ -> tc_error !!tc "Wrong goal shape, expecting hoare or equiv goal with inlined code"
   end;
 
-  let me, stmt = EcLowPhlGoal.tc1_get_stmt side tc in 
-
-  let p, o =
-   let env = EcEnv.Memory.push_active_ss me env in
-   let pos = EcTyping.trans_codepos1 ~memory:(fst me) env p in
-   let off = EcTyping.trans_codeoffset1 ~memory:(fst me) env o in
-   let off = EcMatching.Position.resolve_offset ~base:pos ~offset:off in
-
-   let start = EcMatching.Zipper.offset_of_position env pos stmt in
-   let end_  = EcMatching.Zipper.offset_of_position env off stmt in
-
-   if (end_ < start) then
-     tc_error !!tc "end position cannot be before start position";
+  let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in 
 
-   (start - 1, end_ - start)
+  let pos = 
+    let env = EcEnv.Memory.push_active_ss me env in
+    EcTyping.trans_codepos_range ~memory:(fst me) env pos 
   in
 
-  let stmt     = stmt.s_node in
-  let hd, stmt = List.takedrop p stmt in
-  let stmt, tl = List.takedrop o stmt in
-
   let s = match side with 
   | Some side -> EcProofTyping.tc1_process_prhl_stmt tc side s
   | None -> EcProofTyping.tc1_process_Xhl_stmt tc s 
   in
 
-  t_change_stmt side (hd, stmt, tl) s tc
+  t_change_stmt side pos s tc

src/phl/ecPhlRewrite.mli

@@ -8,4 +8,4 @@ val process_change : side option -> pcodepos -> pexpr -> backward
 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_change_stmt : side option -> pcodepos1 * pcodeoffset1 -> pstmt -> backward
+val process_change_stmt   : side option -> pcodepos_range -> pstmt -> backward

tests/procchange.ec

@@ -4,14 +4,17 @@ require import AllCore Distr.
 theory ProcChangeAssignEquiv.
   module M = {
     proc f(x : int) = {
-      x <- x + 0;
+      x <- 0;
+      x <- x + 1;
+      x <- x + 2;
+      x <- x + 3;
     }
   }.
 
   lemma L : equiv[M.f ~ M.f: true ==> true].
   proof.
   proc.
-    proc change {1} 1 1 : { x <- x; }.
+    proc change {1} [1..3] : { x <- 3; }.
 
     wp. skip. smt().
   abort.
@@ -27,7 +30,7 @@ theory ProcChangeAssignHoareEquiv.
   lemma L : hoare[M.f : true ==> true].
   proof.
   proc.
-    proc change 1 1 : { x <- x ; }. wp. skip. smt().
+    proc change [1..1] : { x <- x ; }. wp. skip. smt().
   abort.
 end ProcChangeAssignHoareEquiv.
 
@@ -42,7 +45,7 @@ theory ProcChangeSampleEquiv.
   lemma L : equiv[M.f ~ M.f : true ==> true].
   proof.
   proc.
-  proc change {1} 1 1 : { x <$ (dunit x); }.
+  proc change {1} [1..1] : { x <$ (dunit x); }.
   rnd. skip. smt().
   abort.
 end ProcChangeSampleEquiv.
@@ -62,7 +65,7 @@ theory ProcChangeIfEquiv.
   lemma L : equiv[M.f ~ M.f : true ==> true].
   proof.
   proc.
-  proc change {1} 1 1 : { 
+  proc change {1} [1..1] : { 
     if (x = y) {
       x <- y;
     } else {
@@ -85,15 +88,47 @@ theory ProcChangeWhileEquiv.
   lemma L : equiv[M.f ~ M.f : true ==> true].
   proof.
   proc.
-  proc change {1} 1 1 : {
+  proc change {1} [1..1] : {
     while (x <> y) {
-      x <- x + 1;
+      x <- x + 1 + 0;
     }
   }.
-  admit. (* FIXME *)
+  proc rewrite {1} 1 /=.
+  proc rewrite {2} 1.1 /=. 
+  sim.
   abort.
 end ProcChangeWhileEquiv.
 
+
+(* -------------------------------------------------------------------- *)
+theory ProcChangeInWhileEquiv.
+  module M = {
+    proc f(x : int, y : int) = {
+    while (x + 0 <> y) {
+        x <- 1;
+        x <- x + 1;
+        x <- 2;
+      }
+    }
+  }.
+  
+  lemma L : equiv[M.f ~ M.f : true ==> true].
+  proof.
+  proc.
+  proc change {1} ^while.2 : {
+    x <- x + 0 + 1;
+  }.
+  wp; skip. smt().
+  proc change {1} [^while.1..^while.2] : {
+    x <- 2;
+  }. wp; skip. smt().
+  proc change {2} [^while.1-1] : {
+    x <- 2;
+  }. wp; skip. smt().
+  abort.
+end ProcChangeInWhileEquiv.
+
+
 (* -------------------------------------------------------------------- *)
 theory ProcChangeAssignHoare.
   module M = {
@@ -105,7 +140,7 @@ theory ProcChangeAssignHoare.
   lemma L : hoare[M.f: true ==> true].
   proof.
   proc.
-    proc change 1 1 : { x <- x; }.
+    proc change [1..1] : { x <- x; }.
     wp; skip; smt().
   abort.
 end ProcChangeAssignHoare.
@@ -121,7 +156,7 @@ theory ProcChangeSampleHoare.
   lemma L : hoare[M.f: true ==> true].
   proof.
   proc.
-  proc change 1 1 : { x <$ (dunit x); }.
+  proc change 1 : { x <$ (dunit x); }.
   rnd; skip; smt().
   abort.
 end ProcChangeSampleHoare.
@@ -141,7 +176,7 @@ theory ProcChangeIfHoare.
   lemma L : hoare[M.f: true ==> true].
   proof.
   proc.
-  proc change 1 1 : { 
+  proc change 1 : { 
     if (x = y) {
       x <- y;
     } else {
@@ -164,11 +199,33 @@ theory ProcChangeWhileHoare.
   lemma L : hoare[M.f: true ==> true].
   proof.
   proc.
-  proc change 1 1 : {
+  proc change 1 : {
     while (x <> y) {
       x <- x + 1;
     }
   }.
-  admit. (* FIXME *)
+  proc rewrite {1} ^while /=; sim.
   abort.
 end ProcChangeWhileHoare.
+
+
+(* -------------------------------------------------------------------- *)
+theory ProcChangeInWhileHoare.
+  module M = {
+    proc f(x : int, y : int) = {
+      while (x + 0 <> y) {
+        x <- x + 1;
+      }
+    }
+  }.
+  
+  lemma L : hoare[M.f : true ==> true].
+  proof.
+  proc.
+  proc change ^while.1 : {
+    x <- x + 0 + 1;
+  }.
+  wp; skip. smt().
+  abort.
+end ProcChangeInWhileHoare.
+