Add support for builtin trait implementations

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