src/Pure/old_term.ML
author wenzelm
Thu Oct 01 23:27:05 2009 +0200 (2009-10-01)
changeset 32843 c8f5a7c8353f
parent 30364 577edc39b501
child 35408 b48ab741683b
permissions -rw-r--r--
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
     1 (*  Title:      Pure/old_term.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3 
     4 Some old-style term operations.
     5 *)
     6 
     7 signature OLD_TERM =
     8 sig
     9   val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
    10   val add_term_names: term * string list -> string list
    11   val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
    12   val add_typ_tfree_names: typ * string list -> string list
    13   val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
    14   val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
    15   val add_term_tfrees: term * (string * sort) list -> (string * sort) list
    16   val add_term_tfree_names: term * string list -> string list
    17   val typ_tfrees: typ -> (string * sort) list
    18   val typ_tvars: typ -> (indexname * sort) list
    19   val term_tfrees: term -> (string * sort) list
    20   val term_tvars: term -> (indexname * sort) list
    21   val add_term_vars: term * term list -> term list
    22   val term_vars: term -> term list
    23   val add_term_frees: term * term list -> term list
    24   val term_frees: term -> term list
    25 end;
    26 
    27 structure OldTerm: OLD_TERM =
    28 struct
    29 
    30 (*iterate a function over all types in a term*)
    31 fun it_term_types f =
    32 let fun iter(Const(_,T), a) = f(T,a)
    33       | iter(Free(_,T), a) = f(T,a)
    34       | iter(Var(_,T), a) = f(T,a)
    35       | iter(Abs(_,T,t), a) = iter(t,f(T,a))
    36       | iter(f$u, a) = iter(f, iter(u, a))
    37       | iter(Bound _, a) = a
    38 in iter end
    39 
    40 (*Accumulates the names in the term, suppressing duplicates.
    41   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
    42 fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
    43   | add_term_names (Free(a,_), bs) = insert (op =) a bs
    44   | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
    45   | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
    46   | add_term_names (_, bs) = bs;
    47 
    48 (*Accumulates the TVars in a type, suppressing duplicates.*)
    49 fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
    50   | add_typ_tvars(TFree(_),vs) = vs
    51   | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
    52 
    53 (*Accumulates the TFrees in a type, suppressing duplicates.*)
    54 fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
    55   | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
    56   | add_typ_tfree_names(TVar(_),fs) = fs;
    57 
    58 fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
    59   | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
    60   | add_typ_tfrees(TVar(_),fs) = fs;
    61 
    62 (*Accumulates the TVars in a term, suppressing duplicates.*)
    63 val add_term_tvars = it_term_types add_typ_tvars;
    64 
    65 (*Accumulates the TFrees in a term, suppressing duplicates.*)
    66 val add_term_tfrees = it_term_types add_typ_tfrees;
    67 val add_term_tfree_names = it_term_types add_typ_tfree_names;
    68 
    69 (*Non-list versions*)
    70 fun typ_tfrees T = add_typ_tfrees(T,[]);
    71 fun typ_tvars T = add_typ_tvars(T,[]);
    72 fun term_tfrees t = add_term_tfrees(t,[]);
    73 fun term_tvars t = add_term_tvars(t,[]);
    74 
    75 
    76 (*Accumulates the Vars in the term, suppressing duplicates.*)
    77 fun add_term_vars (t, vars: term list) = case t of
    78     Var   _ => OrdList.insert TermOrd.term_ord t vars
    79   | Abs (_,_,body) => add_term_vars(body,vars)
    80   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
    81   | _ => vars;
    82 
    83 fun term_vars t = add_term_vars(t,[]);
    84 
    85 (*Accumulates the Frees in the term, suppressing duplicates.*)
    86 fun add_term_frees (t, frees: term list) = case t of
    87     Free   _ => OrdList.insert TermOrd.term_ord t frees
    88   | Abs (_,_,body) => add_term_frees(body,frees)
    89   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
    90   | _ => frees;
    91 
    92 fun term_frees t = add_term_frees(t,[]);
    93 
    94 end;