PR: Feature: Proc change

Author: Gustavo2622

src/ecHiTacticals.ml

@@ -230,8 +230,9 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pauto                     -> EcPhlAuto.t_auto ~conv:`Conv
     | Plossless                 -> EcPhlHiAuto.t_lossless
     | Prepl_stmt infos          -> EcPhlTrans.process_equiv_trans infos
-    | Pprocchange (s, p, f)     -> EcPhlRewrite.process_change s p f
     | Pprocrewrite (s, p, f)    -> EcPhlRewrite.process_rewrite s p f
+    | Pchangestmt (s, p, c)     -> EcPhlRewrite.process_change_stmt s p c
+    | Prwprgm infos             -> EcPhlRwPrgm.process_rw_prgm infos
   in
 
   try  tx tc

src/ecLexer.mll

@@ -97,6 +97,8 @@
     "clear"       , CLEAR      ;        (* KW: tactic *)
     "wlog"        , WLOG       ;        (* KW: tactic *)
 
+    "idassign"    , IDASSIGN   ;        (* KW: tactic *)
+
     (* Auto tactics *)
     "apply"       , APPLY      ;        (* KW: tactic *)
     "rewrite"     , REWRITE    ;        (* KW: tactic *)

src/ecPV.ml

@@ -205,7 +205,6 @@ module PVM = struct
 end
 
 (* -------------------------------------------------------------------- *)
-
 module PV = struct
 
   type t =
@@ -413,6 +412,10 @@ module PV = struct
     { s_pv = Mnpv.set_diff fv1.s_pv fv2.s_pv;
       s_gl = Sm.diff fv1.s_gl fv2.s_gl }
 
+  let inter fv1 fv2 = 
+    { s_pv = Mnpv.inter (fun _ _ t2 -> Some t2) fv1.s_pv fv2.s_pv;
+      s_gl = Sm.inter fv1.s_gl fv2.s_gl }
+
   let interdep env fv1 fv2 =
     let test_pv pv _ =
       Mnpv.mem pv fv2.s_pv ||

src/ecPV.mli

@@ -95,6 +95,7 @@ module PV : sig
   val remove   : env -> prog_var -> t -> t
   val union    : t -> t -> t
   val diff     : t -> t -> t
+  val inter    : t -> t -> t
   val subset   : t -> t -> bool
 
   val interdep     : env -> t -> t -> t

src/ecParser.mly

@@ -466,6 +466,7 @@
 %token HAVE
 %token HINT
 %token HOARE
+%token IDASSIGN
 %token IDTAC
 %token IF
 %token IFF
@@ -3193,15 +3194,20 @@ interleave_info:
 | LOSSLESS
     { Plossless }
 
-| PROC CHANGE side=side? pos=codepos COLON f=sexpr
-    { Pprocchange (side, pos, f) }
+| 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 REWRITE side=side? pos=codepos f=pterm
     { Pprocrewrite (side, pos, `Rw f) }
 
 | PROC REWRITE side=side? pos=codepos SLASHEQ
     { Pprocrewrite (side, pos, `Simpl) }
 
+| IDASSIGN o=codepos x=lvalue_var
+    { Prwprgm (`IdAssign (o, x)) }
+
 bdhoare_split:
 | b1=sform b2=sform b3=sform?
     { BDH_split_bop (b1,b2,b3) }

src/ecParsetree.ml

@@ -770,8 +770,10 @@ type phltactic =
   | Prw_equiv      of rw_eqv_info
   | Psymmetry
   | Pbdhoare_split of bdh_split
-  | Pprocchange    of side option * pcodepos * pexpr
+  | Pchangestmt    of side option * (pcodepos1 * pcodeoffset1) * pstmt
   | Pprocrewrite   of side option * pcodepos * prrewrite
+  | Prwprgm of rwprgm
+
 
     (* Eager *)
   | Peager_seq       of (eager_info * pcodepos1 pair * pformula)
@@ -789,6 +791,10 @@ type phltactic =
   | Pauto
   | Plossless
 
