# HG changeset patch
# User wenzelm
# Date 1394796239 -3600
# Node ID c06202417c4a207f36609b0a22c66a1ce38f32f7
# Parent  ed92ce2ac88e492e4fe1c17e4942b0e3f92a241b
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;

diff -r ed92ce2ac88e -r c06202417c4a src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Mar 14 10:08:36 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Mar 14 12:23:59 2014 +0100
@@ -467,12 +467,14 @@
     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 =
+    fun add_facts global foldx facts =
       foldx (fn (name0, ths) => fn accum =>
         if name0 <> "" andalso
            forall (not o member Thm.eq_thm_prop add_ths) ths andalso
-           (Facts.is_concealed local_facts name0 orelse
+           (Facts.is_concealed facts name0 orelse
             (not generous andalso is_blacklisted_or_something name0)) then
           accum
         else
@@ -497,7 +499,8 @@
                            if name0 = "" then
                              backquote_thm ctxt th
                            else
-                             [Facts.extern ctxt local_facts name0]
+                             [Facts.extern ctxt facts name0,
+                              Name_Space.extern ctxt full_space name0]
                              |> find_first check_thms
                              |> the_default name0
                              |> make_name reserved multi j),
@@ -512,8 +515,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 (unnamed_locals @ named_locals)
-          |> add_facts true Facts.fold_static global_facts
+    `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
+          |> add_facts true Facts.fold_static global_facts global_facts
           |> op @
   end
 
diff -r ed92ce2ac88e -r c06202417c4a src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Fri Mar 14 10:08:36 2014 +0100
+++ b/src/Pure/Isar/generic_target.ML	Fri Mar 14 12:23:59 2014 +0100
@@ -179,7 +179,8 @@
   end;
 
 fun locale_notes locale kind global_facts local_facts =
-  Local_Theory.background_notes kind (Attrib.map_facts (K []) global_facts) #>
+  Local_Theory.background_theory
+    (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
   (fn lthy => lthy |>
     Local_Theory.target (fn ctxt => ctxt |>
       Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #>
@@ -310,7 +311,7 @@
     |> pair (lhs, def));
 
 fun theory_notes kind global_facts local_facts =
-  Local_Theory.background_notes kind global_facts #>
+  Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>
   (fn lthy => lthy |> Local_Theory.map_contexts (fn level => fn ctxt =>
     if level = Local_Theory.level lthy then ctxt
     else
diff -r ed92ce2ac88e -r c06202417c4a src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Fri Mar 14 10:08:36 2014 +0100
+++ b/src/Pure/Isar/local_theory.ML	Fri Mar 14 12:23:59 2014 +0100
@@ -32,8 +32,6 @@
   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
@@ -217,19 +215,6 @@
 
 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 ed92ce2ac88e -r c06202417c4a src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Mar 14 10:08:36 2014 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Mar 14 12:23:59 2014 +0100
@@ -561,7 +561,7 @@
           (* Registrations *)
           (fn thy =>
             fold_rev (fn (_, morph) =>
-              snd o Attrib.global_notes kind (Element.transform_facts morph facts))  (* FIXME background_notes *)
+              snd o Attrib.global_notes kind (Element.transform_facts morph facts))
             (registrations_of (Context.Theory thy) loc) thy));
 
 
diff -r ed92ce2ac88e -r c06202417c4a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Mar 14 10:08:36 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Mar 14 12:23:59 2014 +0100
@@ -30,7 +30,6 @@
   val consts_of: Proof.context -> Consts.T
   val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
-  val facts_of: Proof.context -> Facts.T
   val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
   val naming_of: Proof.context -> Name_Space.naming
   val restore_naming: Proof.context -> Proof.context -> Proof.context
@@ -53,6 +52,9 @@
   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 facts_of: Proof.context -> Facts.T
+  val facts_of_fact: Proof.context -> string -> Facts.T
+  val markup_extern_fact: Proof.context -> string -> Markup.T * xstring
   val pretty_term_abbrev: Proof.context -> term -> Pretty.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
   val check_class: Proof.context -> xstring * Position.T -> class * Position.report list
@@ -208,7 +210,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,              (*cumulative facts*)
+    facts: Facts.T,              (*local facts, based on initial global facts*)
     cases: cases};               (*named case contexts: case, is_proper, running index*)
 
 fun make_data (mode, syntax, tsig, consts, facts, cases) =
@@ -276,7 +278,6 @@
 fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
 
 val consts_of = #1 o #consts o rep_data;
-val facts_of = #facts o rep_data;
 val cases_of = #cases o rep_data;
 
 
@@ -336,13 +337,30 @@
   in (res, ctxt |> transfer thy') end;
 
 
+(* hybrid facts *)
+
+val facts_of = #facts o rep_data;
+
+fun facts_of_fact 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_extern_fact ctxt name =
+  Facts.markup_extern ctxt (facts_of_fact ctxt name) name;
+
+
 
 (** pretty printing **)
 
 fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
 
 fun pretty_fact_name ctxt a =
-  Pretty.block [Pretty.mark_str (Facts.markup_extern ctxt (facts_of ctxt) a), Pretty.str ":"];
+  Pretty.block [Pretty.mark_str (markup_extern_fact ctxt a), Pretty.str ":"];
 
 fun pretty_fact ctxt =
   let
@@ -896,7 +914,16 @@
 
 local
 
-fun retrieve_thms pick context (Facts.Fact s) =
+fun retrieve_global context =
+  Facts.retrieve context (Global_Theory.facts_of (Context.theory_of context));
+
+fun retrieve_generic (context as Context.Proof ctxt) (xname, pos) =
+      if can (fn () => Facts.retrieve context (facts_of ctxt) (xname, Position.none)) ()
+      then Facts.retrieve context (facts_of ctxt) (xname, pos)
+      else retrieve_global context (xname, pos)
+  | retrieve_generic context arg = retrieve_global context arg;
+
+fun retrieve pick context (Facts.Fact s) =
       let
         val ctxt = Context.the_proof context;
         val pos = Syntax.read_token_pos s;
@@ -915,22 +942,21 @@
           | [] => err "Failed to retrieve literal fact"
           | _ => err "Ambiguous specification of literal fact");
       in pick ("", Position.none) [thm] end
-  | retrieve_thms pick context (Facts.Named ((xname, pos), ivs)) =
+  | retrieve pick context (Facts.Named ((xname, pos), ivs)) =
       let
         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));
+          | _ => retrieve_generic context (xname, pos));
       in pick (name, pos) (Facts.select (Facts.Named ((name, pos), ivs)) thms) end;
 
 in
 
-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;
+val get_fact_generic = retrieve (K I);
+val get_fact = retrieve (K I) o Context.Proof;
+val get_fact_single = retrieve 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 ed92ce2ac88e -r c06202417c4a src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Mar 14 10:08:36 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Fri Mar 14 12:23:59 2014 +0100
@@ -381,11 +381,14 @@
 
 fun all_facts_of ctxt =
   let
-    val facts = Proof_Context.facts_of ctxt
-    val visible_facts =
+    fun visible_facts facts =
       Facts.dest_static [] facts
       |> filter_out (Facts.is_concealed facts o #1);
-  in maps Facts.selections visible_facts end;
+  in
+    maps Facts.selections
+     (visible_facts (Proof_Context.facts_of ctxt) @
+      visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt)))
+  end;
 
 fun filter_theorems ctxt theorems query =
   let
@@ -450,10 +453,9 @@
       (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_str (markup, name), Pretty.str (Facts.string_of_selection sel),
-      Pretty.str ":", Pretty.brk 1]
+    [Pretty.mark (#1 (Proof_Context.markup_extern_fact ctxt name)) (Pretty.str name),
+      Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
   end;
 
 in