src/Pure/old_term.ML
changeset 44143 d282b3c5df7c
parent 44142 8e27e0177518
parent 44134 fa98623f1006
child 44144 74b3751ea271
     1.1 --- a/src/Pure/old_term.ML	Wed Aug 10 18:02:16 2011 -0700
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,94 +0,0 @@
     1.4 -(*  Title:      Pure/old_term.ML
     1.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6 -
     1.7 -Some outdated term operations.
     1.8 -*)
     1.9 -
    1.10 -signature OLD_TERM =
    1.11 -sig
    1.12 -  val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
    1.13 -  val add_term_names: term * string list -> string list
    1.14 -  val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
    1.15 -  val add_typ_tfree_names: typ * string list -> string list
    1.16 -  val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
    1.17 -  val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
    1.18 -  val add_term_tfrees: term * (string * sort) list -> (string * sort) list
    1.19 -  val add_term_tfree_names: term * string list -> string list
    1.20 -  val typ_tfrees: typ -> (string * sort) list
    1.21 -  val typ_tvars: typ -> (indexname * sort) list
    1.22 -  val term_tfrees: term -> (string * sort) list
    1.23 -  val term_tvars: term -> (indexname * sort) list
    1.24 -  val add_term_vars: term * term list -> term list
    1.25 -  val term_vars: term -> term list
    1.26 -  val add_term_frees: term * term list -> term list
    1.27 -  val term_frees: term -> term list
    1.28 -end;
    1.29 -
    1.30 -structure OldTerm: OLD_TERM =
    1.31 -struct
    1.32 -
    1.33 -(*iterate a function over all types in a term*)
    1.34 -fun it_term_types f =
    1.35 -let fun iter(Const(_,T), a) = f(T,a)
    1.36 -      | iter(Free(_,T), a) = f(T,a)
    1.37 -      | iter(Var(_,T), a) = f(T,a)
    1.38 -      | iter(Abs(_,T,t), a) = iter(t,f(T,a))
    1.39 -      | iter(f$u, a) = iter(f, iter(u, a))
    1.40 -      | iter(Bound _, a) = a
    1.41 -in iter end
    1.42 -
    1.43 -(*Accumulates the names in the term, suppressing duplicates.
    1.44 -  Includes Frees and Consts.  For choosing unambiguous bound var names.*)
    1.45 -fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
    1.46 -  | add_term_names (Free(a,_), bs) = insert (op =) a bs
    1.47 -  | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
    1.48 -  | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
    1.49 -  | add_term_names (_, bs) = bs;
    1.50 -
    1.51 -(*Accumulates the TVars in a type, suppressing duplicates.*)
    1.52 -fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
    1.53 -  | add_typ_tvars(TFree(_),vs) = vs
    1.54 -  | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
    1.55 -
    1.56 -(*Accumulates the TFrees in a type, suppressing duplicates.*)
    1.57 -fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
    1.58 -  | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
    1.59 -  | add_typ_tfree_names(TVar(_),fs) = fs;
    1.60 -
    1.61 -fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
    1.62 -  | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
    1.63 -  | add_typ_tfrees(TVar(_),fs) = fs;
    1.64 -
    1.65 -(*Accumulates the TVars in a term, suppressing duplicates.*)
    1.66 -val add_term_tvars = it_term_types add_typ_tvars;
    1.67 -
    1.68 -(*Accumulates the TFrees in a term, suppressing duplicates.*)
    1.69 -val add_term_tfrees = it_term_types add_typ_tfrees;
    1.70 -val add_term_tfree_names = it_term_types add_typ_tfree_names;
    1.71 -
    1.72 -(*Non-list versions*)
    1.73 -fun typ_tfrees T = add_typ_tfrees(T,[]);
    1.74 -fun typ_tvars T = add_typ_tvars(T,[]);
    1.75 -fun term_tfrees t = add_term_tfrees(t,[]);
    1.76 -fun term_tvars t = add_term_tvars(t,[]);
    1.77 -
    1.78 -
    1.79 -(*Accumulates the Vars in the term, suppressing duplicates.*)
    1.80 -fun add_term_vars (t, vars: term list) = case t of
    1.81 -    Var   _ => Ord_List.insert Term_Ord.term_ord t vars
    1.82 -  | Abs (_,_,body) => add_term_vars(body,vars)
    1.83 -  | f$t =>  add_term_vars (f, add_term_vars(t, vars))
    1.84 -  | _ => vars;
    1.85 -
    1.86 -fun term_vars t = add_term_vars(t,[]);
    1.87 -
    1.88 -(*Accumulates the Frees in the term, suppressing duplicates.*)
    1.89 -fun add_term_frees (t, frees: term list) = case t of
    1.90 -    Free   _ => Ord_List.insert Term_Ord.term_ord t frees
    1.91 -  | Abs (_,_,body) => add_term_frees(body,frees)
    1.92 -  | f$t =>  add_term_frees (f, add_term_frees(t, frees))
    1.93 -  | _ => frees;
    1.94 -
    1.95 -fun term_frees t = add_term_frees(t,[]);
    1.96 -
    1.97 -end;