--- a/src/Pure/term.ML Wed Jul 13 11:29:08 2005 +0200
+++ b/src/Pure/term.ML Wed Jul 13 11:30:37 2005 +0200
@@ -161,6 +161,10 @@
val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
+ val foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a
+ val foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a
+ val foldl_term_types: (term -> 'a * typ -> 'a) -> 'a * term -> 'a
+ val foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a
val add_term_names: term * string list -> string list
val add_term_varnames: indexname list * term -> indexname list
val term_varnames: term -> indexname list
@@ -191,9 +195,13 @@
val map_typ: (string -> string) -> (string -> string) -> typ -> typ
val map_term: (string -> string) -> (string -> string) -> (string -> string) -> term -> term
val dest_abs: string * typ * term -> string * term
- val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
+ (*val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
val add_vars: (indexname * typ) list * term -> (indexname * typ) list
+ val add_frees: (string * typ) list * term -> (string * typ) list*)
+ val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
+ val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
+ val add_vars: (indexname * typ) list * term -> (indexname * typ) list
val add_frees: (string * typ) list * term -> (string * typ) list
val dummy_patternN: string
val no_dummy_patterns: term -> term
@@ -1187,16 +1195,16 @@
(* left-ro-right traversal *)
-(*foldl atoms of type*)
+(*fold atoms of type*)
fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
| fold_atyps f T = f T
-(*foldl atoms of term*)
+(*fold atoms of term*)
fun fold_aterms f (t $ u) = (fold_aterms f u) o (fold_aterms f t)
| fold_aterms f (Abs (_, _, t)) = fold_aterms f t
| fold_aterms f t = f t;
-(*foldl types of term*)
+(*fold types of term*)
fun fold_term_types f (t as Const (_, T)) = f t T
| fold_term_types f (t as Free (_, T)) = f t T
| fold_term_types f (t as Var (_, T)) = f t T
@@ -1206,7 +1214,26 @@
fun fold_types f = fold_term_types (fn _ => f);
-(*collect variables*)
+(*foldl atoms of type*)
+fun foldl_atyps f (x, Type (_, Ts)) = Library.foldl (foldl_atyps f) (x, Ts)
+ | foldl_atyps f x_atom = f x_atom;
+
+(*foldl atoms of term*)
+fun foldl_aterms f (x, t $ u) = foldl_aterms f (foldl_aterms f (x, t), u)
+ | foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t)
+ | foldl_aterms f x_atom = f x_atom;
+
+(*foldl types of term*)
+fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T)
+ | foldl_term_types f (x, t as Free (_, T)) = f t (x, T)
+ | foldl_term_types f (x, t as Var (_, T)) = f t (x, T)
+ | foldl_term_types f (x, Bound _) = x
+ | foldl_term_types f (x, t as Abs (_, T, b)) = foldl_term_types f (f t (x, T), b)
+ | foldl_term_types f (x, t $ u) = foldl_term_types f (foldl_term_types f (x, t), u);
+
+fun foldl_types f = foldl_term_types (fn _ => f);
+
+(*(*collect variables*)
val add_tvarsT =
let fun add_tvarsT' (TVar v) = insert (op =) v
| add_tvarsT' _ = I
@@ -1219,7 +1246,7 @@
val add_frees =
let fun add_frees' (Free v) = insert (op =) v
| add_frees' _ = I
- in uncurry (fold_aterms add_frees') o swap end;
+ in uncurry (fold_aterms add_frees') o swap end;*)
(*collect variable names*)
val add_term_varnames =
@@ -1227,6 +1254,16 @@
| add_term_varnames' _ xs = xs
in uncurry (fold_aterms add_term_varnames') o swap end;
+fun term_varnames t = add_term_varnames ([], t);*)
+
+(*collect variables*)
+val add_tvarsT = foldl_atyps (fn (vs, TVar v) => insert (op =) v vs | (vs, _) => vs);
+val add_tvars = foldl_types add_tvarsT;
+val add_vars = foldl_aterms (fn (vs, Var v) => insert (op =) v vs | (vs, _) => vs);
+val add_frees = foldl_aterms (fn (vs, Free v) => insert (op =) v vs | (vs, _) => vs);
+
+(*collect variable names*)
+val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
fun term_varnames t = add_term_varnames ([], t);