Use the name matcher implemented in Charon

1 files changed, 48 insertions, 0 deletions

diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml
index a974cdee..f251e169 100644
--- a/compiler/TranslateCore.ml
+++ b/compiler/TranslateCore.ml
@@ -1,6 +1,7 @@
 (** Some utilities for the translation *)
 
 open Contexts
+open ExtractName
 
 (** The local logger *)
 let log = Logging.translate_log
@@ -29,3 +30,50 @@ let trans_ctx_to_pure_fmt_env (ctx : trans_ctx) : PrintPure.fmt_env =
 
 let name_to_string (ctx : trans_ctx) =
   Print.Types.name_to_string (trans_ctx_to_fmt_env ctx)
+
+let match_name_find_opt (ctx : trans_ctx) (name : Types.name)
+    (m : 'a NameMatcherMap.t) : 'a option =
+  let open Charon.NameMatcher in
+  let open ExtractBuiltin in
+  let mctx : ctx =
+    {
+      type_decls = ctx.type_ctx.type_decls;
+      global_decls = ctx.global_ctx.global_decls;
+      trait_decls = ctx.trait_decls_ctx.trait_decls;
+    }
+  in
+  NameMatcherMap.find_opt mctx name m
+
+let match_name_with_generics_find_opt (ctx : trans_ctx) (name : Types.name)
+    (generics : Types.generic_args) (m : 'a NameMatcherMap.t) : 'a option =
+  let open Charon.NameMatcher in
+  let open ExtractBuiltin in
+  let mctx : ctx =
+    {
+      type_decls = ctx.type_ctx.type_decls;
+      global_decls = ctx.global_ctx.global_decls;
+      trait_decls = ctx.trait_decls_ctx.trait_decls;
+    }
+  in
+  NameMatcherMap.find_with_generics_opt mctx name generics m
+
+let name_to_simple_name (ctx : trans_ctx) (n : Types.name) : string list =
+  let mctx : Charon.NameMatcher.ctx =
+    {
+      type_decls = ctx.type_ctx.type_decls;
+      global_decls = ctx.global_ctx.global_decls;
+      trait_decls = ctx.trait_decls_ctx.trait_decls;
+    }
+  in
+  name_to_simple_name mctx n
+
+let name_with_generics_to_simple_name (ctx : trans_ctx) (n : Types.name)
+    (p : Types.generic_params) (g : Types.generic_args) : string list =
+  let mctx : Charon.NameMatcher.ctx =
+    {
+      type_decls = ctx.type_ctx.type_decls;
+      global_decls = ctx.global_ctx.global_decls;
+      trait_decls = ctx.trait_decls_ctx.trait_decls;
+    }
+  in
+  name_with_generics_to_simple_name mctx n p g