summaryrefslogtreecommitdiff
path: root/compiler/ExtractName.ml
diff options
context:
space:
mode:
authorSon Ho2023-11-22 11:14:13 +0100
committerSon Ho2023-11-22 11:14:13 +0100
commit724ff98309444537cf03ba7ccab06d432e2eb376 (patch)
treeb9b86698fa2ecb66440eda609f9855ebf2fd474e /compiler/ExtractName.ml
parent84a505ed9f193885175308ecc837922a41176b5b (diff)
Use NameMatcher.NameMatcherMap instead of associative lists
Diffstat (limited to 'compiler/ExtractName.ml')
-rw-r--r--compiler/ExtractName.ml21
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.