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, 33 insertions, 46 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 04d1f2a8d..c4dce1c7b 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 51d79e821..992f8fca6 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 3036cb134..4ab7b6f75 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 8c9fdf37d..35494d3d2 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 158e33ec9..97c28b154 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