From 3808ca8bd513371d481fca16601ecde5a77d1c7e Mon Sep 17 00:00:00 2001 From: Cameron Low Date: Wed, 19 Feb 2025 11:12:19 +0000 Subject: [PATCH] [internal] Introduce general code position ranges for selecting code blocks. --- src/ecMatching.ml | 49 ++++++++++++++++++++++++++++------------------ src/ecMatching.mli | 18 +++++++++++++---- src/ecTyping.ml | 9 ++++++--- 3 files changed, 50 insertions(+), 26 deletions(-) diff --git a/src/ecMatching.ml b/src/ecMatching.ml index abed6f427..8de810498 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -35,6 +35,7 @@ module Position = struct 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] let shift1 ~(offset : int) ((o, p) : codepos1) : codepos1 = @@ -60,8 +61,8 @@ module Zipper = struct type ('a, 'state) folder = env -> 'a -> 'state -> instr -> 'state * instr list - type ('a, 'state) folder_tl = - env -> 'a -> 'state -> instr -> instr list -> '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; @@ -249,6 +250,17 @@ module Zipper = struct 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 = zipper_of_cpos env top s in + match bot with + | `Base cp -> + let path = (zipper_of_cpos env cp s).z_path in + if path <> zpr.z_path then + raise InvalidCPos; + zpr, snd cp + | `Offset cp1 -> zpr, cp1 + let split_at_cpos1 env cpos1 s = split_at_cpos1 ~after:`Auto env cpos1 s @@ -288,23 +300,22 @@ module Zipper = struct in List.rev after - let fold_tl env cenv cpos f state s = - let zpr = zipper_of_cpos env cpos s in - - match zpr.z_tail with - | [] -> raise InvalidCPos - | i :: tl -> begin - match f (odfl env zpr.z_env) cenv state i tl with - | (state', [i']) when i == i' && state == state' -> (state, s) - | (state', si ) -> (state', zip { zpr with z_tail = si }) - end - - let fold env cenv cpos f state s = - let f e ce st i tl = - let state', si = f e ce st i in - state', si @ tl - in - fold_tl env cenv cpos f state s + let fold_range env cenv cpr f state 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 env cp (stmt tl) in + let env = odfl env zpr.z_env in + let state', si' = f env cenv state (i :: s) in + state', zip { zpr with z_tail = si' @ tl } + + let map_range env cpr f s = + snd (fold_range env () cpr (fun env () _ si -> (), f env si) () s) + + let fold env cenv cp f state s = + 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 let map env cpos f s = fst_map diff --git a/src/ecMatching.mli b/src/ecMatching.mli index 5b1961cc5..552f6f531 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -31,6 +31,7 @@ module Position : sig 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] val shift1 : offset:int -> codepos1 -> codepos1 @@ -92,6 +93,13 @@ module Zipper : sig val zipper_of_cpos_r : env -> codepos -> stmt -> zipper * codepos val zipper_of_cpos : env -> codepos -> stmt -> zipper + (* Return the zipper for the stmt [stmt] from the start of the code position + * range [codepos_range]. It also returns a code position relative to + * 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 + (* Zip the zipper, returning the corresponding statement *) val zip : zipper -> stmt @@ -104,7 +112,7 @@ module Zipper : sig val after : strict:bool -> zipper -> instr list list type ('a, 'state) folder = env -> 'a -> 'state -> instr -> 'state * instr list - type ('a, 'state) folder_tl = env -> 'a -> 'state -> instr -> instr list -> 'state * instr list + type ('a, 'state) folder_l = env -> 'a -> 'state -> instr list -> 'state * instr list (* [fold env v cpos f state s] create the zipper for [s] at [cpos], and apply * [f] to it, along with [v] and the state [state]. [f] must return the @@ -115,14 +123,16 @@ module Zipper : sig *) val fold : env -> 'a -> codepos -> ('a, 'state) folder -> 'state -> stmt -> 'state * stmt - (* Same as above but using [folder_tl]. *) - val fold_tl : env -> 'a -> codepos -> ('a, 'state) folder_tl -> 'state -> stmt -> 'state * stmt - (* [map cpos env f s] is a special case of [fold] where the state and the * out-of-band data are absent *) 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 + + end (* -------------------------------------------------------------------- *) diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 686b08c61..1a978db85 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -2194,7 +2194,11 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) = List.fold_right (fun (cp, up) bd -> let {pl_desc = cp; pl_loc = loc} = cp in let cp = trans_codepos env cp in - let change env _ _ i tl = (), + let change env si = + (* NOTE: There will always be a head element *) + let i, tl = List.takedrop 1 si in + let i = List.hd i in + match up with | Pup_stmt sup -> eval_supdate env sup i @ tl @@ -2203,8 +2207,7 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) = in let env = EcEnv.Memory.push_active !memenv env in try - let _, s = EcMatching.Zipper.fold_tl env () cp change () bd in - s + EcMatching.Zipper.map_range env (cp, `Offset (EcMatching.Zipper.cpos (-1))) change bd with | EcMatching.Zipper.InvalidCPos -> tyerror loc env (InvalidModUpdate MUE_InvalidCodePos);