tuned maxidx_of_typ/typs/term;
authorwenzelm
Wed Jul 06 10:41:44 2005 +0200 (2005-07-06)
changeset 167103d6335ff3982
parent 16709 a4679ac06502
child 16711 2c1f9640b744
tuned maxidx_of_typ/typs/term;
moved adhoc string_of_term to HOL/Tools/ATP/recon_translate_proof.ML;
cleaned signature;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Wed Jul 06 10:41:43 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Wed Jul 06 10:41:44 2005 +0200
     1.3 @@ -30,30 +30,31 @@
     1.4      op $ of term * term
     1.5    exception TYPE of string * typ list * term list
     1.6    exception TERM of string * term list
     1.7 +  val dummyT: typ
     1.8 +  val no_dummyT: typ -> typ
     1.9    val --> : typ * typ -> typ
    1.10    val ---> : typ list * typ -> typ
    1.11 +  val dest_Type: typ -> string * typ list
    1.12 +  val dest_TVar: typ -> indexname * sort
    1.13 +  val dest_TFree: typ -> string * sort
    1.14 +  val is_Bound: term -> bool
    1.15 +  val is_Const: term -> bool
    1.16 +  val is_Free: term -> bool
    1.17 +  val is_Var: term -> bool
    1.18    val is_TVar: typ -> bool
    1.19    val is_funtype: typ -> bool
    1.20 +  val dest_Const: term -> string * typ
    1.21 +  val dest_Free: term -> string * typ
    1.22 +  val dest_Var: term -> indexname * typ
    1.23    val domain_type: typ -> typ
    1.24    val range_type: typ -> typ
    1.25    val binder_types: typ -> typ list
    1.26    val body_type: typ -> typ
    1.27    val strip_type: typ -> typ list * typ
    1.28 -  val is_Bound: term -> bool
    1.29 -  val is_Const: term -> bool
    1.30 -  val is_Free: term -> bool
    1.31 -  val is_Var: term -> bool
    1.32 -  val is_first_order: string list -> term -> bool
    1.33 -  val dest_Type: typ -> string * typ list
    1.34 -  val dest_TVar: typ -> indexname * sort
    1.35 -  val dest_TFree: typ -> string * sort
    1.36 -  val dest_Const: term -> string * typ
    1.37 -  val dest_Free: term -> string * typ
    1.38 -  val dest_Var: term -> indexname * typ
    1.39 +  val type_of1: typ list * term -> typ
    1.40    val type_of: term -> typ
    1.41 -  val type_of1: typ list * term -> typ
    1.42 +  val fastype_of1: typ list * term -> typ
    1.43    val fastype_of: term -> typ
    1.44 -  val fastype_of1: typ list * term -> typ
    1.45    val list_abs: (string * typ) list * term -> term
    1.46    val strip_abs_body: term -> term
    1.47    val strip_abs_vars: term -> (string * typ) list
    1.48 @@ -67,19 +68,11 @@
    1.49    val map_type_tfree: (string * sort -> typ) -> typ -> typ
    1.50    val map_term_types: (typ -> typ) -> term -> term
    1.51    val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
    1.52 +  val aconv: term * term -> bool
    1.53 +  val aconvs: term list * term list -> bool
    1.54    structure Vartab: TABLE
    1.55    structure Typtab: TABLE
    1.56    structure Termtab: TABLE
    1.57 -  val aconv: term * term -> bool
    1.58 -  val aconvs: term list * term list -> bool
    1.59 -  val foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a
    1.60 -  val foldl_term_types: (term -> 'a * typ -> 'a) -> 'a * term -> 'a
    1.61 -  val foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a
    1.62 -  val foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a
    1.63 -  val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term
    1.64 -  val add_term_varnames: indexname list * term -> indexname list
    1.65 -  val term_varnames: term -> indexname list
    1.66 -  val dummyT: typ
    1.67    val itselfT: typ -> typ
    1.68    val a_itselfT: typ
    1.69    val propT: typ
    1.70 @@ -96,7 +89,6 @@
    1.71    val loose_bvar1: term * int -> bool
    1.72    val subst_bounds: term list * term -> term
    1.73    val subst_bound: term * term -> term
    1.74 -  val subst_TVars: (indexname * typ) list -> term -> term
    1.75    val betapply: term * term -> term
    1.76    val eq_ix: indexname * indexname -> bool
    1.77    val ins_ix: indexname * indexname list -> indexname list
    1.78 @@ -109,61 +101,69 @@
    1.79    val inter_term: term list * term list -> term list
    1.80    val could_unify: term * term -> bool
    1.81    val subst_free: (term * term) list -> term -> term
    1.82 -  val subst_atomic: (term * term) list -> term -> term
    1.83 -  val typ_subst_atomic: (typ * typ) list -> typ -> typ
    1.84 -  val subst_atomic_types: (typ * typ) list -> term -> term
    1.85 -  val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
    1.86 -  val typ_subst_TVars: (indexname * typ) list -> typ -> typ
    1.87 -  val subst_Vars: (indexname * term) list -> term -> term
    1.88 -  val incr_tvar: int -> typ -> typ
    1.89    val xless: (string * int) * indexname -> bool
    1.90 -  val atless: term * term -> bool
    1.91 -  val insert_aterm: term * term list -> term list
    1.92    val abstract_over: term * term -> term
    1.93    val lambda: term -> term -> term
    1.94    val absfree: string * typ * term -> term
    1.95    val list_abs_free: (string * typ) list * term -> term
    1.96    val list_all_free: (string * typ) list * term -> term
    1.97    val list_all: (string * typ) list * term -> term
    1.98 +  val subst_atomic: (term * term) list -> term -> term
    1.99 +  val typ_subst_atomic: (typ * typ) list -> typ -> typ
   1.100 +  val subst_atomic_types: (typ * typ) list -> term -> term
   1.101 +  val typ_subst_TVars: (indexname * typ) list -> typ -> typ
   1.102 +  val subst_TVars: (indexname * typ) list -> term -> term
   1.103 +  val subst_Vars: (indexname * term) list -> term -> term
   1.104 +  val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
   1.105 +  val is_first_order: string list -> term -> bool
   1.106    val maxidx_of_typ: typ -> int
   1.107    val maxidx_of_typs: typ list -> int
   1.108    val maxidx_of_term: term -> int
   1.109 -  val maxidx_of_terms: term list -> int
   1.110 +  val incr_tvar: int -> typ -> typ
   1.111    val variant: string list -> string -> string
   1.112    val variantlist: string list * string list -> string list
   1.113      (*note reversed order of args wrt. variant!*)
   1.114 -  val variant_abs: string * typ * term -> string * term
   1.115 -  val rename_wrt_term: term -> (string * typ) list -> (string * typ) list
   1.116 -  val add_new_id: string list * string -> string list
   1.117    val add_typ_classes: typ * class list -> class list
   1.118 -  val add_typ_ixns: indexname list * typ -> indexname list
   1.119 -  val add_typ_tfree_names: typ * string list -> string list
   1.120 -  val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
   1.121 -  val typ_tfrees: typ -> (string * sort) list
   1.122 -  val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
   1.123 -  val typ_tvars: typ -> (indexname * sort) list
   1.124    val add_typ_tycons: typ * string list -> string list
   1.125 -  val add_typ_varnames: typ * string list -> string list
   1.126    val add_term_classes: term * class list -> class list
   1.127 +  val add_term_tycons: term * string list -> string list
   1.128    val add_term_consts: term * string list -> string list
   1.129 +  val add_term_constsT: term * (string * typ) list -> (string * typ) list
   1.130    val term_consts: term -> string list
   1.131    val term_constsT: term -> (string * typ) list
   1.132 +  val exists_Const: (string * typ -> bool) -> term -> bool
   1.133 +  val exists_subterm: (term -> bool) -> term -> bool
   1.134 +  val add_new_id: string list * string -> string list
   1.135 +  val add_term_free_names: term * string list -> string list
   1.136 +  val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
   1.137 +  val add_typ_tfree_names: typ * string list -> string list
   1.138 +  val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
   1.139 +  val add_typ_varnames: typ * string list -> string list
   1.140 +  val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   1.141 +  val add_term_tfrees: term * (string * sort) list -> (string * sort) list
   1.142 +  val add_term_tfree_names: term * string list -> string list
   1.143 +  val add_term_tvarnames: term * string list -> string list
   1.144 +  val typ_tfrees: typ -> (string * sort) list
   1.145 +  val typ_tvars: typ -> (indexname * sort) list
   1.146 +  val term_tfrees: term -> (string * sort) list
   1.147 +  val term_tvars: term -> (indexname * sort) list
   1.148 +  val add_typ_ixns: indexname list * typ -> indexname list
   1.149 +  val add_term_tvar_ixns: term * indexname list -> indexname list
   1.150 +  val atless: term * term -> bool
   1.151 +  val insert_aterm: term * term list -> term list
   1.152 +  val add_term_vars: term * term list -> term list
   1.153 +  val term_vars: term -> term list
   1.154    val add_term_frees: term * term list -> term list
   1.155    val term_frees: term -> term list
   1.156 -  val add_term_free_names: term * string list -> string list
   1.157 +  val variant_abs: string * typ * term -> string * term
   1.158 +  val rename_wrt_term: term -> (string * typ) list -> (string * typ) list
   1.159 +  val foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a
   1.160 +  val foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a
   1.161 +  val foldl_term_types: (term -> 'a * typ -> 'a) -> 'a * term -> 'a
   1.162 +  val foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a
   1.163    val add_term_names: term * string list -> string list
   1.164 -  val add_term_tfree_names: term * string list -> string list
   1.165 -  val add_term_tfrees: term * (string * sort) list -> (string * sort) list
   1.166 -  val term_tfrees: term -> (string * sort) list
   1.167 -  val add_term_tvar_ixns: term * indexname list -> indexname list
   1.168 -  val add_term_tvarnames: term * string list -> string list
   1.169 -  val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   1.170 -  val term_tvars: term -> (indexname * sort) list
   1.171 -  val add_term_tycons: term * string list -> string list
   1.172 -  val add_term_vars: term * term list -> term list
   1.173 -  val term_vars: term -> term list
   1.174 -  val exists_Const: (string * typ -> bool) -> term -> bool
   1.175 -  val exists_subterm: (term -> bool) -> term -> bool
   1.176 +  val add_term_varnames: indexname list * term -> indexname list
   1.177 +  val term_varnames: term -> indexname list
   1.178    val compress_type: typ -> typ
   1.179    val compress_term: term -> term
   1.180    val show_question_marks: bool ref
   1.181 @@ -172,6 +172,7 @@
   1.182  signature TERM =
   1.183  sig
   1.184    include BASIC_TERM
   1.185 +  val argument_type_of: term -> typ
   1.186    val fast_indexname_ord: indexname * indexname -> order
   1.187    val indexname_ord: indexname * indexname -> order
   1.188    val sort_ord: sort * sort -> order
   1.189 @@ -183,16 +184,17 @@
   1.190    val term_lpo: (string -> int) -> term * term -> order
   1.191    val match_bvars: (term * term) * (string * string) list -> (string * string) list
   1.192    val rename_abs: term -> term -> term -> term option
   1.193 -  val argument_type_of: term -> typ
   1.194 +  val maxidx_typ: typ -> int -> int
   1.195 +  val maxidx_typs: typ list -> int -> int
   1.196 +  val maxidx_term: term -> int -> int
   1.197    val invent_names: string list -> string -> int -> string list
   1.198    val map_typ: (string -> string) -> (string -> string) -> typ -> typ
   1.199    val map_term: (string -> string) -> (string -> string) -> (string -> string) -> term -> term
   1.200 +  val dest_abs: string * typ * term -> string * term
   1.201    val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
   1.202    val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
   1.203    val add_vars: (indexname * typ) list * term -> (indexname * typ) list
   1.204    val add_frees: (string * typ) list * term -> (string * typ) list
   1.205 -  val dest_abs: string * typ * term -> string * term
   1.206 -  val no_dummyT: typ -> typ
   1.207    val dummy_patternN: string
   1.208    val no_dummy_patterns: term -> term
   1.209    val replace_dummy_patterns: int * term -> int * term
   1.210 @@ -201,7 +203,6 @@
   1.211    val adhoc_freeze_vars: term -> term * string list
   1.212    val string_of_vname: indexname -> string
   1.213    val string_of_vname': indexname -> string
   1.214 -  val string_of_term: term -> string
   1.215  end;
   1.216  
   1.217  structure Term: TERM =
   1.218 @@ -942,23 +943,25 @@
   1.219                 | _ => error "first_order: unexpected case"
   1.220      in  first_order1 []  end;
   1.221  
   1.222 -(*Computing the maximum index of a typ*)
   1.223 -fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts
   1.224 -  | maxidx_of_typ(TFree _) = ~1
   1.225 -  | maxidx_of_typ(TVar((_,i),_)) = i
   1.226 -and maxidx_of_typs [] = ~1
   1.227 -  | maxidx_of_typs (T::Ts) = Int.max(maxidx_of_typ T, maxidx_of_typs Ts);
   1.228 +
   1.229 +(* maximum index of a typs and terms *)
   1.230  
   1.231 +fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j)
   1.232 +  | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i
   1.233 +  | maxidx_typ (TFree _) i = i
   1.234 +and maxidx_typs [] i = i
   1.235 +  | maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i);
   1.236  
   1.237 -(*Computing the maximum index of a term*)
   1.238 -fun maxidx_of_term (Const(_,T)) = maxidx_of_typ T
   1.239 -  | maxidx_of_term (Bound _) = ~1
   1.240 -  | maxidx_of_term (Free(_,T)) = maxidx_of_typ T
   1.241 -  | maxidx_of_term (Var ((_,i), T)) = Int.max(i, maxidx_of_typ T)
   1.242 -  | maxidx_of_term (Abs (_,T,u)) = Int.max(maxidx_of_term u, maxidx_of_typ T)
   1.243 -  | maxidx_of_term (f$t) = Int.max(maxidx_of_term f,  maxidx_of_term t);
   1.244 +fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j))
   1.245 +  | maxidx_term (Const (_, T)) i = maxidx_typ T i
   1.246 +  | maxidx_term (Free (_, T)) i = maxidx_typ T i
   1.247 +  | maxidx_term (Bound _) i = i
   1.248 +  | maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i)
   1.249 +  | maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i);
   1.250  
   1.251 -fun maxidx_of_terms ts = Library.foldl Int.max (~1, map maxidx_of_term ts);
   1.252 +fun maxidx_of_typ T = maxidx_typ T ~1;
   1.253 +fun maxidx_of_typs Ts = maxidx_typs Ts ~1;
   1.254 +fun maxidx_of_term t = maxidx_term t ~1;
   1.255  
   1.256  
   1.257  (* Increment the index of all Poly's in T by k *)
   1.258 @@ -1193,13 +1196,6 @@
   1.259    | foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t)
   1.260    | foldl_aterms f x_atom = f x_atom;
   1.261  
   1.262 -fun foldl_map_aterms f (x, t $ u) =
   1.263 -      let val (x', t') = foldl_map_aterms f (x, t); val (x'', u') = foldl_map_aterms f (x', u);
   1.264 -      in (x'', t' $ u') end
   1.265 -  | foldl_map_aterms f (x, Abs (a, T, t)) =
   1.266 -      let val (x', t') = foldl_map_aterms f (x, t) in (x', Abs (a, T, t')) end
   1.267 -  | foldl_map_aterms f x_atom = f x_atom;
   1.268 -
   1.269  (*foldl types of term*)
   1.270  fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T)
   1.271    | foldl_term_types f (x, t as Free (_, T)) = f t (x, T)
   1.272 @@ -1320,14 +1316,6 @@
   1.273  fun string_of_vname' (x, ~1) = x
   1.274    | string_of_vname' xi = string_of_vname xi;
   1.275  
   1.276 -fun string_of_term (Const(s,_)) = s
   1.277 -  | string_of_term (Free(s,_)) = s
   1.278 -  | string_of_term (Var(ix,_)) = string_of_vname ix
   1.279 -  | string_of_term (Bound i) = string_of_int i
   1.280 -  | string_of_term (Abs(x,_,t)) = "%" ^ x ^ ". " ^ string_of_term t
   1.281 -  | string_of_term (s $ t) =
   1.282 -      "(" ^ string_of_term s ^ " " ^ string_of_term t ^ ")"
   1.283 -
   1.284  end;
   1.285  
   1.286  structure BasicTerm: BASIC_TERM = Term;