# HG changeset patch # User haftmann # Date 1399616017 -7200 # Node ID 40213e24c8c4e76d3e3e6e87bd6217bbb558183b # Parent 1e50fddbe1f5973c8c76ebbd85ff2d64bb943b4c delete attribute for code abbrev diff -r 1e50fddbe1f5 -r 40213e24c8c4 src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri May 09 08:13:37 2014 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri May 09 08:13:37 2014 +0200 @@ -2606,7 +2606,8 @@ "del"}'' removes) theorems which are applied as rewrite rules to any result of an evaluation. - \item @{attribute (HOL) code_abbrev} declares equations which are + \item @{attribute (HOL) code_abbrev} declares (or with option ``@{text + "del"}'' removes) equations which are applied as rewrite rules to any result of an evaluation and symmetrically during preprocessing to any code equation or evaluation input. diff -r 1e50fddbe1f5 -r 40213e24c8c4 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Fri May 09 08:13:37 2014 +0200 +++ b/src/Tools/Code/code_preproc.ML Fri May 09 08:13:37 2014 +0200 @@ -9,7 +9,6 @@ sig val map_pre: (Proof.context -> Proof.context) -> theory -> theory val map_post: (Proof.context -> Proof.context) -> theory -> theory - val add_unfold: thm -> theory -> theory val add_functrans: string * (Proof.context -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory val del_functrans: string -> theory -> theory val simple_functrans: (Proof.context -> thm list -> thm list option) @@ -87,20 +86,18 @@ val map_pre = map_simpset apfst; val map_post = map_simpset apsnd; -val add_unfold = map_pre o Simplifier.add_simp; -val del_unfold = map_pre o Simplifier.del_simp; -val add_post = map_post o Simplifier.add_simp; -val del_post = map_post o Simplifier.del_simp; +fun process_unfold add_del = map_pre o add_del; +fun process_post add_del = map_post o add_del; -fun add_code_abbrev raw_thm thy = +fun process_abbrev add_del raw_thm thy = let val ctxt = Proof_Context.init_global thy; val thm = Local_Defs.meta_rewrite_rule ctxt raw_thm; val thm_sym = Thm.symmetric thm; in thy |> map_pre_post (fn (pre, post) => - (pre |> simpset_map ctxt (Simplifier.add_simp thm_sym), - post |> simpset_map ctxt (Simplifier.add_simp thm))) + (pre |> simpset_map ctxt (add_del thm_sym), + post |> simpset_map ctxt (add_del thm))) end; fun add_functrans (name, f) = (map_data o apsnd) @@ -520,14 +517,15 @@ val setup = let fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); - fun add_del_attribute_parser add del = - Attrib.add_del (mk_attribute add) (mk_attribute del); + fun add_del_attribute_parser process = + Attrib.add_del (mk_attribute (process Simplifier.add_simp)) + (mk_attribute (process Simplifier.del_simp)); in - Attrib.setup @{binding code_unfold} (add_del_attribute_parser add_unfold del_unfold) + Attrib.setup @{binding code_unfold} (add_del_attribute_parser process_unfold) "preprocessing equations for code generator" - #> Attrib.setup @{binding code_post} (add_del_attribute_parser add_post del_post) + #> Attrib.setup @{binding code_post} (add_del_attribute_parser process_post) "postprocessing equations for code generator" - #> Attrib.setup @{binding code_abbrev} (Scan.succeed (mk_attribute add_code_abbrev)) + #> Attrib.setup @{binding code_abbrev} (add_del_attribute_parser process_abbrev) "post- and preprocessing equations for code generator" end;