src/Pure/term.ML
changeset 16863 79b9a6481ae4
parent 16793 51600bfac176
child 16882 a0273f573f23
     1.1 --- a/src/Pure/term.ML	Fri Jul 15 15:44:17 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Fri Jul 15 15:44:18 2005 +0200
     1.3 @@ -161,12 +161,8 @@
     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 add_term_varnames: term -> indexname list -> indexname list
    1.14    val term_varnames: term -> indexname list
    1.15    val compress_type: typ -> typ
    1.16    val compress_term: term -> term
    1.17 @@ -195,14 +191,10 @@
    1.18    val map_typ: (string -> string) -> (string -> string) -> typ -> typ
    1.19    val map_term: (string -> string) -> (string -> string) -> (string -> string) -> term -> term
    1.20    val dest_abs: string * typ * term -> string * term
    1.21 -  (*val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
    1.22 +  val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
    1.23    val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
    1.24 -  val add_vars: (indexname * typ) list * term -> (indexname * typ) list
    1.25 -  val add_frees: (string * typ) list * term -> (string * typ) list*)
    1.26 -  val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
    1.27 -  val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
    1.28 -  val add_vars: (indexname * typ) list * term -> (indexname * typ) list
    1.29 -  val add_frees: (string * typ) list * term -> (string * typ) list
    1.30 +  val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
    1.31 +  val add_frees: term -> (string * typ) list -> (string * typ) list
    1.32    val dummy_patternN: string
    1.33    val no_dummy_patterns: term -> term
    1.34    val replace_dummy_patterns: int * term -> int * term
    1.35 @@ -1197,74 +1189,32 @@
    1.36  
    1.37  (*fold atoms of type*)
    1.38  fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
    1.39 -  | fold_atyps f T = f T
    1.40 +  | fold_atyps f T = f T;
    1.41  
    1.42  (*fold atoms of term*)
    1.43 -fun fold_aterms f (t $ u) = (fold_aterms f u) o (fold_aterms f t)
    1.44 +fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
    1.45    | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
    1.46 -  | fold_aterms f t = f t;
    1.47 +  | fold_aterms f a = f a;
    1.48  
    1.49  (*fold types of term*)
    1.50  fun fold_term_types f (t as Const (_, T)) = f t T
    1.51    | fold_term_types f (t as Free (_, T)) = f t T
    1.52    | fold_term_types f (t as Var (_, T)) = f t T
    1.53    | fold_term_types f (Bound _) = I
    1.54 -  | fold_term_types f (t as Abs (_, T, b)) = (fold_term_types f b) o (f t T)
    1.55 -  | fold_term_types f (t $ u) = (fold_term_types f u) o (fold_term_types f t);
    1.56 -
    1.57 -fun fold_types f = fold_term_types (fn _ => f);
    1.58 +  | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b
    1.59 +  | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u;
    1.60  
    1.61 -(*foldl atoms of type*)
    1.62 -fun foldl_atyps f (x, Type (_, Ts)) = Library.foldl (foldl_atyps f) (x, Ts)
    1.63 -  | foldl_atyps f x_atom = f x_atom;
    1.64 -
    1.65 -(*foldl atoms of term*)
    1.66 -fun foldl_aterms f (x, t $ u) = foldl_aterms f (foldl_aterms f (x, t), u)
    1.67 -  | foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t)
    1.68 -  | foldl_aterms f x_atom = f x_atom;
    1.69 +fun fold_types f = fold_term_types (K f);
    1.70  
    1.71 -(*foldl types of term*)
    1.72 -fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T)
    1.73 -  | foldl_term_types f (x, t as Free (_, T)) = f t (x, T)
    1.74 -  | foldl_term_types f (x, t as Var (_, T)) = f t (x, T)
    1.75 -  | foldl_term_types f (x, Bound _) = x
    1.76 -  | foldl_term_types f (x, t as Abs (_, T, b)) = foldl_term_types f (f t (x, T), b)
    1.77 -  | foldl_term_types f (x, t $ u) = foldl_term_types f (foldl_term_types f (x, t), u);
    1.78 -
    1.79 -fun foldl_types f = foldl_term_types (fn _ => f);
    1.80 -
    1.81 -(*(*collect variables*)
    1.82 -val add_tvarsT =
    1.83 -  let fun add_tvarsT' (TVar v) = insert (op =) v
    1.84 -         | add_tvarsT' _ = I
    1.85 -  in fold_atyps add_tvarsT' end;
    1.86 +(*collect variables*)
    1.87 +val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
    1.88  val add_tvars = fold_types add_tvarsT;
    1.89 -val add_vars =
    1.90 -  let fun add_vars' (Var v) = insert (op =) v
    1.91 -         | add_vars' _ = I
    1.92 -  in uncurry (fold_aterms add_vars') o swap end;
    1.93 -val add_frees =
    1.94 -  let fun add_frees' (Free v) = insert (op =) v
    1.95 -         | add_frees' _ = I
    1.96 -  in uncurry (fold_aterms add_frees') o swap end;
    1.97 +val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
    1.98 +val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
    1.99  
   1.100  (*collect variable names*)
   1.101 -val add_term_varnames =
   1.102 -  let fun add_term_varnames' (Var (x, _)) xs = ins_ix (x, xs)
   1.103 -         | add_term_varnames' _ xs = xs
   1.104 -  in uncurry (fold_aterms add_term_varnames') o swap end;
   1.105 -  
   1.106 -fun term_varnames t = add_term_varnames ([], t);*)
   1.107 -
   1.108 -(*collect variables*)
   1.109 -val add_tvarsT = foldl_atyps (fn (vs, TVar v) => insert (op =) v vs | (vs, _) => vs);
   1.110 -val add_tvars = foldl_types add_tvarsT;
   1.111 -val add_vars = foldl_aterms (fn (vs, Var v) => insert (op =) v vs | (vs, _) => vs);
   1.112 -val add_frees = foldl_aterms (fn (vs, Free v) => insert (op =) v vs | (vs, _) => vs);
   1.113 -
   1.114 -(*collect variable names*)
   1.115 -val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
   1.116 -fun term_varnames t = add_term_varnames ([], t);
   1.117 +val add_term_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
   1.118 +fun term_varnames t = add_term_varnames t [];
   1.119  
   1.120  
   1.121