# HG changeset patch # User wenzelm # Date 1321733918 -3600 # Node ID 8baa0b7f3f66320cd4ba17e0ddeceb214dec61c3 # Parent 4e88993579711372035ad68d6fe78e115e181786 added ML antiquotation @{attributes}; diff -r 4e8899357971 -r 8baa0b7f3f66 NEWS --- a/NEWS Sat Nov 19 17:20:17 2011 +0100 +++ b/NEWS Sat Nov 19 21:18:38 2011 +0100 @@ -137,6 +137,10 @@ *** ML *** +* Antiquotation @{attributes [...]} embeds attribute source +representation into the ML text, which is particularly useful with +declarations like Local_Theory.note. + * Structure Proof_Context follows standard naming scheme. Old ProofContext has been discontinued. INCOMPATIBILITY. diff -r 4e8899357971 -r 8baa0b7f3f66 doc-src/IsarImplementation/Thy/Isar.thy --- a/doc-src/IsarImplementation/Thy/Isar.thy Sat Nov 19 17:20:17 2011 +0100 +++ b/doc-src/IsarImplementation/Thy/Isar.thy Sat Nov 19 21:18:38 2011 +0100 @@ -562,6 +562,27 @@ \end{description} *} +text %mlantiq {* + \begin{matharray}{rcl} + @{ML_antiquotation_def attributes} & : & @{text ML_antiquotation} \\ + \end{matharray} + + @{rail " + @@{ML_antiquotation attributes} attributes + "} + + \begin{description} + + \item @{text "@{attributes [\]}"} embeds attribute source + representation into the ML text, which is particularly useful with + declarations like @{ML Local_Theory.note}. Attribute names are + internalized at compile time, but the source is unevaluated. This + means attributes with formal arguments (types, terms, theorems) may + be subject to odd effects of dynamic scoping! + + \end{description} +*} + text %mlex {* See also @{command attribute_setup} in \cite{isabelle-isar-ref} which includes some abstract examples. *} diff -r 4e8899357971 -r 8baa0b7f3f66 doc-src/IsarImplementation/Thy/document/Isar.tex --- a/doc-src/IsarImplementation/Thy/document/Isar.tex Sat Nov 19 17:20:17 2011 +0100 +++ b/doc-src/IsarImplementation/Thy/document/Isar.tex Sat Nov 19 21:18:38 2011 +0100 @@ -900,6 +900,45 @@ % \endisadelimmlref % +\isadelimmlantiq +% +\endisadelimmlantiq +% +\isatagmlantiq +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{ML antiquotation}{attributes}\hypertarget{ML antiquotation.attributes}{\hyperlink{ML antiquotation.attributes}{\mbox{\isa{attributes}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ + \end{matharray} + + \begin{railoutput} +\rail@begin{1}{} +\rail@term{\hyperlink{ML antiquotation.attributes}{\mbox{\isa{attributes}}}}[] +\rail@nont{\isa{attributes}}[] +\rail@end +\end{railoutput} + + + \begin{description} + + \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}attributes\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{7D}{\isacharbraceright}}} embeds attribute source + representation into the ML text, which is particularly useful with + declarations like \verb|Local_Theory.note|. Attribute names are + internalized at compile time, but the source is unevaluated. This + means attributes with formal arguments (types, terms, theorems) may + be subject to odd effects of dynamic scoping! + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagmlantiq +{\isafoldmlantiq}% +% +\isadelimmlantiq +% +\endisadelimmlantiq +% \isadelimmlex % \endisadelimmlex diff -r 4e8899357971 -r 8baa0b7f3f66 src/HOL/HOLCF/Tools/fixrec.ML --- a/src/HOL/HOLCF/Tools/fixrec.ML Sat Nov 19 17:20:17 2011 +0100 +++ b/src/HOL/HOLCF/Tools/fixrec.ML Sat Nov 19 21:18:38 2011 +0100 @@ -363,8 +363,7 @@ val simps : (Attrib.binding * thm) list list = map (make_simps lthy) (unfold_thms ~~ blocks') fun mk_bind n : Attrib.binding = - (Binding.qualify true n (Binding.name "simps"), - [Attrib.internal (K Simplifier.simp_add)]) + (Binding.qualify true n (Binding.name "simps"), @{attributes [simp]}) val simps1 : (Attrib.binding * thm list) list = map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps) val simps2 : (Attrib.binding * thm list) list = diff -r 4e8899357971 -r 8baa0b7f3f66 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Sat Nov 19 17:20:17 2011 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Sat Nov 19 21:18:38 2011 +0100 @@ -364,17 +364,16 @@ Variable.add_fixes (map fst lsrs) |> snd |> Proof.theorem NONE (fn thss => fn goal_ctxt => - let - val simps = Proof_Context.export goal_ctxt lthy' (flat thss); - val (simps', lthy'') = + let + val simps = Proof_Context.export goal_ctxt lthy' (flat thss); + val (simps', lthy'') = fold_map Local_Theory.note (names_atts' ~~ map single simps) lthy'; - in - lthy'' - |> Local_Theory.note ((qualify (Binding.name "simps"), - map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]), - maps snd simps') - |> snd - end) + in + lthy'' + |> Local_Theory.note + ((qualify (Binding.name "simps"), @{attributes [simp, nitpick_simp]}), maps snd simps') + |> snd + end) [goals] |> Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ => rewrite_goals_tac defs_thms THEN diff -r 4e8899357971 -r 8baa0b7f3f66 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Sat Nov 19 17:20:17 2011 +0100 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Sat Nov 19 21:18:38 2011 +0100 @@ -260,21 +260,18 @@ (Const (@{const_name last_el}, T), List.last cs))) (fn _ => simp_tac (simpset_of lthy' addsimps [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1); - - val simp_att = [Attrib.internal (K Simplifier.simp_add)] - in lthy' |> Local_Theory.note - ((Binding.name (tyname ^ "_card"), simp_att), [card_UNIV]) ||>> + ((Binding.name (tyname ^ "_card"), @{attributes [simp]}), [card_UNIV]) ||>> Local_Theory.note - ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>> + ((Binding.name (tyname ^ "_pos"), @{attributes [simp]}), pos_eqs) ||>> Local_Theory.note - ((Binding.name (tyname ^ "_val"), simp_att), val_eqs) ||>> + ((Binding.name (tyname ^ "_val"), @{attributes [simp]}), val_eqs) ||>> Local_Theory.note - ((Binding.name (tyname ^ "_first_el"), simp_att), [first_el]) ||>> + ((Binding.name (tyname ^ "_first_el"), @{attributes [simp]}), [first_el]) ||>> Local_Theory.note - ((Binding.name (tyname ^ "_last_el"), simp_att), [last_el]) |> snd |> + ((Binding.name (tyname ^ "_last_el"), @{attributes [simp]}), [last_el]) |> snd |> Local_Theory.exit_global end; diff -r 4e8899357971 -r 8baa0b7f3f66 src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Sat Nov 19 17:20:17 2011 +0100 +++ b/src/HOL/Tools/Function/function.ML Sat Nov 19 21:18:38 2011 +0100 @@ -45,13 +45,11 @@ open Function_Lib open Function_Common -val simp_attribs = map (Attrib.internal o K) - [Simplifier.simp_add, - Code.add_default_eqn_attribute, - Nitpick_Simps.add] +val simp_attribs = + @{attributes [simp, nitpick_simp]} @ [Attrib.internal (K Code.add_default_eqn_attribute)] -val psimp_attribs = map (Attrib.internal o K) - [Nitpick_Psimps.add] +val psimp_attribs = + @{attributes [nitpick_psimp]} fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" diff -r 4e8899357971 -r 8baa0b7f3f66 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Nov 19 17:20:17 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Nov 19 21:18:38 2011 +0100 @@ -1419,6 +1419,7 @@ val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds (maps_modes result_thms) val qname = #qname (dest_steps steps) + (* FIXME !? *) val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute (fn thm => Context.mapping (Code.add_eqn thm) I)))) val thy''' = diff -r 4e8899357971 -r 8baa0b7f3f66 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Nov 19 17:20:17 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Nov 19 21:18:38 2011 +0100 @@ -325,10 +325,11 @@ (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy))) eqs_t in fold (fn (name, eq) => Local_Theory.note - ((Binding.conceal (Binding.qualify true prfx - (Binding.qualify true name (Binding.name "simps"))), - Code.add_default_eqn_attrib :: map (Attrib.internal o K) - [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (names ~~ eqs) lthy + ((Binding.conceal + (Binding.qualify true prfx + (Binding.qualify true name (Binding.name "simps"))), + Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), [eq]) #> snd) + (names ~~ eqs) lthy end) (** ensuring sort constraints **) diff -r 4e8899357971 -r 8baa0b7f3f66 src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Sat Nov 19 17:20:17 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sat Nov 19 21:18:38 2011 +0100 @@ -171,8 +171,7 @@ |> random_aux_primrec_multi (name ^ prfx) proto_eqs |-> (fn proto_simps => prove_simps proto_simps) |-> (fn simps => Local_Theory.note - ((b, Code.add_default_eqn_attrib :: map (Attrib.internal o K) - [Simplifier.simp_add, Nitpick_Simps.add]), simps)) + ((b, Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), simps)) |> snd end diff -r 4e8899357971 -r 8baa0b7f3f66 src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Sat Nov 19 17:20:17 2011 +0100 +++ b/src/HOL/Tools/choice_specification.ML Sat Nov 19 21:18:38 2011 +0100 @@ -194,8 +194,9 @@ args |> apsnd (remove_alls frees) |> apsnd undo_imps |> apsnd Drule.export_without_context - |> Thm.theory_attributes (map (Attrib.attribute thy) - (Attrib.internal (K Nitpick_Choice_Specs.add) :: atts)) + |> Thm.theory_attributes + (map (Attrib.attribute thy) + (@{attributes [nitpick_choice_spec]} @ atts)) |> add_final |> Library.swap end diff -r 4e8899357971 -r 8baa0b7f3f66 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Sat Nov 19 17:20:17 2011 +0100 +++ b/src/HOL/Tools/inductive.ML Sat Nov 19 21:18:38 2011 +0100 @@ -775,9 +775,9 @@ |> Local_Theory.conceal |> Local_Theory.define ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn), - ((Binding.empty, [Attrib.internal (K Nitpick_Unfolds.add)]), - fold_rev lambda params - (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) + ((Binding.empty, @{attributes [nitpick_unfold]}), + fold_rev lambda params + (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) ||> Local_Theory.restore_naming lthy; val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def]) (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params))); diff -r 4e8899357971 -r 8baa0b7f3f66 src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Sat Nov 19 17:20:17 2011 +0100 +++ b/src/HOL/Tools/primrec.ML Sat Nov 19 21:18:38 2011 +0100 @@ -276,8 +276,7 @@ fun attr_bindings prefix = map (fn ((b, attrs), _) => (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec; fun simp_attr_binding prefix = - (Binding.qualify true prefix (Binding.name "simps"), - map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]); + (Binding.qualify true prefix (Binding.name "simps"), @{attributes [simp, nitpick_simp]}); in lthy |> add_primrec_simple fixes (map snd spec) diff -r 4e8899357971 -r 8baa0b7f3f66 src/Pure/Isar/parse_spec.ML --- a/src/Pure/Isar/parse_spec.ML Sat Nov 19 17:20:17 2011 +0100 +++ b/src/Pure/Isar/parse_spec.ML Sat Nov 19 21:18:38 2011 +0100 @@ -6,7 +6,6 @@ signature PARSE_SPEC = sig - val attrib: Attrib.src parser val attribs: Attrib.src list parser val opt_attribs: Attrib.src list parser val thm_name: string -> Attrib.binding parser diff -r 4e8899357971 -r 8baa0b7f3f66 src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Sat Nov 19 17:20:17 2011 +0100 +++ b/src/Pure/ML/ml_thms.ML Sat Nov 19 21:18:38 2011 +0100 @@ -1,11 +1,12 @@ (* Title: Pure/ML/ml_thms.ML Author: Makarius -Isar theorem values within ML. +Attribute source and theorem values within ML. *) signature ML_THMS = sig + val the_attributes: Proof.context -> int -> Args.src list val the_thms: Proof.context -> int -> thm list val the_thm: Proof.context -> int -> thm end; @@ -13,26 +14,49 @@ structure ML_Thms: ML_THMS = struct -(* auxiliary facts table *) +(* auxiliary data *) -structure Aux_Facts = Proof_Data +structure Data = Proof_Data ( - type T = thm list Inttab.table; - fun init _ = Inttab.empty; + type T = Args.src list Inttab.table * thm list Inttab.table; + fun init _ = (Inttab.empty, Inttab.empty); ); -val put_thms = Aux_Facts.map o Inttab.update; +val put_attributes = Data.map o apfst o Inttab.update; +fun the_attributes ctxt name = the (Inttab.lookup (fst (Data.get ctxt)) name); + +val put_thms = Data.map o apsnd o Inttab.update; + +fun the_thms ctxt name = the (Inttab.lookup (snd (Data.get ctxt)) name); +fun the_thm ctxt name = the_single (the_thms ctxt name); + + +(* attribute source *) -fun the_thms ctxt name = the (Inttab.lookup (Aux_Facts.get ctxt) name); -fun the_thm ctxt name = the_single (the_thms ctxt name); +val _ = + Context.>> (Context.map_theory + (ML_Context.add_antiq (Binding.name "attributes") + (fn _ => Scan.lift Parse_Spec.attribs >> (fn raw_srcs => fn background => + let + val thy = Proof_Context.theory_of background; + + val i = serial (); + val srcs = map (Attrib.intern_src thy) raw_srcs; + val _ = map (Attrib.attribute_i thy) srcs; + val (a, background') = background + |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs); + val ml = + ("val " ^ a ^ " = ML_Thms.the_attributes (ML_Context.the_local_context ()) " ^ + string_of_int i ^ ";\n", "Isabelle." ^ a); + in (K ml, background') end)))); + + +(* fact references *) fun thm_bind kind a i = "val " ^ a ^ " = ML_Thms.the_" ^ kind ^ " (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n"; - -(* fact references *) - fun thm_antiq kind scan = ML_Context.add_antiq (Binding.name kind) (fn _ => scan >> (fn ths => fn background => let diff -r 4e8899357971 -r 8baa0b7f3f66 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Nov 19 17:20:17 2011 +0100 +++ b/src/Pure/ROOT.ML Sat Nov 19 21:18:38 2011 +0100 @@ -207,7 +207,6 @@ use "Isar/skip_proof.ML"; use "Isar/method.ML"; use "Isar/proof.ML"; -use "ML/ml_thms.ML"; use "Isar/element.ML"; (*derived theory and proof elements*) @@ -235,6 +234,7 @@ use "Isar/spec_rules.ML"; use "Isar/specification.ML"; use "Isar/typedecl.ML"; +use "ML/ml_thms.ML"; (*toplevel transactions*) use "Isar/proof_node.ML";