From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- library/libobject.ml | 157 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 157 insertions(+) create mode 100644 library/libobject.ml (limited to 'library/libobject.ml') diff --git a/library/libobject.ml b/library/libobject.ml new file mode 100644 index 00000000..2e531e05 --- /dev/null +++ b/library/libobject.ml @@ -0,0 +1,157 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit; + load_function : int -> object_name * 'a -> unit; + open_function : int -> object_name * 'a -> unit; + classify_function : object_name * 'a -> 'a substitutivity; + subst_function : object_name * substitution * 'a -> 'a; + export_function : 'a -> 'a option } + +let yell s = anomaly s + +let default_object s = { + object_name = s; + cache_function = (fun _ -> ()); + load_function = (fun _ _ -> ()); + open_function = (fun _ _ -> ()); + subst_function = (fun _ -> + yell ("The object "^s^" does not know how to substitute!")); + classify_function = (fun (_,obj) -> Keep obj); + export_function = (fun _ -> None)} + + +(* The suggested object declaration is the following: + + declare_object { (default_object "MY OBJECT") with + cache_function = fun (sp,a) -> Mytbl.add sp a} + + and the listed functions are only those which definitions accually + differ from the default. + + This helps introducing new functions in objects. +*) + +let ident_subst_function (_,_,a) = a + +type obj = Dyn.t (* persistent dynamic objects *) + +type dynamic_object_declaration = { + dyn_cache_function : object_name * obj -> unit; + dyn_load_function : int -> object_name * obj -> unit; + dyn_open_function : int -> object_name * obj -> unit; + dyn_subst_function : object_name * substitution * obj -> obj; + dyn_classify_function : object_name * obj -> obj substitutivity; + dyn_export_function : obj -> obj option } + +let object_tag lobj = Dyn.tag lobj + +let cache_tab = + (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) + +let declare_object odecl = + let na = odecl.object_name in + let (infun,outfun) = Dyn.create na in + let cacher (oname,lobj) = + if Dyn.tag lobj = na then odecl.cache_function (oname,outfun lobj) + else anomaly "somehow we got the wrong dynamic object in the cachefun" + and loader i (oname,lobj) = + if Dyn.tag lobj = na then odecl.load_function i (oname,outfun lobj) + else anomaly "somehow we got the wrong dynamic object in the loadfun" + and opener i (oname,lobj) = + if Dyn.tag lobj = na then odecl.open_function i (oname,outfun lobj) + else anomaly "somehow we got the wrong dynamic object in the openfun" + and substituter (oname,sub,lobj) = + if Dyn.tag lobj = na then + infun (odecl.subst_function (oname,sub,outfun lobj)) + else anomaly "somehow we got the wrong dynamic object in the substfun" + and classifier (spopt,lobj) = + if Dyn.tag lobj = na then + match odecl.classify_function (spopt,outfun lobj) with + | Dispose -> Dispose + | Substitute obj -> Substitute (infun obj) + | Keep obj -> Keep (infun obj) + | Anticipate (obj) -> Anticipate (infun obj) + else + anomaly "somehow we got the wrong dynamic object in the classifyfun" + and exporter lobj = + if Dyn.tag lobj = na then + option_app infun (odecl.export_function (outfun lobj)) + else + anomaly "somehow we got the wrong dynamic object in the exportfun" + + in + Hashtbl.add cache_tab na { dyn_cache_function = cacher; + dyn_load_function = loader; + dyn_open_function = opener; + dyn_subst_function = substituter; + dyn_classify_function = classifier; + dyn_export_function = exporter }; + (infun,outfun) + +(* this function describes how the cache, load, open, and export functions + are triggered. In relaxed mode, this function just return a meaningless + value instead of raising an exception when they fail. *) + +let apply_dyn_fun deflt f lobj = + let tag = object_tag lobj in + try + let dodecl = + try + Hashtbl.find cache_tab tag + with Not_found -> + if !relax_flag then + failwith "local to_apply_dyn_fun" + else + anomaly + ("Cannot find library functions for an object with tag "^tag) in + f dodecl + with + Failure "local to_apply_dyn_fun" -> deflt;; + +let cache_object ((_,lobj) as node) = + apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj + +let load_object i ((_,lobj) as node) = + apply_dyn_fun () (fun d -> d.dyn_load_function i node) lobj + +let open_object i ((_,lobj) as node) = + apply_dyn_fun () (fun d -> d.dyn_open_function i node) lobj + +let subst_object ((_,_,lobj) as node) = + apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj + +let classify_object ((_,lobj) as node) = + apply_dyn_fun Dispose (fun d -> d.dyn_classify_function node) lobj + +let export_object lobj = + apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj -- cgit v1.2.3