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/libobject.ml | 43 +++++++++++++------------------------------ 1 file changed, 13 insertions(+), 30 deletions(-) (limited to 'library/libobject.ml') 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; -- cgit v1.2.3