--- 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
--- 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
--- 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 *)
--- 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));
--- 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;
--- 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