Skip to content

Refactor code positions #945

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
Gustavo2622 wants to merge 2 commits into
base: main
Choose a base branch
from
+770 −387
Draft

Refactor code positions #945

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
17ecd15
WIP: refactoring code positions, interleave is assert false'd
Gustavo2622 Mar 20, 2026
d231b78
More fixes interleave still broken
Gustavo2622 Mar 20, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 8 additions & 4 deletions src/ecCorePrinting.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 = [
Expand Down
29 changes: 18 additions & 11 deletions src/ecLowPhlGoal.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -334,19 +341,19 @@ let push_memenvs_pre (hyps : LDecl.hyps) (f : form) =
exception InvalidSplit of codepos1

let s_split env i s =
let module Zpr = EcMatching.Zipper in
try Zpr.split_at_cpos1 env i s
with Zpr.InvalidCPos -> raise (InvalidSplit i)
let module Pos = EcMatching.Position in
try Pos.split_at_cpos1 env i s
with Pos.InvalidCPos -> raise (InvalidSplit i)

let s_split_i env i s =
let module Zpr = EcMatching.Zipper in
try Zpr.find_by_cpos1 ~rev:false env i s
with Zpr.InvalidCPos -> raise (InvalidSplit i)
let module Pos = EcMatching.Position in
try Pos.find_by_cpos1 ~rev:false env i s
with Pos.InvalidCPos -> raise (InvalidSplit i)

let o_split ?rev env i s =
let module Zpr = EcMatching.Zipper in
try Zpr.may_split_at_cpos1 ?rev env i s
with Zpr.InvalidCPos -> raise (InvalidSplit (oget i))
let module Pos = EcMatching.Position in
try Pos.may_split_at_cpos1 ?rev env i s
with Pos.InvalidCPos -> raise (InvalidSplit (oget i))

(* -------------------------------------------------------------------- *)
let t_hS_or_bhS_or_eS ?th ?teh ?tbh ?te tc =
Expand Down Expand Up @@ -692,14 +699,14 @@ let t_fold f (cenv : code_txenv) (cpos : codepos) (_ : form * form) (state, s) =
let env = EcEnv.LDecl.toenv (snd cenv) in
let (me, f) = Zpr.fold env cenv cpos (fun _ -> f) state s in
((me, f, []) : memenv * _ * form list)
with Zpr.InvalidCPos -> tc_error (fst cenv) "invalid code position"
with InvalidCPos -> tc_error (fst cenv) "invalid code position"

let t_zip f (cenv : code_txenv) (cpos : codepos) (prpo : form * form) (state, s) =
try
let env = EcEnv.LDecl.toenv (snd cenv) in
let (me, zpr, gs) = f cenv prpo state (Zpr.zipper_of_cpos env cpos s) in
((me, Zpr.zip zpr, gs) : memenv * _ * form list)
with Zpr.InvalidCPos -> tc_error (fst cenv) "invalid code position"
with InvalidCPos -> tc_error (fst cenv) "invalid code position"

let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc =
let pf = FApi.tc1_penv tc in
Expand Down
Loading
Loading