From 0c68df5ccdacb5d2ed50b533ad613723914dfee7 Mon Sep 17 00:00:00 2001 From: filliatr Date: Fri, 24 Nov 2000 16:13:28 +0000 Subject: certains effets disparaissent a la sortie des sections, d'autres non (selon Summary.survive_section) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@945 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declare.ml | 6 ++++-- library/global.ml | 3 ++- library/goptions.ml | 6 ++++-- library/impargs.ml | 3 ++- library/lib.ml | 12 ++++++------ library/lib.mli | 7 ++++--- library/library.ml | 3 ++- library/nametab.ml | 3 ++- library/summary.ml | 15 +++++++++++++-- library/summary.mli | 4 +++- 10 files changed, 42 insertions(+), 20 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index b90dc2215..e1884ed5f 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -52,7 +52,8 @@ let vartab = ref (Spmap.empty : (identifier * variable_declaration) Spmap.t) let _ = Summary.declare_summary "VARIABLE" { Summary.freeze_function = (fun () -> !vartab); Summary.unfreeze_function = (fun ft -> vartab := ft); - Summary.init_function = (fun () -> vartab := Spmap.empty) } + Summary.init_function = (fun () -> vartab := Spmap.empty); + Summary.survive_section = false } let cache_variable (sp,(id,(d,_,_) as vd)) = begin match d with (* Fails if not well-typed *) @@ -114,7 +115,8 @@ let csttab = ref (Spmap.empty : strength Spmap.t) let _ = Summary.declare_summary "CONSTANT" { Summary.freeze_function = (fun () -> !csttab); Summary.unfreeze_function = (fun ft -> csttab := ft); - Summary.init_function = (fun () -> csttab := Spmap.empty) } + Summary.init_function = (fun () -> csttab := Spmap.empty); + Summary.survive_section = false } let cache_constant (sp,(cdt,stre)) = begin match cdt with diff --git a/library/global.ml b/library/global.ml index d5885ed02..2fcd3c2b6 100644 --- a/library/global.ml +++ b/library/global.ml @@ -23,7 +23,8 @@ let _ = declare_summary "Global environment" { freeze_function = (fun () -> !global_env); unfreeze_function = (fun fr -> global_env := fr); - init_function = (fun () -> global_env := empty_environment) } + init_function = (fun () -> global_env := empty_environment); + survive_section = true } (* Then we export the functions of [Typing] on that environment. *) diff --git a/library/goptions.ml b/library/goptions.ml index dc5f994e3..59d0543e2 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -77,7 +77,8 @@ module MakeTable = Summary.declare_summary kn { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init } + Summary.init_function = init; + Summary.survive_section = true } let (add_option,remove_option) = if A.synchronous then @@ -219,7 +220,8 @@ let _ = Summary.declare_summary "Sync_option" { Summary.freeze_function = freeze_sync_table; Summary.unfreeze_function = unfreeze_sync_table; - Summary.init_function = init_sync_table } + Summary.init_function = init_sync_table; + Summary.survive_section = true } (* Tools for handling options *) diff --git a/library/impargs.ml b/library/impargs.ml index 6ef403f59..3232c4848 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -314,7 +314,8 @@ let _ = Summary.declare_summary "implicits" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init } + Summary.init_function = init; + Summary.survive_section = true } let rollback f x = let fs = freeze () in diff --git a/library/lib.ml b/library/lib.ml index a22f89353..9b5ba27b7 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -9,7 +9,7 @@ open Summary type node = | Leaf of obj | Module of string - | OpenedSection of string + | OpenedSection of string * Summary.frozen (* bool is to tell if the section must be opened automatically *) | ClosedSection of bool * string * library_segment * Nametab.module_contents | FrozenState of Summary.frozen @@ -103,7 +103,7 @@ let contents_after = function let open_section s = let sp = make_path (id_of_string s) OBJ in - add_entry sp (OpenedSection s); + add_entry sp (OpenedSection (s, freeze_summaries())); path_prefix := !path_prefix @ [s]; sp @@ -138,10 +138,10 @@ let export_segment seg = clean [] seg let close_section export f s = - let sp = + let sp,fs = try match find_entry_p is_opened_section with - | sp,OpenedSection s' -> - if s <> s' then error "this is not the last opened section"; sp + | sp,OpenedSection (s',fs) -> + if s <> s' then error "this is not the last opened section"; (sp,fs) | _ -> assert false with Not_found -> error "no opened section" @@ -150,7 +150,7 @@ let close_section export f s = lib_stk := before; let after' = export_segment after in pop_path_prefix (); - let contents = f sp after in + let contents = f fs sp after in add_entry (make_path (id_of_string s) OBJ) (ClosedSection (export, s,after',contents)); Nametab.push_module s contents; diff --git a/library/lib.mli b/library/lib.mli index 96b1941ce..397e5a53b 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -14,7 +14,7 @@ open Summary type node = | Leaf of obj | Module of string - | OpenedSection of string + | OpenedSection of string * Summary.frozen | ClosedSection of bool * string * library_segment * Nametab.module_contents | FrozenState of Summary.frozen @@ -41,8 +41,9 @@ val contents_after : section_path option -> library_segment val open_section : string -> section_path val close_section : export:bool -> - (section_path -> library_segment -> Nametab.module_contents) -> string - -> unit + (Summary.frozen -> section_path -> library_segment + -> Nametab.module_contents) + -> string -> unit val make_path : identifier -> path_kind -> section_path val cwd : unit -> dir_path diff --git a/library/library.ml b/library/library.ml index da7d01895..70cf895e5 100644 --- a/library/library.ml +++ b/library/library.ml @@ -54,7 +54,8 @@ let _ = Summary.declare_summary "MODULES" { Summary.freeze_function = (fun () -> !modules_table); Summary.unfreeze_function = (fun ft -> modules_table := ft); - Summary.init_function = (fun () -> modules_table := Stringmap.empty) } + Summary.init_function = (fun () -> modules_table := Stringmap.empty); + Summary.survive_section = true } let find_module s = try diff --git a/library/nametab.ml b/library/nametab.ml index c45e7d93e..de5c22c09 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -77,7 +77,8 @@ let _ = Summary.declare_summary "names" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init } + Summary.init_function = init; + Summary.survive_section = true } let rollback f x = let fs = freeze () in diff --git a/library/summary.ml b/library/summary.ml index 0ba07a737..8fbd5efe4 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -8,7 +8,8 @@ open Names type 'a summary_declaration = { freeze_function : unit -> 'a; unfreeze_function : 'a -> unit; - init_function : unit -> unit } + init_function : unit -> unit; + survive_section : bool } let summaries = (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t) @@ -21,7 +22,8 @@ let declare_summary sumname sdecl = let ddecl = { freeze_function = dyn_freeze; unfreeze_function = dyn_unfreeze; - init_function = dyn_init} + init_function = dyn_init; + survive_section = sdecl.survive_section } in if Hashtbl.mem summaries sumname then anomalylabstrm "Summary.declare_summary" @@ -44,5 +46,14 @@ let unfreeze_summaries fs = with Not_found -> decl.init_function()) summaries +let unfreeze_lost_summaries fs = + Hashtbl.iter + (fun id decl -> + try + if not decl.survive_section then + decl.unfreeze_function (Stringmap.find id fs) + with Not_found -> decl.init_function()) + summaries + let init_summaries () = Hashtbl.iter (fun _ decl -> decl.init_function()) summaries diff --git a/library/summary.mli b/library/summary.mli index 0d329a947..fc639d7f8 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -11,7 +11,8 @@ open Names type 'a summary_declaration = { freeze_function : unit -> 'a; unfreeze_function : 'a -> unit; - init_function : unit -> unit } + init_function : unit -> unit; + survive_section : bool } val declare_summary : string -> 'a summary_declaration -> unit @@ -19,6 +20,7 @@ type frozen val freeze_summaries : unit -> frozen val unfreeze_summaries : frozen -> unit +val unfreeze_lost_summaries : frozen -> unit val init_summaries : unit -> unit -- cgit v1.2.3