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

12 files changed, 58 insertions, 68 deletions

diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index 00a76efa35..b025cea64a 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -468,7 +468,7 @@ and axiomatize_body env r id d = match r with
   | VarRef _ ->
       assert false
   | ConstRef c ->
-      begin match (Global.lookup_constant c).const_body with
+      begin match body_of_constant (Global.lookup_constant c) with
 	| Some b ->
 	    let b = force b in
 	    let axioms =
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 04d1f2a8de..c4dce1c7b4 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -130,12 +130,12 @@ let check_arity env cb =
 
 let check_fix env cb i =
   match cb.const_body with
-    | None -> raise Impossible
-    | Some lbody ->
-	match kind_of_term (Declarations.force lbody) with
+    | Def lbody ->
+	(match kind_of_term (Declarations.force lbody) with
 	  | Fix ((_,j),recd) when i=j -> check_arity env cb; (true,recd)
 	  | CoFix (j,recd) when i=j -> check_arity env cb; (false,recd)
-	  | _ -> raise Impossible
+	  | _ -> raise Impossible)
+    | Undef _ | OpaqueDef _ -> raise Impossible
 
 let factor_fix env l cb msb =
   let _,recd as check = check_fix env cb 0 in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 51d79e821e..992f8fca68 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -245,7 +245,7 @@ let rec extract_type env db j c args =
 	(match flag_of_type env typ with
 	   | (Info, TypeScheme) ->
 	       let mlt = extract_type_app env db (r, type_sign env typ) args in
-	       (match cb.const_body with
+	       (match body_of_constant cb with
 		  | None -> mlt
 		  | Some _ when is_custom r -> mlt
 		  | Some lbody ->
@@ -258,7 +258,7 @@ let rec extract_type env db j c args =
 		      (* If possible, we take [mlt], otherwise [mlt']. *)
 		      if expand env mlt = expand env mlt' then mlt else mlt')
 	   | _ -> (* only other case here: Info, Default, i.e. not an ML type *)
-	       (match cb.const_body with
+	       (match body_of_constant cb with
 		  | None -> Tunknown (* Brutal approximation ... *)
 		  | Some lbody ->
 		      (* We try to reduce. *)
@@ -478,7 +478,7 @@ and mlt_env env r = match r with
        with Not_found ->
 	 let cb = Environ.lookup_constant kn env in
 	 let typ = Typeops.type_of_constant_type env cb.const_type in
-	 match cb.const_body with
+	 match body_of_constant cb with
 	   | None -> None
 	   | Some l_body ->
 	       (match flag_of_type env typ with
@@ -904,15 +904,9 @@ let extract_fixpoint env vkn (fi,ti,ci) =
 let extract_constant env kn cb =
   let r = ConstRef kn in
   let typ = Typeops.type_of_constant_type env cb.const_type in
-  let warn_info_none () =
-    if not (is_custom r) then begin
-      add_info_axiom r;
-      if not !Flags.load_proofs && cb.const_opaque then add_opaque_ko r
-    end
-  in
-  let warn_info_some () = if cb.const_opaque then add_opaque_ok r
-  in
-  match cb.const_body with
+  let warn_info_none () = if not (is_custom r) then add_info_axiom r in
+  let warn_info_some () = if is_opaque cb then add_opaque r in
+  match body_of_constant cb with
     | None ->
         (match flag_of_type env typ with
 	   | (Info,TypeScheme) ->
@@ -951,7 +945,7 @@ let extract_constant_spec env kn cb =
     | (Logic, Default) -> Sval (r, Tdummy Kother)
     | (Info, TypeScheme) ->
 	let s,vl = type_sign_vl env typ in
-	(match cb.const_body with
+	(match body_of_constant cb with
 	  | None -> Stype (r, vl, None)
 	  | Some body ->
 	      let db = db_from_sign s in
@@ -966,7 +960,7 @@ let extract_with_type env cb =
   match flag_of_type env typ with
     | (Info, TypeScheme) ->
 	let s,vl = type_sign_vl env typ in
-	let body = Option.get cb.const_body in
+	let body = Option.get (body_of_constant cb) in
 	let db = db_from_sign s in
 	let t = extract_type_scheme env db (force body) (List.length s) in
 	Some (vl, t)
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 3036cb1340..4ab7b6f750 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1205,12 +1205,14 @@ let inline_test r t =
   if not (auto_inline ()) then false
   else
     let c = match r with ConstRef c -> c | _ -> assert false in
-    let body = try (Global.lookup_constant c).const_body with _ -> None in
-    if body = None then false
-    else
-      let t1 = eta_red t in
-      let t2 = snd (collect_lams t1) in
-      not (is_fix t2) && ml_size t < 12 && is_not_strict t
+    let has_body =
+      try constant_has_body (Global.lookup_constant c)
+      with _ -> false
+    in
+    has_body &&
+      (let t1 = eta_red t in
+       let t2 = snd (collect_lams t1) in
+       not (is_fix t2) && ml_size t < 12 && is_not_strict t)
 
 let con_of_string s =
   let null = empty_dirpath in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 8c9fdf37da..35494d3d2d 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -175,14 +175,10 @@ let add_info_axiom r = info_axioms := Refset'.add r !info_axioms
 let remove_info_axiom r = info_axioms := Refset'.remove r !info_axioms
 let add_log_axiom r = log_axioms := Refset'.add r !log_axioms
 
-let opaques_ok = ref Refset'.empty
-let opaques_ko = ref Refset'.empty
-let init_opaques () = opaques_ok := Refset'.empty; opaques_ko := Refset'.empty
-let add_opaque_ok r = opaques_ok := Refset'.add r !opaques_ok
-let add_opaque_ko r = opaques_ko := Refset'.add r !opaques_ko
-let remove_opaque r =
-  opaques_ok := Refset'.remove r !opaques_ok;
-  opaques_ko := Refset'.remove r !opaques_ko
+let opaques = ref Refset'.empty
+let init_opaques () = opaques := Refset'.empty
+let add_opaque r = opaques := Refset'.add r !opaques
+let remove_opaque r = opaques := Refset'.remove r !opaques
 
 (*s Extraction modes: modular or monolithic, library or minimal ?
 
@@ -263,23 +259,19 @@ let warning_axioms () =
        str "Having invalid logical axiom in the environment when extracting" ++
        spc () ++ str "may lead to incorrect or non-terminating ML terms." ++
        fnl ())
-  end
+  end;
+  if !Flags.load_proofs = Flags.Dont && info_axioms@log_axioms <> [] then
+    msg_warning
+      (str "Some of these axioms might by due to option -dont-load-proofs.")
 
 let warning_opaques () =
-  let opaques_ok = Refset'.elements !opaques_ok in
-  if opaques_ok = [] then ()
+  let opaques = Refset'.elements !opaques in
+  if opaques = [] then ()
   else msg_warning
     (str "Extraction is accessing the body of the following opaque constants:"
-     ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques_ok)
+     ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques)
      ++ str "." ++ fnl ()
-     ++ str "Be careful if using option -dont-load-proofs later." ++ fnl ());
-  let opaques_ko = Refset'.elements !opaques_ko in
-  if opaques_ko = [] then ()
-  else msg_warning
-    (str "Extraction cannot access the body of the following opaque constants:"
-     ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques_ko)
-     ++ fnl () ++ str "due to option -dont-load-proofs. "
-     ++ str "These constants are treated as axioms." ++ fnl ())
+     ++ str "Be careful if using option -dont-load-proofs later." ++ fnl ())
 
 let warning_both_mod_and_cst q mp r =
  msg_warning
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 158e33ec92..97c28b154a 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -84,8 +84,7 @@ val add_info_axiom : global_reference -> unit
 val remove_info_axiom : global_reference -> unit
 val add_log_axiom : global_reference -> unit
 
-val add_opaque_ok : global_reference -> unit
-val add_opaque_ko : global_reference -> unit
+val add_opaque : global_reference -> unit
 val remove_opaque : global_reference -> unit
 
 val reset_tables : unit -> unit
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
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index f0a5089cc7..78048c8ee6 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -527,8 +527,10 @@ let print internal glob_ref kind xml_library_root =
         Cic2acic.Variable kn,mk_variable_obj id body typ
     | Ln.ConstRef kn ->
        let id = N.id_of_label (N.con_label kn) in
-       let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
-        G.lookup_constant kn in
+       let cb = G.lookup_constant kn in
+       let val0 = D.body_of_constant cb in
+       let typ = cb.D.const_type in
+       let hyps = cb.D.const_hyps in
        let typ = Typeops.type_of_constant_type (Global.env()) typ in
         Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
     | Ln.IndRef (kn,_) ->