From 79a25a71dd3519d8e7a6bd9f3a004c7c0da3a1b5 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 13 Aug 2009 19:10:11 +0000 Subject: Death of "survive_module" and "survive_section" (the first one was only used to allow a module to be ended before the summaries were restored what can be solved by moving upwards the place where the summaries are restored). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12275 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declaremods.ml | 22 +++++++--------------- library/decls.ml | 8 ++------ library/dischargedhypsmap.ml | 4 +--- library/global.ml | 10 +++++----- library/global.mli | 5 +++-- library/goptions.ml | 10 +++------- library/heads.ml | 4 +--- library/impargs.ml | 4 +--- library/lib.ml | 6 ++---- library/library.ml | 4 +--- library/nametab.ml | 4 +--- library/summary.ml | 23 ++++------------------- library/summary.mli | 6 +----- 13 files changed, 32 insertions(+), 78 deletions(-) (limited to 'library') diff --git a/library/declaremods.ml b/library/declaremods.ml index 0aa3d96bb..581e3fd5b 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -100,9 +100,7 @@ let _ = Summary.declare_summary "MODULE-INFO" modtab_substobjs := MPmap.empty; modtab_objects := MPmap.empty; openmod_info := ([],None,None); - library_cache := Dirmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } + library_cache := Dirmap.empty) } (* auxiliary functions to transform full_path and kernel_name given by Lib into module_path and dir_path needed for modules *) @@ -512,9 +510,7 @@ let _ = Summary.declare_summary "MODTYPE-INFO" openmodtype_info := snd ft); Summary.init_function = (fun () -> modtypetab := MPmap.empty; - openmodtype_info := []); - Summary.survive_module = false; - Summary.survive_section = true } + openmodtype_info := []) } let cache_modtype ((sp,kn),(entry,modtypeobjs)) = @@ -754,15 +750,13 @@ let end_module () = dependencies on functor arguments *) let id = basename (fst oldoname) in - let mp = Global.end_module id res_o in + let mp = Global.end_module fs id res_o in begin match sub_o with None -> () | Some sub_mtb -> check_subtypes mp sub_mtb end; - Summary.module_unfreeze_summaries fs; - let substituted = subst_substobjs dir mp substobjs in let node = in_module (None,substobjs,substituted) in let objects = @@ -885,17 +879,15 @@ let end_modtype () = let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in let id = basename (fst oldoname) in - let ln = Global.end_modtype id in let substitute, _, special = Lib.classify_segment lib_stack in let msid = msid_of_prefix prefix in let mbids = !openmodtype_info in - - Summary.module_unfreeze_summaries fs; - let modtypeobjs = empty_subst, mbids, msid, substitute in + let ln = Global.end_modtype fs id in let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs)]) in + if fst oname <> fst oldoname then anomaly "Section paths generated on start_ and end_modtype do not match"; @@ -970,8 +962,8 @@ let rec get_module_substobjs env = function (map_mbid mbid mp (Some resolve))) , mbids, msid, objs) | [] -> match mexpr with - | MSEident _ -> error "Application of a non-functor" - | _ -> error "Application of a functor with too few arguments") + | MSEident _ -> error "Application of a non-functor." + | _ -> error "Application of a functor with too few arguments.") | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr | MSEwith (mty, With_Definition _) -> get_module_substobjs env mty diff --git a/library/decls.ml b/library/decls.ml index 5a8729215..d5d0cb096 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -27,9 +27,7 @@ let vartab = ref (Idmap.empty : variable_data Idmap.t) let _ = Summary.declare_summary "VARIABLE" { Summary.freeze_function = (fun () -> !vartab); Summary.unfreeze_function = (fun ft -> vartab := ft); - Summary.init_function = (fun () -> vartab := Idmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = (fun () -> vartab := Idmap.empty) } let add_variable_data id o = vartab := Idmap.add id o !vartab @@ -47,9 +45,7 @@ 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); - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = (fun () -> csttab := Cmap.empty) } let add_constant_kind kn k = csttab := Cmap.add kn k !csttab diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index 7812b1f9e..ed375a831 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -46,6 +46,4 @@ let _ = Summary.declare_summary "discharged_hypothesis" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = true } + Summary.init_function = init } diff --git a/library/global.ml b/library/global.ml index 4f3a40a8a..ec41c0706 100644 --- a/library/global.ml +++ b/library/global.ml @@ -31,9 +31,7 @@ let _ = declare_summary "Global environment" { freeze_function = (fun () -> !global_env); unfreeze_function = (fun fr -> global_env := fr); - init_function = (fun () -> global_env := empty_environment); - survive_module = true; - survive_section = false } + init_function = (fun () -> global_env := empty_environment) } (* Then we export the functions of [Typing] on that environment. *) @@ -82,9 +80,10 @@ let start_module id = global_env := newenv; mp -let end_module id mtyo = +let end_module fs id mtyo = let l = label_of_id id in let mp,newenv = end_module l mtyo !global_env in + Summary.unfreeze_summaries fs; global_env := newenv; mp @@ -100,9 +99,10 @@ let start_modtype id = global_env := newenv; mp -let end_modtype id = +let end_modtype fs id = let l = label_of_id id in let kn,newenv = end_modtype l !global_env in + Summary.unfreeze_summaries fs; global_env := newenv; kn diff --git a/library/global.mli b/library/global.mli index f0daef0ac..deafacba2 100644 --- a/library/global.mli +++ b/library/global.mli @@ -66,12 +66,13 @@ val set_engagement : engagement -> unit of the started module / module type *) val start_module : identifier -> module_path -val end_module : identifier -> module_struct_entry option -> module_path +val end_module : + Summary.frozen -> identifier -> module_struct_entry option -> module_path val add_module_parameter : mod_bound_id -> module_struct_entry -> unit val start_modtype : identifier -> module_path -val end_modtype : identifier -> module_path +val end_modtype : Summary.frozen -> identifier -> module_path diff --git a/library/goptions.ml b/library/goptions.ml index 6e58fd218..bf431e1fc 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -83,9 +83,7 @@ module MakeTable = Summary.declare_summary nick { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = true } + Summary.init_function = init } let (add_option,remove_option) = if A.synchronous then @@ -244,11 +242,9 @@ let declare_option cast uncast classify_function = (fun _ -> Dispose)} in let _ = declare_summary (nickname key) - {freeze_function = read; + { freeze_function = read; unfreeze_function = write; - init_function = (fun () -> write default); - survive_module = false; - survive_section = false} + init_function = (fun () -> write default) } in fun v -> add_anonymous_leaf (decl_obj v) else write diff --git a/library/heads.ml b/library/heads.ml index ba3a45594..c63634458 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -54,9 +54,7 @@ let _ = Summary.declare_summary "Head_decl" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = true; - Summary.survive_section = false } + Summary.init_function = init } 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 68809d6aa..aedb2d5a8 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -598,6 +598,4 @@ let _ = Summary.declare_summary "implicits" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } diff --git a/library/lib.ml b/library/lib.ml index c033a3805..1a3a07e01 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -519,9 +519,7 @@ let _ = Summary.declare_summary "section-context" { Summary.freeze_function = freeze_sectab; Summary.unfreeze_function = unfreeze_sectab; - Summary.init_function = init_sectab; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init_sectab } (*************) (* Sections. *) @@ -576,7 +574,7 @@ let close_section () = add_entry oname (ClosedSection (List.rev_append secdecls (List.rev secopening))); if !Flags.xml_export then !xml_close_section (basename (fst oname)); let newdecls = List.map discharge_item secdecls in - Summary.section_unfreeze_summaries fs; + Summary.unfreeze_summaries fs; List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; Cooking.clear_cooking_sharing (); Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) diff --git a/library/library.ml b/library/library.ml index 24c2c3803..831687723 100644 --- a/library/library.ml +++ b/library/library.ml @@ -180,9 +180,7 @@ let _ = Summary.declare_summary "MODULES" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } (* various requests to the tables *) diff --git a/library/nametab.ml b/library/nametab.ml index 797f88e39..074386417 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -548,9 +548,7 @@ let _ = Summary.declare_summary "names" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } (* Deprecated synonyms *) diff --git a/library/summary.ml b/library/summary.ml index 145ce9e00..784d79d87 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -14,9 +14,7 @@ open Util type 'a summary_declaration = { freeze_function : unit -> 'a; unfreeze_function : 'a -> unit; - init_function : unit -> unit; - survive_module : bool ; - survive_section : bool } + init_function : unit -> unit } let summaries = (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t) @@ -29,9 +27,7 @@ let internal_declare_summary sumname sdecl = let ddecl = { freeze_function = dyn_freeze; unfreeze_function = dyn_unfreeze; - init_function = dyn_init; - survive_module = sdecl.survive_module; - survive_section = sdecl.survive_section } + init_function = dyn_init } in if Hashtbl.mem summaries sumname then anomalylabstrm "Summary.declare_summary" @@ -51,23 +47,12 @@ let freeze_summaries () = !m -let unfreeze_some_summaries p fs = +let unfreeze_summaries fs = Hashtbl.iter (fun id decl -> - try - if p decl then - decl.unfreeze_function (Stringmap.find id fs) + try decl.unfreeze_function (Stringmap.find id fs) with Not_found -> decl.init_function()) summaries -let unfreeze_summaries = - unfreeze_some_summaries (fun _ -> true) - -let section_unfreeze_summaries = - unfreeze_some_summaries (fun decl -> not decl.survive_section) - -let module_unfreeze_summaries = - unfreeze_some_summaries (fun decl -> not decl.survive_module) - let init_summaries () = Hashtbl.iter (fun _ decl -> decl.init_function()) summaries diff --git a/library/summary.mli b/library/summary.mli index 3e6375b0e..e6e17ef8c 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -14,9 +14,7 @@ type 'a summary_declaration = { freeze_function : unit -> 'a; unfreeze_function : 'a -> unit; - init_function : unit -> unit; - survive_module : bool; (* should be false is most cases *) - survive_section : bool } + init_function : unit -> unit } val declare_summary : string -> 'a summary_declaration -> unit @@ -24,8 +22,6 @@ type frozen val freeze_summaries : unit -> frozen val unfreeze_summaries : frozen -> unit -val section_unfreeze_summaries : frozen -> unit -val module_unfreeze_summaries : frozen -> unit val init_summaries : unit -> unit (** Beware: if some code is dynamically loaded via dynlink after the -- cgit v1.2.3