* (checker|kernel)/Safe_typing: New LightenLibrary.

  This module introduces an indirection behind opaque const_body
  to enable the optional demarshalling of them.

* library/Library checker/Check: Use LightenLibrary.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13377 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 272 insertions, 83 deletions

diff --git a/checker/check.ml b/checker/check.ml
index befcf0646..4c05d0d68 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -40,7 +40,7 @@ type compilation_unit_name = dir_path
 
 type library_disk = {
   md_name : compilation_unit_name;
-  md_compiled : Safe_typing.compiled_library;
+  md_compiled : Safe_typing.LightenLibrary.lighten_compiled_library;
   md_objects : library_objects;
   md_deps : (compilation_unit_name * Digest.t) list;
   md_imports : compilation_unit_name list }
@@ -281,10 +281,10 @@ let with_magic_number_check f a =
 (************************************************************************)
 (* Internalise libraries *)
 
-let mk_library md f digest = {
+let mk_library md f get_table digest = {
   library_name = md.md_name;
   library_filename = f;
-  library_compiled = md.md_compiled;
+  library_compiled = Safe_typing.LightenLibrary.load false get_table md.md_compiled;
   library_deps = md.md_deps;
   library_digest = digest }
 
@@ -298,20 +298,22 @@ let depgraph = ref LibraryMap.empty
 
 let intern_from_file (dir, f) =
   Flags.if_verbose msg (str"[intern "++str f++str" ...");
-  let (md,digest) =
+  let (md,get_table,close,digest) =
     try
       let ch = with_magic_number_check raw_intern_library f in
       let (md:library_disk) = System.marshal_in ch in
       let digest = System.marshal_in ch in
-      close_in ch;
+      let get_table () = (System.marshal_in ch : Safe_typing.LightenLibrary.table) in
       if dir <> md.md_name then
         errorlabstrm "load_physical_library"
           (name_clash_message dir md.md_name f);
       Flags.if_verbose msgnl(str" done]");
-      md,digest
+      md,get_table,(fun () -> close_in ch),digest
     with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in
   depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
-  mk_library md f digest
+  let library = mk_library md f get_table digest in
+  close ();
+  library
 
 let get_deps (dir, f) =
   try LibraryMap.find dir !depgraph
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 6cd47d85d..38f5aacf3 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -61,48 +61,133 @@ 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 lighten_compiled_library 
+  val save : compiled_library -> lighten_compiled_library * table
+  val load : load_proof:bool -> (unit -> table) -> lighten_compiled_library -> compiled_library
+end = struct
+
+  (* The table is implemented as an array of [constr_substituted].
+     Thus, its keys are integers which can be easily embedded inside
+     [constr_substituted]. This way the [compiled_library] type does
+     not have to be changed. *)
+  type table = constr_substituted array
+
+  (* 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 lighten_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 lighten_module mb =
+      { mb with
+	mod_expr = None;
+	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 = on_opaque_const_body x.const_body }
+	| (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)
+    in
+    fun (dp,mb,depends,s) -> (dp,lighten_module mb,depends,s) 
+
+  (* 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    : constr_substituted -> constr_substituted), 
+	 (get_table : unit -> table)) = 
+      (* We use an integer as a key inside the table. *)
+      let counter = ref 0 in
+      (* ... but it is wrap inside a [constr_substituted]. *)
+      let key_as_constr key = Declarations.from_val (Term.Rel key) 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 opaque_definition -> 
+	incr counter; 
+	opaque_definitions := opaque_definition :: !opaque_definitions;
+	key_as_constr !counter), 
+
+       (* Get the final table representation. *)
+       (fun () -> Array.of_list (List.rev !opaque_definitions)))
+    in
+    let encode_const_body : constr_substituted option -> constr_substituted option = function
+      | None -> None
+      | Some ct -> Some (insert ct)
+    in
+    let lightened_library = traverse_library encode_const_body library in
+    (lightened_library, get_table ())
+
+  (* Loading is also a traversing that decode 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 (get_table : unit -> table) lightened_library = 
+    let decode_key : constr_substituted option -> constr_substituted option = 
+      if load_proof then 
+	let table = get_table () in
+	function Some cterm -> 
+	  Some (table.(
+	    try 
+	      match Declarations.force_constr cterm with
+		| Term.Rel key -> key
+		| _ -> assert false
+	    with _ -> assert false
+	  ))
+	  | _ -> None
+      else 
+	fun _ -> None
+    in
+    traverse_library decode_key lightened_library
+
+end
+
 open Validate
 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|]
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index 843352c20..f8c5a48f3 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -23,3 +23,11 @@ val import         :
   System.physical_path -> compiled_library -> Digest.t -> unit
 val unsafe_import  :
   System.physical_path -> compiled_library -> Digest.t -> unit
+
+module LightenLibrary :
+sig
+  type table 
+  type lighten_compiled_library 
+  val save : compiled_library -> lighten_compiled_library * table
+  val load : load_proof:bool -> (unit -> table) -> lighten_compiled_library -> compiled_library
+end
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 92f3805c4..38eb7b3f2 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -833,40 +833,124 @@ let import (dp,mb,depends,engmt) digest senv =
 	  loads = (mp,mb)::senv.loads }
 
 
