From 5676b113920fb48d4898817d6c0ce3353b06107f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 29 Nov 2017 01:42:21 +0100 Subject: [summary] Adapt STM to the new Summary API. We need to a partial restore. I think that we could design a better API, but further work on the toplevel state should improve it progressively. --- engine/evarutil.ml | 7 ++++--- engine/evarutil.mli | 2 +- engine/evd.ml | 5 ++--- engine/evd.mli | 2 +- library/global.ml | 9 ++++++--- library/global.mli | 2 +- library/summary.ml | 8 +++++--- library/summary.mli | 2 +- stm/stm.ml | 48 +++++++++++++++++++++++++++++++----------------- vernac/obligations.ml | 4 ++-- vernac/obligations.mli | 3 +++ 11 files changed, 57 insertions(+), 35 deletions(-) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 907f1b1ac..3445b744a 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -199,9 +199,10 @@ let whd_head_evar sigma c = let meta_counter_summary_name = "meta counter" (* Generator of metavariables *) -let new_meta = - let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in - fun () -> incr meta_ctr; !meta_ctr +let meta_ctr, meta_counter_summary_tag = + Summary.ref_tag 0 ~name:meta_counter_summary_name + +let new_meta () = incr meta_ctr; !meta_ctr let mk_new_meta () = EConstr.mkMeta(new_meta()) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 5fd4634d6..9d0b973a7 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -236,7 +236,7 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> val subterm_source : Evar.t -> Evar_kinds.t Loc.located -> Evar_kinds.t Loc.located -val meta_counter_summary_name : string +val meta_counter_summary_tag : int Summary.Dyn.tag (** Deprecated *) type type_constraint = types option diff --git a/engine/evd.ml b/engine/evd.ml index 45d2a8b08..e33c851f6 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -466,9 +466,8 @@ let add d e i = add_with_name d e i let evar_counter_summary_name = "evar counter" (* Generator of existential names *) -let new_untyped_evar = - let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in - fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr +let evar_ctr, evar_counter_summary_tag = Summary.ref_tag 0 ~name:evar_counter_summary_name +let new_untyped_evar () = incr evar_ctr; Evar.unsafe_of_int !evar_ctr let new_evar evd ?name evi = let evk = new_untyped_evar () in diff --git a/engine/evd.mli b/engine/evd.mli index fb5a6cd16..a915dd7ad 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -613,7 +613,7 @@ type unsolvability_explanation = SeveralInstancesFound of int (* This stuff is internal and should not be used. Currently a hack in the STM relies on it. *) -val evar_counter_summary_name : string +val evar_counter_summary_tag : int Summary.Dyn.tag (** {5 Deprecated functions} *) val create_evar_defs : evar_map -> evar_map diff --git a/library/global.ml b/library/global.ml index 03d7612a4..ce37dfecf 100644 --- a/library/global.ml +++ b/library/global.ml @@ -20,6 +20,7 @@ module GlobalSafeEnv : sig val set_safe_env : Safe_typing.safe_environment -> unit val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit val is_joined_environment : unit -> bool + val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag end = struct @@ -30,9 +31,9 @@ let join_safe_environment ?except () = let is_joined_environment () = Safe_typing.is_joined_environment !global_env - -let () = - Summary.declare_summary global_env_summary_name + +let global_env_summary_tag = + Summary.declare_summary_tag global_env_summary_name { Summary.freeze_function = (function | `Yes -> join_safe_environment (); !global_env | `No -> !global_env @@ -51,6 +52,8 @@ let set_safe_env e = global_env := e end +let global_env_summary_tag = GlobalSafeEnv.global_env_summary_tag + let safe_env = GlobalSafeEnv.safe_env let join_safe_environment ?except () = GlobalSafeEnv.join_safe_environment ?except () diff --git a/library/global.mli b/library/global.mli index 1d68d1082..79c8525c6 100644 --- a/library/global.mli +++ b/library/global.mli @@ -159,4 +159,4 @@ val current_dirpath : unit -> DirPath.t val with_global : (Environ.env -> DirPath.t -> 'a Univ.in_universe_context_set) -> 'a -val global_env_summary_name : string +val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag diff --git a/library/summary.ml b/library/summary.ml index 5fe3160e1..6df17476b 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -87,7 +87,7 @@ let unfreeze_single name state = Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]); iraise e -let unfreeze_summaries { summaries; ml_module } = +let unfreeze_summaries ?(partial=false) { summaries; ml_module } = (* The unfreezing of [ml_modules_summary] has to be anticipated since it * may modify the content of [summaries] by loading new ML modules *) begin match !sum_mod with @@ -98,8 +98,10 @@ let unfreeze_summaries { summaries; ml_module } = let ufz name decl = try decl.unfreeze_function String.Map.(find name summaries) with Not_found -> - Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name); - decl.init_function () + if not partial then begin + Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name); + decl.init_function () + end; in (* String.Map.iter unfreeze_single !sum_map *) String.Map.iter ufz !sum_map diff --git a/library/summary.mli b/library/summary.mli index 9fc6df6ad..09447199e 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -80,7 +80,7 @@ type frozen val empty_frozen : frozen val freeze_summaries : marshallable:marshallable -> frozen -val unfreeze_summaries : frozen -> unit +val unfreeze_summaries : ?partial:bool -> frozen -> unit val init_summaries : unit -> unit (** Typed projection of the summary. Experimental API, use with CARE *) diff --git a/stm/stm.ml b/stm/stm.ml index 8aa832da8..0dbe168b7 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -158,9 +158,10 @@ let mkTransCmd cast cids ceff cqueue = Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff } (* Parts of the system state that are morally part of the proof state *) -let summary_pstate = [ Evarutil.meta_counter_summary_name; - Evd.evar_counter_summary_name; - "program-tcc-table" ] +let summary_pstate = Evarutil.meta_counter_summary_tag, + Evd.evar_counter_summary_tag, + Obligations.program_tcc_summary_tag + type cached_state = | Empty | Error of Exninfo.iexn @@ -762,15 +763,21 @@ end = struct (* {{{ *) let fix_exn_ref = ref (fun x -> x) type proof_part = - Proof_global.t * Summary.frozen_bits (* only meta counters *) + Proof_global.t * + int * (* Evarutil.meta_counter_summary_tag *) + int * (* Evd.evar_counter_summary_tag *) + Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) type partial_state = [ `Full of Vernacstate.t | `ProofOnly of Stateid.t * proof_part ] let proof_part_of_frozen { Vernacstate.proof; system } = + let st = States.summary_of_state system in proof, - Summary.project_summary (States.summary_of_state system) summary_pstate + Summary.project_from_summary st Util.(pi1 summary_pstate), + Summary.project_from_summary st Util.(pi2 summary_pstate), + Summary.project_from_summary st Util.(pi3 summary_pstate) let freeze marshallable id = VCS.set_state id (Valid (Vernacstate.freeze_interp_state marshallable)) @@ -830,16 +837,21 @@ end = struct (* {{{ *) else s with VCS.Expired -> s in VCS.set_state id (Valid s) - | `ProofOnly(ontop,(pstate,counters)) -> + | `ProofOnly(ontop,(pstate,c1,c2,c3)) -> if is_cached_and_valid ontop then let s = get_cached ontop in let s = { s with proof = Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in let s = { s with system = States.replace_summary s.system - (Summary.surgery_summary - (States.summary_of_state s.system) - counters) } in + begin + let st = States.summary_of_state s.system in + let st = Summary.modify_summary st Util.(pi1 summary_pstate) c1 in + let st = Summary.modify_summary st Util.(pi2 summary_pstate) c2 in + let st = Summary.modify_summary st Util.(pi3 summary_pstate) c3 in + st + end + } in VCS.set_state id (Valid s) with VCS.Expired -> () @@ -854,10 +866,10 @@ end = struct (* {{{ *) let same_env { Vernacstate.system = s1 } { Vernacstate.system = s2 } = let s1 = States.summary_of_state s1 in - let e1 = Summary.project_summary s1 [Global.global_env_summary_name] in + let e1 = Summary.project_from_summary s1 Global.global_env_summary_tag in let s2 = States.summary_of_state s2 in - let e2 = Summary.project_summary s2 [Global.global_env_summary_name] in - Summary.pointer_equal e1 e2 + let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in + e1 == e2 let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true) f id @@ -2040,8 +2052,6 @@ and Reach : sig end = struct (* {{{ *) -let pstate = summary_pstate - let async_policy () = let open Flags in if is_universe_polymorphism () then false @@ -2254,10 +2264,14 @@ let known_state ?(redefine_qed=false) ~cache id = (* ugly functions to process nested lemmas, i.e. hard to reproduce * side effects *) let cherry_pick_non_pstate () = - Summary.freeze_summary ~marshallable:`No ~complement:true pstate, - Lib.freeze ~marshallable:`No in + let st = Summary.freeze_summaries ~marshallable:`No in + let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in + let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in + let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in + st, Lib.freeze ~marshallable:`No in + let inject_non_pstate (s,l) = - Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env () + Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env () in let rec pure_cherry_pick_non_pstate safe_id id = stm_purify (fun id -> diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 24d664951..bdae27e5b 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -429,8 +429,8 @@ let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] -let from_prg : program_info ProgMap.t ref = - Summary.ref ProgMap.empty ~name:"program-tcc-table" +let from_prg, program_tcc_summary_tag = + Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" let close sec = if not (ProgMap.is_empty !from_prg) then diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 0602e52e9..bdc97d48c 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -104,3 +104,6 @@ exception NoObligations of Names.Id.t option val explain_no_obligations : Names.Id.t option -> Pp.t val set_program_mode : bool -> unit + +type program_info +val program_tcc_summary_tag : program_info Id.Map.t Summary.Dyn.tag -- cgit v1.2.3