Mise en place d'un mecanisme ne chargeant pas les preuves opaques

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

3 files changed, 64 insertions, 11 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e200e7bf31..fb54c16c8f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -481,7 +481,6 @@ let check_imports senv needed =
   in
   List.iter check needed
 
-
 (* we have an inefficiency: Since loaded files are added to the
 environment every time a module is closed, their components are
 calculated many times. Thic could be avoided in several ways:
@@ -505,6 +504,52 @@ let import (dp,mb,depends) digest senv =
 	  loads = (mp,mb)::senv.loads }
 
 
+(** Remove the body of opaque constants in modules *)
+ 
+let rec lighten_module mb =
+  { mb with
+    mod_expr = option_app lighten_modexpr mb.mod_expr;
+    mod_type = lighten_modtype mb.mod_type;
+    mod_user_type = option_app lighten_modtype mb.mod_user_type }
+
+and lighten_modtype = function
+  | MTBident kn as x -> x
+  | MTBfunsig (mbid,mtb1,mtb2) ->
+      MTBfunsig (mbid, lighten_modtype mtb1, lighten_modtype mtb2)
+  | MTBsig (msid,sign) -> MTBsig (msid, lighten_sig sign)
+
+and lighten_modspec ms =
+  { ms with msb_modtype = lighten_modtype ms.msb_modtype }
+
+and lighten_sig sign = 
+  let lighten_spec (l,spec) = (l,match spec with
+    | SPBconst ({const_opaque=true} as x) -> SPBconst {x with const_body=None}
+    | (SPBconst _ | SPBmind _) as x -> x
+    | SPBmodule m -> SPBmodule (lighten_modspec m)
+    | SPBmodtype m -> SPBmodtype (lighten_modtype m))
+  in
+    List.map lighten_spec sign
+
+and lighten_struct struc = 
+  let lighten_body (l,body) = (l,match body with
+    | SEBconst ({const_opaque=true} as x) -> SEBconst {x with const_body=None}
+    | (SEBconst _ | SEBmind _) as x -> x
+    | SEBmodule m -> SEBmodule (lighten_module m)
+    | SEBmodtype m -> SEBmodtype (lighten_modtype m))
+  in
+    List.map lighten_body struc
+
+and lighten_modexpr = function
+  | MEBfunctor (mbid,mty,mexpr) ->
+      MEBfunctor (mbid,lighten_modtype mty,lighten_modexpr mexpr)
+  | MEBident mp as x -> x
+  | MEBstruct (msid, struc) ->
+      MEBstruct (msid, lighten_struct struc)
+  | MEBapply (mexpr,marg,u) ->
+      MEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)
+
+let lighten_library (dp,mb,depends) = (dp,lighten_module mb,depends)
+
 
 type judgment = unsafe_judgment
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 3efe0d16c2..a5d8dc4d10 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -102,6 +102,9 @@ val export : safe_environment -> dir_path
 val import : compiled_library -> Digest.t -> safe_environment 
       -> module_path * safe_environment
 
+(* Remove the body of opaque constants *)
+
+val lighten_library : compiled_library -> compiled_library
 
 (*s Typing judgments *)
 
diff --git a/library/library.ml b/library/library.ml
index bc74043449..c450114b9e 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -339,10 +339,13 @@ let with_magic_number_check f a =
     spc () ++ str"It is corrupted" ++ spc () ++
     str"or was compiled with another version of Coq.")
 
+let lighten_library m = 
+  if !Options.dont_load_proofs then lighten_library m else m
+
 let mk_library md f digest = {
   library_name = md.md_name;
   library_filename = f;
-  library_compiled = md.md_compiled;
+  library_compiled = lighten_library md.md_compiled;
   library_objects = md.md_objects;
   library_deps = md.md_deps;
   library_imports = md.md_imports;
@@ -371,13 +374,16 @@ let rec intern_library (dir, f) =
 	(str ("The file " ^ f ^ " contains library") ++ spc () ++
 	 pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
          spc() ++ pr_dirpath dir);
-    compunit_cache := CompilingLibraryMap.add dir m !compunit_cache;
-    try
-      List.iter (intern_mandatory_library dir) m.library_deps;
-      m
-    with e ->
-      compunit_cache := CompilingLibraryMap.remove dir !compunit_cache; 
-      raise e
+    intern_and_cache_library dir m
+
+and intern_and_cache_library dir m =
+  compunit_cache := CompilingLibraryMap.add dir m !compunit_cache;
+  try
+    List.iter (intern_mandatory_library dir) m.library_deps;
+    m
+  with e ->
+    compunit_cache := CompilingLibraryMap.remove dir !compunit_cache; 
+    raise e
 
 and intern_mandatory_library caller (dir,d) =
   let m = intern_absolute_library_from dir in
@@ -422,8 +428,7 @@ let rec_intern_by_filename_only id f =
        m'.library_filename);
     m.library_name
   with Not_found ->
-    compunit_cache := CompilingLibraryMap.add m.library_name m !compunit_cache;
-    List.iter (intern_mandatory_library m.library_name) m.library_deps;
+    let m = intern_and_cache_library m.library_name m in
     m.library_name
 
 let locate_qualified_library qid =