different handling of eta expansion
authorhaftmann
Thu Jan 04 14:01:40 2007 +0100 (2007-01-04)
changeset 21990d382f901304c
parent 21989 0315ecfd3d5d
child 21991 04528ce9ded5
different handling of eta expansion
src/Pure/Tools/codegen_package.ML
     1.1 --- a/src/Pure/Tools/codegen_package.ML	Thu Jan 04 14:01:39 2007 +0100
     1.2 +++ b/src/Pure/Tools/codegen_package.ML	Thu Jan 04 14:01:40 2007 +0100
     1.3 @@ -86,6 +86,17 @@
     1.4  val _ = Context.add_setup (Code.init #> CodegenPackageData.init);
     1.5  
     1.6  
     1.7 +(* preparing function equations *)
     1.8 +
     1.9 +fun prep_eqs thy (thms as thm :: _) =
    1.10 +  let
    1.11 +    val ty = (Logic.unvarifyT o CodegenData.typ_func thy) thm;
    1.12 +    val thms' = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
    1.13 +      then thms
    1.14 +      else map (CodegenFuncgr.expand_eta thy 1) thms;
    1.15 +  in (ty, thms') end;
    1.16 +
    1.17 +
    1.18  (* extraction kernel *)
    1.19  
    1.20  fun check_strict (false, _) has_seri x =
    1.21 @@ -268,12 +279,12 @@
    1.22      fun defgen_fun trns =
    1.23        case CodegenFuncgr.funcs funcgr
    1.24          (perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) c_tys)
    1.25 -       of eq_thms as eq_thm :: _ =>
    1.26 +       of thms as _ :: _ =>
    1.27              let
    1.28 +              val (ty, eq_thms) = prep_eqs thy thms;
    1.29                val timeap = if !timing then Output.timeap_msg ("time for " ^ c')
    1.30                  else I;
    1.31                val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
    1.32 -              val ty = (Logic.unvarifyT o CodegenData.typ_func thy) eq_thm;
    1.33                val vs = (map dest_TFree o Consts.typargs consts) (c', ty);
    1.34                val dest_eqthm =
    1.35                  apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify o prop_of;