+and rwprgm = [
+  | `IdAssign of pcodepos * pqsymbol
+]
+
 (* -------------------------------------------------------------------- *)
 type include_exclude = [ `Include | `Exclude ]
 type pdbmap1 = {

src/ecProofTyping.ml

@@ -143,7 +143,7 @@ let tc1_process_prhl_stmt ?map tc side c =
   tc1_process_stmt hyps tc ?map c
 
 let tc1_process_Xhl_stmt ?map tc c =
-    let concl = FApi.tc1_goal tc in
+  let concl = FApi.tc1_goal tc in
   let m = match concl.f_node with FbdHoareS {bhs_m=m} | FhoareS {hs_m=m} -> m | _ -> assert false in
   let hyps   = FApi.tc1_hyps tc in
   let hyps   = LDecl.push_active_ss m hyps in

src/ecTyping.ml

@@ -3665,6 +3665,11 @@ and trans_codepos_range ?(memory : memory option) (env : EcEnv.env) ((cps, cpe)
 and trans_dcodepos1 ?(memory : memory option) (env : EcEnv.env) (p : pcodepos1 doption) : codepos1 doption =
   DOption.map (trans_codepos1 ?memory env) p
 
+and trans_codeoffset1 ?(memory: memory option) (env : EcEnv.env) (o : pcodeoffset1) : codeoffset1 =
+  match o with
+  | `ByOffset   i -> `ByOffset i
+  | `ByPosition p -> `ByPosition (trans_codepos1 ?memory env p) 
+
 (* -------------------------------------------------------------------- *)
 let get_instances (tvi, bty) env =
   let inst = List.pmap

src/ecTyping.mli

@@ -230,6 +230,7 @@ val trans_codepos_range : ?memory:EcMemory.memory -> env -> pcodepos_range -> co
 val trans_codepos1 : ?memory:EcMemory.memory -> env -> pcodepos1 -> codepos1
 val trans_codepos : ?memory:EcMemory.memory -> env -> pcodepos -> codepos
 val trans_dcodepos1 : ?memory:EcMemory.memory -> env -> pcodepos1 doption -> codepos1 doption
+val trans_codeoffset1 : ?memory:EcMemory.memory -> env -> pcodeoffset1 -> codeoffset1
 
 (* -------------------------------------------------------------------- *)
 type ptnmap = ty EcIdent.Mid.t ref

src/phl/ecPhlRewrite.ml

@@ -5,6 +5,7 @@ open EcCoreGoal
 open EcEnv
 open EcModules
 open EcFol
+open Batteries
 
 (* -------------------------------------------------------------------- *)
 let t_change
@@ -112,7 +113,7 @@ let process_rewrite_rw
     let data, e =
       EcUtils.ofdfl
         (fun () -> tc_error !!tc "cannot find a pattern to rewrite")
-        (List.find_map try1 pts) in
+        (List.find_map_opt try1 pts) in
 
     (m, data), expr_of_ss_inv e
   in
@@ -167,3 +168,111 @@ let process_rewrite
   match rw with
   | `Rw rw -> process_rewrite_rw side pos rw tc
   | `Simpl -> process_rewrite_simpl side pos tc
+
+(* -------------------------------------------------------------------- *)
+let t_change_stmt
+  (side : side option)
+  (hd, stmt, tl : instr list * instr list * instr list) 
+  (s : stmt)
+  (tc : tcenv1)
+=
+  let env = FApi.tc1_env tc in
+  let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in 
+
+  let pvs = EcPV.is_write env (stmt @ s.s_node) in
+  let pvs, globs = EcPV.PV.elements pvs in
+
+  let pre_pvs, pre_globs = EcPV.PV.elements @@ EcPV.PV.inter 
+    (EcPV.is_read env 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 eq =
+   List.map
+     (fun (pv, ty) -> f_eq (f_pvar pv ty mleft).inv (f_pvar pv ty mright).inv)
+     pvs
+   @
+   List.map
+     (fun mp -> f_eqglob mp mleft mp mright)
+     globs in
+
+  let pre_eq = 
+    List.map
+      (fun (pv, ty) -> f_eq (f_pvar pv ty mleft).inv (f_pvar pv ty mright).inv)
+      pre_pvs
+    @
+    List.map
+      (fun mp -> f_eqglob mp mleft mp mright)
+      pre_globs
+    in
+
+  let goal1 =
+     f_equivS
+       (snd me) (snd me)
+       {ml=mleft; mr=mright; inv=f_ands pre_eq} 
+       (EcAst.stmt stmt) s
+       {ml=mleft; mr=mright; inv=f_ands eq}
+  in
+
+  let goal2 =
+   EcLowPhlGoal.hl_set_stmt
+     side (FApi.tc1_goal tc)
+     (EcAst.stmt (List.flatten [hd; s.s_node; tl])) in
+
+  FApi.xmutate1 tc `ProcChangeStmt [goal1; goal2]
+
+(* -------------------------------------------------------------------- *)
+let process_change_stmt
+  (side   : side option)
+  ((p, o) : pcodepos1 * pcodeoffset1)
+  (s      : pstmt)
+  (tc     : tcenv1)
+=
+  let env = FApi.tc1_env tc in
+
+  begin match side, (FApi.tc1_goal tc).f_node with
+  | _, FhoareF _ 
+  | _, FeHoareF _
+  | _, FequivF _
+  | _, FbdHoareF _ -> tc_error !!tc "Expecting goal with inlined program code"
+  | Some _, FhoareS _ 
+  | Some _, FeHoareS _
+  | Some _, FbdHoareS _-> tc_error !!tc "Tactic should not receive side for non-relational goal"
+  | None, FequivS _ -> tc_error !!tc "Tactic requires side selector for relational goal"
+  | None, FhoareS _ 
+  | None, FeHoareS _
+  | None, FbdHoareS _
+  | Some _ , FequivS _ -> ()
+  | _ -> 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";
+
+   (start - 1, end_ - start)
+  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