Modules dans COQ\!\!\!\!

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 80 insertions, 18 deletions

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