Using hashes instead of strings in dynamic tags. In case of collision, an

anomaly is raised. As there are very few tags defined in Coq code, this is
very unlikely to appear, and can be fixed by tweaking the name of the
dynamic argument.

This should be more efficient, as we did compare equal strings each time.

2 files changed, 33 insertions, 10 deletions

diff --git a/lib/dyn.ml b/lib/dyn.ml
index 93f19fce9e..abb2fbceec 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -10,16 +10,38 @@ open Errors
 
 (* Dynamics, programmed with DANGER !!! *)
 
-type t = string * Obj.t
+type t = int * Obj.t
 
-let dyntab = ref ([] : string list)
+let dyntab = ref (Int.Map.empty : string Int.Map.t)
+(** Instead of working with tags as strings, which are costly, we use their
+    hash. We ensure unicity of the hash in the [create] function. If ever a
+    collision occurs, which is unlikely, it is sufficient to tweak the offending
+    dynamic tag. *)
 
-let create s =
-  if List.exists (fun s' -> CString.equal s s') !dyntab then
-    anomaly ~label:"Dyn.create" (Pp.str ("already declared dynamic " ^ s));
-  dyntab := s :: !dyntab;
-  ((fun v -> (s,Obj.repr v)),
-   (fun (s',rv) ->
-      if s = s' then Obj.magic rv else failwith "dyn_out"))
+let create (s : string) =
+  let hash = Hashtbl.hash s in
+  let () =
+    if Int.Map.mem hash !dyntab then
+      let old = Int.Map.find hash !dyntab in
+      let msg = Pp.str ("Dynamic tag collision: " ^ s ^ " vs. " ^ old) in
+      anomaly ~label:"Dyn.create" msg
+  in
+  let () = dyntab := Int.Map.add hash s !dyntab in
+  let infun v = (hash, Obj.repr v) in
+  let outfun (nh, rv) =
+    if Int.equal hash nh then Obj.magic rv
+    else
+      let msg = (Pp.str ("dyn_out: expected " ^ s)) in
+      anomaly msg
+  in
+  (infun, outfun)
 
-let tag (s,_) = s
+let has_tag (s, _) tag =
+  let hash = Hashtbl.hash (tag : string) in
+  Int.equal s hash
+
+let tag (s,_) =
+  try Int.Map.find s !dyntab
+  with Not_found ->
+    let msg = Pp.str ("Unknown dynamic tag " ^ (string_of_int s)) in
+    anomaly msg
diff --git a/lib/dyn.mli b/lib/dyn.mli
index 9173e81019..00c0301779 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -12,3 +12,4 @@ type t
 
 val create : string -> ('a -> t) * (t -> 'a)
 val tag : t -> string
+val has_tag : t -> string -> bool