src/Pure/term.ML
changeset 20199 3170fea83ae7
parent 20160 550e36c6a2d1
child 20239 620a3f297072
     1.1 --- a/src/Pure/term.ML	Tue Jul 25 21:18:05 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Tue Jul 25 21:18:06 2006 +0200
     1.3 @@ -42,7 +42,6 @@
     1.4    val is_Free: term -> bool
     1.5    val is_Var: term -> bool
     1.6    val is_TVar: typ -> bool
     1.7 -  val is_funtype: typ -> bool
     1.8    val dest_Const: term -> string * typ
     1.9    val dest_Free: term -> string * typ
    1.10    val dest_Var: term -> indexname * typ
    1.11 @@ -76,9 +75,6 @@
    1.12    val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
    1.13    val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
    1.14    val add_term_names: term * string list -> string list
    1.15 -  val add_term_varnames: term -> indexname list -> indexname list
    1.16 -  val term_varnames: term -> indexname list
    1.17 -  val find_free: term -> string -> term option
    1.18    val aconv: term * term -> bool
    1.19    val aconvs: term list * term list -> bool
    1.20    structure Vartab: TABLE
    1.21 @@ -145,7 +141,6 @@
    1.22    val term_vars: term -> term list
    1.23    val add_term_frees: term * term list -> term list
    1.24    val term_frees: term -> term list
    1.25 -  val variant_abs: string * typ * term -> string * term
    1.26    val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
    1.27    val show_question_marks: bool ref
    1.28  end;
    1.29 @@ -163,6 +158,7 @@
    1.30    val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
    1.31    val add_tfrees: term -> (string * sort) list -> (string * sort) list
    1.32    val add_frees: term -> (string * typ) list -> (string * typ) list
    1.33 +  val add_varnames: term -> indexname list -> indexname list
    1.34    val strip_abs_eta: int -> term -> (string * typ) list * term
    1.35    val fast_indexname_ord: indexname * indexname -> order
    1.36    val indexname_ord: indexname * indexname -> order
    1.37 @@ -303,10 +299,6 @@
    1.38  fun is_TVar (TVar _) = true
    1.39    | is_TVar _ = false;
    1.40  
    1.41 -(*Differs from proofterm/is_fun in its treatment of TVar*)
    1.42 -fun is_funtype (Type("fun",[_,_])) = true
    1.43 -  | is_funtype _ = false;
    1.44 -
    1.45  
    1.46  (** Destructors **)
    1.47  
    1.48 @@ -492,22 +484,11 @@
    1.49  val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
    1.50  val add_tvars = fold_types add_tvarsT;
    1.51  val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
    1.52 +val add_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
    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_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
    1.56  
    1.57 -(*collect variable names*)
    1.58 -val add_term_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
    1.59 -fun term_varnames t = add_term_varnames t [];
    1.60 -
    1.61 -fun find_free t x =
    1.62 -  let
    1.63 -    exception Found of term;
    1.64 -    fun find (t as Free (x', _)) = if x = x' then raise Found t else I
    1.65 -      | find _ = I;
    1.66 -  in (fold_aterms find t (); NONE) handle Found v => SOME v end;
    1.67 -
    1.68 -
    1.69  
    1.70  (** Comparing terms, types, sorts etc. **)
    1.71  
    1.72 @@ -842,9 +823,7 @@
    1.73    in (vs1 @ vs2, t'') end;
    1.74  
    1.75  
    1.76 -(** Specialized equality, membership, insertion etc. **)
    1.77 -
    1.78 -(* variables *)
    1.79 +(* comparing variables *)
    1.80  
    1.81  fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
    1.82  
    1.83 @@ -1071,6 +1050,10 @@
    1.84  
    1.85  (** Identifying first-order terms **)
    1.86  
    1.87 +(*Differs from proofterm/is_fun in its treatment of TVar*)
    1.88 +fun is_funtype (Type("fun",[_,_])) = true
    1.89 +  | is_funtype _ = false;
    1.90 +
    1.91  (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
    1.92  fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t)));
    1.93  
    1.94 @@ -1237,11 +1220,8 @@
    1.95  
    1.96  fun term_frees t = add_term_frees(t,[]);
    1.97  
    1.98 -(*Given an abstraction over P, replaces the bound variable by a Free variable
    1.99 -  having a unique name -- SLOW!*)
   1.100 -fun variant_abs (x, T, b) =
   1.101 -  let val ([x'], _) = Name.variants [x] (declare_term_names b Name.context)
   1.102 -  in (x', subst_bound (Free (x', T), b))  end;
   1.103 +
   1.104 +(* dest abstraction *)
   1.105  
   1.106  fun dest_abs (x, T, body) =
   1.107    let