Merge pull request #676 from hacspec/fix-667

Engine: F*: open modules providing trait impls

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
 
@@ -1434,8 +1435,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
@@ -1456,11 +1501,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) )
@@ -1490,13 +1538,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

hax-lib/src/int/mod.rs

@@ -89,13 +89,38 @@ pub trait Concretization<T> {
  fn concretize(self) -> T;
 }
 
-impl<T: Into<num_bigint::BigInt>> Abstraction for T {
- type AbstractType = Int;
- fn lift(self) -> Self::AbstractType {
- Int::new(self.into())
- }
+/// Instead of defining one overloaded instance, which relies
+/// explicitely on `num_bigint`:
+///
+/// ```ignore
+/// impl<T: Into<num_bigint::BigInt>> Abstraction for T {
+/// type AbstractType = Int;
+/// fn lift(self) -> Self::AbstractType {
+/// Int::new(self.into())
+/// }
+/// }
+/// ```
+///
+/// We define an instance per machine type: we don't want the
+/// interface of this module to rely specifically on
+/// `num_bigint`. This module should be a very thin layer.
+macro_rules! implement_abstraction {
+ ($ty:ident) => {
+ impl Abstraction for $ty {
+ type AbstractType = Int;
+ fn lift(self) -> Self::AbstractType {
+ Int::new(num_bigint::BigInt::from(self))
+ }
+ }
+ };
+ ($($ty:ident)*) => {
+ $(implement_abstraction!($ty);)*
+ };
 }
 
+implement_abstraction!(u8 u16 u32 u64 u128 usize);
+implement_abstraction!(i8 i16 i32 i64 i128 isize);
+
 macro_rules! implement_concretize {
  ($ty:ident $method:ident) => {
  impl Concretization<$ty> for Int {

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

@@ -116,6 +116,63 @@ let v__f (#v_X: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_X
  let _:u8 = f_to_t #v_X #u8 x in
  ()
 '''
+"Traits.Implicit_dependencies_issue_667_.Define_type.fst" = '''
+module Traits.Implicit_dependencies_issue_667_.Define_type
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+type t_MyType = | MyType : t_MyType
+'''
+"Traits.Implicit_dependencies_issue_667_.Impl_type.fst" = '''
+module Traits.Implicit_dependencies_issue_667_.Impl_type
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl: Traits.Implicit_dependencies_issue_667_.Trait_definition.t_MyTrait
+Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType =
+ {
+ f_my_method_pre
+ =
+ (fun (self: Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType) -> true);
+ f_my_method_post
+ =
+ (fun (self: Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType) (out: Prims.unit) ->
+ true);
+ f_my_method = fun (self: Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType) -> ()
+ }
+'''
+"Traits.Implicit_dependencies_issue_667_.Trait_definition.fst" = '''
+module Traits.Implicit_dependencies_issue_667_.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.Implicit_dependencies_issue_667_.Use_type.fst" = '''
+module Traits.Implicit_dependencies_issue_667_.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.Implicit_dependencies_issue_667_.Impl_type in
+ ()
+
+let some_function (x: Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType) : Prims.unit =
+ Traits.Implicit_dependencies_issue_667_.Trait_definition.f_my_method #Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType
+ x
+'''
 "Traits.Unconstrainted_types_issue_677_.fst" = '''
 module Traits.Unconstrainted_types_issue_677_
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

tests/traits/src/lib.rs

@@ -109,7 +109,6 @@ mod for_clauses {
  }
 }
 
-// From issue #677
 mod unconstrainted_types_issue_677 {
  trait PolyOp {
  fn op(x: u32, y: u32) -> u32;
@@ -141,3 +140,26 @@ mod unconstrainted_types_issue_677 {
  assert!(both(10) == (20, 100));
  }
 }
+
+// From issue_667
+mod implicit_dependencies_issue_667 {
+ 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()
+ }
+ }
+}