diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml
index 5f3e239dc..418ccb7d6 100644
--- a/src/ecCorePrinting.ml
+++ b/src/ecCorePrinting.ml
@@ -68,10 +68,14 @@ module type PrinterAPI = sig
   val pp_shorten_path : PPEnv.t -> (path -> qsymbol -> bool) -> path pp
 
   (* ------------------------------------------------------------------ *)
-  val pp_codepos1    : PPEnv.t -> EcMatching.Position.codepos1 pp
-  val pp_codeoffset1 : PPEnv.t -> EcMatching.Position.codeoffset1 pp
-
-  val pp_codepos     : PPEnv.t -> EcMatching.Position.codepos pp
+  val pp_codepos1      : PPEnv.t -> EcMatching.Position.codepos1 pp
+  val pp_codepos_brsel : EcMatching.Position.codepos_brsel pp
+  val pp_codepos_step  : PPEnv.t -> EcMatching.Position.codepos_step pp
+  val pp_codepos_path  : PPEnv.t -> EcMatching.Position.codepos_path pp
+  val pp_codeoffset1   : PPEnv.t -> EcMatching.Position.codeoffset1 pp
+
+  val pp_codepos       : PPEnv.t -> EcMatching.Position.codepos pp
+  val pp_codepos_range : PPEnv.t -> EcMatching.Position.codepos_range pp
 
   (* ------------------------------------------------------------------ *)
   type vsubst = [
diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml
index 00687ebd8..73861b021 100644
--- a/src/ecLowPhlGoal.ml
+++ b/src/ecLowPhlGoal.ml
@@ -206,6 +206,13 @@ let tc1_get_stmt side tc =
   | _            ->
       tc_error_noXhl ~kinds:(hlkinds_Xhl_r `Stmt) !!tc
 
+(* ------------------------------------------------------------------ *)
+let tc1_process_codepos_or_range tc (side, cpr) =
+  let me, _ = tc1_get_stmt side tc in
+  let env = FApi.tc1_env tc in
+  let env = EcEnv.Memory.push_active_ss me env in
+  EcTyping.trans_codepos_or_range env cpr
+
 (* ------------------------------------------------------------------ *)
 let tc1_process_codepos_range tc (side, cpr) =
   let me, _ = tc1_get_stmt side tc in
@@ -334,19 +341,19 @@ let push_memenvs_pre (hyps : LDecl.hyps) (f : form) =
 exception InvalidSplit of codepos1
 
 let s_split env i s =
-  let module Zpr = EcMatching.Zipper in
-  try  Zpr.split_at_cpos1 env i s
-  with Zpr.InvalidCPos -> raise (InvalidSplit i)
+  let module Pos = EcMatching.Position in
+  try  Pos.split_at_cpos1 env i s
+  with Pos.InvalidCPos -> raise (InvalidSplit i)
 
 let s_split_i env i s =
-  let module Zpr = EcMatching.Zipper in
-  try  Zpr.find_by_cpos1 ~rev:false env i s
-  with Zpr.InvalidCPos -> raise (InvalidSplit i)
+  let module Pos = EcMatching.Position in
+  try  Pos.find_by_cpos1 ~rev:false env i s
+  with Pos.InvalidCPos -> raise (InvalidSplit i)
 
 let o_split ?rev env i s =
-  let module Zpr = EcMatching.Zipper in
-  try  Zpr.may_split_at_cpos1 ?rev env i s
-  with Zpr.InvalidCPos -> raise (InvalidSplit (oget i))
+  let module Pos = EcMatching.Position in
+  try  Pos.may_split_at_cpos1 ?rev env i s
+  with Pos.InvalidCPos -> raise (InvalidSplit (oget i))
 
 (* -------------------------------------------------------------------- *)
 let t_hS_or_bhS_or_eS ?th ?teh ?tbh ?te tc =
@@ -692,14 +699,14 @@ let t_fold f (cenv : code_txenv) (cpos : codepos) (_ : form * form) (state, s) =
     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 Zpr.InvalidCPos -> tc_error (fst cenv) "invalid code position"
+  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 Zpr.InvalidCPos -> tc_error (fst cenv) "invalid code position"
+  with InvalidCPos -> tc_error (fst cenv) "invalid code position"
 
 let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc =
   let pf = FApi.tc1_penv tc in
diff --git a/src/ecMatching.ml b/src/ecMatching.ml
index a14e8859b..9657f8094 100644
--- a/src/ecMatching.ml
+++ b/src/ecMatching.ml
@@ -28,15 +28,71 @@ module Position = struct
   and lvmatch = [ `LvmNone | `LvmVar of EcTypes.prog_var ]
 
   type cp_base = [
-    | `ByPos of int
+    | `ByPos of int (* Always <> 0 *)
     | `ByMatch of int option * cp_match
   ]
 
-  type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol]
-  type codepos1      = int * cp_base
-  type codepos       = (codepos1 * codepos_brsel) list * codepos1
-  type codepos_range = codepos * [`Base of codepos | `Offset of codepos1]
-  type codeoffset1   = [`ByOffset of int | `ByPosition of codepos1]
+  exception InvalidCPos
+
+  (* Code positions:
+     Code positions point at specific instructions.
+     
+     Ranges are closed-open for composability:
+     a..b => [a..b[ so that
+     1..a..b..n = 1..a \/ a..b \/ b..n
+     = [1;a[ \/ [a;b[ \/ [b;n[ 
+      and all the unions are disjoint 
+      so we do not repeat elements
+
+    Splits are 
+    codepos1 (linear code positions) are only interpretable wrt
+    to their block
+    The block is either specific via context (possibly implicitly)
+    or via a codeposition path
+
+    The correspondence between single position and ranges is:
+      position a <=> range [a;a+1[
+    This gives us the following desirable properties:
+      - Position a points at the first instruction of any range
+        that starts at a
+      - A range [a;b[ is exactly the union of all the ranges 
+        [i;i+1[ for i in [a;b[
+    
+    Ranges must have a < b
+    TODO: Do we accept a = b or do we add other ways of dealing with
+          pointing at positions between lines of code?
+
+    Normalized code positions are given by the indexes alone
+    and are only meaningful wrt a given block of code
+    They are also converted to only use positive indexes
+  *)
+
+  (* Branch selection *)
+  type codepos_brsel    = [`Cond of bool | `Match of EcSymbols.symbol]
+  type nm_codepos_brsel = [`Cond of bool | `Match of int]
+  (* Linear code position inside a block *)
+  type codepos1       = int * cp_base
+  (* Normalized code position inside a block, always > 0 *)
+  type nm_codepos1    = int
+  (* Codeposition path step *)
+  type codepos_step   = (codepos1 * codepos_brsel)
+  type nm_codepos_step = (nm_codepos1 * nm_codepos_brsel)
+  (* Block selection by codepos + branch selection *)
+  type codepos_path   = codepos_step list
+  type nm_codepos_path = nm_codepos_step list
+  (* Full codeposition = path to block + position in block *)
+  type codepos        = codepos_path * codepos1
+  type nm_codepos      = nm_codepos_path * nm_codepos1
+  (* Code position offset *)
+  type codeoffset1    = [`Relative of int | `Absolute of codepos1]
+  (* Range of linear code positions *)
+  type codepos1_range = (codepos1 * codeoffset1)
+  (* Normalized codepos1 range *)
+  type nm_codepos1_range = (int * int)
+  (* Range + block path *)
+  type codepos_range  = codepos_path * codepos1_range
+  (* Normalized codepos range *)
+  type nm_codepos_range = nm_codepos_path * nm_codepos1_range
 
   let shift1 ~(offset : int) ((o, p) : codepos1) : codepos1 =
     (o + offset, p)
@@ -46,49 +102,88 @@ module Position = struct
 
   let resolve_offset ~(base : codepos1) ~(offset : codeoffset1) : codepos1 =
     match offset with
-    | `ByPosition pos -> pos
-    | `ByOffset   off -> (off + fst base, snd base)
-end
+    | `Absolute pos -> pos
+    | `Relative off -> (off + fst base, snd base)
 
-(* -------------------------------------------------------------------- *)
-module Zipper = struct
-  open Position
+  let codepos1_range_of_codepos1 (cp1: codepos1) : codepos1_range =
+    (cp1, `Relative 1)
 
-  exception InvalidCPos
+  let codepos_range_of_codepos ((cpath, cp1): codepos) : codepos_range = 
+    (cpath, codepos1_range_of_codepos1 cp1)
 
-  module P = EcPath
+  let nm_codepos1_range_of_nm_codepos1 (cp1: nm_codepos1) : nm_codepos1_range =
+    (cp1, cp1+1)
 
-  type ('a, 'state) folder =
-    env -> 'a -> 'state -> instr -> 'state * instr list
+  let nm_codepos_range_of_nm_codepos ((cpath, cp1): nm_codepos) : nm_codepos_range =
+    (cpath, nm_codepos1_range_of_nm_codepos1 cp1)
 
-  type ('a, 'state) folder_l =
-    env -> 'a -> 'state -> instr list -> 'state * instr list
+  let codepos1_of_nm_codepos1 (nm: nm_codepos1) : codepos1 = 
+    (0, `ByPos nm)
 
-  type spath_match_ctxt = {
-    locals : (EcIdent.t * ty) list;
-    prebr  : ((EcIdent.t * ty) list * stmt) list;
-    postbr : ((EcIdent.t * ty) list * stmt) list;
-  }
+  let cpos1 (i: int) : codepos1 = 
+    (0, `ByPos i)
 
-  type ipath =
-  | ZTop
-  | ZWhile  of expr * spath
-  | ZIfThen of expr * spath * stmt
-  | ZIfElse of expr * stmt  * spath
-  | ZMatch  of expr * spath * spath_match_ctxt
+  let cpos1_first : codepos1 =
+    cpos1 1
 
-  and spath = (instr list * instr list) * ipath
+  let cpos1_last : codepos1 =
+    cpos1 (-1)
 
-  type zipper = {
-    z_head : instr list;                (* instructions on my left (rev)       *)
-    z_tail : instr list;                (* instructions on my right (me incl.) *)
-    z_path : ipath;                     (* path (zipper) leading to me         *)
-    z_env  : env option;
-  }
+  let cpos1_after_last : codepos1 =
+    (1, `ByPos (-1))
 
-  let cpos (i : int) : codepos1 = (0, `ByPos i)
+  let cpos1_to_top (cp1: codepos1) : codepos =
+    ([], cp1)
 
-  let zipper ?env hd tl zpr = { z_head = hd; z_tail = tl; z_path = zpr; z_env = env; }
+  (* Top-level first instruction *)
+  let cpos_first : codepos =
+    cpos1_to_top cpos1_first
+
+  let cpos_last : codepos =
+    cpos1_to_top cpos1_last
+
+(* FIXME: check if we need this
+  let codepos_step_of_nm_codepos_step ((cp1, brsel): nm_codepos_step) : codepos_step = 
+    (codepos1_of_nm_codepos1 cp1, brsel)
+
+  let codepos_path_of_nm_codepos_path (cpath: nm_codepos_path) : codepos_path = 
+    List.map codepos_step_of_nm_codepos_step cpath
+
+  let codepos_of_nm_codepos ((nmp, nmcp): nm_codepos) : codepos =
+    (codepos_path_of_nm_codepos_path nmp, codepos1_of_nm_codepos1 nmcp)
+*)
+
+  (* 
+    Check that the ranges are valid and then:
+    if either is empty -> true
+    otherwise possibilities are:
+    1. s1 <= s2 <= min(e1, e2) => false
+    2. s1 <= e1 <= s2 <= e2    => true
+    3. s2 <= s1 <= min(e1, e2) => false
+    4. s2 <= e2 <= s1 <= e1    => true
+  *)
+    
+  let disjoint ((s1, e1): nm_codepos1_range) ((s2, e2): nm_codepos1_range) : bool =
+    if s1 > e1 || s2 > e2 then raise InvalidCPos;
+    (s1 = e1) || (s2 = e2) ||
+    (e1 < s2) || (e2 < s1)
+
+  let nm_codepos_in_nm_codepos_range (cp: nm_codepos1) ((start, fin): nm_codepos1_range) : bool =
+    (start <= cp && cp < fin)
+
+  module Notations = struct
+    let (|+>) (cp: codepos) (offset: int) =
+      shift ~offset cp
+
+    let (+>) (cp1: codepos1) (offset: int) =
+      shift1 ~offset cp1
+
+    let (<+|) (cp: codepos) (i: int) =
+      shift ~offset:(-i) cp
+
+    let (<+) (cp1: codepos1) (i: int) =
+      shift1 ~offset:(-i) cp1
+  end
 
   let find_by_cp_match
     (env     : EcEnv.env)
@@ -149,142 +244,299 @@ module Zipper = struct
     | false -> (s1, ir, s2)
     | true  -> (s2, ir, s1)
 
-  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 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
+  let find_by_nmcpos1 ?(rev = true) (nm: nm_codepos1) (s: stmt) =
+    let nm = nm - 1 in (* Convert to 0-based indexing *)
+    let s1, i, s2 = try 
+      List.pivot_at nm s.s_node 
+    with (Invalid_argument _ | Not_found) -> raise InvalidCPos
+    in
+    (if rev then s1 else List.rev s1), i, s2
+
+  (* Throws InvalidCPos if failing *)
+  let check_nm_cpos1 (nm: nm_codepos1) (s: stmt) : unit =
+    if nm <= 0 || nm > (List.length s.s_node) + 1 then raise InvalidCPos
+
+  (* Normalizes code position wrt stmt *)
+  let normalize_cp_base ?(check = true) (env: EcEnv.env) (cb: cp_base) (s: stmt) : nm_codepos1 =
+    let nm = match cb with
+    | `ByPos i when i > 0 -> i
+    (* + 2 comes from:
+        Convert base position to 0-indexed: i |-> i - 1
+        Convert to position representation: i |-> len(s) - i
+        Convert to 1-indexed again:         i |-> i + 1
+        Obtaining final expression (len(s) - (i - 1)) + 1 = len(s) - i + 2
+     *)
+    | `ByPos i when i < 0 -> (List.length s.s_node) + i + 2 
+    (* i = 0 /\ check => Failure *)
+    | `ByPos _ when check -> raise InvalidCPos;
+    | `ByPos i -> i
+    | `ByMatch (i, cm) -> 
+      let (s1, _, _) = find_by_cp_match env (i, cm) s in
+      (1 + List.length s1)
+    in 
+    if check then check_nm_cpos1 nm s; 
+    nm
+
+  let normalize_cpos1 ?(check = true) (env: EcEnv.env) ((off, cb): codepos1) (s: stmt) : nm_codepos1 = 
+    let nbase = normalize_cp_base ~check:false env cb s in
+    let nm = off + normalize_cp_base ~check:false env cb s in
+    (* Make sure the position we are pointing to is valid in the context *)
+    (* List.length + 1 points to the instruction "after the last" and has 
+       special meaning depending on the context *)
+    if check then check_nm_cpos1 nm s; 
+    nm
+
+  let find_by_cpos1 ?(rev = true) (env : EcEnv.env) (cp1 : codepos1) (s : stmt) =
+    find_by_nmcpos1 ~rev (normalize_cpos1 env cp1 s) s
+
+  (* Selects the index for match arm *)
+  let select_match_arm_idx (env:env) (e: expr) (sel: string) =
+    let  _, indt, _ = oget (EcEnv.Ty.get_top_decl e.e_ty env) in
+    let  indt = oget (EcDecl.tydecl_as_datatype indt) in
+    let  cnames = List.fst indt.tydt_ctors in
+    try  List.findi (fun _ n -> EcSymbols.sym_equal sel n) cnames |> fst
+    with Not_found -> raise InvalidCPos 
+
+  (* Get the block pointed to by brsel for a given instruction *)
+  let normalize_brsel (env: env) (i: instr) (br: codepos_brsel) : (env * stmt) * nm_codepos_brsel =
+    match i.i_node, br with
+    | (Sif (_, t, _),  `Cond true)  -> (env, t), `Cond true
+    | (Sif (_, _, f),  `Cond false) -> (env, f), `Cond false
+    | (Swhile (_, s),  `Cond true)  -> (env, s), `Cond true
+    | (Smatch (e, ss), `Match ms)  -> 
+      let ix = select_match_arm_idx env e ms in
+      let (locals, s) = List.at ss ix in
+      let env = EcEnv.Var.bind_locals locals env in
+      begin try 
+        (env, s), `Match ix
+      with Invalid_argument _ -> 
+        raise InvalidCPos
+      end
+    | _ -> assert false
+
+  let select_branch (env: env) (i: instr) (br: codepos_brsel) : stmt = 
+    normalize_brsel env i br |> fst |> snd
+
+  (* Normalizes a code position step and returns the block it points to *)
+  let normalize_cpos_step (env: env) (s: stmt) ((cp1, brsel): codepos_step) : (env * stmt) * nm_codepos_step =
+    let cp1, brsel = normalize_cpos1 env cp1 s, brsel in
+    let (_, i, _) = find_by_nmcpos1 cp1 s in
+    let (env, s), nmbr = normalize_brsel env i brsel in
+    (env, s), (cp1, nmbr)
+
+  let normalize_cpos_path (env: env) (cpath: codepos_path) (s: stmt) : (env * stmt) * nm_codepos_path =
+    List.fold_left_map (fun (env, s) step -> normalize_cpos_step env s step) (env, s) cpath
+
+  let normalize_cpos (env: env) ((cpath, cp1) : codepos) (s: stmt) : (env * stmt) * nm_codepos =
+    let (env, s), npath = normalize_cpos_path env cpath s in
+    (env, s), (npath, normalize_cpos1 env cp1 s)
+
+  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 
+    | `Relative i -> 
+      let nm = (base + i) in
+      check_nm_cpos1 nm s; nm
+
+  let resolve_offset1_from_cpos1_range env ((start, fin): nm_codepos1_range) (off: codeoffset1) (s: stmt) : nm_codepos1 =
+    match off with
+    | `Absolute off -> 
+      let nm = normalize_cpos1 env off s in
+      if nm_codepos_in_nm_codepos_range nm (start, fin) then raise InvalidCPos; nm
+    | `Relative i -> 
+      let nm = if i > 0 then (fin + i - 1) else start + i in
+      check_nm_cpos1 nm s; nm
+
+  let normalize_cpos1_range ?(strict = false) env ((base, off): codepos1_range) (s: stmt) : nm_codepos1_range = 
+    let start = normalize_cpos1 env base s in
+    let fin = resolve_offset1_from_cpos1 env start off s in
+    if start > fin || (strict && start = fin) then raise InvalidCPos;
+    (start, fin)
+
+  let normalize_cpos_range ?(strict = false) env (cpath, cp1r: codepos_range) (s: stmt) : (env * stmt) * nm_codepos_range =
+    let (env, s), npath = normalize_cpos_path env cpath s in
+    let nm1r = normalize_cpos1_range ~strict env cp1r s in
+    (env, s), (npath, nm1r)
+
+    (* 
+    i is included in the second list since 
+    intervals are closed-open [a,b[
+
+     Extremal cases:
+     - Splitting at 1 should get [], s
+     - Splitting at List.length + 1 should get s, []
+  *)
+  let split_at_nmcpos1 ?(rev=false) (nm: nm_codepos1) (s: stmt) = 
+    (* (nm - 1) = convert nm to 0-indexing *)
+    if (nm - 1) = List.length s.s_node then s.s_node, [] else
+    let s1, i, s2 = find_by_nmcpos1 ~rev nm s in
+    (s1, (i::s2))
+
+  (* Splits instructions by a half-open range specified by two codepositions *)
+  (* Flags:
+    - strict = allow empty ranges where endpoints are equal 
+    - rev1 = return first list reversed?
+    - rev2 = return second list reversed?
+    if not string and endpoints are the same then the values of 
+    rev1 and rev2 should be the same in the call
+  *)
+  let split_by_nmcpr1 ?(strict=false) ?(rev1=false) ?(rev2=false) ((start, fin): nm_codepos1_range) (s: stmt) : instr list * instr list * instr list = 
+    (* if middle range empty then 
+      FIXME: unify with below, uniform implementation should work
+      *)
+    if not strict && start = fin then
+      begin 
+        if rev1 != rev2 then assert false; (* Programming error *)
+        let s1, s2 = split_at_nmcpos1 ~rev:rev1 start s in
+        s1, [], s2
+      end
+    else
+      begin
+        (* Splits s=[0;n[ into:
+           [0; a[ \/ [a;n[ 
+         *)
+        let s1, s2 = split_at_nmcpos1 ~rev:rev1 start s in
+        (* 
+           Re-align position b from block [1;n[ to block 
+           [a; n[ by realigning block [a; n[ to
+           [1; n - (a - 1) [ through
+           (i |-> i - a + 1)
+         *)
+        let fin = fin - start + 1 in
+        (* FIXME: How do we deal with instr list vs stmt?
+            1. Retag at the end of every function and always ret a stmt?
+            2. Deal with instr lists everywhere in the backend and then
+               use a wrapper for mli functions that returns a stmt?
+            3. Case by case 
+        *)
+        let s2, s3 = split_at_nmcpos1 ~rev:rev2 fin (stmt s2) in 
+        s1, s2, s3
       end
 
-    | `ByMatch (i, cm) ->
-        let (s1, i, s2) = find_by_cp_match env (i, cm) s in
+  let split_by_nmcpr1s (cps: nm_codepos1 list) (s: stmt) : instr list list =
+    let cps = List.map (fun t -> t-1) cps in (* Convert to 0-indexing *)
+    let doit ((prev, s, acc): int * instr list * instr list list) (cp: int) : (int * instr list * instr list list) =
+      let s1, s2 = try 
+        List.takedrop (cp - prev) s 
+      with (Invalid_argument _ | Not_found) -> raise InvalidCPos
+      in
+      (cp, s2, s1::acc)
+    in
+    let (_, slast, ss) = List.fold_left doit (0, s.s_node, []) cps in
+    List.rev (slast::ss)
+
+  let split_at_cp_base ?rev (env : EcEnv.env) (cb : cp_base) (s : stmt) =
+    split_at_nmcpos1 ?rev (normalize_cp_base env cb s) s
+  
+  let split_at_cpos1 ?rev (env : EcEnv.env) (cp : codepos1) (s: stmt) =
+    split_at_nmcpos1 ?rev (normalize_cpos1 env cp s) s
 
-        match after with
-        | `No -> (List.rev s1, i :: s2)
-        | _   -> (List.rev_append s1 [i], s2)
+  let split_at_cpos ?rev (env: env) ((cpath, cp1): codepos) (s : stmt) =
+    let (env, s), _cpath = normalize_cpos_path env cpath s in
+    env, split_at_cpos1 ?rev env cp1 s
+
+  let may_split_at_cpos1 ?(rev = false) (env: env) (cpos1: codepos1 option) (s: stmt) =
+    ofdfl
+      (fun () -> if rev then (s.s_node, []) else ([], s.s_node))
+      (omap ((split_at_cpos1 env)^~ s) cpos1)
+end
 
-  let split_at_cpos1 ~after (env : EcEnv.env) ((ipos, cb) : codepos1) s =
-    let (s1, s2) = split_at_cp_base ~after env cb s in
+(* -------------------------------------------------------------------- *)
+module Zipper = struct
+  open Position
 
-    let (s1, s2) =
-      match ipos with
-      | off when off > 0 ->
-          let (ss1, ss2) =
-            try  List.takedrop off s2
-            with (Invalid_argument _ | Not_found) -> raise InvalidCPos in
-          (s1 @ ss1, ss2)
+  module P = EcPath
 
-      | off when off < 0 ->
-          let (ss1, ss2) =
-            try  List.takedrop (List.length s1 + off) s1
-            with (Invalid_argument _ | Not_found) -> raise InvalidCPos in
-          (ss1, ss2 @ s2)
+  type ('a, 'state) folder =
+    env -> 'a -> 'state -> instr -> 'state * instr list
+
+  type ('a, 'state) folder_l =
+    env -> 'a -> 'state -> instr list -> 'state * instr list
+
+  type spath_match_ctxt = {
+    locals : (EcIdent.t * ty) list;
+    prebr  : ((EcIdent.t * ty) list * stmt) list;
+    postbr : ((EcIdent.t * ty) list * stmt) list;
+  }
 
-      | _ -> (s1, s2)
+  type ipath =
+  | ZTop
+  | ZWhile  of expr * spath
+  | ZIfThen of expr * spath * stmt
+  | ZIfElse of expr * stmt  * spath
+  | ZMatch  of expr * spath * spath_match_ctxt
 
-    in (s1, s2)
+  and spath = (instr list * instr list) * ipath
 
-  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
+  type zipper = {
+    z_head : instr list;                (* instructions on my left  (rev)      *)
+    z_tail : instr list;                (* instructions on my right (me incl.) *)
+    z_path : ipath;                     (* path (zipper) leading to me         *)
+    z_env  : env option;
+  }
 
-  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 ?env hd tl zpr = { z_head = hd; z_tail = tl; z_path = zpr; z_env = env; }
 
-  let zipper_at_nm_cpos1
+  let zipper_step_into_block
     (env        : EcEnv.env)
-    ((cp1, sub) : codepos1 * codepos_brsel)
+    ((cp1, sub) : codepos_step)
     (s          : stmt)
     (zpr        : ipath)
-  : (ipath * stmt) * (codepos1 * codepos_brsel) * env
+  : (ipath * stmt) * nm_codepos_step * env
   =
+    (* FIXME: unify with normalization above *)
     let (s1, i, s2) = find_by_cpos1 env cp1 s in
-    let zpr, env =
+    let zpr, step, env =
       match i.i_node, sub with
       | Swhile (e, sw), `Cond true ->
-          (ZWhile (e, ((s1, s2), zpr)), sw), env
+          (ZWhile (e, ((s1, s2), zpr)), sw), `Cond true, env
 
       | Sif (e, ifs1, ifs2), `Cond true ->
-          (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1), env
+          (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1), `Cond true, env
 
       | Sif (e, ifs1, ifs2), `Cond false ->
-          (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2), env
+          (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2), `Cond false, env
 
       | Smatch (e, bs), `Match cn ->
-          let _, indt, _ = oget (EcEnv.Ty.get_top_decl e.e_ty env) in
-          let indt = oget (EcDecl.tydecl_as_datatype indt) in
-          let cnames = List.fst indt.tydt_ctors in
-          let ix, _ =
-            try  List.findi (fun _ n -> EcSymbols.sym_equal cn n) cnames
-            with Not_found -> raise InvalidCPos
-          in
+          let ix = select_match_arm_idx env e cn in
           let prebr, (locals, body), postbr = List.pivot_at ix bs in
           let env = EcEnv.Var.bind_locals locals env in
-          (ZMatch (e, ((s1, s2), zpr), { locals; prebr; postbr; }), body), env
+          (ZMatch (e, ((s1, s2), zpr), { locals; prebr; postbr; }), body), `Match ix, env
 
       | _ -> raise InvalidCPos
-    in zpr, ((0, `ByPos (1 + List.length s1)), sub), env
+    in zpr, ((1 + List.length s1), step), env
 
-  let zipper_of_cpos_r (env : EcEnv.env) ((nm, cp1) : codepos) (s : stmt) =
-    let ((zpr, s), env), nm =
-      List.fold_left_map
-        (fun ((zpr, s), env) nm1 -> let zpr, s, env = zipper_at_nm_cpos1 env nm1 s zpr in (zpr, env), s)
-        ((ZTop, s), env) nm in
+  let pre_zipper_of_codepos_path (env : EcEnv.env) (cpath: codepos_path) (s: stmt) =
+    List.fold_left_map
+      (fun ((zpr, s), env) cps -> 
+      let (zpr, s), step, env = zipper_step_into_block env cps s zpr in ((zpr, s), env), step)
+      ((ZTop, s), env) cpath 
 
-    let s1, i, s2 = find_by_cpos1 env cp1 s in
-    let zpr = zipper ~env s1 (i :: s2) zpr in
+  let zipper_of_cpos_r (env : EcEnv.env) ((cpath, cp1) : codepos) (s : stmt) =
+    let ((zpr, s), env), nmcp = pre_zipper_of_codepos_path env cpath s in
+      
+    let nm = normalize_cpos1 env cp1 s in
+    let s1, s2 = split_at_nmcpos1 ~rev:true nm s in
+    let zpr = zipper ~env s1 s2 zpr in
 
-    (zpr, (nm, (0, `ByPos (1 + List.length s1))))
+    (zpr, ((nmcp, nm), s))
 
   let zipper_of_cpos (env : EcEnv.env) (cp : codepos) (s : stmt) =
     fst (zipper_of_cpos_r env cp s)
 
-  let zipper_of_cpos_range env cpr s =
-    let top, bot = cpr in
-    let zpr, (_, pos) = zipper_of_cpos_r env top s in
-    match bot with
-    | `Base cp -> begin
-      let zpr', (_, pos') = zipper_of_cpos_r env cp s in
-      (* The two positions should identify the same block *)
-      if zpr'.z_path <> zpr.z_path then
-        raise InvalidCPos;
-
-      (* The end position should be after the start *)
-      match pos, pos' with
-      | (_, `ByPos x), (_, `ByPos y) when x <= y ->
-          zpr, (0, `ByPos (y - x))
-      | _ -> raise InvalidCPos
-    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
-
-  let may_split_at_cpos1 ?(rev = false) env cpos1 s =
-    ofdfl
-      (fun () -> if rev then (s.s_node, []) else ([], s.s_node))
-      (omap ((split_at_cpos1 env)^~ s) cpos1)
-
-  let rec zip i ((hd, tl), ip) =
+    (* 
+     Returns:
+      A zipper pointing to the start of the range
+      A split of the block according to the range 
+      The normalized cpos range
+   *) 
+  let zipper_and_split_of_cpos_range (env: env) (path, (base, off) : codepos_range) (s: stmt) : zipper * _ * nm_codepos_range=
+    let (zpr, ((cpath, cbase), s)) = zipper_of_cpos_r env (path, base) s in
+    let coff = resolve_offset1_from_cpos1 env cbase off s in
+    let ss = split_by_nmcpr1 (cbase, coff) s in
+    (zpr, ss, (cpath, (cbase, coff)))
+
+  let rec zip (i: instr option) (((hd, tl), ip): (instr list * instr list) * ipath) =
     let s = stmt (List.rev_append hd (List.ocons i tl)) in
 
     match ip with
@@ -297,14 +549,14 @@ module Zipper = struct
 
   let zip zpr = zip None ((zpr.z_head, zpr.z_tail), zpr.z_path)
 
-  let after ~strict zpr =
+  let after ~strict (zpr: zipper) =
     let rec doit acc ip =
       match ip with
       | ZTop                          -> acc
       | ZWhile  (_, ((_, is), ip))    -> doit (is :: acc) ip
       | ZIfThen (_, ((_, is), ip), _) -> doit (is :: acc) ip
       | ZIfElse (_, _, ((_, is), ip)) -> doit (is :: acc) ip
-      | ZMatch (_, ((_, is), ip), _) -> doit (is :: acc) ip
+      | ZMatch (_, ((_, is), ip), _)  -> doit (is :: acc) ip
     in
 
     let after =
@@ -315,18 +567,18 @@ module Zipper = struct
     in
       List.rev after
 
-  let fold_range env cenv cpr f state s =
-    let (zpr, _), (s, tl) = zipper_and_split_of_cpos_range env cpr s in
+  let fold_range (env: env) cenv (cpr: codepos_range) f state (s: stmt) =
+    let zpr, (_pre, s, tl), _nmcpr = 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 =
+  let map_range (env: env) (cpr: codepos_range) f (s: stmt) =
     snd (fold_range env () cpr (fun env () _ si -> (), f env si) () s)
 
-  let fold env cenv cp f state s =
+  let fold (env: env) cenv ((path, cp1): codepos) f state (s: stmt) =
     let f env cenv state si = f env cenv state (List.hd si) in
-    fold_range env cenv (cp, `Offset (cpos 0)) f state s
+    fold_range env cenv (path, (cp1, `Relative 1)) f state s
 
   let map env cpos f s =
     fst_map
diff --git a/src/ecMatching.mli b/src/ecMatching.mli
index 66c6bc200..c9d90d489 100644
--- a/src/ecMatching.mli
+++ b/src/ecMatching.mli
@@ -21,23 +21,128 @@ module Position : sig
     | `Call   of lvmatch
   ]
 
+
   and lvmatch = [ `LvmNone | `LvmVar of EcTypes.prog_var ]
 
+  exception InvalidCPos
+
   type cp_base = [
-    | `ByPos of int
+    | `ByPos of int (* Always <> 0 *)
     | `ByMatch of int option * cp_match
   ]
 
-  type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol]
-  type codepos1      = int * cp_base
-  type codepos       = (codepos1 * codepos_brsel) list * codepos1
-  type codepos_range = codepos * [`Base of codepos | `Offset of codepos1]
-  type codeoffset1   = [`ByOffset of int | `ByPosition of codepos1]
+  (* Branch selection *)
+  type codepos_brsel  = [`Cond of bool | `Match of EcSymbols.symbol]
+  type nm_codepos_brsel = [`Cond of bool | `Match of int]
+  (* Linear code position inside a block *)
+  type codepos1       = int * cp_base
+  (* Normalized code position inside a block, always > 0 *)
+  type nm_codepos1    = int
+  (* Codeposition path step *)
+  type codepos_step   = (codepos1 * codepos_brsel)
+  type nm_codepos_step = (int * nm_codepos_brsel)
+  (* Block selection by codepos + branch selection *)
+  type codepos_path   = codepos_step list
+  type nm_codepos_path = nm_codepos_step list
+  (* Full codeposition = path to block + position in block *)
+  type codepos         = codepos_path * codepos1
+  type nm_codepos      = nm_codepos_path * nm_codepos1
+  (* Code position offset *)
+  type codeoffset1    = [`Relative of int | `Absolute of codepos1]
+  (* Range of linear code positions *)
+  type codepos1_range = (codepos1 * codeoffset1)
+  (* Normalized codepos1 range *)
+  type nm_codepos1_range = (int * int)
+  (* Range + block path *)
+  type codepos_range  = codepos_path * codepos1_range
+  (* Normalized codepos range *)
+  type nm_codepos_range = nm_codepos_path * nm_codepos1_range
+
+  (* Top-level first and last position *)
+  val cpos_first : codepos
+  val cpos_last  : codepos
+  
+  (* Block-level first and last position *)
+  val cpos1_first       : codepos1
+  val cpos1_last        : codepos1
+  val cpos1_after_last  : codepos1
+
+  val cpos1_to_top : codepos1 -> codepos
 
   val shift1 : offset:int -> codepos1 -> codepos1
   val shift  : offset:int -> codepos  -> codepos
 
   val resolve_offset : base:codepos1 -> offset:codeoffset1 -> codepos1
+
+  val codepos1_range_of_codepos1 : codepos1 -> codepos1_range
+  val codepos_range_of_codepos   : codepos  -> codepos_range
+
+  val nm_codepos1_range_of_nm_codepos1 : nm_codepos1 -> nm_codepos1_range
+  val nm_codepos_range_of_nm_codepos   : nm_codepos  -> nm_codepos_range
+
+  val disjoint : nm_codepos1_range -> nm_codepos1_range -> bool
+
+  val nm_codepos_in_nm_codepos_range : nm_codepos1 -> nm_codepos1_range -> bool
+
+  module Notations : sig
+    val (|+>) : codepos -> int -> codepos
+
+    val (+>) : codepos1 -> int -> codepos1
+
+    val (<+|) : codepos -> int -> codepos
+
+    val (<+) : codepos1 -> int -> codepos1
+  end
+
+  (* Normalization functions *)
+  val find_by_cp_match : env -> (int option * cp_match) -> stmt -> instr list * instr * instr list
+
+  val find_by_nmcpos1 : ?rev:bool -> nm_codepos1 -> stmt -> instr list * instr * instr list
+
+  val check_nm_cpos1 : nm_codepos1 -> stmt -> unit
+
+  val normalize_cp_base : ?check:bool -> env -> cp_base -> stmt -> nm_codepos1
+
+  val normalize_cpos1 : ?check:bool -> env -> codepos1 -> stmt -> nm_codepos1
+
+  val resolve_offset1_from_cpos1 : env -> nm_codepos1 -> codeoffset1 -> stmt -> nm_codepos1 
+
+  val resolve_offset1_from_cpos1_range : env -> nm_codepos1_range -> codeoffset1 -> stmt -> nm_codepos1 
+
+  val find_by_cpos1 : ?rev:bool -> env -> codepos1 -> stmt -> instr list * instr * instr list
+
+  val select_match_arm_idx : env -> expr -> string -> int
+
+  val normalize_brsel : env -> instr -> codepos_brsel -> (env * stmt) * nm_codepos_brsel
+
+  val select_branch : env -> instr -> codepos_brsel -> stmt
+
+  val normalize_cpos_step : env -> stmt -> codepos_step -> (env * stmt) * nm_codepos_step
+
+  val normalize_cpos_path : env -> codepos_path -> stmt -> (env * stmt) * nm_codepos_path
+
+  val normalize_cpos : env ->  codepos -> stmt -> (env * stmt) * nm_codepos
+
+  val normalize_cpos1_range : ?strict:bool -> env -> codepos1_range -> stmt -> nm_codepos1_range 
+
+  val normalize_cpos_range : ?strict:bool -> env -> codepos_range -> stmt -> (env * stmt) * nm_codepos_range
+
+  val split_at_nmcpos1 : ?rev:bool -> nm_codepos1 -> stmt -> instr list * instr list
+
+  val split_at_cp_base : ?rev:bool -> env -> cp_base -> stmt -> instr list * instr list
+
+  val split_at_cpos1 : ?rev:bool -> env -> codepos1 -> stmt -> instr list * instr list
+
+  val split_at_cpos : ?rev:bool -> env -> codepos -> stmt -> env * (instr list * instr list)
+
+  (* 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
+
+  val split_by_nmcpr1 : ?strict:bool -> ?rev1:bool -> ?rev2:bool -> nm_codepos1_range -> stmt -> instr list * instr list * instr list
+
+  val split_by_nmcpr1s : nm_codepos1 list -> stmt -> instr list list
+
+  val cpos1 : int -> codepos1
 end
 
 (* -------------------------------------------------------------------- *)
@@ -66,20 +171,8 @@ module Zipper : sig
     z_env  : env option;                (* env with local vars from previous instructions *)
   }
 
-  exception InvalidCPos
-
-  (* Create a codepos1 from a top-level absolute position *)
-  val cpos : int -> codepos1
-
-  (* Split a statement from a top-level position (codepos1) *)
-  val find_by_cpos1  : ?rev:bool -> env -> codepos1 -> stmt -> instr list * instr * instr list
-  val split_at_cpos1 : env -> codepos1 -> stmt -> instr list * instr list
-
-  (* 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
+(*   val offset_of_position : env -> codepos1 -> stmt -> int *)
 
   (* [zipper] soft constructor *)
   val zipper : ?env : env -> instr list -> instr list -> ipath -> zipper
@@ -90,7 +183,7 @@ module Zipper : sig
    * positions only). The second variant simply throw away the second
    * output.
    *)
-  val zipper_of_cpos_r : env -> codepos -> stmt -> zipper * codepos
+  val zipper_of_cpos_r : env -> codepos -> stmt -> zipper * (nm_codepos * stmt)
   val zipper_of_cpos : env -> codepos -> stmt -> zipper
 
   (* Return the zipper for the stmt [stmt] from the start of the code position
@@ -98,8 +191,8 @@ module Zipper : sig
    * the zipper that represents the final position in the range.
    * 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)
+(*   val zipper_of_cpos_range : env -> codepos_range -> stmt -> zipper * codepos1 *)
+  val zipper_and_split_of_cpos_range : env -> codepos_range -> stmt -> zipper * (instr list * instr list * instr list) * nm_codepos_range
 
   (* Zip the zipper, returning the corresponding statement *)
   val zip : zipper -> stmt
diff --git a/src/ecParser.mly b/src/ecParser.mly
index 52e9f4b49..f747921c4 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -1008,7 +1008,6 @@ pffilter:
       i=pfpos? COLON j=pfpos? { `Range (i, j) }
     | i=pfpos { `Single i }, COMMA)
   RBRACKET
-
   { PFRange (flat, rg) }
 
 | LPBRACE flat=iboption(SLASH) x=ident IN h=form_h RPBRACE
@@ -2565,29 +2564,39 @@ branch_select:
 | DOT { `Cond true }
 | QUESTION { `Cond false }
 
-%inline nm1_codepos:
+%inline codepos_step:
 | i=codepos1 bs=branch_select
     { (i, bs) }
 
+(* FIXME: Syntax *)
+codeoffset1:
+| i=sword       { (`Relative   i :> pcodeoffset1) }
+| AT p=codepos1 { (`Absolute   p :> pcodeoffset1) }
+
+(* FIXME: Unify with above *)
+(* Shift to convert input closed range into closed-open form *)
+%inline codepos1_range:
+| LBRACKET cps=codepos1 DOTDOT cpe=codepos1   RBRACKET { (cps, `Absolute (shift1 ~offset:1 cpe)) }
+| LBRACKET cps=codepos1 MINUS cpe=sword RBRACKET { (cps, `Relative cpe) }
+
+%inline codepos_path:
+| path=rlist0(codepos_step, empty) { path }
+
 codepos:
-| nm=rlist0(nm1_codepos, empty) i=codepos1
-    { (nm, i) }
+| path=codepos_path i=codepos1
+  { (path, i) }
 
 codepos_range:
-| LBRACKET cps=codepos DOTDOT cpe=codepos RBRACKET { (cps, `Base cpe) }
-| LBRACKET cps=codepos MINUS cpe=codepos1 RBRACKET { (cps, `Offset cpe) }
+| path=codepos_path COLON i=codepos1_range
+  { (path, i) }
 
 codepos_or_range:
-| cp=codepos { (cp, `Offset (0, `ByPos 0)) }
-| cpr=codepos_range  { cpr }
-
-codeoffset1:
-| i=sword       { (`ByOffset   i :> pcodeoffset1) }
-| AT p=codepos1 { (`ByPosition p :> pcodeoffset1) }
+| cp=codepos { Pos cp }
+| cpr=codepos_range { Range cpr }
 
 o_codepos1:
 | UNDERSCORE { None }
-| i=codepos1 { Some i}
+| i=codepos1 { Some i }
 
 s_codepos1:
 | n=codepos1
@@ -2650,11 +2659,8 @@ swap_position:
 | offset=codeoffset1
     { { interval = None; offset; } }
 
-| start=codepos1 offset=codeoffset1
-    { { interval = Some (start, None); offset; } }
-
-| LBRACKET start=codepos1 DOTDOT end_=codepos1 RBRACKET offset=codeoffset1
-    { { interval = Some (start, Some end_); offset; } }
+| interval=codepos_or_range offset=codeoffset1
+    { { interval = Some interval; offset; } }
 
 side:
 | LBRACE n=word RBRACE {
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 8e12874e8..f7aed89d4 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -51,16 +51,33 @@ and plvmatch = [ `LvmNone | `LvmVar of pqsymbol ]
 
 type pcp_base  = [ `ByPos of int | `ByMatch of int option * pcp_match ]
 
+(* Code positions *)
 type pbranch_select = [`Cond of bool | `Match of psymbol]
 type pcodepos1 = int * pcp_base
-type pcodepos  = (pcodepos1 * pbranch_select) list * pcodepos1
-type pcodepos_range  = pcodepos * [`Base of pcodepos | `Offset of pcodepos1]
+type pcodepos_step = (pcodepos1 * pbranch_select)
+type pcodepos_path = pcodepos_step list 
+type pcodepos  = pcodepos_path * pcodepos1
 type pdocodepos1 = pcodepos1 doption option
 
+let shift1 ((off,base): pcodepos1) ~(offset: int) : pcodepos1 = 
+  (off + offset, base)
+  
+let shift ((path,cp1): pcodepos) ~(offset: int) : pcodepos = 
+  (path, shift1 ~offset cp1)
+
+(* Code position offsets *)
 type pcodeoffset1 = [
-  | `ByOffset   of int
-  | `ByPosition of pcodepos1
+  | `Relative of int
+  | `Absolute of pcodepos1
 ]
+
+(* Code position ranges *)
+type pcodepos1_range = (pcodepos1 * pcodeoffset1)
+type pcodepos_range  = pcodepos_path * pcodepos1_range
+type pcodepos_or_range = 
+  | Pos   of pcodepos
+  | Range of pcodepos_range
+
 (* -------------------------------------------------------------------- *)
 
 type pty_r =
@@ -351,7 +368,7 @@ and pstructure_item =
   | Pst_import   of (pmsymbol located) list
 
 and pupdate_var = psymbol list * pty
-and pupdate_fun = psymbol * (psymbol list * pty) list * ((pcodepos_range located * pupdate_item) list * pexpr option)
+and pupdate_fun = psymbol * (psymbol list * pty) list * ((pcodepos_or_range located * pupdate_item) list * pexpr option)
 
 and pupdate_item =
   | Pup_stmt of pupdate_stmt
@@ -538,7 +555,7 @@ type preduction = {
 
 (* -------------------------------------------------------------------- *)
 type pswap_kind = {
-  interval : (pcodepos1 * pcodepos1 option) option;
+  interval : pcodepos_or_range option;
   offset   : pcodeoffset1;
 }
 
@@ -679,7 +696,7 @@ type outline_kind =
 
 type outline_info = {
     outline_side: side;
-    outline_range: pcodepos_range;
+    outline_range: pcodepos_or_range;
     outline_kind: outline_kind;
 }
 
@@ -706,7 +723,7 @@ type conseq_ppterm = (conseq_contra * (conseq_info) option) gppterm
 
 (* -------------------------------------------------------------------- *)
 type sim_info = {
-  sim_pos  : pcodepos1 pair option;
+  sim_pos  : pcodepos1 pair option; 
   sim_hint : (pgamepath option pair * pformula) list * pformula option;
   sim_eqs  : pformula option
 }
@@ -790,7 +807,7 @@ type phltactic =
   | Prwprgm of rwprgm
   | Pprocrewrite   of side option * pcodepos * prrewrite
   | Pprocrewriteat of psymbol * ppterm
-  | Pchangestmt    of side option * pcodepos_range * pstmt
+  | Pchangestmt    of side option * pcodepos_or_range * pstmt
   | Phoaresplit
 
     (* Eager *)
diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml
index c3f29cdfa..645cded55 100644
--- a/src/ecPrinting.ml
+++ b/src/ecPrinting.ml
@@ -2407,22 +2407,34 @@ let pp_codepos1 (ppe : PPEnv.t) (fmt : Format.formatter) ((off, cp) : CP.codepos
 (* -------------------------------------------------------------------- *)
 let pp_codeoffset1 (ppe : PPEnv.t) (fmt : Format.formatter) (offset : CP.codeoffset1) =
   match offset with
-  | `ByPosition p -> Format.fprintf fmt "%a" (pp_codepos1 ppe) p
-  | `ByOffset   o -> Format.fprintf fmt "%d" o
+  | `Absolute p -> Format.fprintf fmt "%a" (pp_codepos1 ppe) p
+  | `Relative o -> Format.fprintf fmt "%d" o
+
+let pp_codepos_brsel (fmt: Format.formatter) (br: CP.codepos_brsel) = 
+  Format.fprintf fmt "%s"
+  (match br with
+  | `Cond true -> "."
+  | `Cond false -> "?"
+  | `Match cp -> Format.sprintf "#%s." cp)
+
+let pp_codepos_step (ppe: PPEnv.t) (fmt: Format.formatter) ((cp, br): CP.codepos_step) = 
+  Format.fprintf fmt "%a%a" (pp_codepos1 ppe) cp pp_codepos_brsel br
+
+let pp_codepos_path ppe =
+  (pp_list "" (pp_codepos_step ppe))
 
 (* -------------------------------------------------------------------- *)
-let pp_codepos (ppe : PPEnv.t) (fmt : Format.formatter) ((nm, cp1) : CP.codepos) =
-  let pp_nm (fmt : Format.formatter) ((cp, bs) : CP.codepos1 * CP.codepos_brsel) =
-    let bs =
-      match bs with
-      | `Cond  true  -> "."
-      | `Cond  false -> "?"
-      | `Match cp    -> Format.sprintf "#%s." cp
-      in
-    Format.fprintf fmt "%a%s" (pp_codepos1 ppe) cp bs
-  in
+let pp_codepos (ppe : PPEnv.t) (fmt : Format.formatter) ((cpath, cp1) : CP.codepos) =
+  Format.fprintf fmt "%a%a" (pp_codepos_path ppe) cpath (pp_codepos1 ppe) cp1
+
+let pp_codepos1_range (ppe: PPEnv.t) (fmt: Format.formatter) ((start, fin) : CP.codepos1_range) =
+  Format.fprintf fmt "%a%s%a" (pp_codepos1 ppe) start 
+  (match fin with | `Relative _ -> "+" | `Absolute _ -> "..")
+  (pp_codeoffset1 ppe) fin
+
+let pp_codepos_range (ppe: PPEnv.t) (fmt: Format.formatter) ((cpath, cp1r) : CP.codepos_range) =
+  Format.fprintf fmt "%a:[%a]" (pp_codepos_path ppe) cpath (pp_codepos1_range ppe) cp1r
 
-  Format.fprintf fmt "%a%a" (pp_list "" pp_nm) nm (pp_codepos1 ppe) cp1
 
 (* -------------------------------------------------------------------- *)
 let pp_opdecl_pr (ppe : PPEnv.t) fmt ((basename, ts, ty, op): symbol * ty_param list * ty * prbody option) =
diff --git a/src/ecTyping.ml b/src/ecTyping.ml
index 266b86dc8..49d9314f6 100644
--- a/src/ecTyping.ml
+++ b/src/ecTyping.ml
@@ -2283,7 +2283,7 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
       let body =
         List.fold_right (fun (cpr, up) bd ->
           let {pl_desc = cpr; pl_loc = loc} = cpr in
-          let cp = trans_codepos_range env cpr in
+          let cp = trans_codepos_or_range env cpr in
           let change env si =
             match up with
             | Pup_stmt sup ->
@@ -2295,7 +2295,7 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
           try
             EcMatching.Zipper.map_range env cp change bd
           with
-            | EcMatching.Zipper.InvalidCPos ->
+            | InvalidCPos ->
               tyerror loc env (InvalidModUpdate MUE_InvalidCodePos);
         )
         pupdates
@@ -3745,33 +3745,46 @@ and trans_codepos_brsel (bs : pbranch_select) : codepos_brsel =
   | `Cond b -> `Cond b
   | `Match { pl_desc = x } -> `Match x
 
+and trans_codepos_step ?(memory: memory option) (env: EcEnv.env) ((cp1, brsel): pcodepos_step) : codepos_step =
+  let cp1 = trans_codepos1 ?memory env cp1 in
+  let brsel = trans_codepos_brsel brsel in
+  (cp1, brsel)
+
+and trans_codepos_path ?(memory: memory option) (env: EcEnv.env) (cpath: pcodepos_path) : codepos_path =
+  List.map (trans_codepos_step ?memory env) cpath
+
 (* -------------------------------------------------------------------- *)
-and trans_codepos ?(memory : memory option) (env : EcEnv.env) ((nm, p) : pcodepos) : codepos =
-  let nm = List.map (fun (cp1, bs) -> (trans_codepos1 ?memory env cp1, trans_codepos_brsel bs)) nm in
+and trans_codepos ?(memory : memory option) (env : EcEnv.env) ((cpath, p) : pcodepos) : codepos =
+  let cpath = trans_codepos_path ?memory env cpath in
   let p = trans_codepos1 ?memory env p in
-  (nm, p)
+  (cpath, p)
+
+and trans_codeoffset1 ?(memory: memory option) (env : EcEnv.env) (o : pcodeoffset1) : codeoffset1 =
+  match o with
+  | `Relative i -> `Relative i
+  | `Absolute p -> `Absolute (trans_codepos1 ?memory env p)
+
+and trans_codepos1_range ?(memory: memory option) (env: EcEnv.env) ((start, off): pcodepos1_range) : codepos1_range =
+  let start = trans_codepos1 ?memory env start in
+  let off   = trans_codeoffset1 ?memory env off in
+  (start, off)
 
 (* -------------------------------------------------------------------- *)
-and trans_codepos_range ?(memory : memory option) (env : EcEnv.env) ((cps, cpe) : pcodepos_range) : codepos_range =
-  let cps = trans_codepos ?memory env cps in
-  let cpe =
-    match cpe with
-    | `Base cp ->
-      `Base (trans_codepos ?memory env cp)
-    | `Offset cp ->
-      `Offset (trans_codepos1 ?memory env cp)
-  in
-  (cps, cpe)
+and trans_codepos_range ?(memory : memory option) (env : EcEnv.env) ((cpath, (cstart, coff)) : pcodepos_range) : codepos_range =
+  let cpath = trans_codepos_path ?memory env cpath in
+  let cstart = trans_codepos1 ?memory env cstart in
+  let coff = trans_codeoffset1 ?memory env coff in
+  (cpath, (cstart, coff))
+
+and trans_codepos_or_range ?(memory: memory option) (env : EcEnv.env) (cpor: pcodepos_or_range) : codepos_range =
+  match cpor with
+  | Pos cp -> codepos_range_of_codepos (trans_codepos ?memory env cp)
+  | Range cpr -> trans_codepos_range ?memory env cpr
 
 (* -------------------------------------------------------------------- *)
 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
diff --git a/src/ecTyping.mli b/src/ecTyping.mli
index 6722b92b3..1eee25195 100644
--- a/src/ecTyping.mli
+++ b/src/ecTyping.mli
@@ -240,6 +240,7 @@ val transstmt : ?map:ismap -> env -> EcUnify.unienv -> pstmt -> stmt
 
 (* -------------------------------------------------------------------- *)
 val trans_codepos_range : ?memory:EcMemory.memory -> env -> pcodepos_range -> codepos_range
+val trans_codepos_or_range : ?memory:EcMemory.memory -> env -> pcodepos_or_range -> codepos_range
 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
diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml
index 87a3bc727..556f2b7cf 100644
--- a/src/phl/ecPhlCall.ml
+++ b/src/phl/ecPhlCall.ml
@@ -160,14 +160,14 @@ let t_ehoare_call_core fpre fpost tc =
 let t_ehoare_call fpre fpost tc =
   let _, _, _, s, _, wppre, _ = ehoare_call_pre_post fpre fpost tc in
   let tcenv =
-    EcPhlSeq.t_ehoare_seq (EcMatching.Zipper.cpos (List.length s.s_node)) wppre tc in
+    EcPhlSeq.t_ehoare_seq (EcMatching.Position.cpos1 (List.length s.s_node)) wppre tc in
   let tcenv = FApi.t_swap_goals 0 1 tcenv in
   FApi.t_sub [t_ehoare_call_core fpre fpost; t_id] tcenv
 
 let t_ehoare_call_concave f fpre fpost tc =
   let _, _, _, s, _, wppre, wppost = ehoare_call_pre_post fpre fpost tc in
   let tcenv =
-    EcPhlSeq.t_ehoare_seq (EcMatching.Zipper.cpos (List.length s.s_node))
+    EcPhlSeq.t_ehoare_seq (EcMatching.Position.cpos1 (List.length s.s_node))
      (map_ss_inv2 (fun wppre f -> f_app_simpl f [wppre] txreal) wppre f) tc in
   let tcenv = FApi.t_swap_goals 0 1 tcenv in
   let t_call =
diff --git a/src/phl/ecPhlCodeTx.ml b/src/phl/ecPhlCodeTx.ml
index 2968953af..9dbdb4b83 100644
--- a/src/phl/ecPhlCodeTx.ml
+++ b/src/phl/ecPhlCodeTx.ml
@@ -330,9 +330,9 @@ let cfold_stmt ?(simplify = true) (pf, hyps) (me : memenv) (olen : int option) (
 
 (* -------------------------------------------------------------------- *)
 let t_cfold_r side cpos olen g =
-  let tr = fun side -> `Fold (side, cpos, olen) in
-  let cb = fun cenv _ me zpr -> cfold_stmt cenv me olen zpr in
-  t_code_transform side ~bdhoare:true cpos tr (t_zip cb) g
+    let tr = fun side -> `Fold (side, cpos, olen) in
+    let cb = fun cenv _ me zpr -> cfold_stmt cenv me olen zpr in
+    t_code_transform side ~bdhoare:true cpos tr (t_zip cb) g 
 
 (* -------------------------------------------------------------------- *)
 let t_kill      = FApi.t_low3 "code-tx-kill"      t_kill_r
diff --git a/src/phl/ecPhlCond.ml b/src/phl/ecPhlCond.ml
index 69d5c4210..a3dade6a8 100644
--- a/src/phl/ecPhlCond.ml
+++ b/src/phl/ecPhlCond.ml
@@ -33,7 +33,7 @@ module LowInternal = struct
 
    let t_sub b tc =
      FApi.t_on1seq 0
-       (EcPhlRCond.t_rcond side b (Zpr.cpos 1))
+       (EcPhlRCond.t_rcond side b (EcMatching.Position.cpos1 1))
        (FApi.t_seqs
           [t_introm; EcPhlSkip.t_skip; t_intros_i [m2;h];
            t_finalize h h1 h2; t_simplify])
@@ -113,10 +113,10 @@ let rec t_equiv_cond side tc =
              (FApi.t_seqsub
                 (t_equiv_cond (Some `Left))
                 [FApi.t_seqsub
-                   (EcPhlRCond.Low.t_equiv_rcond `Right true (Zpr.cpos 1))
+                   (EcPhlRCond.Low.t_equiv_rcond `Right true (EcMatching.Position.cpos1 1))
                    [t_aux; t_clear hiff];
                  FApi.t_seqsub
-                   (EcPhlRCond.Low.t_equiv_rcond `Right false (Zpr.cpos 1))
+                   (EcPhlRCond.Low.t_equiv_rcond `Right false (EcMatching.Position.cpos1 1))
                    [t_aux; t_clear hiff]]))
           tc
 
@@ -223,7 +223,7 @@ end = struct
       in
 
       tc
-        |> EcPhlRCond.t_rcond_match side cname (Zpr.cpos 1)
+        |> EcPhlRCond.t_rcond_match side cname (EcMatching.Position.cpos1 1)
         @+ [discharge; clean]
     in
 
diff --git a/src/phl/ecPhlEager.ml b/src/phl/ecPhlEager.ml
index 800de9b7d..780347f42 100644
--- a/src/phl/ecPhlEager.ml
+++ b/src/phl/ecPhlEager.ml
@@ -4,7 +4,7 @@ open EcEnv
 open EcFol
 open EcLowGoal
 open EcLowPhlGoal
-open EcMatching.Zipper
+open EcMatching.Position
 open EcModules
 open EcPV
 open EcTypes
@@ -67,10 +67,16 @@ let destruct_eager tc s =
   let env = FApi.tc1_env tc
   and es = tc1_as_equivS tc
   and ss = List.length s.s_node in
+  Format.eprintf "ss: %d@." ss;
+
+  let ppe = EcPrinting.PPEnv.ofenv env in
 
   let c, c' = (es.es_sl, es.es_sr) in
-  let z, c = s_split env (Zpr.cpos ss) c
-  and c', z' = s_split env (Zpr.cpos (List.length c'.s_node - ss)) c' in
+  let z, c = s_split env EcMatching.Position.Notations.(cpos1_first +> ss) c 
+  and c', z' = s_split env EcMatching.Position.Notations.(cpos1_last <+ ss) c' in
+  Format.eprintf "z: %a@. z': %a@." 
+  EcPrinting.(pp_stmt ppe) (stmt z)
+  EcPrinting.(pp_stmt ppe) (stmt z');
 
   let env, _, _ = FApi.tc1_eflat tc in
   let z_eq_s = ER.EqTest.for_stmt env (stmt z) s
@@ -96,7 +102,8 @@ let destruct_on_op id_op tc =
   let env = FApi.tc1_env tc and es = tc1_as_equivS tc in
   let s =
     try
-      let s, _ = split_at_cpos1 env (-1, `ByMatch (Some (-1), id_op)) es.es_sl
+      (* FIXME CPOS PR: Add function to do these things *)
+      let s, _ = split_at_cpos1 env (0, `ByMatch (Some (-1), id_op)) es.es_sl
       (* ensure the right statement also contains an [id_op]: *)
       and _, _ = split_at_cpos1 env (1, `ByMatch (None, id_op)) es.es_sr in
       s
diff --git a/src/phl/ecPhlEqobs.ml b/src/phl/ecPhlEqobs.ml
index 2cbf0416c..86095b460 100644
--- a/src/phl/ecPhlEqobs.ml
+++ b/src/phl/ecPhlEqobs.ml
@@ -281,6 +281,10 @@ and i_eqobs_in il ir sim local (eqo:Mpv2.t) =
 
 and s_eqobs_in_full sl sr sim local eqo =
   let r1,r2,sim, eqi = s_eqobs_in sl sr sim local eqo in
+  let ppe = EcPrinting.PPEnv.ofenv sim.sim_env in
+  Format.eprintf "Got r1: %a | r2: %a after sim@."
+  EcPrinting.(pp_stmt ppe) (stmt r1)
+  EcPrinting.(pp_stmt ppe) (stmt r2);
   if r1 <> [] || r2 <> [] then raise EqObsInError;
   sim, eqi
 
@@ -470,8 +474,13 @@ let process_eqobs_inS info tc =
     | Some(p1,p2) ->
       let p1 = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Left , p1) in
       let p2 = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Right, p2) in
+      (* Sim skips instructions pointed to FIXME *)
+      let p1 = EcMatching.Position.Notations.(p1 +> 1) in
+      let p2 = EcMatching.Position.Notations.(p2 +> 1) in
       let _,sl2 = s_split env p1 es.es_sl in
       let _,sr2 = s_split env p2 es.es_sr in
+      let ppe = EcPrinting.PPEnv.ofenv env in
+      Format.eprintf "SL2: %a@.SR2:%a@." EcPrinting.(pp_stmt ppe) (stmt sl2) EcPrinting.(pp_stmt ppe) (stmt sr2);
       let _, eqi =
         try s_eqobs_in_full (stmt sl2) (stmt sr2) sim Mpv2.empty_local eqo
         with EqObsInError -> tc_error !!tc "cannot apply sim" in
diff --git a/src/phl/ecPhlExists.ml b/src/phl/ecPhlExists.ml
index 90f017cbb..b86fa7ff8 100644
--- a/src/phl/ecPhlExists.ml
+++ b/src/phl/ecPhlExists.ml
@@ -160,19 +160,19 @@ let process_ecall oside (l, tvi, fs) tc =
     match kind, oside, p1 with
     | `Hoare n, _, Inv_ss p1 ->
         EcPhlSeq.t_hoare_seq
-          (Zpr.cpos (n-1)) p1 tc
+          (EcMatching.Position.cpos1 n) p1 tc
     | `Hoare n, _, Inv_hs p1 ->
         EcPhlSeq.t_hoare_seq
-          (Zpr.cpos (n-1)) (POE.lower p1) tc
+          (EcMatching.Position.cpos1 n) (POE.lower p1) tc
     | `Equiv (n1, n2), None, Inv_ts p1 ->
         EcPhlSeq.t_equiv_seq
-          (Zpr.cpos (n1-1), Zpr.cpos (n2-1)) p1 tc
+          (EcMatching.Position.cpos1 n1, EcMatching.Position.cpos1 n2) p1 tc
     | `Equiv (n1, n2), Some `Left, Inv_ts p1 ->
         EcPhlSeq.t_equiv_seq
-          (Zpr.cpos (n1-1), Zpr.cpos n2) p1 tc
+          (EcMatching.Position.cpos1 n1, EcMatching.Position.cpos1 (n2+1)) p1 tc
     | `Equiv(n1, n2), Some `Right, Inv_ts p1 ->
         EcPhlSeq.t_equiv_seq
-          (Zpr.cpos n1, Zpr.cpos (n2-1)) p1 tc
+          (EcMatching.Position.cpos1 (n1+1), EcMatching.Position.cpos1 n2) p1 tc
     | _ -> tc_error !!tc "mismatched sidedness or kind of conclusion"
   in
 
diff --git a/src/phl/ecPhlHiAuto.ml b/src/phl/ecPhlHiAuto.ml
index c5c23d645..204a92836 100644
--- a/src/phl/ecPhlHiAuto.ml
+++ b/src/phl/ecPhlHiAuto.ml
@@ -54,7 +54,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc =
   tc |> match lls with
 
   | LL_WP ->
-      EcPhlWp.t_wp (Some (Single (Zpr.cpos (-1))))
+      EcPhlWp.t_wp (Some (Single (EcMatching.Position.cpos1 (-1))))
 
   | LL_RND ->
       let m = EcIdent.create "&hr" in 
@@ -69,7 +69,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc =
   | LL_JUMP ->
       let m = EcIdent.create "&hr" in
         ( EcPhlSeq.t_bdhoare_seq
-           (Zpr.cpos (-1)) ({m;inv=f_true}, {m;inv=f_true}, 
+           (EcMatching.Position.cpos1 (-1)) ({m;inv=f_true}, {m;inv=f_true}, 
             {m;inv=f_r1}, {m;inv=f_r1}, {m;inv=f_r0}, {m;inv=f_r1})
 
         @~ FApi.t_onalli (function
@@ -87,7 +87,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc =
       in
 
         ( EcPhlSeq.t_bdhoare_seq
-           (Zpr.cpos (-1)) ({m;inv=f_true}, {m;inv=f_true}, {m;inv=f_r1}, {m;inv=f_r1}, {m;inv=f_r0}, {m;inv=f_r1})
+           (EcMatching.Position.cpos1 (-1)) ({m;inv=f_true}, {m;inv=f_true}, {m;inv=f_r1}, {m;inv=f_r1}, {m;inv=f_r0}, {m;inv=f_r1})
 
         @~ FApi.t_onalli (function
            | 1 -> t_id
@@ -142,8 +142,8 @@ let t_lossless tc =
 
   | FequivS hs ->
     let ml, mr = fst hs.es_ml, fst hs.es_mr in
-      ((EcPhlSeq.t_equiv_seq_onesided `Left (EcMatching.Zipper.cpos 0) {m=ml;inv=f_true} {m=ml;inv=f_true}) @+
-         [ (EcPhlSeq.t_equiv_seq_onesided `Right (EcMatching.Zipper.cpos 0) {m=mr;inv=f_true} {m=mr;inv=f_true}) @+
+      ((EcPhlSeq.t_equiv_seq_onesided `Left (EcMatching.Position.cpos1 0) {m=ml;inv=f_true} {m=ml;inv=f_true}) @+
+         [ (EcPhlSeq.t_equiv_seq_onesided `Right (EcMatching.Position.cpos1 0) {m=mr;inv=f_true} {m=mr;inv=f_true}) @+
              [ EcPhlSkip.t_skip @! t_trivial ;
                t_single
              ];
diff --git a/src/phl/ecPhlHiCond.ml b/src/phl/ecPhlHiCond.ml
index 5c0e6921d..23d33836e 100644
--- a/src/phl/ecPhlHiCond.ml
+++ b/src/phl/ecPhlHiCond.ml
@@ -9,7 +9,7 @@ open EcMatching.Position
 (* -------------------------------------------------------------------- *)
 let process_cond (info : EcParsetree.pcond_info) tc =
   let default_if (i : codepos1 option) s =
-    ofdfl (fun _ -> Zpr.cpos (tc1_pos_last_if tc s)) i in
+    ofdfl (fun _ -> cpos1 (tc1_pos_last_if tc s)) i in
 
   match info with
   | `Head side ->
diff --git a/src/phl/ecPhlInline.ml b/src/phl/ecPhlInline.ml
index 8dca495ff..6f4b8ad93 100644
--- a/src/phl/ecPhlInline.ml
+++ b/src/phl/ecPhlInline.ml
@@ -328,7 +328,7 @@ module HiInternal = struct
     match zip.Zp.z_tail with
     | { i_node = Scall _ } :: tl ->
          pat_of_spath ((zip.Zp.z_head, tl), zip.Zp.z_path)
-    | _ -> raise Zp.InvalidCPos
+    | _ -> raise EcMatching.Position.InvalidCPos
 end
 
 (* -------------------------------------------------------------------- *)
@@ -426,7 +426,7 @@ let process_inline_codepos ~use_tuple side pos tc =
 
     | _, _ -> tc_error !!tc "invalid arguments"
 
-  with EcMatching.Zipper.InvalidCPos ->
+  with EcMatching.Position.InvalidCPos ->
     tc_error !!tc "invalid position"
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml
index 60aa5e71a..68e895d8b 100644
--- a/src/phl/ecPhlLoopTx.ml
+++ b/src/phl/ecPhlLoopTx.ml
@@ -229,8 +229,7 @@ let process_unroll_for ~cfold side cpos tc =
     tc_error !!tc "cannot use deep code position";
 
   let cpos = EcLowPhlGoal.tc1_process_codepos tc (side, cpos) in
-  let z, cpos = Zpr.zipper_of_cpos_r env cpos c in
-  let pos  = 1 + List.length z.Zpr.z_head in
+  let z, ((_nm_path, pos), _) = Zpr.zipper_of_cpos_r env cpos c in
 
   (* Extract loop condition / body *)
   let t, wbody  =
@@ -297,7 +296,7 @@ let process_unroll_for ~cfold side cpos tc =
     match zs with
     | [] -> t_id tc
     | z :: zs ->
-      ((t_rcond side (zs <> []) (Zpr.cpos pos)) @+
+      ((t_rcond side (zs <> []) (EcMatching.Position.cpos1 pos)) @+
       [FApi.t_try (t_intro_i m) @!
        t_conseq (Inv_ss (map_ss_inv1 (fun x -> f_eq x (f_int z)) x)) @!
        t_set i pos z;
@@ -314,16 +313,18 @@ let process_unroll_for ~cfold side cpos tc =
     | _ -> tc_error !!tc "expecting single sided precondition" in
 
   let doi i tc =
+    let open EcMatching.Position in
+    let open Notations in
     if Array.length hds <= i then t_id tc else
     let (_h,pos,_z) = oget hds.(i) in
     if i = 0 then
-      (EcPhlWp.t_wp (Some (Single (Zpr.cpos (pos - 2)))) @!
+      (EcPhlWp.t_wp (Some (Single ((cpos1 pos) <+ 1))) @!
        t_conseq (Inv_ss {inv=f_true;m=x.m}) @! EcPhlTAuto.t_hoare_true) tc
     else
       let (h', pos', z') = oget hds.(i-1) in
       FApi.t_seqs [
-        EcPhlWp.t_wp (Some (Single (Zpr.cpos (pos-2))));
-        EcPhlSeq.t_hoare_seq (Zpr.cpos (pos' - 1)) (map_ss_inv2 f_eq x {m=goal_m;inv=f_int z'}) @+
+        EcPhlWp.t_wp (Some (Single ((cpos1 pos) <+ 1)));
+        EcPhlSeq.t_hoare_seq (cpos1 pos') (map_ss_inv2 f_eq x {m=goal_m;inv=f_int z'}) @+
         [t_apply_hd h'; t_conseq_nm] ] tc
   in
 
@@ -331,7 +332,7 @@ let process_unroll_for ~cfold side cpos tc =
   let tcenv = FApi.t_onalli doi tcenv in
 
   if cfold then begin
-    let cpos = EcMatching.Position.shift ~offset:(-1) cpos in
+    let cpos = EcMatching.Position.Notations.(cpos <+| 1) in
     let clen = blen * (List.length zs - 1) in
 
     FApi.t_last (EcPhlCodeTx.t_cfold side cpos (Some clen)) tcenv
diff --git a/src/phl/ecPhlOutline.ml b/src/phl/ecPhlOutline.ml
index 2898a138b..d0d65536b 100644
--- a/src/phl/ecPhlOutline.ml
+++ b/src/phl/ecPhlOutline.ml
@@ -59,7 +59,7 @@ let process_outline info tc =
   let ppe = EcPrinting.PPEnv.ofenv env in
 
   let range =
-    EcLowPhlGoal.tc1_process_codepos_range tc
+    EcLowPhlGoal.tc1_process_codepos_or_range tc
       (Some side, info.outline_range) in
 
   try
diff --git a/src/phl/ecPhlRewrite.ml b/src/phl/ecPhlRewrite.ml
index 07bc76cc7..11f7d5c05 100644
--- a/src/phl/ecPhlRewrite.ml
+++ b/src/phl/ecPhlRewrite.ml
@@ -239,7 +239,7 @@ let t_change_stmt
   let env = FApi.tc1_env 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 zpr, (_prelude,stmt, epilog), _nmr = 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
@@ -291,7 +291,7 @@ let t_change_stmt
 (* -------------------------------------------------------------------- *)
 let process_change_stmt
   (side   : side option)
-  (pos    : pcodepos_range)
+  (pos    : pcodepos_or_range)
   (s      : pstmt)
   (tc     : tcenv1)
 =
@@ -317,7 +317,7 @@ let process_change_stmt
 
   let pos =
     let env = EcEnv.Memory.push_active_ss me env in
-    EcTyping.trans_codepos_range ~memory:(fst me) env pos
+    EcTyping.trans_codepos_or_range ~memory:(fst me) env pos
   in
 
   let s = match side with
diff --git a/src/phl/ecPhlRewrite.mli b/src/phl/ecPhlRewrite.mli
index 100c4b6bb..bc2a23b6d 100644
--- a/src/phl/ecPhlRewrite.mli
+++ b/src/phl/ecPhlRewrite.mli
@@ -9,4 +9,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 -> pcodepos_range -> pstmt -> backward
+val process_change_stmt   : side option -> pcodepos_or_range -> pstmt -> backward
diff --git a/src/phl/ecPhlRwEquiv.ml b/src/phl/ecPhlRwEquiv.ml
index a568172e8..62ce176c8 100644
--- a/src/phl/ecPhlRwEquiv.ml
+++ b/src/phl/ecPhlRwEquiv.ml
@@ -153,6 +153,7 @@ let process_rewrite_equiv info tc =
 
   (* Offload to the tactic *)
   try
+    (* FIXME: cp should be translated to codepos in process *)
     t_rewrite_equiv side dir cp equiv eqv_pt rargslv tc
   with
   | RwEquivError (RWE_InvalidFunction (got, wanted)) ->
diff --git a/src/phl/ecPhlSeq.ml b/src/phl/ecPhlSeq.ml
index 35d47899d..6132608e8 100644
--- a/src/phl/ecPhlSeq.ml
+++ b/src/phl/ecPhlSeq.ml
@@ -19,6 +19,9 @@ let t_hoare_seq_r i phi tc =
   let hs = tc1_as_hoareS tc in
   let phi = ss_inv_rebind phi (fst hs.hs_m) in
   let s1, s2 = s_split env i hs.hs_s in
+  let ppe = EcPrinting.PPEnv.ofenv env in
+  Format.eprintf "Splitting at index (%a)@." EcPrinting.(pp_codepos1 ppe) i;
+  Format.eprintf "%a@.---------------------------------------@.%a@." EcPrinting.(pp_stmt ppe) (stmt s1) EcPrinting.(pp_stmt ppe) (stmt s2);
   let post = update_hs_ss phi (hs_po hs) in
   let a = f_hoareS (snd hs.hs_m) (hs_pr hs) (stmt s1) post in
   let b = f_hoareS (snd hs.hs_m) phi (stmt s2) (hs_po hs)  in
@@ -146,8 +149,8 @@ let t_equiv_seq_onesided side i pre post tc =
   let generalize_mod_side= sideif side generalize_mod_left generalize_mod_right in
   let ij =
     match side with
-    | `Left  -> (i, Zpr.cpos (List.length s'. s_node))
-    | `Right -> (Zpr.cpos (List.length s'. s_node), i) in
+    | `Left  -> (i, EcMatching.Position.cpos1 (List.length s'. s_node))
+    | `Right -> (EcMatching.Position.cpos1 (List.length s'. s_node), i) in
   let _s1, s2 = s_split env i s in
 
   let modi = EcPV.s_write env (EcModules.stmt s2) in
@@ -216,6 +219,11 @@ let process_phl_bd_info bd_info tc =
 let process_seq ((side, k, phi, bd_info) : seq_info) (tc : tcenv1) =
   let concl = FApi.tc1_goal tc in
 
+  (* Seq is 0-indexed from user side, so convert *)
+  let k = DOption.map (fun cp ->
+    shift1 ~offset:1 cp
+  ) k in
+
   let get_single phi =
     match phi with
     | Single phi -> phi
diff --git a/src/phl/ecPhlSwap.ml b/src/phl/ecPhlSwap.ml
index eacee93b2..0ff1fcd02 100644
--- a/src/phl/ecPhlSwap.ml
+++ b/src/phl/ecPhlSwap.ml
@@ -9,10 +9,11 @@ open EcPV
 open EcMatching.Position
 open EcCoreGoal
 open EcLowGoal
+open EcMatching
 
 (* -------------------------------------------------------------------- *)
 type swap_kind = {
-  interval : (codepos1 * codepos1 option) option;
+  interval : codepos_range;
   offset   : codeoffset1;
 }
 
@@ -62,94 +63,43 @@ module LowInternal = struct
       if not (PV.is_empty m1m2) then error `WW m1m2;
       if not (PV.is_empty m1r2) then error `WR m1r2
 
+
   let swap_stmt
     (pf   : proofenv   )
     (env  : EcEnv.env  )
     (info : swap_kind  )
     (s    : stmt       )
   =
-    let len = List.length s.s_node in
-
-    let p1, p2 (* inclusive *)=
-      match info.interval with
-      | Some (p , None   ) -> p , p
-      | Some (p1, Some p2) -> p1, p2
-      | None ->
-        let p =
-          match info.offset with
-          | `ByOffset offset when offset < 0 -> `ByPos (-1)
-          | _ -> `ByPos 1 in
-        let p : codepos1 = (0, p) in (p, p)
-    in
-
-    let process_cpos (p : codepos1) =
-      try  EcMatching.Zipper.offset_of_position env p s
-      with EcMatching.Zipper.InvalidCPos ->
-        tc_error_lazy pf (fun fmt ->
-          let ppe = EcPrinting.PPEnv.ofenv env in
-          Format.fprintf fmt "invalid position: %a" (EcPrinting.pp_codepos1 ppe) p
-        ) in
-
-    let i1 = process_cpos p1 in
-    let i2 = process_cpos p2 in
-
-    if i2 < i1 then
+    let (env, s), (_, (start, fin)) = try 
+      normalize_cpos_range env info.interval s 
+    with InvalidCPos ->
       tc_error_lazy pf (fun fmt ->
         let ppe = EcPrinting.PPEnv.ofenv env in
-        Format.fprintf fmt
-          "invalid/empty code block: [%a..%a] (resolved as [%d..%d])"
-          (EcPrinting.pp_codepos1 ppe) p1
-          (EcPrinting.pp_codepos1 ppe) p2
-          i1 i2
-      );
-
-    let offset =
-      match info.offset with
-      | `ByPosition p ->
-        let target = EcMatching.Zipper.offset_of_position env p s in
-        if i1 < target && target <= i2 then
-          tc_error_lazy pf (fun fmt ->
-            let ppe = EcPrinting.PPEnv.ofenv env in
-            Format.fprintf fmt
-              "destination is inside the moved block: %a \\in ]%a..%a] (resolved as %d \\in ]%d..%d])"
-              (EcPrinting.pp_codeoffset1 ppe) info.offset
-              (EcPrinting.pp_codepos1 ppe) p1
-              (EcPrinting.pp_codepos1 ppe) p2
-              target i1 i2
-          );
-        if target <= i1 then target - i1 else target - i2 - 1
-
-      | `ByOffset o ->
-        o
+        Format.fprintf fmt "invalid range: %a" (EcPrinting.pp_codepos_range ppe) info.interval
+      )
     in
 
-    let target = if 0 <= offset then i2+offset+1 else i1+offset in
-
-    if target <= 0 then
+    let target = try 
+      resolve_offset1_from_cpos1_range env (start, fin) info.offset s 
+    with InvalidCPos ->
       tc_error_lazy pf (fun fmt ->
         let ppe = EcPrinting.PPEnv.ofenv env in
-        Format.fprintf fmt
-          "offset (%d) is too small by %d: start index is %a (resolved to %d)"
-          offset (1 + abs target) (EcPrinting.pp_codepos1 ppe) p1 i1
-      );
-
-    if target > len+1 then
-      tc_error_lazy pf (fun fmt ->
-        let ppe = EcPrinting.PPEnv.ofenv env in
-        Format.fprintf fmt
-          "offset (%d) is too larget by %d: end index is %a (resolved to %d)"
-          offset (target - len - 1) (EcPrinting.pp_codepos1 ppe) p2 i2
-      );
-
-    let b1, b2, b3 =
-      if target <= i1 then target, i1, i2+1 else i1, i2+1, target in
-
-    let hd , tl = List.takedrop (b1-1 ) s.s_node in
-    let s12, tl = List.takedrop (b2-b1) tl in
-    let s23, tl = List.takedrop (b3-b2) tl in
+        Format.fprintf fmt "invalid offset for swap: %a" (EcPrinting.pp_codeoffset1 ppe) info.offset)
+    in
 
-    check_swap pf env (stmt s12) (stmt s23);
-    stmt (List.flatten [hd; s23; s12; tl])
+    Format.eprintf "Swapping: (start %d, end %d, target %d)@." start fin target;
+
+    match split_by_nmcpr1s 
+      (if target <= start 
+      then [target; start; fin]
+      else 
+        let (_, target) = nm_codepos1_range_of_nm_codepos1 target in
+        [start; fin; target]
+      ) s
+    with 
+    | [hd; s1; s2; tl] -> check_swap pf env (stmt s1) (stmt s2);
+      stmt (List.flatten [hd; s2; s1; tl])
+    | _ -> assert false
 end
 
 (* -------------------------------------------------------------------- *)
@@ -173,26 +123,25 @@ let rec process_swap1 (info : (oside * pswap_kind) located) (tc : tcenv1) =
       (process_swap1 { info with pl_desc = (Some `Right, pos)})
       tc
   else
-    let env = FApi.tc1_env tc in
     let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
-
-    let process_codepos =
-      let env = EcEnv.Memory.push_active_ss me env in
-      fun p -> EcTyping.trans_codepos1 env p in
-
-    let process_codeoffset (o : pcodeoffset1) : codeoffset1 =
-        match o with
-        | `ByOffset   i -> `ByOffset i
-        | `ByPosition p -> `ByPosition (process_codepos p) in
+    let env = EcEnv.Memory.push_active_ss me (FApi.tc1_env tc) in
 
     let interval =
-      Option.map (fun (p1, p2) ->
-        let p1 = process_codepos p1 in
-        let p2 = Option.map process_codepos p2 in
-        (p1, p2)
+      Option.map (fun pcpor ->
+        EcTyping.trans_codepos_or_range ~memory:(fst me) env pcpor
       ) pos.interval in
 
-    let offset = process_codeoffset pos.offset in
+    let offset = EcTyping.trans_codeoffset1 ~memory:(fst me) env pos.offset in
+
+    let interval = match interval, offset with
+    | Some interval, _ -> interval
+    | None, `Relative i -> 
+        codepos_range_of_codepos
+        (if i > 0 then cpos_first else cpos_last)
+    | None, _ -> 
+      tc_error (!!tc) "Cannot give a absolute offset and no range"
+    in
+      
 
     let kind : swap_kind = { interval; offset } in
 
@@ -204,6 +153,8 @@ let process_swap info tc =
 
 (* -------------------------------------------------------------------- *)
 let process_interleave info tc =
+  assert false 
+(*
   let loc = info.pl_loc in
   let (side, pos_n1, lpos2, k) = info.pl_desc in
 
@@ -230,3 +181,4 @@ let process_interleave info tc =
     FApi.t_seq (aux pos1 pos2 k) (aux_list (pos1, n1 + n2) lpos2) tc
 
   in aux_list pos_n1 lpos2 tc
+*)
diff --git a/src/phl/ecPhlSwap.mli b/src/phl/ecPhlSwap.mli
index 6b9c330d1..77a411fc7 100644
--- a/src/phl/ecPhlSwap.mli
+++ b/src/phl/ecPhlSwap.mli
@@ -6,7 +6,7 @@ open EcCoreGoal.FApi
 
 (* -------------------------------------------------------------------- *)
 type swap_kind = {
-  interval : (codepos1 * codepos1 option) option;
+  interval : codepos_range;
   offset   : codeoffset1;
 }
 
diff --git a/tests/fine-grained-module-defs.ec b/tests/fine-grained-module-defs.ec
index 848684c83..f373c93e6 100644
--- a/tests/fine-grained-module-defs.ec
+++ b/tests/fine-grained-module-defs.ec
@@ -32,7 +32,7 @@ end;
 module A_count (B : T) = A(B) with {
   var c : int
   proc f [1 + ^ { c <- c + 1;}]
-  proc g [[^x<- .. ^ <@] ~ { c <- c - 1;}] res ~ (x + 1)
+  proc g [:[^x<- .. ^ <@] ~ { c <- c - 1;}] res ~ (x + 1)
   proc h [^match - #Some.]
 }.
 
diff --git a/tests/outline.ec b/tests/outline.ec
index 3e06798c6..ec307d5e8 100644
--- a/tests/outline.ec
+++ b/tests/outline.ec
@@ -101,7 +101,7 @@ qed.
 
 equiv outline_slice: N.g4 ~ N.g4: true ==> true.
 proc.
-outline {1} [1 .. 2] M.f4.
+outline {1} :[1 .. 2] M.f4.
 by inline*; auto.
 qed.
 
@@ -115,7 +115,7 @@ equiv outline_multi: N.g6 ~ N.g6: true ==> true.
 proof.
 proc.
 outline {1} 2 ~ M.f5.
-outline {1} [3 .. 4] N.g4.
+outline {1} :[3 .. 4] N.g4.
 outline {1} 1 ~ M.f5.
 by inline*; auto.
 qed.
@@ -123,7 +123,7 @@ qed.
 equiv outline_stmt: N.g6 ~ N.g6: true ==> true.
 proof.
 proc.
-outline {1} [1 .. 4] by {
+outline {1} :[1 .. 4] by {
   a <@ M.f5(dint);
   b <@ M.f5(dint);
   N.g4(a,b);
diff --git a/tests/procchange.ec b/tests/procchange.ec
index 6863802f0..35b56d64c 100644
--- a/tests/procchange.ec
+++ b/tests/procchange.ec
@@ -14,7 +14,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] : { x <- 3; }.
     
     wp. skip. smt().
   abort.
@@ -30,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.
 
@@ -45,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.
@@ -65,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 {
@@ -88,7 +88,7 @@ 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 + 0;
     }
@@ -119,10 +119,10 @@ theory ProcChangeInWhileEquiv.
     x <- x + 0 + 1;
   }.
   wp; skip. smt().
-  proc change {1} [^while.1..^while.2] : {
+  proc change {1} ^while.:[1..2] : {
     x <- 2;
   }. wp; skip. smt().
-  proc change {2} [^while.1-1] : {
+  proc change {2} ^while.:[1-1] : {
     x <- 2;
   }. wp; skip. smt().
   abort.
@@ -140,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.