1.1 --- a/src/Tools/Code/code_preproc.ML	Tue Jul 14 16:27:33 2009 +0200
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Tue Jul 14 16:27:34 2009 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  sig
     1.5    val map_pre: (simpset -> simpset) -> theory -> theory
     1.6    val map_post: (simpset -> simpset) -> theory -> theory
     1.7 -  val add_inline: thm -> theory -> theory
     1.8 +  val add_unfold: thm -> theory -> theory
     1.9    val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
    1.10    val del_functrans: string -> theory -> theory
    1.11    val simple_functrans: (theory -> thm list -> thm list option)
    1.12 @@ -77,14 +77,24 @@
    1.13    |> Code.purge_data
    1.14    |> (Code_Preproc_Data.map o map_thmproc) f;
    1.15  
    1.16 -val map_pre = map_data o apfst o apfst;
    1.17 -val map_post = map_data o apfst o apsnd;
    1.18 +val map_pre_post = map_data o apfst;
    1.19 +val map_pre = map_pre_post o apfst;
    1.20 +val map_post = map_pre_post o apsnd;
    1.21  
    1.22 -val add_inline = map_pre o MetaSimplifier.add_simp;
    1.23 -val del_inline = map_pre o MetaSimplifier.del_simp;
    1.24 +val add_unfold = map_pre o MetaSimplifier.add_simp;
    1.25 +val del_unfold = map_pre o MetaSimplifier.del_simp;
    1.26  val add_post = map_post o MetaSimplifier.add_simp;
    1.27  val del_post = map_post o MetaSimplifier.del_simp;
    1.28 -  
    1.29 +
    1.30 +fun add_unfold_post raw_thm thy =
    1.31 +  let
    1.32 +    val thm = LocalDefs.meta_rewrite_rule (ProofContext.init thy) raw_thm;
    1.33 +    val thm_sym = Thm.symmetric thm;
    1.34 +  in
    1.35 +    thy |> map_pre_post (fn (pre, post) =>
    1.36 +      (pre |> MetaSimplifier.add_simp thm, post |> MetaSimplifier.del_simp thm_sym))
    1.37 +  end;
    1.38 +
    1.39  fun add_functrans (name, f) = (map_data o apsnd)
    1.40    (AList.update (op =) (name, (serial (), f)));
    1.41  
    1.42 @@ -526,16 +536,19 @@
    1.43  val setup = 
    1.44    let
    1.45      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
    1.46 -    fun add_del_attribute_parser (add, del) =
    1.47 +    fun add_del_attribute_parser add del =
    1.48        Attrib.add_del (mk_attribute add) (mk_attribute del);
    1.49 +    fun both f g thm = f thm #> g thm;
    1.50    in
    1.51 -    Attrib.setup @{binding code_inline} (add_del_attribute_parser (add_inline, del_inline))
    1.52 +    Attrib.setup @{binding code_unfold} (add_del_attribute_parser 
    1.53 +       (both Codegen.add_unfold add_unfold) (both Codegen.del_unfold del_unfold))
    1.54 +        "preprocessing equations for code generators"
    1.55 +    #> Attrib.setup @{binding code_inline} (add_del_attribute_parser add_unfold del_unfold)
    1.56          "preprocessing equations for code generator"
    1.57 -    #> Attrib.setup @{binding code_post} (add_del_attribute_parser (add_post, del_post))
    1.58 +    #> Attrib.setup @{binding code_post} (add_del_attribute_parser add_post del_post)
    1.59          "postprocessing equations for code generator"
    1.60 -    #> Attrib.setup @{binding code_unfold} (Scan.succeed (mk_attribute
    1.61 -       (fn thm => Codegen.add_unfold thm #> add_inline thm)))
    1.62 -        "preprocessing equations for code generators"
    1.63 +    #> Attrib.setup @{binding code_unfold_post} (Scan.succeed (mk_attribute add_unfold_post))
    1.64 +        "pre- and postprocessing equations for code generator"
    1.65    end;
    1.66  
    1.67  val _ =