From 12965209478bd99dfbe57f07d5b525e51b903f22 Mon Sep 17 00:00:00 2001 From: coq Date: Fri, 2 Aug 2002 17:17:42 +0000 Subject: Modules dans COQ\!\!\!\! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/libobject.ml | 98 ++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 80 insertions(+), 18 deletions(-) (limited to 'library/libobject.ml') diff --git a/library/libobject.ml b/library/libobject.ml index bbd8615be..2049e8e04 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -10,6 +10,7 @@ open Util open Names +open Libnames (* The relax flag is used to make it possible to load files while ignoring failures to incorporate some objects. This can be useful when one @@ -23,18 +24,53 @@ let relax_flag = ref false;; let relax b = relax_flag := b;; +type 'a substitutivity = + Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a + + type 'a object_declaration = { - cache_function : section_path * 'a -> unit; - load_function : section_path * 'a -> unit; - open_function : section_path * 'a -> unit; + object_name : string; + cache_function : object_name * 'a -> 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 : section_path * obj -> unit; - dyn_load_function : section_path * obj -> unit; - dyn_open_function : section_path * obj -> unit; + 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 @@ -42,23 +78,43 @@ let object_tag lobj = Dyn.tag lobj let cache_tab = (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) -let declare_object (na,odecl) = +let declare_object odecl = + let na = odecl.object_name in let (infun,outfun) = Dyn.create na in - let cacher (spopt,lobj) = - if Dyn.tag lobj = na then odecl.cache_function(spopt,outfun lobj) + 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 (spopt,lobj) = - if Dyn.tag lobj = na then odecl.load_function (spopt,outfun lobj) + 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 (spopt,lobj) = - if Dyn.tag lobj = na then odecl.open_function (spopt,outfun lobj) + 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 = - option_app infun (odecl.export_function (outfun 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) @@ -85,11 +141,17 @@ let apply_dyn_fun deflt f lobj = let cache_object ((_,lobj) as node) = apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj -let load_object ((_,lobj) as node) = - apply_dyn_fun () (fun d -> d.dyn_load_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 open_object ((_,lobj) as node) = - apply_dyn_fun () (fun d -> d.dyn_open_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