src/Pure/term.ML
changeset 24483 0b1a8fd26da9
parent 23178 07ba6b58b3d2
child 24671 35075a1e9599
     1.1 --- a/src/Pure/term.ML	Thu Aug 30 11:46:37 2007 +0200
     1.2 +++ b/src/Pure/term.ML	Thu Aug 30 15:04:41 2007 +0200
     1.3 @@ -74,6 +74,7 @@
     1.4    val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
     1.5    val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
     1.6    val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
     1.7 +  val burrow_types: (typ list -> typ list) -> term list -> term list
     1.8    val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
     1.9    val add_term_names: term * string list -> string list
    1.10    val aconv: term * term -> bool
    1.11 @@ -481,6 +482,26 @@
    1.12  
    1.13  fun fold_types f = fold_term_types (K f);
    1.14  
    1.15 +fun replace_types (Const (c, _)) (T :: Ts) = (Const (c, T), Ts)
    1.16 +  | replace_types (Free (x, _)) (T :: Ts) = (Free (x, T), Ts)
    1.17 +  | replace_types (Var (xi, _)) (T :: Ts) = (Var (xi, T), Ts)
    1.18 +  | replace_types (Bound i) Ts = (Bound i, Ts)
    1.19 +  | replace_types (Abs (x, _, b)) (T :: Ts) =
    1.20 +      let val (b', Ts') = replace_types b Ts
    1.21 +      in (Abs (x, T, b'), Ts') end
    1.22 +  | replace_types (t $ u) Ts =
    1.23 +      let
    1.24 +        val (t', Ts') = replace_types t Ts;
    1.25 +        val (u', Ts'') = replace_types u Ts';
    1.26 +      in (t' $ u', Ts'') end;
    1.27 +
    1.28 +fun burrow_types f ts =
    1.29 +  let
    1.30 +    val Ts = rev (fold (fold_types cons) ts []);
    1.31 +    val Ts' = f Ts;
    1.32 +    val (ts', []) = fold_map replace_types ts Ts';
    1.33 +  in ts' end;
    1.34 +
    1.35  (*collect variables*)
    1.36  val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
    1.37  val add_tvars = fold_types add_tvarsT;