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

5 files changed, 20 insertions, 19 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 2c5118e928..4f32bbd99d 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -935,7 +935,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   let f_def = Global.lookup_constant (destConst f) in
   let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
   let f_body =
-    force (Option.get f_def.const_body)
+    force (Option.get (body_of_constant f_def))
   in
   let params,f_body_with_params = decompose_lam_n nb_params f_body in
   let (_,num),(_,_,bodies) = destFix f_body_with_params in
@@ -1051,7 +1051,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
       }
     in
     let get_body const =
-      match (Global.lookup_constant const ).const_body with
+      match body_of_constant (Global.lookup_constant const) with
 	| Some b ->
 	     let body = force b in
 	     Tacred.cbv_norm_flags
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1d089409b0..2ba29ced7a 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -445,7 +445,7 @@ let get_funs_constant mp dp =
   in
   function const ->
     let find_constant_body const =
-      match (Global.lookup_constant const ).const_body with
+      match body_of_constant (Global.lookup_constant const) with
 	| Some b ->
 	    let body = force b in
 	    let body = Tacred.cbv_norm_flags
@@ -579,7 +579,7 @@ let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition
     let finfos = find_Function_infos this_block_funs.(0) in
     try
       let equation =  Option.get finfos.equation_lemma in
-      (Global.lookup_constant equation).Declarations.const_opaque
+      Declarations.is_opaque (Global.lookup_constant equation)
     with Option.IsNone -> (* non recursive definition *)
       false
   in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 38492f88b5..dd48765fb5 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -834,7 +834,7 @@ let make_graph (f_ref:global_reference) =
       | _ -> raise (UserError ("", str "Not a function reference") )
   in
   Dumpglob.pause ();
-  (match c_body.const_body with
+  (match body_of_constant c_body with
      | None -> error "Cannot build a graph over an axiom !"
      | Some b ->
 	 let env = Global.env () in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 1de0f91d15..094d2e50fd 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -120,9 +120,9 @@ let const_of_id id =
 let def_of_const t =
    match (Term.kind_of_term t) with
     Term.Const sp ->
-      (try (match (Global.lookup_constant sp) with
-             {Declarations.const_body=Some c} -> Declarations.force c
-	     |_ -> assert false)
+      (try (match Declarations.body_of_constant (Global.lookup_constant sp) with
+             | Some c -> Declarations.force c
+	     | _ -> assert false)
        with _ -> assert false)
     |_ -> assert false
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 4217b83faf..11fbc01baf 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -136,9 +136,9 @@ let message s = if Flags.is_verbose () then msgnl(str s);;
 let def_of_const t =
    match (kind_of_term t) with
     Const sp ->
-      (try (match (Global.lookup_constant sp) with
-             {const_body=Some c} -> Declarations.force c
-	     |_ -> assert false)
+      (try (match body_of_constant (Global.lookup_constant sp) with
+             | Some c -> Declarations.force c
+	     | _ -> assert false)
        with _ ->
 	 anomaly ("Cannot find definition of constant "^
 		    (string_of_id (id_of_label (con_label sp))))
@@ -939,6 +939,13 @@ let build_new_goal_type () =
   let res = build_and_l sub_gls_types in
   res
 
+let is_opaque_constant c =
+  let cb = Global.lookup_constant c in
+  match cb.Declarations.const_body with
+    | Declarations.OpaqueDef _ -> true
+    | Declarations.Undef _ -> true
+    | Declarations.Def _ -> false
+
 let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal)   =
   (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
   let current_proof_name = get_current_proof_name () in
@@ -958,10 +965,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
       let na_ref = Libnames.Ident (dummy_loc,na) in
       let na_global = Nametab.global na_ref in
       match na_global with
-	  ConstRef c ->
-	    let cb = Global.lookup_constant c in
-	    if cb.Declarations.const_opaque then true
-	    else begin  match cb.const_body with None -> true | _ -> false end
+	  ConstRef c -> is_opaque_constant c
 	| _ -> anomaly "equation_lemma: not a constant"
     in
     let lemma = mkConst (Lib.make_con na) in
@@ -1339,10 +1343,7 @@ let (com_eqn : int -> identifier ->
   fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type ->
     let opacity =
       match terminate_ref with
-	| ConstRef c ->
-	    let cb = Global.lookup_constant c in
-	    if cb.Declarations.const_opaque then true
-	    else begin match cb.const_body with None -> true | _ -> false end
+	| ConstRef c -> is_opaque_constant c
 	| _ -> anomaly "terminate_lemma: not a constant"
     in
     let (evmap, env) = Lemmas.get_current_context() in