diff options
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/ExtractBuiltin.ml | 19 | ||||
-rw-r--r-- | compiler/ExtractName.ml | 21 |
2 files changed, 22 insertions, 18 deletions
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. |