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