src/HOLCF/Tools/fixrec.ML
changeset 33401 fc43fa403a69
parent 33004 715566791eb0
child 33425 7e4f3c66190d
     1.1 --- a/src/HOLCF/Tools/fixrec.ML	Mon Nov 02 17:29:34 2009 -0800
     1.2 +++ b/src/HOLCF/Tools/fixrec.ML	Mon Nov 02 18:39:41 2009 -0800
     1.3 @@ -36,20 +36,9 @@
     1.4  
     1.5  infixr 6 ->>; val (op ->>) = cfunT;
     1.6  
     1.7 -fun cfunsT (Ts, U) = List.foldr cfunT U Ts;
     1.8 -
     1.9  fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
    1.10    | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
    1.11  
    1.12 -fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
    1.13 -  | binder_cfun _   =  [];
    1.14 -
    1.15 -fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
    1.16 -  | body_cfun T   =  T;
    1.17 -
    1.18 -fun strip_cfun T : typ list * typ =
    1.19 -  (binder_cfun T, body_cfun T);
    1.20 -
    1.21  fun maybeT T = Type(@{type_name "maybe"}, [T]);
    1.22  
    1.23  fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T
    1.24 @@ -59,9 +48,27 @@
    1.25    | tupleT [T] = T
    1.26    | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
    1.27  
    1.28 +local
    1.29 +
    1.30 +fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
    1.31 +  | binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U
    1.32 +  | binder_cfun _   =  [];
    1.33 +
    1.34 +fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
    1.35 +  | body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U
    1.36 +  | body_cfun T   =  T;
    1.37 +
    1.38 +fun strip_cfun T : typ list * typ =
    1.39 +  (binder_cfun T, body_cfun T);
    1.40 +
    1.41 +fun cfunsT (Ts, U) = List.foldr cfunT U Ts;
    1.42 +
    1.43 +in
    1.44 +
    1.45  fun matchT (T, U) =
    1.46    body_cfun T ->> cfunsT (binder_cfun T, U) ->> U;
    1.47  
    1.48 +end
    1.49  
    1.50  (*************************************************************************)
    1.51  (***************************** building terms ****************************)
    1.52 @@ -235,10 +242,16 @@
    1.53    | Const(@{const_name Rep_CFun},_)$f$x =>
    1.54        let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
    1.55        in pre_build match_name f rhs' (v::vs) taken' end
    1.56 +  | f$(v as Free(n,T)) =>
    1.57 +      pre_build match_name f rhs (v::vs) taken
    1.58 +  | f$x =>
    1.59 +      let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
    1.60 +      in pre_build match_name f rhs' (v::vs) taken' end
    1.61    | Const(c,T) =>
    1.62        let
    1.63          val n = Name.variant taken "v";
    1.64          fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
    1.65 +          | result_type (Type (@{type_name "fun"},[_,T])) (x::xs) = result_type T xs
    1.66            | result_type T _ = T;
    1.67          val v = Free(n, result_type T vs);
    1.68          val m = Const(match_name c, matchT (T, fastype_of rhs));