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

diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 5cbcc00f5..492f5bc20 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -59,117 +59,19 @@ let check_imports f caller env needed =
   in
   Array.iter check needed
 
+type nativecode_symb_array
 
 type compiled_library =
     DirPath.t *
     module_body *
     (DirPath.t * Digest.t) array *
-    engagement option
-
- (* 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 load : table -> 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 = constr_substituted array
-  let key_of_lazy_constr (c: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 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 (dp,mb,depends,s) -> (dp,traverse_module mb,depends,s) 
-
-  (* 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 table lightened_library =
-    let decode_key = function
-      | Undef _ | Def _ -> assert false
-      | OpaqueDef k ->
-          let k = key_of_lazy_constr k in
-	  let body =
-	    try table.(k)
-	    with _ -> error "Error while retrieving an opaque body"
-	  in
-	  OpaqueDef (lazy_constr_from_val body)
-    in
-    traverse_library decode_key lightened_library
-
-end
+    engagement option *
+    nativecode_symb_array
 
 open Validate
 let val_deps = val_array (val_tuple ~name:"dep"[|val_dp;no_val|])
-let val_vo = val_tuple ~name:"vo" [|val_dp;val_module;val_deps;val_opt val_eng|]
+let val_vo = val_tuple ~name:"vo"
+  [|val_dp;val_module;val_deps;val_opt val_eng; no_val|]
 
 (* This function should append a certificate to the .vo file.
    The digest must be part of the certicate to rule out attackers
@@ -180,8 +82,9 @@ let stamp_library file digest = ()
 
 (* When the module is checked, digests do not need to match, but a
    warning is issued in case of mismatch *)
-let import file (dp,mb,depends,engmt as vo) digest =
+let import file (dp,mb,depends,engmt,_ as vo) table digest =
   Validate.apply !Flags.debug val_vo vo;
+  Validate.apply !Flags.debug (val_array Term.val_constr) table;
   Flags.if_verbose ppnl (str "*** vo structure validated ***"); pp_flush ();
   let env = !genv in
   check_imports msg_warning dp env depends;
@@ -193,7 +96,7 @@ let import file (dp,mb,depends,engmt as vo) digest =
   full_add_module dp mb digest
 
 (* When the module is admitted, digests *must* match *)
-let unsafe_import file (dp,mb,depends,engmt as vo) digest =
+let unsafe_import file (dp,mb,depends,engmt,_ as vo) digest =
   if !Flags.debug then ignore vo; (*Validate.apply !Flags.debug val_vo vo;*)
   let env = !genv in
   check_imports (errorlabstrm"unsafe_import") dp env depends;