The tactic swap now takes generalized code position.

Moreover, offsets can bow be absolute (i.e. can be a code-position).
In that case, the meaning is "move the code block before the targetted
instruction".

This work brings some breaking changes:

 - the variant `swap i1 i2 i3` has been removed. It was a way to
   give a direct access to the low-level functionality, but its
   interface is brittle and is not used by any development

 - a bug has been found in the resolution of negative code
   position (they were all shifted by one, making impossible to
   target the last instruction). This now has been fixed.

Author: strub

src/ecCorePrinting.ml

@@ -24,7 +24,6 @@ module type PrinterAPI = sig
 
   (* ------------------------------------------------------------------ *)
   val string_of_hcmp : EcFol.hoarecmp -> string
-  val string_of_cpos1 : EcMatching.Position.codepos1 -> string
 
   (* ------------------------------------------------------------------ *)
   type 'a pp = Format.formatter -> 'a -> unit
@@ -63,6 +62,10 @@ module type PrinterAPI = sig
   val pp_tyunivar : PPEnv.t -> EcUid.uid pp
   val pp_path     : path pp
 
+  (* ------------------------------------------------------------------ *)
+  val pp_codepos1    : PPEnv.t -> EcMatching.Position.codepos1 pp
+  val pp_codeoffset1 : PPEnv.t -> EcMatching.Position.codeoffset1 pp
+
   (* ------------------------------------------------------------------ *)
   val pp_typedecl    : PPEnv.t -> (path * tydecl                  ) pp
   val pp_opdecl      : ?long:bool -> PPEnv.t -> (path * operator  ) pp

src/ecHiTacticals.ml

@@ -236,8 +236,9 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
   with (* PHL Specific low errors *)
   | EcLowPhlGoal.InvalidSplit cpos1 ->
       tc_error_lazy !!tc (fun fmt ->
-        Format.fprintf fmt "invalid split index: %s"
-          (EcPrinting.string_of_cpos1 cpos1))
+        let ppe = EcPrinting.PPEnv.ofenv (FApi.tc1_env tc) in
+        Format.fprintf fmt "invalid split index: %a"
+          (EcPrinting.pp_codepos1 ppe) cpos1)
 
 (* -------------------------------------------------------------------- *)
 and process_sub (ttenv : ttenv) tts tc =

src/ecMatching.ml

@@ -32,6 +32,15 @@ module Position = struct
 
   type codepos1   = int * cp_base
   type codepos    = (codepos1 * int) list * codepos1
+  type codeoffset1 = [`ByOffset of int | `ByPosition of codepos1]
+
+  let shift ~(offset : int) ((o, p) : codepos1) : codepos1 =
+    (o + offset, p)
+
+  let resolve_offset ~(base : codepos1) ~(offset : codeoffset1) : codepos1 =
+    match offset with
+    | `ByPosition pos -> pos
+    | `ByOffset   off -> (off + fst base, snd base)
 end
 
 (* -------------------------------------------------------------------- *)
@@ -111,20 +120,28 @@ module Zipper = struct
     | false -> (s1, ir, s2)
     | true  -> (s2, ir, s1)
 
