--- a/NEWS Sat Mar 14 17:52:53 2009 +0100
+++ b/NEWS Sun Mar 15 16:59:17 2009 +0100
@@ -602,6 +602,9 @@
delicate details of mutexes and condition variables. [Poly/ML 5.2.1
or later]
+* Simplified ML attribute and method setup, cf. functions Attrib.setup
+and Method.setup, as well as commands 'attribute_setup'.
+
* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
to 'a -> thm, while results are always tagged with an authentic oracle
name. The Isar command 'oracle' is now polymorphic, no argument type
--- a/doc-src/IsarRef/Thy/Spec.thy Sat Mar 14 17:52:53 2009 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Sun Mar 15 16:59:17 2009 +0100
@@ -800,6 +800,7 @@
@{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
@{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
\begin{mldecls}
@@ -812,6 +813,8 @@
;
('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
;
+ 'attribute\_setup' name '=' text text
+ ;
\end{rail}
\begin{description}
@@ -856,6 +859,34 @@
invoke local theory specification packages without going through
concrete outer syntax, for example.
+ \item @{command "attribute_setup"}~@{text "name = text description"}
+ defines an attribute in the current theory. The given @{text
+ "text"} has to be an ML expression of type
+ @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
+ structure @{ML_struct Args} and @{ML_struct Attrib}.
+
+ In principle, attributes can operate both on a given theorem and the
+ implicit context, although in practice only one is modified and the
+ other serves as parameter. Here are examples for these two cases:
+
+ \end{description}
+*}
+
+ attribute_setup my_rule = {*
+ Attrib.thms >> (fn ths =>
+ Thm.rule_attribute (fn context: Context.generic => fn th: thm =>
+ let val th' = th OF ths
+ in th' end)) *} "my rule"
+
+ attribute_setup my_declatation = {*
+ Attrib.thms >> (fn ths =>
+ Thm.declaration_attribute (fn th: thm => fn context: Context.generic =>
+ let val context' = context
+ in context' end)) *} "my declaration"
+
+text {*
+ \begin{description}
+
\item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
theorems produced in ML both in the theory context and the ML
toplevel, associating it with the provided name. Theorems are put
--- a/doc-src/IsarRef/Thy/document/Spec.tex Sat Mar 14 17:52:53 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Sun Mar 15 16:59:17 2009 +0100
@@ -808,6 +808,7 @@
\indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
\indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
\indexdef{}{command}{local\_setup}\hypertarget{command.local-setup}{\hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
+ \indexdef{}{command}{attribute\_setup}\hypertarget{command.attribute-setup}{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
\end{matharray}
\begin{mldecls}
@@ -820,6 +821,8 @@
;
('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
;
+ 'attribute\_setup' name '=' text text
+ ;
\end{rail}
\begin{description}
@@ -862,6 +865,47 @@
invoke local theory specification packages without going through
concrete outer syntax, for example.
+ \item \hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}
+ defines an attribute in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type
+ \verb|attribute context_parser|, cf.\ basic parsers defined in
+ structure \verb|Args| and \verb|Attrib|.
+
+ In principle, attributes can operate both on a given theorem and the
+ implicit context, although in practice only one is modified and the
+ other serves as parameter. Here are examples for these two cases:
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+\ \ \ \ %
+\endisadelimML
+%
+\isatagML
+\isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
+\ my{\isacharunderscore}rule\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
+\ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ Thm{\isachardot}rule{\isacharunderscore}attribute\ {\isacharparenleft}fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\ fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ \ \ let\ val\ th{\isacharprime}\ {\isacharequal}\ th\ OF\ ths\isanewline
+\ \ \ \ \ \ \ \ \ \ in\ th{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ rule{\isachardoublequoteclose}\isanewline
+\isanewline
+\ \ \ \ \isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
+\ my{\isacharunderscore}declatation\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
+\ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ Thm{\isachardot}declaration{\isacharunderscore}attribute\ {\isacharparenleft}fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\ fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ \ \ let\ val\ context{\isacharprime}\ {\isacharequal}\ context\isanewline
+\ \ \ \ \ \ \ \ \ \ in\ context{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ declaration{\isachardoublequoteclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+\begin{description}
+
\item \verb|bind_thms|~\isa{{\isachardoublequote}{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}{\isachardoublequote}} stores a list of
theorems produced in ML both in the theory context and the ML
toplevel, associating it with the provided name. Theorems are put
--- a/etc/isar-keywords-ZF.el Sat Mar 14 17:52:53 2009 +0100
+++ b/etc/isar-keywords-ZF.el Sun Mar 15 16:59:17 2009 +0100
@@ -31,6 +31,7 @@
"apply_end"
"arities"
"assume"
+ "attribute_setup"
"axclass"
"axiomatization"
"axioms"
@@ -349,6 +350,7 @@
'("ML"
"abbreviation"
"arities"
+ "attribute_setup"
"axclass"
"axiomatization"
"axioms"
--- a/etc/isar-keywords.el Sat Mar 14 17:52:53 2009 +0100
+++ b/etc/isar-keywords.el Sun Mar 15 16:59:17 2009 +0100
@@ -35,6 +35,7 @@
"atp_info"
"atp_kill"
"atp_messages"
+ "attribute_setup"
"automaton"
"ax_specification"
"axclass"
@@ -421,6 +422,7 @@
"abbreviation"
"arities"
"atom_decl"
+ "attribute_setup"
"automaton"
"axclass"
"axiomatization"
--- a/lib/jedit/isabelle.xml Sat Mar 14 17:52:53 2009 +0100
+++ b/lib/jedit/isabelle.xml Sun Mar 15 16:59:17 2009 +0100
@@ -61,6 +61,7 @@
<LABEL>atp_kill</LABEL>
<LABEL>atp_messages</LABEL>
<KEYWORD4>attach</KEYWORD4>
+ <OPERATOR>attribute_setup</OPERATOR>
<OPERATOR>automaton</OPERATOR>
<KEYWORD4>avoids</KEYWORD4>
<OPERATOR>ax_specification</OPERATOR>
--- a/src/HOL/Algebra/ringsimp.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Sun Mar 15 16:59:17 2009 +0100
@@ -62,11 +62,11 @@
Thm.declaration_attribute
(fn _ => Data.map (AList.delete struct_eq s));
-val attribute = Attrib.syntax
- (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
- Scan.succeed true) -- Scan.lift Args.name --
- Scan.repeat Args.term
- >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)));
+val attribute =
+ Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
+ Scan.succeed true) -- Scan.lift Args.name --
+ Scan.repeat Args.term
+ >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts));
(** Setup **)
@@ -74,6 +74,6 @@
val setup =
Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
"normalisation of algebraic structure" #>
- Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
+ Attrib.setup @{binding algebra} attribute "theorems controlling algebra method";
end;
--- a/src/HOL/Import/hol4rews.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Import/hol4rews.ML Sun Mar 15 16:59:17 2009 +0100
@@ -649,6 +649,6 @@
in
val hol4_setup =
initial_maps #>
- Attrib.add_attributes
- [("hol4rew", Attrib.no_args add_hol4_rewrite, "HOL4 rewrite rule")]
+ Attrib.setup @{binding hol4rew} (Scan.succeed add_hol4_rewrite) "HOL4 rewrite rule"
+
end
--- a/src/HOL/Import/shuffler.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Import/shuffler.ML Sun Mar 15 16:59:17 2009 +0100
@@ -689,6 +689,6 @@
add_shuffle_rule imp_comm #>
add_shuffle_rule Drule.norm_hhf_eq #>
add_shuffle_rule Drule.triv_forall_equality #>
- Attrib.add_attributes [("shuffle_rule", Attrib.no_args shuffle_attr, "declare rule for shuffler")]
+ Attrib.setup @{binding shuffle_rule} (Scan.succeed shuffle_attr) "declare rule for shuffler";
end
--- a/src/HOL/Library/reify_data.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Library/reify_data.ML Sun Mar 15 16:59:17 2009 +0100
@@ -32,8 +32,8 @@
val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
-val setup = Attrib.add_attributes
- [("reify", Attrib.add_del_args add del, "Reify data"),
- ("reflection", Attrib.add_del_args radd rdel, "Reflection data")];
+val setup =
+ Attrib.setup @{binding reify} (Attrib.add_del add del) "reify data" #>
+ Attrib.setup @{binding reflection} (Attrib.add_del radd rdel) "reflection data";
end;
--- a/src/HOL/NSA/transfer.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/NSA/transfer.ML Sun Mar 15 16:59:17 2009 +0100
@@ -108,14 +108,13 @@
{intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
val setup =
- Attrib.add_attributes
- [("transfer_intro", Attrib.add_del_args intro_add intro_del,
- "declaration of transfer introduction rule"),
- ("transfer_unfold", Attrib.add_del_args unfold_add unfold_del,
- "declaration of transfer unfolding rule"),
- ("transfer_refold", Attrib.add_del_args refold_add refold_del,
- "declaration of transfer refolding rule")] #>
- Method.add_method ("transfer", Method.thms_ctxt_args (fn ths => fn ctxt =>
- SIMPLE_METHOD' (transfer_tac ctxt ths)), "transfer principle");
+ Attrib.setup @{binding transfer_intro} (Attrib.add_del intro_add intro_del)
+ "declaration of transfer introduction rule" #>
+ Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del)
+ "declaration of transfer unfolding rule" #>
+ Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del)
+ "declaration of transfer refolding rule" #>
+ Method.setup @{binding transfer} (Attrib.thms >> (fn ths => fn ctxt =>
+ SIMPLE_METHOD' (transfer_tac ctxt ths))) "transfer principle";
end;
--- a/src/HOL/Nominal/nominal_thmdecls.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Sun Mar 15 16:59:17 2009 +0100
@@ -187,12 +187,14 @@
val setup =
- Attrib.add_attributes
- [("eqvt", Attrib.add_del_args eqvt_add eqvt_del, "equivariance theorem declaration"),
- ("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del,
- "equivariance theorem declaration (without checking the form of the lemma)"),
- ("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"),
- ("bij", Attrib.add_del_args bij_add bij_del, "bijection theorem declaration")] #>
+ Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del)
+ "equivariance theorem declaration" #>
+ Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
+ "equivariance theorem declaration (without checking the form of the lemma)" #>
+ Attrib.setup @{binding fresh} (Attrib.add_del fresh_add fresh_del)
+ "freshness theorem declaration" #>
+ Attrib.setup @{binding "bij"} (Attrib.add_del bij_add bij_del)
+ "bijection theorem declaration" #>
PureThy.add_thms_dynamic (Binding.name "eqvts", #eqvts o Data.get) #>
PureThy.add_thms_dynamic (Binding.name "freshs", #freshs o Data.get) #>
PureThy.add_thms_dynamic (Binding.name "bijs", #bijs o Data.get);
--- a/src/HOL/Orderings.thy Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Orderings.thy Sun Mar 15 16:59:17 2009 +0100
@@ -372,13 +372,13 @@
Thm.declaration_attribute
(fn _ => Data.map (AList.delete struct_eq s));
-val attribute = Attrib.syntax
- (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) ||
- Args.del >> K NONE) --| Args.colon (* FIXME ||
- Scan.succeed true *) ) -- Scan.lift Args.name --
- Scan.repeat Args.term
- >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
- | ((NONE, n), ts) => del_struct (n, ts)));
+val attribute =
+ Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) ||
+ Args.del >> K NONE) --| Args.colon (* FIXME ||
+ Scan.succeed true *) ) -- Scan.lift Args.name --
+ Scan.repeat Args.term
+ >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
+ | ((NONE, n), ts) => del_struct (n, ts));
(** Diagnostic command **)
@@ -398,7 +398,7 @@
val setup =
Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #>
- Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
+ Attrib.setup @{binding order} attribute "theorems controlling transitivity reasoner";
end;
--- a/src/HOL/Statespace/state_fun.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Statespace/state_fun.ML Sun Mar 15 16:59:17 2009 +0100
@@ -371,7 +371,7 @@
val mk_destr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ b $ a) "the_"
-fun statefun_simp_attr src (ctxt,thm) =
+val statefun_simp_attr = Thm.declaration_attribute (fn thm => fn ctxt =>
let
val (lookup_ss,ex_lookup_ss,simprocs_active) = StateFunData.get ctxt;
val (lookup_ss', ex_lookup_ss') =
@@ -381,15 +381,14 @@
fun activate_simprocs ctxt =
if simprocs_active then ctxt
else Simplifier.map_ss (fn ss => ss addsimprocs [lookup_simproc,update_simproc]) ctxt
-
-
- val ctxt' = ctxt
- |> activate_simprocs
- |> (StateFunData.put (lookup_ss',ex_lookup_ss',true))
- in (ctxt', thm) end;
+ in
+ ctxt
+ |> activate_simprocs
+ |> (StateFunData.put (lookup_ss',ex_lookup_ss',true))
+ end);
val setup =
- init_state_fun_data
- #> Attrib.add_attributes
- [("statefun_simp",statefun_simp_attr,"simplification in statespaces")]
+ init_state_fun_data #>
+ Attrib.setup @{binding statefun_simp} (Scan.succeed statefun_simp_attr)
+ "simplification in statespaces"
end
--- a/src/HOL/TLA/Action.thy Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/TLA/Action.thy Sun Mar 15 16:59:17 2009 +0100
@@ -124,12 +124,9 @@
| _ => th;
*}
-setup {*
- Attrib.add_attributes [
- ("action_unlift", Attrib.no_args (Thm.rule_attribute (K action_unlift)), ""),
- ("action_rewrite", Attrib.no_args (Thm.rule_attribute (K action_rewrite)), ""),
- ("action_use", Attrib.no_args (Thm.rule_attribute (K action_use)), "")]
-*}
+attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *} ""
+attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *} ""
+attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *} ""
(* =========================== square / angle brackets =========================== *)
--- a/src/HOL/TLA/Intensional.thy Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/TLA/Intensional.thy Sun Mar 15 16:59:17 2009 +0100
@@ -294,13 +294,10 @@
| _ => th
*}
-setup {*
- Attrib.add_attributes [
- ("int_unlift", Attrib.no_args (Thm.rule_attribute (K int_unlift)), ""),
- ("int_rewrite", Attrib.no_args (Thm.rule_attribute (K int_rewrite)), ""),
- ("flatten", Attrib.no_args (Thm.rule_attribute (K flatten)), ""),
- ("int_use", Attrib.no_args (Thm.rule_attribute (K int_use)), "")]
-*}
+attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *} ""
+attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *} ""
+attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *} ""
+attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *} ""
lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
by (simp add: Valid_def)
--- a/src/HOL/TLA/TLA.thy Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/TLA/TLA.thy Sun Mar 15 16:59:17 2009 +0100
@@ -130,13 +130,11 @@
fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th;
*}
-setup {*
- Attrib.add_attributes [
- ("temp_unlift", Attrib.no_args (Thm.rule_attribute (K temp_unlift)), ""),
- ("temp_rewrite", Attrib.no_args (Thm.rule_attribute (K temp_rewrite)), ""),
- ("temp_use", Attrib.no_args (Thm.rule_attribute (K temp_use)), ""),
- ("try_rewrite", Attrib.no_args (Thm.rule_attribute (K try_rewrite)), "")]
-*}
+attribute_setup temp_unlift = {* Scan.succeed (Thm.rule_attribute (K temp_unlift)) *} ""
+attribute_setup temp_rewrite = {* Scan.succeed (Thm.rule_attribute (K temp_rewrite)) *} ""
+attribute_setup temp_use = {* Scan.succeed (Thm.rule_attribute (K temp_use)) *} ""
+attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *} ""
+
(* Update classical reasoner---will be updated once more below! *)
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sun Mar 15 16:59:17 2009 +0100
@@ -191,8 +191,8 @@
in
-val att_syntax = Attrib.syntax
- (Scan.lift (Args.$$$ delN >> K del) ||
+val attribute =
+ Scan.lift (Args.$$$ delN >> K del) ||
((keyword2 semiringN opsN |-- terms) --
(keyword2 semiringN rulesN |-- thms)) --
(optional (keyword2 ringN opsN |-- terms) --
@@ -200,7 +200,7 @@
optional (keyword2 idomN rulesN |-- thms) --
optional (keyword2 idealN rulesN |-- thms)
>> (fn (((sr, r), id), idl) =>
- add {semiring = sr, ring = r, idom = id, ideal = idl}));
+ add {semiring = sr, ring = r, idom = id, ideal = idl});
end;
@@ -208,8 +208,7 @@
(* theory setup *)
val setup =
- Attrib.add_attributes
- [("normalizer", att_syntax, "semiring normalizer data"),
- ("algebra", Attrib.add_del_args add_ss del_ss, "Pre-simplification for algebra")];
+ Attrib.setup @{binding normalizer} attribute "semiring normalizer data" #>
+ Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra";
end;
--- a/src/HOL/Tools/Qelim/cooper_data.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML Sun Mar 15 16:59:17 2009 +0100
@@ -77,15 +77,14 @@
fun optional scan = Scan.optional scan [];
in
-val att_syntax = Attrib.syntax
- ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
- optional (keyword constsN |-- terms) >> add)
+val attribute =
+ (Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
+ optional (keyword constsN |-- terms) >> add
end;
(* theory setup *)
-val setup =
- Attrib.add_attributes [("presburger", att_syntax, "Cooper data")];
+val setup = Attrib.setup @{binding presburger} attribute "Cooper data";
end;
--- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML Sun Mar 15 16:59:17 2009 +0100
@@ -122,8 +122,8 @@
val terms = thms >> map Drule.dest_term;
in
-val att_syntax = Attrib.syntax
- ((keyword minfN |-- thms)
+val attribute =
+ (keyword minfN |-- thms)
-- (keyword pinfN |-- thms)
-- (keyword nmiN |-- thms)
-- (keyword npiN |-- thms)
@@ -135,14 +135,13 @@
add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense,
qe = hd qe, atoms = atoms},
{isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
- else error "only one theorem for qe!"))
+ else error "only one theorem for qe!")
end;
(* theory setup *)
-val setup =
- Attrib.add_attributes [("ferrack", att_syntax, "Ferrante Rackoff data")];
+val setup = Attrib.setup @{binding ferrack} attribute "Ferrante Rackoff data";
end;
--- a/src/HOL/Tools/Qelim/langford_data.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Tools/Qelim/langford_data.ML Sun Mar 15 16:59:17 2009 +0100
@@ -85,8 +85,8 @@
val terms = thms >> map Drule.dest_term;
in
-val att_syntax = Attrib.syntax
- ((keyword qeN |-- thms)
+val attribute =
+ (keyword qeN |-- thms)
-- (keyword gatherN |-- thms)
-- (keyword atomsN |-- terms) >>
(fn ((qes,gs), atoms) =>
@@ -97,14 +97,13 @@
val entry = {qe_bnds = q1, qe_nolb = q2,
qe_noub = q3, gs = gss, gst = gst, atoms = atoms}
in add entry end
- else error "Need 3 theorems for qe and at least one for gs"))
+ else error "Need 3 theorems for qe and at least one for gs")
end;
(* theory setup *)
val setup =
- Attrib.add_attributes
-[("langford", att_syntax, "Langford data"),
- ("langfordsimp", Attrib.add_del_args add_simp del_simp, "Langford simpset")];
+ Attrib.setup @{binding langford} attribute "Langford data" #>
+ Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset";
end;
--- a/src/HOL/Tools/function_package/fundef_package.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Sun Mar 15 16:59:17 2009 +0100
@@ -196,9 +196,8 @@
(* setup *)
val setup =
- Attrib.add_attributes
- [("fundef_cong", Attrib.add_del_args FundefCtxTree.cong_add FundefCtxTree.cong_del,
- "declaration of congruence rule for function definitions")]
+ Attrib.setup @{binding fundef_cong} (Attrib.add_del FundefCtxTree.cong_add FundefCtxTree.cong_del)
+ "declaration of congruence rule for function definitions"
#> setup_case_cong
#> FundefRelation.setup
#> FundefCommon.TerminationSimps.setup
--- a/src/HOL/Tools/inductive_package.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Sun Mar 15 16:59:17 2009 +0100
@@ -935,8 +935,8 @@
val setup =
Method.setup @{binding ind_cases} ind_cases "dynamic case analysis on predicates" #>
- Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del,
- "declaration of monotonicity rule")];
+ Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del)
+ "declaration of monotonicity rule";
(* outer syntax *)
--- a/src/HOL/Tools/inductive_realizer.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Sun Mar 15 16:59:17 2009 +0100
@@ -505,13 +505,13 @@
| SOME (SOME sets') => sets \\ sets')
end I);
-val ind_realizer = Attrib.syntax
- ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
+val ind_realizer =
+ (Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
Scan.option (Scan.lift (Args.colon) |--
- Scan.repeat1 Args.const))) >> rlz_attrib);
+ Scan.repeat1 Args.const))) >> rlz_attrib;
val setup =
- Attrib.add_attributes [("ind_realizer", ind_realizer, "add realizers for inductive set")];
+ Attrib.setup @{binding ind_realizer} ind_realizer "add realizers for inductive set";
end;
--- a/src/HOL/Tools/inductive_set_package.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML Sun Mar 15 16:59:17 2009 +0100
@@ -530,20 +530,17 @@
(* setup theory *)
val setup =
- Attrib.add_attributes
- [("pred_set_conv", Attrib.no_args pred_set_conv_att,
- "declare rules for converting between predicate and set notation"),
- ("to_set", Attrib.syntax (Attrib.thms >> to_set_att),
- "convert rule to set notation"),
- ("to_pred", Attrib.syntax (Attrib.thms >> to_pred_att),
- "convert rule to predicate notation")] #>
+ Attrib.setup @{binding pred_set_conv} (Scan.succeed pred_set_conv_att)
+ "declare rules for converting between predicate and set notation" #>
+ Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att) "convert rule to set notation" #>
+ Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att) "convert rule to predicate notation" #>
Code.add_attribute ("ind_set",
Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att) #>
Codegen.add_preprocessor codegen_preproc #>
- Attrib.add_attributes [("mono_set", Attrib.add_del_args mono_add_att mono_del_att,
- "declaration of monotonicity rule for set operators")] #>
- Context.theory_map (Simplifier.map_ss (fn ss =>
- ss addsimprocs [collect_mem_simproc]));
+ Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
+ "declaration of monotonicity rule for set operators" #>
+ Context.theory_map (Simplifier.map_ss (fn ss => ss addsimprocs [collect_mem_simproc]));
+
(* outer syntax *)
--- a/src/HOL/Tools/lin_arith.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML Sun Mar 15 16:59:17 2009 +0100
@@ -930,8 +930,8 @@
Context.mapping
(setup_options #>
Method.setup @{binding arith} arith_method "decide linear arithmetic" #>
- Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add,
- "declaration of split rules for arithmetic procedure")]) I;
+ Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
+ "declaration of split rules for arithmetic procedure") I;
end;
--- a/src/HOL/Tools/recdef_package.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Tools/recdef_package.ML Sun Mar 15 16:59:17 2009 +0100
@@ -282,10 +282,12 @@
(* setup theory *)
val setup =
- Attrib.add_attributes
- [(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
- (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
- (recdef_wfN, Attrib.add_del_args wf_add wf_del, "declaration of recdef wf rule")];
+ Attrib.setup @{binding recdef_simp} (Attrib.add_del simp_add simp_del)
+ "declaration of recdef simp rule" #>
+ Attrib.setup @{binding recdef_cong} (Attrib.add_del cong_add cong_del)
+ "declaration of recdef cong rule" #>
+ Attrib.setup @{binding recdef_wf} (Attrib.add_del wf_add wf_del)
+ "declaration of recdef wf rule";
(* outer syntax *)
--- a/src/HOL/Tools/res_axioms.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Sun Mar 15 16:59:17 2009 +0100
@@ -528,12 +528,11 @@
(** Attribute for converting a theorem into clauses **)
-val clausify = Attrib.syntax (Scan.lift OuterParse.nat
- >> (fn i => Thm.rule_attribute (fn context => fn th =>
- Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))));
+val clausify = Scan.lift OuterParse.nat >>
+ (fn i => Thm.rule_attribute (fn context => fn th =>
+ Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i)));
-val setup_attrs = Attrib.add_attributes
- [("clausify", clausify, "conversion of theorem to clauses")];
+val setup_attrs = Attrib.setup @{binding clausify} clausify "conversion of theorem to clauses";
--- a/src/HOL/Tools/split_rule.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/Tools/split_rule.ML Sun Mar 15 16:59:17 2009 +0100
@@ -145,18 +145,17 @@
(* FIXME dynamically scoped due to Args.name_source/pair_tac *)
-val split_format = Attrib.syntax (Scan.lift
+val split_format = Scan.lift
(Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
OuterParse.and_list1 (Scan.repeat Args.name_source)
>> (fn xss => Thm.rule_attribute (fn context =>
- split_rule_goal (Context.proof_of context) xss))));
+ split_rule_goal (Context.proof_of context) xss)));
val setup =
- Attrib.add_attributes
- [("split_format", split_format,
- "split pair-typed subterms in premises, or function arguments"),
- ("split_rule", Attrib.no_args (Thm.rule_attribute (K split_rule)),
- "curries ALL function variables occurring in a rule's conclusion")];
+ Attrib.setup @{binding split_format} split_format
+ "split pair-typed subterms in premises, or function arguments" #>
+ Attrib.setup @{binding split_rule} (Scan.succeed (Thm.rule_attribute (K split_rule)))
+ "curries ALL function variables occurring in a rule's conclusion";
end;
--- a/src/HOL/UNITY/Comp/Alloc.thy Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy Sun Mar 15 16:59:17 2009 +0100
@@ -298,7 +298,7 @@
lemmas lessThanBspec = lessThan_iff [THEN iffD2, THEN [2] bspec]
-setup {*
+attribute_setup normalized = {*
let
fun normalized th =
normalized (th RS spec
@@ -307,9 +307,9 @@
handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1))
handle THM _ => th;
in
- Attrib.add_attributes [("normalized", Attrib.no_args (Thm.rule_attribute (K normalized)), "")]
+ Scan.succeed (Thm.rule_attribute (K normalized))
end
-*}
+*} ""
(*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
ML {*
--- a/src/HOL/ex/predicate_compile.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/HOL/ex/predicate_compile.ML Sun Mar 15 16:59:17 2009 +0100
@@ -1334,11 +1334,11 @@
val code_ind_cases_attrib = attrib add_elim_thm
-val setup = Attrib.add_attributes
- [("code_ind_intros", Attrib.no_args code_ind_intros_attrib,
- "adding alternative introduction rules for code generation of inductive predicates"),
- ("code_ind_cases", Attrib.no_args code_ind_cases_attrib,
- "adding alternative elimination rules for code generation of inductive predicates")]
+val setup =
+ Attrib.setup @{binding code_ind_intros} (Scan.succeed code_ind_intros_attrib)
+ "adding alternative introduction rules for code generation of inductive predicates" #>
+ Attrib.setup @{binding code_ind_cases} (Scan.succeed code_ind_cases_attrib)
+ "adding alternative elimination rules for code generation of inductive predicates";
end;
--- a/src/Provers/clasimp.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/Provers/clasimp.ML Sun Mar 15 16:59:17 2009 +0100
@@ -268,10 +268,10 @@
val iff_add' = attrib' addIffs_generic;
val iff_del = attrib (op delIffs) o attrib' delIffs_generic;
-val iff_att = Attrib.syntax (Scan.lift
+fun iff_att x = (Scan.lift
(Args.del >> K iff_del ||
Scan.option Args.add -- Args.query >> K iff_add' ||
- Scan.option Args.add >> K iff_add));
+ Scan.option Args.add >> K iff_add)) x;
(* method modifiers *)
@@ -311,8 +311,7 @@
(* theory setup *)
val clasimp_setup =
- (Attrib.add_attributes
- [("iff", iff_att, "declaration of Simplifier / Classical rules")] #>
+ (Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
Method.add_methods
[("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
--- a/src/Provers/classical.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/Provers/classical.ML Sun Mar 15 16:59:17 2009 +0100
@@ -215,7 +215,7 @@
(*Creates rules to eliminate ~A, from rules to introduce A*)
fun swapify intrs = intrs RLN (2, [Data.swap]);
-fun swapped x = Attrib.no_args (fn (x, th) => (x, th RSN (2, Data.swap))) x;
+val swapped = Thm.rule_attribute (fn _ => fn th => th RSN (2, Data.swap));
(*Uses introduction rules in the normal way, or on negated assumptions,
trying rules in order. *)
@@ -956,16 +956,17 @@
val destN = "dest";
val ruleN = "rule";
-val setup_attrs = Attrib.add_attributes
- [("swapped", swapped, "classical swap of introduction rule"),
- (destN, ContextRules.add_args safe_dest haz_dest ContextRules.dest_query,
- "declaration of Classical destruction rule"),
- (elimN, ContextRules.add_args safe_elim haz_elim ContextRules.elim_query,
- "declaration of Classical elimination rule"),
- (introN, ContextRules.add_args safe_intro haz_intro ContextRules.intro_query,
- "declaration of Classical introduction rule"),
- (ruleN, Attrib.syntax (Scan.lift Args.del >> K rule_del),
- "remove declaration of intro/elim/dest rule")];
+val setup_attrs =
+ Attrib.setup @{binding swapped} (Scan.succeed swapped)
+ "classical swap of introduction rule" #>
+ Attrib.setup @{binding dest} (ContextRules.add safe_dest haz_dest ContextRules.dest_query)
+ "declaration of Classical destruction rule" #>
+ Attrib.setup @{binding elim} (ContextRules.add safe_elim haz_elim ContextRules.elim_query)
+ "declaration of Classical elimination rule" #>
+ Attrib.setup @{binding intro} (ContextRules.add safe_intro haz_intro ContextRules.intro_query)
+ "declaration of Classical introduction rule" #>
+ Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
+ "remove declaration of intro/elim/dest rule";
--- a/src/Provers/splitter.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/Provers/splitter.ML Sun Mar 15 16:59:17 2009 +0100
@@ -479,8 +479,7 @@
(* theory setup *)
val setup =
- Attrib.add_attributes
- [(splitN, Attrib.add_del_args split_add split_del, "declaration of case split rule")] #>
+ Attrib.setup @{binding split} (Attrib.add_del split_add split_del) "declare case split rule" #>
Method.setup @{binding split} split_meth "apply case split rule";
end;
--- a/src/Pure/Isar/attrib.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/Pure/Isar/attrib.ML Sun Mar 15 16:59:17 2009 +0100
@@ -25,7 +25,10 @@
val crude_closure: Proof.context -> src -> src
val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
val syntax: attribute context_parser -> src -> attribute
+ val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
+ val attribute_setup: string * Position.T -> string * Position.T -> string -> theory -> theory
val no_args: attribute -> src -> attribute
+ val add_del: attribute -> attribute -> attribute context_parser
val add_del_args: attribute -> attribute -> src -> attribute
val thm_sel: Facts.interval list parser
val thm: thm context_parser
@@ -150,16 +153,27 @@
in Attributes.map add thy end;
-(* attribute syntax *)
+(* attribute setup *)
+
+fun syntax scan src (context, th) =
+ let val (f: attribute, context') = Args.syntax "attribute" scan src context
+ in f (context', th) end;
+
+fun setup name scan comment = add_attributes [(Binding.name_of name, syntax scan, comment)];
-fun syntax scan src (st, th) =
- let val (f: attribute, st') = Args.syntax "attribute" scan src st
- in f (st', th) end;
+fun attribute_setup name (txt, pos) cmt =
+ Context.theory_map (ML_Context.expression pos
+ "val (name, scan, comment): binding * attribute context_parser * string"
+ "Context.map_theory (Attrib.setup name scan comment)"
+ ("(" ^ ML_Syntax.make_binding name ^ ", " ^ txt ^ ", " ^ ML_Syntax.print_string cmt ^ ")"));
+
+
+(* basic syntax *)
fun no_args x = syntax (Scan.succeed x);
-fun add_del_args add del = syntax
- (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add));
+fun add_del add del = (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add));
+fun add_del_args add del = syntax (add_del add del);
--- a/src/Pure/Isar/calculation.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/Pure/Isar/calculation.ML Sun Mar 15 16:59:17 2009 +0100
@@ -88,14 +88,13 @@
(* concrete syntax *)
-val trans_att = Attrib.add_del_args trans_add trans_del;
-val sym_att = Attrib.add_del_args sym_add sym_del;
-
val _ = Context.>> (Context.map_theory
- (Attrib.add_attributes
- [("trans", trans_att, "declaration of transitivity rule"),
- ("sym", sym_att, "declaration of symmetry rule"),
- ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
+ (Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del)
+ "declaration of transitivity rule" #>
+ Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del)
+ "declaration of symmetry rule" #>
+ Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric)
+ "resolution with symmetry rule" #>
PureThy.add_thms
[((Binding.empty, transitive_thm), [trans_add]),
((Binding.empty, symmetric_thm), [sym_add])] #> snd));
--- a/src/Pure/Isar/code.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/Pure/Isar/code.ML Sun Mar 15 16:59:17 2009 +0100
@@ -100,12 +100,11 @@
val _ =
let
- val code_attr = Attrib.syntax (Scan.peek (fn context =>
- List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))));
+ val code_attr = Scan.peek (fn context =>
+ List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context))));
in
Context.>> (Context.map_theory
- (Attrib.add_attributes
- [("code", code_attr, "declare theorems for code generation")]))
+ (Attrib.setup (Binding.name "code") code_attr "declare theorems for code generation"))
end;
--- a/src/Pure/Isar/context_rules.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/Pure/Isar/context_rules.ML Sun Mar 15 16:59:17 2009 +0100
@@ -29,9 +29,8 @@
val elim_query: int option -> attribute
val dest_query: int option -> attribute
val rule_del: attribute
- val add_args:
- (int option -> attribute) -> (int option -> attribute) -> (int option -> attribute) ->
- Attrib.src -> attribute
+ val add: (int option -> attribute) -> (int option -> attribute) -> (int option -> attribute) ->
+ attribute context_parser
end;
structure ContextRules: CONTEXT_RULES =
@@ -203,17 +202,18 @@
(* concrete syntax *)
-fun add_args a b c = Attrib.syntax
+fun add a b c x =
(Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) --
- Scan.option OuterParse.nat) >> (fn (f, n) => f n));
+ Scan.option OuterParse.nat) >> (fn (f, n) => f n)) x;
-val rule_atts =
- [("intro", add_args intro_bang intro intro_query, "declaration of introduction rule"),
- ("elim", add_args elim_bang elim elim_query, "declaration of elimination rule"),
- ("dest", add_args dest_bang dest dest_query, "declaration of destruction rule"),
- ("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
- "remove declaration of intro/elim/dest rule")];
-
-val _ = Context.>> (Context.map_theory (Attrib.add_attributes rule_atts));
+val _ = Context.>> (Context.map_theory
+ (Attrib.setup (Binding.name "intro") (add intro_bang intro intro_query)
+ "declaration of introduction rule" #>
+ Attrib.setup (Binding.name "elim") (add elim_bang elim elim_query)
+ "declaration of elimination rule" #>
+ Attrib.setup (Binding.name "dest") (add dest_bang dest dest_query)
+ "declaration of destruction rule" #>
+ Attrib.setup (Binding.name "rule") (Scan.lift Args.del >> K rule_del)
+ "remove declaration of intro/elim/dest rule"));
end;
--- a/src/Pure/Isar/isar_cmd.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Sun Mar 15 16:59:17 2009 +0100
@@ -155,9 +155,7 @@
val body = SymbolPos.content (SymbolPos.explode (body_txt, body_pos));
val txt =
"local\n\
- \ val name = " ^ ML_Syntax.print_string name ^ ";\n\
- \ val pos = " ^ ML_Syntax.print_position pos ^ ";\n\
- \ val binding = Binding.make (name, pos);\n\
+ \ val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
\ val body = " ^ body ^ ";\n\
\in\n\
\ val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
--- a/src/Pure/Isar/isar_syn.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sun Mar 15 16:59:17 2009 +0100
@@ -328,6 +328,11 @@
(P.ML_source >> IsarCmd.local_setup);
val _ =
+ OuterSyntax.command "attribute_setup" "define attribute in ML" (K.tag_ml K.thy_decl)
+ (P.position P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
+ >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
+
+val _ =
OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
(P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
>> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
--- a/src/Pure/Isar/rule_insts.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML Sun Mar 15 16:59:17 2009 +0100
@@ -218,8 +218,8 @@
in
-val where_att = Attrib.syntax (Scan.lift (P.and_list inst) >> (fn args =>
- Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)));
+fun where_att x = (Scan.lift (P.and_list inst) >> (fn args =>
+ Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args))) x;
end;
@@ -241,8 +241,8 @@
in
-val of_att = Attrib.syntax (Scan.lift insts >> (fn args =>
- Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)));
+fun of_att x = (Scan.lift insts >> (fn args =>
+ Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args))) x;
end;
@@ -250,9 +250,8 @@
(* setup *)
val _ = Context.>> (Context.map_theory
- (Attrib.add_attributes
- [("where", where_att, "named instantiation of theorem"),
- ("of", of_att, "positional instantiation of theorem")]));
+ (Attrib.setup (Binding.name "where") where_att "named instantiation of theorem" #>
+ Attrib.setup (Binding.name "of") of_att "positional instantiation of theorem"));
--- a/src/Pure/ML/ml_antiquote.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Sun Mar 15 16:59:17 2009 +0100
@@ -59,9 +59,8 @@
structure P = OuterParse;
-val _ = inline "binding" (Scan.lift (P.position Args.name) >> (fn b =>
- ML_Syntax.atomic ("Binding.make " ^
- ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position b)));
+val _ = inline "binding"
+ (Scan.lift (P.position Args.name) >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
val _ = value "theory"
(Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)
--- a/src/Pure/ML/ml_syntax.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/Pure/ML/ml_syntax.ML Sun Mar 15 16:59:17 2009 +0100
@@ -20,6 +20,7 @@
val print_strings: string list -> string
val print_properties: Properties.T -> string
val print_position: Position.T -> string
+ val make_binding: string * Position.T -> string
val print_indexname: indexname -> string
val print_class: class -> string
val print_sort: sort -> string
@@ -72,6 +73,7 @@
val print_properties = print_list (print_pair print_string print_string);
fun print_position pos = "Position.of_properties " ^ print_properties (Position.properties_of pos);
+fun make_binding (name, pos) = "Binding.make " ^ print_pair print_string print_position (name, pos);
val print_indexname = print_pair print_string print_int;
--- a/src/Pure/Proof/extraction.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/Pure/Proof/extraction.ML Sun Mar 15 16:59:17 2009 +0100
@@ -374,8 +374,7 @@
val add_expand_thms = fold add_expand_thm;
-val extraction_expand =
- Attrib.no_args (Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm th) I));
+val extraction_expand = Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm th) I);
(** types with computational content **)
@@ -435,9 +434,8 @@
"(realizes (r) (!!x. PROP P (x))) == \
\ (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
- Attrib.add_attributes
- [("extraction_expand", extraction_expand,
- "specify theorems / definitions to be expanded during extraction")]));
+ Attrib.setup (Binding.name "extraction_expand") (Scan.succeed extraction_expand)
+ "specify theorems / definitions to be expanded during extraction"));
(**** extract program ****)
--- a/src/Pure/Tools/named_thms.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/Pure/Tools/named_thms.ML Sun Mar 15 16:59:17 2009 +0100
@@ -34,7 +34,7 @@
val del = Thm.declaration_attribute del_thm;
val setup =
- Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #>
+ Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
PureThy.add_thms_dynamic (Binding.name name, Data.get);
end;
--- a/src/Pure/simplifier.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/Pure/simplifier.ML Sun Mar 15 16:59:17 2009 +0100
@@ -334,11 +334,11 @@
in
-val simproc_att = Attrib.syntax
- (Scan.peek (fn context =>
+val simproc_att =
+ Scan.peek (fn context =>
add_del :|-- (fn decl =>
Scan.repeat1 (Args.named_attribute (decl o get_simproc context))
- >> (Library.apply o map Morphism.form))));
+ >> (Library.apply o map Morphism.form)));
end;
@@ -355,10 +355,10 @@
in
-val simplified =
- Attrib.syntax (conv_mode -- Attrib.thms >> (fn (f, ths) => Thm.rule_attribute (fn context =>
+val simplified = conv_mode -- Attrib.thms >>
+ (fn (f, ths) => Thm.rule_attribute (fn context =>
f ((if null ths then I else MetaSimplifier.clear_ss)
- (local_simpset_of (Context.proof_of context)) addsimps ths))));
+ (local_simpset_of (Context.proof_of context)) addsimps ths)));
end;
@@ -366,11 +366,12 @@
(* setup attributes *)
val _ = Context.>> (Context.map_theory
- (Attrib.add_attributes
- [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rewrite rule"),
- (congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"),
- ("simproc", simproc_att, "declaration of simplification procedures"),
- ("simplified", simplified, "simplified rule")]));
+ (Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del)
+ "declaration of Simplifier rewrite rule" #>
+ Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
+ "declaration of Simplifier congruence rule" #>
+ Attrib.setup (Binding.name "simproc") simproc_att "declaration of simplification procedures" #>
+ Attrib.setup (Binding.name "simplified") simplified "simplified rule"));
--- a/src/Tools/induct.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/Tools/induct.ML Sun Mar 15 16:59:17 2009 +0100
@@ -253,11 +253,11 @@
Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
Scan.lift (Args.$$$ k) >> K "";
-fun attrib add_type add_pred del = Attrib.syntax
- (spec typeN Args.tyname >> add_type ||
+fun attrib add_type add_pred del =
+ spec typeN Args.tyname >> add_type ||
spec predN Args.const >> add_pred ||
spec setN Args.const >> add_pred ||
- Scan.lift Args.del >> K del);
+ Scan.lift Args.del >> K del;
val cases_att = attrib cases_type cases_pred cases_del;
val induct_att = attrib induct_type induct_pred induct_del;
@@ -265,10 +265,10 @@
in
-val attrib_setup = Attrib.add_attributes
- [(casesN, cases_att, "declaration of cases rule"),
- (inductN, induct_att, "declaration of induction rule"),
- (coinductN, coinduct_att, "declaration of coinduction rule")];
+val attrib_setup =
+ Attrib.setup @{binding cases} cases_att "declaration of cases rule" #>
+ Attrib.setup @{binding induct} induct_att "declaration of induction rule" #>
+ Attrib.setup @{binding coinduct} coinduct_att "declaration of coinduction rule";
end;
--- a/src/ZF/Tools/typechk.ML Sat Mar 14 17:52:53 2009 +0100
+++ b/src/ZF/Tools/typechk.ML Sun Mar 15 16:59:17 2009 +0100
@@ -110,8 +110,6 @@
(* concrete syntax *)
-val TC_att = Attrib.add_del_args TC_add TC_del;
-
val typecheck_meth =
Method.only_sectioned_args
[Args.add -- Args.colon >> K (I, TC_add),
@@ -127,7 +125,7 @@
(* theory setup *)
val setup =
- Attrib.add_attributes [("TC", TC_att, "declaration of type-checking rule")] #>
+ Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #>
Simplifier.map_simpset (fn ss => ss setSolver type_solver);