Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks

 The recent experiment with -dont-load-proofs in the stdlib showed that
 this options isn't fully safe: some axioms were generated (Include ?
 functor application ? This is still to be fully understood).

 Instead, I've implemented an idea of Yann: only load opaque proofs when
 we need them. This is almost as fast as -dont-load-proofs (on the stdlib,
 we're now 15% faster than before instead of 20% faster with -dont-load-proofs),
 but fully compatible with Coq standard behavior.

 Technically, the const_body field of Declarations.constant_body now regroup
 const_body + const_opaque + const_inline in a ternary type. It is now either:
  - Undef : an axiom or parameter, with an inline info
  - Def : a transparent definition, with a constr_substituted
  - OpaqueDef : an opaque definition, with a lazy constr_substitued
 Accessing the lazy constr of an OpaqueDef might trigger the read on disk of
 the final section of a .vo, where opaque proofs are located.

 Some functions (body_of_constant, is_opaque, constant_has_body) emulate
 the behavior of the old fields. The rest of Coq (including the checker)
 has been adapted accordingly, either via direct access to the new const_body
 or via these new functions. Many places look nicer now (ok, subjective notion).

 There are now three options: -lazy-load-proofs (default), -force-load-proofs
 (earlier semantics), -dont-load-proofs. Note that -outputstate now implies
 -force-load-proofs (otherwise the marshaling fails on some delayed lazy).

 On the way, I fixed what looked like a bug : a module type
 (T with Definition x := c) was accepted even when x in T was opaque.
 I also tried to clarify Subtyping.check_constant.

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

1 files changed, 32 insertions, 31 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 335c2a94e..aad541d21 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -84,40 +84,41 @@ and check_with_aux_def env sign with_decl mp equiv =
           | With_Definition ([],_) -> assert false
 	  | With_Definition ([id],c) ->
 	      let cb = match spec with
-		  SFBconst cb -> cb
+		| SFBconst cb -> cb
 		| _ -> error_not_a_constant l
 	      in
-		begin
-		  match cb.const_body with
-		    | None ->
-			let (j,cst1) = Typeops.infer env' c in
-			let typ = Typeops.type_of_constant_type env' cb.const_type in
-			let cst2 = Reduction.conv_leq env' j.uj_type typ in
-			let cst =
-			  union_constraints
-			    (union_constraints cb.const_constraints cst1)
-			    cst2 in
-			let body = Some (Declarations.from_val j.uj_val) in
-			let cb' = {cb with
-				     const_body = body;
-				     const_body_code = Cemitcodes.from_val
-                            (compile_constant_body env' body false);
-                                     const_constraints = cst} in
-			  SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
-		    | Some b ->
-			let cst1 = Reduction.conv env' c (Declarations.force b) in
-			let cst = union_constraints cb.const_constraints cst1 in
-			let body = Some (Declarations.from_val c) in
-			let cb' = {cb with
-				     const_body = body;
-				     const_body_code = Cemitcodes.from_val
-                            (compile_constant_body env' body false);
-                                     const_constraints = cst} in
-			  SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
-	      end
+	      let def,cst = match cb.const_body with
+		| Undef _ ->
+		    let (j,cst1) = Typeops.infer env' c in
+		    let typ = Typeops.type_of_constant_type env' cb.const_type in
+		    let cst2 = Reduction.conv_leq env' j.uj_type typ in
+		    let cst =
+		      union_constraints
+			(union_constraints cb.const_constraints cst1)
+			cst2
+		    in
+		    let def = Def (Declarations.from_val j.uj_val) in
+		    def,cst
+		| Def cs ->
+		    let cst1 = Reduction.conv env' c (Declarations.force cs) in
+		    let cst = union_constraints cb.const_constraints cst1 in
+		    let def = Def (Declarations.from_val c) in
+		    def,cst
+		| OpaqueDef _ ->
+		    (* We cannot make transparent an opaque field *)
+		    raise Reduction.NotConvertible
+	      in
+	      let cb' =
+		{ cb with
+		  const_body = def;
+		  const_body_code =
+		    Cemitcodes.from_val (compile_constant_body env' def);
+		  const_constraints = cst }
+	      in
+	      SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
 	  | With_Definition (_::_,c) ->
 	      let old = match spec with
-		  SFBmodule msb -> msb
+		| SFBmodule msb -> msb
 		| _ -> error_not_a_module (string_of_label l)
 	      in
 		begin
@@ -136,7 +137,7 @@ and check_with_aux_def env sign with_decl mp equiv =
 		end
 	  | _ -> anomaly "Modtyping:incorrect use of with"
     with
-	Not_found -> error_no_such_label l
+      | Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_incorrect_with_constraint l
 
 and check_with_aux_mod env sign with_decl mp equiv =