refactor(pl): looptx as program transformations

src/ecLowPhlGoal.ml

@@ -823,89 +823,6 @@ let abstract_info2 env fl' fr' =
     end;
     ((topl, fl, oil, sigl), (topr, fr, oir, sigr))
 
-(* -------------------------------------------------------------------- *)
-type code_txenv = proofenv * LDecl.hyps
-
-type 'a code_tx =
-     code_txenv -> 'a -> form pair -> memenv * stmt
-   -> memenv * stmt * form list
-
-type 'a zip_t =
-     code_txenv -> form pair -> memenv -> Zpr.zipper
-  -> memenv * Zpr.zipper * form list
-
-let t_fold f (cenv : code_txenv) (cpos : codepos) (_ : form * form) (state, s) =
-  try
-    let env = EcEnv.LDecl.toenv (snd cenv) in
-    let (me, f) = Zpr.fold env cenv cpos (fun _ -> f) state s in
-      ((me, f, []) : memenv * _ * form list)
-  with InvalidCPos -> tc_error (fst cenv) "invalid code position"
-
-let t_zip f (cenv : code_txenv) (cpos : codepos) (prpo : form * form) (state, s) =
-  try
-    let env = EcEnv.LDecl.toenv (snd cenv) in
-    let (me, zpr, gs) = f cenv prpo state (Zpr.zipper_of_cpos env cpos s) in
-      ((me, Zpr.zip zpr, gs) : memenv * _ * form list)
-  with InvalidCPos -> tc_error (fst cenv) "invalid code position"
-
-let t_code_transform (side : oside) cpos tr tx tc =
-  let pf = FApi.tc1_penv tc in
-
-  match side with
-  | None -> begin
-      let (hyps, concl) = FApi.tc1_flat tc in
-
-      match concl.f_node with
-      | FhoareS hs ->
-          let pr, po = hs_pr hs, hs_po hs in
-          (* The transformations only use the postcondition for the
-             program variables it reads: give them the conjunction of the
-             main and exceptional postconditions, so that none is missed. *)
-          let po = f_ands (POE.fold (fun fs f -> fs @ [f]) [] po.hsi_inv) in
-          let (me, stmt, cs) =
-            tx (pf, hyps) cpos (pr.inv, po) (hs.hs_m, hs.hs_s) in
-          let concl =
-            f_hoareS (snd me) pr stmt (hs_po hs)
-          in
-          FApi.xmutate1 tc (tr None) (cs @ [concl])
-
-      | FbdHoareS bhs ->
-          let pr, po = bhs_pr bhs, bhs_po bhs in
-          let (me, stmt, cs) =
-            tx (pf, hyps) cpos (pr.inv, po.inv) (bhs.bhs_m, bhs.bhs_s) in
-          let concl = f_bdHoareS (snd me) pr stmt po bhs.bhs_cmp (bhs_bd bhs) in
-          FApi.xmutate1 tc (tr None) (cs @ [concl])
-
-      | FeHoareS ehs ->
-          let pr, po = ehs_pr ehs, ehs_po ehs in
-          let (me, stmt, cs) =
-            tx (pf, hyps) cpos (pr.inv, po.inv) (ehs.ehs_m, ehs.ehs_s) in
-          let concl = f_eHoareS (snd me) pr stmt po in
-          FApi.xmutate1 tc (tr None) (cs @ [concl])
-
-      | _ ->
-        let kinds =
-            [`PHoare `Stmt; `Hoare `Stmt; `EHoare `Stmt ] in
-        tc_error_noXhl ~kinds:kinds pf
-  end
-
-  | Some side ->
-      let hyps      = FApi.tc1_hyps tc in
-      let es        = tc1_as_equivS tc in
-      let pre, post = es_pr es, es_po es in
-      let me, stmt     =
-        match side with
-        | `Left  -> (es.es_ml, es.es_sl)
-        | `Right -> (es.es_mr, es.es_sr) in
-      let (_, mt), stmt, cs = tx (pf, hyps) cpos (pre.inv, post.inv) (me, stmt) in
-      let concl =
-        match side with
-        | `Left  -> f_equivS mt (snd es.es_mr) (es_pr es) stmt es.es_sr (es_po es)
-        | `Right -> f_equivS (snd es.es_ml) mt (es_pr es) es.es_sl stmt (es_po es)
-      in
-
-      FApi.xmutate1 tc (tr (Some side)) (cs @ [concl])
-
 (* -------------------------------------------------------------------- *)
 let get_single tc = function
   | Single f -> f

src/ecMatching.ml

