diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 2 | ||||
| -rw-r--r-- | library/libobject.ml | 43 | ||||
| -rw-r--r-- | library/libobject.mli | 1 |
3 files changed, 15 insertions, 31 deletions
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 |