# HG changeset patch # User haftmann # Date 1465241326 -7200 # Node ID d562c9948deec004145b39be77b8397d3eb3047a # Parent 7c593d4f1f8944e56a406bf749f944391492157c explicit tagging of code equations de-baroquifies interface diff -r 7c593d4f1f89 -r d562c9948dee src/Doc/Codegen/Further.thy --- a/src/Doc/Codegen/Further.thy Mon Jun 06 21:28:45 2016 +0200 +++ b/src/Doc/Codegen/Further.thy Mon Jun 06 21:28:46 2016 +0200 @@ -242,7 +242,7 @@ text %mlref \ \begin{mldecls} @{index_ML Code.read_const: "theory -> string -> string"} \\ - @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\ + @{index_ML Code.add_eqn: "Code.kind * bool -> thm -> theory -> theory"} \\ @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\ @{index_ML Code_Preproc.map_pre: "(Proof.context -> Proof.context) -> theory -> theory"} \\ @{index_ML Code_Preproc.map_post: "(Proof.context -> Proof.context) -> theory -> theory"} \\ @@ -261,11 +261,11 @@ \item @{ML Code.read_const}~@{text thy}~@{text s} reads a constant as a concrete term expression @{text s}. - \item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function - theorem @{text "thm"} to executable content. + \item @{ML Code.add_eqn}~@{text "(kind, default)"}~@{text "thm"}~@{text "thy"} adds code equation + @{text "thm"} to executable content. - \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes function - theorem @{text "thm"} from executable content, if present. + \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes code equation + @{text "thm"} from executable content, if present. \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes the preprocessor simpset. diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Library/Mapping.thy --- a/src/HOL/Library/Mapping.thy Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Library/Mapping.thy Mon Jun 06 21:28:46 2016 +0200 @@ -121,7 +121,7 @@ definition "lookup_default d m k = (case Mapping.lookup m k of None \ d | Some v \ v)" declare [[code drop: Mapping.lookup]] -setup \Code.add_default_eqn @{thm Mapping.lookup.abs_eq}\ \ \FIXME lifting\ +setup \Code.add_eqn (Code.Equation, true) @{thm Mapping.lookup.abs_eq}\ \ \FIXME lifting\ lift_definition update :: "'a \ 'b \ ('a, 'b) mapping \ ('a, 'b) mapping" is "\k v m. m(k \ v)" parametric update_parametric . diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Library/old_recdef.ML --- a/src/HOL/Library/old_recdef.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Library/old_recdef.ML Mon Jun 06 21:28:46 2016 +0200 @@ -2834,7 +2834,7 @@ val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx); val simp_att = if null tcs then [Simplifier.simp_add, - Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute] + Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute Code.Equation] else []; val ((simps' :: rules', [induct']), thy2) = Proof_Context.theory_of ctxt1 diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Jun 06 21:28:46 2016 +0200 @@ -1146,7 +1146,7 @@ |> Proof_Context.export names_lthy lthy end; - val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else []; + val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else []; val anonymous_notes = [(rel_code_thms, code_attrs @ nitpicksimp_attrs)] @@ -1577,7 +1577,7 @@ 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 []; + val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else []; in ((induct_thms, induct_thm, mk_induct_attrs ctrss), (rec_thmss, code_attrs @ nitpicksimp_attrs @ simp_attrs)) @@ -2234,7 +2234,7 @@ val fpTs = map (domain_type o fastype_of) dtors; val fpBTs = map B_ify_T fpTs; - val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else []; + val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else []; val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss; val ns = map length ctr_Tsss; diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon Jun 06 21:28:46 2016 +0200 @@ -2147,7 +2147,7 @@ |> derive_and_update_coinduct_cong_intross [corec_info]; val cong_intros_pairs = AList.group (op =) cong_intro_pairs; - val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else []; + val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else []; val anonymous_notes = []; (* TODO: diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Jun 06 21:28:46 2016 +0200 @@ -1522,7 +1522,7 @@ val common_name = mk_common_name fun_names; val common_qualify = fold_rev I qualifys; - val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else []; + val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else []; val anonymous_notes = [(flat disc_iff_or_disc_thmss, simp_attrs)] diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Jun 06 21:28:46 2016 +0200 @@ -455,7 +455,7 @@ Old_Datatype_Data.interpretation (old_interpretation_of prefs f) #> fp_sugars_interpretation name (Local_Theory.background_theory o new_interpretation_of prefs f); -val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]}; +val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib Code.Equation :: @{attributes [nitpick_simp, simp]}; fun datatype_compat fpT_names lthy = let diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Jun 06 21:28:46 2016 +0200 @@ -638,7 +638,7 @@ 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 code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else []; val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy); diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Jun 06 21:28:46 2016 +0200 @@ -354,7 +354,7 @@ end; (* Ideally, the "[code]" attribute would be generated only if the "code" plugin is enabled. *) - val code_attrs = Code.add_default_eqn_attrib; + val code_attrs = Code.add_default_eqn_attrib Code.Equation; val massage_multi_notes = maps (fn (thmN, thmss, attrs) => diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Jun 06 21:28:46 2016 +0200 @@ -1068,7 +1068,7 @@ 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 code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else []; val nontriv_disc_eq_thmss = map (map (fn th => th RS @{thm eq_False[THEN iffD2]} diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Mon Jun 06 21:28:46 2016 +0200 @@ -112,8 +112,8 @@ #-> fold Code.del_eqn #> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms) #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.theoremK - [((qualify reflN, [Code.add_nbe_default_eqn_attribute]), [([thm], [])]), - ((qualify simpsN, [Code.add_default_eqn_attribute]), [(rev thms, [])])]) + [((qualify reflN, [Code.add_default_eqn_attribute Code.Nbe]), [([thm], [])]), + ((qualify simpsN, [Code.add_default_eqn_attribute Code.Equation]), [(rev thms, [])])]) #> snd end; @@ -127,7 +127,7 @@ if can (Code.constrset_of_consts thy) unover_ctrs then thy |> Code.add_datatype ctrs - |> fold_rev Code.add_default_eqn case_thms + |> fold_rev (Code.add_eqn (Code.Equation, true)) case_thms |> Code.add_case (mk_case_certificate (Proof_Context.init_global thy) case_thms) |> not (Sorts.has_instance (Sign.classes_of thy) fcT_name [HOLogic.class_equal]) ? add_equality fcT fcT_name As ctrs inject_thms distinct_thms diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/Function/function.ML Mon Jun 06 21:28:46 2016 +0200 @@ -45,7 +45,7 @@ open Function_Common val simp_attribs = - @{attributes [simp, nitpick_simp]} @ [Attrib.internal (K Code.add_default_eqn_attribute)] + @{attributes [simp, nitpick_simp]} @ [Code.add_default_eqn_attrib Code.Equation] val psimp_attribs = @{attributes [nitpick_psimp]} diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Mon Jun 06 21:28:46 2016 +0200 @@ -451,17 +451,17 @@ in if is_valid_eq abs_eq_thm then - (ABS_EQ, Code.add_default_eqn abs_eq_thm thy) + (ABS_EQ, Code.add_eqn (Code.Equation, true) abs_eq_thm thy) else let val (rty_body, qty_body) = get_body_types (rty, qty) in if rty_body = qty_body then - (REP_EQ, Code.add_default_eqn (the opt_rep_eq_thm) thy) + (REP_EQ, Code.add_eqn (Code.Equation, true) (the opt_rep_eq_thm) thy) else if is_some opt_rep_eq_thm andalso is_valid_abs_eq (the opt_rep_eq_thm) then - (REP_EQ, Code.add_abs_default_eqn (the opt_rep_eq_thm) thy) + (REP_EQ, Code.add_eqn (Code.Abstract, true) (the opt_rep_eq_thm) thy) else (NONE_EQ, thy) end diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/Old_Datatype/old_primrec.ML --- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Mon Jun 06 21:28:46 2016 +0200 @@ -275,7 +275,7 @@ let val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy); fun attr_bindings prefix = map (fn ((b, attrs), _) => - (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec; + (Binding.qualify false prefix b, Code.add_default_eqn_attrib Code.Equation :: attrs)) spec; fun simp_attr_binding prefix = (Binding.qualify true prefix (Binding.name "simps"), @{attributes [simp, nitpick_simp]}); in diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/Old_Datatype/old_rep_datatype.ML --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Mon Jun 06 21:28:46 2016 +0200 @@ -570,7 +570,7 @@ ((prfx (Binding.name "splits"), []), [(maps (fn (x, y) => [x, y]) splits, [])]), ((Binding.empty, [Simplifier.simp_add]), [(flat case_rewrites @ flat distinct @ rec_rewrites, [])]), - ((Binding.empty, [Code.add_default_eqn_attribute]), [(rec_rewrites, [])]), + ((Binding.empty, [Code.add_default_eqn_attribute Code.Equation]), [(rec_rewrites, [])]), ((Binding.empty, [iff_add]), [(flat inject, [])]), ((Binding.empty, [Classical.safe_elim NONE]), [(map (fn th => th RS notE) (flat distinct), [])]), diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/Old_Datatype/old_size.ML --- a/src/HOL/Tools/Old_Datatype/old_size.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/Old_Datatype/old_size.ML Mon Jun 06 21:28:46 2016 +0200 @@ -196,8 +196,7 @@ |> Global_Theory.note_thmss "" [((Binding.name "size", [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp}, - Thm.declaration_attribute (fn thm => - Context.mapping (Code.add_default_eqn thm) I)]), + Code.add_default_eqn_attribute Code.Equation]), [(size_eqns, [])])]; in diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Jun 06 21:28:46 2016 +0200 @@ -1421,7 +1421,9 @@ val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds (maps_modes result_thms) val qname = #qname (dest_steps steps) - val attrib = Thm.declaration_attribute (fn thm => Context.mapping (Code.add_eqn thm) I) + val attrib = Thm.declaration_attribute (fn thm => Context.mapping + (Code.add_eqn (Code.Equation, false) thm) I) + (*FIXME default code equation!?*) val thy''' = cond_timeit (Config.get ctxt Quickcheck.timing) "Setting code equations...." (fn _ => fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Jun 06 21:28:46 2016 +0200 @@ -111,7 +111,7 @@ in thy |> Code.del_eqns const - |> fold Code.add_eqn eqs + |> fold (Code.add_eqn (Code.Equation, false)) eqs (*FIXME default code equation!?*) end fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy = diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Jun 06 21:28:46 2016 +0200 @@ -385,7 +385,7 @@ fold (fn (name, eq) => Local_Theory.note ((Binding.qualify true prfx (Binding.qualify true name (Binding.name "simps")), - [Code.add_default_eqn_attrib]), [eq]) #> snd) + [Code.add_default_eqn_attrib Code.Equation]), [eq]) #> snd) (names ~~ eqs) lthy end) diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Mon Jun 06 21:28:46 2016 +0200 @@ -179,7 +179,7 @@ |> random_aux_primrec_multi (name ^ prfx) proto_eqs |-> prove_simps |-> (fn simps => Local_Theory.note - ((b, Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), simps)) + ((b, Code.add_default_eqn_attrib Code.Equation:: @{attributes [simp, nitpick_simp]}), simps)) |> snd end diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/code_evaluation.ML --- a/src/HOL/Tools/code_evaluation.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/code_evaluation.ML Mon Jun 06 21:28:46 2016 +0200 @@ -93,7 +93,7 @@ in thy |> Code.del_eqns const - |> fold Code.add_eqn eqs + |> fold (Code.add_eqn (Code.Equation, false)) eqs end; fun ensure_term_of_code (tyco, (vs, cs)) = @@ -125,7 +125,7 @@ in thy |> Code.del_eqns const - |> Code.add_eqn eq + |> Code.add_eqn (Code.Equation, false) eq end; fun ensure_abs_term_of_code (tyco, (vs, ((abs, (_, ty)), (proj, _)))) = diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/HOL/Tools/record.ML Mon Jun 06 21:28:46 2016 +0200 @@ -1778,7 +1778,7 @@ in thy |> Code.add_datatype [ext] - |> fold Code.add_default_eqn simps + |> fold (Code.add_eqn (Code.Equation, true)) simps |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal]) |> `(fn lthy => Syntax.check_term lthy eq) |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq)) @@ -1787,8 +1787,8 @@ |-> (fn eq_def => fn thy => thy |> Code.del_eqn eq_def - |> Code.add_default_eqn (mk_eq (Proof_Context.init_global thy) eq_def)) - |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl (Proof_Context.init_global thy)) thy) + |> Code.add_eqn (Code.Equation, true) (mk_eq (Proof_Context.init_global thy) eq_def)) + |> (fn thy => Code.add_eqn (Code.Nbe, true) (mk_eq_refl (Proof_Context.init_global thy)) thy) |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext)) |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext)) end @@ -2045,7 +2045,7 @@ ||>> (Global_Theory.add_defs false o map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) upd_specs ||>> (Global_Theory.add_defs false o - map (rpair [Code.add_default_eqn_attribute] + map (rpair [Code.add_default_eqn_attribute Code.Equation] o apfst (Binding.concealed o Binding.name))) [make_spec, fields_spec, extend_spec, truncate_spec]); val defs_ctxt = Proof_Context.init_global defs_thy; diff -r 7c593d4f1f89 -r d562c9948dee src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/Pure/Isar/code.ML Mon Jun 06 21:28:46 2016 +0200 @@ -46,18 +46,13 @@ val abstype_interpretation: (string * ((string * sort) list * ((string * ((string * sort) list * typ)) * (string * thm))) -> theory -> theory) -> theory -> theory - val add_eqn: thm -> theory -> theory - val add_nbe_eqn: thm -> theory -> theory - val add_abs_eqn: thm -> theory -> theory - val add_default_eqn: thm -> theory -> theory - val add_default_eqn_attribute: attribute - val add_default_eqn_attrib: Token.src - val add_nbe_default_eqn: thm -> theory -> theory - val add_nbe_default_eqn_attribute: attribute - val add_nbe_default_eqn_attrib: Token.src - val add_abs_default_eqn: thm -> theory -> theory - val add_abs_default_eqn_attribute: attribute - val add_abs_default_eqn_attrib: Token.src + type kind + val Equation: kind + val Nbe: kind + val Abstract: kind + val add_eqn: kind * bool -> thm -> theory -> theory + val add_default_eqn_attribute: kind -> attribute + val add_default_eqn_attrib: kind -> Token.src val del_eqn: thm -> theory -> theory val del_eqns: string -> theory -> theory val del_exception: string -> theory -> theory @@ -1073,6 +1068,14 @@ (* code equations *) +(* + external distinction: + kind * default + processual distinction: + thm * proper for concrete equations + thm for abstract equations +*) + fun gen_add_eqn default (raw_thm, proper) thy = let val thm = Thm.close_derivation raw_thm; @@ -1112,34 +1115,25 @@ val c = const_abs_eqn thy abs_thm; in change_fun_spec c (K (Abstr ((abs_thm, tyco), default))) thy end; -fun add_eqn thm thy = - gen_add_eqn false (mk_eqn thy (thm, true)) thy; - -fun add_nbe_eqn thm thy = - gen_add_eqn false (mk_eqn thy (thm, false)) thy; - -fun add_default_eqn thm thy = - case mk_eqn_liberal thy thm - of SOME eqn => gen_add_eqn true eqn thy - | NONE => thy; +datatype kind = Equation | Nbe | Abstract; -val add_default_eqn_attribute = Thm.declaration_attribute - (fn thm => Context.mapping (add_default_eqn thm) I); -val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute); - -fun add_nbe_default_eqn thm thy = - gen_add_eqn true (mk_eqn thy (thm, false)) thy; +fun add_eqn (kind, default) thm thy = + case (kind, default) of + (Equation, true) => (case mk_eqn_liberal thy thm of + SOME eqn => gen_add_eqn true eqn thy + | NONE => thy) + | (Equation, false) => gen_add_eqn false (mk_eqn thy (thm, true)) thy + | (Nbe, _) => gen_add_eqn default (mk_eqn thy (thm, false)) thy + | (Abstract, _) => gen_add_abs_eqn default (mk_abs_eqn thy thm) thy; -val add_nbe_default_eqn_attribute = Thm.declaration_attribute - (fn thm => Context.mapping (add_nbe_default_eqn thm) I); -val add_nbe_default_eqn_attrib = Attrib.internal (K add_nbe_default_eqn_attribute); +fun lift_attribute f = Thm.declaration_attribute + (fn thm => Context.mapping (f thm) I); -fun add_abs_eqn raw_thm thy = gen_add_abs_eqn false (mk_abs_eqn thy raw_thm) thy; -fun add_abs_default_eqn raw_thm thy = gen_add_abs_eqn true (mk_abs_eqn thy raw_thm) thy; +fun add_default_eqn_attribute kind = + lift_attribute (add_eqn (kind, true)); -val add_abs_default_eqn_attribute = Thm.declaration_attribute - (fn thm => Context.mapping (add_abs_default_eqn thm) I); -val add_abs_default_eqn_attrib = Attrib.internal (K add_abs_default_eqn_attribute); +fun add_default_eqn_attrib kind = + Attrib.internal (K (add_default_eqn_attribute kind)); fun add_eqn_maybe_abs thm thy = case mk_eqn_maybe_abs thy thm @@ -1297,18 +1291,17 @@ val _ = Theory.setup (let - fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); - fun mk_const_attribute f cs = - mk_attribute (K (fold (fn c => fn thy => f (read_const thy c) thy) cs)); + fun lift_const_attribute f cs = + lift_attribute (K (fold (fn c => fn thy => f (read_const thy c) thy) cs)); val code_attribute_parser = - Args.$$$ "equation" |-- Scan.succeed (mk_attribute add_eqn) - || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn) - || Args.$$$ "abstype" |-- Scan.succeed (mk_attribute add_abstype) - || Args.$$$ "abstract" |-- Scan.succeed (mk_attribute add_abs_eqn) - || Args.del |-- Scan.succeed (mk_attribute del_eqn) - || Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term >> mk_const_attribute del_eqns) - || Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term >> mk_const_attribute del_exception) - || Scan.succeed (mk_attribute add_eqn_maybe_abs); + Args.$$$ "equation" |-- Scan.succeed (lift_attribute (add_eqn (Equation, false))) + || Args.$$$ "nbe" |-- Scan.succeed (lift_attribute (add_eqn (Nbe, false))) + || Args.$$$ "abstract" |-- Scan.succeed (lift_attribute (add_eqn (Abstract, false))) + || Args.$$$ "abstype" |-- Scan.succeed (lift_attribute add_abstype) + || Args.del |-- Scan.succeed (lift_attribute del_eqn) + || Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term >> lift_const_attribute del_eqns) + || Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term >> lift_const_attribute del_exception) + || Scan.succeed (lift_attribute add_eqn_maybe_abs); in Attrib.setup @{binding code} (Scan.lift code_attribute_parser) "declare theorems for code generation" diff -r 7c593d4f1f89 -r d562c9948dee src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/Pure/Isar/specification.ML Mon Jun 06 21:28:46 2016 +0200 @@ -260,7 +260,7 @@ val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]); val ([(def_name, [th'])], lthy4) = lthy3 - |> Local_Theory.notes [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])]; + |> Local_Theory.notes [((name, Code.add_default_eqn_attrib Code.Equation :: atts), [([th], [])])]; val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs; diff -r 7c593d4f1f89 -r d562c9948dee src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Mon Jun 06 21:28:45 2016 +0200 +++ b/src/Pure/Proof/extraction.ML Mon Jun 06 21:28:46 2016 +0200 @@ -810,7 +810,7 @@ (Proof_Checker.thm_of_proof thy' (fst (Proofterm.freeze_thaw_prf prf)))))) |> snd - |> fold Code.add_default_eqn def_thms + |> fold (Code.add_eqn (Code.Equation, true)) def_thms end | SOME _ => thy);