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.

7 files changed, 55 insertions, 47 deletions

diff --git a/lib/dyn.ml b/lib/dyn.ml
index 93f19fce9..abb2fbcee 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 9173e8101..00c030177 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
diff --git a/library/declaremods.ml b/library/declaremods.ml
index dae585d5a..c60e008d1 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -369,7 +369,7 @@ let rec replace_module_object idl mp0 objs0 mp1 objs1 =
   match idl, objs0 with
   | _,[] -> []
   | id::idl,(id',obj)::tail when Id.equal id id' ->
-    assert (String.equal (object_tag obj) "MODULE");
+    assert (object_has_tag obj "MODULE");
     let mp_id = MPdot(mp0, Label.of_id id) in
     let objs = match idl with
       | [] -> Lib.subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1
diff --git a/library/libobject.ml b/library/libobject.ml
index 7cf286321..3bbb1e90e 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -74,7 +74,8 @@ type dynamic_object_declaration = {
   dyn_discharge_function : object_name * obj -> obj option;
   dyn_rebuild_function : obj -> obj }
 
-let object_tag lobj = Dyn.tag lobj
+let object_tag = Dyn.tag
+let object_has_tag = Dyn.has_tag
 
 let cache_tab =
   (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
@@ -82,36 +83,18 @@ let cache_tab =
 let declare_object_full odecl =
   let na = odecl.object_name in
   let (infun,outfun) = Dyn.create na in
-  let cacher (oname,lobj) =
-    if String.equal (Dyn.tag lobj) na then odecl.cache_function (oname,outfun lobj)
-    else anomaly (Pp.str "somehow we got the wrong dynamic object in the cachefun")
-  and loader i (oname,lobj) =
-    if String.equal (Dyn.tag lobj) na then odecl.load_function i (oname,outfun lobj)
-    else anomaly (Pp.str "somehow we got the wrong dynamic object in the loadfun")
-  and opener i (oname,lobj) =
-    if String.equal (Dyn.tag lobj) na then odecl.open_function i (oname,outfun lobj)
-    else anomaly (Pp.str "somehow we got the wrong dynamic object in the openfun")
-  and substituter (sub,lobj) = 
-    if String.equal (Dyn.tag lobj) na then 
-      infun (odecl.subst_function (sub,outfun lobj))
-    else anomaly (Pp.str "somehow we got the wrong dynamic object in the substfun")
-  and classifier lobj =
-    if String.equal (Dyn.tag lobj) na then
-      match odecl.classify_function (outfun lobj) with
-	| Dispose -> Dispose
-	| Substitute obj -> Substitute (infun obj)
-	| Keep obj -> Keep (infun obj)
-	| Anticipate (obj) -> Anticipate (infun obj)
-    else
-      anomaly (Pp.str "somehow we got the wrong dynamic object in the classifyfun")
+  let cacher (oname,lobj) = odecl.cache_function (oname,outfun lobj)
+  and loader i (oname,lobj) = odecl.load_function i (oname,outfun lobj)
+  and opener i (oname,lobj) = odecl.open_function i (oname,outfun lobj)
+  and substituter (sub,lobj) = infun (odecl.subst_function (sub,outfun lobj))
+  and classifier lobj = match odecl.classify_function (outfun lobj) with
+  | Dispose -> Dispose
+  | Substitute obj -> Substitute (infun obj)
+  | Keep obj -> Keep (infun obj)
+  | Anticipate (obj) -> Anticipate (infun obj)
   and discharge (oname,lobj) =
-    if String.equal (Dyn.tag lobj) na then
-      Option.map infun (odecl.discharge_function (oname,outfun lobj))
-    else
-      anomaly (Pp.str "somehow we got the wrong dynamic object in the dischargefun")
-  and rebuild lobj =
-    if String.equal (Dyn.tag lobj) na then infun (odecl.rebuild_function (outfun lobj))
-    else anomaly (Pp.str "somehow we got the wrong dynamic object in the rebuildfun")
+    Option.map infun (odecl.discharge_function (oname,outfun lobj))
+  and rebuild lobj = infun (odecl.rebuild_function (outfun lobj))
   in
   Hashtbl.add cache_tab na { dyn_cache_function = cacher;
 			     dyn_load_function = loader;
diff --git a/library/libobject.mli b/library/libobject.mli
index e886c4db0..3986b3d3f 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -100,6 +100,7 @@ val declare_object :
   'a object_declaration -> ('a -> obj)
 
 val object_tag : obj -> string
+val object_has_tag : obj -> string -> bool
 
 val cache_object : object_name * obj -> unit
 val load_object : int -> object_name * obj -> unit
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 1bba78334..261e8583e 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -689,11 +689,12 @@ and intern_tacarg strict onlytac ist = function
     let (_, arg) = Genintern.generic_intern ist arg in
     TacGeneric arg
   | TacDynamic(loc,t) as x ->
-      (match Dyn.tag t with
-	| "tactic" | "value" -> x
-        | "constr" -> if onlytac then error_tactic_expected loc else x
-	| s -> anomaly ~loc
-                 (str "Unknown dynamic: <" ++ str s ++ str ">"))
+    if Dyn.has_tag t "tactic" || Dyn.has_tag t "value" then x
+    else if Dyn.has_tag t "constr" then
+      if onlytac then error_tactic_expected loc else x
+    else
+      let tag = Dyn.tag t in
+      anomaly ~loc (str "Unknown dynamic: <" ++ str tag ++ str ">")
 
 (* Reads the rules of a Match Context or a Match *)
 and intern_match_rule onlytac ist = function
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 3eb61ccdf..4f2dd2f33 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -251,7 +251,7 @@ let eterm_obligations env name evm fs ?status t ty =
 	 in
 	 let tac = match Store.get ev.evar_extra evar_tactic with
 	   | Some t ->
-	       if String.equal (Dyn.tag t) "tactic" then
+	       if Dyn.has_tag t "tactic" then
 		 Some (Tacinterp.interp 
 			  (Tacinterp.globTacticIn (Tacinterp.tactic_out t)))
 	       else None