From 80aba8d52c650ef8e4ada694c20bf12c15849694 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 8 Aug 2013 18:52:47 +0000 Subject: enhance marshallable option for freeze (minor TODO in safe_typing) It can be: `Yes Full data, in a state that can be marshalled `No Full data, good for Undo only `Shallow Partial data, marshallable, good for slave processes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16682 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/conv_oracle.mli | 2 +- kernel/declareops.ml | 11 +++++++++++ kernel/declareops.mli | 1 + kernel/modops.ml | 52 +++++++++++++++++++++++++++++++++++++++++++++++++ kernel/modops.mli | 2 ++ kernel/safe_typing.ml | 17 +++++++++++++++- kernel/safe_typing.mli | 2 ++ library/declaremods.ml | 2 +- library/global.ml | 9 +++++++-- library/lib.ml | 8 +++++--- library/lib.mli | 2 +- library/library.ml | 11 ++++------- library/states.ml | 4 ++-- library/states.mli | 2 +- library/summary.ml | 5 +++-- library/summary.mli | 13 +++++++++---- proofs/proof_global.ml | 9 ++++++++- proofs/proof_global.mli | 2 +- toplevel/coqtop.ml | 2 +- toplevel/metasyntax.ml | 2 +- toplevel/stm.ml | 17 +++++++++++----- toplevel/vernac.ml | 2 +- 22 files changed, 142 insertions(+), 35 deletions(-) diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 822c3ea70..7bb62112c 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -36,5 +36,5 @@ val get_transp_state : unit -> transparent_state (**************************** Summary operations *) type oracle -val freeze : bool -> oracle +val freeze : [ `Yes | `No | `Shallow ] -> oracle val unfreeze : oracle -> unit diff --git a/kernel/declareops.ml b/kernel/declareops.ml index e597ea9a9..b0f320942 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -211,6 +211,17 @@ let join_constant_body cb = | OpaqueDef d -> ignore(Future.join d) | _ -> () +let prune_constant_body cb = + let cst, cbo = cb.const_constraints, cb.const_body in + let cst' = Future.drop cst in + let cbo' = match cbo with + | OpaqueDef d -> + let d' = Future.drop d in + if d' == d then cbo else OpaqueDef d' + | _ -> cbo in + if cst' == cst && cbo' == cbo then cb + else {cb with const_constraints = cst'; const_body = cbo'} + let string_of_side_effect = function | NewConstant (c,_) -> Names.string_of_con c type side_effects = side_effect list diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 635b8c47a..0da7c85c7 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -59,6 +59,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body val join_constant_body : constant_body -> unit +val prune_constant_body : constant_body -> constant_body (** {6 Hash-consing} *) diff --git a/kernel/modops.ml b/kernel/modops.ml index 39e5514c9..5f79c5363 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -617,3 +617,55 @@ and join_struct_expr_body = function match wdcl with | With_module_body _ -> () | With_definition_body (_, sb) -> join_constant_body sb + +let rec prune_module_body mb = + let me, mta, mt = mb.mod_expr, mb.mod_type_alg, mb.mod_type in + let me' = Option.smartmap prune_struct_expr_body me in + let mta' = Option.smartmap prune_struct_expr_body mta in + let mt' = prune_struct_expr_body mt in + if me' == me && mta' == mta && mt' == mt then mb + else {mb with mod_expr = me'; mod_type_alg = mta'; mod_type = mt'} +and prune_structure_body struc = + let prune_body (l,body as orig) = match body with + | SFBconst sb -> + let sb' = prune_constant_body sb in + if sb == sb' then orig else (l, SFBconst sb') + | SFBmind _ -> orig + | SFBmodule m -> + let m' = prune_module_body m in + if m == m' then orig else (l, SFBmodule m') + | SFBmodtype m -> + let te, te_alg = m.typ_expr, m.typ_expr_alg in + let te' = prune_struct_expr_body te in + let te_alg' = + Option.smartmap prune_struct_expr_body te_alg in + if te' == te && te_alg' == te_alg then orig + else (l, SFBmodtype {m with typ_expr = te'; typ_expr_alg = te_alg'}) in + CList.smartmap prune_body struc +and prune_struct_expr_body orig = match orig with + | SEBfunctor (id,t,e) -> + let te, ta = t.typ_expr, t.typ_expr_alg in + let te' = prune_struct_expr_body te in + let ta' = Option.smartmap prune_struct_expr_body ta in + let e' = prune_struct_expr_body e in + if te' == te && ta' == ta && e' == e then orig + else SEBfunctor(id, {t with typ_expr = te'; typ_expr_alg = ta'}, e') + | SEBident _ -> orig + | SEBstruct s -> + let s' = prune_structure_body s in + if s' == s then orig else SEBstruct s' + | SEBapply (mexpr,marg,u) -> + let mexpr' = prune_struct_expr_body mexpr in + let marg' = prune_struct_expr_body marg in + if mexpr' == mexpr && marg' == marg then orig + else SEBapply (mexpr', marg', u) + | SEBwith (seb,wdcl) -> + let seb' = prune_struct_expr_body seb in + let wdcl' = match wdcl with + | With_module_body _ -> wdcl + | With_definition_body (id, sb) -> + let sb' = prune_constant_body sb in + if sb' == sb then wdcl else With_definition_body (id, sb') in + if seb' == seb && wdcl' == wdcl then orig + else SEBwith (seb', wdcl') + diff --git a/kernel/modops.mli b/kernel/modops.mli index 30f9274d2..c0943233b 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -54,6 +54,8 @@ val join_module_body : module_body -> unit val join_structure_body : structure_body -> unit val join_struct_expr_body : struct_expr_body -> unit +val prune_structure_body : structure_body -> structure_body + (** Errors *) type signature_mismatch_error = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 13368aab9..eb5c01692 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -132,12 +132,27 @@ let add_constraints cst senv = let is_curmod_library senv = match senv.modinfo.variant with LIBRARY _ -> true | _ -> false -let rec join_safe_environment e = +let join_safe_environment e = join_structure_body e.revstruct; List.fold_left (fun e fc -> add_constraints (Now (Future.join fc)) e) {e with future_cst = []} e.future_cst +(* TODO : out of place and maybe incomplete w.r.t. modules *) +let prune_env env = + let env = Environ.pre_env env in + let prune_ckey (cb,k) = Declareops.prune_constant_body cb, k in + let prune_globals glob = + {glob with Pre_env.env_constants = + Cmap_env.map prune_ckey glob.Pre_env.env_constants } in + Environ.env_of_pre_env + {env with Pre_env.env_globals = prune_globals env.Pre_env.env_globals} +let prune_safe_environment e = + let e = {e with revstruct = prune_structure_body e.revstruct; + future_cst = []; + env = prune_env e.env} in + {e with old = e} + let check_modlabel l senv = if exists_modlabel l senv then error_existing_label l let check_objlabel l senv = diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 210d601fb..e9716930b 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -34,6 +34,8 @@ val is_curmod_library : safe_environment -> bool (* safe_environment has functional data affected by lazy computations, * thus this function returns a new safe_environment *) val join_safe_environment : safe_environment -> safe_environment +(* future computations are just dropped by this function *) +val prune_safe_environment : safe_environment -> safe_environment val empty_environment : safe_environment val is_empty : safe_environment -> bool 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 diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 0c0aac715..470d19b71 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -391,6 +391,13 @@ module V82 = struct end type state = pstate list -let freeze () = !pstates +let drop_hook_mode p = { p with hook = None; mode = None } + +let freeze ~marshallable = + match marshallable with + | `Yes -> + Errors.anomaly (Pp.str"full marshalling of proof state not supported") + | `Shallow -> List.map drop_hook_mode !pstates + | `No -> !pstates let unfreeze s = pstates := s; update_proof_mode () diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index a5fe33992..61bb5c0dd 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -140,5 +140,5 @@ module V82 : sig end type state -val freeze : unit -> state +val freeze : marshallable:[`Yes | `No | `Shallow] -> state val unfreeze : state -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 1dba38001..394cce6ce 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -128,7 +128,7 @@ let compile_files () = | [] -> () | [vf] -> compile_file vf (* One compilation : no need to save init state *) | l -> - let init_state = States.freeze ~marshallable:false in + let init_state = States.freeze ~marshallable:`No in let coqdoc_init_state = Lexer.location_table () in List.iter (fun vf -> diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 46037bcbc..e9fd0620d 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1075,7 +1075,7 @@ let inNotation : notation_obj -> obj = (**********************************************************************) let with_lib_stk_protection f x = - let fs = Lib.freeze false in + let fs = Lib.freeze `No in try let a = f x in Lib.unfreeze fs; a with reraise -> let reraise = Errors.push reraise in diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 218929f23..d9d63d796 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -382,7 +382,7 @@ end = struct (* {{{ *) (* hack to make futures functional *) let in_t, out_t = Dyn.create "state4future" let () = Future.set_freeze - (fun () -> in_t (freeze_global_state (), !cur_id)) + (fun () -> in_t (freeze_global_state `No, !cur_id)) (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i) let is_cached id = @@ -407,14 +407,21 @@ end = struct (* {{{ *) Pp.feedback ~state_id:id (Interface.ErrorMsg (loc, msg)); Stateid.add_state_id e ?valid id - let define ?(cache=false) f id = + let string_of_cache = function + | `Yes -> "Yes" | `No -> "No" | `Marshallable -> "Marshallable" + let marshallable_of_cache = function + | `Yes -> `No + | `No -> assert false + | `Marshallable -> `Shallow + + let define ?(cache=`No) f id = if is_cached id then anomaly (str"defining state "++str(string_of_state_id id)++str" twice"); try prerr_endline ("defining " ^ string_of_state_id id ^ " (cache=" ^ string_of_bool cache ^ ")"); f (); - if cache then freeze id; + if cache <> `No then freeze (marshallable_of_cache cache) id; cur_id := id; feedback ~state_id:id Interface.Processed; VCS.reached id true; @@ -466,8 +473,8 @@ let known_state ~cache id = (* ugly functions to process nested lemmas, i.e. hard to reproduce * side effects *) let cherry_pick_non_pstate () = - Summary.freeze_summary ~marshallable:false ~complement:true pstate, - Lib.freeze ~marshallable:false in + Summary.freeze_summary ~marshallable:`No ~complement:true pstate, + Lib.freeze ~marshallable:`No in let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l in let rec pure_cherry_pick_non_pstate id = Future.purify (fun id -> diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 88802fc34..888c3411d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -188,7 +188,7 @@ let set_formatter_translator() = let pr_new_syntax loc ocom = let loc = Loc.unloc loc in if !beautify_file then set_formatter_translator(); - let fs = States.freeze ~marshallable:false in + let fs = States.freeze ~marshallable:`No in let com = match ocom with | Some VernacNop -> mt() | Some com -> Ppvernac.pr_vernac com -- cgit v1.2.3