From c838148cfd5b2cbe27967a23a3f85a07c7df2643 Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Fri, 20 Mar 2026 18:30:57 +0000 Subject: [PATCH 01/12] WIP: refactoring code positions, interleave is assert false'd --- src/ecCorePrinting.ml | 12 +- src/ecLowPhlGoal.ml | 29 +- src/ecMatching.ml | 541 ++++++++++++++++++++++-------- src/ecMatching.mli | 137 ++++++-- src/ecParser.mly | 42 ++- src/ecParsetree.ml | 35 +- src/ecPrinting.ml | 38 ++- src/ecTyping.ml | 53 +-- src/ecTyping.mli | 1 + src/phl/ecPhlCall.ml | 4 +- src/phl/ecPhlCodeTx.ml | 6 +- src/phl/ecPhlCond.ml | 8 +- src/phl/ecPhlEager.ml | 15 +- src/phl/ecPhlEqobs.ml | 6 + src/phl/ecPhlExists.ml | 10 +- src/phl/ecPhlHiAuto.ml | 10 +- src/phl/ecPhlHiCond.ml | 2 +- src/phl/ecPhlInline.ml | 4 +- src/phl/ecPhlLoopTx.ml | 15 +- src/phl/ecPhlOutline.ml | 2 +- src/phl/ecPhlRewrite.ml | 6 +- src/phl/ecPhlRewrite.mli | 2 +- src/phl/ecPhlRwEquiv.ml | 1 + src/phl/ecPhlSeq.ml | 12 +- src/phl/ecPhlSwap.ml | 134 +++----- src/phl/ecPhlSwap.mli | 2 +- tests/fine-grained-module-defs.ec | 2 +- tests/outline.ec | 6 +- tests/procchange.ec | 30 +- 29 files changed, 779 insertions(+), 386 deletions(-) diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml index 5f3e239dc5..418ccb7d64 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 6daabbfd6d..571232ee7b 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 @@ -369,19 +376,19 @@ let logicS_read (env : env) (f : logicS) = 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 = @@ -727,14 +734,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 a14e8859b3..f69fd09eac 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,296 @@ 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) else nm + + let normalize_cpos1 (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 *) + 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 +546,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 +564,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 66c6bc2006..f0639e875b 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 : 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 d97f4ccb93..25f43c658f 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 877f370741..c58e521301 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 dff558c4db..78f8b2062d 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -2419,22 +2419,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 266b86dc87..49d9314f6f 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 6722b92b3e..1eee25195b 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 87a3bc727e..556f2b7cf2 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 a49af0d92f..1a938a6fd8 100644 --- a/src/phl/ecPhlCodeTx.ml +++ b/src/phl/ecPhlCodeTx.ml @@ -422,9 +422,9 @@ let t_cfold (olen : int option) (tc : tcenv1) = - let tr = fun side -> `Fold (side, cpos, olen) in - let cb = fun cenv _ me zpr -> cfold_stmt ~eager cenv me olen zpr in - t_code_transform side ~bdhoare:true cpos tr (t_zip cb) tc + let tr = fun side -> `Fold (side, cpos, olen) in + let cb = fun cenv _ me zpr -> cfold_stmt ~eager cenv me olen zpr in + t_code_transform side ~bdhoare:true cpos tr (t_zip cb) tc (* -------------------------------------------------------------------- *) 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 69d5c42104..a3dade6a85 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 800de9b7d4..780347f428 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 2cbf0416c8..fd11f0346a 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 @@ -472,6 +476,8 @@ let process_eqobs_inS info tc = let p2 = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Right, p2) 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 90f017cbb1..b86fa7ff87 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 c5c23d6456..204a928368 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 5c0e6921d8..23d33836e3 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 8dca495ffe..6f4b8ad938 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 cbe4027de1..96a9b37cc5 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 ~eager:false side cpos (Some clen)) tcenv diff --git a/src/phl/ecPhlOutline.ml b/src/phl/ecPhlOutline.ml index 2898a138b5..d0d65536bb 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 331d1c9477..3ffc034336 100644 --- a/src/phl/ecPhlRewrite.ml +++ b/src/phl/ecPhlRewrite.ml @@ -278,7 +278,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) = + let zpr, (_prelude,stmt, epilog), _nmr = EcMatching.Zipper.zipper_and_split_of_cpos_range env pos stmt in (* Collect the variables that may be modified by the surrounding context, @@ -358,7 +358,7 @@ let t_change_stmt (* -------------------------------------------------------------------- *) let process_change_stmt (side : side option) - (pos : pcodepos_range) + (pos : pcodepos_or_range) (s : pstmt) (tc : tcenv1) = @@ -384,7 +384,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 100c4b6bb9..bc2a23b6d5 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 a568172e85..62ce176c82 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 35d47899d5..6132608e89 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 eacee93b2d..0ff1fcd02d 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 6b9c330d11..77a411fc78 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 848684c83c..f373c93e6d 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 3e06798c63..ec307d5e89 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 25eb8f40aa..1654c81445 100644 --- a/tests/procchange.ec +++ b/tests/procchange.ec @@ -30,7 +30,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. @@ -47,7 +47,7 @@ theory ProcChangeAssignHoare. 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 ProcChangeAssignHoare. @@ -64,7 +64,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. @@ -86,7 +86,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 { @@ -111,7 +111,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; } @@ -150,15 +150,31 @@ 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. end ProcChangeInWhileEquiv. +(* -------------------------------------------------------------------- *) +theory ProcChangeAssignHoare. + module M = { + proc f(x : int) = { + x <- x + 0; + } + }. + + lemma L : hoare[M.f: true ==> true]. + proof. + proc. + proc change :[1..1] : { x <- x; }. + wp; skip; smt(). + abort. +end ProcChangeAssignHoare. + (* -------------------------------------------------------------------- *) theory ProcChangeSampleHoare. module M = { From 2003b7dc68d8deaf7431009ea927d26473b4caf9 Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Fri, 20 Mar 2026 19:03:59 +0000 Subject: [PATCH 02/12] More fixes interleave still broken --- src/ecMatching.ml | 11 +++++++---- src/ecMatching.mli | 2 +- src/phl/ecPhlEqobs.ml | 3 +++ 3 files changed, 11 insertions(+), 5 deletions(-) diff --git a/src/ecMatching.ml b/src/ecMatching.ml index f69fd09eac..9657f80946 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -273,15 +273,18 @@ module Position = struct | `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) else nm + in + if check then check_nm_cpos1 nm s; + nm - let normalize_cpos1 (env: EcEnv.env) ((off, cb): codepos1) (s: stmt) : nm_codepos1 = + 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 *) - check_nm_cpos1 nm s; nm + 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 @@ -341,7 +344,7 @@ module Position = struct 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 + 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 = diff --git a/src/ecMatching.mli b/src/ecMatching.mli index f0639e875b..c9d90d4896 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -103,7 +103,7 @@ module Position : sig val normalize_cp_base : ?check:bool -> env -> cp_base -> stmt -> nm_codepos1 - val normalize_cpos1 : env -> codepos1 -> 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 diff --git a/src/phl/ecPhlEqobs.ml b/src/phl/ecPhlEqobs.ml index fd11f0346a..86095b4605 100644 --- a/src/phl/ecPhlEqobs.ml +++ b/src/phl/ecPhlEqobs.ml @@ -474,6 +474,9 @@ 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 From e67a6a71bd171e56f1ad801bd04c7a42ccb505e1 Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Mon, 23 Mar 2026 12:49:24 +0000 Subject: [PATCH 03/12] 4 checks failing, interleave broken --- src/ecParser.mly | 6 ++++-- src/phl/ecPhlCall.ml | 8 ++++---- src/phl/ecPhlFel.ml | 2 ++ src/phl/ecPhlHiAuto.ml | 10 +++++----- src/phl/ecPhlRnd.ml | 10 +++++++++- src/phl/ecPhlSeq.ml | 6 +++--- src/phl/ecPhlSp.ml | 5 +++++ src/phl/ecPhlSwap.ml | 1 + src/phl/ecPhlWp.ml | 16 ++++++++++++---- 9 files changed, 45 insertions(+), 19 deletions(-) diff --git a/src/ecParser.mly b/src/ecParser.mly index 25f43c658f..bfc73baf49 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -2587,8 +2587,10 @@ codepos: { (path, i) } codepos_range: -| path=codepos_path COLON i=codepos1_range - { (path, i) } +| r=codepos1_range + { ([], r) } +| path=rlist1(codepos_step, empty) COLON r=codepos1_range + { (path, r) } codepos_or_range: | cp=codepos { Pos cp } diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml index 556f2b7cf2..64e72894a4 100644 --- a/src/phl/ecPhlCall.ml +++ b/src/phl/ecPhlCall.ml @@ -158,16 +158,16 @@ 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 _, _, _, _, _, wppre, _ = ehoare_call_pre_post fpre fpost tc in let tcenv = - EcPhlSeq.t_ehoare_seq (EcMatching.Position.cpos1 (List.length s.s_node)) wppre tc in + EcPhlSeq.t_ehoare_seq (EcMatching.Position.cpos1_after_last) 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 _, _, _, _, _, wppre, wppost = ehoare_call_pre_post fpre fpost tc in let tcenv = - EcPhlSeq.t_ehoare_seq (EcMatching.Position.cpos1 (List.length s.s_node)) + EcPhlSeq.t_ehoare_seq (EcMatching.Position.cpos1_after_last) (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/ecPhlFel.ml b/src/phl/ecPhlFel.ml index b3cbef12c7..fd3d163205 100644 --- a/src/phl/ecPhlFel.ml +++ b/src/phl/ecPhlFel.ml @@ -115,6 +115,8 @@ let callable_oracles_stmt env modv = let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc = let env, _, concl = FApi.tc1_eflat tc in + let at_pos = EcMatching.Position.Notations.(at_pos +> 1) in + let (pr, bd) = match concl.f_node with | Fapp ({ f_node =Fop (op, _) }, [pr; bd]) diff --git a/src/phl/ecPhlHiAuto.ml b/src/phl/ecPhlHiAuto.ml index 204a928368..aaf9ec0e73 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 (EcMatching.Position.cpos1 (-1)))) + EcPhlWp.t_wp (Some (Single (EcMatching.Position.cpos1_last))) | 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 - (EcMatching.Position.cpos1 (-1)) ({m;inv=f_true}, {m;inv=f_true}, + (EcMatching.Position.cpos1_last) ({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 - (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}) + (EcMatching.Position.cpos1_last) ({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.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}) @+ + ((EcPhlSeq.t_equiv_seq_onesided `Left (EcMatching.Position.cpos1_first) {m=ml;inv=f_true} {m=ml;inv=f_true}) @+ + [ (EcPhlSeq.t_equiv_seq_onesided `Right (EcMatching.Position.cpos1_first) {m=mr;inv=f_true} {m=mr;inv=f_true}) @+ [ EcPhlSkip.t_skip @! t_trivial ; t_single ]; diff --git a/src/phl/ecPhlRnd.ml b/src/phl/ecPhlRnd.ml index 2f6008da42..a1462ef611 100644 --- a/src/phl/ecPhlRnd.ml +++ b/src/phl/ecPhlRnd.ml @@ -646,9 +646,14 @@ let t_equiv_rnd ?pos side bij_info = (FApi.t_low3 "equiv-rnd" t_equiv_rnd_r) side pos bij_info (* -------------------------------------------------------------------- *) -let process_rnd side pos tac_info tc = +let process_rnd (side: side option) (pos: (bool * pcodepos1) doption option) tac_info tc = let concl = FApi.tc1_goal tc in + (* Rnd takes 0-indexed positions from user side *) + let pos = Option.map (DOption.map (fun (b, cp) -> + (b, EcParsetree.shift1 ~offset:1 cp) + )) pos in + match side, pos, tac_info with | None, None, PNoRndParams when is_hoareS concl -> t_hoare_rnd tc @@ -719,6 +724,9 @@ let process_rndsem ~reduce side pos tc = let concl = FApi.tc1_goal tc in let pos = EcLowPhlGoal.tc1_process_codepos1 tc (side, pos) in + (* Rndsem takes 0-indexed positions *) + let pos = EcMatching.Position.Notations.(pos +> 1) in + match side with | None when is_hoareS concl -> t_hoare_rndsem reduce pos tc diff --git a/src/phl/ecPhlSeq.ml b/src/phl/ecPhlSeq.ml index 6132608e89..b0109f4ac5 100644 --- a/src/phl/ecPhlSeq.ml +++ b/src/phl/ecPhlSeq.ml @@ -135,7 +135,7 @@ let t_equiv_seq_onesided side i pre post tc = let env = FApi.tc1_env tc in let es = tc1_as_equivS tc in let (ml, mr) = fst es.es_ml, fst es.es_mr in - let s, s', p', q' = + let s, _s', p', q' = match side with | `Left -> let p' = ss_inv_generalize_as_left pre ml mr in @@ -149,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, EcMatching.Position.cpos1 (List.length s'. s_node)) - | `Right -> (EcMatching.Position.cpos1 (List.length s'. s_node), i) in + | `Left -> (i, EcMatching.Position.cpos1_after_last ) + | `Right -> (EcMatching.Position.cpos1_after_last, i) in let _s1, s2 = s_split env i s in let modi = EcPV.s_write env (EcModules.stmt s2) in diff --git a/src/phl/ecPhlSp.ml b/src/phl/ecPhlSp.ml index 564495bfdd..4675f081de 100644 --- a/src/phl/ecPhlSp.ml +++ b/src/phl/ecPhlSp.ml @@ -304,4 +304,9 @@ let t_sp = FApi.t_low1 "sp" t_sp_side let process_sp (cpos : pcodepos1 doption option) (tc : tcenv1) = let env = FApi.tc1_env tc in let cpos = Option.map (EcTyping.trans_dcodepos1 env) cpos in + let cpos = + Option.map (DOption.map (fun cp -> + EcMatching.Position.Notations.(cp +> 1) + )) cpos + in t_sp cpos tc diff --git a/src/phl/ecPhlSwap.ml b/src/phl/ecPhlSwap.ml index 0ff1fcd02d..8469af97f4 100644 --- a/src/phl/ecPhlSwap.ml +++ b/src/phl/ecPhlSwap.ml @@ -80,6 +80,7 @@ module LowInternal = struct in let target = try + Format.eprintf "Start: %d | End: %d@." start fin ; resolve_offset1_from_cpos1_range env (start, fin) info.offset s with InvalidCPos -> tc_error_lazy pf (fun fmt -> diff --git a/src/phl/ecPhlWp.ml b/src/phl/ecPhlWp.ml index 535d936210..f414444fe6 100644 --- a/src/phl/ecPhlWp.ml +++ b/src/phl/ecPhlWp.ml @@ -1,5 +1,6 @@ (* -------------------------------------------------------------------- *) open EcUtils +open EcParsetree open EcPath open EcAst open EcModules @@ -253,7 +254,14 @@ let t_wp_r ?(uselet=true) k g = let t_wp ?(uselet=true) = FApi.t_low1 "wp" (t_wp_r ~uselet) (* -------------------------------------------------------------------- *) -let process_wp pos tc = - let pos = - Option.map (EcTyping.trans_dcodepos1 (FApi.tc1_env tc)) pos - in t_wp pos tc +let process_wp (cpos : pcodepos1 doption option) tc = + let env = (FApi.tc1_env tc) in + let cpos = + Option.map (EcTyping.trans_dcodepos1 env) cpos + in + let cpos = + Option.map (DOption.map (fun cp -> + EcMatching.Position.Notations.(cp +> 1) + )) cpos + in + t_wp cpos tc From 5e5ac292e369a515a49d32c26d314e3aa73a5129 Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Mon, 23 Mar 2026 20:22:08 +0000 Subject: [PATCH 04/12] Stdlib and unit tests passing --- src/ecMatching.ml | 30 +++++++++++++++++++++--------- src/ecMatching.mli | 8 ++++++-- src/ecParser.mly | 7 ++++++- src/phl/ecPhlEager.ml | 2 +- src/phl/ecPhlSwap.ml | 17 ++++++++--------- tests/fine-grained-module-defs.ec | 2 +- tests/outline.ec | 6 +++--- tests/procchange.ec | 26 +++++--------------------- 8 files changed, 51 insertions(+), 47 deletions(-) diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 9657f80946..f2e12a0e4f 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -171,6 +171,14 @@ module Position = struct let nm_codepos_in_nm_codepos_range (cp: nm_codepos1) ((start, fin): nm_codepos1_range) : bool = (start <= cp && cp < fin) + let cp1_point_at_instr (cp: codepos1) : codepos1 = + match snd cp with + | `ByPos j when j < 0 -> (fst cp, `ByPos (j-1)) + | _ -> cp + + let cp_point_at_instr ((cpath, cp1): codepos) : codepos = + (cpath, cp1_point_at_instr cp1) + module Notations = struct let (|+>) (cp: codepos) (offset: int) = shift ~offset cp @@ -266,6 +274,8 @@ module Position = struct Convert to 1-indexed again: i |-> i + 1 Obtaining final expression (len(s) - (i - 1)) + 1 = len(s) - i + 2 *) + (* FIXME: disallows pos after last when using negative codepos *) + | `ByPos i when i < 0 -> (List.length s.s_node) + i + 1 | `ByPos i when i < 0 -> (List.length s.s_node) + i + 2 (* i = 0 /\ check => Failure *) | `ByPos _ when check -> raise InvalidCPos; @@ -278,7 +288,6 @@ module Position = struct 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 @@ -286,8 +295,12 @@ module Position = struct if check then check_nm_cpos1 nm s; nm + let find_and_normalize_cpos1 ?(rev = true) (env : EcEnv.env) (cp1 : codepos1) (s : stmt) = + let nm = normalize_cpos1 env cp1 s in + find_by_nmcpos1 ~rev 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 + find_and_normalize_cpos1 ~rev env cp1 s |> fst (* Selects the index for match arm *) let select_match_arm_idx (env:env) (e: expr) (sel: string) = @@ -319,10 +332,9 @@ module Position = struct (* 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 (_, i, _), nm_cp1 = find_and_normalize_cpos1 env cp1 s in let (env, s), nmbr = normalize_brsel env i brsel in - (env, s), (cp1, nmbr) + (env, s), (nm_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 @@ -347,15 +359,15 @@ module Position = struct 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 normalize_cpos1_range 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; + if 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 normalize_cpos_range 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 + let nm1r = normalize_cpos1_range env cp1r s in (env, s), (npath, nm1r) (* diff --git a/src/ecMatching.mli b/src/ecMatching.mli index c9d90d4896..aad6134b58 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -72,6 +72,10 @@ module Position : sig val shift1 : offset:int -> codepos1 -> codepos1 val shift : offset:int -> codepos -> codepos + (* FIXME: maybe remove? *) + val cp1_point_at_instr : codepos1 -> codepos1 + val cp_point_at_instr : codepos -> codepos + val resolve_offset : base:codepos1 -> offset:codeoffset1 -> codepos1 val codepos1_range_of_codepos1 : codepos1 -> codepos1_range @@ -123,9 +127,9 @@ module Position : sig 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_cpos1_range : env -> codepos1_range -> stmt -> nm_codepos1_range - val normalize_cpos_range : ?strict:bool -> env -> codepos_range -> stmt -> (env * stmt) * nm_codepos_range + val normalize_cpos_range : env -> codepos_range -> stmt -> (env * stmt) * nm_codepos_range val split_at_nmcpos1 : ?rev:bool -> nm_codepos1 -> stmt -> instr list * instr list diff --git a/src/ecParser.mly b/src/ecParser.mly index bfc73baf49..725378a6f5 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -2577,7 +2577,12 @@ codeoffset1: (* 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) } +| LBRACKET cps=codepos1 MINUS cpe=loc(sword) RBRACKET { + if (unloc cpe) > 0 then + (cps, `Relative ((unloc cpe) + 1)) + else + parse_error (loc cpe) (Some "cannot give negative offset for codepos range end") +} %inline codepos_path: | path=rlist0(codepos_step, empty) { path } diff --git a/src/phl/ecPhlEager.ml b/src/phl/ecPhlEager.ml index 780347f428..b868e5d3b1 100644 --- a/src/phl/ecPhlEager.ml +++ b/src/phl/ecPhlEager.ml @@ -73,7 +73,7 @@ let destruct_eager tc s = let c, c' = (es.es_sl, es.es_sr) 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 + and c', z' = s_split env EcMatching.Position.Notations.(cpos1_after_last <+ ss) c' in Format.eprintf "z: %a@. z': %a@." EcPrinting.(pp_stmt ppe) (stmt z) EcPrinting.(pp_stmt ppe) (stmt z'); diff --git a/src/phl/ecPhlSwap.ml b/src/phl/ecPhlSwap.ml index 8469af97f4..ef90639e2f 100644 --- a/src/phl/ecPhlSwap.ml +++ b/src/phl/ecPhlSwap.ml @@ -9,7 +9,6 @@ open EcPV open EcMatching.Position open EcCoreGoal open EcLowGoal -open EcMatching (* -------------------------------------------------------------------- *) type swap_kind = { @@ -71,7 +70,8 @@ module LowInternal = struct (s : stmt ) = let (env, s), (_, (start, fin)) = try - normalize_cpos_range env info.interval s + let (cpath, (start, fin)) = info.interval in + normalize_cpos_range env (cpath, (start, fin)) s with InvalidCPos -> tc_error_lazy pf (fun fmt -> let ppe = EcPrinting.PPEnv.ofenv env in @@ -80,7 +80,7 @@ module LowInternal = struct in let target = try - Format.eprintf "Start: %d | End: %d@." start fin ; + Format.eprintf "Start: %d | End: %d | Len: %d@." start fin (List.length s.s_node); resolve_offset1_from_cpos1_range env (start, fin) info.offset s with InvalidCPos -> tc_error_lazy pf (fun fmt -> @@ -154,8 +154,6 @@ 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 @@ -167,13 +165,15 @@ let process_interleave info tc = "invalide interleave range (%i + %i * %i <= %i)" pos1 k n1 pos2; + (* FIXME: should use t_swap and not process_swap *) let rec aux pos1 pos2 k tc = if k <= 0 then t_id tc else let data : pswap_kind = + (* Represent range [pos2, pos2+n2[ *) let p1 = (0, `ByPos pos2) in - let p2 = (0, `ByPos (pos2+n2-1)) in - let o = `ByOffset ((pos1+n1) - pos2) in - { interval = Some (p1, Some p2); offset = o; } in + let p2 = (0, `ByPos (pos2+n2)) in + let o = `Relative ((pos1+n1) - pos2) in + { interval = Some (Range ([], (p1, `Absolute p2))); offset = o; } in FApi.t_seq (process_swap1 (mk_loc loc (side, data))) (aux (pos1+n1+n2) (pos2+n2) (k-1)) @@ -182,4 +182,3 @@ 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/tests/fine-grained-module-defs.ec b/tests/fine-grained-module-defs.ec index f373c93e6d..848684c83c 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 ec307d5e89..3e06798c63 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 1654c81445..19c9b4beb0 100644 --- a/tests/procchange.ec +++ b/tests/procchange.ec @@ -30,7 +30,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. @@ -47,7 +47,7 @@ theory ProcChangeAssignHoare. 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 ProcChangeAssignHoare. @@ -64,7 +64,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. @@ -86,7 +86,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 { @@ -111,7 +111,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; } @@ -159,22 +159,6 @@ theory ProcChangeInWhileEquiv. abort. end ProcChangeInWhileEquiv. -(* -------------------------------------------------------------------- *) -theory ProcChangeAssignHoare. - module M = { - proc f(x : int) = { - x <- x + 0; - } - }. - - lemma L : hoare[M.f: true ==> true]. - proof. - proc. - proc change :[1..1] : { x <- x; }. - wp; skip; smt(). - abort. -end ProcChangeAssignHoare. - (* -------------------------------------------------------------------- *) theory ProcChangeSampleHoare. module M = { From db02b072bfdf0512a0de1f9cfc90599d5ccafa1d Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Wed, 25 Mar 2026 11:36:43 +0000 Subject: [PATCH 05/12] Added code gaps, unit + stdlib checking --- src/ecCorePrinting.ml | 2 + src/ecLowPhlGoal.ml | 29 ++++ src/ecMatching.ml | 317 +++++++++++++++++++++++++++++----------- src/ecMatching.mli | 87 ++++++++++- src/ecParser.mly | 85 +++++++---- src/ecParsetree.ml | 43 ++++-- src/ecPrinting.ml | 12 +- src/ecTyping.ml | 25 ++++ src/ecTyping.mli | 6 + src/phl/ecPhlCall.ml | 4 +- src/phl/ecPhlCond.ml | 8 +- src/phl/ecPhlEager.ml | 8 +- src/phl/ecPhlEqobs.ml | 18 +-- src/phl/ecPhlExists.ml | 11 +- src/phl/ecPhlFel.ml | 8 +- src/phl/ecPhlFel.mli | 4 +- src/phl/ecPhlHiAuto.ml | 11 +- src/phl/ecPhlHiCond.ml | 10 +- src/phl/ecPhlLoopTx.ml | 40 ++++- src/phl/ecPhlRnd.ml | 8 - src/phl/ecPhlRwEquiv.ml | 2 +- src/phl/ecPhlSeq.ml | 42 +++--- src/phl/ecPhlSeq.mli | 10 +- src/phl/ecPhlSp.ml | 19 +-- src/phl/ecPhlSp.mli | 4 +- src/phl/ecPhlSwap.ml | 31 ++-- src/phl/ecPhlSwap.mli | 2 +- src/phl/ecPhlWhile.ml | 4 +- src/phl/ecPhlWp.ml | 32 ++-- src/phl/ecPhlWp.mli | 4 +- 30 files changed, 617 insertions(+), 269 deletions(-) diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml index 418ccb7d64..0b6fbc8198 100644 --- a/src/ecCorePrinting.ml +++ b/src/ecCorePrinting.ml @@ -76,6 +76,8 @@ module type PrinterAPI = sig val pp_codepos : PPEnv.t -> EcMatching.Position.codepos pp val pp_codepos_range : PPEnv.t -> EcMatching.Position.codepos_range pp + val pp_codegap1 : PPEnv.t -> EcMatching.Position.codegap1 pp + val pp_codegap : PPEnv.t -> EcMatching.Position.codegap pp (* ------------------------------------------------------------------ *) type vsubst = [ diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index 571232ee7b..369897d01f 100644 --- a/src/ecLowPhlGoal.ml +++ b/src/ecLowPhlGoal.ml @@ -390,6 +390,35 @@ let o_split ?rev env i s = try Pos.may_split_at_cpos1 ?rev env i s with Pos.InvalidCPos -> raise (InvalidSplit (oget i)) +(* Gap-based split functions *) +let s_split_at_gap env (g : codegap1) s = + let module Pos = EcMatching.Position in + try Pos.split_at_cgap1 env g s + with Pos.InvalidCPos -> + let cp = match g with GapBefore cp | GapAfter cp -> cp in + raise (InvalidSplit cp) + +let o_split_at_gap ?rev env (g : codegap1 option) s = + let module Pos = EcMatching.Position in + try Pos.may_split_at_cgap1 ?rev env g s + with Pos.InvalidCPos -> + let cp = match oget g with GapBefore cp | GapAfter cp -> cp in + raise (InvalidSplit cp) + +(* -------------------------------------------------------------------- *) +(* Gap processing functions *) +let tc1_process_codegap1 tc (side, g) = + 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_codegap1 env g + +let tc1_process_codegap tc (side, g) = + 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_codegap env g + (* -------------------------------------------------------------------- *) let t_hS_or_bhS_or_eS ?th ?teh ?tbh ?te tc = match (FApi.tc1_goal tc).f_node with diff --git a/src/ecMatching.ml b/src/ecMatching.ml index f2e12a0e4f..034ca67d15 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -34,37 +34,37 @@ module Position = struct 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? + (* Code positions and code gaps: + + A block of n instructions has: + - n positions (0-indexed), each pointing AT an instruction + - n+1 gaps (0-indexed), each pointing BETWEEN instructions + + gap 0 | instr 0 | gap 1 | instr 1 | gap 2 | ... | instr n-1 | gap n + + Positions (nm_codepos1): 0-indexed, range [0, n-1] + Gaps (nm_codegap1): 0-indexed, range [0, n] + gap k = before instruction k (= after instruction k-1) + gap 0 = start of block, gap n = end of block + + Conversions: + gap_before(pos) = pos (* gap immediately before instruction pos *) + gap_after(pos) = pos + 1 (* gap immediately after instruction pos *) + instr_after(gap) = gap (* instruction immediately after gap; requires gap < n *) + instr_before(gap) = gap - 1 (* instruction immediately before gap; requires gap > 0 *) + + Ranges are pairs of gaps (g1, g2) containing instructions g1, g1+1, ..., g2-1. + User writes [a..b] (1-indexed, closed-closed), which translates to + gap pair (a-1, b) in 0-indexed representation. - 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 + Tactics that split code take gaps (seq, wp, sp, fel, sim/eqobs). + Tactics that target instructions take positions (kill, alias, set, cfold, + proc change, fission, fusion, unroll, inline, call, cond). + Swap takes a range (gap pair) + a gap offset. + + Pre-normalization code positions (codepos1) use user syntax (1-indexed, + possibly negative, possibly match-based). Normalization resolves them + to 0-indexed nm_codepos1 values. *) (* Branch selection *) @@ -94,6 +94,60 @@ module Position = struct (* Normalized codepos range *) type nm_codepos_range = nm_codepos_path * nm_codepos1_range + (* --- Gap types --- *) + (* Normalized gap inside a block, 0-indexed, range [0, n] *) + type nm_codegap1 = int + (* Typed but unnormalized gap *) + type codegap1 = + | GapBefore of codepos1 (* gap immediately before this instruction *) + | GapAfter of codepos1 (* gap immediately after this instruction *) + (* Full gap with path *) + type codegap = codepos_path * codegap1 + (* Normalized gap with path *) + type nm_codegap = nm_codepos_path * nm_codegap1 + (* Gap-based range *) + type codegap1_range = codegap1 * codegap1 + type nm_codegap1_range = nm_codegap1 * nm_codegap1 + type codegap_range = codepos_path * codegap1_range + type nm_codegap_range = nm_codepos_path * nm_codegap1_range + (* Gap-based offset for swap *) + type codegap_offset1 = + | GapAbsolute of codegap1 + | GapRelative of int + + let cpos1 (i: int) : codepos1 = + (0, `ByPos i) + + let cpos1_first : codepos1 = cpos1 0 + let cpos1_last : codepos1 = cpos1 (-1) + + (* Boundary gap constructors *) + let codegap1_start : codegap1 = GapBefore cpos1_first + let codegap1_end : codegap1 = GapAfter cpos1_last + + (* Convenience constructors *) + let gap_before_pos (cp : codepos1) : codegap1 = GapBefore cp + let gap_after_pos (cp : codepos1) : codegap1 = GapAfter cp + + (* Position <-> Gap conversions (normalized, 0-indexed) *) + let gap_before (pos : nm_codepos1) : nm_codegap1 = pos + let gap_after (pos : nm_codepos1) : nm_codegap1 = pos + 1 + let instr_after (gap : nm_codegap1) : nm_codepos1 = gap (* requires gap < n *) + let instr_before (gap : nm_codegap1) : nm_codepos1 = gap - 1 (* requires gap > 0 *) + + (* Single-instruction range as gap pair *) + let gap_range_of_pos (pos : nm_codepos1) : nm_codegap1_range = + (gap_before pos, gap_after pos) + + let gap_range_of_cpos ((path, pos) : nm_codepos) : nm_codegap_range = + (path, gap_range_of_pos pos) + + (* Gap counting helpers *) + let gap_after_n (n : int) : codegap1 = GapAfter (0, `ByPos n) + let gap_before_n (n : int) : codegap1 = GapBefore (0, `ByPos n) + let gap_after_last_n (n : int) : codegap1 = GapAfter (0, `ByPos (-n)) + let gap_before_last_n(n : int) : codegap1 = GapBefore (0, `ByPos (-n)) + let shift1 ~(offset : int) ((o, p) : codepos1) : codepos1 = (o + offset, p) @@ -120,15 +174,6 @@ module Position = struct let codepos1_of_nm_codepos1 (nm: nm_codepos1) : codepos1 = (0, `ByPos nm) - let cpos1 (i: int) : codepos1 = - (0, `ByPos i) - - let cpos1_first : codepos1 = - cpos1 1 - - let cpos1_last : codepos1 = - cpos1 (-1) - let cpos1_after_last : codepos1 = (1, `ByPos (-1)) @@ -171,14 +216,6 @@ module Position = struct let nm_codepos_in_nm_codepos_range (cp: nm_codepos1) ((start, fin): nm_codepos1_range) : bool = (start <= cp && cp < fin) - let cp1_point_at_instr (cp: codepos1) : codepos1 = - match snd cp with - | `ByPos j when j < 0 -> (fst cp, `ByPos (j-1)) - | _ -> cp - - let cp_point_at_instr ((cpath, cp1): codepos) : codepos = - (cpath, cp1_point_at_instr cp1) - module Notations = struct let (|+>) (cp: codepos) (offset: int) = shift ~offset cp @@ -253,44 +290,32 @@ module Position = struct | true -> (s2, ir, s1) 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 + 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 *) + (* Throws InvalidCPos if failing — allows [0, n] where n is "after last" *) let check_nm_cpos1 (nm: nm_codepos1) (s: stmt) : unit = - if nm <= 0 || nm > (List.length s.s_node) + 1 then raise InvalidCPos + if nm < 0 || nm > List.length s.s_node then raise InvalidCPos - (* Normalizes code position wrt stmt *) + (* Normalizes code position wrt stmt — input is 0-indexed *) 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 - *) - (* FIXME: disallows pos after last when using negative codepos *) - | `ByPos i when i < 0 -> (List.length s.s_node) + i + 1 - | `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) -> + | `ByPos i when i >= 0 -> i + | `ByPos i (* i < 0 *) -> (List.length s.s_node) + 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; + 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 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 + (* List.length points to the position "after the last" and has special meaning depending on the context *) if check then check_nm_cpos1 nm s; nm @@ -370,17 +395,16 @@ module Position = struct let nm1r = normalize_cpos1_range env cp1r s in (env, s), (npath, nm1r) - (* - i is included in the second list since + (* + 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, [] + Extremal cases (0-indexed): + - Splitting at 0 should get [], s + - Splitting at List.length 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 split_at_nmcpos1 ?(rev=false) (nm: nm_codepos1) (s: stmt) = + if nm = List.length s.s_node then s.s_node, [] else let s1, i, s2 = find_by_nmcpos1 ~rev nm s in (s1, (i::s2)) @@ -408,13 +432,11 @@ module Position = struct [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) + (* + Re-align position b from block [0;n[ to sub-block + [a; n[ by realigning to [0; n-a[ through (i |-> i - a) *) - let fin = fin - start + 1 in + let fin = fin - start 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 @@ -426,7 +448,6 @@ module Position = struct end 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 @@ -451,6 +472,128 @@ module Position = struct ofdfl (fun () -> if rev then (s.s_node, []) else ([], s.s_node)) (omap ((split_at_cpos1 env)^~ s) cpos1) + + (* --- Gap normalization and split functions --- *) + + (* Check that a normalized gap is valid for the given statement *) + let check_nm_cgap1 (nm : nm_codegap1) (s : stmt) : unit = + if nm < 0 || nm > List.length s.s_node then raise InvalidCPos + + (* Normalize a codegap1 to nm_codegap1 *) + let normalize_cgap1 (env : env) (g : codegap1) (s : stmt) : nm_codegap1 = + let nm = match g with + | GapBefore cp -> normalize_cpos1 env cp s |> gap_before + | GapAfter cp -> normalize_cpos1 env cp s |> gap_after + in + check_nm_cgap1 nm s; nm + + (* Normalize a full codegap (with path) *) + let normalize_cgap (env : env) ((cpath, g1) : codegap) (s : stmt) : (env * stmt) * nm_codegap = + let (env, s), npath = normalize_cpos_path env cpath s in + (env, s), (npath, normalize_cgap1 env g1 s) + + (* Normalize a codegap1_range *) + let normalize_cgap1_range (env : env) ((g1, g2) : codegap1_range) (s : stmt) : nm_codegap1_range = + let nm1 = normalize_cgap1 env g1 s in + let nm2 = normalize_cgap1 env g2 s in + if nm1 > nm2 then raise InvalidCPos; + (nm1, nm2) + + (* Normalize a full codegap_range (with path) *) + let normalize_cgap_range (env : env) ((cpath, gr) : codegap_range) (s : stmt) : (env * stmt) * nm_codegap_range = + let (env, s), npath = normalize_cpos_path env cpath s in + let nmgr = normalize_cgap1_range env gr s in + (env, s), (npath, nmgr) + + (* Split at a normalized gap *) + let split_at_nmcgap1 (nm : nm_codegap1) (s : stmt) : instr list * instr list = + try List.takedrop nm s.s_node + with Invalid_argument _ -> raise InvalidCPos + + (* Split at a codegap1 *) + let split_at_cgap1 (env : env) (g : codegap1) (s : stmt) : instr list * instr list = + split_at_nmcgap1 (normalize_cgap1 env g s) s + + (* Split at a full codegap (with path) *) + let split_at_cgap (env : env) ((cpath, g1) : codegap) (s : stmt) : env * (instr list * instr list) = + let (env, s), _npath = normalize_cpos_path env cpath s in + env, split_at_cgap1 env g1 s + + (* Optional gap split *) + let may_split_at_cgap1 ?(rev = false) (env : env) (g : codegap1 option) (s : stmt) : instr list * instr list = + ofdfl + (fun () -> if rev then (s.s_node, []) else ([], s.s_node)) + (omap (fun g -> split_at_cgap1 env g s) g) + + (* Split by normalized gap range into (before, inside, after) *) + let split_by_nmcgap_range ((g1, g2) : nm_codegap1_range) (s : stmt) : instr list * instr list * instr list = + let before, rest = try List.takedrop g1 s.s_node + with Invalid_argument _ -> raise InvalidCPos in + let inside, after = try List.takedrop (g2 - g1) rest + with Invalid_argument _ -> raise InvalidCPos in + (before, inside, after) + + (* Split by a list of normalized gaps *) + let split_by_nmcgaps (gaps : nm_codegap1 list) (s : stmt) : instr list list = + let doit (prev, rest, acc) gap = + let seg, rest = try List.takedrop (gap - prev) rest + with (Invalid_argument _ | Not_found) -> raise InvalidCPos in + (gap, rest, seg :: acc) + in + let (_, last, segs) = List.fold_left doit (0, s.s_node, []) gaps in + List.rev (last :: segs) + + (* Resolve a gap offset relative to a gap range *) + let resolve_gap_offset (env : env) ((g1, g2) : nm_codegap1_range) (off : codegap_offset1) (s : stmt) : nm_codegap1 = + let nm = match off with + | GapAbsolute g -> + let nm = normalize_cgap1 env g s in + if g1 <= nm && nm <= g2 then raise InvalidCPos; nm + | GapRelative i -> + if i > 0 then g2 + i + else g1 + i + in + check_nm_cgap1 nm s; nm + + (* Semantic helpers for match-based finding *) + let find_last_match (env : env) (cm : cp_match) (s : stmt) = + find_by_cp_match env (Some (-1), cm) s + + let find_first_match (env : env) (cm : cp_match) (s : stmt) = + find_by_cp_match env (None, cm) s + + let find_nth_match (env : env) (n : int) (cm : cp_match) (s : stmt) = + find_by_cp_match env (Some n, cm) s + + (* [split_by_match env ~occ ~gap cm s] splits [s] at the gap before/after + the [occ]-th occurrence of [cm]. *) + let split_by_match (env : env) ~(occ : int) ~(gap : [`Before | `After]) (cm : cp_match) (s : stmt) = + let (s1, _i, s2) = find_by_cp_match env (Some occ, cm) s in + match gap with + | `Before -> (s1, _i :: s2) + | `After -> (s1 @ [_i], s2) + + let gap_before_match (env : env) ~(occ : int) (cm : cp_match) (s : stmt) : nm_codegap1 = + let (s1, _, _) = find_by_cp_match env (Some occ, cm) s in + List.length s1 + + let gap_after_match (env : env) ~(occ : int) (cm : cp_match) (s : stmt) : nm_codegap1 = + let (s1, _, _) = find_by_cp_match env (Some occ, cm) s in + List.length s1 + 1 + + (* Block iteration helpers *) + let fold_blocks ~(start : nm_codegap1) ~(block_size : int) (s : stmt) + (f : int -> nm_codegap1 -> nm_codegap1 -> 'a -> 'a) (init : 'a) : 'a = + let n = List.length s.s_node in + let rec aux idx g acc = + if g + block_size > n then acc + else aux (idx + 1) (g + block_size) (f idx g (g + block_size) acc) + in + aux 0 start init + + let iter_blocks ~(start : nm_codegap1) ~(block_size : int) (s : stmt) + (f : int -> nm_codegap1 -> nm_codegap1 -> unit) : unit = + fold_blocks ~start ~block_size s (fun idx g1 g2 () -> f idx g1 g2) () end (* -------------------------------------------------------------------- *) @@ -516,7 +659,7 @@ module Zipper = struct (ZMatch (e, ((s1, s2), zpr), { locals; prebr; postbr; }), body), `Match ix, env | _ -> raise InvalidCPos - in zpr, ((1 + List.length s1), step), env + in zpr, ((List.length s1), step), env let pre_zipper_of_codepos_path (env : EcEnv.env) (cpath: codepos_path) (s: stmt) = List.fold_left_map diff --git a/src/ecMatching.mli b/src/ecMatching.mli index aad6134b58..fa544e3a48 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -72,10 +72,6 @@ module Position : sig val shift1 : offset:int -> codepos1 -> codepos1 val shift : offset:int -> codepos -> codepos - (* FIXME: maybe remove? *) - val cp1_point_at_instr : codepos1 -> codepos1 - val cp_point_at_instr : codepos -> codepos - val resolve_offset : base:codepos1 -> offset:codeoffset1 -> codepos1 val codepos1_range_of_codepos1 : codepos1 -> codepos1_range @@ -147,6 +143,89 @@ module Position : sig val split_by_nmcpr1s : nm_codepos1 list -> stmt -> instr list list val cpos1 : int -> codepos1 + + (* --- Gap types --- *) + (* Normalized gap inside a block, 0-indexed, range [0, n] *) + type nm_codegap1 = int + (* Typed but unnormalized gap *) + type codegap1 = + | GapBefore of codepos1 + | GapAfter of codepos1 + (* Full gap with path *) + type codegap = codepos_path * codegap1 + (* Normalized gap with path *) + type nm_codegap = nm_codepos_path * nm_codegap1 + (* Gap-based ranges *) + type codegap1_range = codegap1 * codegap1 + type nm_codegap1_range = nm_codegap1 * nm_codegap1 + type codegap_range = codepos_path * codegap1_range + type nm_codegap_range = nm_codepos_path * nm_codegap1_range + (* Gap-based offset for swap *) + type codegap_offset1 = + | GapAbsolute of codegap1 + | GapRelative of int + + (* Boundary gap constructors *) + val codegap1_start : codegap1 + val codegap1_end : codegap1 + + (* Convenience constructors *) + val gap_before_pos : codepos1 -> codegap1 + val gap_after_pos : codepos1 -> codegap1 + + (* Position <-> Gap conversions (normalized, 0-indexed) *) + val gap_before : nm_codepos1 -> nm_codegap1 + val gap_after : nm_codepos1 -> nm_codegap1 + val instr_after : nm_codegap1 -> nm_codepos1 + val instr_before : nm_codegap1 -> nm_codepos1 + + (* Single-instruction range as gap pair *) + val gap_range_of_pos : nm_codepos1 -> nm_codegap1_range + val gap_range_of_cpos : nm_codepos -> nm_codegap_range + + (* Gap counting helpers *) + val gap_after_n : int -> codegap1 + val gap_before_n : int -> codegap1 + val gap_after_last_n : int -> codegap1 + val gap_before_last_n : int -> codegap1 + + (* Gap normalization *) + val check_nm_cgap1 : nm_codegap1 -> stmt -> unit + val normalize_cgap1 : env -> codegap1 -> stmt -> nm_codegap1 + val normalize_cgap : env -> codegap -> stmt -> (env * stmt) * nm_codegap + val normalize_cgap1_range : env -> codegap1_range -> stmt -> nm_codegap1_range + val normalize_cgap_range : env -> codegap_range -> stmt -> (env * stmt) * nm_codegap_range + + (* Split at gap *) + val split_at_nmcgap1 : nm_codegap1 -> stmt -> instr list * instr list + val split_at_cgap1 : env -> codegap1 -> stmt -> instr list * instr list + val split_at_cgap : env -> codegap -> stmt -> env * (instr list * instr list) + val may_split_at_cgap1 : ?rev:bool -> env -> codegap1 option -> stmt -> instr list * instr list + + (* Range operations on gaps *) + val split_by_nmcgap_range : nm_codegap1_range -> stmt -> instr list * instr list * instr list + val split_by_nmcgaps : nm_codegap1 list -> stmt -> instr list list + + (* Resolve gap offset relative to a gap range *) + val resolve_gap_offset : env -> nm_codegap1_range -> codegap_offset1 -> stmt -> nm_codegap1 + + (* Semantic helpers for match-based finding *) + val find_last_match : env -> cp_match -> stmt -> instr list * instr * instr list + val find_first_match : env -> cp_match -> stmt -> instr list * instr * instr list + val find_nth_match : env -> int -> cp_match -> stmt -> instr list * instr * instr list + + (* [split_by_match env ~occ ~gap cm s] splits [s] at the gap before/after + the [occ]-th occurrence of [cm]. *) + val split_by_match : env -> occ:int -> gap:[`Before | `After] -> cp_match -> stmt -> instr list * instr list + + val gap_before_match : env -> occ:int -> cp_match -> stmt -> nm_codegap1 + val gap_after_match : env -> occ:int -> cp_match -> stmt -> nm_codegap1 + + (* Block iteration *) + val fold_blocks : start:nm_codegap1 -> block_size:int -> stmt -> + (int -> nm_codegap1 -> nm_codegap1 -> 'a -> 'a) -> 'a -> 'a + val iter_blocks : start:nm_codegap1 -> block_size:int -> stmt -> + (int -> nm_codegap1 -> nm_codegap1 -> unit) -> unit end (* -------------------------------------------------------------------- *) diff --git a/src/ecParser.mly b/src/ecParser.mly index 725378a6f5..044d83664b 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -2553,12 +2553,27 @@ codepos1_wo_off: | k=icodepos i=option(brace(sword)) { (`ByMatch (i, k) :> pcp_base) } +(* 0-indexed variant: bare integer produces ByPos0 *) +codepos1_wo_off_0: +| i=sword + { (`ByPos0 i :> pcp_base) } + +| k=icodepos i=option(brace(sword)) + { (`ByMatch (i, k) :> pcp_base) } + codepos1: | cp=codepos1_wo_off { (0, cp) } | cp=codepos1_wo_off AMP PLUS i=word { ( i, cp) } | cp=codepos1_wo_off AMP MINUS i=word { (-i, cp) } +(* 0-indexed variant *) +codepos1_0: +| cp=codepos1_wo_off_0 { (0, cp) } + +| cp=codepos1_wo_off_0 AMP PLUS i=word { ( i, cp) } +| cp=codepos1_wo_off_0 AMP MINUS i=word { (-i, cp) } + branch_select: | SHARP s=boident DOT {`Match s} | DOT { `Cond true } @@ -2568,10 +2583,41 @@ branch_select: | i=codepos1 bs=branch_select { (i, bs) } -(* FIXME: Syntax *) -codeoffset1: -| i=sword { (`Relative i :> pcodeoffset1) } -| AT p=codepos1 { (`Absolute p :> pcodeoffset1) } +(* Gap grammar productions *) +(* Base explicit gap — direction override only *) +codegap1: +| HAT LT i=codepos1 { GapBefore i } +| HAT GT i=codepos1 { GapAfter i } + +(* Default-before: bare integer means gap before (1-indexed) *) +codegap1_before: +| i=codepos1 { GapBefore i } +| g=codegap1 { g } + +(* 0-indexed GapBefore: bare integer is 0-indexed gap number (e.g. seq) *) +codegap1_0before: +| i=codepos1_0 { GapBefore i } +| g=codegap1 { g } + +(* Default-after: bare integer means gap after (e.g. wp, sp) *) +codegap1_after: +| i=codepos1 { GapAfter i } +| g=codegap1 { g } + +(* Gap-based offset for swap *) +codegap_offset1: +| i=sword { PGapRelative i } +| AT g=codegap1_before { PGapAbsolute g } + +(* Optional gap positions *) +o_codegap1_before: +| UNDERSCORE { None } +| g=codegap1_before { Some g } + +(* s_codegap1 variants for doption *) +s_codegap1_0before: +| g=codegap1_0before { Single g } +| g1=codegap1_0before g2=codegap1_0before { Double (g1, g2) } (* FIXME: Unify with above *) (* Shift to convert input closed range into closed-open form *) @@ -2601,17 +2647,6 @@ codepos_or_range: | cp=codepos { Pos cp } | cpr=codepos_range { Range cpr } -o_codepos1: -| UNDERSCORE { None } -| i=codepos1 { Some i } - -s_codepos1: -| n=codepos1 - { Single n } - -| n1=codepos1 n2=codepos1 - { Double (n1, n2) } - semrndpos1: | b=boption(STAR) c=codepos1 { (b, c) } @@ -2663,10 +2698,10 @@ swap_info: | s=side? p=swap_position { (s, p) } swap_position: -| offset=codeoffset1 +| offset=codegap_offset1 { { interval = None; offset; } } -| interval=codepos_or_range offset=codeoffset1 +| interval=codepos_or_range offset=codegap_offset1 { { interval = Some interval; offset; } } side: @@ -2893,13 +2928,13 @@ form_or_double_form: | s=option(side) { `Head (s) } -| s=option(side) i1=o_codepos1 i2=o_codepos1 COLON f=sform +| s=option(side) i1=o_codegap1_before i2=o_codegap1_before COLON f=sform { `Seq (s, (i1, i2), f) } | CEQ f=sform { `Seq (None, (None, None), f) } -| s=option(side) i=codepos1? COLON LPAREN +| s=option(side) i=codegap1_before? COLON LPAREN UNDERSCORE COLON f1=form LONGARROW f2=form RPAREN { @@ -2956,13 +2991,13 @@ interleave_info: | PROC STAR { Pfun `Code } -| SEQ s=side? pos=s_codepos1 COLON p=form_or_double_form f=app_bd_info +| SEQ s=side? pos=s_codegap1_0before COLON p=form_or_double_form f=app_bd_info { Pseq (s, pos, p, f) } -| WP n=s_codepos1? +| WP n=s_codegap1_0before? { Pwp n } -| SP n=s_codepos1? +| SP n=s_codegap1_0before? { Psp n } | SKIP @@ -3009,7 +3044,7 @@ interleave_info: | RND s=side? info=rnd_info c=prefix(COLON, semrndpos)? { Prnd (s, c, info) } -| RNDSEM red=boption(STAR) s=side? c=codepos1 +| RNDSEM red=boption(STAR) s=side? c=codepos1_0 { Prndsem (red, s, c) } | INLINE s=side? u=inlineopt? o=occurences? @@ -3140,7 +3175,7 @@ interleave_info: | BYPR f1=sform f2=sform { PPr (Some (f1, f2)) } -| FEL at_pos=codepos1 cntr=sform delta=sform q=sform +| FEL at_pos=codegap1_after cntr=sform delta=sform q=sform f_event=sform some_p=fel_pred_specs inv=sform? { let info = { pfel_cntr = cntr; @@ -3266,7 +3301,7 @@ fel_pred_specs: {assoc_ps} eqobs_in_pos: -| i1=codepos1 i2=codepos1 { (i1, i2) } +| i1=codegap1_after i2=codegap1_after { (i1, i2) } eqobs_in_eqglob1: | LPAREN mp1= uoption(loc(fident)) TILD mp2= uoption(loc(fident)) COLON diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index c58e521301..7d9d33d55f 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -49,7 +49,9 @@ type pcp_match = [ and plvmatch = [ `LvmNone | `LvmVar of pqsymbol ] -type pcp_base = [ `ByPos of int | `ByMatch of int option * pcp_match ] +(* `ByPos: 1-indexed position (standard user syntax) + `ByPos0: 0-indexed position (used by seq, rndsem, etc.) *) +type pcp_base = [ `ByPos of int | `ByPos0 of int | `ByMatch of int option * pcp_match ] (* Code positions *) type pbranch_select = [`Cond of bool | `Match of psymbol] @@ -74,10 +76,31 @@ type pcodeoffset1 = [ (* Code position ranges *) type pcodepos1_range = (pcodepos1 * pcodeoffset1) type pcodepos_range = pcodepos_path * pcodepos1_range -type pcodepos_or_range = +type pcodepos_or_range = | Pos of pcodepos | Range of pcodepos_range +(* Code gap types *) +type pcodegap1 = + | GapBefore of pcodepos1 + | GapAfter of pcodepos1 + +(* Boundary gap constructors *) +let pcodegap1_start : pcodegap1 = GapBefore (0, `ByPos 1) +let pcodegap1_end : pcodegap1 = GapAfter (0, `ByPos (-1)) + +type pcodegap = pcodepos_path * pcodegap1 + +type pcodegap1_range = pcodegap1 * pcodegap1 +type pcodegap_range = pcodepos_path * pcodegap1_range + +(* Gap-based offset for swap *) +type pcodegap_offset1 = + | PGapAbsolute of pcodegap1 + | PGapRelative of int + +type pdocodegap1 = pcodegap1 doption option + (* -------------------------------------------------------------------- *) type pty_r = @@ -556,7 +579,7 @@ type preduction = { (* -------------------------------------------------------------------- *) type pswap_kind = { interval : pcodepos_or_range option; - offset : pcodeoffset1; + offset : pcodegap_offset1; } type interleave_info = oside * (int * int) * ((int * int) list) * int @@ -648,13 +671,13 @@ type fun_info = [ (* -------------------------------------------------------------------- *) type seq_info = - oside * pcodepos1 doption * pformula doption * p_seq_xt_info + oside * pcodegap1 doption * pformula doption * p_seq_xt_info (* -------------------------------------------------------------------- *) type pcond_info = [ | `Head of oside - | `Seq of oside * pcodepos1 option pair * pformula - | `SeqOne of side * pcodepos1 option * pformula * pformula + | `Seq of oside * pcodegap1 option pair * pformula + | `SeqOne of side * pcodegap1 option * pformula * pformula ] (* -------------------------------------------------------------------- *) @@ -723,7 +746,7 @@ type conseq_ppterm = (conseq_contra * (conseq_info) option) gppterm (* -------------------------------------------------------------------- *) type sim_info = { - sim_pos : pcodepos1 pair option; + sim_pos : pcodegap1 pair option; sim_hint : (pgamepath option pair * pformula) list * pformula option; sim_eqs : pformula option } @@ -759,8 +782,8 @@ type phltactic = | Prepl_stmt of trans_info | Pfun of fun_info | Pseq of seq_info - | Pwp of pdocodepos1 - | Psp of pdocodepos1 + | Pwp of pdocodegap1 + | Psp of pdocodegap1 | Pwhile of (oside * while_info) | Pasyncwhile of async_while_info | Pfission of (oside * pcodepos * (int * (int * int))) @@ -796,7 +819,7 @@ type phltactic = | Pbydeno of ([`PHoare | `Equiv | `EHoare ] * (deno_ppterm * bool * pformula option)) | PPr of (pformula * pformula) option | Pbyupto - | Pfel of (pcodepos1 * fel_info) + | Pfel of (pcodegap1 * fel_info) | Phoare | Pprbounded | Psim of crushmode option* sim_info diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 78f8b2062d..854e190e38 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -2386,8 +2386,10 @@ let pp_scvar ppe fmt vs = let pp_codepos1 (ppe : PPEnv.t) (fmt : Format.formatter) ((off, cp) : CP.codepos1) = let s : string = match cp with + | `ByPos i when i >= 0 -> + string_of_int (i + 1) (* 0-indexed internal → 1-indexed display *) | `ByPos i -> - string_of_int i + string_of_int i (* negative positions displayed as-is *) | `ByMatch (i, k) -> let s = @@ -2447,6 +2449,14 @@ let pp_codepos1_range (ppe: PPEnv.t) (fmt: Format.formatter) ((start, fin) : CP. 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 +(* -------------------------------------------------------------------- *) +let pp_codegap1 (ppe : PPEnv.t) (fmt : Format.formatter) (g : CP.codegap1) = + match g with + | CP.GapBefore cp -> Format.fprintf fmt "^<%a" (pp_codepos1 ppe) cp + | CP.GapAfter cp -> Format.fprintf fmt "^>%a" (pp_codepos1 ppe) cp + +let pp_codegap (ppe : PPEnv.t) (fmt : Format.formatter) ((cpath, g1) : CP.codegap) = + Format.fprintf fmt "%a%a" (pp_codepos_path ppe) cpath (pp_codegap1 ppe) g1 (* -------------------------------------------------------------------- *) 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 49d9314f6f..7ea313cc95 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -3732,7 +3732,9 @@ and trans_cp_match ?(memory : memory option) (env : EcEnv.env) (p : pcp_match) : (* -------------------------------------------------------------------- *) and trans_cp_base ?(memory : memory option) (env : EcEnv.env) (p : pcp_base) : cp_base = match p with + | `ByPos i when i > 0 -> `ByPos (i - 1) | `ByPos _ as p -> (p :> cp_base) + | `ByPos0 i -> `ByPos i (* already 0-indexed, no conversion *) | `ByMatch (i, p) -> `ByMatch (i, trans_cp_match ?memory env p) (* -------------------------------------------------------------------- *) @@ -3785,6 +3787,29 @@ and trans_codepos_or_range ?(memory: memory option) (env : EcEnv.env) (cpor: pco and trans_dcodepos1 ?(memory : memory option) (env : EcEnv.env) (p : pcodepos1 doption) : codepos1 doption = DOption.map (trans_codepos1 ?memory env) p +(* -------------------------------------------------------------------- *) +and trans_codegap1 ?(memory : memory option) (env : EcEnv.env) (g : pcodegap1) : codegap1 = + match g with + | GapBefore cp -> GapBefore (trans_codepos1 ?memory env cp) + | GapAfter cp -> GapAfter (trans_codepos1 ?memory env cp) + +and trans_codegap ?(memory : memory option) (env : EcEnv.env) ((cpath, g1) : pcodegap) : codegap = + (trans_codepos_path ?memory env cpath, trans_codegap1 ?memory env g1) + +and trans_codegap1_range ?(memory : memory option) (env : EcEnv.env) ((g1, g2) : pcodegap1_range) : codegap1_range = + (trans_codegap1 ?memory env g1, trans_codegap1 ?memory env g2) + +and trans_codegap_range ?(memory : memory option) (env : EcEnv.env) ((cpath, gr) : pcodegap_range) : codegap_range = + (trans_codepos_path ?memory env cpath, trans_codegap1_range ?memory env gr) + +and trans_codegap_offset1 ?(memory : memory option) (env : EcEnv.env) (o : pcodegap_offset1) : codegap_offset1 = + match o with + | PGapRelative i -> GapRelative i + | PGapAbsolute g -> GapAbsolute (trans_codegap1 ?memory env g) + +and trans_dcodegap1 ?(memory : memory option) (env : EcEnv.env) (p : pcodegap1 doption) : codegap1 doption = + DOption.map (trans_codegap1 ?memory env) p + (* -------------------------------------------------------------------- *) let get_instances (tvi, bty) env = let inst = List.pmap diff --git a/src/ecTyping.mli b/src/ecTyping.mli index 1eee25195b..468a695f13 100644 --- a/src/ecTyping.mli +++ b/src/ecTyping.mli @@ -245,6 +245,12 @@ val trans_codepos1 : ?memory:EcMemory.memory -> env -> pcodepos1 -> codepos1 val trans_codepos : ?memory:EcMemory.memory -> env -> pcodepos -> codepos val trans_dcodepos1 : ?memory:EcMemory.memory -> env -> pcodepos1 doption -> codepos1 doption val trans_codeoffset1 : ?memory:EcMemory.memory -> env -> pcodeoffset1 -> codeoffset1 +val trans_codegap1 : ?memory:EcMemory.memory -> env -> pcodegap1 -> codegap1 +val trans_codegap : ?memory:EcMemory.memory -> env -> pcodegap -> codegap +val trans_codegap1_range : ?memory:EcMemory.memory -> env -> pcodegap1_range -> codegap1_range +val trans_codegap_range : ?memory:EcMemory.memory -> env -> pcodegap_range -> codegap_range +val trans_codegap_offset1 : ?memory:EcMemory.memory -> env -> pcodegap_offset1 -> codegap_offset1 +val trans_dcodegap1 : ?memory:EcMemory.memory -> env -> pcodegap1 doption -> codegap1 doption (* -------------------------------------------------------------------- *) type ptnmap = ty EcIdent.Mid.t ref diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml index 64e72894a4..6e4021436a 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 _, _, _, _, _, wppre, _ = ehoare_call_pre_post fpre fpost tc in let tcenv = - EcPhlSeq.t_ehoare_seq (EcMatching.Position.cpos1_after_last) wppre tc in + EcPhlSeq.t_ehoare_seq (GapBefore (EcMatching.Position.cpos1_last)) 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 _, _, _, _, _, wppre, wppost = ehoare_call_pre_post fpre fpost tc in let tcenv = - EcPhlSeq.t_ehoare_seq (EcMatching.Position.cpos1_after_last) + EcPhlSeq.t_ehoare_seq (GapBefore (EcMatching.Position.cpos1_last)) (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/ecPhlCond.ml b/src/phl/ecPhlCond.ml index a3dade6a85..65af601e03 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 (EcMatching.Position.cpos1 1)) + (EcPhlRCond.t_rcond side b (EcMatching.Position.cpos1 0)) (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 (EcMatching.Position.cpos1 1)) + (EcPhlRCond.Low.t_equiv_rcond `Right true (EcMatching.Position.cpos1 0)) [t_aux; t_clear hiff]; FApi.t_seqsub - (EcPhlRCond.Low.t_equiv_rcond `Right false (EcMatching.Position.cpos1 1)) + (EcPhlRCond.Low.t_equiv_rcond `Right false (EcMatching.Position.cpos1 0)) [t_aux; t_clear hiff]])) tc @@ -223,7 +223,7 @@ end = struct in tc - |> EcPhlRCond.t_rcond_match side cname (EcMatching.Position.cpos1 1) + |> EcPhlRCond.t_rcond_match side cname (EcMatching.Position.cpos1 0) @+ [discharge; clean] in diff --git a/src/phl/ecPhlEager.ml b/src/phl/ecPhlEager.ml index b868e5d3b1..65d8efd3f2 100644 --- a/src/phl/ecPhlEager.ml +++ b/src/phl/ecPhlEager.ml @@ -67,16 +67,10 @@ 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 EcMatching.Position.Notations.(cpos1_first +> ss) c + let z, c = s_split env EcMatching.Position.Notations.(cpos1_first +> ss) c and c', z' = s_split env EcMatching.Position.Notations.(cpos1_after_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 diff --git a/src/phl/ecPhlEqobs.ml b/src/phl/ecPhlEqobs.ml index 86095b4605..89b3031660 100644 --- a/src/phl/ecPhlEqobs.ml +++ b/src/phl/ecPhlEqobs.ml @@ -281,10 +281,6 @@ 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 @@ -472,15 +468,11 @@ let process_eqobs_inS info tc = (FApi.t_try (FApi.t_seq EcPhlSkip.t_skip t_trivial)) (t_eqobs_inS sim eqo 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); + (* sim positions are gaps: sim applies to instructions after the gap *) + let p1 = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left , p1) in + let p2 = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Right, p2) in + let _,sl2 = s_split_at_gap env p1 es.es_sl in + let _,sr2 = s_split_at_gap env p2 es.es_sr in 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 b86fa7ff87..cef7b79990 100644 --- a/src/phl/ecPhlExists.ml +++ b/src/phl/ecPhlExists.ml @@ -8,6 +8,7 @@ open EcSubst open EcCoreGoal open EcLowGoal open EcLowPhlGoal +open EcMatching.Position module L = EcLocation module APT = EcParsetree @@ -160,19 +161,19 @@ let process_ecall oside (l, tvi, fs) tc = match kind, oside, p1 with | `Hoare n, _, Inv_ss p1 -> EcPhlSeq.t_hoare_seq - (EcMatching.Position.cpos1 n) p1 tc + (GapBefore (EcMatching.Position.cpos1 (n - 1))) p1 tc | `Hoare n, _, Inv_hs p1 -> EcPhlSeq.t_hoare_seq - (EcMatching.Position.cpos1 n) (POE.lower p1) tc + (GapBefore (EcMatching.Position.cpos1 (n - 1))) (POE.lower p1) tc | `Equiv (n1, n2), None, Inv_ts p1 -> EcPhlSeq.t_equiv_seq - (EcMatching.Position.cpos1 n1, EcMatching.Position.cpos1 n2) p1 tc + (GapBefore (EcMatching.Position.cpos1 (n1 - 1)), GapBefore (EcMatching.Position.cpos1 (n2 - 1))) p1 tc | `Equiv (n1, n2), Some `Left, Inv_ts p1 -> EcPhlSeq.t_equiv_seq - (EcMatching.Position.cpos1 n1, EcMatching.Position.cpos1 (n2+1)) p1 tc + (GapBefore (EcMatching.Position.cpos1 (n1 - 1)), GapBefore (EcMatching.Position.cpos1 n2)) p1 tc | `Equiv(n1, n2), Some `Right, Inv_ts p1 -> EcPhlSeq.t_equiv_seq - (EcMatching.Position.cpos1 (n1+1), EcMatching.Position.cpos1 n2) p1 tc + (GapBefore (EcMatching.Position.cpos1 n1), GapBefore (EcMatching.Position.cpos1 (n2 - 1))) p1 tc | _ -> tc_error !!tc "mismatched sidedness or kind of conclusion" in diff --git a/src/phl/ecPhlFel.ml b/src/phl/ecPhlFel.ml index fd3d163205..24e6ee88ed 100644 --- a/src/phl/ecPhlFel.ml +++ b/src/phl/ecPhlFel.ml @@ -112,11 +112,11 @@ let callable_oracles_stmt env modv = (* -------------------------------------------------------------------- *) (* FIXME: do we have to subst more? *) +(* [t_failure_event_r (gap, ...)]: splits the function body at [gap]; + FEL is applied to instructions after the gap. *) let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc = let env, _, concl = FApi.tc1_eflat tc in - let at_pos = EcMatching.Position.Notations.(at_pos +> 1) in - let (pr, bd) = match concl.f_node with | Fapp ({ f_node =Fop (op, _) }, [pr; bd]) @@ -135,7 +135,7 @@ let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc = with _ -> tc_error !!tc "not applicable to abstract functions" in - let s_hd, s_tl = EcLowPhlGoal.s_split env at_pos fdef.f_body in + let s_hd, s_tl = EcLowPhlGoal.s_split_at_gap env at_pos fdef.f_body in let fve = PV.fv env f_event.m f_event.inv in let fvc = PV.fv env cntr.m cntr.inv in let fvi = PV.fv env inv.m inv.inv in @@ -273,7 +273,7 @@ let process_fel at_pos (infos : fel_info) tc = let m = EcIdent.create "&hr" in - let at_pos = EcTyping.trans_codepos1 env at_pos in + let at_pos = EcTyping.trans_codegap1 env at_pos in let hyps = LDecl.inv_memenv1 m hyps1 in let cntr = {m;inv=TTC.pf_process_form !!tc hyps tint infos.pfel_cntr} in let hypsq = LDecl.push_active_ss (EcMemory.abstract pr.pr_mem) hyps1 in diff --git a/src/phl/ecPhlFel.mli b/src/phl/ecPhlFel.mli index e6769715a0..cab7b0366f 100644 --- a/src/phl/ecPhlFel.mli +++ b/src/phl/ecPhlFel.mli @@ -7,11 +7,11 @@ open EcMatching.Position (* -------------------------------------------------------------------- *) val t_failure_event : - codepos1 + codegap1 -> ss_inv -> form -> form -> ss_inv -> (xpath * ss_inv) list -> ss_inv -> backward (* -------------------------------------------------------------------- *) -val process_fel : pcodepos1 -> fel_info -> backward +val process_fel : pcodegap1 -> fel_info -> backward diff --git a/src/phl/ecPhlHiAuto.ml b/src/phl/ecPhlHiAuto.ml index aaf9ec0e73..31a2f99735 100644 --- a/src/phl/ecPhlHiAuto.ml +++ b/src/phl/ecPhlHiAuto.ml @@ -7,6 +7,7 @@ open EcModules open EcCoreGoal open EcLowGoal open EcLowPhlGoal +open EcMatching.Position (* -------------------------------------------------------------------- *) type ll_strategy = @@ -54,7 +55,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc = tc |> match lls with | LL_WP -> - EcPhlWp.t_wp (Some (Single (EcMatching.Position.cpos1_last))) + EcPhlWp.t_wp (Some (Single (GapBefore (EcMatching.Position.cpos1_last)))) | LL_RND -> let m = EcIdent.create "&hr" in @@ -69,7 +70,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc = | LL_JUMP -> let m = EcIdent.create "&hr" in ( EcPhlSeq.t_bdhoare_seq - (EcMatching.Position.cpos1_last) ({m;inv=f_true}, {m;inv=f_true}, + (GapBefore (EcMatching.Position.cpos1_last)) ({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 +88,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc = in ( EcPhlSeq.t_bdhoare_seq - (EcMatching.Position.cpos1_last) ({m;inv=f_true}, {m;inv=f_true}, {m;inv=f_r1}, {m;inv=f_r1}, {m;inv=f_r0}, {m;inv=f_r1}) + (GapBefore (EcMatching.Position.cpos1_last)) ({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 +143,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.Position.cpos1_first) {m=ml;inv=f_true} {m=ml;inv=f_true}) @+ - [ (EcPhlSeq.t_equiv_seq_onesided `Right (EcMatching.Position.cpos1_first) {m=mr;inv=f_true} {m=mr;inv=f_true}) @+ + ((EcPhlSeq.t_equiv_seq_onesided `Left (EcMatching.Position.codegap1_start) {m=ml;inv=f_true} {m=ml;inv=f_true}) @+ + [ (EcPhlSeq.t_equiv_seq_onesided `Right (EcMatching.Position.codegap1_start) {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 23d33836e3..cb19956841 100644 --- a/src/phl/ecPhlHiCond.ml +++ b/src/phl/ecPhlHiCond.ml @@ -8,8 +8,8 @@ open EcMatching.Position (* -------------------------------------------------------------------- *) let process_cond (info : EcParsetree.pcond_info) tc = - let default_if (i : codepos1 option) s = - ofdfl (fun _ -> cpos1 (tc1_pos_last_if tc s)) i in + let default_if (i : codegap1 option) s = + ofdfl (fun _ -> GapBefore (cpos1 (tc1_pos_last_if tc s))) i in match info with | `Head side -> @@ -22,8 +22,8 @@ let process_cond (info : EcParsetree.pcond_info) tc = | `Seq (side, (i1, i2), f) -> let es = tc1_as_equivS tc in let f = EcProofTyping.tc1_process_prhl_formula tc f in - let i1 = Option.map (fun i1 -> EcLowPhlGoal.tc1_process_codepos1 tc (side, i1)) i1 in - let i2 = Option.map (fun i2 -> EcLowPhlGoal.tc1_process_codepos1 tc (side, i2)) i2 in + let i1 = Option.map (fun i1 -> EcLowPhlGoal.tc1_process_codegap1 tc (side, i1)) i1 in + let i2 = Option.map (fun i2 -> EcLowPhlGoal.tc1_process_codegap1 tc (side, i2)) i2 in let n1 = default_if i1 es.es_sl in let n2 = default_if i2 es.es_sr in FApi.t_seqsub (EcPhlSeq.t_equiv_seq (n1, n2) f) @@ -31,7 +31,7 @@ let process_cond (info : EcParsetree.pcond_info) tc = | `SeqOne (s, i, f1, f2) -> let es = tc1_as_equivS tc in - let i = Option.map (fun i1 -> EcLowPhlGoal.tc1_process_codepos1 tc (Some s, i1)) i in + let i = Option.map (fun i1 -> EcLowPhlGoal.tc1_process_codegap1 tc (Some s, i1)) i in let n = default_if i (match s with `Left -> es.es_sl | `Right -> es.es_sr) in let _, f1 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f1 in let _, f2 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f2 in diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml index 96a9b37cc5..27b3b749a8 100644 --- a/src/phl/ecPhlLoopTx.ml +++ b/src/phl/ecPhlLoopTx.ml @@ -285,13 +285,28 @@ let process_unroll_for ~cfold side cpos tc = let m = LDecl.fresh_id hyps "&m" in let x = f_pvar x tint goal_m in + (* Record the proof handle, position, and counter value for iteration [i]. + Used by [doi] below to revisit each unrolled iteration's subgoal. *) let t_set i pos z tc = hds.(i) <- Some (FApi.tc1_handle tc, pos, z); t_id tc in + (* Strengthen the goal by replacing the current precondition with [post], + closing the two side-conditions (pre ⇒ post, post ⇒ pre) via [t_trivial]. *) let t_conseq post tc = (EcPhlConseq.t_conseq (tc1_get_pre tc) post @+ [ t_trivial; t_trivial; t_id]) tc in + (* Main unrolling loop: processes the list [zs] of counter values produced + by [eval_cond]. For each value [z]: + 1. Apply [t_rcond] at position [pos] (0-indexed) to split the while into + its body (when [zs] is non-empty, i.e. guard is true) or skip it + (when [zs] is empty, i.e. guard is false). + 2. On the "guard proved" subgoal: introduce the guard hypothesis, + strengthen the pre to [x = z], and record iteration info via [t_set]. + 3. On the "rest of program" subgoal: recurse with the next counter value, + advancing [pos] by [blen] (the loop body length) since the unrolled + body instructions now precede the remaining while. + [pos] is a 0-indexed normalized position used to construct [cpos1 pos]. *) let rec t_doit i pos zs tc = match zs with | [] -> t_id tc @@ -302,6 +317,10 @@ let process_unroll_for ~cfold side cpos tc = t_set i pos z; t_doit (i+1) (pos + blen) zs]) tc in + (* Close a subgoal of the form hoare[... : pre ==> true] by: + 1. Weakening the postcondition to hoare-with-no-memory via [t_hoareS_conseq_nm] + 2. Closing side conditions with [t_trivial] + 3. Closing the main goal with [t_hoare_true] *) let t_conseq_nm tc = match (tc1_get_pre tc) with | Inv_ss inv -> @@ -312,19 +331,30 @@ let process_unroll_for ~cfold side cpos tc = [ t_trivial; t_trivial; EcPhlTAuto.t_hoare_true]) tc | _ -> tc_error !!tc "expecting single sided precondition" in + (* Second pass: revisit the subgoals recorded by [t_set] during [t_doit]. + For each iteration [i]: + - [pos] is the 0-indexed position of the while loop (rcond target). + - [init_pos] = pos - 1 is the counter init/increment assignment that + precedes the while; WP must consume through it to evaluate [x = z]. + - i=0: WP from [init_pos] onward, strengthen pre to true, close with + [t_hoare_true]. + - i>0: WP from [init_pos] onward, then seq-split at the previous + iteration's rcond position [pos'] with postcondition [x = z'], + applying the recorded proof handle [h'] and [t_conseq_nm]. *) 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 + let (_h, pos, _z) = oget hds.(i) in + let init_pos = pos - 1 in + let wp_gap = GapBefore (cpos1 init_pos) in if i = 0 then - (EcPhlWp.t_wp (Some (Single ((cpos1 pos) <+ 1))) @! + (EcPhlWp.t_wp (Some (Single wp_gap)) @! 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 ((cpos1 pos) <+ 1))); - EcPhlSeq.t_hoare_seq (cpos1 pos') (map_ss_inv2 f_eq x {m=goal_m;inv=f_int z'}) @+ + EcPhlWp.t_wp (Some (Single wp_gap)); + EcPhlSeq.t_hoare_seq (GapBefore (cpos1 pos')) (map_ss_inv2 f_eq x {m=goal_m;inv=f_int z'}) @+ [t_apply_hd h'; t_conseq_nm] ] tc in diff --git a/src/phl/ecPhlRnd.ml b/src/phl/ecPhlRnd.ml index a1462ef611..96ef8cb790 100644 --- a/src/phl/ecPhlRnd.ml +++ b/src/phl/ecPhlRnd.ml @@ -649,11 +649,6 @@ let t_equiv_rnd ?pos side bij_info = let process_rnd (side: side option) (pos: (bool * pcodepos1) doption option) tac_info tc = let concl = FApi.tc1_goal tc in - (* Rnd takes 0-indexed positions from user side *) - let pos = Option.map (DOption.map (fun (b, cp) -> - (b, EcParsetree.shift1 ~offset:1 cp) - )) pos in - match side, pos, tac_info with | None, None, PNoRndParams when is_hoareS concl -> t_hoare_rnd tc @@ -724,9 +719,6 @@ let process_rndsem ~reduce side pos tc = let concl = FApi.tc1_goal tc in let pos = EcLowPhlGoal.tc1_process_codepos1 tc (side, pos) in - (* Rndsem takes 0-indexed positions *) - let pos = EcMatching.Position.Notations.(pos +> 1) in - match side with | None when is_hoareS concl -> t_hoare_rndsem reduce pos tc diff --git a/src/phl/ecPhlRwEquiv.ml b/src/phl/ecPhlRwEquiv.ml index 62ce176c82..9fab600d3f 100644 --- a/src/phl/ecPhlRwEquiv.ml +++ b/src/phl/ecPhlRwEquiv.ml @@ -80,7 +80,7 @@ let t_rewrite_equiv side dir cp (equiv : equivF) equiv_pt rargslv tc = t_onselect p (t_seqs [ - EcPhlEqobs.process_eqobs_in none {sim_pos = some (cp, cp); sim_hint = ([], none); sim_eqs = none}; + EcPhlEqobs.process_eqobs_in none {sim_pos = some (GapAfter cp, GapAfter cp); sim_hint = ([], none); sim_eqs = none}; (match side, dir with | `Left, `LtoR -> t_id | `Left, `RtoL -> EcPhlSym.t_equiv_sym diff --git a/src/phl/ecPhlSeq.ml b/src/phl/ecPhlSeq.ml index b0109f4ac5..05287d4bd4 100644 --- a/src/phl/ecPhlSeq.ml +++ b/src/phl/ecPhlSeq.ml @@ -14,14 +14,13 @@ open EcLowPhlGoal module TTC = EcProofTyping (* -------------------------------------------------------------------- *) +(* [t_hoare_seq_r gap phi]: splits the statement at [gap]; the first + subgoal covers instructions before the gap, the second after. *) let t_hoare_seq_r i phi tc = let env = FApi.tc1_env tc in 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 s1, s2 = s_split_at_gap env i hs.hs_s in 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 @@ -33,7 +32,7 @@ let t_hoare_seq = FApi.t_low2 "hoare-seq" t_hoare_seq_r let t_ehoare_seq_r i phi tc = let env = FApi.tc1_env tc in let hs = tc1_as_ehoareS tc in - let s1, s2 = s_split env i hs.ehs_s in + let s1, s2 = s_split_at_gap env i hs.ehs_s in let phi = ss_inv_rebind phi (fst hs.ehs_m) in let a = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) (stmt s1) phi in let b = f_eHoareS (snd hs.ehs_m) phi (stmt s2) (ehs_po hs) in @@ -52,7 +51,7 @@ let t_bdhoare_seq_r_low i (phi, pR, f1, f2, g1, g2) tc = let f2 = ss_inv_rebind f2 m in let g1 = ss_inv_rebind g1 m in let g2 = ss_inv_rebind g2 m in - let s1, s2 = s_split env i bhs.bhs_s in + let s1, s2 = s_split_at_gap env i bhs.bhs_s in let s1, s2 = stmt s1, stmt s2 in let nR = map_ss_inv1 f_not pR in let mt = snd bhs.bhs_m in @@ -123,8 +122,8 @@ let t_bdhoare_seq = FApi.t_low2 "bdhoare-seq" t_bdhoare_seq_r let t_equiv_seq (i, j) phi tc = let env = FApi.tc1_env tc in let es = tc1_as_equivS tc in - let sl1,sl2 = s_split env i es.es_sl in - let sr1,sr2 = s_split env j es.es_sr in + let sl1,sl2 = s_split_at_gap env i es.es_sl in + let sr1,sr2 = s_split_at_gap env j es.es_sr in let mtl, mtr = snd es.es_ml, snd es.es_mr in let a = f_equivS mtl mtr (es_pr es) (stmt sl1) (stmt sr1) phi in let b = f_equivS mtl mtr phi (stmt sl2) (stmt sr2) (es_po es) in @@ -137,11 +136,11 @@ let t_equiv_seq_onesided side i pre post tc = let (ml, mr) = fst es.es_ml, fst es.es_mr in let s, _s', p', q' = match side with - | `Left -> + | `Left -> let p' = ss_inv_generalize_as_left pre ml mr in let q' = ss_inv_generalize_as_left post ml mr in es.es_sl, es.es_sr, p', q' - | `Right -> + | `Right -> let p' = ss_inv_generalize_as_right pre ml mr in let q' = ss_inv_generalize_as_right post ml mr in es.es_sr, es.es_sl, p', q' @@ -149,9 +148,9 @@ 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, EcMatching.Position.cpos1_after_last ) - | `Right -> (EcMatching.Position.cpos1_after_last, i) in - let _s1, s2 = s_split env i s in + | `Left -> (i, EcMatching.Position.codegap1_end) + | `Right -> (EcMatching.Position.codegap1_end, i) in + let _s1, s2 = s_split_at_gap env i s in let modi = EcPV.s_write env (EcModules.stmt s2) in let r = map_ts_inv2 f_and p' (generalize_mod_side env modi (map_ts_inv2 f_imp q' (es_po es))) in @@ -219,11 +218,6 @@ 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 @@ -237,13 +231,13 @@ let process_seq ((side, k, phi, bd_info) : seq_info) (tc : tcenv1) = | Single i, PSeqNone when is_hoareS concl -> check_side side; let _, phi = TTC.tc1_process_Xhl_formula tc (get_single phi) in - let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (side, i) in t_hoare_seq i phi tc | Single i, PSeqNone when is_eHoareS concl -> check_side side; let _, phi = TTC.tc1_process_Xhl_formula_xreal tc (get_single phi) in - let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (side, i) in t_ehoare_seq i phi tc | Single i, PSeqNone when is_equivS concl -> @@ -258,21 +252,21 @@ let process_seq ((side, k, phi, bd_info) : seq_info) (tc : tcenv1) = match side with | None -> tc_error !!tc "seq onsided: side information expected" | Some side -> side in - let i = EcLowPhlGoal.tc1_process_codepos1 tc (Some side, i) in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (Some side, i) in t_equiv_seq_onesided side i pre post tc | Single i, _ when is_bdHoareS concl -> check_side side; let _, pia = TTC.tc1_process_Xhl_formula tc (get_single phi) in let (ra, f1, f2, f3, f4) = process_phl_bd_info bd_info tc in - let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (side, i) in t_bdhoare_seq i (ra, pia, f1, f2, f3, f4) tc | Double (i, j), PSeqNone when is_equivS concl -> check_side side; let phi = TTC.tc1_process_prhl_formula tc (get_single phi) in - let i = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Left, i) in - let j = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Left, j) in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left, i) in + let j = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left, j) in t_equiv_seq (i, j) phi tc | Single _, PSeqNone diff --git a/src/phl/ecPhlSeq.mli b/src/phl/ecPhlSeq.mli index b5b905ad58..fd699b62e3 100644 --- a/src/phl/ecPhlSeq.mli +++ b/src/phl/ecPhlSeq.mli @@ -6,11 +6,11 @@ open EcMatching.Position open EcAst (* -------------------------------------------------------------------- *) -val t_hoare_seq : codepos1 -> ss_inv -> backward -val t_ehoare_seq : codepos1 -> ss_inv -> backward -val t_bdhoare_seq : codepos1 -> ss_inv tuple6 -> backward -val t_equiv_seq : codepos1 pair -> ts_inv -> backward -val t_equiv_seq_onesided : side -> codepos1 -> ss_inv -> ss_inv -> backward +val t_hoare_seq : codegap1 -> ss_inv -> backward +val t_ehoare_seq : codegap1 -> ss_inv -> backward +val t_bdhoare_seq : codegap1 -> ss_inv tuple6 -> backward +val t_equiv_seq : codegap1 pair -> ts_inv -> backward +val t_equiv_seq_onesided : side -> codegap1 -> ss_inv -> ss_inv -> backward (* -------------------------------------------------------------------- *) val process_seq : seq_info -> backward diff --git a/src/phl/ecPhlSp.ml b/src/phl/ecPhlSp.ml index 4675f081de..f3abed6535 100644 --- a/src/phl/ecPhlSp.ml +++ b/src/phl/ecPhlSp.ml @@ -242,7 +242,7 @@ let t_sp_side pos tc = match concl.f_node, pos with | FhoareS hs, (None | Some (Single _)) -> let pos = pos |> omap as_single in - let stmt1, stmt2 = o_split ~rev:true env pos hs.hs_s in + let stmt1, stmt2 = o_split_at_gap ~rev:true env pos hs.hs_s in let stmt1, hs_pr = LI.sp_stmt hs.hs_m env stmt1 (hs_pr hs).inv in check_sp_progress pos stmt1; let m = fst hs.hs_m in @@ -258,7 +258,7 @@ let t_sp_side pos tc = | FbdHoareS bhs, (None | Some (Single _)) -> let pos = pos |> omap as_single in - let stmt1, stmt2 = o_split ~rev:true env pos bhs.bhs_s in + let stmt1, stmt2 = o_split_at_gap ~rev:true env pos bhs.bhs_s in check_form_indep stmt1 bhs.bhs_m (bhs_bd bhs).inv; let stmt1, bhs_pr = LI.sp_stmt bhs.bhs_m env stmt1 (bhs_pr bhs).inv in check_sp_progress pos stmt1; @@ -271,8 +271,8 @@ let t_sp_side pos tc = let posL = pos |> omap fst in let posR = pos |> omap snd in - let stmtL1, stmtL2 = o_split ~rev:true env posL es.es_sl in - let stmtR1, stmtR2 = o_split ~rev:true env posR es.es_sr in + let stmtL1, stmtL2 = o_split_at_gap ~rev:true env posL es.es_sl in + let stmtR1, stmtR2 = o_split_at_gap ~rev:true env posR es.es_sr in let es_pr = (es_pr es) in let ml, mr = fst es.es_ml, fst es.es_mr in @@ -301,12 +301,9 @@ let t_sp_side pos tc = let t_sp = FApi.t_low1 "sp" t_sp_side (* -------------------------------------------------------------------- *) -let process_sp (cpos : pcodepos1 doption option) (tc : tcenv1) = +(* [process_sp gap]: splits the statement at [gap]; instructions after the + gap are kept, sp is applied to instructions before the gap. *) +let process_sp (cpos : pcodegap1 doption option) (tc : tcenv1) = let env = FApi.tc1_env tc in - let cpos = Option.map (EcTyping.trans_dcodepos1 env) cpos in - let cpos = - Option.map (DOption.map (fun cp -> - EcMatching.Position.Notations.(cp +> 1) - )) cpos - in + let cpos = Option.map (EcTyping.trans_dcodegap1 env) cpos in t_sp cpos tc diff --git a/src/phl/ecPhlSp.mli b/src/phl/ecPhlSp.mli index 2625f40305..3592d8caf5 100644 --- a/src/phl/ecPhlSp.mli +++ b/src/phl/ecPhlSp.mli @@ -5,7 +5,7 @@ open EcCoreGoal.FApi open EcUtils (* -------------------------------------------------------------------- *) -val t_sp : (codepos1 doption) option -> backward +val t_sp : (codegap1 doption) option -> backward (* -------------------------------------------------------------------- *) -val process_sp : (pcodepos1 doption) option -> backward +val process_sp : (pcodegap1 doption) option -> backward diff --git a/src/phl/ecPhlSwap.ml b/src/phl/ecPhlSwap.ml index ef90639e2f..462163c244 100644 --- a/src/phl/ecPhlSwap.ml +++ b/src/phl/ecPhlSwap.ml @@ -13,7 +13,7 @@ open EcLowGoal (* -------------------------------------------------------------------- *) type swap_kind = { interval : codepos_range; - offset : codeoffset1; + offset : codegap_offset1; } (* -------------------------------------------------------------------- *) @@ -79,23 +79,16 @@ module LowInternal = struct ) in - let target = try - Format.eprintf "Start: %d | End: %d | Len: %d@." start fin (List.length s.s_node); - resolve_offset1_from_cpos1_range env (start, fin) info.offset s + let target = try + resolve_gap_offset env (start, fin) info.offset s with InvalidCPos -> - tc_error_lazy pf (fun fmt -> - let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt "invalid offset for swap: %a" (EcPrinting.pp_codeoffset1 ppe) info.offset) + tc_error pf "invalid offset for swap" in - Format.eprintf "Swapping: (start %d, end %d, target %d)@." start fin target; - - match split_by_nmcpr1s - (if target <= start + 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] + else [start; fin; target] ) s with | [hd; s1; s2; tl] -> check_swap pf env (stmt s1) (stmt s2); @@ -132,14 +125,14 @@ let rec process_swap1 (info : (oside * pswap_kind) located) (tc : tcenv1) = EcTyping.trans_codepos_or_range ~memory:(fst me) env pcpor ) pos.interval in - let offset = EcTyping.trans_codeoffset1 ~memory:(fst me) env pos.offset in + let offset = EcTyping.trans_codegap_offset1 ~memory:(fst me) env pos.offset in let interval = match interval, offset with | Some interval, _ -> interval - | None, `Relative i -> + | None, GapRelative i -> codepos_range_of_codepos (if i > 0 then cpos_first else cpos_last) - | None, _ -> + | None, _ -> tc_error (!!tc) "Cannot give a absolute offset and no range" in @@ -165,14 +158,14 @@ let process_interleave info tc = "invalide interleave range (%i + %i * %i <= %i)" pos1 k n1 pos2; - (* FIXME: should use t_swap and not process_swap *) + (* FIXME: should use t_swap and not process_swap; offset should use gap type *) let rec aux pos1 pos2 k tc = if k <= 0 then t_id tc else let data : pswap_kind = (* Represent range [pos2, pos2+n2[ *) let p1 = (0, `ByPos pos2) in let p2 = (0, `ByPos (pos2+n2)) in - let o = `Relative ((pos1+n1) - pos2) in + let o = PGapRelative ((pos1+n1) - pos2) in { interval = Some (Range ([], (p1, `Absolute p2))); offset = o; } in FApi.t_seq (process_swap1 (mk_loc loc (side, data))) diff --git a/src/phl/ecPhlSwap.mli b/src/phl/ecPhlSwap.mli index 77a411fc78..b58c6c3956 100644 --- a/src/phl/ecPhlSwap.mli +++ b/src/phl/ecPhlSwap.mli @@ -7,7 +7,7 @@ open EcCoreGoal.FApi (* -------------------------------------------------------------------- *) type swap_kind = { interval : codepos_range; - offset : codeoffset1; + offset : codegap_offset1; } (* -------------------------------------------------------------------- *) diff --git a/src/phl/ecPhlWhile.ml b/src/phl/ecPhlWhile.ml index 5fd61874c8..75f3315c36 100644 --- a/src/phl/ecPhlWhile.ml +++ b/src/phl/ecPhlWhile.ml @@ -10,6 +10,7 @@ open EcParsetree open EcCoreGoal open EcLowPhlGoal open EcLowGoal +open EcMatching.Position module Sx = EcPath.Sx module TTC = EcProofTyping @@ -113,7 +114,8 @@ let t_ehoare_while inv tc = let m = EcMemory.memory hs.ehs_m in let e = ss_inv_of_expr m e in let tc = - FApi.t_rotate `Left 1 (EcPhlSeq.t_ehoare_seq (0, `ByPos (List.length hs.ehs_s.s_node - 1)) inv tc) in + (* FIXME: codepos should not be constructed inline *) + FApi.t_rotate `Left 1 (EcPhlSeq.t_ehoare_seq (GapBefore (0, `ByPos (List.length hs.ehs_s.s_node - 1))) inv tc) in FApi.t_sub [(EcPhlConseq.t_ehoareS_conseq inv (map_ss_inv2 f_interp_ehoare_form (map_ss_inv1 f_not e) inv)) @+ [t_trivial; diff --git a/src/phl/ecPhlWp.ml b/src/phl/ecPhlWp.ml index f414444fe6..74a529345d 100644 --- a/src/phl/ecPhlWp.ml +++ b/src/phl/ecPhlWp.ml @@ -8,6 +8,7 @@ open EcFol open EcCoreGoal open EcLowPhlGoal +open EcMatching.Position (* -------------------------------------------------------------------- *) module LowInternal = struct @@ -163,11 +164,13 @@ module TacInternal = struct if EcUtils.is_some i && not (List.is_empty rm) then tc_error !!tc "remaining %i instruction(s)" (List.length rm) - let t_hoare_wp ?(uselet=true) i tc = + (* [t_hoare_wp gap]: splits the statement at [gap]; instructions before the + gap are kept, wp is applied to instructions after the gap. *) + let t_hoare_wp ?(uselet=true) (i : codegap1 option) tc = let hyps = FApi.tc1_hyps tc in let env = EcEnv.LDecl.toenv hyps in let hs = tc1_as_hoareS tc in - let (s_hd, s_wp) = o_split env i hs.hs_s in + let (s_hd, s_wp) = o_split_at_gap env i hs.hs_s in let s_wp = EcModules.stmt s_wp in let { exnmap = (eposts, d) } as post = (hs_po hs).hsi_inv in let s_wp, post = wp ~uselet ~onesided:true hyps hs.hs_m s_wp post in @@ -178,10 +181,10 @@ module TacInternal = struct let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s post in FApi.xmutate1 tc `Wp [concl] - let t_ehoare_wp ?(uselet=true) i tc = + let t_ehoare_wp ?(uselet=true) (i : codegap1 option) tc = let env = FApi.tc1_env tc in let hs = tc1_as_ehoareS tc in - let (s_hd, s_wp) = o_split env i hs.ehs_s in + let (s_hd, s_wp) = o_split_at_gap env i hs.ehs_s in let s_wp = EcModules.stmt s_wp in let (s_wp, post) = ewp ~uselet env hs.ehs_m s_wp (ehs_po hs).inv in check_wp_progress tc i hs.ehs_s s_wp; @@ -190,11 +193,11 @@ module TacInternal = struct let concl = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) s {m;inv=post} in FApi.xmutate1 tc `Wp [concl] - let t_bdhoare_wp ?(uselet=true) i tc = + let t_bdhoare_wp ?(uselet=true) (i : codegap1 option) tc = let hyps = FApi.tc1_hyps tc in let env = EcEnv.LDecl.toenv hyps in let bhs = tc1_as_bdhoareS tc in - let (s_hd, s_wp) = o_split env i bhs.bhs_s in + let (s_hd, s_wp) = o_split_at_gap env i bhs.bhs_s in let s_wp = EcModules.stmt s_wp in let s_wp, post = wp ~uselet hyps bhs.bhs_m s_wp (POE.empty (bhs_po bhs).inv) @@ -205,14 +208,14 @@ module TacInternal = struct let concl = f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) s {m;inv=post} bhs.bhs_cmp (bhs_bd bhs) in FApi.xmutate1 tc `Wp [concl] - let t_equiv_wp ?(uselet=true) ij tc = + let t_equiv_wp ?(uselet=true) (ij : (codegap1 * codegap1) option) tc = let hyps = FApi.tc1_hyps tc in let env = EcEnv.LDecl.toenv hyps in let es = tc1_as_equivS tc in let ml, mr = (fst es.es_ml), (fst es.es_mr) in let i = omap fst ij and j = omap snd ij in - let s_hdl,s_wpl = o_split env i es.es_sl in - let s_hdr,s_wpr = o_split env j es.es_sr in + let s_hdl,s_wpl = o_split_at_gap env i es.es_sl in + let s_hdr,s_wpr = o_split_at_gap env j es.es_sr in let meml, s_wpl = es.es_ml, EcModules.stmt s_wpl in let memr, s_wpr = es.es_mr, EcModules.stmt s_wpr in let post = es_po es in @@ -254,14 +257,11 @@ let t_wp_r ?(uselet=true) k g = let t_wp ?(uselet=true) = FApi.t_low1 "wp" (t_wp_r ~uselet) (* -------------------------------------------------------------------- *) -let process_wp (cpos : pcodepos1 doption option) tc = +(* [process_wp gap]: splits the statement at [gap]; instructions before the + gap are kept, wp is applied to instructions after the gap. *) +let process_wp (cpos : pcodegap1 doption option) tc = let env = (FApi.tc1_env tc) in let cpos = - Option.map (EcTyping.trans_dcodepos1 env) cpos - in - let cpos = - Option.map (DOption.map (fun cp -> - EcMatching.Position.Notations.(cp +> 1) - )) cpos + Option.map (EcTyping.trans_dcodegap1 env) cpos in t_wp cpos tc diff --git a/src/phl/ecPhlWp.mli b/src/phl/ecPhlWp.mli index fc8689f6d2..c0017f5780 100644 --- a/src/phl/ecPhlWp.mli +++ b/src/phl/ecPhlWp.mli @@ -12,6 +12,6 @@ open EcCoreGoal.FApi * soundness of the bounded hoare logic. *) -val t_wp : ?uselet:bool -> (codepos1 doption) option -> backward +val t_wp : ?uselet:bool -> (codegap1 doption) option -> backward -val process_wp : (pcodepos1 doption) option -> backward +val process_wp : (pcodegap1 doption) option -> backward From 5e2b2ea6504da4a018f1a227ad20ab0160af5380 Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Wed, 25 Mar 2026 13:13:19 +0000 Subject: [PATCH 06/12] Fixed example --- examples/global-hybrid/GlobalHybridExamp2.ec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/global-hybrid/GlobalHybridExamp2.ec b/examples/global-hybrid/GlobalHybridExamp2.ec index db248c762c..89a74d3374 100644 --- a/examples/global-hybrid/GlobalHybridExamp2.ec +++ b/examples/global-hybrid/GlobalHybridExamp2.ec @@ -416,7 +416,7 @@ rcondf{1} 1; first auto. rcondf{2} 1; first auto; smt(). rcondt{2} 1; first auto. wp; inline*. -swap{2} 2 -1; swap{2} 6 -4; swap{2} 10 -7. +swap{2} 2 -1; swap{2} 6 -4. seq 2 3 : (#pre /\ x{1} = r0{2} /\ y{1} = r1{2} /\ x0{2} = A); first auto. From 5b090f5aff94bc7b9fce9ddb7a881d113af1e28a Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Wed, 25 Mar 2026 14:41:45 +0000 Subject: [PATCH 07/12] Fix position invalidation in unroll_for --- src/phl/ecPhlLoopTx.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml index 27b3b749a8..b8bf396d5e 100644 --- a/src/phl/ecPhlLoopTx.ml +++ b/src/phl/ecPhlLoopTx.ml @@ -362,7 +362,11 @@ let process_unroll_for ~cfold side cpos tc = let tcenv = FApi.t_onalli doi tcenv in if cfold then begin - let cpos = EcMatching.Position.Notations.(cpos <+| 1) in + (* Use normalized position: pos - 1 is the loop counter initialization + assignment that immediately precedes the while loop at pos. + We cannot reuse the original match-based cpos here because t_doit + has transformed the code, potentially invalidating the match. *) + let cpos = ([], EcMatching.Position.cpos1 (pos - 1)) in let clen = blen * (List.length zs - 1) in FApi.t_last (EcPhlCodeTx.t_cfold ~eager:false side cpos (Some clen)) tcenv From 4cc5733f8842dc37d99d8b8c5695676884a9e898 Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Wed, 25 Mar 2026 15:16:20 +0000 Subject: [PATCH 08/12] Restore WP behaviour for negative indices --- src/ecParser.mly | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/ecParser.mly b/src/ecParser.mly index 044d83664b..2aa646e117 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -2594,9 +2594,13 @@ codegap1_before: | i=codepos1 { GapBefore i } | g=codegap1 { g } -(* 0-indexed GapBefore: bare integer is 0-indexed gap number (e.g. seq) *) +(* 0-indexed gap: GapBefore for non-negative, GapAfter for negative + (negative indexes count from the end, so "in the direction of travel" + means GapAfter — e.g. wp -1 = gap after last instruction) *) codegap1_0before: -| i=codepos1_0 { GapBefore i } +| i=codepos1_0 { match snd i with + | `ByPos0 n when n < 0 -> GapAfter i + | _ -> GapBefore i } | g=codegap1 { g } (* Default-after: bare integer means gap after (e.g. wp, sp) *) From 5efabbdb30fd7c32e88dbe44f7e2489ce83ebcc3 Mon Sep 17 00:00:00 2001 From: Gustavo2622 Date: Wed, 25 Mar 2026 19:36:12 +0000 Subject: [PATCH 09/12] Removed codepos_range, ranges must be gaps --- src/ecCorePrinting.ml | 9 +- src/ecHiTacticals.ml | 8 +- src/ecLowPhlGoal.ml | 36 +++---- src/ecMatching.ml | 198 +++++++++++---------------------------- src/ecMatching.mli | 66 +++++-------- src/ecParser.mly | 24 ++--- src/ecParsetree.ml | 16 ++-- src/ecPrinting.ml | 23 +++-- src/ecTyping.ml | 18 +--- src/ecTyping.mli | 3 +- src/phl/ecPhlEager.ml | 13 +-- src/phl/ecPhlEager.mli | 4 +- src/phl/ecPhlEqobs.ml | 4 +- src/phl/ecPhlFel.ml | 2 +- src/phl/ecPhlOutline.mli | 2 +- src/phl/ecPhlRewrite.ml | 4 +- src/phl/ecPhlRnd.ml | 8 +- src/phl/ecPhlRnd.mli | 2 +- src/phl/ecPhlSeq.ml | 12 +-- src/phl/ecPhlSp.ml | 8 +- src/phl/ecPhlSwap.ml | 12 +-- src/phl/ecPhlSwap.mli | 2 +- src/phl/ecPhlWp.ml | 10 +- 23 files changed, 181 insertions(+), 303 deletions(-) diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml index 0b6fbc8198..dc89869590 100644 --- a/src/ecCorePrinting.ml +++ b/src/ecCorePrinting.ml @@ -74,10 +74,11 @@ module type PrinterAPI = sig 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 - val pp_codegap1 : PPEnv.t -> EcMatching.Position.codegap1 pp - val pp_codegap : PPEnv.t -> EcMatching.Position.codegap pp + val pp_codepos : PPEnv.t -> EcMatching.Position.codepos pp + val pp_codegap1 : PPEnv.t -> EcMatching.Position.codegap1 pp + val pp_codegap : PPEnv.t -> EcMatching.Position.codegap pp + val pp_codegap1_range : PPEnv.t -> EcMatching.Position.codegap1_range pp + val pp_codegap_range : PPEnv.t -> EcMatching.Position.codegap_range pp (* ------------------------------------------------------------------ *) type vsubst = [ diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index 86338c5af9..e749a0f03c 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -238,11 +238,15 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) = try tx tc with (* PHL Specific low errors *) - | EcLowPhlGoal.InvalidSplit cpos1 -> + | EcLowPhlGoal.InvalidSplit is -> tc_error_lazy !!tc (fun fmt -> let ppe = EcPrinting.PPEnv.ofenv (FApi.tc1_env tc) in Format.fprintf fmt "invalid split index: %a" - (EcPrinting.pp_codepos1 ppe) cpos1) + (fun fmt is -> match is with + | `Gap gap -> Format.fprintf fmt "%a" EcPrinting.(pp_codegap1 ppe) gap + | `Instr i -> Format.fprintf fmt "%a" EcPrinting.(pp_codepos1 ppe) i + ) is) + (* -------------------------------------------------------------------- *) and process_sub (ttenv : ttenv) tts tc = diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index 369897d01f..d15a0a5064 100644 --- a/src/ecLowPhlGoal.ml +++ b/src/ecLowPhlGoal.ml @@ -207,18 +207,18 @@ 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 tc1_process_codepos_or_range tc (side, cpor) = 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 + EcTyping.trans_codepos_or_range env cpor (* ------------------------------------------------------------------ *) -let tc1_process_codepos_range tc (side, cpr) = +let tc1_process_codegap_range tc (side, cgr) = 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_range env cpr + EcTyping.trans_codegap_range env cgr (* ------------------------------------------------------------------ *) let tc1_process_codepos tc (side, cpos) = @@ -373,37 +373,23 @@ let logicS_read (env : env) (f : logicS) = | `EHoare hs -> eHoareS_read env hs (* -------------------------------------------------------------------- *) -exception InvalidSplit of codepos1 +exception InvalidSplit of [ `Instr of codepos1 | `Gap of codegap1 ] + let s_split env i s = let module Pos = EcMatching.Position in - try Pos.split_at_cpos1 env i s - with Pos.InvalidCPos -> raise (InvalidSplit i) + try Pos.split_at_cgap1 env i s + with Pos.InvalidCPos -> raise (InvalidSplit (`Gap i)) let s_split_i env i s = let module Pos = EcMatching.Position in try Pos.find_by_cpos1 ~rev:false env i s - with Pos.InvalidCPos -> raise (InvalidSplit i) + with Pos.InvalidCPos -> raise (InvalidSplit (`Instr i)) let o_split ?rev env i s = let module Pos = EcMatching.Position in - try Pos.may_split_at_cpos1 ?rev env i s - with Pos.InvalidCPos -> raise (InvalidSplit (oget i)) - -(* Gap-based split functions *) -let s_split_at_gap env (g : codegap1) s = - let module Pos = EcMatching.Position in - try Pos.split_at_cgap1 env g s - with Pos.InvalidCPos -> - let cp = match g with GapBefore cp | GapAfter cp -> cp in - raise (InvalidSplit cp) - -let o_split_at_gap ?rev env (g : codegap1 option) s = - let module Pos = EcMatching.Position in - try Pos.may_split_at_cgap1 ?rev env g s - with Pos.InvalidCPos -> - let cp = match oget g with GapBefore cp | GapAfter cp -> cp in - raise (InvalidSplit cp) + try Pos.may_split_at_cgap1 ?rev env i s + with Pos.InvalidCPos -> raise (InvalidSplit (`Gap(oget i))) (* -------------------------------------------------------------------- *) (* Gap processing functions *) diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 034ca67d15..590b7cf9e3 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -85,14 +85,6 @@ module Position = struct 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 (* --- Gap types --- *) (* Normalized gap inside a block, 0-indexed, range [0, n] *) @@ -118,17 +110,36 @@ module Position = struct let cpos1 (i: int) : codepos1 = (0, `ByPos i) + let shift1 ~(offset : int) ((o, p) : codepos1) : codepos1 = + (o + offset, p) + + let shift ~(offset : int) ((outp, p) : codepos) : codepos = + (outp, shift1 ~offset p) + let cpos1_first : codepos1 = cpos1 0 let cpos1_last : codepos1 = cpos1 (-1) (* Boundary gap constructors *) let codegap1_start : codegap1 = GapBefore cpos1_first let codegap1_end : codegap1 = GapAfter cpos1_last + let codegap_start : codegap = ([], codegap1_start) + let codegap_end : codegap = ([], codegap1_end) (* Convenience constructors *) let gap_before_pos (cp : codepos1) : codegap1 = GapBefore cp let gap_after_pos (cp : codepos1) : codegap1 = GapAfter cp + (* Gap -> instr *) + let instr_before_gap (cg : codegap1) : codepos1 = + match cg with + | GapAfter cp -> cp + | GapBefore cp -> shift1 ~offset:(-1) cp + + let instr_after_gap (cg : codegap1) : codepos1 = + match cg with + | GapAfter cp -> shift1 ~offset:1 cp + | GapBefore cp -> cp + (* Position <-> Gap conversions (normalized, 0-indexed) *) let gap_before (pos : nm_codepos1) : nm_codegap1 = pos let gap_after (pos : nm_codepos1) : nm_codegap1 = pos + 1 @@ -143,33 +154,27 @@ module Position = struct (path, gap_range_of_pos pos) (* Gap counting helpers *) - let gap_after_n (n : int) : codegap1 = GapAfter (0, `ByPos n) - let gap_before_n (n : int) : codegap1 = GapBefore (0, `ByPos n) + let gap_after_n (n : int) : codegap1 = GapAfter (0, `ByPos (n-1)) + let gap_before_n (n : int) : codegap1 = GapBefore (0, `ByPos (n-1)) let gap_after_last_n (n : int) : codegap1 = GapAfter (0, `ByPos (-n)) let gap_before_last_n(n : int) : codegap1 = GapBefore (0, `ByPos (-n)) - let shift1 ~(offset : int) ((o, p) : codepos1) : codepos1 = - (o + offset, p) - - let shift ~(offset : int) ((outp, p) : codepos) : codepos = - (outp, shift1 ~offset p) - let resolve_offset ~(base : codepos1) ~(offset : codeoffset1) : codepos1 = match offset with | `Absolute pos -> pos | `Relative off -> (off + fst base, snd base) - let codepos1_range_of_codepos1 (cp1: codepos1) : codepos1_range = - (cp1, `Relative 1) + let codegap1_range_of_codepos1 (cp1: codepos1) : codegap1_range = + (gap_before_pos cp1, gap_after_pos cp1) - let codepos_range_of_codepos ((cpath, cp1): codepos) : codepos_range = - (cpath, codepos1_range_of_codepos1 cp1) + let codegap_range_of_codepos ((cpath, cp1): codepos) : codegap_range = + (cpath, codegap1_range_of_codepos1 cp1) - let nm_codepos1_range_of_nm_codepos1 (cp1: nm_codepos1) : nm_codepos1_range = - (cp1, cp1+1) + let nm_codegap1_range_of_nm_codepos1 (cp1: nm_codepos1) : nm_codegap1_range = + (gap_before cp1, gap_after cp1) - let nm_codepos_range_of_nm_codepos ((cpath, cp1): nm_codepos) : nm_codepos_range = - (cpath, nm_codepos1_range_of_nm_codepos1 cp1) + let nm_codepos_range_of_nm_codepos ((cpath, cp1): nm_codepos) : nm_codegap_range = + (cpath, nm_codegap1_range_of_nm_codepos1 cp1) let codepos1_of_nm_codepos1 (nm: nm_codepos1) : codepos1 = (0, `ByPos nm) @@ -208,12 +213,14 @@ module Position = struct 4. s2 <= e2 <= s1 <= e1 => true *) - let disjoint ((s1, e1): nm_codepos1_range) ((s2, e2): nm_codepos1_range) : bool = + let disjoint ((s1, e1): nm_codegap1_range) ((s2, e2): nm_codegap1_range) : bool = if s1 > e1 || s2 > e2 then raise InvalidCPos; - (s1 = e1) || (s2 = e2) || - (e1 < s2) || (e2 < s1) + (s1 = e1) || (s2 = e2) || (* Degenerate case where one of the reanges is empty *) + (max s1 s2 >= min e1 e2) (* Otherwise, intersection of (a, b) /\ (c, d) *) + (* = (max a c, min b d) *) + (* and this is empty if lower_lim >= upper_lim *) - let nm_codepos_in_nm_codepos_range (cp: nm_codepos1) ((start, fin): nm_codepos1_range) : bool = + let nm_codepos1_in_nm_codegap1_range (cp: nm_codepos1) ((start, fin): nm_codegap1_range) : bool = (start <= cp && cp < fin) module Notations = struct @@ -287,7 +294,13 @@ module Position = struct match rev with | false -> (s1, ir, s2) - | true -> (s2, ir, s1) + | true -> (List.rev s2, ir, List.rev s1) + + let exists_match (env: env) (cpm: cp_match) (s: stmt) : bool = + try + ignore (find_by_cp_match env (None, cpm) s); + true + with InvalidCPos -> false let find_by_nmcpos1 ?(rev = true) (nm: nm_codepos1) (s: stmt) = let s1, i, s2 = try @@ -375,104 +388,6 @@ module Position = struct 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 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 then raise InvalidCPos; - (start, fin) - - let normalize_cpos_range 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 env cp1r s in - (env, s), (npath, nm1r) - - (* - i is included in the second list since - intervals are closed-open [a,b[ - - Extremal cases (0-indexed): - - Splitting at 0 should get [], s - - Splitting at List.length should get s, [] - *) - let split_at_nmcpos1 ?(rev=false) (nm: nm_codepos1) (s: stmt) = - if nm = 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 [0;n[ to sub-block - [a; n[ by realigning to [0; n-a[ through (i |-> i - a) - *) - let fin = fin - start 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 - - let split_by_nmcpr1s (cps: nm_codepos1 list) (s: stmt) : instr list list = - 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 - - 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) - (* --- Gap normalization and split functions --- *) (* Check that a normalized gap is valid for the given statement *) @@ -568,10 +483,10 @@ module Position = struct (* [split_by_match env ~occ ~gap cm s] splits [s] at the gap before/after the [occ]-th occurrence of [cm]. *) let split_by_match (env : env) ~(occ : int) ~(gap : [`Before | `After]) (cm : cp_match) (s : stmt) = - let (s1, _i, s2) = find_by_cp_match env (Some occ, cm) s in + let (s1, i, s2) = find_by_cp_match env (Some occ, cm) s in match gap with - | `Before -> (s1, _i :: s2) - | `After -> (s1 @ [_i], s2) + | `Before -> (s1, i :: s2) + | `After -> (s1 @ [i], s2) let gap_before_match (env : env) ~(occ : int) (cm : cp_match) (s : stmt) : nm_codegap1 = let (s1, _, _) = find_by_cp_match env (Some occ, cm) s in @@ -671,8 +586,8 @@ module Zipper = struct 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 + let s1, s2 = split_at_nmcgap1 (gap_before nm) s in + let zpr = zipper ~env (List.rev s1) s2 zpr in (zpr, ((nmcp, nm), s)) @@ -685,11 +600,12 @@ module Zipper = struct 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 zipper_and_split_of_cgap_range (env: env) (path, (start, fin) : codegap_range) (s: stmt) : zipper * _ * nm_codegap_range = + let (zpr, ((cpath, _), s)) = zipper_of_cpos_r env (path, (instr_after_gap start)) s in + let start = normalize_cgap1 env start s in + let fin = normalize_cgap1 env fin s in + let ss = split_by_nmcgap_range (start, fin) s in + (zpr, ss, (cpath, (start, fin))) 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 @@ -722,18 +638,18 @@ module Zipper = struct in List.rev after - 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 fold_range (env: env) cenv (cpr: codegap_range) f state (s: stmt) = + let zpr, (_pre, s, tl), _nmcpr = zipper_and_split_of_cgap_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: env) (cpr: codepos_range) f (s: stmt) = + let map_range (env: env) (cpr: codegap_range) f (s: stmt) = snd (fold_range env () cpr (fun env () _ si -> (), f env si) () 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 (path, (cp1, `Relative 1)) f state s + fold_range env cenv (path, codegap1_range_of_codepos1 cp1) f state s let map env cpos f s = fst_map diff --git a/src/ecMatching.mli b/src/ecMatching.mli index fa544e3a48..be5eae5810 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -49,14 +49,6 @@ module Position : sig 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 @@ -74,16 +66,6 @@ module Position : sig 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 @@ -97,6 +79,8 @@ module Position : sig (* Normalization functions *) val find_by_cp_match : env -> (int option * cp_match) -> stmt -> instr list * instr * instr list + val exists_match : env -> cp_match -> stmt -> bool + val find_by_nmcpos1 : ?rev:bool -> nm_codepos1 -> stmt -> instr list * instr * instr list val check_nm_cpos1 : nm_codepos1 -> stmt -> unit @@ -107,8 +91,6 @@ module Position : sig 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 @@ -123,25 +105,6 @@ module Position : sig val normalize_cpos : env -> codepos -> stmt -> (env * stmt) * nm_codepos - val normalize_cpos1_range : env -> codepos1_range -> stmt -> nm_codepos1_range - - val normalize_cpos_range : 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 (* --- Gap types --- *) @@ -168,10 +131,14 @@ module Position : sig (* Boundary gap constructors *) val codegap1_start : codegap1 val codegap1_end : codegap1 + val codegap_start : codegap + val codegap_end : codegap (* Convenience constructors *) - val gap_before_pos : codepos1 -> codegap1 - val gap_after_pos : codepos1 -> codegap1 + val gap_before_pos : codepos1 -> codegap1 + val gap_after_pos : codepos1 -> codegap1 + val instr_before_gap : codegap1 -> codepos1 + val instr_after_gap : codegap1 -> codepos1 (* Position <-> Gap conversions (normalized, 0-indexed) *) val gap_before : nm_codepos1 -> nm_codegap1 @@ -226,6 +193,17 @@ module Position : sig (int -> nm_codegap1 -> nm_codegap1 -> 'a -> 'a) -> 'a -> 'a val iter_blocks : start:nm_codegap1 -> block_size:int -> stmt -> (int -> nm_codegap1 -> nm_codegap1 -> unit) -> unit + + (* Conversion between pos and gap for ranges *) + val codegap1_range_of_codepos1 : codepos1 -> codegap1_range + val codegap_range_of_codepos : codepos -> codegap_range + + val nm_codegap1_range_of_nm_codepos1 : nm_codepos1 -> nm_codegap1_range + val nm_codepos_range_of_nm_codepos : nm_codepos -> nm_codegap_range + + val disjoint : nm_codegap1_range -> nm_codegap1_range -> bool + + val nm_codepos1_in_nm_codegap1_range : nm_codepos1 -> nm_codegap1_range -> bool end (* -------------------------------------------------------------------- *) @@ -275,7 +253,7 @@ module Zipper : sig * Raise [InvalidCPos] if [codepos_range] is not a valid range for [stmt]. *) (* val zipper_of_cpos_range : env -> codepos_range -> stmt -> zipper * codepos1 *) - val zipper_and_split_of_cpos_range : env -> codepos_range -> stmt -> zipper * (instr list * instr list * instr list) * nm_codepos_range + val zipper_and_split_of_cgap_range : env -> codegap_range -> stmt -> zipper * (instr list * instr list * instr list) * nm_codegap_range (* Zip the zipper, returning the corresponding statement *) val zip : zipper -> stmt @@ -306,8 +284,8 @@ module Zipper : sig val map : env -> codepos -> (instr -> 'a * instr list) -> stmt -> 'a * stmt (* Variants of the above but using code position ranges *) - val fold_range : env -> 'a -> codepos_range -> ('a, 'state) folder_l -> 'state -> stmt -> 'state * stmt - val map_range : env -> codepos_range -> (env -> instr list -> instr list) -> stmt -> stmt + val fold_range : env -> 'a -> codegap_range -> ('a, 'state) folder_l -> 'state -> stmt -> 'state * stmt + val map_range : env -> codegap_range -> (env -> instr list -> instr list) -> stmt -> stmt end diff --git a/src/ecParser.mly b/src/ecParser.mly index 2aa646e117..5b6efd6a26 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -2625,13 +2625,13 @@ s_codegap1_0before: (* 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=loc(sword) RBRACKET { - if (unloc cpe) > 0 then - (cps, `Relative ((unloc cpe) + 1)) +%inline codegap1_range: +| LBRACKET cps=codepos1 DOTDOT cpe=codepos1 RBRACKET { (GapBefore cps, GapAfter cpe) } +| LBRACKET cps=codepos1 MINUS cpo=loc(sword) RBRACKET { + if (unloc cpo) > 0 then + (GapBefore cps, GapAfter (shift1 ~offset:(unloc cpo) cps)) else - parse_error (loc cpe) (Some "cannot give negative offset for codepos range end") + parse_error (loc cpo) (Some "cannot give negative offset for codepos range end") } %inline codepos_path: @@ -2641,15 +2641,15 @@ codepos: | path=codepos_path i=codepos1 { (path, i) } -codepos_range: -| r=codepos1_range +codegap_range: +| r=codegap1_range { ([], r) } -| path=rlist1(codepos_step, empty) COLON r=codepos1_range +| path=rlist1(codepos_step, empty) COLON r=codegap1_range { (path, r) } codepos_or_range: | cp=codepos { Pos cp } -| cpr=codepos_range { Range cpr } +| cpr=codegap_range { Range cpr } semrndpos1: | b=boption(STAR) c=codepos1 @@ -2903,7 +2903,7 @@ logtactic: { Pwlog (ids, b, f) } eager_tac: -| SEQ n1=codepos1 n2=codepos1 COLON s=stmt COLON p=form_or_double_form +| SEQ n1=codegap1_0before n2=codegap1_0before COLON s=stmt COLON p=form_or_double_form { Peager_seq ((n1, n2), s, p) } | IF @@ -3048,7 +3048,7 @@ interleave_info: | RND s=side? info=rnd_info c=prefix(COLON, semrndpos)? { Prnd (s, c, info) } -| RNDSEM red=boption(STAR) s=side? c=codepos1_0 +| RNDSEM red=boption(STAR) s=side? c=codegap1_0before { Prndsem (red, s, c) } | INLINE s=side? u=inlineopt? o=occurences? diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 7d9d33d55f..c3336aa190 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -73,13 +73,6 @@ type pcodeoffset1 = [ | `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 - (* Code gap types *) type pcodegap1 = | GapBefore of pcodepos1 @@ -94,6 +87,11 @@ type pcodegap = pcodepos_path * pcodegap1 type pcodegap1_range = pcodegap1 * pcodegap1 type pcodegap_range = pcodepos_path * pcodegap1_range +(* Code position ranges *) +type pcodepos_or_range = + | Pos of pcodepos + | Range of pcodegap_range + (* Gap-based offset for swap *) type pcodegap_offset1 = | PGapAbsolute of pcodegap1 @@ -804,7 +802,7 @@ type phltactic = | Pkill of (oside * pcodepos * int option) | Pasgncase of (oside * pcodepos) | Prnd of oside * psemrndpos option * rnd_tac_info_f - | Prndsem of bool * oside * pcodepos1 + | Prndsem of bool * oside * pcodegap1 | Palias of (oside * pcodepos * osymbol_r) | Pweakmem of (oside * psymbol * fun_params) | Pset of (oside * pcodepos * bool * psymbol * pexpr) @@ -834,7 +832,7 @@ type phltactic = | Phoaresplit (* Eager *) - | Peager_seq of (pcodepos1 pair * pstmt * pformula doption) + | Peager_seq of (pcodegap1 pair * pstmt * pformula doption) | Peager_if | Peager_while of pformula | Peager_fun_def diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 854e190e38..48dbdaeaf3 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -2441,14 +2441,6 @@ let pp_codepos_path ppe = 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 - (* -------------------------------------------------------------------- *) let pp_codegap1 (ppe : PPEnv.t) (fmt : Format.formatter) (g : CP.codegap1) = match g with @@ -2458,6 +2450,21 @@ let pp_codegap1 (ppe : PPEnv.t) (fmt : Format.formatter) (g : CP.codegap1) = let pp_codegap (ppe : PPEnv.t) (fmt : Format.formatter) ((cpath, g1) : CP.codegap) = Format.fprintf fmt "%a%a" (pp_codepos_path ppe) cpath (pp_codegap1 ppe) g1 +let symbol_and_codepos1_of_codegap1_range_edge (cg: CP.codegap1) : symbol * CP.codepos1 = + match cg with + | GapBefore cp -> "[", cp + | GapAfter cp -> "]", cp + +(* -------------------------------------------------------------------- *) +let pp_codegap1_range (ppe: PPEnv.t) (fmt: Format.formatter) ((start, fin) : CP.codegap1_range) = + let s, cps = symbol_and_codepos1_of_codegap1_range_edge start in + let e, cpe = symbol_and_codepos1_of_codegap1_range_edge fin in + Format.fprintf fmt "%s%a;%a%s" s (pp_codepos1 ppe) cps (pp_codepos1 ppe) cpe e + +(* FIXME: change when we can change the syntax *) +let pp_codegap_range (ppe: PPEnv.t) (fmt: Format.formatter) ((cpath, cp1r) : CP.codegap_range) = + Format.fprintf fmt "%a:[%a]" (pp_codepos_path ppe) cpath (pp_codegap1_range ppe) cp1r + (* -------------------------------------------------------------------- *) let pp_opdecl_pr (ppe : PPEnv.t) fmt ((basename, ts, ty, op): symbol * ty_param list * ty * prbody option) = let ppe = PPEnv.add_locals ppe ts in diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 7ea313cc95..7b9c639564 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -3766,22 +3766,10 @@ and trans_codeoffset1 ?(memory: memory option) (env : EcEnv.env) (o : pcodeoffse | `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) ((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 = +and trans_codepos_or_range ?(memory: memory option) (env : EcEnv.env) (cpor: pcodepos_or_range) : codegap_range = match cpor with - | Pos cp -> codepos_range_of_codepos (trans_codepos ?memory env cp) - | Range cpr -> trans_codepos_range ?memory env cpr + | Pos cp -> codegap_range_of_codepos (trans_codepos ?memory env cp) + | Range cpr -> trans_codegap_range ?memory env cpr (* -------------------------------------------------------------------- *) and trans_dcodepos1 ?(memory : memory option) (env : EcEnv.env) (p : pcodepos1 doption) : codepos1 doption = diff --git a/src/ecTyping.mli b/src/ecTyping.mli index 468a695f13..936c461aa0 100644 --- a/src/ecTyping.mli +++ b/src/ecTyping.mli @@ -239,8 +239,7 @@ type ismap = (instr list) EcMaps.Mstr.t 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_codepos_or_range : ?memory:EcMemory.memory -> env -> pcodepos_or_range -> codegap_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/ecPhlEager.ml b/src/phl/ecPhlEager.ml index 65d8efd3f2..87c4809eaa 100644 --- a/src/phl/ecPhlEager.ml +++ b/src/phl/ecPhlEager.ml @@ -69,8 +69,8 @@ let destruct_eager tc s = and ss = List.length s.s_node in let c, c' = (es.es_sl, es.es_sr) in - let z, c = s_split env EcMatching.Position.Notations.(cpos1_first +> ss) c - and c', z' = s_split env EcMatching.Position.Notations.(cpos1_after_last <+ ss) c' in + let z, c = s_split env (gap_after_n ss) c + and c', z' = s_split env (gap_before_last_n ss) c' in let env, _, _ = FApi.tc1_eflat tc in let z_eq_s = ER.EqTest.for_stmt env (stmt z) s @@ -96,10 +96,11 @@ let destruct_on_op id_op tc = let env = FApi.tc1_env tc and es = tc1_as_equivS tc in let s = try - (* FIXME CPOS PR: Add function to do these things *) - let s, _ = split_at_cpos1 env (0, `ByMatch (Some (-1), id_op)) es.es_sl + let s, _ = split_by_match env ~occ:(-1) ~gap:`Before id_op es.es_sl in (* ensure the right statement also contains an [id_op]: *) - and _, _ = split_at_cpos1 env (1, `ByMatch (None, id_op)) es.es_sr in + if not @@ exists_match env id_op es.es_sr then + tc_error_lazy !!tc (fun fmt -> + Format.fprintf fmt "eager: right side does not match operator"); s with InvalidCPos -> tc_error_lazy !!tc (fun fmt -> @@ -408,7 +409,7 @@ let t_eager_call = FApi.t_low2 "eager-call" t_eager_call_r let process_seq (i, j) s factor tc = let open BatTuple.Tuple2 in let indices = - mapn (tc1_process_codepos1 tc) ((Some `Left, i), (Some `Right, j)) + mapn (tc1_process_codegap1 tc) ((Some `Left, i), (Some `Right, j)) and factor = factor |> ( function Single p -> (p, p) | Double pp -> pp ) diff --git a/src/phl/ecPhlEager.mli b/src/phl/ecPhlEager.mli index 6d5c2b0580..0bb47604c8 100644 --- a/src/phl/ecPhlEager.mli +++ b/src/phl/ecPhlEager.mli @@ -5,7 +5,7 @@ open EcParsetree open EcCoreGoal.FApi open EcMatching.Position -val process_seq : pcodepos1 pair -> pstmt -> pformula doption -> backward +val process_seq : pcodegap1 pair -> pstmt -> pformula doption -> backward (** Tactic [eager seq] derives the following proof: {v (a) S; c₁ ~ c₁'; S : P ==> R₂ @@ -19,7 +19,7 @@ val process_seq : pcodepos1 pair -> pstmt -> pformula doption -> backward provided), as well as [S]. The predicate [={Q.1}] means equality on all free variables bound to the first memory in [Q]. *) -val t_eager_seq : codepos1 pair -> stmt -> ts_inv pair -> backward +val t_eager_seq : codegap1 pair -> stmt -> ts_inv pair -> backward (** Internal variant of [eager seq] *) val process_if : backward diff --git a/src/phl/ecPhlEqobs.ml b/src/phl/ecPhlEqobs.ml index 89b3031660..d7f9b0d1cd 100644 --- a/src/phl/ecPhlEqobs.ml +++ b/src/phl/ecPhlEqobs.ml @@ -471,8 +471,8 @@ let process_eqobs_inS info tc = (* sim positions are gaps: sim applies to instructions after the gap *) let p1 = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left , p1) in let p2 = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Right, p2) in - let _,sl2 = s_split_at_gap env p1 es.es_sl in - let _,sr2 = s_split_at_gap env p2 es.es_sr in + let _,sl2 = s_split env p1 es.es_sl in + let _,sr2 = s_split env p2 es.es_sr in 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/ecPhlFel.ml b/src/phl/ecPhlFel.ml index 24e6ee88ed..dfb9d2203b 100644 --- a/src/phl/ecPhlFel.ml +++ b/src/phl/ecPhlFel.ml @@ -135,7 +135,7 @@ let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc = with _ -> tc_error !!tc "not applicable to abstract functions" in - let s_hd, s_tl = EcLowPhlGoal.s_split_at_gap env at_pos fdef.f_body in + let s_hd, s_tl = EcLowPhlGoal.s_split env at_pos fdef.f_body in let fve = PV.fv env f_event.m f_event.inv in let fvc = PV.fv env cntr.m cntr.inv in let fvi = PV.fv env inv.m inv.inv in diff --git a/src/phl/ecPhlOutline.mli b/src/phl/ecPhlOutline.mli index d7ed5d99d8..cd00312531 100644 --- a/src/phl/ecPhlOutline.mli +++ b/src/phl/ecPhlOutline.mli @@ -17,6 +17,6 @@ type outline_variant = cpr: selects the particular slice of the program to outline. variant: choose the type of outlining: procedure or statement. *) -val t_outline : side -> codepos_range -> outline_variant -> backward +val t_outline : side -> codegap_range -> outline_variant -> backward val process_outline : outline_info -> backward diff --git a/src/phl/ecPhlRewrite.ml b/src/phl/ecPhlRewrite.ml index 3ffc034336..0f159d6737 100644 --- a/src/phl/ecPhlRewrite.ml +++ b/src/phl/ecPhlRewrite.ml @@ -271,7 +271,7 @@ let zpr_write (env : env) = - the original program-logic goal with the selected range rewritten. *) let t_change_stmt (side : side option) - (pos : EcMatching.Position.codepos_range) + (pos : EcMatching.Position.codegap_range) (s : stmt) (tc : tcenv1) = @@ -279,7 +279,7 @@ let t_change_stmt let me, stmt = EcLowPhlGoal.tc1_get_stmt side tc in let zpr, (_prelude,stmt, epilog), _nmr = - EcMatching.Zipper.zipper_and_split_of_cpos_range env pos stmt in + EcMatching.Zipper.zipper_and_split_of_cgap_range env pos stmt in (* Collect the variables that may be modified by the surrounding context, excluding the fragment being replaced. *) diff --git a/src/phl/ecPhlRnd.ml b/src/phl/ecPhlRnd.ml index 96ef8cb790..268c3d7311 100644 --- a/src/phl/ecPhlRnd.ml +++ b/src/phl/ecPhlRnd.ml @@ -598,7 +598,7 @@ let wp_equiv_rnd_r bij tc = subtc) (* -------------------------------------------------------------------- *) -let t_equiv_rnd_r side pos bij_info tc = +let t_equiv_rnd_r side (pos: (bool * codepos1) doption option) bij_info tc = match side, pos, bij_info with | Some side, None, (None, None) -> wp_equiv_disj_rnd_r side tc @@ -617,8 +617,8 @@ let t_equiv_rnd_r side pos bij_info tc = t_id tc | Some ((bl, il), (br, ir)) -> FApi.t_seq - (Core.t_equiv_rndsem_r bl `Left il) - (Core.t_equiv_rndsem_r br `Right ir) + (Core.t_equiv_rndsem_r bl `Left (gap_before_pos il)) + (Core.t_equiv_rndsem_r br `Right (gap_before_pos ir)) tc in let bij = @@ -717,7 +717,7 @@ let t_equiv_rndsem = FApi.t_low3 "equiv-rndsem" Core.t_equiv_rndsem_r (* -------------------------------------------------------------------- *) let process_rndsem ~reduce side pos tc = let concl = FApi.tc1_goal tc in - let pos = EcLowPhlGoal.tc1_process_codepos1 tc (side, pos) in + let pos = EcLowPhlGoal.tc1_process_codegap1 tc (side, pos) in match side with | None when is_hoareS concl -> diff --git a/src/phl/ecPhlRnd.mli b/src/phl/ecPhlRnd.mli index e636ac6d93..52483dd088 100644 --- a/src/phl/ecPhlRnd.mli +++ b/src/phl/ecPhlRnd.mli @@ -25,4 +25,4 @@ val t_equiv_rnd : ?pos:semrndpos -> oside -> (mkbij_t option) pair -> backward val process_rnd : oside -> psemrndpos option -> rnd_infos_t -> backward (* -------------------------------------------------------------------- *) -val process_rndsem : reduce:bool -> oside -> pcodepos1 -> backward +val process_rndsem : reduce:bool -> oside -> pcodegap1 -> backward diff --git a/src/phl/ecPhlSeq.ml b/src/phl/ecPhlSeq.ml index 05287d4bd4..0b14bf08e6 100644 --- a/src/phl/ecPhlSeq.ml +++ b/src/phl/ecPhlSeq.ml @@ -20,7 +20,7 @@ let t_hoare_seq_r i phi tc = let env = FApi.tc1_env tc in let hs = tc1_as_hoareS tc in let phi = ss_inv_rebind phi (fst hs.hs_m) in - let s1, s2 = s_split_at_gap env i hs.hs_s in + let s1, s2 = s_split env i hs.hs_s in 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 @@ -32,7 +32,7 @@ let t_hoare_seq = FApi.t_low2 "hoare-seq" t_hoare_seq_r let t_ehoare_seq_r i phi tc = let env = FApi.tc1_env tc in let hs = tc1_as_ehoareS tc in - let s1, s2 = s_split_at_gap env i hs.ehs_s in + let s1, s2 = s_split env i hs.ehs_s in let phi = ss_inv_rebind phi (fst hs.ehs_m) in let a = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) (stmt s1) phi in let b = f_eHoareS (snd hs.ehs_m) phi (stmt s2) (ehs_po hs) in @@ -51,7 +51,7 @@ let t_bdhoare_seq_r_low i (phi, pR, f1, f2, g1, g2) tc = let f2 = ss_inv_rebind f2 m in let g1 = ss_inv_rebind g1 m in let g2 = ss_inv_rebind g2 m in - let s1, s2 = s_split_at_gap env i bhs.bhs_s in + let s1, s2 = s_split env i bhs.bhs_s in let s1, s2 = stmt s1, stmt s2 in let nR = map_ss_inv1 f_not pR in let mt = snd bhs.bhs_m in @@ -122,8 +122,8 @@ let t_bdhoare_seq = FApi.t_low2 "bdhoare-seq" t_bdhoare_seq_r let t_equiv_seq (i, j) phi tc = let env = FApi.tc1_env tc in let es = tc1_as_equivS tc in - let sl1,sl2 = s_split_at_gap env i es.es_sl in - let sr1,sr2 = s_split_at_gap env j es.es_sr in + let sl1,sl2 = s_split env i es.es_sl in + let sr1,sr2 = s_split env j es.es_sr in let mtl, mtr = snd es.es_ml, snd es.es_mr in let a = f_equivS mtl mtr (es_pr es) (stmt sl1) (stmt sr1) phi in let b = f_equivS mtl mtr phi (stmt sl2) (stmt sr2) (es_po es) in @@ -150,7 +150,7 @@ let t_equiv_seq_onesided side i pre post tc = match side with | `Left -> (i, EcMatching.Position.codegap1_end) | `Right -> (EcMatching.Position.codegap1_end, i) in - let _s1, s2 = s_split_at_gap env i s in + let _s1, s2 = s_split env i s in let modi = EcPV.s_write env (EcModules.stmt s2) in let r = map_ts_inv2 f_and p' (generalize_mod_side env modi (map_ts_inv2 f_imp q' (es_po es))) in diff --git a/src/phl/ecPhlSp.ml b/src/phl/ecPhlSp.ml index f3abed6535..3eae4f7c74 100644 --- a/src/phl/ecPhlSp.ml +++ b/src/phl/ecPhlSp.ml @@ -242,7 +242,7 @@ let t_sp_side pos tc = match concl.f_node, pos with | FhoareS hs, (None | Some (Single _)) -> let pos = pos |> omap as_single in - let stmt1, stmt2 = o_split_at_gap ~rev:true env pos hs.hs_s in + let stmt1, stmt2 = o_split ~rev:true env pos hs.hs_s in let stmt1, hs_pr = LI.sp_stmt hs.hs_m env stmt1 (hs_pr hs).inv in check_sp_progress pos stmt1; let m = fst hs.hs_m in @@ -258,7 +258,7 @@ let t_sp_side pos tc = | FbdHoareS bhs, (None | Some (Single _)) -> let pos = pos |> omap as_single in - let stmt1, stmt2 = o_split_at_gap ~rev:true env pos bhs.bhs_s in + let stmt1, stmt2 = o_split ~rev:true env pos bhs.bhs_s in check_form_indep stmt1 bhs.bhs_m (bhs_bd bhs).inv; let stmt1, bhs_pr = LI.sp_stmt bhs.bhs_m env stmt1 (bhs_pr bhs).inv in check_sp_progress pos stmt1; @@ -271,8 +271,8 @@ let t_sp_side pos tc = let posL = pos |> omap fst in let posR = pos |> omap snd in - let stmtL1, stmtL2 = o_split_at_gap ~rev:true env posL es.es_sl in - let stmtR1, stmtR2 = o_split_at_gap ~rev:true env posR es.es_sr in + let stmtL1, stmtL2 = o_split ~rev:true env posL es.es_sl in + let stmtR1, stmtR2 = o_split ~rev:true env posR es.es_sr in let es_pr = (es_pr es) in let ml, mr = fst es.es_ml, fst es.es_mr in diff --git a/src/phl/ecPhlSwap.ml b/src/phl/ecPhlSwap.ml index 462163c244..30bdbe4c75 100644 --- a/src/phl/ecPhlSwap.ml +++ b/src/phl/ecPhlSwap.ml @@ -12,7 +12,7 @@ open EcLowGoal (* -------------------------------------------------------------------- *) type swap_kind = { - interval : codepos_range; + interval : codegap_range; offset : codegap_offset1; } @@ -71,11 +71,11 @@ module LowInternal = struct = let (env, s), (_, (start, fin)) = try let (cpath, (start, fin)) = info.interval in - normalize_cpos_range env (cpath, (start, fin)) s + normalize_cgap_range env (cpath, (start, fin)) s with InvalidCPos -> tc_error_lazy pf (fun fmt -> let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt "invalid range: %a" (EcPrinting.pp_codepos_range ppe) info.interval + Format.fprintf fmt "invalid range: %a" (EcPrinting.pp_codegap_range ppe) info.interval ) in @@ -85,7 +85,7 @@ module LowInternal = struct tc_error pf "invalid offset for swap" in - match split_by_nmcpr1s + match split_by_nmcgaps (if target <= start then [target; start; fin] else [start; fin; target] @@ -130,7 +130,7 @@ let rec process_swap1 (info : (oside * pswap_kind) located) (tc : tcenv1) = let interval = match interval, offset with | Some interval, _ -> interval | None, GapRelative i -> - codepos_range_of_codepos + codegap_range_of_codepos (if i > 0 then cpos_first else cpos_last) | None, _ -> tc_error (!!tc) "Cannot give a absolute offset and no range" @@ -166,7 +166,7 @@ let process_interleave info tc = let p1 = (0, `ByPos pos2) in let p2 = (0, `ByPos (pos2+n2)) in let o = PGapRelative ((pos1+n1) - pos2) in - { interval = Some (Range ([], (p1, `Absolute p2))); offset = o; } in + { interval = Some (Range ([], (GapBefore p1, GapBefore p2))); offset = o; } in FApi.t_seq (process_swap1 (mk_loc loc (side, data))) (aux (pos1+n1+n2) (pos2+n2) (k-1)) diff --git a/src/phl/ecPhlSwap.mli b/src/phl/ecPhlSwap.mli index b58c6c3956..fc920cea79 100644 --- a/src/phl/ecPhlSwap.mli +++ b/src/phl/ecPhlSwap.mli @@ -6,7 +6,7 @@ open EcCoreGoal.FApi (* -------------------------------------------------------------------- *) type swap_kind = { - interval : codepos_range; + interval : codegap_range; offset : codegap_offset1; } diff --git a/src/phl/ecPhlWp.ml b/src/phl/ecPhlWp.ml index 74a529345d..18085f7061 100644 --- a/src/phl/ecPhlWp.ml +++ b/src/phl/ecPhlWp.ml @@ -170,7 +170,7 @@ module TacInternal = struct let hyps = FApi.tc1_hyps tc in let env = EcEnv.LDecl.toenv hyps in let hs = tc1_as_hoareS tc in - let (s_hd, s_wp) = o_split_at_gap env i hs.hs_s in + let (s_hd, s_wp) = o_split env i hs.hs_s in let s_wp = EcModules.stmt s_wp in let { exnmap = (eposts, d) } as post = (hs_po hs).hsi_inv in let s_wp, post = wp ~uselet ~onesided:true hyps hs.hs_m s_wp post in @@ -184,7 +184,7 @@ module TacInternal = struct let t_ehoare_wp ?(uselet=true) (i : codegap1 option) tc = let env = FApi.tc1_env tc in let hs = tc1_as_ehoareS tc in - let (s_hd, s_wp) = o_split_at_gap env i hs.ehs_s in + let (s_hd, s_wp) = o_split env i hs.ehs_s in let s_wp = EcModules.stmt s_wp in let (s_wp, post) = ewp ~uselet env hs.ehs_m s_wp (ehs_po hs).inv in check_wp_progress tc i hs.ehs_s s_wp; @@ -197,7 +197,7 @@ module TacInternal = struct let hyps = FApi.tc1_hyps tc in let env = EcEnv.LDecl.toenv hyps in let bhs = tc1_as_bdhoareS tc in - let (s_hd, s_wp) = o_split_at_gap env i bhs.bhs_s in + let (s_hd, s_wp) = o_split env i bhs.bhs_s in let s_wp = EcModules.stmt s_wp in let s_wp, post = wp ~uselet hyps bhs.bhs_m s_wp (POE.empty (bhs_po bhs).inv) @@ -214,8 +214,8 @@ module TacInternal = struct let es = tc1_as_equivS tc in let ml, mr = (fst es.es_ml), (fst es.es_mr) in let i = omap fst ij and j = omap snd ij in - let s_hdl,s_wpl = o_split_at_gap env i es.es_sl in - let s_hdr,s_wpr = o_split_at_gap env j es.es_sr in + let s_hdl,s_wpl = o_split env i es.es_sl in + let s_hdr,s_wpr = o_split env j es.es_sr in let meml, s_wpl = es.es_ml, EcModules.stmt s_wpl in let memr, s_wpr = es.es_mr, EcModules.stmt s_wpr in let post = es_po es in From ca6051f9db29735f2a81838947807c12acd7efa3 Mon Sep 17 00:00:00 2001 From: Gustavo2622 Date: Wed, 25 Mar 2026 21:58:03 +0000 Subject: [PATCH 10/12] Fixed for examples --- src/ecMatching.ml | 2 +- src/ecMatching.mli | 2 +- src/ecParser.mly | 8 +++++--- 3 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 590b7cf9e3..5b731009e5 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -173,7 +173,7 @@ module Position = struct let nm_codegap1_range_of_nm_codepos1 (cp1: nm_codepos1) : nm_codegap1_range = (gap_before cp1, gap_after cp1) - let nm_codepos_range_of_nm_codepos ((cpath, cp1): nm_codepos) : nm_codegap_range = + let nm_codegap_range_of_nm_codepos ((cpath, cp1): nm_codepos) : nm_codegap_range = (cpath, nm_codegap1_range_of_nm_codepos1 cp1) let codepos1_of_nm_codepos1 (nm: nm_codepos1) : codepos1 = diff --git a/src/ecMatching.mli b/src/ecMatching.mli index be5eae5810..c6d9fdd366 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -199,7 +199,7 @@ module Position : sig val codegap_range_of_codepos : codepos -> codegap_range val nm_codegap1_range_of_nm_codepos1 : nm_codepos1 -> nm_codegap1_range - val nm_codepos_range_of_nm_codepos : nm_codepos -> nm_codegap_range + val nm_codegap_range_of_nm_codepos : nm_codepos -> nm_codegap_range val disjoint : nm_codegap1_range -> nm_codegap1_range -> bool diff --git a/src/ecParser.mly b/src/ecParser.mly index 5b6efd6a26..324477a307 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -2594,13 +2594,15 @@ codegap1_before: | i=codepos1 { GapBefore i } | g=codegap1 { g } +(* FIXME: decide on semantic before merge *) (* 0-indexed gap: GapBefore for non-negative, GapAfter for negative (negative indexes count from the end, so "in the direction of travel" - means GapAfter — e.g. wp -1 = gap after last instruction) *) + means GapAfter — e.g. wp -1 = gap after last instruction) *) codegap1_0before: -| i=codepos1_0 { match snd i with +| i=codepos1_0 { GapBefore i } + (* { match snd i with | `ByPos0 n when n < 0 -> GapAfter i - | _ -> GapBefore i } + | _ -> GapBefore i } *) | g=codegap1 { g } (* Default-after: bare integer means gap after (e.g. wp, sp) *) From 7b03bccd2efbcfaee96130ec74a3482a4ac8ce63 Mon Sep 17 00:00:00 2001 From: Gustavo2622 Date: Wed, 25 Mar 2026 22:46:19 +0000 Subject: [PATCH 11/12] Dont check intermediate codepos when normalizing gaps --- src/ecMatching.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 5b731009e5..0450a3f669 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -397,8 +397,8 @@ module Position = struct (* Normalize a codegap1 to nm_codegap1 *) let normalize_cgap1 (env : env) (g : codegap1) (s : stmt) : nm_codegap1 = let nm = match g with - | GapBefore cp -> normalize_cpos1 env cp s |> gap_before - | GapAfter cp -> normalize_cpos1 env cp s |> gap_after + | GapBefore cp -> normalize_cpos1 ~check:false env cp s |> gap_before + | GapAfter cp -> normalize_cpos1 ~check:false env cp s |> gap_after in check_nm_cgap1 nm s; nm From ed9fa49728c8d871771e120578cf1d63d812a8dc Mon Sep 17 00:00:00 2001 From: Gustavo2622 Date: Wed, 25 Mar 2026 23:27:55 +0000 Subject: [PATCH 12/12] Tighten checks when normalizing codepositions --- src/ecMatching.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 0450a3f669..30e6448780 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -311,7 +311,7 @@ module Position = struct (* Throws InvalidCPos if failing — allows [0, n] where n is "after last" *) let check_nm_cpos1 (nm: nm_codepos1) (s: stmt) : unit = - if nm < 0 || nm > List.length s.s_node then raise InvalidCPos + if nm < 0 || nm >= List.length s.s_node then raise InvalidCPos (* Normalizes code position wrt stmt — input is 0-indexed *) let normalize_cp_base ?(check = true) (env: EcEnv.env) (cb: cp_base) (s: stmt) : nm_codepos1 =