From 724ff98309444537cf03ba7ccab06d432e2eb376 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 22 Nov 2023 11:14:13 +0100
Subject: Use NameMatcher.NameMatcherMap instead of associative lists

---
 compiler/ExtractBuiltin.ml | 19 ++++++++++++++-----
 compiler/ExtractName.ml    | 21 ++++++++-------------
 2 files changed, 22 insertions(+), 18 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index ef746ddf..6de47920 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -299,10 +299,15 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info list) list
   ]
 
 let mk_builtin_funs_map () =
-  NameMatcherMap.of_list
-    (List.map
-       (fun (name, filter, info) -> (name, (filter, info)))
-       (builtin_funs ()))
+  let m =
+    NameMatcherMap.of_list
+      (List.map
+         (fun (name, filter, info) -> (name, (filter, info)))
+         (builtin_funs ()))
+  in
+  log#ldebug
+    (lazy ("builtin_funs_map:\n" ^ NameMatcherMap.to_string (fun _ -> "") m));
+  m
 
 let builtin_funs_map = mk_memoized mk_builtin_funs_map
 
@@ -555,6 +560,10 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list =
   ]
 
 let mk_builtin_trait_impls_map () =
-  NameMatcherMap.of_list (builtin_trait_impls_info ())
+  let m = NameMatcherMap.of_list (builtin_trait_impls_info ()) in
+  log#ldebug
+    (lazy
+      ("builtin_trait_impls_map:\n" ^ NameMatcherMap.to_string (fun _ -> "") m));
+  m
 
 let builtin_trait_impls_map = mk_memoized mk_builtin_trait_impls_map
diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 0943aefe..94222ae1 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -5,29 +5,24 @@ open Charon.NameMatcher
 let log = Logging.extract_log
 
 module NameMatcherMap = struct
-  type 'a t = (pattern * 'a) list
+  module NMM = NameMatcherMap
+
+  type 'a t = 'a NMM.t
 
   let config = { map_vars_to_vars = true }
 
   let find_opt (ctx : ctx) (name : Types.name) (m : 'a t) : 'a option =
-    match List.find_opt (fun (pat, _) -> match_name ctx config pat name) m with
-    | None -> None
-    | Some (_, v) -> Some v
+    NMM.find_opt ctx config name m
 
   let find_with_generics_opt (ctx : ctx) (name : Types.name)
       (g : Types.generic_args) (m : 'a t) : 'a option =
-    match
-      List.find_opt
-        (fun (pat, _) -> match_name_with_generics ctx config pat name g)
-        m
-    with
-    | None -> None
-    | Some (_, v) -> Some v
+    NMM.find_with_generics_opt ctx config name g m
 
   let mem (ctx : ctx) (name : Types.name) (m : 'a t) : bool =
-    find_opt ctx name m <> None
+    NMM.mem ctx config name m
 
-  let of_list (ls : (pattern * 'a) list) : 'a t = ls
+  let of_list (ls : (pattern * 'a) list) : 'a t = NMM.of_list ls
+  let to_string = NMM.to_string
 end
 
 (** Helper to convert name patterns to names for extraction.
-- 
cgit v1.2.3