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

7 files changed, 108 insertions, 203 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 90327da6c..3c1f6a415 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -18,8 +18,8 @@ open Util
 
 let body_of_constant cb = match cb.const_body with
   | Undef _ -> None
-  | Def c -> Some c
-  | OpaqueDef lc -> Some (force_lazy_constr lc)
+  | Def c -> Some (Lazyconstr.force c)
+  | OpaqueDef lc -> Some (Lazyconstr.force_opaque lc)
 
 let constant_has_body cb = match cb.const_body with
   | Undef _ -> false
@@ -84,14 +84,8 @@ let hcons_const_type = function
 
 let hcons_const_def = function
   | Undef inl -> Undef inl
-  | Def l_constr ->
-    let constr = force l_constr in
-    Def (from_val (Term.hcons_constr constr))
-  | OpaqueDef lc ->
-    if lazy_constr_is_val lc then
-      let constr = force_opaque lc in
-      OpaqueDef (opaque_from_val (Term.hcons_constr constr))
-    else OpaqueDef lc
+  | Def cs -> Def (from_val (Term.hcons_constr (Lazyconstr.force cs)))
+  | OpaqueDef lc -> OpaqueDef (Lazyconstr.hcons_lazy_constr lc)
 
 let hcons_const_body cb =
   { cb with
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 1616e4639..c4d67ba52 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -8,7 +8,6 @@
 
 open Declarations
 open Mod_subst
-open Lazyconstr
 
 (** Operations concerning types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
@@ -18,13 +17,14 @@ open Lazyconstr
 val subst_const_def : substitution -> constant_def -> constant_def
 val subst_const_body : substitution -> constant_body -> constant_body
 
-(** Is there a actual body in const_body or const_body_opaque ? *)
+(** Is there a actual body in const_body ? *)
 
 val constant_has_body : constant_body -> bool
 
-(** Accessing const_body_opaque or const_body *)
+(** Accessing const_body, forcing access to opaque proof term if needed.
+    Only use this function if you know what you're doing. *)
 
-val body_of_constant : constant_body -> constr_substituted option
+val body_of_constant : constant_body -> Term.constr option
 
 val is_opaque : constant_body -> bool
 
diff --git a/kernel/lazyconstr.ml b/kernel/lazyconstr.ml
index 31cb76575..21aba6348 100644
--- a/kernel/lazyconstr.ml
+++ b/kernel/lazyconstr.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Names
 open Term
 open Mod_subst
 
@@ -20,24 +21,56 @@ let force = force subst_mps
 
 let subst_constr_subst = subst_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. The ['a substituted] type isn't really great
-    here, so we store "manually" a substitution list, the younger one at top.
+(** 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.
+    In the [Indirect] case, we accumulate "manually" a substitution
+    list, the younger one coming first. Nota: no [Direct] constructor
+    should end in a .vo, this is checked by coqchk.
 *)
 
-type lazy_constr = constr_substituted Lazy.t * substitution list
+type lazy_constr =
+  | Indirect of substitution list * DirPath.t * int (* lib,index *)
+  | Direct of constr_substituted (* opaque in section or interactive session *)
 
-let force_lazy_constr (c,l) =
-  List.fold_right subst_constr_subst l (Lazy.force c)
+(* TODO : this hcons function could probably be improved (for instance
+   hash the dir_path in the Indirect case) *)
 
-let lazy_constr_is_val (c,_) = Lazy.lazy_is_val c
+let hcons_lazy_constr = function
+  | Direct c -> Direct (from_val (hcons_constr (force c)))
+  | Indirect _ as lc -> lc
 
-let make_lazy_constr c = (c, [])
+let subst_lazy_constr sub = function
+  | Direct cs -> Direct (subst_constr_subst sub cs)
+  | Indirect (l,dp,i) -> Indirect (sub::l,dp,i)
 
-let force_opaque lc = force (force_lazy_constr lc)
+let default_get_opaque dp _ =
+  Errors.error
+    ("Cannot access an opaque term in library " ^ DirPath.to_string dp)
+
+let default_mk_opaque _ = None
+
+let get_opaque = ref default_get_opaque
+let mk_opaque = ref default_mk_opaque
+let set_indirect_opaque_accessor f = (get_opaque := f)
+let set_indirect_opaque_creator f = (mk_opaque := f)
+let reset_indirect_opaque_creator () = (mk_opaque := default_mk_opaque)
 
-let opaque_from_val c = (Lazy.lazy_from_val (from_val c), [])
+let force_lazy_constr = function
+  | Direct c -> c
+  | Indirect (l,dp,i) ->
+    List.fold_right subst_constr_subst l (from_val (!get_opaque dp i))
 
-let subst_lazy_constr sub (c,l) = (c,sub::l)
+let turn_indirect lc = match lc with
+  | Indirect _ ->
+    Errors.anomaly (Pp.str "Indirecting an already indirect opaque")
+  | Direct c ->
+    (* this constr_substituted shouldn't have been substituted yet *)
+    assert (fst (Mod_subst.repr_substituted c) == None);
+    match !mk_opaque (force c) with
+      | None -> lc
+      | Some (dp,i) -> Indirect ([],dp,i)
+
+let force_opaque lc = force (force_lazy_constr lc)
 
+let opaque_from_val c = Direct (from_val c)
diff --git a/kernel/lazyconstr.mli b/kernel/lazyconstr.mli
index 17c9bcc76..f6188f536 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
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 20ca16476..a1b820466 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -272,6 +272,13 @@ let add_constant dir l decl senv =
       let cb = Term_typing.translate_recipe senv.env r in
       if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
   in
+  let cb = match cb.const_body with
+    | OpaqueDef lc when DirPath.is_empty dir ->
+      (* In coqc, opaque constants outside sections will be stored
+         indirectly in a specific table *)
+      { cb with const_body = OpaqueDef (Lazyconstr.turn_indirect lc) }
+    | _ -> cb
+  in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
   let senv'' = match cb.const_body with
     | Undef (Some lev) ->
@@ -767,148 +774,6 @@ let import lib digest senv =
   mp, senv, lib.comp_natsymbs
 
 
- (* Store the body of modules' opaque constants inside a table.  
-
-    This module is used during the serialization and deserialization
-    of vo files. 
-
-    By adding an indirection to the opaque constant definitions, we
-    gain the ability not to load them. As these constant definitions
-    are usually big terms, we save a deserialization time as well as
-    some memory space. *)
-module LightenLibrary : sig
-  type table 
-  type lightened_compiled_library 
-  val save : compiled_library -> lightened_compiled_library * table
-  val load : load_proof:Flags.load_proofs -> table Lazy.t
-    -> lightened_compiled_library -> compiled_library
-end = struct
-
-  (* The table is implemented as an array of [constr_substituted].
-     Keys are hence integers. To avoid changing the [compiled_library]
-     type, we brutally encode integers into [lazy_constr]. This isn't
-     pretty, but shouldn't be dangerous since the produced structure
-     [lightened_compiled_library] is abstract and only meant for writing
-     to .vo via Marshal (which doesn't care about types).
-  *)
-  type table = Lazyconstr.constr_substituted array
-  let key_as_lazy_constr (i:int) = (Obj.magic i : Lazyconstr.lazy_constr)
-  let key_of_lazy_constr (c:Lazyconstr.lazy_constr) = (Obj.magic c : int)
-
-  (* To avoid any future misuse of the lightened library that could 
-     interpret encoded keys as real [constr_substituted], we hide 
-     these kind of values behind an abstract datatype. *)
-  type lightened_compiled_library = compiled_library
-
-  (* Map a [compiled_library] to another one by just updating 
-     the opaque term [t] to [on_opaque_const_body t]. *)
-  let traverse_library on_opaque_const_body =
-    let rec traverse_module mb =
-      match mb.mod_expr with 
-	  None -> 
-	    { mb with
-		mod_expr = None;
-		mod_type = traverse_modexpr mb.mod_type;
-	    }
-	| Some impl when impl == mb.mod_type-> 
-	    let mtb =  traverse_modexpr mb.mod_type in 
-	      { mb with
-		  mod_expr = Some mtb;
-		  mod_type = mtb;
-	      }    
-	| Some impl -> 
-	    { mb with
-		mod_expr = Option.map traverse_modexpr mb.mod_expr;
-		mod_type = traverse_modexpr mb.mod_type;
-	    }    
-    and traverse_struct struc =
-      let traverse_body (l,body) = (l,match body with
-	| SFBconst cb when Declareops.is_opaque cb ->
-	  SFBconst {cb with const_body = on_opaque_const_body cb.const_body}
-	| (SFBconst _ | SFBmind _ ) as x ->
-	  x
-	| SFBmodule m -> 
-	  SFBmodule (traverse_module m)
-	| SFBmodtype m -> 
-	  SFBmodtype ({m with typ_expr = traverse_modexpr m.typ_expr}))
-      in
-      List.map traverse_body struc
-	
-    and traverse_modexpr = function
-      | SEBfunctor (mbid,mty,mexpr) ->
-	SEBfunctor (mbid,
-		    ({mty with
-		      typ_expr = traverse_modexpr mty.typ_expr}),
-		    traverse_modexpr mexpr)
-      | SEBident mp as x -> x
-      | SEBstruct (struc) ->
-	SEBstruct  (traverse_struct struc)
-      | SEBapply (mexpr,marg,u) ->
-	SEBapply (traverse_modexpr mexpr,traverse_modexpr marg,u)
-      | SEBwith (seb,wdcl) ->
-	SEBwith (traverse_modexpr seb,wdcl)
-    in
-    fun clib -> { clib with comp_mod = traverse_module clib.comp_mod }
-
-  (* To disburden a library from opaque definitions, we simply 
-     traverse it and add an indirection between the module body 
-     and its reference to a [const_body]. *)
-  let save library = 
-    let ((insert    : constant_def -> constant_def),
-	 (get_table : unit -> table)) = 
-      (* We use an integer as a key inside the table. *)
-      let counter = ref (-1) in
-
-      (* During the traversal, the table is implemented by a list 
-	 to get constant time insertion. *)
-      let opaque_definitions = ref [] in
-      
-      ((* Insert inside the table. *) 
-	(fun def ->
-	  let opaque_definition = match def with
-	    | OpaqueDef lc -> Lazyconstr.force_lazy_constr lc
-	    | _ -> assert false
-	  in
-	  incr counter;
-	  opaque_definitions := opaque_definition :: !opaque_definitions;
-	  OpaqueDef (key_as_lazy_constr !counter)),
-
-       (* Get the final table representation. *)
-       (fun () -> Array.of_list (List.rev !opaque_definitions)))
-    in
-    let lightened_library = traverse_library insert library in
-    (lightened_library, get_table ())
-
-  (* Loading is also a traversing that decodes the embedded keys that
-     are inside the [lightened_library]. If the [load_proof] flag is
-     set, we lookup inside the table to graft the
-     [constr_substituted]. Otherwise, we set the [const_body] field
-     to [None]. 
-  *)
-  let load ~load_proof (table : table Lazy.t) lightened_library =
-    let decode_key = function
-      | Undef _ | Def _ -> assert false
-      | OpaqueDef k ->
-	  let k = key_of_lazy_constr k in
-	  let access key =
-	    try (Lazy.force table).(key)
-	    with e when Errors.noncritical e ->
-              error "Error while retrieving an opaque body"
-	  in
-	  match load_proof with
-	    | Flags.Force ->
-	      let lc = Lazy.lazy_from_val (access k) in
-	      OpaqueDef (Lazyconstr.make_lazy_constr lc)
-	    | Flags.Lazy ->
-	      let lc = lazy (access k) in
-	      OpaqueDef (Lazyconstr.make_lazy_constr lc)
-	    | Flags.Dont ->
-	      Undef None
-    in
-    traverse_library decode_key lightened_library
-
-end
-
 type judgment = unsafe_judgment
 
 let j_val j = j.uj_val
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 1bb43a53e..cd24bd8d0 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -112,17 +112,6 @@ val export : safe_environment -> DirPath.t
 val import : compiled_library -> Digest.t -> safe_environment
       -> module_path * safe_environment * Nativecode.symbol array
 
-(** Remove the body of opaque constants *)
-
-module LightenLibrary :
-sig
-  type table
-  type lightened_compiled_library
-  val save : compiled_library -> lightened_compiled_library * table
-  val load : load_proof:Flags.load_proofs -> table Lazy.t ->
-    lightened_compiled_library -> compiled_library
-end
-
 (** {6 Typing judgments } *)
 
 type judgment
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index c70a3f2eb..67d80fa50 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -80,26 +80,31 @@ let global_vars_set_constant_type env = function
 	  (fun t c -> Id.Set.union (global_vars_set env t) c))
       ctx ~init:Id.Set.empty
 
+let check_declared_variables declared inferred =
+  let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
+  let undeclared_set = Id.Set.diff (mk_set inferred) (mk_set declared) in
+  if not (Id.Set.is_empty undeclared_set) then
+    error ("The following section variables are used but not declared:\n"^
+              (String.concat ", "
+                 (List.map Id.to_string (Id.Set.elements undeclared_set))))
+
 let build_constant_declaration env (def,typ,cst,inline_code,ctx) =
-  let hyps = 
+  let hyps =
     let inferred =
       let ids_typ = global_vars_set_constant_type env typ in
       let ids_def = match def with
-      | Undef _ -> Id.Set.empty
-      | Def cs -> global_vars_set env (Lazyconstr.force cs)
-      | OpaqueDef lc -> 
-          global_vars_set env (Lazyconstr.force_opaque lc) in
-      keep_hyps env (Id.Set.union ids_typ ids_def) in
-    let declared = match ctx with
-      | None -> inferred 
-      | Some declared -> declared in
-    let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
-    let inferred_set, declared_set = mk_set inferred, mk_set declared in
-    if not (Id.Set.subset inferred_set declared_set) then
-      error ("The following section variable are used but not declared:\n"^
-        (String.concat ", " (List.map Id.to_string
-          (Id.Set.elements (Id.Set.diff inferred_set declared_set)))));
-    declared in
+        | Undef _ -> Id.Set.empty
+        | Def cs -> global_vars_set env (Lazyconstr.force cs)
+        | OpaqueDef lc -> global_vars_set env (Lazyconstr.force_opaque lc)
+      in
+      keep_hyps env (Id.Set.union ids_typ ids_def)
+    in
+    match ctx with
+      | None -> inferred
+      | Some declared ->
+        check_declared_variables declared inferred;
+        declared
+  in
   let tps = Cemitcodes.from_val (compile_constant_body env def) in
   { const_hyps = hyps;
     const_body = def;