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

1 files changed, 23 insertions, 13 deletions

diff --git a/checker/declarations.ml b/checker/declarations.ml
index af8b1f217..cfaa2f5f7 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -480,24 +480,34 @@ let subst_substituted s r =
 
 let force_constr = force subst_mps
 
+let from_val c = ref (LSval c)
+
 type constr_substituted = constr substituted
 
 let val_cstr_subst = val_substituted val_constr
 
 let subst_constr_subst = subst_substituted
 
-(** Beware! In .vo files, lazy_constr are stored as integers
-   used as indexes for a separate table. The actual lazy_constr is restored
-   later, by [Safe_typing.LightenLibrary.load]. This allows us
-   to use here a different definition of lazy_constr than coqtop:
-   since the checker will inspect all proofs parts, even opaque
-   ones, no need to use Lazy.t here *)
+(* Nota : in coqtop, the [lazy_constr] type also have a [Direct]
+   constructor, but it shouldn't occur inside a .vo, so we ignore it *)
+
+type lazy_constr =
+  | Indirect of substitution list * DirPath.t * int
+(* | Direct of constr_substituted *)
+
+let subst_lazy_constr sub = function
+  | Indirect (l,dp,i) -> Indirect (sub::l,dp,i)
+
+let indirect_opaque_access =
+  ref ((fun dp i -> assert false) : DirPath.t -> int -> constr)
+
+let force_lazy_constr = function
+  | Indirect (l,dp,i) ->
+    let c = !indirect_opaque_access dp i in
+    force_constr (List.fold_right subst_constr_subst l (from_val c))
 
-type lazy_constr = constr_substituted
-let subst_lazy_constr = subst_substituted
-let force_lazy_constr = force_constr
-let lazy_constr_from_val c = c
-let val_lazy_constr = val_cstr_subst
+let val_lazy_constr =
+  val_sum "lazy_constr" 0 [|[|val_list val_subst;val_dp;val_int|]|]
 
 (** Inlining level of parameters at functor applications.
     This is ignored by the checker. *)
@@ -532,8 +542,8 @@ type constant_body = {
 
 let body_of_constant cb = match cb.const_body with
   | Undef _ -> None
-  | Def c -> Some c
-  | OpaqueDef c -> Some c
+  | Def c -> Some (force_constr c)
+  | OpaqueDef c -> Some (force_lazy_constr c)
 
 let constant_has_body cb = match cb.const_body with
   | Undef _ -> false