# HG changeset patch # User wenzelm # Date 1394788116 -3600 # Node ID ed92ce2ac88e492e4fe1c17e4942b0e3f92a241b # Parent b7add947a6effcc9ce75e737b936a678159ea675 just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.); more thorough background_notes: distribute global notes to all contexts; diff -r b7add947a6ef -r ed92ce2ac88e src/HOL/Lattices_Big.thy --- a/src/HOL/Lattices_Big.thy Thu Mar 13 17:26:22 2014 +0100 +++ b/src/HOL/Lattices_Big.thy Fri Mar 14 10:08:36 2014 +0100 @@ -640,6 +640,11 @@ shows "Max M \ Max N" using assms by (fact Max.antimono) +end + +context linorder (* FIXME *) +begin + lemma mono_Min_commute: assumes "mono f" assumes "finite A" and "A \ {}" diff -r b7add947a6ef -r ed92ce2ac88e src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Mar 13 17:26:22 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Mar 14 10:08:36 2014 +0100 @@ -459,7 +459,7 @@ else is_too_complex val local_facts = Proof_Context.facts_of ctxt - val named_locals = local_facts |> Facts.dest_static [] + val named_locals = local_facts |> Facts.dest_static [global_facts] val assms = Assumption.all_assms_of ctxt fun is_good_unnamed_local th = not (Thm.has_name_hint th) andalso @@ -467,14 +467,12 @@ val unnamed_locals = union Thm.eq_thm_prop (Facts.props local_facts) chained |> filter is_good_unnamed_local |> map (pair "" o single) - val full_space = - Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp - fun add_facts global foldx facts = + fun add_facts global foldx = foldx (fn (name0, ths) => fn accum => if name0 <> "" andalso forall (not o member Thm.eq_thm_prop add_ths) ths andalso - (Facts.is_concealed facts name0 orelse + (Facts.is_concealed local_facts name0 orelse (not generous andalso is_blacklisted_or_something name0)) then accum else @@ -499,8 +497,7 @@ if name0 = "" then backquote_thm ctxt th else - [Facts.extern ctxt facts name0, - Name_Space.extern ctxt full_space name0] + [Facts.extern ctxt local_facts name0] |> find_first check_thms |> the_default name0 |> make_name reserved multi j), @@ -515,8 +512,8 @@ (* The single-theorem names go before the multiple-theorem ones (e.g., "xxx" vs. "xxx(3)"), so that single names are preferred when both are available. *) - `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals) - |> add_facts true Facts.fold_static global_facts global_facts + `I [] |> add_facts false fold (unnamed_locals @ named_locals) + |> add_facts true Facts.fold_static global_facts |> op @ end diff -r b7add947a6ef -r ed92ce2ac88e src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Thu Mar 13 17:26:22 2014 +0100 +++ b/src/Pure/Isar/attrib.ML Fri Mar 14 10:08:36 2014 +0100 @@ -213,7 +213,7 @@ fun gen_thm pick = Scan.depend (fn context => let - val get = Context.cases (Global_Theory.get_fact context) Proof_Context.get_fact context; + val get = Proof_Context.get_fact_generic context; val get_fact = get o Facts.Fact; fun get_named pos name = get (Facts.Named ((name, pos), NONE)); in @@ -249,6 +249,8 @@ (** partial evaluation -- observing rule/declaration/mixed attributes **) +(*NB: result length may change due to rearrangement of symbolic expression*) + local fun apply_att src (context, th) = diff -r b7add947a6ef -r ed92ce2ac88e src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Thu Mar 13 17:26:22 2014 +0100 +++ b/src/Pure/Isar/generic_target.ML Fri Mar 14 10:08:36 2014 +0100 @@ -179,8 +179,7 @@ end; fun locale_notes locale kind global_facts local_facts = - Local_Theory.background_theory - (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #> + Local_Theory.background_notes kind (Attrib.map_facts (K []) global_facts) #> (fn lthy => lthy |> Local_Theory.target (fn ctxt => ctxt |> Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #> @@ -311,7 +310,7 @@ |> pair (lhs, def)); fun theory_notes kind global_facts local_facts = - Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #> + Local_Theory.background_notes kind global_facts #> (fn lthy => lthy |> Local_Theory.map_contexts (fn level => fn ctxt => if level = Local_Theory.level lthy then ctxt else diff -r b7add947a6ef -r ed92ce2ac88e src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Thu Mar 13 17:26:22 2014 +0100 +++ b/src/Pure/Isar/local_theory.ML Fri Mar 14 10:08:36 2014 +0100 @@ -32,6 +32,8 @@ val raw_theory: (theory -> theory) -> local_theory -> local_theory val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory val background_theory: (theory -> theory) -> local_theory -> local_theory + val background_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list -> + local_theory -> local_theory val target_of: local_theory -> Proof.context val target: (Proof.context -> Proof.context) -> local_theory -> local_theory val target_morphism: local_theory -> morphism @@ -215,6 +217,19 @@ fun background_theory f = #2 o background_theory_result (f #> pair ()); +fun background_notes kind facts lthy = + let + val facts1 = Attrib.partial_evaluation lthy facts; + val facts0 = Attrib.map_facts (K []) facts1; + in + lthy + |> background_theory (Attrib.global_notes kind facts1 #> snd) + |> map_contexts (fn _ => fn ctxt => ctxt + |> Proof_Context.map_naming (K (naming_of lthy)) + |> Attrib.local_notes kind facts0 |> snd + |> Proof_Context.restore_naming ctxt) + end; + (* target contexts *) diff -r b7add947a6ef -r ed92ce2ac88e src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Mar 13 17:26:22 2014 +0100 +++ b/src/Pure/Isar/locale.ML Fri Mar 14 10:08:36 2014 +0100 @@ -561,7 +561,7 @@ (* Registrations *) (fn thy => fold_rev (fn (_, morph) => - snd o Attrib.global_notes kind (Element.transform_facts morph facts)) + snd o Attrib.global_notes kind (Element.transform_facts morph facts)) (* FIXME background_notes *) (registrations_of (Context.Theory thy) loc) thy)); diff -r b7add947a6ef -r ed92ce2ac88e src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Mar 13 17:26:22 2014 +0100 +++ b/src/Pure/Isar/proof_context.ML Fri Mar 14 10:08:36 2014 +0100 @@ -53,9 +53,7 @@ val transfer: theory -> Proof.context -> Proof.context val background_theory: (theory -> theory) -> Proof.context -> Proof.context val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context - val extern_fact: Proof.context -> string -> xstring val pretty_term_abbrev: Proof.context -> term -> Pretty.T - val markup_fact: Proof.context -> string -> Markup.T val pretty_fact: Proof.context -> string * thm list -> Pretty.T val check_class: Proof.context -> xstring * Position.T -> class * Position.report list val read_class: Proof.context -> string -> class @@ -120,6 +118,7 @@ (term list list * (Proof.context -> Proof.context)) * Proof.context val fact_tac: Proof.context -> thm list -> int -> tactic val some_fact_tac: Proof.context -> int -> tactic + val get_fact_generic: Context.generic -> Facts.ref -> thm list val get_fact: Proof.context -> Facts.ref -> thm list val get_fact_single: Proof.context -> Facts.ref -> thm val get_thms: Proof.context -> xstring -> thm list @@ -209,7 +208,7 @@ syntax: Local_Syntax.T, (*local syntax*) tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*) consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*) - facts: Facts.T, (*local facts*) + facts: Facts.T, (*cumulative facts*) cases: cases}; (*named case contexts: case, is_proper, running index*) fun make_data (mode, syntax, tsig, consts, facts, cases) = @@ -223,7 +222,7 @@ Local_Syntax.init thy, (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy), (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy), - Facts.empty, + Global_Theory.facts_of thy, empty_cases); ); @@ -340,28 +339,10 @@ (** pretty printing **) -(* extern *) - -fun which_facts ctxt name = - let - val local_facts = facts_of ctxt; - val global_facts = Global_Theory.facts_of (theory_of ctxt); - in - if is_some (Facts.lookup (Context.Proof ctxt) local_facts name) - then local_facts else global_facts - end; - -fun markup_fact ctxt name = Name_Space.markup (Facts.space_of (which_facts ctxt name)) name; - -fun extern_fact ctxt name = Facts.extern ctxt (which_facts ctxt name) name; - - -(* pretty *) - fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt); fun pretty_fact_name ctxt a = - Pretty.block [Pretty.mark_str (markup_fact ctxt a, extern_fact ctxt a), Pretty.str ":"]; + Pretty.block [Pretty.mark_str (Facts.markup_extern ctxt (facts_of ctxt) a), Pretty.str ":"]; fun pretty_fact ctxt = let @@ -911,12 +892,13 @@ end; -(* get_thm(s) *) +(* get facts *) local -fun retrieve_thms pick ctxt (Facts.Fact s) = +fun retrieve_thms pick context (Facts.Fact s) = let + val ctxt = Context.the_proof context; val pos = Syntax.read_token_pos s; val prop = Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s @@ -927,34 +909,28 @@ fun prove_fact th = Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th]))); val results = map_filter (try prove_fact) (potential_facts ctxt prop'); - val res = + val thm = (case distinct Thm.eq_thm_prop results of - [res] => res + [thm] => thm | [] => err "Failed to retrieve literal fact" | _ => err "Ambiguous specification of literal fact"); - in pick ("", Position.none) [res] end - | retrieve_thms pick ctxt xthmref = + in pick ("", Position.none) [thm] end + | retrieve_thms pick context (Facts.Named ((xname, pos), ivs)) = let - val thy = theory_of ctxt; - val local_facts = facts_of ctxt; - val thmref = Facts.map_name_of_ref (Facts.intern local_facts) xthmref; - val name = Facts.name_of_ref thmref; - val pos = Facts.pos_of_ref xthmref; - val thms = - if name = "" then [Thm.transfer thy Drule.dummy_thm] - else - (case Facts.lookup (Context.Proof ctxt) local_facts name of - SOME (_, ths) => - (Context_Position.report ctxt pos - (Name_Space.markup (Facts.space_of local_facts) name); - map (Thm.transfer thy) (Facts.select thmref ths)) - | NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref); - in pick (name, pos) thms end; + val thy = Context.theory_of context; + val facts = Context.cases Global_Theory.facts_of facts_of context; + val (name, thms) = + (case xname of + "" => (xname, [Thm.transfer thy Drule.dummy_thm]) + | "_" => (xname, [Thm.transfer thy Drule.asm_rl]) + | _ => Facts.retrieve context facts (xname, pos)); + in pick (name, pos) (Facts.select (Facts.Named ((name, pos), ivs)) thms) end; in -val get_fact = retrieve_thms (K I); -val get_fact_single = retrieve_thms Facts.the_single; +val get_fact_generic = retrieve_thms (K I); +val get_fact = retrieve_thms (K I) o Context.Proof; +val get_fact_single = retrieve_thms Facts.the_single o Context.Proof; fun get_thms ctxt = get_fact ctxt o Facts.named; fun get_thm ctxt = get_fact_single ctxt o Facts.named; diff -r b7add947a6ef -r ed92ce2ac88e src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Thu Mar 13 17:26:22 2014 +0100 +++ b/src/Pure/Tools/find_theorems.ML Fri Mar 14 10:08:36 2014 +0100 @@ -381,14 +381,11 @@ fun all_facts_of ctxt = let - fun visible_facts facts = + val facts = Proof_Context.facts_of ctxt + val visible_facts = Facts.dest_static [] facts |> filter_out (Facts.is_concealed facts o #1); - in - maps Facts.selections - (visible_facts (Proof_Context.facts_of ctxt) @ - visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt))) - end; + in maps Facts.selections visible_facts end; fun filter_theorems ctxt theorems query = let @@ -453,9 +450,10 @@ (case thmref of Facts.Named ((name, _), sel) => (name, sel) | Facts.Fact _ => raise Fail "Illegal literal fact"); + val (markup, _) = Facts.markup_extern ctxt (Proof_Context.facts_of ctxt) name; in - [Pretty.mark (Proof_Context.markup_fact ctxt name) (Pretty.str name), - Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1] + [Pretty.mark_str (markup, name), Pretty.str (Facts.string_of_selection sel), + Pretty.str ":", Pretty.brk 1] end; in diff -r b7add947a6ef -r ed92ce2ac88e src/Pure/facts.ML --- a/src/Pure/facts.ML Thu Mar 13 17:26:22 2014 +0100 +++ b/src/Pure/facts.ML Fri Mar 14 10:08:36 2014 +0100 @@ -26,7 +26,9 @@ val check: Context.generic -> T -> xstring * Position.T -> string val intern: T -> xstring -> string val extern: Proof.context -> T -> string -> xstring + val markup_extern: Proof.context -> T -> string -> Markup.T * xstring val lookup: Context.generic -> T -> string -> (bool * thm list) option + val retrieve: Context.generic -> T -> xstring * Position.T -> string * thm list val defined: T -> string -> bool val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a val dest_static: T list -> T -> (string * thm list) list @@ -155,6 +157,7 @@ val intern = Name_Space.intern o space_of; fun extern ctxt = Name_Space.extern ctxt o space_of; +fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of val defined = is_some oo (Name_Space.lookup_key o facts_of); @@ -164,6 +167,18 @@ | SOME (_, Static ths) => SOME (true, ths) | SOME (_, Dynamic f) => SOME (false, f context)); +fun retrieve context facts (xname, pos) = + let + val name = check context facts (xname, pos); + val thms = + (case lookup context facts name of + SOME (static, thms) => + (if static then () + else Context_Position.report_generic context pos (Markup.dynamic_fact name); + thms) + | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos)); + in (name, map (Thm.transfer (Context.theory_of context)) thms) end; + fun fold_static f = Name_Space.fold_table (fn (name, Static ths) => f (name, ths) | _ => I) o facts_of; diff -r b7add947a6ef -r ed92ce2ac88e src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Thu Mar 13 17:26:22 2014 +0100 +++ b/src/Pure/global_theory.ML Fri Mar 14 10:08:36 2014 +0100 @@ -11,7 +11,6 @@ val intern_fact: theory -> xstring -> string val defined_fact: theory -> string -> bool val hide_fact: bool -> string -> theory -> theory - val get_fact: Context.generic -> theory -> Facts.ref -> thm list val get_thms: theory -> xstring -> thm list val get_thm: theory -> xstring -> thm val all_thms_of: theory -> (string * thm) list @@ -64,31 +63,13 @@ fun hide_fact fully name = Data.map (Facts.hide fully name); -(** retrieve theorems **) - -fun get_fact context thy xthmref = - let - val facts = facts_of thy; - val xname = Facts.name_of_ref xthmref; - val pos = Facts.pos_of_ref xthmref; +(* retrieve theorems *) - val name = - (case intern_fact thy xname of - "_" => "Pure.asm_rl" - | name => name); - val res = Facts.lookup context facts name; - in - (case res of - NONE => error ("Unknown fact " ^ quote name ^ Position.here pos) - | SOME (static, ths) => - (Context_Position.report_generic context pos (Name_Space.markup (Facts.space_of facts) name); - if static then () - else Context_Position.report_generic context pos (Markup.dynamic_fact name); - Facts.select xthmref (map (Thm.transfer thy) ths))) - end; +fun get_thms thy xname = + #2 (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none)); -fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named; -fun get_thm thy name = Facts.the_single (name, Position.none) (get_thms thy name); +fun get_thm thy xname = + Facts.the_single (xname, Position.none) (get_thms thy xname); fun all_thms_of thy = Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];