Merge pull request #1049 from hacspec/fix-1021

fix(engine) Move variant constructors in recursive bundling.

engine/lib/concrete_ident/concrete_ident.ml

@@ -630,6 +630,10 @@ module Create = struct
     in
     let path = List.drop_last_exn old.def_id.path @ [ last ] in
     { old with def_id = { old.def_id with path } }
+
+  let constructor name =
+    let path = name.def_id.path @ [ { data = Ctor; disambiguator = 0 } ] in
+    { name with def_id = { name.def_id with path } }
 end
 
 let lookup_raw_impl_info (impl : t) : Types.impl_infos option =

engine/lib/concrete_ident/concrete_ident.mli

@@ -30,6 +30,10 @@ module Create : sig
   val fresh_module : from:t list -> t
   val move_under : new_parent:t -> t -> t
 
+  val constructor : t -> t
+  (** [constructor ident] adds a [Ctor] to [ident]
+      this allows to build a constructor from a variant name. *)
+
   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 *)

engine/lib/dependencies.ml

@@ -450,11 +450,19 @@ module Make (F : Features.T) = struct
                     )))
         | _ -> []
       in
-
+      let variant_and_constructors_renamings =
+        List.concat_map ~f:variants_renamings renamings
+        |> List.concat_map ~f:(fun (old_name, new_name) ->
+               [
+                 (old_name, new_name);
+                 ( Concrete_ident.Create.constructor old_name,
+                   Concrete_ident.Create.constructor new_name );
+               ])
+      in
       let renamings =
         Map.of_alist_exn
           (module Concrete_ident)
-          (renamings @ List.concat_map ~f:variants_renamings renamings)
+          (renamings @ variant_and_constructors_renamings)
       in
       let rename =
         let renamer _lvl i = Map.find renamings i |> Option.value ~default:i in

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_805309848 {g as g}
+include Cyclic_modules.Rec_bundle_696247411 {g as g}
 '''
 "Cyclic_modules.C.fst" = '''
 module Cyclic_modules.C
@@ -272,8 +272,8 @@ open FStar.Mul
 
 include Cyclic_modules.Rec1_same_name.Rec_bundle_213192514 {f91805216 as f}
 '''
-"Cyclic_modules.Rec_bundle_805309848.fst" = '''
-module Cyclic_modules.Rec_bundle_805309848
+"Cyclic_modules.Rec_bundle_696247411.fst" = '''
+module Cyclic_modules.Rec_bundle_696247411
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
@@ -350,49 +350,94 @@ include Cyclic_modules.Typ_b.Rec_bundle_546955701 {t_T2Rec as t_T2Rec}
 
 include Cyclic_modules.Typ_b.Rec_bundle_546955701 {T2Rec_T2 as T2Rec_T2}
 '''
