1 files changed, 107 insertions, 46 deletions

diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index a669c5e8..bc067dc5 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -1,19 +1,16 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: safe_typing.ml 10275 2007-10-30 11:01:24Z barras $ *)
-
 open Pp
 open Util
 open Names
 open Declarations
 open Environ
-open Mod_checking
 
 (************************************************************************)
 (*
@@ -21,7 +18,6 @@ open Mod_checking
  *)
 
 let genv = ref empty_env
-let reset () = genv := empty_env
 let get_env () = !genv
 
 let set_engagement c =
@@ -63,51 +59,116 @@ let check_imports f caller env needed =
   List.iter check needed
 
 
-
-(* Remove the body of opaque constants in modules *)
-(* also remove mod_expr ? Good idea!*)
-let rec lighten_module mb =
-  { mb with
-    mod_expr = Option.map lighten_modexpr mb.mod_expr;
-    mod_type = lighten_modexpr mb.mod_type }
-
-and lighten_struct struc =
-  let lighten_body (l,body) = (l,match body with
-    | SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None}
-    | (SFBconst _ | SFBmind _ ) as x -> x
-    | SFBmodule m -> SFBmodule (lighten_module m)
-    | SFBmodtype m -> SFBmodtype
-	({m with
-	    typ_expr = lighten_modexpr m.typ_expr}))
-  in
-    List.map lighten_body struc
-
-and lighten_modexpr = function
-  | SEBfunctor (mbid,mty,mexpr) ->
-      SEBfunctor (mbid,
-		    ({mty with
-			typ_expr = lighten_modexpr mty.typ_expr}),
-		  lighten_modexpr mexpr)
-  | SEBident mp as x -> x
-  | SEBstruct ( struc) ->
-      SEBstruct ( lighten_struct struc)
-  | SEBapply (mexpr,marg,u) ->
-      SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)
-  | SEBwith (seb,wdcl) ->
-      SEBwith (lighten_modexpr seb,wdcl)
-
-let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s)
-
-
 type compiled_library =
     dir_path *
     module_body *
     (dir_path * Digest.t) list *
     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
+
 open Validate
-let val_deps = val_list (val_tuple"dep"[|val_dp;no_val|])
-let val_vo = val_tuple "vo" [|val_dp;val_module;val_deps;val_opt val_eng|]
+let val_deps = val_list (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|]
 
 (* This function should append a certificate to the .vo file.
    The digest must be part of the certicate to rule out attackers
@@ -124,15 +185,15 @@ let import file (dp,mb,depends,engmt as vo) digest =
   let env = !genv in
   check_imports msg_warning dp env depends;
   check_engagement env engmt;
-  check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb;
+  Mod_checking.check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb;
   stamp_library file digest;
   (* We drop proofs once checked *)
 (*  let mb = lighten_module mb in*)
   full_add_module dp mb digest
 
 (* When the module is admitted, digests *must* match *)
-let unsafe_import file (dp,mb,depends,engmt) digest =
-(*  if !Flags.debug then Validate.apply !Flags.debug val_vo vo;*)
+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;
   check_engagement env engmt;