diff options
author | Son Ho | 2023-10-24 15:01:55 +0200 |
---|---|---|
committer | Son Ho | 2023-10-24 15:01:55 +0200 |
commit | be70eed487b507dc002660a4c891397003165e75 (patch) | |
tree | c583606a23478c76c6e74c33ba2fe471e2eff4fe /compiler/Translate.ml | |
parent | 63107911c16a9991f7d5cf8c6df621318a03ca3b (diff) |
Add support for builtin trait implementations
Diffstat (limited to '')
-rw-r--r-- | compiler/Translate.ml | 17 |
1 files changed, 16 insertions, 1 deletions
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 |