-(* Remove the body of opaque constants in modules *)
- let rec lighten_module mb =
-  { mb with
-    mod_expr = None;
-    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,
+ (* 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 lighten_compiled_library 
+  val save : compiled_library -> lighten_compiled_library * table
+  val load : load_proof:bool -> (unit -> table) -> lighten_compiled_library -> compiled_library
+end = struct
+
+  (* The table is implemented as an array of [constr_substituted].
+     Thus, its keys are integers which can be easily embedded inside
+     [constr_substituted]. This way the [compiled_library] type does
+     not have to be changed. *)
+  type table = constr_substituted array
+
+  (* 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 lighten_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 lighten_module mb =
+      { mb with
+	mod_expr = None;
+	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 = on_opaque_const_body x.const_body }
+	| (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)
-
+		      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)
+    in
+    fun (dp,mb,depends,s) -> (dp,lighten_module mb,depends,s) 
+
+  (* 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    : constr_substituted -> constr_substituted), 
+	 (get_table : unit -> table)) = 
+      (* We use an integer as a key inside the table. *)
+      let counter = ref 0 in
+      (* ... but it is wrap inside a [constr_substituted]. *)
+      let key_as_constr key = Declarations.from_val (Term.mkRel key) 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 opaque_definition -> 
+	incr counter; 
+	opaque_definitions := opaque_definition :: !opaque_definitions;
+	key_as_constr !counter), 
+
+       (* Get the final table representation. *)
+       (fun () -> Array.of_list (List.rev !opaque_definitions)))
+    in
+    let encode_const_body : constr_substituted option -> constr_substituted option = function
+      | None -> None
+      | Some ct -> Some (insert ct)
+    in
+    let lightened_library = traverse_library encode_const_body library in
+    (lightened_library, get_table ())
+
+  (* Loading is also a traversing that decode 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 (get_table : unit -> table) lightened_library = 
+    let decode_key : constr_substituted option -> constr_substituted option = 
+      if load_proof then 
+	let table = get_table () in
+	function Some cterm -> 
+	  Some (table.(
+	    try 
+	      Term.destRel (Declarations.force cterm)
+	    with _ -> assert false
+	  ))
+	  | _ -> None
+      else 
+	fun _ -> None
+    in
+    traverse_library decode_key lightened_library
+
+end
 
 type judgment = unsafe_judgment
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 351dda701..25e0a05ba 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -112,7 +112,13 @@ val import : compiled_library -> Digest.t -> safe_environment
 
 (** Remove the body of opaque constants *)
 
-val lighten_library : compiled_library -> compiled_library
+module LightenLibrary :
+sig
+  type table 
+  type lighten_compiled_library 
+  val save : compiled_library -> lighten_compiled_library * table
+  val load : load_proof:bool -> (unit -> table) -> lighten_compiled_library -> compiled_library
+end
 
 (** {6 Typing judgments } *)
 
diff --git a/library/library.ml b/library/library.ml
index 42cad4454..6bb609fce 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -117,7 +117,7 @@ type compilation_unit_name = dir_path
 
 type library_disk = {
   md_name : compilation_unit_name;
-  md_compiled : compiled_library;
+  md_compiled : LightenLibrary.lighten_compiled_library;
   md_objects : Declaremods.library_objects;
   md_deps : (compilation_unit_name * Digest.t) list;
   md_imports : compilation_unit_name list }
@@ -387,9 +387,9 @@ let try_locate_qualified_library (loc,qid) =
 (************************************************************************)
 (* Internalise libraries *)
 
-let mk_library md digest = {
+let mk_library md get_table digest = {
   library_name = md.md_name;
-  library_compiled = md.md_compiled;
+  library_compiled = LightenLibrary.load false get_table md.md_compiled;
   library_objects = md.md_objects;
   library_deps = md.md_deps;
   library_imports = md.md_imports;
@@ -397,11 +397,13 @@ let mk_library md digest = {
 
 let intern_from_file f =
   let ch = System.with_magic_number_check raw_intern_library f in
-  let md = System.marshal_in ch in
+  let lmd = System.marshal_in ch in
   let digest = System.marshal_in ch in
+  let get_table () = (System.marshal_in ch : LightenLibrary.table) in
+  register_library_filename lmd.md_name f;
+  let library = mk_library lmd get_table digest in
   close_in ch;
-  register_library_filename md.md_name f;
-  mk_library md digest
+  library
 
 let rec intern_library needed (dir, f) =
   (* Look if in the current logical environment *)
@@ -615,6 +617,7 @@ let error_recursively_dependent_library dir =
    writing the content and computing the checksum... *)
 let save_library_to dir f =
   let cenv, seg = Declaremods.end_library dir in
+  let cenv, table = LightenLibrary.save cenv in
   let md = {
     md_name = dir;
     md_compiled = cenv;
@@ -629,6 +632,7 @@ let save_library_to dir f =
     flush ch;
     let di = Digest.file f' in
     System.marshal_out ch di;
+    System.marshal_out ch table;
     close_out ch
   with e -> warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e