+"Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539.fst" = '''
+module Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+type t_Context =
+  | Context_A : i32 -> t_Context
+  | Context_B : i32 -> t_Context
+
+let test (x: Core.Option.t_Option i32) : Core.Option.t_Option t_Context =
+  Core.Option.impl__map #i32 #t_Context x Context_A
+
+let h (_: Prims.unit) : t_Context = Context_A 1l <: t_Context
+
+let f (_: Prims.unit) : t_Context = h ()
+'''
+"Cyclic_modules.Variant_constructor_a.fst" = '''
+module Cyclic_modules.Variant_constructor_a
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+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_584097539 {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_584097539 {test as impl__Context__test}
+
+include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {f as f}
+'''
+"Cyclic_modules.Variant_constructor_b.fst" = '''
+module Cyclic_modules.Variant_constructor_b
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+include Cyclic_modules.Variant_constructor_a.Rec_bundle_584097539 {h as h}
+'''
 "Cyclic_modules.fst" = '''
 module Cyclic_modules
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Rec_bundle_805309848 {b as b}
+include Cyclic_modules.Rec_bundle_696247411 {b as b}
+
+include Cyclic_modules.Rec_bundle_696247411 {c as c}
+
+include Cyclic_modules.Rec_bundle_696247411 {d as d}
 
-include Cyclic_modules.Rec_bundle_805309848 {c as c}
+include Cyclic_modules.Rec_bundle_696247411 {de as de}
 
-include Cyclic_modules.Rec_bundle_805309848 {d as d}
+include Cyclic_modules.Rec_bundle_696247411 {disjoint_cycle_a as disjoint_cycle_a}
 
-include Cyclic_modules.Rec_bundle_805309848 {de as de}
+include Cyclic_modules.Rec_bundle_696247411 {disjoint_cycle_b as disjoint_cycle_b}
 
-include Cyclic_modules.Rec_bundle_805309848 {disjoint_cycle_a as disjoint_cycle_a}
+include Cyclic_modules.Rec_bundle_696247411 {e as e}
 
-include Cyclic_modules.Rec_bundle_805309848 {disjoint_cycle_b as disjoint_cycle_b}
+include Cyclic_modules.Rec_bundle_696247411 {enums_a as enums_a}
 
-include Cyclic_modules.Rec_bundle_805309848 {e as e}
+include Cyclic_modules.Rec_bundle_696247411 {enums_b as enums_b}
 
-include Cyclic_modules.Rec_bundle_805309848 {enums_a as enums_a}
+include Cyclic_modules.Rec_bundle_696247411 {m1 as m1}
 
-include Cyclic_modules.Rec_bundle_805309848 {enums_b as enums_b}
+include Cyclic_modules.Rec_bundle_696247411 {m2 as m2}
 
-include Cyclic_modules.Rec_bundle_805309848 {m1 as m1}
+include Cyclic_modules.Rec_bundle_696247411 {v_rec as v_rec}
 
-include Cyclic_modules.Rec_bundle_805309848 {m2 as m2}
+include Cyclic_modules.Rec_bundle_696247411 {rec1_same_name as rec1_same_name}
 
-include Cyclic_modules.Rec_bundle_805309848 {v_rec as v_rec}
+include Cyclic_modules.Rec_bundle_696247411 {rec2_same_name as rec2_same_name}
 
-include Cyclic_modules.Rec_bundle_805309848 {rec1_same_name as rec1_same_name}
+include Cyclic_modules.Rec_bundle_696247411 {std as std}
 
-include Cyclic_modules.Rec_bundle_805309848 {rec2_same_name as rec2_same_name}
+include Cyclic_modules.Rec_bundle_696247411 {typ_a as typ_a}
 
-include Cyclic_modules.Rec_bundle_805309848 {std as std}
+include Cyclic_modules.Rec_bundle_696247411 {typ_b as typ_b}
 
-include Cyclic_modules.Rec_bundle_805309848 {typ_a as typ_a}
+include Cyclic_modules.Rec_bundle_696247411 {variant_constructor_a as variant_constructor_a}
 
-include Cyclic_modules.Rec_bundle_805309848 {typ_b as typ_b}
+include Cyclic_modules.Rec_bundle_696247411 {variant_constructor_b as variant_constructor_b}
 
-include Cyclic_modules.Rec_bundle_805309848 {f as f}
+include Cyclic_modules.Rec_bundle_696247411 {f as f}
 
-include Cyclic_modules.Rec_bundle_805309848 {h as h}
+include Cyclic_modules.Rec_bundle_696247411 {h as h}
 
-include Cyclic_modules.Rec_bundle_805309848 {h2 as h2}
+include Cyclic_modules.Rec_bundle_696247411 {h2 as h2}
 '''

tests/cyclic-modules/src/lib.rs

@@ -146,3 +146,23 @@ pub mod disjoint_cycle_b {
         super::disjoint_cycle_a::g()
     }
 }
+
+pub mod variant_constructor_a {
+    pub enum Context {
+        A(i32),
+        B(i32),
+    }
+    pub fn f() -> Context {
+        super::variant_constructor_b::h()
+    }
+    impl Context {
+        pub fn test(x: Option<i32>) -> Option<Context> {
+            x.map(Self::A)
+        }
+    }
+}
+pub mod variant_constructor_b {
+    pub fn h() -> super::variant_constructor_a::Context {
+        super::variant_constructor_a::Context::A(1)
+    }
+}