From 5ea872c80cc8b9d2845629cc75369f061e3bad05 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 1 Sep 2016 14:22:13 +0200 Subject: More efficient data structure to check if a native file is loaded. Spotted by PMP. --- kernel/nativecode.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'kernel/nativecode.ml') diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index e2f43b93e..87302dcf5 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1930,13 +1930,15 @@ let compile_constant env sigma prefix ~interactive con cb = arg|]))):: [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix -let loaded_native_files = ref ([] : string list) +module StringOrd = struct type t = string let compare = String.compare end +module StringSet = Set.Make(StringOrd) -let is_loaded_native_file s = String.List.mem s !loaded_native_files +let loaded_native_files = ref StringSet.empty + +let is_loaded_native_file s = StringSet.mem s !loaded_native_files let register_native_file s = - if not (is_loaded_native_file s) then - loaded_native_files := s :: !loaded_native_files + loaded_native_files := StringSet.add s !loaded_native_files let is_code_loaded ~interactive name = match !name with -- cgit v1.2.3