diff options
37 files changed, 171 insertions, 536 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 955ad9a88..4b4b36865 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -23,13 +23,7 @@ open Nameops open Misctypes (*i*) -let generalizable_table = ref Id.Pred.empty - -let _ = - Summary.declare_summary "generalizable-ident" - { Summary.freeze_function = (fun () -> !generalizable_table); - Summary.unfreeze_function = (fun r -> generalizable_table := r); - Summary.init_function = (fun () -> generalizable_table := Id.Pred.empty) } +let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident" let declare_generalizable_ident table (loc,id) = if not (Id.equal id (root_of_id id)) then diff --git a/interp/notation.ml b/interp/notation.ml index 37ad387da..81ef06f6f 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -16,7 +16,6 @@ open Term open Nametab open Libnames open Globnames -open Summary open Constrexpr open Notation_term open Glob_term @@ -920,10 +919,10 @@ let init () = scope_class_map := Gmap.add ScopeSort "type_scope" Gmap.empty let _ = - declare_summary "symbols" - { freeze_function = freeze; - unfreeze_function = unfreeze; - init_function = init } + Summary.declare_summary "symbols" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init } let with_notation_protection f x = let fs = freeze () in diff --git a/interp/reserve.ml b/interp/reserve.ml index 30953007e..0efcafcd2 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -22,8 +22,8 @@ type key = | RefKey of global_reference | Oth -let reserve_table = ref Id.Map.empty -let reserve_revtable = ref Gmapl.empty +let reserve_table = Summary.ref Id.Map.empty ~name:"reserved-type" +let reserve_revtable = Summary.ref Gmapl.empty ~name:"reserved-type-rev" let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) @@ -41,17 +41,6 @@ let in_reserved : Id.t * notation_constr -> obj = declare_object {(default_object "RESERVED-TYPE") with cache_function = cache_reserved_type } -let freeze_reserved () = (!reserve_table,!reserve_revtable) -let unfreeze_reserved (r,rr) = reserve_table := r; reserve_revtable := rr -let init_reserved () = - reserve_table := Id.Map.empty; reserve_revtable := Gmapl.empty - -let _ = - Summary.declare_summary "reserved-type" - { Summary.freeze_function = freeze_reserved; - Summary.unfreeze_function = unfreeze_reserved; - Summary.init_function = init_reserved } - let declare_reserved_type_binding (loc,id) t = if not (Id.equal id (root_of_id id)) then user_err_loc(loc,"declare_reserved_type", diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 96ba0bcc5..a023462b7 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -21,13 +21,9 @@ open Nametab type version = Flags.compat_version option -let syntax_table = ref (KNmap.empty : (interpretation*version) KNmap.t) - -let _ = Summary.declare_summary - "SYNTAXCONSTANT" - { Summary.freeze_function = (fun () -> !syntax_table); - Summary.unfreeze_function = (fun ft -> syntax_table := ft); - Summary.init_function = (fun () -> syntax_table := KNmap.empty) } +let syntax_table = + Summary.ref (KNmap.empty : (interpretation*version) KNmap.t) + ~name:"SYNTAXCONSTANT" let add_syntax_constant kn c onlyparse = syntax_table := KNmap.add kn (c,onlyparse) !syntax_table diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 6f013e46f..758bf821f 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -28,6 +28,10 @@ type oracle = level Id.Map.t * level Cmap.t let var_opacity = ref Id.Map.empty let cst_opacity = ref Cmap.empty +(* summary operations *) +let freeze () = (!var_opacity, !cst_opacity) +let unfreeze (vo,co) = (cst_opacity := co; var_opacity := vo) + let get_strategy = function | VarKey id -> (try Id.Map.find id !var_opacity @@ -65,8 +69,3 @@ let oracle_order l2r k1 k2 = | Level n1, Opaque -> true | Level n1, Level n2 -> n1 < n2 | _ -> l2r (* use recommended default *) - -(* summary operations *) -let init() = (cst_opacity := Cmap.empty; var_opacity := Id.Map.empty) -let freeze () = (!var_opacity, !cst_opacity) -let unfreeze (vo,co) = (cst_opacity := co; var_opacity := vo) diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 2a6db4b4b..4d8779664 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -36,6 +36,5 @@ val get_transp_state : unit -> transparent_state (**************************** Summary operations *) type oracle -val init : unit -> unit val freeze : unit -> oracle val unfreeze : oracle -> unit diff --git a/library/declaremods.ml b/library/declaremods.ml index bdb7bd368..cf333a886 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -83,10 +83,14 @@ type substitutive_objects = * Modules which where created with Module M:=mexpr or with Module M:SIG. ... End M. have the keep list empty. *) + let modtab_substobjs = - ref (MPmap.empty : substitutive_objects MPmap.t) + Summary.ref (MPmap.empty : substitutive_objects MPmap.t) + ~name:"MODULE-INFO-1" + let modtab_objects = - ref (MPmap.empty : (object_prefix * lib_objects) MPmap.t) + Summary.ref (MPmap.empty : (object_prefix * lib_objects) MPmap.t) + ~name:"MODULE-INFO-2" type current_module_info = { cur_mp : module_path; (** current started interactive module (if any) *) @@ -101,34 +105,12 @@ let default_module_info = cur_typ = None; cur_typs = [] } -let openmod_info = ref default_module_info +let openmod_info = Summary.ref default_module_info ~name:"MODULE-INFO-3" (* The library_cache here is needed to avoid recalculations of substituted modules object during "reloading" of libraries *) -let library_cache = ref Dirmap.empty - -let freeze_mod_tables () = - !modtab_substobjs, - !modtab_objects, - !openmod_info, - !library_cache - -let unfreeze_mod_tables (sobjs,objs,info,libcache) = - modtab_substobjs := sobjs; - modtab_objects := objs; - openmod_info := info; - library_cache := libcache - -let init_mod_tables () = - modtab_substobjs := MPmap.empty; - modtab_objects := MPmap.empty; - openmod_info := default_module_info; - library_cache := Dirmap.empty - -let _ = Summary.declare_summary "MODULE-INFO" - { Summary.freeze_function = freeze_mod_tables; - Summary.unfreeze_function = unfreeze_mod_tables; - Summary.init_function = init_mod_tables } +let library_cache = Summary.ref Dirmap.empty ~name:"MODULE-INFO-4" + (* auxiliary functions to transform full_path and kernel_name given by Lib into module_path and DirPath.t needed for modules *) @@ -303,24 +285,14 @@ let in_modkeep : lib_objects -> obj = The module M gets its objects from SIG *) let modtypetab = - ref (MPmap.empty : substitutive_objects MPmap.t) + Summary.ref (MPmap.empty : substitutive_objects MPmap.t) + ~name:"MODTYPE-INFO-1" (* currently started interactive module type. We remember its arguments if it is a functor type *) let openmodtype_info = - ref ([],[] : MBId.t list * module_type_body list) - -let freeze_modtyp_tables () = - !modtypetab, !openmodtype_info -let unfreeze_modtyp_tables (mtt,omti) = - modtypetab := mtt; openmodtype_info := omti -let init_modtyp_tables () = - modtypetab := MPmap.empty; openmodtype_info := [],[] - -let _ = Summary.declare_summary "MODTYPE-INFO" - { Summary.freeze_function = freeze_modtyp_tables; - Summary.unfreeze_function = unfreeze_modtyp_tables; - Summary.init_function = init_modtyp_tables } + Summary.ref ([],[] : MBId.t list * module_type_body list) + ~name:"MODTYPE-INFO-2" let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) = let mp = mp_of_kn kn in diff --git a/library/decls.ml b/library/decls.ml index 0ceea8b43..a93913a77 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -20,12 +20,8 @@ open Libnames type variable_data = DirPath.t * bool (* opacity *) * Univ.constraints * logical_kind -let vartab = ref (Id.Map.empty : variable_data Id.Map.t) - -let _ = Summary.declare_summary "VARIABLE" - { Summary.freeze_function = (fun () -> !vartab); - Summary.unfreeze_function = (fun ft -> vartab := ft); - Summary.init_function = (fun () -> vartab := Id.Map.empty) } +let vartab = + Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE" let add_variable_data id o = vartab := Id.Map.add id o !vartab @@ -42,12 +38,7 @@ let variable_exists id = Id.Map.mem id !vartab (** Datas associated to global parameters and constants *) -let csttab = ref (Cmap.empty : logical_kind Cmap.t) - -let _ = Summary.declare_summary "CONSTANT" - { Summary.freeze_function = (fun () -> !csttab); - Summary.unfreeze_function = (fun ft -> csttab := ft); - Summary.init_function = (fun () -> csttab := Cmap.empty) } +let csttab = Summary.ref (Cmap.empty : logical_kind Cmap.t) ~name:"CONSTANT" let add_constant_kind kn k = csttab := Cmap.add kn k !csttab diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index c26f652df..64267db01 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -10,28 +10,10 @@ open Libnames type discharged_hyps = full_path list -let discharged_hyps_map = ref Spmap.empty +let discharged_hyps_map = Summary.ref Spmap.empty ~name:"discharged_hypothesis" let set_discharged_hyps sp hyps = discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map let get_discharged_hyps sp = - try - Spmap.find sp !discharged_hyps_map - with Not_found -> - [] - -(*s Registration as global tables and rollback. *) - -let init () = - discharged_hyps_map := Spmap.empty - -let freeze () = !discharged_hyps_map - -let unfreeze dhm = discharged_hyps_map := dhm - -let _ = - Summary.declare_summary "discharged_hypothesis" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } + try Spmap.find sp !discharged_hyps_map with Not_found -> [] diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli index bc90220db..f2173bf49 100644 --- a/library/dischargedhypsmap.mli +++ b/library/dischargedhypsmap.mli @@ -13,8 +13,8 @@ open Nametab type discharged_hyps = full_path list -(** Discharged hypothesis. Here we store the discharged hypothesis of each - constant or inductive type declaration. *) +(** Discharged hypothesis. Here we store the discharged hypothesis of each + constant or inductive type declaration. *) val set_discharged_hyps : full_path -> discharged_hyps -> unit val get_discharged_hyps : full_path -> discharged_hyps diff --git a/library/global.ml b/library/global.ml index 929f7418f..f120ef195 100644 --- a/library/global.ml +++ b/library/global.ml @@ -10,12 +10,11 @@ open Names open Term open Environ open Safe_typing -open Summary (* We introduce here the global environment of the system, and we declare it as a synchronized table. *) -let global_env = ref empty_environment +let global_env = Summary.ref empty_environment ~name:"Global environment" let safe_env () = !global_env @@ -23,12 +22,6 @@ let env () = env_of_safe_env !global_env let env_is_empty () = is_empty !global_env -let _ = - declare_summary "Global environment" - { freeze_function = (fun () -> !global_env); - unfreeze_function = (fun fr -> global_env := fr); - init_function = (fun () -> global_env := empty_environment) } - (* Then we export the functions of [Typing] on that environment. *) let universes () = universes (env()) diff --git a/library/goptions.ml b/library/goptions.ml index 381b67726..bdc6ab89d 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -65,17 +65,10 @@ module MakeTable = module MySet = Set.Make (struct type t = A.t let compare = compare end) - let t = ref (MySet.empty : MySet.t) - - let _ = - if A.synchronous then - let freeze () = !t in - let unfreeze c = t := c in - let init () = t := MySet.empty in - Summary.declare_summary nick - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } + let t = + if A.synchronous + then Summary.ref MySet.empty ~name:nick + else ref MySet.empty let (add_option,remove_option) = if A.synchronous then @@ -216,7 +209,6 @@ with Not_found -> or List.mem_assoc (nickname key) !ref_table then error "Sorry, this option name is already used." -open Summary open Libobject open Lib @@ -247,10 +239,10 @@ let declare_option cast uncast discharge_function = (fun (_,v) -> Some v); load_function = (fun _ (_,v) -> write v)} in - let _ = declare_summary (nickname key) - { freeze_function = read; - unfreeze_function = write; - init_function = (fun () -> write default) } + let _ = Summary.declare_summary (nickname key) + { Summary.freeze_function = read; + Summary.unfreeze_function = write; + Summary.init_function = (fun () -> write default) } in begin fun v -> add_anonymous_leaf (decl_obj v) end , begin fun v -> add_anonymous_leaf (ldecl_obj v) end , diff --git a/library/heads.ml b/library/heads.ml index e6c9bc9a8..022e61156 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -52,19 +52,7 @@ module Evalrefmap = Map.Make (Evalreford) -let head_map = ref Evalrefmap.empty - -let init () = head_map := Evalrefmap.empty - -let freeze () = !head_map - -let unfreeze hm = head_map := hm - -let _ = - Summary.declare_summary "Head_decl" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } +let head_map = Summary.ref Evalrefmap.empty ~name:"Head_decl" let variable_head id = Evalrefmap.find (EvalVarRef id) !head_map let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map diff --git a/library/impargs.ml b/library/impargs.ml index 56dca8e3f..0026bc489 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -463,7 +463,7 @@ type implicit_discharge_request = | ImplInteractive of global_reference * implicits_flags * implicit_interactive_request -let implicits_table = ref Refmap.empty +let implicits_table = Summary.ref Refmap.empty ~name:"implicits" let implicits_of_global ref = try @@ -713,15 +713,3 @@ let rec select_impargs_size n = function let select_stronger_impargs = function | [] -> [] (* Tolerance for (DefaultImpArgs,[]) *) | (_,impls)::_ -> impls - -(*s Registration as global tables *) - -let init () = implicits_table := Refmap.empty -let freeze () = !implicits_table -let unfreeze t = implicits_table := t - -let _ = - Summary.declare_summary "implicits" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } diff --git a/library/lib.ml b/library/lib.ml index 30beb653f..c7454edaf 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -13,7 +13,6 @@ open Libnames open Globnames open Nameops open Libobject -open Summary type is_type = bool (* Module Type or just Module *) type export = bool option (* None for a Module Type *) @@ -217,10 +216,7 @@ let anonymous_id = fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n)) let add_anonymous_entry node = - let id = anonymous_id () in - let name = make_oname id in - add_entry name node; - name + add_entry (make_oname (anonymous_id ())) node let add_leaf id obj = let (path, _) = current_prefix () in @@ -253,7 +249,7 @@ let add_anonymous_leaf obj = add_entry oname (Leaf obj) let add_frozen_state () = - let _ = add_anonymous_entry (FrozenState (freeze_summaries())) in () + add_anonymous_entry (FrozenState (Summary.freeze_summaries())) (* Modules. *) @@ -331,7 +327,7 @@ let start_compilation s mp = if not (Names.DirPath.equal (snd (snd (!path_prefix))) Names.DirPath.empty) then error "some sections are already opened"; let prefix = s, (mp, Names.DirPath.empty) in - let _ = add_anonymous_entry (CompilingLibrary prefix) in + let () = add_anonymous_entry (CompilingLibrary prefix) in comp_name := Some s; path_prefix := prefix @@ -406,8 +402,9 @@ type variable_context = variable_info list type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap.t let sectab = - ref ([] : ((Names.Id.t * Decl_kinds.binding_kind) list * - Cooking.work_list * abstr_list) list) + Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind) list * + Cooking.work_list * abstr_list) list) + ~name:"section-context" let add_section () = sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),(Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab @@ -475,16 +472,6 @@ let section_instance = function let is_in_section ref = try ignore (section_instance ref); true with Not_found -> false -let init_sectab () = sectab := [] -let freeze_sectab () = !sectab -let unfreeze_sectab s = sectab := s - -let _ = - Summary.declare_summary "section-context" - { Summary.freeze_function = freeze_sectab; - Summary.unfreeze_function = unfreeze_sectab; - Summary.init_function = init_sectab } - (*************) (* Sections. *) @@ -502,7 +489,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 = freeze_summaries() in + let fs = Summary.freeze_summaries() 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); @@ -564,7 +551,7 @@ let set_lib_stk new_lib_stk = lib_stk := new_lib_stk; recalc_path_prefix (); let spf = match find_entry_p is_frozen_state with - | (sp, FrozenState f) -> unfreeze_summaries f; sp + | (sp, FrozenState f) -> Summary.unfreeze_summaries f; sp | _ -> assert false in let (after,_,_) = split_lib spf in @@ -635,7 +622,7 @@ let init () = add_frozen_state (); comp_name := None; path_prefix := initial_prefix; - init_summaries() + Summary.init_summaries () (* Misc *) diff --git a/library/library.ml b/library/library.ml index 7c34a62d0..e1ef4515d 100644 --- a/library/library.ml +++ b/library/library.ml @@ -45,40 +45,16 @@ module LibraryMap = Map.Make(LibraryOrdered) module LibraryFilenameMap = Map.Make(LibraryOrdered) (* This is a map from names to loaded libraries *) -let libraries_table = ref LibraryMap.empty +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 libraries_loaded_list = ref [] -let libraries_imports_list = ref [] -let libraries_exports_list = ref [] - -let freeze () = - !libraries_table, - !libraries_loaded_list, - !libraries_imports_list, - !libraries_exports_list - -let unfreeze (mt,mo,mi,me) = - libraries_table := mt; - libraries_loaded_list := mo; - libraries_imports_list := mi; - libraries_exports_list := me - -let init () = - libraries_table := LibraryMap.empty; - libraries_loaded_list := []; - libraries_imports_list := []; - libraries_exports_list := [] - -let _ = - Summary.declare_summary "MODULES" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } +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/loadpath.ml b/library/loadpath.ml index 315cbf96e..873703aff 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -20,13 +20,7 @@ type t = { path_is_root : bool; } -let load_paths = ref ([] : t list) - -let () = Summary.declare_summary "LOADPATHS" { - Summary.freeze_function = (fun () -> !load_paths); - Summary.unfreeze_function = (fun l -> load_paths := l); - Summary.init_function = (fun () -> load_paths := []); -} +let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" let logical p = p.path_logical diff --git a/library/nametab.ml b/library/nametab.ml index 01324a3a4..1d43725f6 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -540,19 +540,9 @@ let global_inductive r = (********************************************************************) (* Registration of tables as a global table and rollback *) -type frozen = ccitab * dirtab * mptab * kntab +type frozen = ccitab * dirtab * mptab * kntab * globrevtab * mprevtab * mptrevtab * knrevtab -let init () = - the_ccitab := ExtRefTab.empty; - the_dirtab := DirTab.empty; - the_modtypetab := MPTab.empty; - the_tactictab := KnTab.empty; - the_globrevtab := Globrevtab.empty; - the_modrevtab := MPmap.empty; - the_modtyperevtab := MPmap.empty; - the_tacticrevtab := KNmap.empty - let freeze () : frozen = !the_ccitab, !the_dirtab, @@ -577,7 +567,7 @@ let _ = Summary.declare_summary "names" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init } + Summary.init_function = Summary.nop } (* Deprecated synonyms *) diff --git a/library/summary.ml b/library/summary.ml index c6de35744..797cb64bf 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -19,6 +19,9 @@ let summaries = (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t) let internal_declare_summary sumname sdecl = + if Hashtbl.mem summaries sumname then + anomaly ~label:"Summary.declare_summary" + (str "Cannot declare a summary twice: " ++ str sumname); let (infun,outfun) = Dyn.create sumname in let dyn_freeze () = infun (sdecl.freeze_function()) and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum) @@ -28,9 +31,6 @@ let internal_declare_summary sumname sdecl = unfreeze_function = dyn_unfreeze; init_function = dyn_init } in - if Hashtbl.mem summaries sumname then - anomaly ~label:"Summary.declare_summary" - (str "Cannot declare a summary twice: " ++ str sumname); Hashtbl.add summaries sumname ddecl let declare_summary sumname decl = @@ -45,7 +45,6 @@ let freeze_summaries () = summaries; !m - let unfreeze_summaries fs = Hashtbl.iter (fun id decl -> @@ -55,3 +54,18 @@ let unfreeze_summaries fs = let init_summaries () = Hashtbl.iter (fun _ decl -> decl.init_function()) summaries + +(** For global tables registered statically before the end of coqtop + launch, the following empty [init_function] could be used. *) + +let nop () = () + +(** All-in-one reference declaration + registration *) + +let ref ~name x = + let r = ref x in + declare_summary name + { freeze_function = (fun () -> !r); + unfreeze_function = ((:=) r); + init_function = (fun () -> r := x) }; + r diff --git a/library/summary.mli b/library/summary.mli index 7ded099ab..fd1b324c9 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -14,17 +14,36 @@ type 'a summary_declaration = { unfreeze_function : 'a -> unit; init_function : unit -> unit } +(** For tables registered during the launch of coqtop, the [init_function] + will be run only once, during an [init_summaries] done at the end of + coqtop initialization. For tables registered later (for instance + during a plugin dynlink), [init_function] is used when unfreezing + an earlier frozen state that doesn't contain any value for this table. + + Beware: for tables registered dynamically after the initialization + of Coq, their init functions may not be run immediately. It is hence + the responsability of plugins to initialize themselves properly. +*) + val declare_summary : string -> 'a summary_declaration -> unit +(** All-in-one reference declaration + summary registration. + It behaves just as OCaml's standard [ref] function, except + that a [declare_summary] is done, with [name] as string. + The [init_function] restores the reference to its initial value. *) + +val ref : name:string -> 'a -> 'a ref + +(** For global tables registered statically before the end of coqtop + launch, the following empty [init_function] could be used. *) + +val nop : unit -> unit + +(** The type [frozen] is a snapshot of the states of all the registered + tables of the system. *) + type frozen val freeze_summaries : unit -> frozen val unfreeze_summaries : frozen -> unit val init_summaries : unit -> unit - -(** Beware: if some code is dynamically loaded via dynlink after the - initialization of Coq, the init functions of any summary declared - by this code may not be run. It is hence the responsability of - plugins to initialize themselves properly. -*) - diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 8edc56467..85e80dcb6 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -330,13 +330,11 @@ let init_grammar () = let init () = init_grammar () -open Summary - let _ = - declare_summary "GRAMMAR_LEXER" - { freeze_function = freeze; - unfreeze_function = unfreeze; - init_function = init } + Summary.declare_summary "GRAMMAR_LEXER" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init } let with_grammar_rule_protection f x = let fs = freeze () in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index a848d9c21..ebe7230ec 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -11,7 +11,6 @@ open Term open Declarations open Nameops open Namegen -open Summary open Libobject open Goptions open Libnames @@ -561,7 +560,7 @@ let _ = declare_string_option type lang = Ocaml | Haskell | Scheme -let lang_ref = ref Ocaml +let lang_ref = Summary.ref Ocaml ~name:"ExtrLang" let lang () = !lang_ref @@ -571,18 +570,13 @@ let extr_lang : lang -> obj = cache_function = (fun (_,l) -> lang_ref := l); load_function = (fun _ (_,l) -> lang_ref := l)} -let _ = declare_summary "Extraction Lang" - { freeze_function = (fun () -> !lang_ref); - unfreeze_function = ((:=) lang_ref); - init_function = (fun () -> lang_ref := Ocaml) } - let extraction_language x = Lib.add_anonymous_leaf (extr_lang x) (*s Extraction Inline/NoInline *) let empty_inline_table = (Refset'.empty,Refset'.empty) -let inline_table = ref empty_inline_table +let inline_table = Summary.ref empty_inline_table ~name:"ExtrInline" let to_inline r = Refset'.mem r (fst !inline_table) @@ -609,11 +603,6 @@ let inline_extraction : bool * global_reference list -> obj = (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l))) } -let _ = declare_summary "Extraction Inline" - { freeze_function = (fun () -> !inline_table); - unfreeze_function = ((:=) inline_table); - init_function = (fun () -> inline_table := empty_inline_table) } - (* Grammar entries. *) let extraction_inline b l = @@ -652,7 +641,7 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ()) type int_or_id = ArgInt of int | ArgId of Id.t -let implicits_table = ref Refmap'.empty +let implicits_table = Summary.ref Refmap'.empty ~name:"ExtrImplicit" let implicits_of_global r = try Refmap'.find r !implicits_table with Not_found -> [] @@ -688,11 +677,6 @@ let implicit_extraction : global_reference * int_or_id list -> obj = subst_function = (fun (s,(r,l)) -> (fst (subst_global s r), l)) } -let _ = declare_summary "Extraction Implicit" - { freeze_function = (fun () -> !implicits_table); - unfreeze_function = ((:=) implicits_table); - init_function = (fun () -> implicits_table := Refmap'.empty) } - (* Grammar entries. *) let extraction_implicit r l = @@ -702,7 +686,7 @@ let extraction_implicit r l = (*s Extraction Blacklist of filenames not to use while extracting *) -let blacklist_table = ref Id.Set.empty +let blacklist_table = Summary.ref Id.Set.empty ~name:"ExtrBlacklist" let modfile_ids = ref [] let modfile_mps = ref MPmap.empty @@ -747,11 +731,6 @@ let blacklist_extraction : string list -> obj = subst_function = (fun (_,x) -> x) } -let _ = declare_summary "Extraction Blacklist" - { freeze_function = (fun () -> !blacklist_table); - unfreeze_function = ((:=) blacklist_table); - init_function = (fun () -> blacklist_table := Id.Set.empty) } - (* Grammar entries. *) let extraction_blacklist l = @@ -779,7 +758,7 @@ let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ()) let use_type_scheme_nb_args, register_type_scheme_nb_args = let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r -let customs = ref Refmap'.empty +let customs = Summary.ref Refmap'.empty ~name:"ExtrCustom" let add_custom r ids s = customs := Refmap'.add r (ids,s) !customs @@ -791,7 +770,7 @@ let find_custom r = snd (Refmap'.find r !customs) let find_type_custom r = Refmap'.find r !customs -let custom_matchs = ref Refmap'.empty +let custom_matchs = Summary.ref Refmap'.empty ~name:"ExtrCustomMatchs" let add_custom_match r s = custom_matchs := Refmap'.add r s !custom_matchs @@ -823,11 +802,6 @@ let in_customs : global_reference * string list * string -> obj = (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str)) } -let _ = declare_summary "ML extractions" - { freeze_function = (fun () -> !customs); - unfreeze_function = ((:=) customs); - init_function = (fun () -> customs := Refmap'.empty) } - let in_custom_matchs : global_reference * string -> obj = declare_object {(default_object "ML extractions custom matchs") with @@ -837,11 +811,6 @@ let in_custom_matchs : global_reference * string -> obj = subst_function = (fun (subs,(r,s)) -> (fst (subst_global subs r), s)) } -let _ = declare_summary "ML extractions custom match" - { freeze_function = (fun () -> !custom_matchs); - unfreeze_function = ((:=) custom_matchs); - init_function = (fun () -> custom_matchs := Refmap'.empty) } - (* Grammar entries. *) let extract_constant_inline inline r ids s = diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 1e8f4afdf..c6f04027b 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -238,8 +238,9 @@ type function_info = (* let function_table = ref ([] : function_db) *) -let from_function = ref Cmap.empty -let from_graph = ref Indmap.empty +let from_function = Summary.ref Cmap.empty ~name:"functions_db_fn" +let from_graph = Summary.ref Indmap.empty ~name:"functions_db_gr" + (* let rec do_cache_info finfo = function | [] -> raise Not_found @@ -371,26 +372,6 @@ let in_Function : function_info -> Libobject.obj = } - -(* Synchronisation with reset *) -let freeze () = - !from_function,!from_graph -let unfreeze (functions,graphs) = -(* Pp.msgnl (str "unfreezing function_table : " ++ pr_table l); *) - from_function := functions; - from_graph := graphs - -let init () = -(* Pp.msgnl (str "reseting function_table"); *) - from_function := Cmap.empty; - from_graph := Indmap.empty - -let _ = - Summary.declare_summary "functions_db_sum" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } - let find_or_none id = try Some (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly (Pp.str "Not a constant") diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 1b2ba0e87..48741525d 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -333,9 +333,9 @@ type ring_info = module Cmap = Map.Make(struct type t = constr let compare = constr_ord end) -let from_carrier = ref Cmap.empty -let from_relation = ref Cmap.empty -let from_name = ref Spmap.empty +let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" +let from_relation = Summary.ref Cmap.empty ~name:"ring-tac-rel-table" +let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table" let ring_for_carrier r = Cmap.find r !from_carrier let ring_for_relation rel = Cmap.find rel !from_relation @@ -366,18 +366,6 @@ let find_ring_structure env sigma l = (str"cannot find a declared ring structure for equality"++ spc()++str"\""++pr_constr req++str"\"")) *) -let _ = - Summary.declare_summary "tactic-new-ring-table" - { Summary.freeze_function = - (fun () -> !from_carrier,!from_relation,!from_name); - Summary.unfreeze_function = - (fun (ct,rt,nt) -> - from_carrier := ct; from_relation := rt; from_name := nt); - Summary.init_function = - (fun () -> - from_carrier := Cmap.empty; from_relation := Cmap.empty; - from_name := Spmap.empty) } - let add_entry (sp,_kn) e = (* let _ = ty e.ring_lemma1 in let _ = ty e.ring_lemma2 in @@ -910,10 +898,9 @@ type field_info = field_pre_tac : glob_tactic_expr; field_post_tac : glob_tactic_expr } -let field_from_carrier = ref Cmap.empty -let field_from_relation = ref Cmap.empty -let field_from_name = ref Spmap.empty - +let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table" +let field_from_relation = Summary.ref Cmap.empty ~name:"field-tac-rel-table" +let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table" let field_for_carrier r = Cmap.find r !field_from_carrier let field_for_relation rel = Cmap.find rel !field_from_relation @@ -943,19 +930,6 @@ let find_field_structure env sigma l = (str"cannot find a declared field structure for equality"++ spc()++str"\""++pr_constr req++str"\"")) *) -let _ = - Summary.declare_summary "tactic-new-field-table" - { Summary.freeze_function = - (fun () -> !field_from_carrier,!field_from_relation,!field_from_name); - Summary.unfreeze_function = - (fun (ct,rt,nt) -> - field_from_carrier := ct; field_from_relation := rt; - field_from_name := nt); - Summary.init_function = - (fun () -> - field_from_carrier := Cmap.empty; field_from_relation := Cmap.empty; - field_from_name := Spmap.empty) } - let add_field_entry (sp,_kn) e = (* let _ = ty e.field_ok in diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 42099f5db..4562c5aa5 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -15,14 +15,9 @@ open Util open Libobject (*i*) -let empty_name_table = (Refmap.empty : Name.t list list Refmap.t) -let name_table = ref empty_name_table - -let _ = - Summary.declare_summary "rename-arguments" - { Summary.freeze_function = (fun () -> !name_table); - Summary.unfreeze_function = (fun r -> name_table := r); - Summary.init_function = (fun () -> name_table := empty_name_table) } +let name_table = + Summary.ref (Refmap.empty : Name.t list list Refmap.t) + ~name:"rename-arguments" type req = | ReqLocal diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d9a22b3e7..82dda8e0f 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -164,11 +164,7 @@ let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c) (* Generator of metavariables *) let new_meta = - let meta_ctr = ref 0 in - Summary.declare_summary "meta counter" - { Summary.freeze_function = (fun () -> !meta_ctr); - Summary.unfreeze_function = (fun n -> meta_ctr := n); - Summary.init_function = (fun () -> meta_ctr := 0) }; + let meta_ctr = Summary.ref 0 ~name:"meta counter" in fun () -> incr meta_ctr; !meta_ctr let mk_new_meta () = mkMeta(new_meta()) @@ -262,11 +258,7 @@ let make_pure_subst evi args = (* Generator of existential names *) let new_untyped_evar = - let evar_ctr = ref 0 in - Summary.declare_summary "evar counter" - { Summary.freeze_function = (fun () -> !evar_ctr); - Summary.unfreeze_function = (fun n -> evar_ctr := n); - Summary.init_function = (fun () -> evar_ctr := 0) }; + let evar_ctr = Summary.ref 0 ~name:"evar counter" in fun () -> incr evar_ctr; existential_of_int !evar_ctr (*------------------------------------* diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 7c2ac1a27..5aced6e10 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -39,8 +39,10 @@ type struc_typ = { s_PROJKIND : (Name.t * bool) list; s_PROJ : constant option list } -let structure_table = ref (Indmap.empty : struc_typ Indmap.t) -let projection_table = ref Cmap.empty +let structure_table = + Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs" +let projection_table = + Summary.ref Cmap.empty ~name:"record-projs" (* TODO: could be unify struc_typ and struc_tuple ? in particular, is the inductive always (fst constructor) ? It seems so... *) @@ -126,15 +128,7 @@ module MethodsDnet : Term_dnet.S let direction = true end) -let meth_dnet = ref MethodsDnet.empty - -open Summary - -let _ = - declare_summary "record-methods-state" - { freeze_function = (fun () -> !meth_dnet); - unfreeze_function = (fun m -> meth_dnet := m); - init_function = (fun () -> meth_dnet := MethodsDnet.empty) } +let meth_dnet = Summary.ref MethodsDnet.empty ~name:"record-methods-state" open Libobject @@ -194,7 +188,9 @@ type cs_pattern = | Sort_cs of sorts_family | Default_cs -let object_table = ref (Refmap.empty : (cs_pattern * obj_typ) list Refmap.t) +let object_table = + Summary.ref (Refmap.empty : (cs_pattern * obj_typ) list Refmap.t) + ~name:"record-canonical-structs" let canonical_projections () = Refmap.fold (fun x -> List.fold_right (fun (y,c) acc -> ((x,y),c)::acc)) @@ -346,21 +342,3 @@ let is_open_canonical_projection env sigma (c,args) = not (isConstruct hd) with Failure _ -> false with Not_found -> false - -let freeze () = - !structure_table, !projection_table, !object_table - -let unfreeze (s,p,o) = - structure_table := s; projection_table := p; object_table := o - -let init () = - structure_table := Indmap.empty; projection_table := Cmap.empty; - object_table := Refmap.empty - -let _ = init() - -let _ = - Summary.declare_summary "objdefs" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index b46b69c62..efc2a7467 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -134,22 +134,7 @@ type constant_evaluation = type frozen = constant_evaluation Cmap.t -let eval_table = ref (Cmap.empty : frozen) - -let init () = - eval_table := Cmap.empty - -let freeze () = - !eval_table - -let unfreeze ct = - eval_table := ct - -let _ = - Summary.declare_summary "evaluation" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } +let eval_table = Summary.ref (Cmap.empty : frozen) ~name:"evaluation" (* [compute_consteval] determines whether c is an "elimination constant" @@ -548,13 +533,8 @@ type behaviour = { b_dont_expose_case: bool; } -let behaviour_table = ref (Refmap.empty : behaviour Refmap.t) - -let _ = - Summary.declare_summary "simplbehaviour" - { Summary.freeze_function = (fun () -> !behaviour_table); - Summary.unfreeze_function = (fun x -> behaviour_table := x); - Summary.init_function = (fun () -> behaviour_table := Refmap.empty) } +let behaviour_table = + Summary.ref (Refmap.empty : behaviour Refmap.t) ~name:"simplbehaviour" type simpl_flag = [ `SimplDontExposeCase | `SimplNeverUnfold ] type req = diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 25109ffcf..86ff2a28f 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -93,25 +93,8 @@ let new_instance cl pri glob impl = * states management *) -let classes : typeclasses ref = ref Gmap.empty - -let instances : instances ref = ref Gmap.empty - -let freeze () = !classes, !instances - -let unfreeze (cl,is) = - classes:=cl; - instances:=is - -let init () = - classes:= Gmap.empty; - instances:= Gmap.empty - -let _ = - Summary.declare_summary "classes_and_instances" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } +let classes : typeclasses ref = Summary.ref Gmap.empty ~name:"classes" +let instances : instances ref = Summary.ref Gmap.empty ~name:"instances" let class_info c = try Gmap.find c !classes diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 828da8688..80d0ead96 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -20,7 +20,6 @@ open Tacred open Closure open RedFlags open Libobject -open Summary open Misctypes (* call by value normalisation function using the virtual machine *) @@ -106,10 +105,10 @@ let inStrategy : strategy_obj -> obj = let set_strategy local str = Lib.add_anonymous_leaf (inStrategy (local,str)) -let _ = declare_summary "Transparent constants and variables" - { freeze_function = Conv_oracle.freeze; - unfreeze_function = Conv_oracle.unfreeze; - init_function = Conv_oracle.init } +let _ = Summary.declare_summary "Transparent constants and variables" + { Summary.freeze_function = Conv_oracle.freeze; + Summary.unfreeze_function = Conv_oracle.unfreeze; + Summary.init_function = Summary.nop } (* Generic reduction: reduction functions used in reduction tactics *) @@ -148,7 +147,7 @@ let reduction_tab = ref String.Map.empty (* table of custom reduction expressions, synchronized, filled by command Declare Reduction *) -let red_expr_tab = ref String.Map.empty +let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction" let declare_reduction s f = if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab @@ -253,8 +252,3 @@ let inReduction : bool * string * red_expr -> obj = let declare_red_expr locality s expr = Lib.add_anonymous_leaf (inReduction (locality,s,expr)) - -let _ = declare_summary "Declare Reduction" - { freeze_function = (fun () -> !red_expr_tab); - unfreeze_function = ((:=) red_expr_tab); - init_function = (fun () -> red_expr_tab := String.Map.empty) } diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 38a616dde..39e0c653c 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -58,16 +58,7 @@ module HintDN = Term_dnet.Make(HintIdent)(HintOpt) (* Summary and Object declaration *) let rewtab = - ref (String.Map.empty : HintDN.t String.Map.t) - -let _ = - let init () = rewtab := String.Map.empty in - let freeze () = !rewtab in - let unfreeze fs = rewtab := fs in - Summary.declare_summary "autorewrite" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } + Summary.ref (String.Map.empty : HintDN.t String.Map.t) ~name:"autorewrite" let raw_find_base bas = String.Map.find bas !rewtab diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 45a705f35..8da15e8da 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -276,20 +276,13 @@ let make_hints g st only_classes sign = (PathEmpty, []) sign in Hint_db.add_list hintlist (Hint_db.empty st true) -let autogoal_hints_cache : (bool * Environ.named_context_val * hint_db) option ref = ref None +let autogoal_hints_cache + : (bool * Environ.named_context_val * hint_db) option ref + = Summary.ref None ~name:"autogoal-hints-cache" let freeze () = !autogoal_hints_cache let unfreeze v = autogoal_hints_cache := v -let init () = autogoal_hints_cache := None -let _ = init () - -let _ = - Summary.declare_summary "autogoal-hints-cache" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } - -let make_autogoal_hints = +let make_autogoal_hints = fun only_classes ?(st=full_transparent_state) g -> let sign = pf_filtered_hyps g in match freeze () with diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index a8188d582..0ec167873 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -406,7 +406,6 @@ END open Tactics open Glob_term -open Summary open Libobject open Lib @@ -415,8 +414,8 @@ open Lib x R y -> x == z -> z R y (in the left table) *) -let transitivity_right_table = ref [] -let transitivity_left_table = ref [] +let transitivity_right_table = Summary.ref [] ~name:"transitivity-steps-r" +let transitivity_left_table = Summary.ref [] ~name:"transitivity-steps-l" (* [step] tries to apply a rewriting lemma; then apply [tac] intended to complete to proof of the last hypothesis (assumed to state an equality) *) @@ -448,24 +447,6 @@ let inTransitivity : bool * constr -> obj = subst_function = subst_transitivity_lemma; classify_function = (fun o -> Substitute o) } -(* Synchronisation with reset *) - -let freeze () = !transitivity_left_table, !transitivity_right_table - -let unfreeze (l,r) = - transitivity_left_table := l; - transitivity_right_table := r - -let init () = - transitivity_left_table := []; - transitivity_right_table := [] - -let _ = - declare_summary "transitivity-steps" - { freeze_function = freeze; - unfreeze_function = unfreeze; - init_function = init } - (* Main entry points *) let add_transitivity_lemma left lem = diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index db2c19f00..d1abdd0af 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -155,17 +155,12 @@ let lookup_tactic s = (* Summary and Object declaration *) -let mactab = ref (Gmap.empty : (ltac_constant,glob_tactic_expr) Gmap.t) +let mactab = + Summary.ref (Gmap.empty : (ltac_constant,glob_tactic_expr) Gmap.t) + ~name:"tactic-definition" let lookup_ltacref r = Gmap.find r !mactab -let _ = - Summary.declare_summary "tactic-definition" - { Summary.freeze_function = (fun () -> !mactab); - Summary.unfreeze_function = (fun fs -> mactab := fs); - Summary.init_function = (fun () -> mactab := Gmap.empty); } - - (* We have identifier <| global_reference <| constr *) diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml index 561485833..7a13890b5 100644 --- a/tactics/tactic_option.ml +++ b/tactics/tactic_option.ml @@ -10,12 +10,17 @@ open Libobject open Pp let declare_tactic_option ?(default=Tacexpr.TacId []) name = - let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref default in - let default_tactic : Proof_type.tactic ref = ref (Tacinterp.eval_tactic !default_tactic_expr) in - let locality = ref false in - let set_default_tactic local t = + let locality = Summary.ref false ~name:(name^"-locality") in + let default_tactic_expr : Tacexpr.glob_tactic_expr ref = + Summary.ref default ~name:(name^"-default-tacexpr") + in + let default_tactic : Proof_type.tactic ref = + ref (Tacinterp.eval_tactic !default_tactic_expr) + in + let set_default_tactic local t = locality := local; - default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t + default_tactic_expr := t; + default_tactic := Tacinterp.eval_tactic t in let cache (_, (local, tac)) = set_default_tactic local tac in let load (_, (local, tac)) = @@ -43,12 +48,4 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name = Pptactic.pr_glob_tactic (Global.env ()) !default_tactic_expr ++ (if !locality then str" (locally defined)" else str" (globally defined)") in - let freeze () = !locality, !default_tactic_expr in - let unfreeze (local, t) = set_default_tactic local t in - let init () = () in - Summary.declare_summary name - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init }; - put, get, print - + put, get, print diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 5acbb78b7..5413e69a0 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -32,7 +32,7 @@ type individual_scheme_object_function = inductive -> constr type 'a scheme_kind = string -let scheme_map = ref Indmap.empty +let scheme_map = Summary.ref Indmap.empty ~name:"Schemes" let cache_one_scheme kind (ind,const) = let map = try Indmap.find ind !scheme_map with Not_found -> String.Map.empty in @@ -61,19 +61,6 @@ let inScheme : string * (inductive * constant) array -> obj = discharge_function = discharge_scheme} (**********************************************************************) -(* Saving/restoring the table of scheme *) - -let freeze_schemes () = !scheme_map -let unfreeze_schemes sch = scheme_map := sch -let init_schemes () = scheme_map := Indmap.empty - -let _ = - Summary.declare_summary "Schemes" - { Summary.freeze_function = freeze_schemes; - Summary.unfreeze_function = unfreeze_schemes; - Summary.init_function = init_schemes } - -(**********************************************************************) (* The table of scheme building functions *) type individual diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 7a0c498b2..8c7c377bf 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -446,23 +446,8 @@ let map_first m = assert(false) with Found x -> x -let from_prg : program_info ProgMap.t ref = ref ProgMap.empty - -let freeze () = !from_prg -let unfreeze v = from_prg := v -let init () = from_prg := ProgMap.empty - -(** Beware: if this code is dynamically loaded via dynlink after the start - of Coq, then this [init] function will not be run by [Lib.init ()]. - Luckily, here we can launch [init] at load-time. *) - -let _ = init () - -let _ = - Summary.declare_summary "program-tcc-table" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } +let from_prg : program_info ProgMap.t ref = + Summary.ref ProgMap.empty ~name:"program-tcc-table" let close sec = if not (ProgMap.is_empty !from_prg) then |