From 400327165edcba667ebb70ebb89052455656b719 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 19 Nov 2013 19:50:51 +0100 Subject: 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. --- library/declaremods.ml | 2 +- library/libobject.ml | 43 +++++++++++++------------------------------ library/libobject.mli | 1 + 3 files changed, 15 insertions(+), 31 deletions(-) (limited to 'library') 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 -- cgit v1.2.3