# HG changeset patch # User blanchet # Date 1420489454 -3600 # Node ID 5ca195783da869c5c12f111655a662a1ae6c4a97 # Parent c5f6e2c4472cfd619fc99f13220b7a6679f7cd35 generate [code] only with 'code' plugin enabled diff -r c5f6e2c4472c -r 5ca195783da8 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Jan 05 11:00:12 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Jan 05 21:24:14 2015 +0100 @@ -1020,7 +1020,7 @@ |> map Thm.close_derivation) end; - val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else []; + val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else []; val anonymous_notes = [(rel_code_thms, code_attrs @ nitpicksimp_attrs)] @@ -1455,7 +1455,7 @@ val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms; - val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else []; + 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_attrs @ nitpicksimp_attrs @ simp_attrs)) @@ -2081,7 +2081,7 @@ val fpTs = map (domain_type o fastype_of) dtors; val fpBTs = map B_ify_T fpTs; - val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else []; + 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; diff -r c5f6e2c4472c -r 5ca195783da8 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Jan 05 11:00:12 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Jan 05 21:24:14 2015 +0100 @@ -83,7 +83,6 @@ val nitpicksimp_attrs = @{attributes [nitpick_simp]}; val simp_attrs = @{attributes [simp]}; -val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs; exception PRIMCOREC of string * term list; @@ -1413,6 +1412,8 @@ val common_name = mk_common_name fun_names; + val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else []; + val anonymous_notes = [(flat disc_iff_or_disc_thmss, simp_attrs)] |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); @@ -1428,7 +1429,7 @@ [(coinductN, map (if n2m then single else K []) coinduct_thms, coinduct_attrs), (coinduct_strongN, map (if n2m then single else K []) coinduct_strong_thms, coinduct_attrs), - (codeN, code_thmss, code_nitpicksimp_attrs), + (codeN, code_thmss, code_attrs @ nitpicksimp_attrs), (ctrN, ctr_thmss, []), (discN, disc_thmss, []), (disc_iffN, disc_iff_thmss, []), diff -r c5f6e2c4472c -r 5ca195783da8 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Jan 05 11:00:12 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Jan 05 21:24:14 2015 +0100 @@ -89,7 +89,7 @@ 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; +val nitpicksimp_simp_attrs = nitpicksimp_attrs @ simp_attrs; exception OLD_PRIMREC of unit; exception PRIMREC of string * term list; @@ -438,7 +438,7 @@ else warning ("no equation for constructor " ^ Syntax.string_of_term ctxt ctr)); val ctr_spec_eqn_data_list = - map (fn ((x, y), z) => (x, z)) ctr_spec_eqn_data_list' @ + map (apfst fst) ctr_spec_eqn_data_list' @ (drop n_funs rec_specs |> maps #ctr_specs |> map (rpair [])); val recs = take n_funs rec_specs |> map #recx; @@ -548,13 +548,12 @@ val simp_thms = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs |> fst |> map_filter (try (fn (x, [y]) => - (#fun_name x, #user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y))) - |> map2 (fn j => fn (fun_name, user_eqn, num_extra_args, rec_thm) => + (#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y))) + |> map (fn (user_eqn, num_extra_args, rec_thm) => mk_primrec_tac lthy' num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps def_thms rec_thm |> K |> Goal.prove_sorry lthy' [] [] user_eqn - |> Thm.close_derivation) - js; + |> Thm.close_derivation); in ((js, simp_thms), lthy') end; @@ -591,14 +590,12 @@ lthy |> Local_Theory.notes (notes @ common_notes) |> snd) end; -fun add_primrec_simple' opts fixes ts lthy = +fun add_primrec_simple0 plugins nonexhaustive transfer fixes ts lthy = let val actual_nn = length fixes; - val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts) - |> the_default Plugin_Name.default_filter; - val nonexhaustives = replicate actual_nn (exists (can (fn Nonexhaustive_Option => ())) opts); - val transfers = replicate actual_nn (exists (can (fn Transfer_Option => ())) opts); + val nonexhaustives = replicate actual_nn nonexhaustive; + val transfers = replicate actual_nn transfer; val (((names, defs), prove), lthy') = prepare_primrec plugins nonexhaustives transfers fixes ts lthy @@ -618,7 +615,7 @@ space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns)); fun add_primrec_simple fixes ts lthy = - add_primrec_simple' [] fixes ts lthy + add_primrec_simple0 Plugin_Name.default_filter false false fixes ts lthy handle OLD_PRIMREC () => Old_Primrec.add_primrec_simple fixes ts lthy |>> apsnd (apsnd (pair [] o single)) o apfst single; @@ -626,9 +623,16 @@ fun gen_primrec old_primrec prep_spec opts (raw_fixes : (binding * 'a option * mixfix) list) raw_specs lthy = let - val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes) + val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes); val _ = null d orelse raise PRIMREC ("duplicate function name(s): " ^ commas d, []); + val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts) + |> the_default Plugin_Name.default_filter; + val nonexhaustive = exists (can (fn Nonexhaustive_Option => ())) opts; + val transfer = exists (can (fn Transfer_Option => ())) opts; + + val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else []; + val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy); val mk_notes = @@ -637,7 +641,7 @@ val (bs, attrss) = map_split (fst o nth specs) js; val notes = @{map 3} (fn b => fn attrs => fn thm => - ((Binding.qualify false prefix b, code_nitpicksimp_simp_attrs @ attrs), + ((Binding.qualify false prefix b, code_attrs @ nitpicksimp_simp_attrs @ attrs), [([thm], [])])) bs attrss thms; in @@ -645,7 +649,7 @@ end); in lthy - |> add_primrec_simple' opts fixes (map snd specs) + |> add_primrec_simple0 plugins nonexhaustive transfer fixes (map snd specs) |-> (fn (names, (ts, (jss, simpss))) => Spec_Rules.add Spec_Rules.Equational (ts, flat simpss) #> Local_Theory.notes (mk_notes jss names simpss) diff -r c5f6e2c4472c -r 5ca195783da8 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Jan 05 11:00:12 2015 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Jan 05 21:24:14 2015 +0100 @@ -75,6 +75,8 @@ val ctr_of_ctr_spec: ('c, 'a) ctr_spec -> 'c val args_of_ctr_spec: ('c, 'a) ctr_spec -> 'a list + val code_plugin: string + type ctr_options = (string -> bool) * bool type ctr_options_cmd = (Proof.context -> string -> bool) * bool