@@ -389,6 +389,15 @@ module Position = struct
     let (env, s), npath = normalize_cpos_path env cpath s in
     (env, s), (npath, normalize_cpos1 env cp1 s)
 
+  (* The code position denoting a normalized one, with absolute positions
+     only: resolving it again in the same statement needs no lookup and
+     yields the same position. *)
+  let cpos_of_nm_cpos ((cpath, cp1) : nm_codepos) : codepos =
+    let brsel : nm_codepos_brsel -> codepos_brsel = function
+      | `Cond b   -> `Cond b
+      | `Match ix -> `MatchByPos ix in
+    (List.map (fun (i, br) -> (cpos1 i, brsel br)) cpath, cpos1 cp1)
+
   let resolve_offset1_from_cpos1 env (base: nm_codepos1) (off: codeoffset1) (s: stmt) : nm_codepos1 = 
     match off with
     | `Absolute off -> normalize_cpos1 env off s 

src/ecMatching.mli

@@ -110,6 +110,9 @@ module Position : sig
 
   val normalize_cpos : env ->  codepos -> stmt -> (env * stmt) * nm_codepos
 
+  (* The code position denoting a normalized one (absolute positions only). *)
+  val cpos_of_nm_cpos : nm_codepos -> codepos
+
   val cpos1 : int -> codepos1
 
   (* --- Gap types --- *)

src/phl/README.md

@@ -109,8 +109,10 @@ Current catalogue: `rndsem` (`EcTrRndSem`), `rcond` (`EcTrRCond`),
 `rmatch` (`EcTrRMatch`), `if-push` (`EcTrIfPush`), `match-push`
 (`EcTrMatchPush`), `swap` (`EcTrSwap`), `inline` (`EcTrInline`), `kill`
 (`EcTrKill`), `alias` (`EcTrAlias`), `set` (`EcTrSet`), `set-match`
-(`EcTrSetMatch`), `cfold` (`EcTrCFold`), `asgn-case` (`EcTrAsgnCase`) and
-`simplify-if` (`EcTrSimplifyIf`). `if-push` / `match-push` push
+(`EcTrSetMatch`), `cfold` (`EcTrCFold`), `asgn-case` (`EcTrAsgnCase`),
+`simplify-if` (`EcTrSimplifyIf`), and the loop transformations `fission`
+(`EcTrFission`), `fusion` (`EcTrFusion`), `unroll` (`EcTrUnroll`) and
+`splitwhile` (`EcTrSplitWhile`). `if-push` / `match-push` push
 the continuation of a leading conditional / `match` into its branches: the
 `if` and `match` tactics are push + rule on the conditional alone
 (`Ec<Logic>If`, `Ec<Logic>Match`).

src/phl/REFACTORING.md

@@ -420,15 +420,29 @@ Current catalogue:
 - `asgn-case` (`EcTrAsgnCase`): splits a tuple assignment into one
   assignment per variable (`case <-`); no obligation;
 - `simplify-if` (`EcTrSimplifyIf`): turns a conditional whose branches are
-  assignments into a single assignment (`simplify if`); no obligation.
+  assignments into a single assignment (`simplify if`); no obligation;
+- `fission` (`EcTrFission`, splitting the loop at a — possibly nested —
+  position in two loops at two offsets of its body, its prelude of `n`
+  instructions duplicated; read / write independence, determinism and
+  `raise`-freedom side conditions; no obligation), used by `fission` in
+  every logic;
+- `fusion` (`EcTrFusion`, the inverse: merging two consecutive loops with
+  equal preludes, conditions and epilogs, under the side conditions of
+  `fission`; no obligation), used by `fusion` in every logic;
+- `unroll` (`EcTrUnroll`): `while e do c` becomes
+  `if e then c; while e do c`; no obligation; used by `unroll` (`unroll
+  for` stays derived: rcond, wp, seq, conseq, cfold);
+- `splitwhile` (`EcTrSplitWhile`): `while e do c` becomes
+  `while (e /\ b) do c; while e do c`; no obligation; used by
+  `splitwhile`.
 
 The decisions of a conditional or a match are computed by `EcPlRCond`.
 The `if` and `match` tactics are push + rule on the conditional alone: they
 push the continuation into the branches (when there is one) through the
 transformation rule (on each side, for the two-sided equiv forms), then
 apply the `if` / `match` rule of their logic (`Ec<Logic>If`,
 `Ec<Logic>Match`), stated on the conditional alone. Further entries come
-with the tactics that use them: the loop transformations and proc rewrite.
+with the tactics that use them: proc rewrite / change.
 
 Exception: the framed form of `match C k` (used when the variables of the
 discriminant `e` are neither read nor written by the prefix, and the