diff options
author | Son Ho | 2023-11-22 11:14:13 +0100 |
---|---|---|
committer | Son Ho | 2023-11-22 11:14:13 +0100 |
commit | 724ff98309444537cf03ba7ccab06d432e2eb376 (patch) | |
tree | b9b86698fa2ecb66440eda609f9855ebf2fd474e /compiler/ExtractName.ml | |
parent | 84a505ed9f193885175308ecc837922a41176b5b (diff) |
Use NameMatcher.NameMatcherMap instead of associative lists
Diffstat (limited to 'compiler/ExtractName.ml')
-rw-r--r-- | compiler/ExtractName.ml | 21 |
1 files changed, 8 insertions, 13 deletions
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. |