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, 27 insertions, 8 deletions

diff --git a/kernel/lazyconstr.mli b/kernel/lazyconstr.mli
index 17c9bcc76b..f6188f5364 100644
--- a/kernel/lazyconstr.mli
+++ b/kernel/lazyconstr.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Names
 open Term
 open Mod_subst
 
@@ -19,16 +20,34 @@ val force : constr_substituted -> constr
 val subst_constr_subst :
   substitution -> constr_substituted -> constr_substituted
 
-(** Opaque proof terms are not loaded immediately, but are there
-    in a lazy form. Forcing this lazy may trigger some unmarshal of
-    the necessary structure. *)
+(** Opaque proof terms might be in some external tables. The
+    [force_opaque] function below allows to access these tables,
+    this might trigger the read of some extra parts of .vo files *)
 
 type lazy_constr
 
-val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr
-val force_lazy_constr : lazy_constr -> constr_substituted
-val make_lazy_constr : constr_substituted Lazy.t -> lazy_constr
-val lazy_constr_is_val : lazy_constr -> bool
+(** From a [constr] to some (immediate) [lazy_constr]. *)
+val opaque_from_val : constr -> lazy_constr
+
+(** Turn an immediate [lazy_constr] into an indirect one, thanks
+    to the indirect opaque creator configured below. *)
+val turn_indirect : lazy_constr -> lazy_constr
 
+(** From a [lazy_constr] back to a [constr]. This might use the
+    indirect opaque accessor configured below. *)
 val force_opaque : lazy_constr -> constr
-val opaque_from_val : constr -> lazy_constr
+
+val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr
+
+val hcons_lazy_constr : lazy_constr -> lazy_constr
+
+(** When stored indirectly, opaque terms are indexed by their library
+    dirpath and an integer index. The following two functions activate
+    this indirect storage, by telling how to store and retrieve terms.
+    Default creator always returns [None], preventing the creation of
+    any indirect link, and default accessor always raises an error.
+*)
+
+val set_indirect_opaque_creator : (constr -> (DirPath.t * int) option) -> unit
+val set_indirect_opaque_accessor : (DirPath.t -> int -> constr) -> unit
+val reset_indirect_opaque_creator : unit -> unit