provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
authorwenzelm
Tue Dec 30 21:46:14 2008 +0100 (2008-12-30)
changeset 29257660234d959f7
parent 29256 2f1759641087
child 29258 bce03c644efb
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
renamed add_varnames to add_var_names;
removed old add_typ_ixns, add_term_tvar_ixns;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Tue Dec 30 20:53:21 2008 +0100
     1.2 +++ b/src/Pure/term.ML	Tue Dec 30 21:46:14 2008 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  Simply typed lambda-calculus: types, terms, and basic operations.
     1.5  *)
     1.6  
     1.7 -infix 9  $;
     1.8 +infix 9 $;
     1.9  infixr 5 -->;
    1.10  infixr --->;
    1.11  infix aconv;
    1.12 @@ -132,8 +132,6 @@
    1.13    val typ_tvars: typ -> (indexname * sort) list
    1.14    val term_tfrees: term -> (string * sort) list
    1.15    val term_tvars: term -> (indexname * sort) list
    1.16 -  val add_typ_ixns: indexname list * typ -> indexname list
    1.17 -  val add_term_tvar_ixns: term * indexname list -> indexname list
    1.18    val add_term_vars: term * term list -> term list
    1.19    val term_vars: term -> term list
    1.20    val add_term_frees: term * term list -> term list
    1.21 @@ -150,12 +148,17 @@
    1.22    val a_itselfT: typ
    1.23    val all: typ -> term
    1.24    val argument_type_of: term -> int -> typ
    1.25 +  val add_tvar_namesT: typ -> indexname list -> indexname list
    1.26 +  val add_tvar_names: term -> indexname list -> indexname list
    1.27    val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
    1.28    val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
    1.29 +  val add_var_names: term -> indexname list -> indexname list
    1.30    val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
    1.31 -  val add_varnames: term -> indexname list -> indexname list
    1.32 +  val add_tfree_namesT: typ -> string list -> string list
    1.33 +  val add_tfree_names: term -> string list -> string list
    1.34    val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
    1.35    val add_tfrees: term -> (string * sort) list -> (string * sort) list
    1.36 +  val add_free_names: term -> string list -> string list
    1.37    val add_frees: term -> (string * typ) list -> (string * typ) list
    1.38    val hidden_polymorphism: term -> (indexname * sort) list
    1.39    val strip_abs_eta: int -> term -> (string * typ) list * term
    1.40 @@ -492,12 +495,17 @@
    1.41    in ts' end;
    1.42  
    1.43  (*collect variables*)
    1.44 +val add_tvar_namesT = fold_atyps (fn TVar (xi, _) => insert (op =) xi | _ => I);
    1.45 +val add_tvar_names = fold_types add_tvar_namesT;
    1.46  val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
    1.47  val add_tvars = fold_types add_tvarsT;
    1.48 +val add_var_names = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
    1.49  val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
    1.50 -val add_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
    1.51 +val add_tfree_namesT = fold_atyps (fn TFree (xi, _) => insert (op =) xi | _ => I);
    1.52 +val add_tfree_names = fold_types add_tfree_namesT;
    1.53  val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
    1.54  val add_tfrees = fold_types add_tfreesT;
    1.55 +val add_free_names = fold_aterms (fn Free (x, _) => insert (op =) x | _ => I);
    1.56  val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
    1.57  
    1.58  (*extra type variables in a term, not covered by its type*)
    1.59 @@ -1141,22 +1149,6 @@
    1.60  fun term_tfrees t = add_term_tfrees(t,[]);
    1.61  fun term_tvars t = add_term_tvars(t,[]);
    1.62  
    1.63 -(*special code to enforce left-to-right collection of TVar-indexnames*)
    1.64 -
    1.65 -fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts)
    1.66 -  | add_typ_ixns(ixns,TVar(ixn,_)) = if member (op =) ixns ixn then ixns
    1.67 -                                     else ixns@[ixn]
    1.68 -  | add_typ_ixns(ixns,TFree(_)) = ixns;
    1.69 -
    1.70 -fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
    1.71 -  | add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T)
    1.72 -  | add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T)
    1.73 -  | add_term_tvar_ixns(Bound _,ixns) = ixns
    1.74 -  | add_term_tvar_ixns(Abs(_,T,t),ixns) =
    1.75 -      add_term_tvar_ixns(t,add_typ_ixns(ixns,T))
    1.76 -  | add_term_tvar_ixns(f$t,ixns) =
    1.77 -      add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
    1.78 -
    1.79  
    1.80  (** Frees and Vars **)
    1.81