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 --- CHANGES | 4 ++-- contrib/ring/Ring_theory.v | 2 ++ contrib/ring/ring.ml | 3 ++- 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 +++- parsing/pretty.ml | 4 ++-- pretyping/classops.ml | 3 ++- pretyping/recordops.ml | 3 ++- pretyping/syntax_def.ml | 3 ++- pretyping/tacred.ml | 3 ++- proofs/tacinterp.ml | 3 ++- tactics/auto.ml | 3 ++- tactics/dhyp.ml | 3 ++- tactics/equality.ml | 3 ++- toplevel/discharge.ml | 3 ++- toplevel/metasyntax.ml | 6 ++++-- toplevel/mltop.ml4 | 3 ++- 25 files changed, 74 insertions(+), 37 deletions(-) diff --git a/CHANGES b/CHANGES index 250386151..a474a84c5 100644 --- a/CHANGES +++ b/CHANGES @@ -74,6 +74,8 @@ que les 3 primitives), on peut typer avec "constr", "tactic", ou Arguments" et non plus selon la valeur qu'elle avait au moment de la définition dans la section. +- SearchPattern / SearchRewrite (contrib de Yves Bertot) + Tactiques - Langage de tactique @@ -90,8 +92,6 @@ Tactiques en général plus son nom (sauf dans les cas "simples"). Rem : c'est une source d'incompatibilité. -- EAuto réussit parfois plus (source d'incompatibilité). - - Intro échoue si le nom d'hypothèse existe au lieu de mettre un avertissement - Plus de "Require Prolog" (intégré par défaut) diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v index 2901942ef..c04eee57e 100644 --- a/contrib/ring/Ring_theory.v +++ b/contrib/ring/Ring_theory.v @@ -370,6 +370,8 @@ Save. End Theory_of_rings. +Hints Resolve Th_mult_zero_left Th_plus_reg_left : core. + Implicit Arguments Off. Definition Semi_Ring_Theory_of : diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 7b96983a7..d2c379659 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -126,7 +126,8 @@ let _ = Summary.declare_summary "tactic-ring-table" { Summary.freeze_function = (fun () -> !theories_map); Summary.unfreeze_function = (fun t -> theories_map := t); - Summary.init_function = (fun () -> theories_map := Cmap.empty) } + Summary.init_function = (fun () -> theories_map := Cmap.empty); + Summary.survive_section = false } (* declare a new type of object in the environment, "tactic-ring-theory" The functions theory_to_obj and obj_to_theory do the conversions 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 diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 7c4c40aa1..1d1deed7d 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -248,7 +248,7 @@ let rec print_library_entry with_values ent = match ent with | (sp,Lib.Leaf lobj) -> [< print_leaf_entry with_values sep (sp,lobj) >] - | (_,Lib.OpenedSection str) -> + | (_,Lib.OpenedSection (str,_)) -> [< 'sTR(" >>>>>>> Section " ^ str); 'fNL >] | (sp,Lib.ClosedSection _) -> [< 'sTR(" >>>>>>> Closed Section " ^ (string_of_id (basename sp))); @@ -286,7 +286,7 @@ let list_filter_vec f vec = let read_sec_context sec = let rec get_cxt in_cxt = function - | ((sp,Lib.OpenedSection str) as hd)::rest -> + | ((sp,Lib.OpenedSection (str,_)) as hd)::rest -> if str = sec then (hd::in_cxt) else get_cxt (hd::in_cxt) rest | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest diff --git a/pretyping/classops.ml b/pretyping/classops.ml index a452cf645..89542564d 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -182,7 +182,8 @@ let _ = Summary.declare_summary "inh_graph" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init } + Summary.init_function = init; + Summary.survive_section = true } (* classe d'un terme *) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 45b16c935..ef0e839bb 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -104,4 +104,5 @@ let _ = Summary.declare_summary "objdefs" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init } + Summary.init_function = init; + Summary.survive_section = true } diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml index f90627f7e..4801d017e 100644 --- a/pretyping/syntax_def.ml +++ b/pretyping/syntax_def.ml @@ -14,7 +14,8 @@ 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 := Spmap.empty) } + Summary.init_function = (fun () -> syntax_table := Spmap.empty); + Summary.survive_section = false } let add_syntax_constant sp c = syntax_table := Spmap.add sp c !syntax_table diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 1edeb78f8..ca2bcb705 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -49,7 +49,8 @@ let _ = Summary.declare_summary "evaluation" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init } + Summary.init_function = init; + Summary.survive_section = true } (* Check that c is an "elimination constant" diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 422d41222..4cd1641b1 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -169,7 +169,8 @@ let _ = Summary.declare_summary "tactic-definition" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init } + Summary.init_function = init; + Summary.survive_section = false } (* Unboxes the tactic_arg *) let unvarg = function diff --git a/tactics/auto.ml b/tactics/auto.ml index 27b04eedb..70ff2e639 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -142,7 +142,8 @@ let unfreeze fs = searchtable := fs let _ = Summary.declare_summary "search" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init } + Summary.init_function = init; + Summary.survive_section = false } (**************************************************************************) diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 628c337f9..6497287ab 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -177,7 +177,8 @@ let _ = Summary.declare_summary "destruct-hyp-concl" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init } + Summary.init_function = init; + Summary.survive_section = true } let cache_dd (_,(na,dd)) = try diff --git a/tactics/equality.ml b/tactics/equality.ml index a90114641..96c323d73 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1574,7 +1574,8 @@ let _ = Summary.declare_summary "autorewrite" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init } + Summary.init_function = init; + Summary.survive_section = false } (*Adds a list of rules to the rule table*) let add_list_rules rbase lrl = diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 6e79134bb..2b552fffc 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -290,13 +290,14 @@ and module_contents seg = let close_section _ s = let oldenv = Global.env() in - let process_segment sec_sp decls = + let process_segment fs sec_sp decls = let newdir = dirpath sec_sp in let olddir = wd_of_sp sec_sp in let (ops,ids,_) = List.fold_left (process_item oldenv newdir olddir) ([],[],([],[],[])) decls in + Summary.unfreeze_lost_summaries fs; Global.pop_named_decls ids; List.iter process_operation (List.rev ops); module_contents decls diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index eb7543f3d..0597238cd 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -38,7 +38,8 @@ let _ = declare_summary "syntax" { freeze_function = Esyntax.freeze; unfreeze_function = Esyntax.unfreeze; - init_function = Esyntax.init } + init_function = Esyntax.init; + survive_section = false } (* Pretty-printing objects = syntax_entry *) let cache_syntax (_,ppobj) = Esyntax.add_ppobject ppobj @@ -69,7 +70,8 @@ let _ = declare_summary "GRAMMAR_LEXER" { freeze_function = Egrammar.freeze; unfreeze_function = Egrammar.unfreeze; - init_function = Egrammar.init} + init_function = Egrammar.init; + survive_section = false } (* Tokens *) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index f255739b3..0c81359cb 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -200,7 +200,8 @@ let _ = Summary.declare_summary "ML-MODULES" { Summary.freeze_function = (fun () -> List.rev (get_loaded_modules())); Summary.unfreeze_function = (fun x -> unfreeze_ml_modules x); - Summary.init_function = (fun () -> init_ml_modules ()) } + Summary.init_function = (fun () -> init_ml_modules ()); + Summary.survive_section = true } (* Same as restore_ml_modules, but verbosely *) -- cgit v1.2.3