src/Pure/term.ML
changeset 16790 be2780f435e1
parent 16787 b6b6e2faaa41
child 16793 51600bfac176
     1.1 --- a/src/Pure/term.ML	Wed Jul 13 11:29:08 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Wed Jul 13 11:30:37 2005 +0200
     1.3 @@ -161,6 +161,10 @@
     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 foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a
     1.8 +  val foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a
     1.9 +  val foldl_term_types: (term -> 'a * typ -> 'a) -> 'a * term -> 'a
    1.10 +  val foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a
    1.11    val add_term_names: term * string list -> string list
    1.12    val add_term_varnames: indexname list * term -> indexname list
    1.13    val term_varnames: term -> indexname list
    1.14 @@ -191,9 +195,13 @@
    1.15    val map_typ: (string -> string) -> (string -> string) -> typ -> typ
    1.16    val map_term: (string -> string) -> (string -> string) -> (string -> string) -> term -> term
    1.17    val dest_abs: string * typ * term -> string * term
    1.18 -  val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
    1.19 +  (*val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
    1.20    val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
    1.21    val add_vars: (indexname * typ) list * term -> (indexname * typ) list
    1.22 +  val add_frees: (string * typ) list * term -> (string * typ) list*)
    1.23 +  val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
    1.24 +  val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
    1.25 +  val add_vars: (indexname * typ) list * term -> (indexname * typ) list
    1.26    val add_frees: (string * typ) list * term -> (string * typ) list
    1.27    val dummy_patternN: string
    1.28    val no_dummy_patterns: term -> term
    1.29 @@ -1187,16 +1195,16 @@
    1.30  
    1.31  (* left-ro-right traversal *)
    1.32  
    1.33 -(*foldl atoms of type*)
    1.34 +(*fold atoms of type*)
    1.35  fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
    1.36    | fold_atyps f T = f T
    1.37  
    1.38 -(*foldl atoms of term*)
    1.39 +(*fold atoms of term*)
    1.40  fun fold_aterms f (t $ u) = (fold_aterms f u) o (fold_aterms f t)
    1.41    | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
    1.42    | fold_aterms f t = f t;
    1.43  
    1.44 -(*foldl types of term*)
    1.45 +(*fold types of term*)
    1.46  fun fold_term_types f (t as Const (_, T)) = f t T
    1.47    | fold_term_types f (t as Free (_, T)) = f t T
    1.48    | fold_term_types f (t as Var (_, T)) = f t T
    1.49 @@ -1206,7 +1214,26 @@
    1.50  
    1.51  fun fold_types f = fold_term_types (fn _ => f);
    1.52  
    1.53 -(*collect variables*)
    1.54 +(*foldl atoms of type*)
    1.55 +fun foldl_atyps f (x, Type (_, Ts)) = Library.foldl (foldl_atyps f) (x, Ts)
    1.56 +  | foldl_atyps f x_atom = f x_atom;
    1.57 +
    1.58 +(*foldl atoms of term*)
    1.59 +fun foldl_aterms f (x, t $ u) = foldl_aterms f (foldl_aterms f (x, t), u)
    1.60 +  | foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t)
    1.61 +  | foldl_aterms f x_atom = f x_atom;
    1.62 +
    1.63 +(*foldl types of term*)
    1.64 +fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T)
    1.65 +  | foldl_term_types f (x, t as Free (_, T)) = f t (x, T)
    1.66 +  | foldl_term_types f (x, t as Var (_, T)) = f t (x, T)
    1.67 +  | foldl_term_types f (x, Bound _) = x
    1.68 +  | foldl_term_types f (x, t as Abs (_, T, b)) = foldl_term_types f (f t (x, T), b)
    1.69 +  | foldl_term_types f (x, t $ u) = foldl_term_types f (foldl_term_types f (x, t), u);
    1.70 +
    1.71 +fun foldl_types f = foldl_term_types (fn _ => f);
    1.72 +
    1.73 +(*(*collect variables*)
    1.74  val add_tvarsT =
    1.75    let fun add_tvarsT' (TVar v) = insert (op =) v
    1.76           | add_tvarsT' _ = I
    1.77 @@ -1219,7 +1246,7 @@
    1.78  val add_frees =
    1.79    let fun add_frees' (Free v) = insert (op =) v
    1.80           | add_frees' _ = I
    1.81 -  in uncurry (fold_aterms add_frees') o swap end;
    1.82 +  in uncurry (fold_aterms add_frees') o swap end;*)
    1.83  
    1.84  (*collect variable names*)
    1.85  val add_term_varnames =
    1.86 @@ -1227,6 +1254,16 @@
    1.87           | add_term_varnames' _ xs = xs
    1.88    in uncurry (fold_aterms add_term_varnames') o swap end;
    1.89    
    1.90 +fun term_varnames t = add_term_varnames ([], t);*)
    1.91 +
    1.92 +(*collect variables*)
    1.93 +val add_tvarsT = foldl_atyps (fn (vs, TVar v) => insert (op =) v vs | (vs, _) => vs);
    1.94 +val add_tvars = foldl_types add_tvarsT;
    1.95 +val add_vars = foldl_aterms (fn (vs, Var v) => insert (op =) v vs | (vs, _) => vs);
    1.96 +val add_frees = foldl_aterms (fn (vs, Free v) => insert (op =) v vs | (vs, _) => vs);
    1.97 +
    1.98 +(*collect variable names*)
    1.99 +val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
   1.100  fun term_varnames t = add_term_varnames ([], t);
   1.101  
   1.102