-  let split_at_cp_base ~after (env : EcEnv.env) (cb : cp_base) (s : stmt) =
+  type after = [`Yes | `No | `Auto]
+
+  let split_at_cp_base ~(after : after) (env : EcEnv.env) (cb : cp_base) (s : stmt) =
     match cb with
     | `ByPos i -> begin
-        let i = if i < 0 then List.length s.s_node + i else i in
-        try  List.takedrop (i - if after then 0 else 1) s.s_node
+        let after =
+          match after with
+          | `Auto -> 0 <= i
+          | `Yes  -> true
+          | `No   -> false in
+        let i = if i < 0 then List.length s.s_node + i + 1 else i in
+        let i = i - if after then 0 else 1 in
+        try  List.takedrop i s.s_node
         with (Invalid_argument _ | Not_found) -> raise InvalidCPos
       end
 
     | `ByMatch (i, cm) ->
         let (s1, i, s2) = find_by_cp_match env (i, cm) s in
 
         match after with
-        | false -> (List.rev s1, i :: s2)
-        | true  -> (List.rev_append s1 [i], s2)
+        | `No -> (List.rev s1, i :: s2)
+        | _   -> (List.rev_append s1 [i], s2)
 
   let split_at_cpos1 ~after (env : EcEnv.env) ((ipos, cb) : codepos1) s =
     let (s1, s2) = split_at_cp_base ~after env cb s in
@@ -147,11 +164,15 @@ module Zipper = struct
 
     in (s1, s2)
 
-  let find_by_cpos1 ?(rev = true) (env : EcEnv.env) (cpos1 : codepos1) s =
-    match split_at_cpos1 ~after:false env cpos1 s with
+  let find_by_cpos1 ?(rev = true) (env : EcEnv.env) (cpos1 : codepos1) (s : stmt) =
+    match split_at_cpos1 ~after:`No env cpos1 s with
     | (s1, i :: s2) -> ((if rev then List.rev s1 else s1), i, s2)
     | _ -> raise InvalidCPos
 
+  let offset_of_position (env : EcEnv.env) (cpos : codepos1) (s : stmt) =
+    let (s, _) = split_at_cpos1 ~after:`No env cpos s in
+    1 + List.length s
+
   let zipper_at_nm_cpos1 (env : EcEnv.env) ((cp1, sub) : codepos1 * int) s zpr =
     let (s1, i, s2) = find_by_cpos1 env cp1 s in
 
@@ -178,7 +199,7 @@ module Zipper = struct
     zipper s1 (i :: s2) zpr
 
   let split_at_cpos1 env cpos1 s =
-    split_at_cpos1 ~after:true env cpos1 s
+    split_at_cpos1 ~after:`Auto env cpos1 s
 
   let may_split_at_cpos1 ?(rev = false) env cpos1 s =
     ofdfl

src/ecMatching.mli

@@ -26,8 +26,12 @@ module Position : sig
     | `ByMatch of int option * cp_match
   ]
 
-  type codepos1   = int * cp_base
-  type codepos    = (codepos1 * int) list * codepos1
+  type codepos1    = int * cp_base
+  type codepos     = (codepos1 * int) list * codepos1
+  type codeoffset1 = [`ByOffset of int | `ByPosition of codepos1]
+
+  val shift : offset:int -> codepos1 -> codepos1
+  val resolve_offset : base:codepos1 -> offset:codeoffset1 -> codepos1
 end
 
 (* -------------------------------------------------------------------- *)
@@ -60,6 +64,9 @@ module Zipper : sig
   (* Split a statement from an optional top-level position (codepos1) *)
   val may_split_at_cpos1 : ?rev:bool -> env -> codepos1 option -> stmt -> instr list * instr list
 
+  (* Find the absolute offset of a top-level position (codepos1) w.r.t. a given statement *)
+  val offset_of_position : env -> codepos1 -> stmt -> int
+
   (* [zipper] soft constructor *)
   val zipper : instr list -> instr list -> ipath -> zipper
 

src/ecParser.mly

@@ -2639,6 +2639,10 @@ codepos:
 | nm=rlist0(nm1_codepos, empty) i=codepos1
     { (List.rev nm, i) }
 
+codeoffset1:
+| i=sword       { (`ByOffset   i :> pcodeoffset1) }
+| AT p=codepos1 { (`ByPosition p :> pcodeoffset1) }
+
 o_codepos1:
 | UNDERSCORE { None }
 | i=codepos1 { Some i}
@@ -2691,21 +2695,24 @@ rnd_info:
 | phi=sform d1=sform d2=sform d3=sform d4=sform p=sform?
     { PMultRndParams ((phi, d1, d2, d3, d4), p) }
 
-swap_info:
-| s=side? p=swap_pos { s,p }
+(* ------------------------------------------------------------------------ *)
+(* Code motion                                                              *)
+%public phltactic:
+| SWAP info=iplist1(loc(swap_info), COMMA) %prec prec_below_comma
+    { Pswap info }
 
-swap_pos:
-| i1=word i2=word i3=word
-    { SKbase (i1, i2, i3) }
+swap_info:
+| s=side? p=swap_position { (s, p) }
 
-| p=sword
-    { SKmove p }
+swap_position:
+| offset=codeoffset1
+    { { interval = None; offset; } }
 
-| i1=word p=sword
-    { SKmovei (i1, p) }
+| start=codepos1 offset=codeoffset1
+    { { interval = Some (start, None); offset; } }
 
-| LBRACKET i1=word DOTDOT i2=word RBRACKET p=sword
-    { SKmoveinter (i1, i2, p) }
+| LBRACKET start=codepos1 DOTDOT end_=codepos1 RBRACKET offset=codeoffset1
+    { { interval = Some (start, Some end_); offset; } }
 
 side:
 | LBRACE n=word RBRACE {
@@ -2984,7 +2991,7 @@ interleave_info:
 | s=brace(stmt) { OKstmt(s) }
 | r=sexpr? LEAT f=loc(fident) { OKproc(f, r) }
 
-phltactic:
+%public phltactic:
 | PROC
    { Pfun `Def }
 
@@ -3041,9 +3048,6 @@ phltactic:
       | Some _, true  ->
           parse_error s.pl_loc (Some "cannot give side and '='") }
 
