From ef3111086ebebd83beb464858635501e9e50e3a6 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 19 Dec 2024 14:12:32 +0100 Subject: [PATCH 1/4] Stable bundle names. --- engine/lib/concrete_ident/concrete_ident.mli | 1 + engine/lib/dependencies.ml | 6 +++++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/engine/lib/concrete_ident/concrete_ident.mli b/engine/lib/concrete_ident/concrete_ident.mli index e87f71b22..687a50c31 100644 --- a/engine/lib/concrete_ident/concrete_ident.mli +++ b/engine/lib/concrete_ident/concrete_ident.mli @@ -27,6 +27,7 @@ val eq_name : name -> t -> bool val to_debug_string : t -> string module Create : sig + val parent : t -> t val fresh_module : from:t list -> t val move_under : new_parent:t -> t -> t diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml index 6637e60c8..ea0b897ef 100644 --- a/engine/lib/dependencies.ml +++ b/engine/lib/dependencies.ml @@ -413,8 +413,12 @@ module Make (F : Features.T) = struct in let transform (bundle : item list) = + let module_names = + List.map ~f:(ident_of >> Concrete_ident.Create.parent) bundle + |> List.dedup_and_sort ~compare:Concrete_ident.compare + in let ns : Concrete_ident.t = - Concrete_ident.Create.fresh_module ~from:(List.map ~f:ident_of bundle) + Concrete_ident.Create.fresh_module ~from:module_names in let new_name_under_ns : Concrete_ident.t -> Concrete_ident.t = Concrete_ident.Create.move_under ~new_parent:ns From b7a9e3404fa0132244ac12417ba58b046b5a1817 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 19 Dec 2024 14:25:40 +0100 Subject: [PATCH 2/4] Add real disambiguator instead of modifying string to resolve name clashes in bundles. --- engine/lib/concrete_ident/concrete_ident.ml | 8 ++++++++ engine/lib/concrete_ident/concrete_ident.mli | 4 ++++ engine/lib/dependencies.ml | 5 +---- 3 files changed, 13 insertions(+), 4 deletions(-) diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml index b0d0cc160..3d6627f60 100644 --- a/engine/lib/concrete_ident/concrete_ident.ml +++ b/engine/lib/concrete_ident/concrete_ident.ml @@ -635,6 +635,14 @@ module Create = struct let constructor name = let path = name.def_id.path @ [ { data = Ctor; disambiguator = 0 } ] in { name with def_id = { name.def_id with path } } + + let add_disambiguator name disambiguator = + let path = name.def_id.path in + let last = List.last_exn path in + let path = + List.drop_last_exn path @ [ { data = last.data; disambiguator } ] + in + { name with def_id = { name.def_id with path } } end let lookup_raw_impl_info (impl : t) : Types.impl_infos option = diff --git a/engine/lib/concrete_ident/concrete_ident.mli b/engine/lib/concrete_ident/concrete_ident.mli index 687a50c31..545a23da3 100644 --- a/engine/lib/concrete_ident/concrete_ident.mli +++ b/engine/lib/concrete_ident/concrete_ident.mli @@ -38,6 +38,10 @@ module Create : sig val map_last : f:(string -> string) -> t -> t (** [map_last f ident] applies [f] on the last chunk of [ident]'s path if it holds a string *) + + val add_disambiguator : t -> int -> t + (** [add_disambiguator ident d] changes the disambiguator on + the last chunk of [ident]'s path to [d] *) end type view = { crate : string; path : string list; definition : string } diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml index ea0b897ef..72819746b 100644 --- a/engine/lib/dependencies.ml +++ b/engine/lib/dependencies.ml @@ -435,10 +435,7 @@ module Make (F : Features.T) = struct (List.mem duplicates (new_name_under_ns id) ~equal:Concrete_ident.equal) then id - else - Concrete_ident.Create.map_last - ~f:(fun name -> name ^ (Concrete_ident.hash id |> Int.to_string)) - id + else Concrete_ident.Create.add_disambiguator id (Concrete_ident.hash id) in let renamings = List.map From bbbfe4cbedcdd8b24ce393c379243de6f317c050 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Mon, 23 Dec 2024 16:36:49 +0100 Subject: [PATCH 3/4] Avoid exception when taking parent of module to create rec bundle. --- engine/lib/concrete_ident/concrete_ident.ml | 5 +- .../toolchain__cyclic-modules into-fstar.snap | 230 +++++++++--------- 2 files changed, 117 insertions(+), 118 deletions(-) diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml index 3d6627f60..fb8be0b19 100644 --- a/engine/lib/concrete_ident/concrete_ident.ml +++ b/engine/lib/concrete_ident/concrete_ident.ml @@ -596,14 +596,13 @@ module Create = struct let len x = List.length x.def_id.path in let compare x y = len x - len y in let id = List.min_elt ~compare from |> Option.value_exn in - let parent = parent id in { kind = Kind.Value; def_id = { - parent.def_id with + id.def_id with path = - parent.def_id.path + id.def_id.path @ [ { data = TypeNs "rec_bundle"; diff --git a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap index af07fc045..b19c9d7d9 100644 --- a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap @@ -32,7 +32,7 @@ module Cyclic_modules.B open Core open FStar.Mul -include Cyclic_modules.Rec_bundle_318256792 {g as g} +include Cyclic_modules.Rec_bundle_367033742 {g as g} ''' "Cyclic_modules.C.fst" = ''' module Cyclic_modules.C @@ -42,8 +42,8 @@ open FStar.Mul let i (_: Prims.unit) : Prims.unit = () ''' -"Cyclic_modules.D.Rec_bundle_773034964.fst" = ''' -module Cyclic_modules.D.Rec_bundle_773034964 +"Cyclic_modules.D.Rec_bundle_81544935.fst" = ''' +module Cyclic_modules.D.Rec_bundle_81544935 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -62,9 +62,9 @@ module Cyclic_modules.D open Core open FStar.Mul -include Cyclic_modules.D.Rec_bundle_773034964 {d1 as d1} +include Cyclic_modules.D.Rec_bundle_81544935 {d1 as d1} -include Cyclic_modules.D.Rec_bundle_773034964 {d2 as d2} +include Cyclic_modules.D.Rec_bundle_81544935 {d2 as d2} ''' "Cyclic_modules.De.fst" = ''' module Cyclic_modules.De @@ -72,10 +72,10 @@ module Cyclic_modules.De open Core open FStar.Mul -include Cyclic_modules.D.Rec_bundle_773034964 {de1 as de1} +include Cyclic_modules.D.Rec_bundle_81544935 {de1 as de1} ''' -"Cyclic_modules.Disjoint_cycle_a.Rec_bundle_317759688.fst" = ''' -module Cyclic_modules.Disjoint_cycle_a.Rec_bundle_317759688 +"Cyclic_modules.Disjoint_cycle_a.Rec_bundle_177270903.fst" = ''' +module Cyclic_modules.Disjoint_cycle_a.Rec_bundle_177270903 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -94,9 +94,9 @@ module Cyclic_modules.Disjoint_cycle_a open Core open FStar.Mul -include Cyclic_modules.Disjoint_cycle_a.Rec_bundle_317759688 {g as g} +include Cyclic_modules.Disjoint_cycle_a.Rec_bundle_177270903 {g as g} -include Cyclic_modules.Disjoint_cycle_a.Rec_bundle_317759688 {f as f} +include Cyclic_modules.Disjoint_cycle_a.Rec_bundle_177270903 {f as f} ''' "Cyclic_modules.Disjoint_cycle_b.fst" = ''' module Cyclic_modules.Disjoint_cycle_b @@ -104,9 +104,9 @@ module Cyclic_modules.Disjoint_cycle_b open Core open FStar.Mul -include Cyclic_modules.Disjoint_cycle_a.Rec_bundle_317759688 {h as h} +include Cyclic_modules.Disjoint_cycle_a.Rec_bundle_177270903 {h as h} -include Cyclic_modules.Disjoint_cycle_a.Rec_bundle_317759688 {i as i} +include Cyclic_modules.Disjoint_cycle_a.Rec_bundle_177270903 {i as i} ''' "Cyclic_modules.E.fst" = ''' module Cyclic_modules.E @@ -114,47 +114,47 @@ module Cyclic_modules.E open Core open FStar.Mul -include Cyclic_modules.D.Rec_bundle_773034964 {e1 as e1} +include Cyclic_modules.D.Rec_bundle_81544935 {e1 as e1} ''' -"Cyclic_modules.Enums_a.fst" = ''' -module Cyclic_modules.Enums_a +"Cyclic_modules.Enums_a.Rec_bundle_1009707801.fst" = ''' +module Cyclic_modules.Enums_a.Rec_bundle_1009707801 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {t_T240131830 as t_T} +type t_T_366415196 = + | T_366415196_A : t_T_366415196 + | T_366415196_B : t_T_366415196 + | T_366415196_C : Alloc.Vec.t_Vec t_T_240131830 Alloc.Alloc.t_Global -> t_T_366415196 -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T240131830_A as T_A} - -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T240131830_B as T_B} +and t_U = + | U_A : t_U + | U_B : t_U + | U_C : Alloc.Vec.t_Vec t_T_240131830 Alloc.Alloc.t_Global -> t_U -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T240131830_C as T_C} +and t_T_240131830 = + | T_240131830_A : t_T_240131830 + | T_240131830_B : t_T_240131830 + | T_240131830_C : Alloc.Vec.t_Vec t_U Alloc.Alloc.t_Global -> t_T_240131830 + | T_240131830_D : Alloc.Vec.t_Vec t_T_366415196 Alloc.Alloc.t_Global -> t_T_240131830 -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T240131830_D as T_D} +let f (_: Prims.unit) : t_T_366415196 = T_366415196_A <: t_T_366415196 ''' -"Cyclic_modules.Enums_b.Rec_bundle_994866580.fst" = ''' -module Cyclic_modules.Enums_b.Rec_bundle_994866580 +"Cyclic_modules.Enums_a.fst" = ''' +module Cyclic_modules.Enums_a #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul -type t_T366415196 = - | T366415196_A : t_T366415196 - | T366415196_B : t_T366415196 - | T366415196_C : Alloc.Vec.t_Vec t_T240131830 Alloc.Alloc.t_Global -> t_T366415196 +include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {t_T_240131830 as t_T} -and t_U = - | U_A : t_U - | U_B : t_U - | U_C : Alloc.Vec.t_Vec t_T240131830 Alloc.Alloc.t_Global -> t_U +include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {T_240131830_A as T_A} -and t_T240131830 = - | T240131830_A : t_T240131830 - | T240131830_B : t_T240131830 - | T240131830_C : Alloc.Vec.t_Vec t_U Alloc.Alloc.t_Global -> t_T240131830 - | T240131830_D : Alloc.Vec.t_Vec t_T366415196 Alloc.Alloc.t_Global -> t_T240131830 +include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {T_240131830_B as T_B} -let f (_: Prims.unit) : t_T366415196 = T366415196_A <: t_T366415196 +include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {T_240131830_C as T_C} + +include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {T_240131830_D as T_D} ''' "Cyclic_modules.Enums_b.fst" = ''' module Cyclic_modules.Enums_b @@ -162,42 +162,42 @@ module Cyclic_modules.Enums_b open Core open FStar.Mul -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {t_T366415196 as t_T} +include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {t_T_366415196 as t_T} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T366415196_A as T_A} +include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {T_366415196_A as T_A} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T366415196_B as T_B} +include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {T_366415196_B as T_B} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T366415196_C as T_C} +include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {T_366415196_C as T_C} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {t_U as t_U} +include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {t_U as t_U} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {U_A as U_A} +include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {U_A as U_A} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {U_B as U_B} +include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {U_B as U_B} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {U_C as U_C} +include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {U_C as U_C} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {f as f} +include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {f as f} ''' -"Cyclic_modules.Late_skip_a.fst" = ''' -module Cyclic_modules.Late_skip_a +"Cyclic_modules.Late_skip_a.Rec_bundle_658016071.fst" = ''' +module Cyclic_modules.Late_skip_a.Rec_bundle_658016071 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul -include Cyclic_modules.Late_skip_b.Rec_bundle_447022631 {f749016415 as f} +let rec ff_749016415 (_: Prims.unit) : Prims.unit = ff_377825240 () + +and ff_377825240 (_: Prims.unit) : Prims.Pure Prims.unit (requires true) (fun _ -> Prims.l_True) = + ff_749016415 () ''' -"Cyclic_modules.Late_skip_b.Rec_bundle_447022631.fst" = ''' -module Cyclic_modules.Late_skip_b.Rec_bundle_447022631 +"Cyclic_modules.Late_skip_a.fst" = ''' +module Cyclic_modules.Late_skip_a #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul -let rec f749016415 (_: Prims.unit) : Prims.unit = f377825240 () - -and f377825240 (_: Prims.unit) : Prims.Pure Prims.unit (requires true) (fun _ -> Prims.l_True) = - f749016415 () +include Cyclic_modules.Late_skip_a.Rec_bundle_658016071 {ff_749016415 as f} ''' "Cyclic_modules.Late_skip_b.fst" = ''' module Cyclic_modules.Late_skip_b @@ -205,18 +205,10 @@ module Cyclic_modules.Late_skip_b open Core open FStar.Mul -include Cyclic_modules.Late_skip_b.Rec_bundle_447022631 {f377825240 as f} +include Cyclic_modules.Late_skip_a.Rec_bundle_658016071 {ff_377825240 as f} ''' -"Cyclic_modules.M1.fst" = ''' -module Cyclic_modules.M1 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" -open Core -open FStar.Mul - -include Cyclic_modules.M2.Rec_bundle_489499412 {a as a} -''' -"Cyclic_modules.M2.Rec_bundle_489499412.fst" = ''' -module Cyclic_modules.M2.Rec_bundle_489499412 +"Cyclic_modules.M1.Rec_bundle_892895908.fst" = ''' +module Cyclic_modules.M1.Rec_bundle_892895908 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -231,17 +223,25 @@ let b (_: Prims.unit) : Prims.unit = let _:Prims.unit = a () in d () ''' +"Cyclic_modules.M1.fst" = ''' +module Cyclic_modules.M1 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.M1.Rec_bundle_892895908 {a as a} +''' "Cyclic_modules.M2.fst" = ''' module Cyclic_modules.M2 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul -include Cyclic_modules.M2.Rec_bundle_489499412 {c as c} +include Cyclic_modules.M1.Rec_bundle_892895908 {c as c} -include Cyclic_modules.M2.Rec_bundle_489499412 {d as d} +include Cyclic_modules.M1.Rec_bundle_892895908 {d as d} -include Cyclic_modules.M2.Rec_bundle_489499412 {b as b} +include Cyclic_modules.M1.Rec_bundle_892895908 {b as b} ''' "Cyclic_modules.Rec.fst" = ''' module Cyclic_modules.Rec @@ -273,15 +273,15 @@ and g2 (x: t_T) : t_T = | T_t1 -> g1 x | T_t2 -> hf x ''' -"Cyclic_modules.Rec1_same_name.Rec_bundle_213192514.fst" = ''' -module Cyclic_modules.Rec1_same_name.Rec_bundle_213192514 +"Cyclic_modules.Rec1_same_name.Rec_bundle_563905053.fst" = ''' +module Cyclic_modules.Rec1_same_name.Rec_bundle_563905053 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul -let rec f533409751 (x: i32) : i32 = f91805216 x +let rec ff_533409751 (x: i32) : i32 = ff_91805216 x -and f91805216 (x: i32) : i32 = if x >. 0l then f533409751 (x -! 1l <: i32) else 0l +and ff_91805216 (x: i32) : i32 = if x >. 0l then ff_533409751 (x -! 1l <: i32) else 0l ''' "Cyclic_modules.Rec1_same_name.fst" = ''' module Cyclic_modules.Rec1_same_name @@ -289,7 +289,7 @@ module Cyclic_modules.Rec1_same_name open Core open FStar.Mul -include Cyclic_modules.Rec1_same_name.Rec_bundle_213192514 {f533409751 as f} +include Cyclic_modules.Rec1_same_name.Rec_bundle_563905053 {ff_533409751 as f} ''' "Cyclic_modules.Rec2_same_name.fst" = ''' module Cyclic_modules.Rec2_same_name @@ -297,10 +297,10 @@ module Cyclic_modules.Rec2_same_name open Core open FStar.Mul -include Cyclic_modules.Rec1_same_name.Rec_bundle_213192514 {f91805216 as f} +include Cyclic_modules.Rec1_same_name.Rec_bundle_563905053 {ff_91805216 as f} ''' -"Cyclic_modules.Rec_bundle_318256792.fst" = ''' -module Cyclic_modules.Rec_bundle_318256792 +"Cyclic_modules.Rec_bundle_367033742.fst" = ''' +module Cyclic_modules.Rec_bundle_367033742 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -315,24 +315,8 @@ let h (_: Prims.unit) : Prims.unit = let h2 (_: Prims.unit) : Prims.unit = Cyclic_modules.C.i () ''' -"Cyclic_modules.Typ_a.fst" = ''' -module Cyclic_modules.Typ_a -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" -open Core -open FStar.Mul - -include Cyclic_modules.Typ_b.Rec_bundle_546955701 {t_T as t_T} - -include Cyclic_modules.Typ_b.Rec_bundle_546955701 {T_T as T_T} - -include Cyclic_modules.Typ_b.Rec_bundle_546955701 {t_TRec as t_TRec} - -include Cyclic_modules.Typ_b.Rec_bundle_546955701 {TRec_T as TRec_T} - -include Cyclic_modules.Typ_b.Rec_bundle_546955701 {TRec_Empty as TRec_Empty} -''' -"Cyclic_modules.Typ_b.Rec_bundle_546955701.fst" = ''' -module Cyclic_modules.Typ_b.Rec_bundle_546955701 +"Cyclic_modules.Typ_a.Rec_bundle_830459646.fst" = ''' +module Cyclic_modules.Typ_a.Rec_bundle_830459646 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -353,32 +337,48 @@ and t_T1Rec = | T1Rec_T1 : Alloc.Boxed.t_Box t_T2Rec Alloc.Alloc.t_Global -> t_T and t_T2Rec = | T2Rec_T2 : t_TRec -> t_T2Rec ''' +"Cyclic_modules.Typ_a.fst" = ''' +module Cyclic_modules.Typ_a +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.Typ_a.Rec_bundle_830459646 {t_T as t_T} + +include Cyclic_modules.Typ_a.Rec_bundle_830459646 {T_T as T_T} + +include Cyclic_modules.Typ_a.Rec_bundle_830459646 {t_TRec as t_TRec} + +include Cyclic_modules.Typ_a.Rec_bundle_830459646 {TRec_T as TRec_T} + +include Cyclic_modules.Typ_a.Rec_bundle_830459646 {TRec_Empty as TRec_Empty} +''' "Cyclic_modules.Typ_b.fst" = ''' module Cyclic_modules.Typ_b #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul -include Cyclic_modules.Typ_b.Rec_bundle_546955701 {t_T1 as t_T1} +include Cyclic_modules.Typ_a.Rec_bundle_830459646 {t_T1 as t_T1} -include Cyclic_modules.Typ_b.Rec_bundle_546955701 {T1_T1 as T1_T1} +include Cyclic_modules.Typ_a.Rec_bundle_830459646 {T1_T1 as T1_T1} -include Cyclic_modules.Typ_b.Rec_bundle_546955701 {t_T1_cast_to_repr as t_T1_cast_to_repr} +include Cyclic_modules.Typ_a.Rec_bundle_830459646 {t_T1_cast_to_repr as t_T1_cast_to_repr} -include Cyclic_modules.Typ_b.Rec_bundle_546955701 {t_T2 as t_T2} +include Cyclic_modules.Typ_a.Rec_bundle_830459646 {t_T2 as t_T2} -include Cyclic_modules.Typ_b.Rec_bundle_546955701 {T2_T2 as T2_T2} +include Cyclic_modules.Typ_a.Rec_bundle_830459646 {T2_T2 as T2_T2} -include Cyclic_modules.Typ_b.Rec_bundle_546955701 {t_T1Rec as t_T1Rec} +include Cyclic_modules.Typ_a.Rec_bundle_830459646 {t_T1Rec as t_T1Rec} -include Cyclic_modules.Typ_b.Rec_bundle_546955701 {T1Rec_T1 as T1Rec_T1} +include Cyclic_modules.Typ_a.Rec_bundle_830459646 {T1Rec_T1 as T1Rec_T1} -include Cyclic_modules.Typ_b.Rec_bundle_546955701 {t_T2Rec as t_T2Rec} +include Cyclic_modules.Typ_a.Rec_bundle_830459646 {t_T2Rec as t_T2Rec} -include Cyclic_modules.Typ_b.Rec_bundle_546955701 {T2Rec_T2 as T2Rec_T2} +include Cyclic_modules.Typ_a.Rec_bundle_830459646 {T2Rec_T2 as T2Rec_T2} ''' -"Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539.fst" = ''' -module Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 +"Cyclic_modules.Variant_constructor_a.Rec_bundle_748213522.fst" = ''' +module Cyclic_modules.Variant_constructor_a.Rec_bundle_748213522 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -400,15 +400,15 @@ module Cyclic_modules.Variant_constructor_a open Core open FStar.Mul -include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {t_Context as t_Context} +include Cyclic_modules.Variant_constructor_a.Rec_bundle_748213522 {t_Context as t_Context} -include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {Context_A as Context_A} +include Cyclic_modules.Variant_constructor_a.Rec_bundle_748213522 {Context_A as Context_A} -include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {Context_B as Context_B} +include Cyclic_modules.Variant_constructor_a.Rec_bundle_748213522 {Context_B as Context_B} -include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {test as impl__Context__test} +include Cyclic_modules.Variant_constructor_a.Rec_bundle_748213522 {test as impl__Context__test} -include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {f as f} +include Cyclic_modules.Variant_constructor_a.Rec_bundle_748213522 {f as f} ''' "Cyclic_modules.Variant_constructor_b.fst" = ''' module Cyclic_modules.Variant_constructor_b @@ -416,7 +416,7 @@ module Cyclic_modules.Variant_constructor_b open Core open FStar.Mul -include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {h as h} +include Cyclic_modules.Variant_constructor_a.Rec_bundle_748213522 {h as h} ''' "Cyclic_modules.fst" = ''' module Cyclic_modules @@ -424,9 +424,9 @@ module Cyclic_modules open Core open FStar.Mul -include Cyclic_modules.Rec_bundle_318256792 {f as f} +include Cyclic_modules.Rec_bundle_367033742 {f as f} -include Cyclic_modules.Rec_bundle_318256792 {h as h} +include Cyclic_modules.Rec_bundle_367033742 {h as h} -include Cyclic_modules.Rec_bundle_318256792 {h2 as h2} +include Cyclic_modules.Rec_bundle_367033742 {h2 as h2} ''' From 254990dcb2d80d48c184246681aeb2ceccd867d6 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 24 Dec 2024 12:25:50 +0100 Subject: [PATCH 4/4] Rename rec_bundle as cyclic_bundle. --- engine/lib/concrete_ident/concrete_ident.ml | 15 +- .../toolchain__cyclic-modules into-fstar.snap | 172 +++++++++--------- 2 files changed, 95 insertions(+), 92 deletions(-) diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml index fb8be0b19..75505210d 100644 --- a/engine/lib/concrete_ident/concrete_ident.ml +++ b/engine/lib/concrete_ident/concrete_ident.ml @@ -605,7 +605,7 @@ module Create = struct id.def_id.path @ [ { - data = TypeNs "rec_bundle"; + data = TypeNs "cyclic_bundle"; disambiguator = [%hash: t list] from; }; ]; @@ -637,11 +637,14 @@ module Create = struct let add_disambiguator name disambiguator = let path = name.def_id.path in - let last = List.last_exn path in - let path = - List.drop_last_exn path @ [ { data = last.data; disambiguator } ] - in - { name with def_id = { name.def_id with path } } + if List.is_empty path then name + else + (* The following two `exn` function calls cannot fail as the path is not empty. *) + let last = List.last_exn path in + let path = + List.drop_last_exn path @ [ { data = last.data; disambiguator } ] + in + { name with def_id = { name.def_id with path } } end let lookup_raw_impl_info (impl : t) : Types.impl_infos option = diff --git a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap index b19c9d7d9..1cb9dc501 100644 --- a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap @@ -32,7 +32,7 @@ module Cyclic_modules.B open Core open FStar.Mul -include Cyclic_modules.Rec_bundle_367033742 {g as g} +include Cyclic_modules.Cyclic_bundle_367033742 {g as g} ''' "Cyclic_modules.C.fst" = ''' module Cyclic_modules.C @@ -42,8 +42,24 @@ open FStar.Mul let i (_: Prims.unit) : Prims.unit = () ''' -"Cyclic_modules.D.Rec_bundle_81544935.fst" = ''' -module Cyclic_modules.D.Rec_bundle_81544935 +"Cyclic_modules.Cyclic_bundle_367033742.fst" = ''' +module Cyclic_modules.Cyclic_bundle_367033742 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +let f (_: Prims.unit) : Prims.unit = () + +let g (_: Prims.unit) : Prims.unit = f () + +let h (_: Prims.unit) : Prims.unit = + let _:Prims.unit = g () in + Cyclic_modules.C.i () + +let h2 (_: Prims.unit) : Prims.unit = Cyclic_modules.C.i () +''' +"Cyclic_modules.D.Cyclic_bundle_81544935.fst" = ''' +module Cyclic_modules.D.Cyclic_bundle_81544935 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -62,9 +78,9 @@ module Cyclic_modules.D open Core open FStar.Mul -include Cyclic_modules.D.Rec_bundle_81544935 {d1 as d1} +include Cyclic_modules.D.Cyclic_bundle_81544935 {d1 as d1} -include Cyclic_modules.D.Rec_bundle_81544935 {d2 as d2} +include Cyclic_modules.D.Cyclic_bundle_81544935 {d2 as d2} ''' "Cyclic_modules.De.fst" = ''' module Cyclic_modules.De @@ -72,10 +88,10 @@ module Cyclic_modules.De open Core open FStar.Mul -include Cyclic_modules.D.Rec_bundle_81544935 {de1 as de1} +include Cyclic_modules.D.Cyclic_bundle_81544935 {de1 as de1} ''' -"Cyclic_modules.Disjoint_cycle_a.Rec_bundle_177270903.fst" = ''' -module Cyclic_modules.Disjoint_cycle_a.Rec_bundle_177270903 +"Cyclic_modules.Disjoint_cycle_a.Cyclic_bundle_177270903.fst" = ''' +module Cyclic_modules.Disjoint_cycle_a.Cyclic_bundle_177270903 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -94,9 +110,9 @@ module Cyclic_modules.Disjoint_cycle_a open Core open FStar.Mul -include Cyclic_modules.Disjoint_cycle_a.Rec_bundle_177270903 {g as g} +include Cyclic_modules.Disjoint_cycle_a.Cyclic_bundle_177270903 {g as g} -include Cyclic_modules.Disjoint_cycle_a.Rec_bundle_177270903 {f as f} +include Cyclic_modules.Disjoint_cycle_a.Cyclic_bundle_177270903 {f as f} ''' "Cyclic_modules.Disjoint_cycle_b.fst" = ''' module Cyclic_modules.Disjoint_cycle_b @@ -104,9 +120,9 @@ module Cyclic_modules.Disjoint_cycle_b open Core open FStar.Mul -include Cyclic_modules.Disjoint_cycle_a.Rec_bundle_177270903 {h as h} +include Cyclic_modules.Disjoint_cycle_a.Cyclic_bundle_177270903 {h as h} -include Cyclic_modules.Disjoint_cycle_a.Rec_bundle_177270903 {i as i} +include Cyclic_modules.Disjoint_cycle_a.Cyclic_bundle_177270903 {i as i} ''' "Cyclic_modules.E.fst" = ''' module Cyclic_modules.E @@ -114,10 +130,10 @@ module Cyclic_modules.E open Core open FStar.Mul -include Cyclic_modules.D.Rec_bundle_81544935 {e1 as e1} +include Cyclic_modules.D.Cyclic_bundle_81544935 {e1 as e1} ''' -"Cyclic_modules.Enums_a.Rec_bundle_1009707801.fst" = ''' -module Cyclic_modules.Enums_a.Rec_bundle_1009707801 +"Cyclic_modules.Enums_a.Cyclic_bundle_1009707801.fst" = ''' +module Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -146,15 +162,15 @@ module Cyclic_modules.Enums_a open Core open FStar.Mul -include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {t_T_240131830 as t_T} +include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {t_T_240131830 as t_T} -include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {T_240131830_A as T_A} +include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_240131830_A as T_A} -include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {T_240131830_B as T_B} +include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_240131830_B as T_B} -include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {T_240131830_C as T_C} +include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_240131830_C as T_C} -include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {T_240131830_D as T_D} +include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_240131830_D as T_D} ''' "Cyclic_modules.Enums_b.fst" = ''' module Cyclic_modules.Enums_b @@ -162,26 +178,26 @@ module Cyclic_modules.Enums_b open Core open FStar.Mul -include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {t_T_366415196 as t_T} +include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {t_T_366415196 as t_T} -include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {T_366415196_A as T_A} +include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_366415196_A as T_A} -include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {T_366415196_B as T_B} +include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_366415196_B as T_B} -include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {T_366415196_C as T_C} +include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_366415196_C as T_C} -include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {t_U as t_U} +include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {t_U as t_U} -include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {U_A as U_A} +include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {U_A as U_A} -include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {U_B as U_B} +include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {U_B as U_B} -include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {U_C as U_C} +include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {U_C as U_C} -include Cyclic_modules.Enums_a.Rec_bundle_1009707801 {f as f} +include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {f as f} ''' -"Cyclic_modules.Late_skip_a.Rec_bundle_658016071.fst" = ''' -module Cyclic_modules.Late_skip_a.Rec_bundle_658016071 +"Cyclic_modules.Late_skip_a.Cyclic_bundle_658016071.fst" = ''' +module Cyclic_modules.Late_skip_a.Cyclic_bundle_658016071 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -197,7 +213,7 @@ module Cyclic_modules.Late_skip_a open Core open FStar.Mul -include Cyclic_modules.Late_skip_a.Rec_bundle_658016071 {ff_749016415 as f} +include Cyclic_modules.Late_skip_a.Cyclic_bundle_658016071 {ff_749016415 as f} ''' "Cyclic_modules.Late_skip_b.fst" = ''' module Cyclic_modules.Late_skip_b @@ -205,10 +221,10 @@ module Cyclic_modules.Late_skip_b open Core open FStar.Mul -include Cyclic_modules.Late_skip_a.Rec_bundle_658016071 {ff_377825240 as f} +include Cyclic_modules.Late_skip_a.Cyclic_bundle_658016071 {ff_377825240 as f} ''' -"Cyclic_modules.M1.Rec_bundle_892895908.fst" = ''' -module Cyclic_modules.M1.Rec_bundle_892895908 +"Cyclic_modules.M1.Cyclic_bundle_892895908.fst" = ''' +module Cyclic_modules.M1.Cyclic_bundle_892895908 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -229,7 +245,7 @@ module Cyclic_modules.M1 open Core open FStar.Mul -include Cyclic_modules.M1.Rec_bundle_892895908 {a as a} +include Cyclic_modules.M1.Cyclic_bundle_892895908 {a as a} ''' "Cyclic_modules.M2.fst" = ''' module Cyclic_modules.M2 @@ -237,11 +253,11 @@ module Cyclic_modules.M2 open Core open FStar.Mul -include Cyclic_modules.M1.Rec_bundle_892895908 {c as c} +include Cyclic_modules.M1.Cyclic_bundle_892895908 {c as c} -include Cyclic_modules.M1.Rec_bundle_892895908 {d as d} +include Cyclic_modules.M1.Cyclic_bundle_892895908 {d as d} -include Cyclic_modules.M1.Rec_bundle_892895908 {b as b} +include Cyclic_modules.M1.Cyclic_bundle_892895908 {b as b} ''' "Cyclic_modules.Rec.fst" = ''' module Cyclic_modules.Rec @@ -273,8 +289,8 @@ and g2 (x: t_T) : t_T = | T_t1 -> g1 x | T_t2 -> hf x ''' -"Cyclic_modules.Rec1_same_name.Rec_bundle_563905053.fst" = ''' -module Cyclic_modules.Rec1_same_name.Rec_bundle_563905053 +"Cyclic_modules.Rec1_same_name.Cyclic_bundle_563905053.fst" = ''' +module Cyclic_modules.Rec1_same_name.Cyclic_bundle_563905053 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -289,7 +305,7 @@ module Cyclic_modules.Rec1_same_name open Core open FStar.Mul -include Cyclic_modules.Rec1_same_name.Rec_bundle_563905053 {ff_533409751 as f} +include Cyclic_modules.Rec1_same_name.Cyclic_bundle_563905053 {ff_533409751 as f} ''' "Cyclic_modules.Rec2_same_name.fst" = ''' module Cyclic_modules.Rec2_same_name @@ -297,26 +313,10 @@ module Cyclic_modules.Rec2_same_name open Core open FStar.Mul -include Cyclic_modules.Rec1_same_name.Rec_bundle_563905053 {ff_91805216 as f} -''' -"Cyclic_modules.Rec_bundle_367033742.fst" = ''' -module Cyclic_modules.Rec_bundle_367033742 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" -open Core -open FStar.Mul - -let f (_: Prims.unit) : Prims.unit = () - -let g (_: Prims.unit) : Prims.unit = f () - -let h (_: Prims.unit) : Prims.unit = - let _:Prims.unit = g () in - Cyclic_modules.C.i () - -let h2 (_: Prims.unit) : Prims.unit = Cyclic_modules.C.i () +include Cyclic_modules.Rec1_same_name.Cyclic_bundle_563905053 {ff_91805216 as f} ''' -"Cyclic_modules.Typ_a.Rec_bundle_830459646.fst" = ''' -module Cyclic_modules.Typ_a.Rec_bundle_830459646 +"Cyclic_modules.Typ_a.Cyclic_bundle_830459646.fst" = ''' +module Cyclic_modules.Typ_a.Cyclic_bundle_830459646 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -343,15 +343,15 @@ module Cyclic_modules.Typ_a open Core open FStar.Mul -include Cyclic_modules.Typ_a.Rec_bundle_830459646 {t_T as t_T} +include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_T as t_T} -include Cyclic_modules.Typ_a.Rec_bundle_830459646 {T_T as T_T} +include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {T_T as T_T} -include Cyclic_modules.Typ_a.Rec_bundle_830459646 {t_TRec as t_TRec} +include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_TRec as t_TRec} -include Cyclic_modules.Typ_a.Rec_bundle_830459646 {TRec_T as TRec_T} +include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {TRec_T as TRec_T} -include Cyclic_modules.Typ_a.Rec_bundle_830459646 {TRec_Empty as TRec_Empty} +include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {TRec_Empty as TRec_Empty} ''' "Cyclic_modules.Typ_b.fst" = ''' module Cyclic_modules.Typ_b @@ -359,26 +359,26 @@ module Cyclic_modules.Typ_b open Core open FStar.Mul -include Cyclic_modules.Typ_a.Rec_bundle_830459646 {t_T1 as t_T1} +include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_T1 as t_T1} -include Cyclic_modules.Typ_a.Rec_bundle_830459646 {T1_T1 as T1_T1} +include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {T1_T1 as T1_T1} -include Cyclic_modules.Typ_a.Rec_bundle_830459646 {t_T1_cast_to_repr as t_T1_cast_to_repr} +include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_T1_cast_to_repr as t_T1_cast_to_repr} -include Cyclic_modules.Typ_a.Rec_bundle_830459646 {t_T2 as t_T2} +include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_T2 as t_T2} -include Cyclic_modules.Typ_a.Rec_bundle_830459646 {T2_T2 as T2_T2} +include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {T2_T2 as T2_T2} -include Cyclic_modules.Typ_a.Rec_bundle_830459646 {t_T1Rec as t_T1Rec} +include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_T1Rec as t_T1Rec} -include Cyclic_modules.Typ_a.Rec_bundle_830459646 {T1Rec_T1 as T1Rec_T1} +include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {T1Rec_T1 as T1Rec_T1} -include Cyclic_modules.Typ_a.Rec_bundle_830459646 {t_T2Rec as t_T2Rec} +include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_T2Rec as t_T2Rec} -include Cyclic_modules.Typ_a.Rec_bundle_830459646 {T2Rec_T2 as T2Rec_T2} +include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {T2Rec_T2 as T2Rec_T2} ''' -"Cyclic_modules.Variant_constructor_a.Rec_bundle_748213522.fst" = ''' -module Cyclic_modules.Variant_constructor_a.Rec_bundle_748213522 +"Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522.fst" = ''' +module Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -400,15 +400,15 @@ module Cyclic_modules.Variant_constructor_a open Core open FStar.Mul -include Cyclic_modules.Variant_constructor_a.Rec_bundle_748213522 {t_Context as t_Context} +include Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522 {t_Context as t_Context} -include Cyclic_modules.Variant_constructor_a.Rec_bundle_748213522 {Context_A as Context_A} +include Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522 {Context_A as Context_A} -include Cyclic_modules.Variant_constructor_a.Rec_bundle_748213522 {Context_B as Context_B} +include Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522 {Context_B as Context_B} -include Cyclic_modules.Variant_constructor_a.Rec_bundle_748213522 {test as impl__Context__test} +include Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522 {test as impl__Context__test} -include Cyclic_modules.Variant_constructor_a.Rec_bundle_748213522 {f as f} +include Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522 {f as f} ''' "Cyclic_modules.Variant_constructor_b.fst" = ''' module Cyclic_modules.Variant_constructor_b @@ -416,7 +416,7 @@ module Cyclic_modules.Variant_constructor_b open Core open FStar.Mul -include Cyclic_modules.Variant_constructor_a.Rec_bundle_748213522 {h as h} +include Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522 {h as h} ''' "Cyclic_modules.fst" = ''' module Cyclic_modules @@ -424,9 +424,9 @@ module Cyclic_modules open Core open FStar.Mul -include Cyclic_modules.Rec_bundle_367033742 {f as f} +include Cyclic_modules.Cyclic_bundle_367033742 {f as f} -include Cyclic_modules.Rec_bundle_367033742 {h as h} +include Cyclic_modules.Cyclic_bundle_367033742 {h as h} -include Cyclic_modules.Rec_bundle_367033742 {h2 as h2} +include Cyclic_modules.Cyclic_bundle_367033742 {h2 as h2} '''