function transformer preprocessor applies to both code generators
authorhaftmann
Wed Jan 13 10:18:45 2010 +0100 (2010-01-13)
changeset 34893ecdc526af73a
parent 34892 6144d233b99a
child 34894 fadbdd350dd1
function transformer preprocessor applies to both code generators
src/HOL/Library/Efficient_Nat.thy
src/HOL/Tools/recfun_codegen.ML
src/Tools/Code/code_preproc.ML
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Jan 13 09:13:30 2010 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Wed Jan 13 10:18:45 2010 +0100
     1.3 @@ -161,7 +161,7 @@
     1.4        end
     1.5    in get_first mk_thms eqs end;
     1.6  
     1.7 -fun eqn_suc_preproc thy thms =
     1.8 +fun eqn_suc_base_preproc thy thms =
     1.9    let
    1.10      val dest = fst o Logic.dest_equals o prop_of;
    1.11      val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
    1.12 @@ -171,10 +171,7 @@
    1.13         else NONE
    1.14    end;
    1.15  
    1.16 -val eqn_suc_preproc1 = Code_Preproc.simple_functrans eqn_suc_preproc;
    1.17 -
    1.18 -fun eqn_suc_preproc2 thy thms = eqn_suc_preproc thy thms
    1.19 -  |> the_default thms;
    1.20 +val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc;
    1.21  
    1.22  fun remove_suc_clause thy thms =
    1.23    let
    1.24 @@ -217,9 +214,8 @@
    1.25    end;
    1.26  in
    1.27  
    1.28 -  Codegen.add_preprocessor eqn_suc_preproc2
    1.29 +  Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
    1.30    #> Codegen.add_preprocessor clause_suc_preproc
    1.31 -  #> Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc1)
    1.32  
    1.33  end;
    1.34  *}
     2.1 --- a/src/HOL/Tools/recfun_codegen.ML	Wed Jan 13 09:13:30 2010 +0100
     2.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Wed Jan 13 10:18:45 2010 +0100
     2.3 @@ -43,7 +43,7 @@
     2.4  fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
     2.5    let
     2.6      val c = AxClass.unoverload_const thy (raw_c, T);
     2.7 -    val raw_thms = Code.get_cert thy I c
     2.8 +    val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c
     2.9        |> Code.eqns_of_cert thy
    2.10        |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    2.11        |> map (AxClass.overload thy)
     3.1 --- a/src/Tools/Code/code_preproc.ML	Wed Jan 13 09:13:30 2010 +0100
     3.2 +++ b/src/Tools/Code/code_preproc.ML	Wed Jan 13 10:18:45 2010 +0100
     3.3 @@ -14,6 +14,7 @@
     3.4    val del_functrans: string -> theory -> theory
     3.5    val simple_functrans: (theory -> thm list -> thm list option)
     3.6      -> theory -> (thm * bool) list -> (thm * bool) list option
     3.7 +  val preprocess_functrans: theory -> (thm * bool) list -> (thm * bool) list
     3.8    val print_codeproc: theory -> unit
     3.9  
    3.10    type code_algebra
    3.11 @@ -120,15 +121,18 @@
    3.12    #> Logic.dest_equals
    3.13    #> snd;
    3.14  
    3.15 -fun preprocess thy eqns =
    3.16 +fun preprocess_functrans thy = 
    3.17    let
    3.18 -    val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
    3.19      val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
    3.20        o the_thmproc) thy;
    3.21 +  in perhaps (perhaps_loop (perhaps_apply functrans)) end;
    3.22 +
    3.23 +fun preprocess thy =
    3.24 +  let
    3.25 +    val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
    3.26    in
    3.27 -    eqns
    3.28 -    |> perhaps (perhaps_loop (perhaps_apply functrans))
    3.29 -    |> (map o apfst) (rewrite_eqn pre)
    3.30 +    preprocess_functrans thy
    3.31 +    #> (map o apfst) (rewrite_eqn pre)
    3.32    end;
    3.33  
    3.34  fun preprocess_conv thy ct =