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.

1 files changed, 13 insertions, 30 deletions

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;