Repository: cryspen/hax (language: rust)

Issue:
Recursive bundling tries to import submodules
```rust
mod a {
    pub fn f () {
        super::b::i()
    }
    pub mod aa {
        pub fn g(){}
    }
}

mod b {
    pub fn i() {super::a::f()}
}

```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/7cf8c4885c/gist=e733e19f5d4940c1b835e5e408ddf407)

In the generated code for module `a` we have `include Playground.A.Rec_bundle_927482861 {aa as aa}`. This shouldn't be here and doesn't lax-check.

The fix for this should be similar to https://github.com/hacspec/hax/pull/1030


Discussion / hints:

Fix patch:
diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
index 7d5570673..a54e28eeb 100644
--- a/engine/lib/dependencies.ml
+++ b/engine/lib/dependencies.ml
@@ -383,7 +383,11 @@ module Make (F : Features.T) = struct
     let aliases =
       List.map (old_new :: variants_renamings old_new)
         ~f:(fun (old_ident, new_ident) ->
-          { item with v = Alias { name = old_ident; item = new_ident } })
+          {
+            item with
+            v = Alias { name = old_ident; item = new_ident };
+            attrs = [];
+          })
     in
     item' :: aliases
 
@@ -397,7 +401,8 @@ module Make (F : Features.T) = struct
           and they have dummy names. *)
       let non_use_items =
         List.filter
-          ~f:(fun item -> match item.v with Use _ -> false | _ -> true)
+          ~f:(fun item ->
+            match item.v with Use _ | NotImplementedYet -> false | _ -> true)
           items
       in
       let bundles =


Test patch:
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 b1eaee72a..3edbdc730 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_696247411 {g as g}
+include Cyclic_modules.Rec_bundle_318256792 {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_696247411.fst" = '''
-module Cyclic_modules.Rec_bundle_696247411
+"Cyclic_modules.Rec_bundle_318256792.fst" = '''
+module Cyclic_modules.Rec_bundle_318256792
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
@@ -397,47 +397,9 @@ module Cyclic_modules
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Rec_bundle_696247411 {b as b}
+include Cyclic_modules.Rec_bundle_318256792 {f as f}
 
-include Cyclic_modules.Rec_bundle_696247411 {c as c}
+include Cyclic_modules.Rec_bundle_318256792 {h as h}
 
-include Cyclic_modules.Rec_bundle_696247411 {d as d}
-
-include Cyclic_modules.Rec_bundle_696247411 {de as de}
-
-include Cyclic_modules.Rec_bundle_696247411 {disjoint_cycle_a as disjoint_cycle_a}
-
-include Cyclic_modules.Rec_bundle_696247411 {disjoint_cycle_b as disjoint_cycle_b}
-
-include Cyclic_modules.Rec_bundle_696247411 {e as e}
-
-include Cyclic_modules.Rec_bundle_696247411 {enums_a as enums_a}
-
-include Cyclic_modules.Rec_bundle_696247411 {enums_b as enums_b}
-
-include Cyclic_modules.Rec_bundle_696247411 {m1 as m1}
-
-include Cyclic_modules.Rec_bundle_696247411 {m2 as m2}
-
-include Cyclic_modules.Rec_bundle_696247411 {v_rec as v_rec}
-
-include Cyclic_modules.Rec_bundle_696247411 {rec1_same_name as rec1_same_name}
-
-include Cyclic_modules.Rec_bundle_696247411 {rec2_same_name as rec2_same_name}
-
-include Cyclic_modules.Rec_bundle_696247411 {std as std}
-
-include Cyclic_modules.Rec_bundle_696247411 {typ_a as typ_a}
-
-include Cyclic_modules.Rec_bundle_696247411 {typ_b as typ_b}
-
-include Cyclic_modules.Rec_bundle_696247411 {variant_constructor_a as variant_constructor_a}
-
-include Cyclic_modules.Rec_bundle_696247411 {variant_constructor_b as variant_constructor_b}
-
-include Cyclic_modules.Rec_bundle_696247411 {f as f}
-
-include Cyclic_modules.Rec_bundle_696247411 {h as h}
-
-include Cyclic_modules.Rec_bundle_696247411 {h2 as h2}
+include Cyclic_modules.Rec_bundle_318256792 {h2 as h2}
 '''