# HG changeset patch # User blanchet # Date 1410770947 -7200 # Node ID a5a3b576fcfb8978fcd9de65eae64b9ffabbca26 # Parent 7553a1bcecb7df2fa48ed4db8db34dcc2dcfa184 generate 'code' attribute only if 'code' plugin is enabled diff -r 7553a1bcecb7 -r a5a3b576fcfb src/Doc/Datatypes/Datatypes.thy --- 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]} \\ diff -r 7553a1bcecb7 -r a5a3b576fcfb src/HOL/Extraction.thy --- 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 *} diff -r 7553a1bcecb7 -r a5a3b576fcfb src/HOL/Nitpick.thy --- 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 \ '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 \ '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 diff -r 7553a1bcecb7 -r a5a3b576fcfb src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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), diff -r 7553a1bcecb7 -r a5a3b576fcfb src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- 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 diff -r 7553a1bcecb7 -r a5a3b576fcfb src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- 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 => ([], [])); diff -r 7553a1bcecb7 -r a5a3b576fcfb src/HOL/Tools/BNF/bnf_lfp_compat.ML --- 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); diff -r 7553a1bcecb7 -r a5a3b576fcfb src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- 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 => []); diff -r 7553a1bcecb7 -r a5a3b576fcfb src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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; diff -r 7553a1bcecb7 -r a5a3b576fcfb src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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;