src/Pure/term.ML
changeset 16787 b6b6e2faaa41
parent 16724 1c8317722b4c
child 16790 be2780f435e1
     1.1 --- a/src/Pure/term.ML	Wed Jul 13 10:48:21 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Wed Jul 13 11:16:34 2005 +0200
     1.3 @@ -157,10 +157,10 @@
     1.4    val term_frees: term -> term list
     1.5    val variant_abs: string * typ * term -> string * term
     1.6    val rename_wrt_term: term -> (string * typ) list -> (string * typ) list
     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 fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
    1.12 +  val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
    1.13 +  val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
    1.14 +  val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
    1.15    val add_term_names: term * string list -> string list
    1.16    val add_term_varnames: indexname list * term -> indexname list
    1.17    val term_varnames: term -> indexname list
    1.18 @@ -191,8 +191,8 @@
    1.19    val map_typ: (string -> string) -> (string -> string) -> typ -> typ
    1.20    val map_term: (string -> string) -> (string -> string) -> (string -> string) -> term -> term
    1.21    val dest_abs: string * typ * term -> string * term
    1.22 -  val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
    1.23 -  val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
    1.24 +  val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
    1.25 +  val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
    1.26    val add_vars: (indexname * typ) list * term -> (indexname * typ) list
    1.27    val add_frees: (string * typ) list * term -> (string * typ) list
    1.28    val dummy_patternN: string
    1.29 @@ -1188,32 +1188,45 @@
    1.30  (* left-ro-right traversal *)
    1.31  
    1.32  (*foldl atoms of type*)
    1.33 -fun foldl_atyps f (x, Type (_, Ts)) = Library.foldl (foldl_atyps f) (x, Ts)
    1.34 -  | foldl_atyps f x_atom = f x_atom;
    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 -fun foldl_aterms f (x, t $ u) = foldl_aterms f (foldl_aterms f (x, t), u)
    1.40 -  | foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t)
    1.41 -  | foldl_aterms f x_atom = f x_atom;
    1.42 +fun fold_aterms f (t $ u) = (fold_aterms f u) o (fold_aterms f t)
    1.43 +  | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
    1.44 +  | fold_aterms f t = f t;
    1.45  
    1.46  (*foldl types of term*)
    1.47 -fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T)
    1.48 -  | foldl_term_types f (x, t as Free (_, T)) = f t (x, T)
    1.49 -  | foldl_term_types f (x, t as Var (_, T)) = f t (x, T)
    1.50 -  | foldl_term_types f (x, Bound _) = x
    1.51 -  | foldl_term_types f (x, t as Abs (_, T, b)) = foldl_term_types f (f t (x, T), b)
    1.52 -  | foldl_term_types f (x, t $ u) = foldl_term_types f (foldl_term_types f (x, t), u);
    1.53 +fun fold_term_types f (t as Const (_, T)) = f t T
    1.54 +  | fold_term_types f (t as Free (_, T)) = f t T
    1.55 +  | fold_term_types f (t as Var (_, T)) = f t T
    1.56 +  | fold_term_types f (Bound _) = I
    1.57 +  | fold_term_types f (t as Abs (_, T, b)) = (fold_term_types f b) o (f t T)
    1.58 +  | fold_term_types f (t $ u) = (fold_term_types f u) o (fold_term_types f t);
    1.59  
    1.60 -fun foldl_types f = foldl_term_types (fn _ => f);
    1.61 +fun fold_types f = fold_term_types (fn _ => f);
    1.62  
    1.63  (*collect variables*)
    1.64 -val add_tvarsT = foldl_atyps (fn (vs, TVar v) => insert (op =) v vs | (vs, _) => vs);
    1.65 -val add_tvars = foldl_types add_tvarsT;
    1.66 -val add_vars = foldl_aterms (fn (vs, Var v) => insert (op =) v vs | (vs, _) => vs);
    1.67 -val add_frees = foldl_aterms (fn (vs, Free v) => insert (op =) v vs | (vs, _) => vs);
    1.68 +val add_tvarsT =
    1.69 +  let fun add_tvarsT' (TVar v) = insert (op =) v
    1.70 +         | add_tvarsT' _ = I
    1.71 +  in fold_atyps add_tvarsT' end;
    1.72 +val add_tvars = fold_types add_tvarsT;
    1.73 +val add_vars =
    1.74 +  let fun add_vars' (Var v) = insert (op =) v
    1.75 +         | add_vars' _ = I
    1.76 +  in uncurry (fold_aterms add_vars') o swap end;
    1.77 +val add_frees =
    1.78 +  let fun add_frees' (Free v) = insert (op =) v
    1.79 +         | add_frees' _ = I
    1.80 +  in uncurry (fold_aterms add_frees') o swap end;
    1.81  
    1.82  (*collect variable names*)
    1.83 -val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
    1.84 +val add_term_varnames =
    1.85 +  let fun add_term_varnames' (Var (x, _)) xs = ins_ix (x, xs)
    1.86 +         | add_term_varnames' _ xs = xs
    1.87 +  in uncurry (fold_aterms add_term_varnames') o swap end;
    1.88 +  
    1.89  fun term_varnames t = add_term_varnames ([], t);
    1.90  
    1.91  
    1.92 @@ -1258,7 +1271,7 @@
    1.93    | is_dummy_pattern _ = false;
    1.94  
    1.95  fun no_dummy_patterns tm =
    1.96 -  if not (foldl_aterms (fn (b, t) => b orelse is_dummy_pattern t) (false, tm)) then tm
    1.97 +  if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
    1.98    else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
    1.99  
   1.100  fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =