Revised infrastructure for lazy loading of opaque proofs

 Get rid of the LightenLibrary hack : no more last-minute
 collect of opaque terms and Obj.magic tricks. Instead, we
 make coqc accumulate the opaque terms as soon as constant_bodies
 are created outside sections. In these cases, the opaque
 terms are placed in a special table, and some (DirPath.t * int)
 are used as indexes in constant_body. In an interactive session,
 the local opaque terms stay directly stored in the constant_body.

 The structure of .vo file stays similar : magic number, regular
 library structure, digest of the first part, array of opaque terms.
 In addition, we now have a final checksum for checking the
 integrity of the whole .vo file. The other difference is that
 lazy_constr aren't changed into int indexes in .vo files, but are
 now coded as (substitution list * DirPath.t * int). In particular
 this approach allows to refer to opaque terms from another
 library. This (and accumulating substitutions in lazy_constr)
 seems to greatly help decreasing the size of opaque tables :
 -20% of vo size on the standard library :-). The compilation times
 are slightly better, but that can be statistic noise.

 The -force-load-proofs isn't active anymore : it behaves now
 just like -lazy-load-proofs. The -dont-load-proofs mode has
 slightly changed : opaque terms aren't seen as axioms anymore,
 but accessing their bodies will raise an error.

 Btw, API change : Declareops.body_of_constant now produces directly
 a constr option instead of a constr_substituted option

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

6 files changed, 7 insertions, 12 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ef4dca26d..74d719438 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -940,8 +940,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 (*   observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
   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 =
-    Lazyconstr.force (Option.get (body_of_constant f_def))
+  let f_body = 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
@@ -1058,8 +1057,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
     in
     let get_body const =
       match body_of_constant (Global.lookup_constant const) with
-	| Some b ->
-	     let body = Lazyconstr.force b in
+	| Some body ->
 	     Tacred.cbv_norm_flags
 	       (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
 	       (Global.env ())
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 09637d273..50a4703f6 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -403,8 +403,7 @@ let get_funs_constant mp dp =
   function const ->
     let find_constant_body const =
       match body_of_constant (Global.lookup_constant const) with
-	| Some b ->
-	    let body = Lazyconstr.force b in
+	| Some body ->
 	    let body = Tacred.cbv_norm_flags
 	      (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
 	      (Global.env ())
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f0f76860a..609e2916d 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -766,9 +766,8 @@ let make_graph (f_ref:global_reference) =
   Dumpglob.pause ();
   (match body_of_constant c_body with
      | None -> error "Cannot build a graph over an axiom !"
-     | Some b ->
+     | Some body ->
 	 let env = Global.env () in
-	 let body = Lazyconstr.force b in
 	 let extern_body,extern_type =
 	   with_full_print
 	     (fun () ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 4d1cefe5a..1e8f4afdf 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -116,7 +116,7 @@ let def_of_const t =
    match (Term.kind_of_term t) with
     Term.Const sp ->
       (try (match Declareops.body_of_constant (Global.lookup_constant sp) with
-             | Some c -> Lazyconstr.force c
+             | Some c -> c
 	     | _ -> assert false)
        with Not_found -> assert false)
     |_ -> assert false
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 597233d01..a8ffd51ef 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -69,7 +69,7 @@ let def_of_const t =
    match (kind_of_term t) with
     Const sp ->
       (try (match body_of_constant (Global.lookup_constant sp) with
-             | Some c -> Lazyconstr.force c
+             | Some c -> c
 	     | _ -> raise Not_found)
        with Not_found ->
 	 anomaly (str "Cannot find definition of constant " ++
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index a34d4a682..ddc4725c3 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -229,8 +229,7 @@ let mk_constant_obj id bo ty variables hyps =
       Acic.Constant (Names.Id.to_string id,None,ty,params)
    | Some c ->
       Acic.Constant
-       (Names.Id.to_string id, Some (Unshare.unshare (Lazyconstr.force c)),
-         ty,params)
+       (Names.Id.to_string id, Some (Unshare.unshare c), ty,params)
 ;;
 
 let mk_inductive_obj sp mib packs variables nparams hyps finite =