-| SWAP info=iplist1(loc(swap_info), COMMA) %prec prec_below_comma
-    { Pswap info }
-
 | INTERLEAVE info=loc(interleave_info)
     { Pinterleave info }
 

src/ecParsetree.ml

@@ -503,12 +503,16 @@ type pcodepos1 = int * pcp_base
 type pcodepos  = (pcodepos1 * int) list * pcodepos1
 type pdocodepos1 = pcodepos1 doption option
 
+type pcodeoffset1 = [
+  | `ByOffset   of int
+  | `ByPosition of pcodepos1
+]
+
 (* -------------------------------------------------------------------- *)
-type swap_kind =
-  | SKbase      of int * int * int
-  | SKmove      of int
-  | SKmovei     of int * int
-  | SKmoveinter of int * int * int
+type pswap_kind = {
+  interval : (pcodepos1 * pcodepos1 option) option;
+  offset   : pcodeoffset1;
+}
 
 type interleave_info = oside * (int * int) * ((int * int) list) * int
 
@@ -729,7 +733,7 @@ type phltactic =
   | Prmatch        of (oside * symbol * pcodepos1)
   | Pcond          of pcond_info
   | Pmatch         of matchmode
-  | Pswap          of ((oside * swap_kind) located list)
+  | Pswap          of ((oside * pswap_kind) located list)
   | Pcfold         of (oside * pcodepos * int option)
   | Pinline        of inline_info
   | Poutline       of outline_info

src/ecPrinting.ml

@@ -1315,33 +1315,6 @@ let string_of_locality = function
 let pp_locality fmt lc =
   Format.fprintf fmt "%s" (odfl "" (string_of_locality lc))
 
-(* -------------------------------------------------------------------- *)
-let string_of_cpos1 ((off, cp) : EcMatching.Position.codepos1) =
-  let s =
-    match cp with
-    | `ByPos i ->
-        string_of_int i
-
-    | `ByMatch (i, k) ->
-        let s =
-          let k =
-            match k with
-            | `If       -> "if"
-            | `While    -> "while"
-            | `Assign _ -> "<-"
-            | `Sample   -> "<$"
-            | `Call     -> "<@"
-          in Printf.sprintf "^%s" k in
-
-        match i with
-        | None | Some 1 -> s
-        | Some i -> Printf.sprintf "%s{%d}" s i
-  in
-
-  if off = 0 then s else
-
-  Printf.sprintf "%s%s%d" s (if off < 0 then "-" else "+") (abs off)
-
 (* -------------------------------------------------------------------- *)
 (* suppose g is a formula consisting of the application of a binary
    operator op with scope onm and precedence opprec to formula
@@ -2138,6 +2111,41 @@ let pp_scvar ppe fmt vs =
 
   pp_list "@ " pp_grp fmt vs
 
+(* -------------------------------------------------------------------- *)
+let pp_codepos1 (ppe : PPEnv.t) (fmt : Format.formatter) ((off, cp) : EcMatching.Position.codepos1) =
+  let s : string =
+    match cp with
+    | `ByPos i ->
+        string_of_int i
+
+    | `ByMatch (i, k) ->
+        let s =
+          let k =
+            match k with
+            | `If     -> "if"
+            | `While  -> "while"
+            | `Sample -> "<$"
+            | `Call   -> "<@"
+            | `Assign `LvmNone -> "<-"
+            | `Assign (`LvmVar pv) -> Format.asprintf "%a<-" (pp_pv ppe) pv
+          in Format.asprintf "^%s" k in
+
+        match i with
+        | None | Some 1 -> s
+        | Some i -> Format.asprintf "%s{%d}" s i
+  in
+
+  if off = 0 then
+    Format.fprintf fmt "%s" s
+  else
+    Format.fprintf fmt "%s%s%d" s (if off < 0 then "-" else "+") (abs off)
+
+(* -------------------------------------------------------------------- *)
+let pp_codeoffset1 (ppe : PPEnv.t) (fmt : Format.formatter) (offset : EcMatching.Position.codeoffset1) =
+  match offset with
+  | `ByPosition p -> Format.fprintf fmt "%a" (pp_codepos1 ppe) p
+  | `ByOffset   o -> Format.fprintf fmt "%d" o
+  
 (* -------------------------------------------------------------------- *)
 let pp_opdecl_pr (ppe : PPEnv.t) fmt (basename, ts, ty, op) =
   let ppe = PPEnv.add_locals ppe (List.map fst ts) in