Add the ability to specify the implicit status of section variables and

whether or not to keep them regardless of the actual dependencies (in
order to implement the proper discharge behavior for type classes). 
This means adding an argument to rebuild_function in libobject, giving
this information on variables after a section's constants have been
discharged (discharge_function is too early). Surface syntax for
Variable not added yet.


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

1 files changed, 8 insertions, 7 deletions

diff --git a/library/libobject.ml b/library/libobject.ml
index 7c74d402b..b24a46e38 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -28,6 +28,7 @@ let relax b = relax_flag := b;;
 type 'a substitutivity = 
     Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
 
+type discharge_info = (identifier * bool * bool) list
 
 type 'a object_declaration = {
   object_name : string;
@@ -37,7 +38,7 @@ type 'a object_declaration = {
   classify_function : object_name * 'a -> 'a substitutivity;
   subst_function : object_name * substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
-  rebuild_function : 'a -> 'a;
+  rebuild_function : discharge_info * 'a -> 'a;
   export_function : 'a -> 'a option }
 
 let yell s = anomaly s
@@ -51,7 +52,7 @@ let default_object s = {
     yell ("The object "^s^" does not know how to substitute!"));
   classify_function = (fun (_,obj) -> Keep obj);
   discharge_function = (fun _ -> None);
-  rebuild_function = (fun x -> x);
+  rebuild_function = (fun (_,x) -> x);
   export_function = (fun _ -> None)} 
 
 
@@ -77,7 +78,7 @@ type dynamic_object_declaration = {
   dyn_subst_function : object_name * substitution * obj -> obj;
   dyn_classify_function : object_name * obj -> obj substitutivity;
   dyn_discharge_function : object_name * obj -> obj option;
-  dyn_rebuild_function : obj -> obj;
+  dyn_rebuild_function : discharge_info * obj -> obj;
   dyn_export_function : obj -> obj option }
 
 let object_tag lobj = Dyn.tag lobj
@@ -115,8 +116,8 @@ let declare_object odecl =
       Option.map infun (odecl.discharge_function (oname,outfun lobj))
     else 
       anomaly "somehow we got the wrong dynamic object in the dischargefun"
-  and rebuild lobj = 
-    if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj))
+  and rebuild (varinfo,lobj) = 
+    if Dyn.tag lobj = na then infun (odecl.rebuild_function (varinfo,outfun lobj))
     else anomaly "somehow we got the wrong dynamic object in the rebuildfun"
   and exporter lobj = 
     if Dyn.tag lobj = na then 
@@ -173,8 +174,8 @@ let classify_object ((_,lobj) as node) =
 let discharge_object ((_,lobj) as node) = 
   apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj
 
-let rebuild_object lobj =
-  apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj
+let rebuild_object ((_,lobj) as node) =
+  apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function node) lobj
 
 let export_object lobj =
   apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj