summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Extract.ml32
-rw-r--r--compiler/ExtractBase.ml17
-rw-r--r--compiler/ExtractBuiltin.ml34
-rw-r--r--compiler/Translate.ml17
4 files changed, 80 insertions, 20 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index ddc02fa7..a1c9605b 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -4320,7 +4320,15 @@ let extract_trait_decl_register_names (ctx : extraction_ctx)
let builtin_info =
SimpleNameMap.find_opt sname (builtin_trait_decls_map ())
in
- let ctx = ctx_add_trait_decl trait_decl ctx in
+ let ctx =
+ let trait_name =
+ match builtin_info with
+ | None -> ctx.fmt.trait_decl_name trait_decl
+ | Some info -> info.extract_name
+ in
+ let is_opaque = false in
+ ctx_add is_opaque (TraitDeclId trait_decl.def_id) trait_name ctx
+ in
(* Parent clauses *)
let ctx =
extract_trait_decl_register_parent_clause_names ctx trait_decl builtin_info
@@ -4338,11 +4346,31 @@ let extract_trait_decl_register_names (ctx : extraction_ctx)
(** Similar to {!extract_type_decl_register_names} *)
let extract_trait_impl_register_names (ctx : extraction_ctx)
(trait_impl : trait_impl) : extraction_ctx =
+ let trait_decl =
+ TraitDeclId.Map.find trait_impl.impl_trait.trait_decl_id
+ ctx.trans_trait_decls
+ in
+ (* Check if the trait implementation is builtin *)
+ let builtin_info =
+ let open ExtractBuiltin in
+ let type_sname = name_to_simple_name trait_impl.name in
+ let trait_sname = name_to_simple_name trait_decl.name in
+ SimpleNamePairMap.find_opt (type_sname, trait_sname)
+ (builtin_trait_impls_map ())
+ in
+
(* For now we do not support overriding provided methods *)
assert (trait_impl.provided_methods = []);
(* Everything is taken care of by {!extract_trait_decl_register_names} *but*
the name of the implementation itself *)
- ctx_add_trait_impl trait_impl ctx
+ (* Compute the name *)
+ let name =
+ match builtin_info with
+ | None -> ctx.fmt.trait_impl_name trait_decl trait_impl
+ | Some name -> name
+ in
+ let is_opaque = false in
+ ctx_add is_opaque (TraitImplId trait_impl.def_id) name ctx
(** Small helper.
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 22b017e5..3ff299f2 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1272,23 +1272,6 @@ let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl)
ctx.fun_name_info;
}
-let ctx_add_trait_decl (d : trait_decl) (ctx : extraction_ctx) : extraction_ctx
- =
- let is_opaque = false in
- let name = ctx.fmt.trait_decl_name d in
- ctx_add is_opaque (TraitDeclId d.def_id) name ctx
-
-let ctx_add_trait_impl (d : trait_impl) (ctx : extraction_ctx) : extraction_ctx
- =
- (* We need to lookup the trait decl that is implemented by the trait impl *)
- let decl =
- Pure.TraitDeclId.Map.find d.impl_trait.trait_decl_id ctx.trans_trait_decls
- in
- (* Compute the name *)
- let is_opaque = false in
- let name = ctx.fmt.trait_impl_name decl d in
- ctx_add is_opaque (TraitImplId d.def_id) name ctx
-
type names_map_init = {
keywords : string list;
assumed_adts : (assumed_ty * string) list;
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 0d591028..d3cea54e 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -517,3 +517,37 @@ let mk_builtin_trait_decls_map () =
(builtin_trait_decls_info ()))
let builtin_trait_decls_map = mk_memoized mk_builtin_trait_decls_map
+
+(* TODO: generalize this.
+
+ For now, the key is:
+ - name of the impl (ex.: "alloc.boxed.Boxed")
+ - name of the implemented trait (ex.: "core.ops.deref.Deref"
+*)
+type simple_name_pair = simple_name * simple_name [@@deriving show, ord]
+
+module SimpleNamePairOrd = struct
+ type t = simple_name_pair
+
+ let compare = compare_simple_name_pair
+ let to_string = show_simple_name_pair
+ let pp_t = pp_simple_name_pair
+ let show_t = show_simple_name_pair
+end
+
+module SimpleNamePairMap = Collections.MakeMap (SimpleNamePairOrd)
+
+let builtin_trait_impls_info () : ((string list * string list) * string) list =
+ [
+ (* core::ops::Deref<alloc::boxed::Box<T>> *)
+ ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "Deref" ]),
+ "alloc.boxed.Box.coreOpsDerefInst" );
+ (* core::ops::DerefMut<alloc::boxed::Box<T>> *)
+ ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "DerefMut" ]),
+ "alloc.boxed.Box.coreOpsDerefMutInst" );
+ ]
+
+let mk_builtin_trait_impls_map () =
+ SimpleNamePairMap.of_list (builtin_trait_impls_info ())
+
+let builtin_trait_impls_map = mk_memoized mk_builtin_trait_impls_map
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 95252b61..74a8537f 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -764,8 +764,23 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
(** Export a trait implementation. *)
let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
(ctx : gen_ctx) (trait_impl_id : Pure.trait_impl_id) : unit =
+ (* Lookup the definition *)
let trait_impl = T.TraitImplId.Map.find trait_impl_id ctx.trans_trait_impls in
- Extract.extract_trait_impl ctx fmt trait_impl
+ let trait_decl =
+ Pure.TraitDeclId.Map.find trait_impl.impl_trait.trait_decl_id
+ ctx.trans_trait_decls
+ in
+ (* Check if the trait implementation is builtin *)
+ let builtin_info =
+ let open ExtractBuiltin in
+ let type_sname = name_to_simple_name trait_impl.name in
+ let trait_sname = name_to_simple_name trait_decl.name in
+ SimpleNamePairMap.find_opt (type_sname, trait_sname)
+ (builtin_trait_impls_map ())
+ in
+ match builtin_info with
+ | None -> Extract.extract_trait_impl ctx fmt trait_impl
+ | Some _ -> ()
(** A generic utility to generate the extracted definitions: as we may want to
split the definitions between different files (or not), we can control