--- 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.
--- 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 [\<dots>]}"} 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. *}
--- 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
--- 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 =
--- 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
--- 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;
--- 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 "_"
--- 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''' =
--- 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 **)
--- 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
--- 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
--- 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)));
--- 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)
--- 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
--- 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
--- 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";