unfold_fun_n
authorhaftmann
Wed Jun 30 11:38:51 2010 +0200 (2010-06-30)
changeset 37640fc27be4c6b1c
parent 37639 5b6733e6e033
child 37641 39bd6f7c25c2
unfold_fun_n
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Wed Jun 30 11:38:51 2010 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Jun 30 11:38:51 2010 +0200
     1.3 @@ -40,6 +40,7 @@
     1.4    val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list
     1.5    val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
     1.6    val unfold_fun: itype -> itype list * itype
     1.7 +  val unfold_fun_n: int -> itype -> itype list * itype
     1.8    val unfold_app: iterm -> iterm * iterm list
     1.9    val unfold_abs: iterm -> (vname option * itype) list * iterm
    1.10    val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
    1.11 @@ -396,6 +397,13 @@
    1.12    (fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE
    1.13      | _ => NONE);
    1.14  
    1.15 +fun unfold_fun_n n ty =
    1.16 +  let
    1.17 +    val (tys1, ty1) = unfold_fun ty;
    1.18 +    val (tys3, tys2) = chop n tys1;
    1.19 +    val ty3 = Library.foldr (fn (ty1, ty2) => fun_tyco `%% [ty1, ty2]) (tys2, ty1);
    1.20 +  in (tys3, ty3) end;
    1.21 +
    1.22  end; (* local *)
    1.23  
    1.24