feat(engine/fstar): add a prelude that explicits typeclass dependencies

engine/backends/fstar/fstar_backend.ml

@@ -78,6 +78,7 @@ module FStarNamePolicy = struct
 end
 
 module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (FStarNamePolicy)
+module Visitors = Ast_visitors.Make (InputLanguage)
 open AST
 module F = Fstar_ast
 
@@ -1431,8 +1432,52 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
            if interface_mode then [ (`Impl s, `Newline); (`Intf s, `Newline) ]
            else [ (`Impl s, `Newline) ])
 
-let string_of_items ~signature_only (bo : BackendOptions.t) m items :
+(** Convers a namespace to a module name *)
+let module_name (ns : string * string list) : string =
+  String.concat ~sep:"."
+    (List.map ~f:(map_first_letter String.uppercase) (fst ns :: snd ns))
+
+let string_of_items ~signature_only ~mod_name (bo : BackendOptions.t) m items :
     string * string =
+  let collect_trait_goal_idents =
+    object
+      inherit [_] Visitors.reduce as super
+      inherit [_] U.Sets.Concrete_ident.monoid as _m
+
+      method! visit_trait_goal (_env : unit) x =
+        Set.singleton (module Concrete_ident) x.trait
+    end
+  in
+  let header =
+    let lines =
+      List.map ~f:(collect_trait_goal_idents#visit_item ()) items
+      |> Set.union_list (module Concrete_ident)
+      |> Set.map
+           (module String)
+           ~f:(fun i -> U.Concrete_ident_view.to_namespace i |> module_name)
+      |> Fn.flip Set.remove mod_name
+      |> Set.to_list
+      |> List.filter ~f:(fun m ->
+             (* Special treatment for modules handled specifically in our F* libraries *)
+             String.is_prefix ~prefix:"Core." m |> not
+             && String.is_prefix ~prefix:"Alloc." m |> not
+             && String.equal "Hax_lib.Int" m |> not)
+      |> List.map ~f:(fun mod_path -> "let open " ^ mod_path ^ " in")
+    in
+    match lines with
+    | [] -> ""
+    | _ ->
+        "let _ ="
+        ^ ([
+             "(* This module has implicit dependencies, here we make them \
+              explicit. *)";
+             "(* The implicit dependencies arise from typeclasses instances. *)";
+           ]
+           @ lines @ [ "()" ]
+          |> List.map ~f:(( ^ ) "\n  ")
+          |> String.concat ~sep:"")
+        ^ "\n\n"
+  in
   let strings =
     List.concat_map ~f:(strings_of_item ~signature_only bo m items) items
     |> List.map
@@ -1453,11 +1498,14 @@ let string_of_items ~signature_only (bo : BackendOptions.t) m items :
         strings
     in
     let n = List.length l - 1 in
-    List.mapi
-      ~f:(fun i (s, space) ->
-        s ^ if [%matches? `NoNewline] space || [%eq: int] i n then "" else "\n")
-      l
-    |> String.concat ~sep:"\n"
+    let lines =
+      List.mapi
+        ~f:(fun i (s, space) ->
+          s
+          ^ if [%matches? `NoNewline] space || [%eq: int] i n then "" else "\n")
+        l
+    in
+    match lines with [] -> "" | _ -> header ^ String.concat ~sep:"\n" lines
   in
   ( string_for (function `Impl s -> Some s | _ -> None),
     string_for (function `Intf s -> Some s | _ -> None) )
@@ -1487,13 +1535,10 @@ let translate m (bo : BackendOptions.t) (items : AST.item list) :
            in
            List.exists ~f:contains_dropped_body items
          in
-         let mod_name =
-           String.concat ~sep:"."
-             (List.map
-                ~f:(map_first_letter String.uppercase)
-                (fst ns :: snd ns))
+         let mod_name = module_name ns in
+         let impl, intf =
+           string_of_items ~signature_only ~mod_name bo m items
          in
-         let impl, intf = string_of_items ~signature_only bo m items in
          let make ~ext body =
            if String.is_empty body then None
            else

test-harness/src/snapshots/toolchain__literals into-coq.snap

@@ -58,14 +58,6 @@ Definition fn_pointer_cast (_ : unit) : unit :=
       x : int32 -> int32 in
   tt.
 
-Definition numeric (_ : unit) : unit :=
-  let (_ : uint_size) := (@repr WORDSIZE32 123) : uint_size in
-  let (_ : uint_size) := (@repr WORDSIZE32 42) : uint_size in
-  let (_ : uint_size) := (@repr WORDSIZE32 42) : uint_size in
-  let (_ : int32) := (@repr WORDSIZE32 42) : int32 in
-  let (_ : int128) := (@repr WORDSIZE128 22222222222222222222) : int128 in
-  tt.
-
 Definition math_integers (x : t_Int_t) : int8 :=
   let (_ : t_Int_t) := f_lift (@repr WORDSIZE32 3) : t_Int_t in
   let _ := (impl__Int___unsafe_from_str -340282366920938463463374607431768211455000)>.?(impl__Int___unsafe_from_str 340282366920938463463374607431768211455000) : bool in
@@ -90,6 +82,14 @@ Definition math_integers (x : t_Int_t) : int8 :=
   let (_ : uint_size) := impl__Int__to_usize x : uint_size in
   impl__Int__to_u8 (x.+(x.*x)).
 
+Definition numeric (_ : unit) : unit :=
+  let (_ : uint_size) := (@repr WORDSIZE32 123) : uint_size in
+  let (_ : uint_size) := (@repr WORDSIZE32 42) : uint_size in
+  let (_ : uint_size) := (@repr WORDSIZE32 42) : uint_size in
+  let (_ : int32) := (@repr WORDSIZE32 42) : int32 in
+  let (_ : int128) := (@repr WORDSIZE128 22222222222222222222) : int128 in
+  tt.
+
 Definition empty_array (_ : unit) : unit :=
   let (_ : seq int8) := unsize !TODO empty array! : seq int8 in
   tt.

test-harness/src/snapshots/toolchain__literals into-fstar.snap

@@ -109,14 +109,6 @@ let fn_pointer_cast (_: Prims.unit) : Prims.unit =
   let (f: (u32 -> u32)): u32 -> u32 = fun x -> x in
   ()
 
-let numeric (_: Prims.unit) : Prims.unit =
-  let (_: usize):usize = sz 123 in
-  let (_: isize):isize = isz (-42) in
-  let (_: isize):isize = isz 42 in
-  let (_: i32):i32 = (-42l) in
-  let (_: u128):u128 = pub_u128 22222222222222222222 in
-  ()
-
 let math_integers (x: Hax_lib.Int.t_Int)
     : Prims.Pure u8
       (requires x > (0 <: Hax_lib.Int.t_Int) && x < (16 <: Hax_lib.Int.t_Int))
@@ -147,6 +139,14 @@ let math_integers (x: Hax_lib.Int.t_Int)
   let (_: usize):usize = Hax_lib.Int.impl__Int__to_usize x in
   Hax_lib.Int.impl__Int__to_u8 (x + (x * x <: Hax_lib.Int.t_Int) <: Hax_lib.Int.t_Int)
 
+let numeric (_: Prims.unit) : Prims.unit =
+  let (_: usize):usize = sz 123 in
+  let (_: isize):isize = isz (-42) in
+  let (_: isize):isize = isz 42 in
+  let (_: i32):i32 = (-42l) in
+  let (_: u128):u128 = pub_u128 22222222222222222222 in
+  ()
+
 let empty_array (_: Prims.unit) : Prims.unit =
   let (_: t_Slice u8):t_Slice u8 =
     Rust_primitives.unsize (let list:Prims.list u8 = [] in

test-harness/src/snapshots/toolchain__traits into-fstar.snap

@@ -29,6 +29,62 @@ Compiling traits v0.1.0 (WORKSPACE_ROOT/traits)
 diagnostics = []
 
 [stdout.files]
+"Traits.Issue_667_implicit_dependencies.Define_type.fst" = '''
+module Traits.Issue_667_implicit_dependencies.Define_type
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+type t_MyType = | MyType : t_MyType
+'''
+"Traits.Issue_667_implicit_dependencies.Impl_type.fst" = '''
+module Traits.Issue_667_implicit_dependencies.Impl_type
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl: Traits.Issue_667_implicit_dependencies.Trait_definition.t_MyTrait
+Traits.Issue_667_implicit_dependencies.Define_type.t_MyType =
+  {
+    f_my_method_pre
+    =
+    (fun (self: Traits.Issue_667_implicit_dependencies.Define_type.t_MyType) -> true);
+    f_my_method_post
+    =
+    (fun (self: Traits.Issue_667_implicit_dependencies.Define_type.t_MyType) (out: Prims.unit) ->
+        true);
+    f_my_method = fun (self: Traits.Issue_667_implicit_dependencies.Define_type.t_MyType) -> ()
+  }
+'''
+"Traits.Issue_667_implicit_dependencies.Trait_definition.fst" = '''
+module Traits.Issue_667_implicit_dependencies.Trait_definition
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+class t_MyTrait (v_Self: Type0) = {
+  f_my_method_pre:v_Self -> bool;
+  f_my_method_post:v_Self -> Prims.unit -> bool;
+  f_my_method:x0: v_Self
+    -> Prims.Pure Prims.unit (f_my_method_pre x0) (fun result -> f_my_method_post x0 result)
+}
+'''
+"Traits.Issue_667_implicit_dependencies.Use_type.fst" = '''
+module Traits.Issue_667_implicit_dependencies.Use_type
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let _ =
+  (* This module has implicit dependencies, here we make them explicit. *)
+  (* The implicit dependencies arise from typeclasses instances. *)
+  let open Traits.Issue_667_implicit_dependencies.Impl_type in
+  ()
+
+let some_function (x: Traits.Issue_667_implicit_dependencies.Define_type.t_MyType) : Prims.unit =
+  Traits.Issue_667_implicit_dependencies.Trait_definition.f_my_method x
+'''
 "Traits.fst" = '''
 module Traits
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

tests/traits/src/lib.rs

@@ -77,3 +77,25 @@ impl Error {
         || Self::Fail
     }
 }
+
+mod issue_667_implicit_dependencies {
+    mod trait_definition {
+        pub trait MyTrait {
+            fn my_method(self);
+        }
+    }
+    mod define_type {
+        pub struct MyType;
+    }
+    mod impl_type {
+        impl super::trait_definition::MyTrait for super::define_type::MyType {
+            fn my_method(self) {}
+        }
+    }
+    mod use_type {
+        fn some_function(x: super::define_type::MyType) {
+            use super::trait_definition::MyTrait;
+            x.my_method()
+        }
+    }
+}