--- a/src/Doc/Datatypes/Datatypes.thy Sun Sep 14 22:59:30 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 15 10:49:07 2014 +0200
@@ -753,7 +753,9 @@
\item[@{text "t."}\hthm{case} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.case(1)[no_vars]} \\
-@{thm list.case(2)[no_vars]}
+@{thm list.case(2)[no_vars]} \\
+(The @{text "[code]"} attribute is set by the @{text code} plugin,
+Section~\ref{ssec:code-generator}.)
\item[@{text "t."}\hthm{case_cong} @{text "[fundef_cong]"}\rm:] ~ \\
@{thm list.case_cong[no_vars]}
@@ -788,7 +790,9 @@
\item[@{text "t."}\hthm{sel} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.sel(1)[no_vars]} \\
-@{thm list.sel(2)[no_vars]}
+@{thm list.sel(2)[no_vars]} \\
+(The @{text "[code]"} attribute is set by the @{text code} plugin,
+Section~\ref{ssec:code-generator}.)
\item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rm:] ~ \\
@{thm list.collapse(1)[no_vars]} \\
@@ -829,7 +833,8 @@
\noindent
In addition, equational versions of @{text t.disc} are registered with the
-@{text "[code]"} attribute.
+@{text "[code]"} attribute. (The @{text "[code]"} attribute is set by the
+@{text code} plugin, Section~\ref{ssec:code-generator}.)
*}
@@ -857,7 +862,9 @@
\item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.set(1)[no_vars]} \\
-@{thm list.set(2)[no_vars]}
+@{thm list.set(2)[no_vars]} \\
+(The @{text "[code]"} attribute is set by the @{text code} plugin,
+Section~\ref{ssec:code-generator}.)
\item[@{text "t."}\hthm{set_cases} @{text "[consumes 1, cases set: set\<^sub>i_t]"}\rm:] ~ \\
@{thm list.set_cases[no_vars]}
@@ -871,7 +878,9 @@
\item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.map(1)[no_vars]} \\
-@{thm list.map(2)[no_vars]}
+@{thm list.map(2)[no_vars]} \\
+(The @{text "[code]"} attribute is set by the @{text code} plugin,
+Section~\ref{ssec:code-generator}.)
\item[@{text "t."}\hthm{map_disc_iff} @{text "[simp]"}\rm:] ~ \\
@{thm list.map_disc_iff[no_vars]}
@@ -903,7 +912,9 @@
\noindent
In addition, equational versions of @{text t.rel_inject} and @{text
-rel_distinct} are registered with the @{text "[code]"} attribute.
+rel_distinct} are registered with the @{text "[code]"} attribute. (The
+@{text "[code]"} attribute is set by the @{text code} plugin,
+Section~\ref{ssec:code-generator}.)
The second subgroup consists of more abstract properties of the set functions,
the map function, and the relator:
@@ -999,7 +1010,9 @@
\item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.rec(1)[no_vars]} \\
-@{thm list.rec(2)[no_vars]}
+@{thm list.rec(2)[no_vars]} \\
+(The @{text "[code]"} attribute is set by the @{text code} plugin,
+Section~\ref{ssec:code-generator}.)
\end{description}
\end{indentblock}
@@ -1804,7 +1817,9 @@
@{thm llist.corec(2)[no_vars]}
\item[@{text "t."}\hthm{corec_code} @{text "[code]"}\rm:] ~ \\
-@{thm llist.corec_code[no_vars]}
+@{thm llist.corec_code[no_vars]} \\
+(The @{text "[code]"} attribute is set by the @{text code} plugin,
+Section~\ref{ssec:code-generator}.)
\item[@{text "t."}\hthm{corec_disc}\rm:] ~ \\
@{thm llist.corec_disc(1)[no_vars]} \\
--- a/src/HOL/Extraction.thy Sun Sep 14 22:59:30 2014 +0200
+++ b/src/HOL/Extraction.thy Mon Sep 15 10:49:07 2014 +0200
@@ -37,7 +37,7 @@
induct_forall_def induct_implies_def induct_equal_def induct_conj_def
induct_true_def induct_false_def
-datatype (plugins only: code) sumbool = Left | Right
+datatype (plugins only:) sumbool = Left | Right
subsection {* Type of extracted program *}
--- a/src/HOL/Nitpick.thy Sun Sep 14 22:59:30 2014 +0200
+++ b/src/HOL/Nitpick.thy Mon Sep 15 10:49:07 2014 +0200
@@ -14,9 +14,9 @@
"nitpick_params" :: thy_decl
begin
-datatype (plugins only: code) (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
-datatype (plugins only: code) (dead 'a, dead 'b) pair_box = PairBox 'a 'b
-datatype (plugins only: code) (dead 'a) word = Word "'a set"
+datatype (plugins only:) (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
+datatype (plugins only:) (dead 'a, dead 'b) pair_box = PairBox 'a 'b
+datatype (plugins only:) (dead 'a) word = Word "'a set"
typedecl bisim_iterator
typedecl unsigned_bit
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Sep 14 22:59:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 15 10:49:07 2014 +0200
@@ -93,7 +93,7 @@
val mk_induct_attrs: term list list -> Token.src list
val mk_coinduct_attrs: typ list -> term list list -> term list list -> int list list ->
Token.src list * Token.src list
- val derive_induct_recs_thms_for_types: BNF_Def.bnf list ->
+ val derive_induct_recs_thms_for_types: (string -> bool) -> BNF_Def.bnf list ->
('a * typ list list list list * term list list * 'b) option -> thm -> thm list ->
BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list ->
typ list list list -> thm list -> thm list -> thm list -> term list list -> thm list list ->
@@ -311,7 +311,6 @@
val fundefcong_attrs = @{attributes [fundef_cong]};
val nitpicksimp_attrs = @{attributes [nitpick_simp]};
-val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
val simp_attrs = @{attributes [simp]};
val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
@@ -626,7 +625,7 @@
mk_induct_attrs ctrAss)
end;
-fun derive_induct_recs_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_rec_thms
+fun derive_induct_recs_thms_for_types plugins pre_bnfs rec_args_typess ctor_induct ctor_rec_thms
live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions
abs_inverses ctrss ctr_defss recs rec_defs lthy =
let
@@ -763,9 +762,11 @@
end;
val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms;
+
+ val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
in
((induct_thms, induct_thm, mk_induct_attrs ctrss),
- (rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
+ (rec_thmss, code_attrs @ nitpicksimp_attrs @ simp_attrs))
end;
fun mk_coinduct_attrs fpTs ctrss discss mss =
@@ -1364,6 +1365,8 @@
fp_b_names fpTs thmss)
#> filter_out (null o fst o hd o snd);
+ val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
+
val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss;
val ns = map length ctr_Tsss;
val kss = map (fn n => 1 upto n) ns;
@@ -1923,14 +1926,14 @@
end;
val anonymous_notes =
- [(rel_eq_thms, code_nitpicksimp_attrs)]
+ [(rel_eq_thms, code_attrs @ nitpicksimp_attrs)]
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
val notes =
[(case_transferN, [case_transfer_thms], K []),
(ctr_transferN, ctr_transfer_thms, K []),
(disc_transferN, disc_transfer_thms, K []),
- (mapN, map_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
+ (mapN, map_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)),
(map_disc_iffN, map_disc_iff_thms, K simp_attrs),
(map_selN, map_sel_thms, K []),
(rel_casesN, [rel_cases_thm], K rel_cases_attrs),
@@ -1938,7 +1941,7 @@
(rel_injectN, rel_inject_thms, K simp_attrs),
(rel_introsN, rel_intro_thms, K []),
(rel_selN, rel_sel_thms, K []),
- (setN, set_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
+ (setN, set_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)),
(set_casesN, set_cases_thms, nth set_cases_attrss),
(set_introsN, set_intros_thms, K []),
(set_selN, set_sel_thms, K [])]
@@ -1985,9 +1988,9 @@
(recs, rec_defs)), lthy) =
let
val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) =
- derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct xtor_co_rec_thms
- live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses type_definitions
- abs_inverses ctrss ctr_defss recs rec_defs lthy;
+ derive_induct_recs_thms_for_types plugins pre_bnfs recs_args_types xtor_co_induct
+ xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses
+ type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy;
val induct_type_attr = Attrib.internal o K o Induct.induct_type;
val induct_pred_attr = Attrib.internal o K o Induct.induct_pred;
@@ -2111,7 +2114,7 @@
fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
(coinduct_strongN, map single coinduct_strong_thms, K coinduct_attrs),
(corecN, corec_thmss, K []),
- (corec_codeN, map single corec_code_thms, K code_nitpicksimp_attrs),
+ (corec_codeN, map single corec_code_thms, K (code_attrs @ nitpicksimp_attrs)),
(corec_discN, corec_disc_thmss, K []),
(corec_disc_iffN, corec_disc_iff_thmss, K corec_disc_iff_attrs),
(corec_selN, corec_sel_thmss, K corec_sel_attrs),
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Sun Sep 14 22:59:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Sep 15 10:49:07 2014 +0200
@@ -11,13 +11,14 @@
val unfold_splits_lets: term -> term
val dest_map: Proof.context -> string -> term -> term * term list
- val mutualize_fp_sugars: BNF_Util.fp_kind -> int list -> binding list -> typ list -> term list ->
- term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory ->
+ val mutualize_fp_sugars: (string -> bool) -> BNF_Util.fp_kind -> int list -> binding list ->
+ typ list -> term list -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list ->
+ local_theory ->
(BNF_FP_Def_Sugar.fp_sugar list
* (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
* local_theory
- val nested_to_mutual_fps: BNF_Util.fp_kind -> binding list -> typ list -> term list ->
- (term * term list list) list list -> local_theory ->
+ val nested_to_mutual_fps: (string -> bool) -> BNF_Util.fp_kind -> binding list -> typ list ->
+ term list -> (term * term list list) list list -> local_theory ->
(typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
* (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
* local_theory
@@ -116,7 +117,7 @@
|> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
|> map_filter I;
-fun mutualize_fp_sugars fp cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy =
+fun mutualize_fp_sugars plugins fp cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy =
let
val thy = Proof_Context.theory_of no_defs_lthy;
@@ -269,7 +270,7 @@
val ((common_co_inducts, co_inductss', co_rec_thmss, co_rec_disc_thmss, co_rec_sel_thmsss),
fp_sugar_thms) =
if fp = Least_FP then
- derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
+ derive_induct_recs_thms_for_types plugins pre_bnfs recs_args_types xtor_co_induct
xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs
lthy
@@ -332,7 +333,7 @@
val impossible_caller = Bound ~1;
-fun nested_to_mutual_fps fp actual_bs actual_Ts actual_callers actual_callssss0 lthy =
+fun nested_to_mutual_fps plugins fp actual_bs actual_Ts actual_callers actual_callssss0 lthy =
let
val qsoty = quote o Syntax.string_of_typ lthy;
val qsotys = space_implode " or " o map qsoty;
@@ -456,8 +457,8 @@
if length perm_Tss = 1 then
((perm_fp_sugars0, (NONE, NONE)), lthy)
else
- mutualize_fp_sugars fp perm_cliques perm_bs perm_frozen_gen_Ts perm_callers perm_callssss
- perm_fp_sugars0 lthy;
+ mutualize_fp_sugars plugins fp perm_cliques perm_bs perm_frozen_gen_Ts perm_callers
+ perm_callssss perm_fp_sugars0 lthy;
val fp_sugars = unpermute perm_fp_sugars;
in
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sun Sep 14 22:59:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Sep 15 10:49:07 2014 +0200
@@ -409,7 +409,7 @@
val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs,
common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
- nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
+ nested_to_mutual_fps (K true) Greatest_FP bs res_Ts callers callssss0 lthy0;
val coinduct_attrs_pair =
(case gfp_sugar_thms of SOME ((_, attrs_pair), _, _, _, _) => attrs_pair | NONE => ([], []));
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Sun Sep 14 22:59:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 15 10:49:07 2014 +0200
@@ -286,7 +286,8 @@
val ((fp_sugars', (lfp_sugar_thms', _)), lthy') =
if nn > nn_fp then
- mutualize_fp_sugars Least_FP cliques compat_bs fpTs' callers callssss fp_sugars lthy
+ mutualize_fp_sugars (K true) Least_FP cliques compat_bs fpTs' callers callssss fp_sugars
+ lthy
else
((fp_sugars, (NONE, NONE)), lthy);
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Sun Sep 14 22:59:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Mon Sep 15 10:49:07 2014 +0200
@@ -31,7 +31,7 @@
val ((missing_arg_Ts, perm0_kks,
fp_sugars as {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _,
(lfp_sugar_thms, _)), lthy) =
- nested_to_mutual_fps Least_FP bs arg_Ts callers callssss0 lthy0;
+ nested_to_mutual_fps (K true) Least_FP bs arg_Ts callers callssss0 lthy0;
val induct_attrs = (case lfp_sugar_thms of SOME ((_, _, attrs), _) => attrs | NONE => []);
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Sun Sep 14 22:59:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Sep 15 10:49:07 2014 +0200
@@ -32,7 +32,6 @@
val nitpicksimp_attrs = @{attributes [nitpick_simp]};
val simp_attrs = @{attributes [simp]};
-val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs @ simp_attrs;
structure Data = Generic_Data
(
@@ -346,6 +345,9 @@
(map single rec_o_map_thms, size_o_map_thmss)
end;
+ (* Ideally, the "[code]" attribute would be generated only if the "code" plugin is enabled. *)
+ val code_attrs = Code.add_default_eqn_attrib;
+
val massage_multi_notes =
maps (fn (thmN, thmss, attrs) =>
map2 (fn T_name => fn thms =>
@@ -356,7 +358,7 @@
val notes =
[(rec_o_mapN, rec_o_map_thmss, []),
- (sizeN, size_thmss, code_nitpicksimp_simp_attrs),
+ (sizeN, size_thmss, code_attrs :: nitpicksimp_attrs @ simp_attrs),
(size_o_mapN, size_o_map_thmss, [])]
|> massage_multi_notes;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sun Sep 14 22:59:30 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Sep 15 10:49:07 2014 +0200
@@ -91,7 +91,7 @@
open Ctr_Sugar_Tactics
open Ctr_Sugar_Code
-val code_plugin = "code"
+val code_plugin = "code";
type ctr_sugar =
{T: typ,
@@ -250,8 +250,6 @@
val inductsimp_attrs = @{attributes [induct_simp]};
val nitpicksimp_attrs = @{attributes [nitpick_simp]};
val simp_attrs = @{attributes [simp]};
-val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
-val code_nitpicksimp_simp_attrs = code_nitpicksimp_attrs @ simp_attrs;
fun unflat_lookup eq xs ys = map (fn xs' => permute_like_unique eq xs xs' ys);
@@ -978,17 +976,19 @@
val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
+ val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
+
val nontriv_disc_eq_thmss =
map (map (fn th => th RS @{thm eq_False[THEN iffD2]}
handle THM _ => th RS @{thm eq_True[THEN iffD2]})) nontriv_disc_thmss;
val anonymous_notes =
[(map (fn th => th RS notE) distinct_thms, safe_elim_attrs),
- (flat nontriv_disc_eq_thmss, code_nitpicksimp_attrs)]
+ (flat nontriv_disc_eq_thmss, code_attrs @ nitpicksimp_attrs)]
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
val notes =
- [(caseN, case_thms, code_nitpicksimp_simp_attrs),
+ [(caseN, case_thms, code_attrs @ nitpicksimp_attrs @ simp_attrs),
(case_congN, [case_cong_thm], []),
(case_cong_weak_thmsN, [case_cong_weak_thm], cong_attrs),
(case_eq_ifN, case_eq_if_thms, []),
@@ -1003,7 +1003,7 @@
(expandN, expand_thms, []),
(injectN, inject_thms, iff_attrs @ inductsimp_attrs),
(nchotomyN, [nchotomy_thm], []),
- (selN, all_sel_thms, code_nitpicksimp_simp_attrs),
+ (selN, all_sel_thms, code_attrs @ nitpicksimp_attrs @ simp_attrs),
(splitN, [split_thm], []),
(split_asmN, [split_asm_thm], []),
(split_selN, split_sel_thms, []),
@@ -1022,16 +1022,16 @@
|> fold (Spec_Rules.add Spec_Rules.Equational)
(filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
|> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Case_Translation.register
- (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
+ (fn phi => Case_Translation.register
+ (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
|> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs])
|> plugins code_plugin ?
- Local_Theory.declaration {syntax = false, pervasive = false}
- (fn phi => Context.mapping
- (add_ctr_code fcT_name (map (Morphism.typ phi) As)
- (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
- (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
- I)
+ Local_Theory.declaration {syntax = false, pervasive = false}
+ (fn phi => Context.mapping
+ (add_ctr_code fcT_name (map (Morphism.typ phi) As)
+ (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
+ (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
+ I)
|> Local_Theory.notes (anonymous_notes @ notes)
(* for "datatype_realizer.ML": *)
|>> name_noted_thms fcT_name exhaustN;