added Attrib.global_notes/local_notes/generic_notes convenience;
authorwenzelm
Sun Apr 01 19:07:32 2012 +0200 (2012-04-01)
changeset 47249c0481c3c2a6c
parent 47248 afacccb4e2c7
child 47250 6523a21076a8
added Attrib.global_notes/local_notes/generic_notes convenience;
src/Pure/Isar/attrib.ML
src/Pure/Isar/bundle.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/locale.ML
src/Tools/interpretation_with_defs.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Sun Apr 01 19:04:52 2012 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sun Apr 01 19:07:32 2012 +0200
     1.3 @@ -25,6 +25,12 @@
     1.4    val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
     1.5      (('c * 'a list) * ('b * 'a list) list) list ->
     1.6      (('c * 'att list) * ('fact * 'att list) list) list
     1.7 +  val global_notes: string -> (binding * (thm list * src list) list) list ->
     1.8 +    theory -> (string * thm list) list * theory
     1.9 +  val local_notes: string -> (binding * (thm list * src list) list) list ->
    1.10 +    Proof.context -> (string * thm list) list * Proof.context
    1.11 +  val generic_notes: string -> (binding * (thm list * src list) list) list ->
    1.12 +    Context.generic -> (string * thm list) list * Context.generic
    1.13    val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
    1.14    val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
    1.15    val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
    1.16 @@ -138,6 +144,15 @@
    1.17  
    1.18  (* fact expressions *)
    1.19  
    1.20 +fun global_notes kind facts thy = thy |>
    1.21 +  Global_Theory.note_thmss kind (map_facts (map (attribute_i thy)) facts);
    1.22 +
    1.23 +fun local_notes kind facts ctxt = ctxt |>
    1.24 +  Proof_Context.note_thmss kind (map_facts (map (attribute_i (Proof_Context.theory_of ctxt))) facts);
    1.25 +
    1.26 +fun generic_notes kind facts context = context |>
    1.27 +  Context.mapping_result (global_notes kind facts) (local_notes kind facts);
    1.28 +
    1.29  fun eval_thms ctxt srcs = ctxt
    1.30    |> Proof_Context.note_thmss ""
    1.31      (map_facts_refs (map (attribute (Proof_Context.theory_of ctxt))) (Proof_Context.get_fact ctxt)
     2.1 --- a/src/Pure/Isar/bundle.ML	Sun Apr 01 19:04:52 2012 +0200
     2.2 +++ b/src/Pure/Isar/bundle.ML	Sun Apr 01 19:07:32 2012 +0200
     2.3 @@ -87,11 +87,8 @@
     2.4  local
     2.5  
     2.6  fun gen_includes prep args ctxt =
     2.7 -  let
     2.8 -    val decls = maps (the_bundle ctxt o prep ctxt) args;
     2.9 -    val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
    2.10 -    val note = ((Binding.empty, []), map (apsnd (map attrib)) decls);
    2.11 -  in #2 (Proof_Context.note_thmss "" [note] ctxt) end;
    2.12 +  let val decls = maps (the_bundle ctxt o prep ctxt) args
    2.13 +  in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end;
    2.14  
    2.15  fun gen_context prep args (Context.Theory thy) =
    2.16        Named_Target.theory_init thy
     3.1 --- a/src/Pure/Isar/element.ML	Sun Apr 01 19:04:52 2012 +0200
     3.2 +++ b/src/Pure/Isar/element.ML	Sun Apr 01 19:07:32 2012 +0200
     3.3 @@ -51,8 +51,6 @@
     3.4    val satisfy_morphism: witness list -> morphism
     3.5    val eq_morphism: theory -> thm list -> morphism option
     3.6    val transfer_morphism: theory -> morphism
     3.7 -  val generic_note_thmss: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
     3.8 -    Context.generic -> (string * thm list) list * Context.generic
     3.9    val init: context_i -> Context.generic -> Context.generic
    3.10    val activate_i: context_i -> Proof.context -> context_i * Proof.context
    3.11    val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
    3.12 @@ -483,16 +481,6 @@
    3.13  
    3.14  (* init *)
    3.15  
    3.16 -fun generic_note_thmss kind facts context =
    3.17 -  let
    3.18 -    val facts' =
    3.19 -      Attrib.map_facts (map (Attrib.attribute_i (Context.theory_of context))) facts;
    3.20 -  in
    3.21 -    context |> Context.mapping_result
    3.22 -      (Global_Theory.note_thmss kind facts')
    3.23 -      (Proof_Context.note_thmss kind facts')
    3.24 -  end;
    3.25 -
    3.26  fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
    3.27    | init (Constrains _) = I
    3.28    | init (Assumes asms) = Context.map_proof (fn ctxt =>
    3.29 @@ -514,7 +502,7 @@
    3.30            |> fold Variable.auto_fixes (map #1 asms)
    3.31            |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
    3.32        in ctxt' end)
    3.33 -  | init (Notes (kind, facts)) = generic_note_thmss kind facts #> #2;
    3.34 +  | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
    3.35  
    3.36  
    3.37  (* activate *)
     4.1 --- a/src/Pure/Isar/expression.ML	Sun Apr 01 19:04:52 2012 +0200
     4.2 +++ b/src/Pure/Isar/expression.ML	Sun Apr 01 19:07:32 2012 +0200
     4.3 @@ -816,7 +816,7 @@
     4.4  local
     4.5  
     4.6  fun note_eqns_register deps witss attrss eqns export export' =
     4.7 -  Element.generic_note_thmss Thm.lemmaK
     4.8 +  Attrib.generic_notes Thm.lemmaK
     4.9      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
    4.10    #-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
    4.11    #-> (fn eqns => fold (fn ((dep, morph), wits) =>
    4.12 @@ -885,12 +885,10 @@
    4.13  
    4.14  fun note_eqns_dependency target deps witss attrss eqns export export' ctxt =
    4.15    let
    4.16 -    val thy = Proof_Context.theory_of ctxt;
    4.17 -
    4.18      val facts =
    4.19        (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
    4.20      val eqns' = ctxt
    4.21 -      |> Proof_Context.note_thmss Thm.lemmaK (Attrib.map_facts (map (Attrib.attribute_i thy)) facts)
    4.22 +      |> Attrib.local_notes Thm.lemmaK facts
    4.23        |-> (fn facts => `(fn ctxt => meta_rewrite ctxt (maps snd facts)))
    4.24        |> fst;  (* FIXME duplication to add_thmss *)
    4.25    in
     5.1 --- a/src/Pure/Isar/generic_target.ML	Sun Apr 01 19:04:52 2012 +0200
     5.2 +++ b/src/Pure/Isar/generic_target.ML	Sun Apr 01 19:07:32 2012 +0200
     5.3 @@ -142,7 +142,6 @@
     5.4  
     5.5  fun notes target_notes kind facts lthy =
     5.6    let
     5.7 -    val thy = Proof_Context.theory_of lthy;
     5.8      val facts' = facts
     5.9        |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
    5.10            (Local_Theory.full_name lthy (fst a))) bs))
    5.11 @@ -152,7 +151,7 @@
    5.12    in
    5.13      lthy
    5.14      |> target_notes kind global_facts local_facts
    5.15 -    |> Proof_Context.note_thmss kind (Attrib.map_facts (map (Attrib.attribute_i thy)) local_facts)
    5.16 +    |> Attrib.local_notes kind local_facts
    5.17    end;
    5.18  
    5.19  
    5.20 @@ -215,15 +214,9 @@
    5.21            (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
    5.22    in ((lhs, def), lthy3) end;
    5.23  
    5.24 -fun theory_notes kind global_facts lthy =
    5.25 -  let
    5.26 -    val thy = Proof_Context.theory_of lthy;
    5.27 -    val global_facts' = Attrib.map_facts (map (Attrib.attribute_i thy)) global_facts;
    5.28 -  in
    5.29 -    lthy
    5.30 -    |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
    5.31 -    |> Local_Theory.target (Proof_Context.note_thmss kind global_facts' #> snd)
    5.32 -  end;
    5.33 +fun theory_notes kind global_facts =
    5.34 +  Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>
    5.35 +  Local_Theory.target (Attrib.local_notes kind global_facts #> snd);
    5.36  
    5.37  fun theory_abbrev prmode ((b, mx), t) =
    5.38    Local_Theory.background_theory
     6.1 --- a/src/Pure/Isar/locale.ML	Sun Apr 01 19:04:52 2012 +0200
     6.2 +++ b/src/Pure/Isar/locale.ML	Sun Apr 01 19:07:32 2012 +0200
     6.3 @@ -535,18 +535,13 @@
     6.4  fun add_thmss _ _ [] ctxt = ctxt
     6.5    | add_thmss loc kind facts ctxt =
     6.6        ctxt
     6.7 -      |> Proof_Context.note_thmss kind
     6.8 -        (Attrib.map_facts (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) facts)
     6.9 -      |> snd
    6.10 +      |> Attrib.local_notes kind facts |> snd
    6.11        |> Proof_Context.background_theory
    6.12          ((change_locale loc o apfst o apsnd) (cons ((kind, facts), serial ())) #>
    6.13            (* Registrations *)
    6.14 -          (fn thy => fold_rev (fn (_, morph) =>
    6.15 -                let
    6.16 -                  val facts' = facts
    6.17 -                    |> Element.transform_facts morph
    6.18 -                    |> Attrib.map_facts (map (Attrib.attribute_i thy));
    6.19 -                in snd o Global_Theory.note_thmss kind facts' end)
    6.20 +          (fn thy =>
    6.21 +            fold_rev (fn (_, morph) =>
    6.22 +              snd o Attrib.global_notes kind (Element.transform_facts morph facts))
    6.23              (registrations_of (Context.Theory thy) loc) thy));
    6.24  
    6.25  
     7.1 --- a/src/Tools/interpretation_with_defs.ML	Sun Apr 01 19:04:52 2012 +0200
     7.2 +++ b/src/Tools/interpretation_with_defs.ML	Sun Apr 01 19:07:32 2012 +0200
     7.3 @@ -23,7 +23,7 @@
     7.4        map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
     7.5          maps snd;
     7.6    in
     7.7 -    Element.generic_note_thmss Thm.lemmaK
     7.8 +    Attrib.generic_notes Thm.lemmaK
     7.9        (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
    7.10      #-> (fn facts => `(fn context => meta_rewrite context facts))
    7.11      #-> (fn eqns => fold (fn ((dep, morph), wits) =>