just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
authorwenzelm
Fri Mar 14 10:08:36 2014 +0100 (2014-03-14)
changeset 56140ed92ce2ac88e
parent 56139 b7add947a6ef
child 56141 c06202417c4a
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
more thorough background_notes: distribute global notes to all contexts;
src/HOL/Lattices_Big.thy
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof_context.ML
src/Pure/Tools/find_theorems.ML
src/Pure/facts.ML
src/Pure/global_theory.ML
     1.1 --- a/src/HOL/Lattices_Big.thy	Thu Mar 13 17:26:22 2014 +0100
     1.2 +++ b/src/HOL/Lattices_Big.thy	Fri Mar 14 10:08:36 2014 +0100
     1.3 @@ -640,6 +640,11 @@
     1.4    shows "Max M \<le> Max N"
     1.5    using assms by (fact Max.antimono)
     1.6  
     1.7 +end
     1.8 +
     1.9 +context linorder  (* FIXME *)
    1.10 +begin
    1.11 +
    1.12  lemma mono_Min_commute:
    1.13    assumes "mono f"
    1.14    assumes "finite A" and "A \<noteq> {}"
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Mar 13 17:26:22 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Mar 14 10:08:36 2014 +0100
     2.3 @@ -459,7 +459,7 @@
     2.4        else
     2.5          is_too_complex
     2.6      val local_facts = Proof_Context.facts_of ctxt
     2.7 -    val named_locals = local_facts |> Facts.dest_static []
     2.8 +    val named_locals = local_facts |> Facts.dest_static [global_facts]
     2.9      val assms = Assumption.all_assms_of ctxt
    2.10      fun is_good_unnamed_local th =
    2.11        not (Thm.has_name_hint th) andalso
    2.12 @@ -467,14 +467,12 @@
    2.13      val unnamed_locals =
    2.14        union Thm.eq_thm_prop (Facts.props local_facts) chained
    2.15        |> filter is_good_unnamed_local |> map (pair "" o single)
    2.16 -    val full_space =
    2.17 -      Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
    2.18      val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp
    2.19 -    fun add_facts global foldx facts =
    2.20 +    fun add_facts global foldx =
    2.21        foldx (fn (name0, ths) => fn accum =>
    2.22          if name0 <> "" andalso
    2.23             forall (not o member Thm.eq_thm_prop add_ths) ths andalso
    2.24 -           (Facts.is_concealed facts name0 orelse
    2.25 +           (Facts.is_concealed local_facts name0 orelse
    2.26              (not generous andalso is_blacklisted_or_something name0)) then
    2.27            accum
    2.28          else
    2.29 @@ -499,8 +497,7 @@
    2.30                             if name0 = "" then
    2.31                               backquote_thm ctxt th
    2.32                             else
    2.33 -                             [Facts.extern ctxt facts name0,
    2.34 -                              Name_Space.extern ctxt full_space name0]
    2.35 +                             [Facts.extern ctxt local_facts name0]
    2.36                               |> find_first check_thms
    2.37                               |> the_default name0
    2.38                               |> make_name reserved multi j),
    2.39 @@ -515,8 +512,8 @@
    2.40      (* The single-theorem names go before the multiple-theorem ones (e.g.,
    2.41         "xxx" vs. "xxx(3)"), so that single names are preferred when both are
    2.42         available. *)
    2.43 -    `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
    2.44 -          |> add_facts true Facts.fold_static global_facts global_facts
    2.45 +    `I [] |> add_facts false fold (unnamed_locals @ named_locals)
    2.46 +          |> add_facts true Facts.fold_static global_facts
    2.47            |> op @
    2.48    end
    2.49  
     3.1 --- a/src/Pure/Isar/attrib.ML	Thu Mar 13 17:26:22 2014 +0100
     3.2 +++ b/src/Pure/Isar/attrib.ML	Fri Mar 14 10:08:36 2014 +0100
     3.3 @@ -213,7 +213,7 @@
     3.4  
     3.5  fun gen_thm pick = Scan.depend (fn context =>
     3.6    let
     3.7 -    val get = Context.cases (Global_Theory.get_fact context) Proof_Context.get_fact context;
     3.8 +    val get = Proof_Context.get_fact_generic context;
     3.9      val get_fact = get o Facts.Fact;
    3.10      fun get_named pos name = get (Facts.Named ((name, pos), NONE));
    3.11    in
    3.12 @@ -249,6 +249,8 @@
    3.13  
    3.14  (** partial evaluation -- observing rule/declaration/mixed attributes **)
    3.15  
    3.16 +(*NB: result length may change due to rearrangement of symbolic expression*)
    3.17 +
    3.18  local
    3.19  
    3.20  fun apply_att src (context, th) =
     4.1 --- a/src/Pure/Isar/generic_target.ML	Thu Mar 13 17:26:22 2014 +0100
     4.2 +++ b/src/Pure/Isar/generic_target.ML	Fri Mar 14 10:08:36 2014 +0100
     4.3 @@ -179,8 +179,7 @@
     4.4    end;
     4.5  
     4.6  fun locale_notes locale kind global_facts local_facts =
     4.7 -  Local_Theory.background_theory
     4.8 -    (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
     4.9 +  Local_Theory.background_notes kind (Attrib.map_facts (K []) global_facts) #>
    4.10    (fn lthy => lthy |>
    4.11      Local_Theory.target (fn ctxt => ctxt |>
    4.12        Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #>
    4.13 @@ -311,7 +310,7 @@
    4.14      |> pair (lhs, def));
    4.15  
    4.16  fun theory_notes kind global_facts local_facts =
    4.17 -  Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>
    4.18 +  Local_Theory.background_notes kind global_facts #>
    4.19    (fn lthy => lthy |> Local_Theory.map_contexts (fn level => fn ctxt =>
    4.20      if level = Local_Theory.level lthy then ctxt
    4.21      else
     5.1 --- a/src/Pure/Isar/local_theory.ML	Thu Mar 13 17:26:22 2014 +0100
     5.2 +++ b/src/Pure/Isar/local_theory.ML	Fri Mar 14 10:08:36 2014 +0100
     5.3 @@ -32,6 +32,8 @@
     5.4    val raw_theory: (theory -> theory) -> local_theory -> local_theory
     5.5    val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
     5.6    val background_theory: (theory -> theory) -> local_theory -> local_theory
     5.7 +  val background_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
     5.8 +    local_theory -> local_theory
     5.9    val target_of: local_theory -> Proof.context
    5.10    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
    5.11    val target_morphism: local_theory -> morphism
    5.12 @@ -215,6 +217,19 @@
    5.13  
    5.14  fun background_theory f = #2 o background_theory_result (f #> pair ());
    5.15  
    5.16 +fun background_notes kind facts lthy =
    5.17 +  let
    5.18 +    val facts1 = Attrib.partial_evaluation lthy facts;
    5.19 +    val facts0 = Attrib.map_facts (K []) facts1;
    5.20 +  in
    5.21 +    lthy
    5.22 +    |> background_theory (Attrib.global_notes kind facts1 #> snd)
    5.23 +    |> map_contexts (fn _ => fn ctxt => ctxt
    5.24 +      |> Proof_Context.map_naming (K (naming_of lthy))
    5.25 +      |> Attrib.local_notes kind facts0 |> snd
    5.26 +      |> Proof_Context.restore_naming ctxt)
    5.27 +  end;
    5.28 +
    5.29  
    5.30  (* target contexts *)
    5.31  
     6.1 --- a/src/Pure/Isar/locale.ML	Thu Mar 13 17:26:22 2014 +0100
     6.2 +++ b/src/Pure/Isar/locale.ML	Fri Mar 14 10:08:36 2014 +0100
     6.3 @@ -561,7 +561,7 @@
     6.4            (* Registrations *)
     6.5            (fn thy =>
     6.6              fold_rev (fn (_, morph) =>
     6.7 -              snd o Attrib.global_notes kind (Element.transform_facts morph facts))
     6.8 +              snd o Attrib.global_notes kind (Element.transform_facts morph facts))  (* FIXME background_notes *)
     6.9              (registrations_of (Context.Theory thy) loc) thy));
    6.10  
    6.11  
     7.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 13 17:26:22 2014 +0100
     7.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Mar 14 10:08:36 2014 +0100
     7.3 @@ -53,9 +53,7 @@
     7.4    val transfer: theory -> Proof.context -> Proof.context
     7.5    val background_theory: (theory -> theory) -> Proof.context -> Proof.context
     7.6    val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
     7.7 -  val extern_fact: Proof.context -> string -> xstring
     7.8    val pretty_term_abbrev: Proof.context -> term -> Pretty.T
     7.9 -  val markup_fact: Proof.context -> string -> Markup.T
    7.10    val pretty_fact: Proof.context -> string * thm list -> Pretty.T
    7.11    val check_class: Proof.context -> xstring * Position.T -> class * Position.report list
    7.12    val read_class: Proof.context -> string -> class
    7.13 @@ -120,6 +118,7 @@
    7.14      (term list list * (Proof.context -> Proof.context)) * Proof.context
    7.15    val fact_tac: Proof.context -> thm list -> int -> tactic
    7.16    val some_fact_tac: Proof.context -> int -> tactic
    7.17 +  val get_fact_generic: Context.generic -> Facts.ref -> thm list
    7.18    val get_fact: Proof.context -> Facts.ref -> thm list
    7.19    val get_fact_single: Proof.context -> Facts.ref -> thm
    7.20    val get_thms: Proof.context -> xstring -> thm list
    7.21 @@ -209,7 +208,7 @@
    7.22      syntax: Local_Syntax.T,      (*local syntax*)
    7.23      tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
    7.24      consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
    7.25 -    facts: Facts.T,              (*local facts*)
    7.26 +    facts: Facts.T,              (*cumulative facts*)
    7.27      cases: cases};               (*named case contexts: case, is_proper, running index*)
    7.28  
    7.29  fun make_data (mode, syntax, tsig, consts, facts, cases) =
    7.30 @@ -223,7 +222,7 @@
    7.31        Local_Syntax.init thy,
    7.32        (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy),
    7.33        (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy),
    7.34 -      Facts.empty,
    7.35 +      Global_Theory.facts_of thy,
    7.36        empty_cases);
    7.37  );
    7.38  
    7.39 @@ -340,28 +339,10 @@
    7.40  
    7.41  (** pretty printing **)
    7.42  
    7.43 -(* extern *)
    7.44 -
    7.45 -fun which_facts ctxt name =
    7.46 -  let
    7.47 -    val local_facts = facts_of ctxt;
    7.48 -    val global_facts = Global_Theory.facts_of (theory_of ctxt);
    7.49 -  in
    7.50 -    if is_some (Facts.lookup (Context.Proof ctxt) local_facts name)
    7.51 -    then local_facts else global_facts
    7.52 -  end;
    7.53 -
    7.54 -fun markup_fact ctxt name = Name_Space.markup (Facts.space_of (which_facts ctxt name)) name;
    7.55 -
    7.56 -fun extern_fact ctxt name = Facts.extern ctxt (which_facts ctxt name) name;
    7.57 -
    7.58 -
    7.59 -(* pretty *)
    7.60 -
    7.61  fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
    7.62  
    7.63  fun pretty_fact_name ctxt a =
    7.64 -  Pretty.block [Pretty.mark_str (markup_fact ctxt a, extern_fact ctxt a), Pretty.str ":"];
    7.65 +  Pretty.block [Pretty.mark_str (Facts.markup_extern ctxt (facts_of ctxt) a), Pretty.str ":"];
    7.66  
    7.67  fun pretty_fact ctxt =
    7.68    let
    7.69 @@ -911,12 +892,13 @@
    7.70  end;
    7.71  
    7.72  
    7.73 -(* get_thm(s) *)
    7.74 +(* get facts *)
    7.75  
    7.76  local
    7.77  
    7.78 -fun retrieve_thms pick ctxt (Facts.Fact s) =
    7.79 +fun retrieve_thms pick context (Facts.Fact s) =
    7.80        let
    7.81 +        val ctxt = Context.the_proof context;
    7.82          val pos = Syntax.read_token_pos s;
    7.83          val prop =
    7.84            Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
    7.85 @@ -927,34 +909,28 @@
    7.86          fun prove_fact th =
    7.87            Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
    7.88          val results = map_filter (try prove_fact) (potential_facts ctxt prop');
    7.89 -        val res =
    7.90 +        val thm =
    7.91            (case distinct Thm.eq_thm_prop results of
    7.92 -            [res] => res
    7.93 +            [thm] => thm
    7.94            | [] => err "Failed to retrieve literal fact"
    7.95            | _ => err "Ambiguous specification of literal fact");
    7.96 -      in pick ("", Position.none) [res] end
    7.97 -  | retrieve_thms pick ctxt xthmref =
    7.98 +      in pick ("", Position.none) [thm] end
    7.99 +  | retrieve_thms pick context (Facts.Named ((xname, pos), ivs)) =
   7.100        let
   7.101 -        val thy = theory_of ctxt;
   7.102 -        val local_facts = facts_of ctxt;
   7.103 -        val thmref = Facts.map_name_of_ref (Facts.intern local_facts) xthmref;
   7.104 -        val name = Facts.name_of_ref thmref;
   7.105 -        val pos = Facts.pos_of_ref xthmref;
   7.106 -        val thms =
   7.107 -          if name = "" then [Thm.transfer thy Drule.dummy_thm]
   7.108 -          else
   7.109 -            (case Facts.lookup (Context.Proof ctxt) local_facts name of
   7.110 -              SOME (_, ths) =>
   7.111 -                (Context_Position.report ctxt pos
   7.112 -                  (Name_Space.markup (Facts.space_of local_facts) name);
   7.113 -                 map (Thm.transfer thy) (Facts.select thmref ths))
   7.114 -            | NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref);
   7.115 -      in pick (name, pos) thms end;
   7.116 +        val thy = Context.theory_of context;
   7.117 +        val facts = Context.cases Global_Theory.facts_of facts_of context;
   7.118 +        val (name, thms) =
   7.119 +          (case xname of
   7.120 +            "" => (xname, [Thm.transfer thy Drule.dummy_thm])
   7.121 +          | "_" => (xname, [Thm.transfer thy Drule.asm_rl])
   7.122 +          | _ => Facts.retrieve context facts (xname, pos));
   7.123 +      in pick (name, pos) (Facts.select (Facts.Named ((name, pos), ivs)) thms) end;
   7.124  
   7.125  in
   7.126  
   7.127 -val get_fact = retrieve_thms (K I);
   7.128 -val get_fact_single = retrieve_thms Facts.the_single;
   7.129 +val get_fact_generic = retrieve_thms (K I);
   7.130 +val get_fact = retrieve_thms (K I) o Context.Proof;
   7.131 +val get_fact_single = retrieve_thms Facts.the_single o Context.Proof;
   7.132  
   7.133  fun get_thms ctxt = get_fact ctxt o Facts.named;
   7.134  fun get_thm ctxt = get_fact_single ctxt o Facts.named;
     8.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Mar 13 17:26:22 2014 +0100
     8.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Mar 14 10:08:36 2014 +0100
     8.3 @@ -381,14 +381,11 @@
     8.4  
     8.5  fun all_facts_of ctxt =
     8.6    let
     8.7 -    fun visible_facts facts =
     8.8 +    val facts = Proof_Context.facts_of ctxt
     8.9 +    val visible_facts =
    8.10        Facts.dest_static [] facts
    8.11        |> filter_out (Facts.is_concealed facts o #1);
    8.12 -  in
    8.13 -    maps Facts.selections
    8.14 -     (visible_facts (Proof_Context.facts_of ctxt) @
    8.15 -      visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt)))
    8.16 -  end;
    8.17 +  in maps Facts.selections visible_facts end;
    8.18  
    8.19  fun filter_theorems ctxt theorems query =
    8.20    let
    8.21 @@ -453,9 +450,10 @@
    8.22        (case thmref of
    8.23          Facts.Named ((name, _), sel) => (name, sel)
    8.24        | Facts.Fact _ => raise Fail "Illegal literal fact");
    8.25 +    val (markup, _) = Facts.markup_extern ctxt (Proof_Context.facts_of ctxt) name;
    8.26    in
    8.27 -    [Pretty.mark (Proof_Context.markup_fact ctxt name) (Pretty.str name),
    8.28 -      Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
    8.29 +    [Pretty.mark_str (markup, name), Pretty.str (Facts.string_of_selection sel),
    8.30 +      Pretty.str ":", Pretty.brk 1]
    8.31    end;
    8.32  
    8.33  in
     9.1 --- a/src/Pure/facts.ML	Thu Mar 13 17:26:22 2014 +0100
     9.2 +++ b/src/Pure/facts.ML	Fri Mar 14 10:08:36 2014 +0100
     9.3 @@ -26,7 +26,9 @@
     9.4    val check: Context.generic -> T -> xstring * Position.T -> string
     9.5    val intern: T -> xstring -> string
     9.6    val extern: Proof.context -> T -> string -> xstring
     9.7 +  val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
     9.8    val lookup: Context.generic -> T -> string -> (bool * thm list) option
     9.9 +  val retrieve: Context.generic -> T -> xstring * Position.T -> string * thm list
    9.10    val defined: T -> string -> bool
    9.11    val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
    9.12    val dest_static: T list -> T -> (string * thm list) list
    9.13 @@ -155,6 +157,7 @@
    9.14  
    9.15  val intern = Name_Space.intern o space_of;
    9.16  fun extern ctxt = Name_Space.extern ctxt o space_of;
    9.17 +fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of
    9.18  
    9.19  val defined = is_some oo (Name_Space.lookup_key o facts_of);
    9.20  
    9.21 @@ -164,6 +167,18 @@
    9.22    | SOME (_, Static ths) => SOME (true, ths)
    9.23    | SOME (_, Dynamic f) => SOME (false, f context));
    9.24  
    9.25 +fun retrieve context facts (xname, pos) =
    9.26 +  let
    9.27 +    val name = check context facts (xname, pos);
    9.28 +    val thms =
    9.29 +      (case lookup context facts name of
    9.30 +        SOME (static, thms) =>
    9.31 +          (if static then ()
    9.32 +           else Context_Position.report_generic context pos (Markup.dynamic_fact name);
    9.33 +           thms)
    9.34 +      | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
    9.35 +  in (name, map (Thm.transfer (Context.theory_of context)) thms) end;
    9.36 +
    9.37  fun fold_static f =
    9.38    Name_Space.fold_table (fn (name, Static ths) => f (name, ths) | _ => I) o facts_of;
    9.39  
    10.1 --- a/src/Pure/global_theory.ML	Thu Mar 13 17:26:22 2014 +0100
    10.2 +++ b/src/Pure/global_theory.ML	Fri Mar 14 10:08:36 2014 +0100
    10.3 @@ -11,7 +11,6 @@
    10.4    val intern_fact: theory -> xstring -> string
    10.5    val defined_fact: theory -> string -> bool
    10.6    val hide_fact: bool -> string -> theory -> theory
    10.7 -  val get_fact: Context.generic -> theory -> Facts.ref -> thm list
    10.8    val get_thms: theory -> xstring -> thm list
    10.9    val get_thm: theory -> xstring -> thm
   10.10    val all_thms_of: theory -> (string * thm) list
   10.11 @@ -64,31 +63,13 @@
   10.12  fun hide_fact fully name = Data.map (Facts.hide fully name);
   10.13  
   10.14  
   10.15 -(** retrieve theorems **)
   10.16 -
   10.17 -fun get_fact context thy xthmref =
   10.18 -  let
   10.19 -    val facts = facts_of thy;
   10.20 -    val xname = Facts.name_of_ref xthmref;
   10.21 -    val pos = Facts.pos_of_ref xthmref;
   10.22 +(* retrieve theorems *)
   10.23  
   10.24 -    val name =
   10.25 -      (case intern_fact thy xname of
   10.26 -        "_" => "Pure.asm_rl"
   10.27 -      | name => name);
   10.28 -    val res = Facts.lookup context facts name;
   10.29 -  in
   10.30 -    (case res of
   10.31 -      NONE => error ("Unknown fact " ^ quote name ^ Position.here pos)
   10.32 -    | SOME (static, ths) =>
   10.33 -        (Context_Position.report_generic context pos (Name_Space.markup (Facts.space_of facts) name);
   10.34 -         if static then ()
   10.35 -         else Context_Position.report_generic context pos (Markup.dynamic_fact name);
   10.36 -         Facts.select xthmref (map (Thm.transfer thy) ths)))
   10.37 -  end;
   10.38 +fun get_thms thy xname =
   10.39 +  #2 (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none));
   10.40  
   10.41 -fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named;
   10.42 -fun get_thm thy name = Facts.the_single (name, Position.none) (get_thms thy name);
   10.43 +fun get_thm thy xname =
   10.44 +  Facts.the_single (xname, Position.none) (get_thms thy xname);
   10.45  
   10.46  fun all_thms_of thy =
   10.47    Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];