diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 2 | ||||
| -rw-r--r-- | library/global.ml | 9 | ||||
| -rw-r--r-- | library/lib.ml | 8 | ||||
| -rw-r--r-- | library/lib.mli | 2 | ||||
| -rw-r--r-- | library/library.ml | 11 | ||||
| -rw-r--r-- | library/states.ml | 4 | ||||
| -rw-r--r-- | library/states.mli | 2 | ||||
| -rw-r--r-- | library/summary.ml | 5 | ||||
| -rw-r--r-- | library/summary.mli | 13 |
9 files changed, 33 insertions, 23 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index c8f9d6161..0dfee9787 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -822,7 +822,7 @@ end (** {6 Module operations handling summary freeze/unfreeze *) let protect_summaries f = - let fs = Summary.freeze_summaries ~marshallable:false in + let fs = Summary.freeze_summaries ~marshallable:`No in try f fs with reraise -> (* Something wrong: undo the whole process *) diff --git a/library/global.ml b/library/global.ml index a0528a624..22b69e4f2 100644 --- a/library/global.ml +++ b/library/global.ml @@ -27,10 +27,15 @@ let global_env = ref empty_environment let join_safe_environment () = global_env := Safe_typing.join_safe_environment !global_env +let prune_safe_environment env = Safe_typing.prune_safe_environment env +(* XXX TODO pass args so that these functions can stop at the current + * file boundaries *) let () = Summary.declare_summary "Global environment" - { Summary.freeze_function = (fun b -> - if b then join_safe_environment (); !global_env); + { Summary.freeze_function = (function + | `Yes -> join_safe_environment (); !global_env + | `No -> !global_env + | `Shallow -> prune_safe_environment !global_env); unfreeze_function = (fun fr -> global_env := fr); init_function = (fun () -> global_env := empty_environment) } diff --git a/library/lib.ml b/library/lib.ml index b4371812b..379d0e8ad 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -250,7 +250,7 @@ let add_anonymous_leaf obj = let add_frozen_state () = add_anonymous_entry - (FrozenState (Summary.freeze_summaries ~marshallable:false)) + (FrozenState (Summary.freeze_summaries ~marshallable:`No)) (* Modules. *) @@ -485,7 +485,7 @@ let open_section id = let name = make_path id, make_kn id (* this makes little sense however *) in if Nametab.exists_section dir then errorlabstrm "open_section" (pr_id id ++ str " already exists."); - let fs = Summary.freeze_summaries ~marshallable:false in + let fs = Summary.freeze_summaries ~marshallable:`No in add_entry name (OpenedSection (prefix, fs)); (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); @@ -529,7 +529,9 @@ let close_section () = type frozen = Names.DirPath.t option * library_segment -let freeze ~marshallable:_ = (!comp_name, !lib_stk) +let freeze ~marshallable = + if marshallable = `Shallow then !comp_name, [] + else !comp_name, !lib_stk let unfreeze (mn,stk) = comp_name := mn; diff --git a/library/lib.mli b/library/lib.mli index 04f8d0775..1362fabf8 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -151,7 +151,7 @@ val close_section : unit -> unit type frozen -val freeze : marshallable:bool -> frozen +val freeze : marshallable:Summary.marshallable -> frozen val unfreeze : frozen -> unit val init : unit -> unit diff --git a/library/library.ml b/library/library.ml index 0766a62d7..472b1fb1d 100644 --- a/library/library.ml +++ b/library/library.ml @@ -44,20 +44,17 @@ module LibraryOrdered = DirPath module LibraryMap = Map.Make(LibraryOrdered) module LibraryFilenameMap = Map.Make(LibraryOrdered) -let join x = Safe_typing.join_compiled_library x.library_compiled (* This is a map from names to loaded libraries *) -let freeze b l = if b then (LibraryMap.iter (fun _ x -> join x) l; l) else l -let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY" ~freeze +let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY" (* This is the map of loaded libraries filename *) (* (not synchronized so as not to be caught in the states on disk) *) let libraries_filename_table = ref LibraryFilenameMap.empty (* These are the _ordered_ sets of loaded, imported and exported libraries *) -let freeze b l = if b then (List.iter join l; l) else l -let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" ~freeze -let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT" ~freeze -let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT" ~freeze +let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" +let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT" +let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT" (* various requests to the tables *) diff --git a/library/states.ml b/library/states.ml index 93b2c120e..a06e7ce80 100644 --- a/library/states.ml +++ b/library/states.ml @@ -23,7 +23,7 @@ let (extern_state,intern_state) = extern_intern Coq_config.state_magic_number in (fun s -> let s = ensure_suffix s in - raw_extern s (freeze ~marshallable:true)), + raw_extern s (freeze ~marshallable:`Yes)), (fun s -> let s = ensure_suffix s in let paths = Loadpath.get_paths () in @@ -33,7 +33,7 @@ let (extern_state,intern_state) = (* Rollback. *) let with_state_protection f x = - let st = freeze ~marshallable:false in + let st = freeze ~marshallable:`No in try let a = f x in unfreeze st; a with reraise -> diff --git a/library/states.mli b/library/states.mli index da6f33d65..0babae6af 100644 --- a/library/states.mli +++ b/library/states.mli @@ -17,7 +17,7 @@ val intern_state : string -> unit val extern_state : string -> unit type state -val freeze : marshallable:bool -> state +val freeze : marshallable:Summary.marshallable -> state val unfreeze : state -> unit (** {6 Rollback } *) diff --git a/library/summary.ml b/library/summary.ml index 53e9f7002..b46ce85b1 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -10,8 +10,9 @@ open Pp open Errors open Util +type marshallable = [ `Yes | `No | `Shallow ] type 'a summary_declaration = { - freeze_function : bool -> 'a; + freeze_function : marshallable -> 'a; unfreeze_function : 'a -> unit; init_function : unit -> unit } @@ -48,7 +49,7 @@ let freeze_summaries ~marshallable = Hashtbl.iter (fun id decl -> (* to debug missing Lazy.force - if marshallable then begin + if marshallable <> `No then begin prerr_endline ("begin marshalling " ^ id); ignore(Marshal.to_string (decl.freeze_function marshallable) []); prerr_endline ("end marshalling " ^ id); diff --git a/library/summary.mli b/library/summary.mli index 698034ad6..38d5fc7e8 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -9,10 +9,15 @@ (** This module registers the declaration of global tables, which will be kept in synchronization during the various backtracks of the system. *) +type marshallable = + [ `Yes (* Full data will be marshalled to disk *) + | `No (* Full data will be store in memory, e.g. for Undo *) + | `Shallow ] (* Only part of the data will be marshalled to a slave process *) + type 'a summary_declaration = { (** freeze_function [true] is for marshalling to disk. * e.g. lazy must be forced *) - freeze_function : bool -> 'a; + freeze_function : marshallable -> 'a; unfreeze_function : 'a -> unit; init_function : unit -> unit } @@ -35,7 +40,7 @@ val declare_summary : string -> 'a summary_declaration -> unit The [init_function] restores the reference to its initial value. The [freeze_function] can be overridden *) -val ref : ?freeze:(bool -> 'a -> 'a) -> name:string -> 'a -> 'a ref +val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref (** For global tables registered statically before the end of coqtop launch, the following empty [init_function] could be used. *) @@ -47,7 +52,7 @@ val nop : unit -> unit type frozen -val freeze_summaries : marshallable:bool -> frozen +val freeze_summaries : marshallable:marshallable -> frozen val unfreeze_summaries : frozen -> unit val init_summaries : unit -> unit @@ -55,5 +60,5 @@ val init_summaries : unit -> unit type frozen_bits val freeze_summary : - marshallable:bool -> ?complement:bool -> string list -> frozen_bits + marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits val unfreeze_summary : frozen_bits -> unit |