diff options
| -rw-r--r-- | checker/check.ml | 16 | ||||
| -rw-r--r-- | checker/safe_typing.ml | 157 | ||||
| -rw-r--r-- | checker/safe_typing.mli | 8 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 150 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 8 | ||||
| -rw-r--r-- | library/library.ml | 16 |
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 |