Repository: cryspen/hax (language: rust)

Issue:
No renaming of enum variant constructor as closure in cyclic dependencies bundling
```rust
pub mod a {
    pub enum Context {
        A(i32),
        B(i32)
    }
    pub fn f () -> Context {super::b::h()}
    impl Context {
        pub fn test (x: Option<i32>) -> Option<Context> {
            x.map(Self::A)
        }
    }
}
pub mod b {
    pub fn h () -> super::a::Context {
        super::a::Context::A(1)
    }
}
```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/21672cd0da/gist=02e1f1d6a4c867fd25f808a5c95689e5)

We produce `Playground.A.Context.v_A` for `Self::A` but it should be renamed to belong to the bundle.


Discussion / hints:
Using the variant constructor as a closure seems to refer to something that doesn't exist even when bundling is not involved:

```rust

pub enum Context {
    A(i32),
    B(i32)
}
impl Context {
    pub fn test (x: Option<i32>) -> Option<Context> {
        x.map(Self::A)
    }
}

```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/21672cd0da/gist=23a4a138fa1f6c4fb6919105572f4941)

@W95Psp Is this supposed to function?
> Using the variant constructor as a closure seems to refer to something that doesn't exist even when bundling is not involved:
> 
> pub enum Context {
>     A(i32),
>     B(i32)
> }
> impl Context {
>     pub fn test (x: Option<i32>) -> Option<Context> {
>         x.map(Self::A)
>     }
> }
> 
> [Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/21672cd0da/gist=23a4a138fa1f6c4fb6919105572f4941)
> 
> [@W95Psp](https://github.com/W95Psp) Is this supposed to function?

We produce the following fstar for this:

```
module Playground
#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 impl__Context__test
      (x: Core.Option.t_Option i32)
    : Core.Option.t_Option t_Context =
  Core.Option.impl__map #i32
    #t_Context
    x
    Playground.Context.v_A
```

I think just replacing `Playground.Context.v_A` by `Context_A` would work in f*. One way to do that would be to recognize `GlobalName` (if we do it in `import_thir`) or `GlobalVar` (if we add a phase for this, which is probably the best choice) for which the id is `path_to_enum::Variant::Ctor` and replace them with the corresponding `Construct` expression.
The solution should also work for structs:

```rust
struct Test(i32);
impl Test {
    pub fn test (x: Option<i32>) -> Option<Test> {
        x.map(Self)
    }
}
```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/21672cd0da/gist=6e93c68c42baae44f76c9aac2cdeb12b)

The case of structs is very similar (we get a `GlobalVar` expr with the id of the struct followed by `Ctor`). Maybe the solution would be to add a phase catching this kind of expressions, looking for the corresponding type definition (we need to get some information like `is_struct`) and replace with the right expression. It is probably more complicated than a `Construct` expression as this needs to be applied. so maybe we can do something like `(fun x -> Construct x)`.


This is a duplicate of #914, closing.
#914 is now fixed but we need to rename even with the `Ctor` at the end of names

Fix patch:
diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml
index e367d7037..c5bebf76f 100644
--- a/engine/lib/concrete_ident/concrete_ident.ml
+++ b/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 =
diff --git a/engine/lib/concrete_ident/concrete_ident.mli b/engine/lib/concrete_ident/concrete_ident.mli
index 8a5e413eb..e87f71b22 100644
--- a/engine/lib/concrete_ident/concrete_ident.mli
+++ b/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 *)
diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
index 2cbe2a32e..7d5570673 100644
--- a/engine/lib/dependencies.ml
+++ b/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 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 2b4320887..b1eaee72a 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_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}
 '''
diff --git a/tests/cyclic-modules/src/lib.rs b/tests/cyclic-modules/src/lib.rs
index 781a1e156..b59be2d80 100644
--- a/tests/cyclic-modules/src/lib.rs
+++ b/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)
+    }
+}