1(* Title: Pure/term.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Author: Makarius 4 5Simply typed lambda-calculus: types, terms, and basic operations. 6*) 7 8infix 9 $; 9infixr 5 -->; 10infixr --->; 11infix aconv; 12 13signature BASIC_TERM = 14sig 15 type indexname = string * int 16 type class = string 17 type sort = class list 18 type arity = string * sort list * sort 19 datatype typ = 20 Type of string * typ list | 21 TFree of string * sort | 22 TVar of indexname * sort 23 datatype term = 24 Const of string * typ | 25 Free of string * typ | 26 Var of indexname * typ | 27 Bound of int | 28 Abs of string * typ * term | 29 $ of term * term 30 exception TYPE of string * typ list * term list 31 exception TERM of string * term list 32 val dummyS: sort 33 val dummyT: typ 34 val no_dummyT: typ -> typ 35 val --> : typ * typ -> typ 36 val ---> : typ list * typ -> typ 37 val is_Type: typ -> bool 38 val is_TFree: typ -> bool 39 val is_TVar: typ -> bool 40 val dest_Type: typ -> string * typ list 41 val dest_TFree: typ -> string * sort 42 val dest_TVar: typ -> indexname * sort 43 val is_Bound: term -> bool 44 val is_Const: term -> bool 45 val is_Free: term -> bool 46 val is_Var: term -> bool 47 val dest_Const: term -> string * typ 48 val dest_Free: term -> string * typ 49 val dest_Var: term -> indexname * typ 50 val dest_comb: term -> term * term 51 val domain_type: typ -> typ 52 val range_type: typ -> typ 53 val dest_funT: typ -> typ * typ 54 val binder_types: typ -> typ list 55 val body_type: typ -> typ 56 val strip_type: typ -> typ list * typ 57 val type_of1: typ list * term -> typ 58 val type_of: term -> typ 59 val fastype_of1: typ list * term -> typ 60 val fastype_of: term -> typ 61 val strip_abs: term -> (string * typ) list * term 62 val strip_abs_body: term -> term 63 val strip_abs_vars: term -> (string * typ) list 64 val strip_qnt_body: string -> term -> term 65 val strip_qnt_vars: string -> term -> (string * typ) list 66 val list_comb: term * term list -> term 67 val strip_comb: term -> term * term list 68 val head_of: term -> term 69 val size_of_term: term -> int 70 val size_of_typ: typ -> int 71 val map_atyps: (typ -> typ) -> typ -> typ 72 val map_aterms: (term -> term) -> term -> term 73 val map_type_tvar: (indexname * sort -> typ) -> typ -> typ 74 val map_type_tfree: (string * sort -> typ) -> typ -> typ 75 val map_types: (typ -> typ) -> term -> term 76 val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a 77 val fold_atyps_sorts: (typ * sort -> 'a -> 'a) -> typ -> 'a -> 'a 78 val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a 79 val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a 80 val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a 81 val burrow_types: (typ list -> typ list) -> term list -> term list 82 val aconv: term * term -> bool 83 val propT: typ 84 val strip_all_body: term -> term 85 val strip_all_vars: term -> (string * typ) list 86 val incr_bv: int * int * term -> term 87 val incr_boundvars: int -> term -> term 88 val add_loose_bnos: term * int * int list -> int list 89 val loose_bnos: term -> int list 90 val loose_bvar: term * int -> bool 91 val loose_bvar1: term * int -> bool 92 val subst_bounds: term list * term -> term 93 val subst_bound: term * term -> term 94 val betapply: term * term -> term 95 val betapplys: term * term list -> term 96 val subst_free: (term * term) list -> term -> term 97 val abstract_over: term * term -> term 98 val lambda: term -> term -> term 99 val absfree: string * typ -> term -> term 100 val absdummy: typ -> term -> term 101 val subst_atomic: (term * term) list -> term -> term 102 val typ_subst_atomic: (typ * typ) list -> typ -> typ 103 val subst_atomic_types: (typ * typ) list -> term -> term 104 val typ_subst_TVars: (indexname * typ) list -> typ -> typ 105 val subst_TVars: (indexname * typ) list -> term -> term 106 val subst_Vars: (indexname * term) list -> term -> term 107 val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term 108 val is_first_order: string list -> term -> bool 109 val maxidx_of_typ: typ -> int 110 val maxidx_of_typs: typ list -> int 111 val maxidx_of_term: term -> int 112 val fold_subtypes: (typ -> 'a -> 'a) -> typ -> 'a -> 'a 113 val exists_subtype: (typ -> bool) -> typ -> bool 114 val exists_type: (typ -> bool) -> term -> bool 115 val exists_subterm: (term -> bool) -> term -> bool 116 val exists_Const: (string * typ -> bool) -> term -> bool 117end; 118 119signature TERM = 120sig 121 include BASIC_TERM 122 val aT: sort -> typ 123 val itselfT: typ -> typ 124 val a_itselfT: typ 125 val argument_type_of: term -> int -> typ 126 val abs: string * typ -> term -> term 127 val add_tvar_namesT: typ -> indexname list -> indexname list 128 val add_tvar_names: term -> indexname list -> indexname list 129 val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list 130 val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list 131 val add_var_names: term -> indexname list -> indexname list 132 val add_vars: term -> (indexname * typ) list -> (indexname * typ) list 133 val add_tfree_namesT: typ -> string list -> string list 134 val add_tfree_names: term -> string list -> string list 135 val add_tfreesT: typ -> (string * sort) list -> (string * sort) list 136 val add_tfrees: term -> (string * sort) list -> (string * sort) list 137 val add_free_names: term -> string list -> string list 138 val add_frees: term -> (string * typ) list -> (string * typ) list 139 val add_const_names: term -> string list -> string list 140 val add_consts: term -> (string * typ) list -> (string * typ) list 141 val hidden_polymorphism: term -> (indexname * sort) list 142 val declare_typ_names: typ -> Name.context -> Name.context 143 val declare_term_names: term -> Name.context -> Name.context 144 val declare_term_frees: term -> Name.context -> Name.context 145 val variant_frees: term -> (string * 'a) list -> (string * 'a) list 146 val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list 147 val eq_ix: indexname * indexname -> bool 148 val eq_tvar: (indexname * sort) * (indexname * sort) -> bool 149 val eq_var: (indexname * typ) * (indexname * typ) -> bool 150 val aconv_untyped: term * term -> bool 151 val could_unify: term * term -> bool 152 val strip_abs_eta: int -> term -> (string * typ) list * term 153 val match_bvars: (term * term) -> (string * string) list -> (string * string) list 154 val map_abs_vars: (string -> string) -> term -> term 155 val rename_abs: term -> term -> term -> term option 156 val is_open: term -> bool 157 val is_dependent: term -> bool 158 val term_name: term -> string 159 val dependent_lambda_name: string * term -> term -> term 160 val lambda_name: string * term -> term -> term 161 val close_schematic_term: term -> term 162 val maxidx_typ: typ -> int -> int 163 val maxidx_typs: typ list -> int -> int 164 val maxidx_term: term -> int -> int 165 val could_beta_contract: term -> bool 166 val could_eta_contract: term -> bool 167 val could_beta_eta_contract: term -> bool 168 val dest_abs: string * typ * term -> string * term 169 val dummy_pattern: typ -> term 170 val dummy: term 171 val dummy_prop: term 172 val is_dummy_pattern: term -> bool 173 val free_dummy_patterns: term -> Name.context -> term * Name.context 174 val no_dummy_patterns: term -> term 175 val replace_dummy_patterns: term -> int -> term * int 176 val show_dummy_patterns: term -> term 177 val string_of_vname: indexname -> string 178 val string_of_vname': indexname -> string 179end; 180 181structure Term: TERM = 182struct 183 184(*Indexnames can be quickly renamed by adding an offset to the integer part, 185 for resolution.*) 186type indexname = string * int; 187 188(*Types are classified by sorts.*) 189type class = string; 190type sort = class list; 191type arity = string * sort list * sort; 192 193(*The sorts attached to TFrees and TVars specify the sort of that variable.*) 194datatype typ = Type of string * typ list 195 | TFree of string * sort 196 | TVar of indexname * sort; 197 198(*Terms. Bound variables are indicated by depth number. 199 Free variables, (scheme) variables and constants have names. 200 An term is "closed" if every bound variable of level "lev" 201 is enclosed by at least "lev" abstractions. 202 203 It is possible to create meaningless terms containing loose bound vars 204 or type mismatches. But such terms are not allowed in rules. *) 205 206datatype term = 207 Const of string * typ 208 | Free of string * typ 209 | Var of indexname * typ 210 | Bound of int 211 | Abs of string*typ*term 212 | op $ of term*term; 213 214(*Errors involving type mismatches*) 215exception TYPE of string * typ list * term list; 216 217(*Errors errors involving terms*) 218exception TERM of string * term list; 219 220(*Note variable naming conventions! 221 a,b,c: string 222 f,g,h: functions (including terms of function type) 223 i,j,m,n: int 224 t,u: term 225 v,w: indexnames 226 x,y: any 227 A,B,C: term (denoting formulae) 228 T,U: typ 229*) 230 231 232(** Types **) 233 234(*dummies for type-inference etc.*) 235val dummyS = [""]; 236val dummyT = Type ("dummy", []); 237 238fun no_dummyT typ = 239 let 240 fun check (T as Type ("dummy", _)) = 241 raise TYPE ("Illegal occurrence of '_' dummy type", [T], []) 242 | check (Type (_, Ts)) = List.app check Ts 243 | check _ = (); 244 in check typ; typ end; 245 246fun S --> T = Type("fun",[S,T]); 247 248(*handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)*) 249val op ---> = Library.foldr (op -->); 250 251 252(** Discriminators **) 253 254fun is_Type (Type _) = true 255 | is_Type _ = false; 256 257fun is_TFree (TFree _) = true 258 | is_TFree _ = false; 259 260fun is_TVar (TVar _) = true 261 | is_TVar _ = false; 262 263 264(** Destructors **) 265 266fun dest_Type (Type x) = x 267 | dest_Type T = raise TYPE ("dest_Type", [T], []); 268 269fun dest_TFree (TFree x) = x 270 | dest_TFree T = raise TYPE ("dest_TFree", [T], []); 271 272fun dest_TVar (TVar x) = x 273 | dest_TVar T = raise TYPE ("dest_TVar", [T], []); 274 275 276(** Discriminators **) 277 278fun is_Bound (Bound _) = true 279 | is_Bound _ = false; 280 281fun is_Const (Const _) = true 282 | is_Const _ = false; 283 284fun is_Free (Free _) = true 285 | is_Free _ = false; 286 287fun is_Var (Var _) = true 288 | is_Var _ = false; 289 290 291(** Destructors **) 292 293fun dest_Const (Const x) = x 294 | dest_Const t = raise TERM("dest_Const", [t]); 295 296fun dest_Free (Free x) = x 297 | dest_Free t = raise TERM("dest_Free", [t]); 298 299fun dest_Var (Var x) = x 300 | dest_Var t = raise TERM("dest_Var", [t]); 301 302fun dest_comb (t1 $ t2) = (t1, t2) 303 | dest_comb t = raise TERM("dest_comb", [t]); 304 305 306fun domain_type (Type ("fun", [T, _])) = T; 307 308fun range_type (Type ("fun", [_, U])) = U; 309 310fun dest_funT (Type ("fun", [T, U])) = (T, U) 311 | dest_funT T = raise TYPE ("dest_funT", [T], []); 312 313 314(*maps [T1,...,Tn]--->T to the list [T1,T2,...,Tn]*) 315fun binder_types (Type ("fun", [T, U])) = T :: binder_types U 316 | binder_types _ = []; 317 318(*maps [T1,...,Tn]--->T to T*) 319fun body_type (Type ("fun", [_, U])) = body_type U 320 | body_type T = T; 321 322(*maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T)*) 323fun strip_type T = (binder_types T, body_type T); 324 325 326(*Compute the type of the term, checking that combinations are well-typed 327 Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*) 328fun type_of1 (Ts, Const (_,T)) = T 329 | type_of1 (Ts, Free (_,T)) = T 330 | type_of1 (Ts, Bound i) = (nth Ts i 331 handle General.Subscript => raise TYPE("type_of: bound variable", [], [Bound i])) 332 | type_of1 (Ts, Var (_,T)) = T 333 | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body) 334 | type_of1 (Ts, f$u) = 335 let val U = type_of1(Ts,u) 336 and T = type_of1(Ts,f) 337 in case T of 338 Type("fun",[T1,T2]) => 339 if T1=U then T2 else raise TYPE 340 ("type_of: type mismatch in application", [T1,U], [f$u]) 341 | _ => raise TYPE 342 ("type_of: function type is expected in application", 343 [T,U], [f$u]) 344 end; 345 346fun type_of t : typ = type_of1 ([],t); 347 348(*Determines the type of a term, with minimal checking*) 349fun fastype_of1 (Ts, f$u) = 350 (case fastype_of1 (Ts,f) of 351 Type("fun",[_,T]) => T 352 | _ => raise TERM("fastype_of: expected function type", [f$u])) 353 | fastype_of1 (_, Const (_,T)) = T 354 | fastype_of1 (_, Free (_,T)) = T 355 | fastype_of1 (Ts, Bound i) = (nth Ts i 356 handle General.Subscript => raise TERM("fastype_of: Bound", [Bound i])) 357 | fastype_of1 (_, Var (_,T)) = T 358 | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u); 359 360fun fastype_of t : typ = fastype_of1 ([],t); 361 362(*Determine the argument type of a function*) 363fun argument_type_of tm k = 364 let 365 fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i - 1) U 366 | argT _ T = raise TYPE ("argument_type_of", [T], []); 367 368 fun arg 0 _ (Abs (_, T, _)) = T 369 | arg i Ts (Abs (_, T, t)) = arg (i - 1) (T :: Ts) t 370 | arg i Ts (t $ _) = arg (i + 1) Ts t 371 | arg i Ts a = argT i (fastype_of1 (Ts, a)); 372 in arg k [] tm end; 373 374 375fun abs (x, T) t = Abs (x, T, t); 376 377fun strip_abs (Abs (a, T, t)) = 378 let val (a', t') = strip_abs t 379 in ((a, T) :: a', t') end 380 | strip_abs t = ([], t); 381 382(*maps (x1,...,xn)t to t*) 383fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t 384 | strip_abs_body u = u; 385 386(*maps (x1,...,xn)t to [x1, ..., xn]*) 387fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t 388 | strip_abs_vars u = [] : (string*typ) list; 389 390 391fun strip_qnt_body qnt = 392let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm 393 | strip t = t 394in strip end; 395 396fun strip_qnt_vars qnt = 397let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else [] 398 | strip t = [] : (string*typ) list 399in strip end; 400 401 402(*maps (f, [t1,...,tn]) to f(t1,...,tn)*) 403val list_comb : term * term list -> term = Library.foldl (op $); 404 405 406(*maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tail-recursive*) 407fun strip_comb u : term * term list = 408 let fun stripc (f$t, ts) = stripc (f, t::ts) 409 | stripc x = x 410 in stripc(u,[]) end; 411 412 413(*maps f(t1,...,tn) to f , which is never a combination*) 414fun head_of (f$t) = head_of f 415 | head_of u = u; 416 417(*number of atoms and abstractions in a term*) 418fun size_of_term tm = 419 let 420 fun add_size (t $ u) n = add_size t (add_size u n) 421 | add_size (Abs (_ ,_, t)) n = add_size t (n + 1) 422 | add_size _ n = n + 1; 423 in add_size tm 0 end; 424 425(*number of atoms and constructors in a type*) 426fun size_of_typ ty = 427 let 428 fun add_size (Type (_, tys)) n = fold add_size tys (n + 1) 429 | add_size _ n = n + 1; 430 in add_size ty 0 end; 431 432fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts) 433 | map_atyps f T = f T; 434 435fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u 436 | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t) 437 | map_aterms f t = f t; 438 439fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T); 440fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T); 441 442fun map_types f = 443 let 444 fun map_aux (Const (a, T)) = Const (a, f T) 445 | map_aux (Free (a, T)) = Free (a, f T) 446 | map_aux (Var (v, T)) = Var (v, f T) 447 | map_aux (Bound i) = Bound i 448 | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t) 449 | map_aux (t $ u) = map_aux t $ map_aux u; 450 in map_aux end; 451 452 453(* fold types and terms *) 454 455fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts 456 | fold_atyps f T = f T; 457 458fun fold_atyps_sorts f = 459 fold_atyps (fn T as TFree (_, S) => f (T, S) | T as TVar (_, S) => f (T, S)); 460 461fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u 462 | fold_aterms f (Abs (_, _, t)) = fold_aterms f t 463 | fold_aterms f a = f a; 464 465fun fold_term_types f (t as Const (_, T)) = f t T 466 | fold_term_types f (t as Free (_, T)) = f t T 467 | fold_term_types f (t as Var (_, T)) = f t T 468 | fold_term_types f (Bound _) = I 469 | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b 470 | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u; 471 472fun fold_types f = fold_term_types (K f); 473 474fun replace_types (Const (c, _)) (T :: Ts) = (Const (c, T), Ts) 475 | replace_types (Free (x, _)) (T :: Ts) = (Free (x, T), Ts) 476 | replace_types (Var (xi, _)) (T :: Ts) = (Var (xi, T), Ts) 477 | replace_types (Bound i) Ts = (Bound i, Ts) 478 | replace_types (Abs (x, _, b)) (T :: Ts) = 479 let val (b', Ts') = replace_types b Ts 480 in (Abs (x, T, b'), Ts') end 481 | replace_types (t $ u) Ts = 482 let 483 val (t', Ts') = replace_types t Ts; 484 val (u', Ts'') = replace_types u Ts'; 485 in (t' $ u', Ts'') end; 486 487fun burrow_types f ts = 488 let 489 val Ts = rev ((fold o fold_types) cons ts []); 490 val Ts' = f Ts; 491 val (ts', []) = fold_map replace_types ts Ts'; 492 in ts' end; 493 494(*collect variables*) 495val add_tvar_namesT = fold_atyps (fn TVar (xi, _) => insert (op =) xi | _ => I); 496val add_tvar_names = fold_types add_tvar_namesT; 497val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I); 498val add_tvars = fold_types add_tvarsT; 499val add_var_names = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I); 500val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I); 501val add_tfree_namesT = fold_atyps (fn TFree (a, _) => insert (op =) a | _ => I); 502val add_tfree_names = fold_types add_tfree_namesT; 503val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I); 504val add_tfrees = fold_types add_tfreesT; 505val add_free_names = fold_aterms (fn Free (x, _) => insert (op =) x | _ => I); 506val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I); 507val add_const_names = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I); 508val add_consts = fold_aterms (fn Const c => insert (op =) c | _ => I); 509 510(*extra type variables in a term, not covered by its type*) 511fun hidden_polymorphism t = 512 let 513 val T = fastype_of t; 514 val tvarsT = add_tvarsT T []; 515 val extra_tvars = fold_types (fold_atyps 516 (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t []; 517 in extra_tvars end; 518 519 520(* renaming variables *) 521 522val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I); 523 524fun declare_term_names tm = 525 fold_aterms 526 (fn Const (a, _) => Name.declare (Long_Name.base_name a) 527 | Free (a, _) => Name.declare a 528 | _ => I) tm #> 529 fold_types declare_typ_names tm; 530 531val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I); 532 533fun variant_frees t frees = 534 fst (fold_map Name.variant (map fst frees) (declare_term_names t Name.context)) ~~ 535 map snd frees; 536 537fun rename_wrt_term t frees = rev (variant_frees t frees); (*reversed result!*) 538 539 540 541(** Comparing terms **) 542 543(* variables *) 544 545fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y; 546 547fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S'; 548fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T'; 549 550 551(* alpha equivalence *) 552 553fun tm1 aconv tm2 = 554 pointer_eq (tm1, tm2) orelse 555 (case (tm1, tm2) of 556 (t1 $ u1, t2 $ u2) => t1 aconv t2 andalso u1 aconv u2 557 | (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2 558 | (a1, a2) => a1 = a2); 559 560fun aconv_untyped (tm1, tm2) = 561 pointer_eq (tm1, tm2) orelse 562 (case (tm1, tm2) of 563 (t1 $ u1, t2 $ u2) => aconv_untyped (t1, t2) andalso aconv_untyped (u1, u2) 564 | (Abs (_, _, t1), Abs (_, _, t2)) => aconv_untyped (t1, t2) 565 | (Const (a, _), Const (b, _)) => a = b 566 | (Free (x, _), Free (y, _)) => x = y 567 | (Var (xi, _), Var (yj, _)) => xi = yj 568 | (Bound i, Bound j) => i = j 569 | _ => false); 570 571 572(*A fast unification filter: true unless the two terms cannot be unified. 573 Terms must be NORMAL. Treats all Vars as distinct. *) 574fun could_unify (t, u) = 575 let 576 fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g 577 | matchrands _ _ = true; 578 in 579 case (head_of t, head_of u) of 580 (_, Var _) => true 581 | (Var _, _) => true 582 | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u 583 | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u 584 | (Bound i, Bound j) => i = j andalso matchrands t u 585 | (Abs _, _) => true (*because of possible eta equality*) 586 | (_, Abs _) => true 587 | _ => false 588 end; 589 590 591 592(** Connectives of higher order logic **) 593 594fun aT S = TFree (Name.aT, S); 595 596fun itselfT ty = Type ("itself", [ty]); 597val a_itselfT = itselfT (TFree (Name.aT, [])); 598 599val propT : typ = Type ("prop",[]); 600 601(*maps \<And>x1...xn. t to t*) 602fun strip_all_body (Const ("Pure.all", _) $ Abs (_, _, t)) = strip_all_body t 603 | strip_all_body t = t; 604 605(*maps \<And>x1...xn. t to [x1, ..., xn]*) 606fun strip_all_vars (Const ("Pure.all", _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t 607 | strip_all_vars t = []; 608 609(*increments a term's non-local bound variables 610 required when moving a term within abstractions 611 inc is increment for bound variables 612 lev is level at which a bound variable is considered 'loose'*) 613fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u 614 | incr_bv (inc, lev, Abs(a,T,body)) = 615 Abs(a, T, incr_bv(inc,lev+1,body)) 616 | incr_bv (inc, lev, f$t) = 617 incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 618 | incr_bv (inc, lev, u) = u; 619 620fun incr_boundvars 0 t = t 621 | incr_boundvars inc t = incr_bv(inc,0,t); 622 623(*Scan a pair of terms; while they are similar, 624 accumulate corresponding bound vars in "al"*) 625fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = 626 match_bvs(s, t, if x="" orelse y="" then al 627 else (x,y)::al) 628 | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 629 | match_bvs(_,_,al) = al; 630 631(* strip abstractions created by parameters *) 632fun match_bvars (s,t) al = match_bvs(strip_abs_body s, strip_abs_body t, al); 633 634fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u 635 | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t) 636 | map_abs_vars f t = t; 637 638fun rename_abs pat obj t = 639 let 640 val ren = match_bvs (pat, obj, []); 641 fun ren_abs (Abs (x, T, b)) = 642 Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b) 643 | ren_abs (f $ t) = ren_abs f $ ren_abs t 644 | ren_abs t = t 645 in if null ren then NONE else SOME (ren_abs t) end; 646 647(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond. 648 (Bound 0) is loose at level 0 *) 649fun add_loose_bnos (Bound i, lev, js) = 650 if i<lev then js else insert (op =) (i - lev) js 651 | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js) 652 | add_loose_bnos (f$t, lev, js) = 653 add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 654 | add_loose_bnos (_, _, js) = js; 655 656fun loose_bnos t = add_loose_bnos (t, 0, []); 657 658(* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to 659 level k or beyond. *) 660fun loose_bvar(Bound i,k) = i >= k 661 | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k) 662 | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1) 663 | loose_bvar _ = false; 664 665fun loose_bvar1(Bound i,k) = i = k 666 | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 667 | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1) 668 | loose_bvar1 _ = false; 669 670fun is_open t = loose_bvar (t, 0); 671fun is_dependent t = loose_bvar1 (t, 0); 672 673(*Substitute arguments for loose bound variables. 674 Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi). 675 Note that for ((\<lambda>x y. c) a b), the bound vars in c are x=1 and y=0 676 and the appropriate call is subst_bounds([b,a], c) . 677 Loose bound variables >=n are reduced by "n" to 678 compensate for the disappearance of lambdas. 679*) 680fun subst_bounds (args: term list, t) : term = 681 let 682 val n = length args; 683 fun subst (t as Bound i, lev) = 684 (if i < lev then raise Same.SAME (*var is locally bound*) 685 else incr_boundvars lev (nth args (i - lev)) 686 handle General.Subscript => Bound (i - n)) (*loose: change it*) 687 | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1)) 688 | subst (f $ t, lev) = 689 (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t) 690 handle Same.SAME => f $ subst (t, lev)) 691 | subst _ = raise Same.SAME; 692 in case args of [] => t | _ => (subst (t, 0) handle Same.SAME => t) end; 693 694(*Special case: one argument*) 695fun subst_bound (arg, t) : term = 696 let 697 fun subst (Bound i, lev) = 698 if i < lev then raise Same.SAME (*var is locally bound*) 699 else if i = lev then incr_boundvars lev arg 700 else Bound (i - 1) (*loose: change it*) 701 | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1)) 702 | subst (f $ t, lev) = 703 (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t) 704 handle Same.SAME => f $ subst (t, lev)) 705 | subst _ = raise Same.SAME; 706 in subst (t, 0) handle Same.SAME => t end; 707 708(*beta-reduce if possible, else form application*) 709fun betapply (Abs(_,_,t), u) = subst_bound (u,t) 710 | betapply (f,u) = f$u; 711 712val betapplys = Library.foldl betapply; 713 714 715(*unfolding abstractions with substitution 716 of bound variables and implicit eta-expansion*) 717fun strip_abs_eta k t = 718 let 719 val used = fold_aterms declare_term_frees t Name.context; 720 fun strip_abs t (0, used) = (([], t), (0, used)) 721 | strip_abs (Abs (v, T, t)) (k, used) = 722 let 723 val (v', used') = Name.variant v used; 724 val t' = subst_bound (Free (v', T), t); 725 val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used'); 726 in (((v', T) :: vs, t''), (k', used'')) end 727 | strip_abs t (k, used) = (([], t), (k, used)); 728 fun expand_eta [] t _ = ([], t) 729 | expand_eta (T::Ts) t used = 730 let 731 val (v, used') = Name.variant "" used; 732 val (vs, t') = expand_eta Ts (t $ Free (v, T)) used'; 733 in ((v, T) :: vs, t') end; 734 val ((vs1, t'), (k', used')) = strip_abs t (k, used); 735 val Ts = fst (chop k' (binder_types (fastype_of t'))); 736 val (vs2, t'') = expand_eta Ts t' used'; 737 in (vs1 @ vs2, t'') end; 738 739 740(*Substitute new for free occurrences of old in a term*) 741fun subst_free [] = I 742 | subst_free pairs = 743 let fun substf u = 744 case AList.lookup (op aconv) pairs u of 745 SOME u' => u' 746 | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t) 747 | t$u' => substf t $ substf u' 748 | _ => u) 749 in substf end; 750 751(*Abstraction of the term "body" over its occurrences of v, 752 which must contain no loose bound variables. 753 The resulting term is ready to become the body of an Abs.*) 754fun abstract_over (v, body) = 755 let 756 fun abs lev tm = 757 if v aconv tm then Bound lev 758 else 759 (case tm of 760 Abs (a, T, t) => Abs (a, T, abs (lev + 1) t) 761 | t $ u => 762 (abs lev t $ (abs lev u handle Same.SAME => u) 763 handle Same.SAME => t $ abs lev u) 764 | _ => raise Same.SAME); 765 in abs 0 body handle Same.SAME => body end; 766 767fun term_name (Const (x, _)) = Long_Name.base_name x 768 | term_name (Free (x, _)) = x 769 | term_name (Var ((x, _), _)) = x 770 | term_name _ = Name.uu; 771 772fun dependent_lambda_name (x, v) t = 773 let val t' = abstract_over (v, t) 774 in if is_dependent t' then Abs (if x = "" then term_name v else x, fastype_of v, t') else t end; 775 776fun lambda_name (x, v) t = 777 Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t)); 778 779fun lambda v t = lambda_name ("", v) t; 780 781fun absfree (a, T) body = Abs (a, T, abstract_over (Free (a, T), body)); 782fun absdummy T body = Abs (Name.uu_, T, body); 783 784(*Replace the ATOMIC term ti by ui; inst = [(t1,u1), ..., (tn,un)]. 785 A simultaneous substitution: [ (a,b), (b,a) ] swaps a and b. *) 786fun subst_atomic [] tm = tm 787 | subst_atomic inst tm = 788 let 789 fun subst (Abs (a, T, body)) = Abs (a, T, subst body) 790 | subst (t $ u) = subst t $ subst u 791 | subst t = the_default t (AList.lookup (op aconv) inst t); 792 in subst tm end; 793 794(*Replace the ATOMIC type Ti by Ui; inst = [(T1,U1), ..., (Tn,Un)].*) 795fun typ_subst_atomic [] ty = ty 796 | typ_subst_atomic inst ty = 797 let 798 fun subst (Type (a, Ts)) = Type (a, map subst Ts) 799 | subst T = the_default T (AList.lookup (op = : typ * typ -> bool) inst T); 800 in subst ty end; 801 802fun subst_atomic_types [] tm = tm 803 | subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm; 804 805fun typ_subst_TVars [] ty = ty 806 | typ_subst_TVars inst ty = 807 let 808 fun subst (Type (a, Ts)) = Type (a, map subst Ts) 809 | subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi) 810 | subst T = T; 811 in subst ty end; 812 813fun subst_TVars [] tm = tm 814 | subst_TVars inst tm = map_types (typ_subst_TVars inst) tm; 815 816fun subst_Vars [] tm = tm 817 | subst_Vars inst tm = 818 let 819 fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi) 820 | subst (Abs (a, T, t)) = Abs (a, T, subst t) 821 | subst (t $ u) = subst t $ subst u 822 | subst t = t; 823 in subst tm end; 824 825fun subst_vars ([], []) tm = tm 826 | subst_vars ([], inst) tm = subst_Vars inst tm 827 | subst_vars (instT, inst) tm = 828 let 829 fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T) 830 | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T) 831 | subst (Var (xi, T)) = 832 (case AList.lookup (op =) inst xi of 833 NONE => Var (xi, typ_subst_TVars instT T) 834 | SOME t => t) 835 | subst (t as Bound _) = t 836 | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t) 837 | subst (t $ u) = subst t $ subst u; 838 in subst tm end; 839 840fun close_schematic_term t = 841 let 842 val extra_types = map (fn v => Const ("Pure.type", itselfT (TVar v))) (hidden_polymorphism t); 843 val extra_terms = map Var (add_vars t []); 844 in fold lambda (extra_terms @ extra_types) t end; 845 846 847 848(** Identifying first-order terms **) 849 850(*Differs from proofterm/is_fun in its treatment of TVar*) 851fun is_funtype (Type ("fun", [_, _])) = true 852 | is_funtype _ = false; 853 854(*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*) 855fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts, t))); 856 857(*First order means in all terms of the form f(t1,...,tn) no argument has a 858 function type. The supplied quantifiers are excluded: their argument always 859 has a function type through a recursive call into its body.*) 860fun is_first_order quants = 861 let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body 862 | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) = 863 member (op =) quants q andalso (*it is a known quantifier*) 864 not (is_funtype T) andalso first_order1 (T::Ts) body 865 | first_order1 Ts t = 866 case strip_comb t of 867 (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts 868 | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts 869 | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts 870 | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts 871 | (Abs _, ts) => false (*not in beta-normal form*) 872 | _ => error "first_order: unexpected case" 873 in first_order1 [] end; 874 875 876(* maximum index of typs and terms *) 877 878fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j) 879 | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i 880 | maxidx_typ (TFree _) i = i 881and maxidx_typs [] i = i 882 | maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i); 883 884fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j)) 885 | maxidx_term (Const (_, T)) i = maxidx_typ T i 886 | maxidx_term (Free (_, T)) i = maxidx_typ T i 887 | maxidx_term (Bound _) i = i 888 | maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i) 889 | maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i); 890 891fun maxidx_of_typ T = maxidx_typ T ~1; 892fun maxidx_of_typs Ts = maxidx_typs Ts ~1; 893fun maxidx_of_term t = maxidx_term t ~1; 894 895 896 897(** misc syntax operations **) 898 899(* substructure *) 900 901fun fold_subtypes f = 902 let 903 fun iter ty = 904 (case ty of Type (_, Ts) => f ty #> fold iter Ts | _ => f ty); 905 in iter end; 906 907fun exists_subtype P = 908 let 909 fun ex ty = P ty orelse 910 (case ty of Type (_, Ts) => exists ex Ts | _ => false); 911 in ex end; 912 913fun exists_type P = 914 let 915 fun ex (Const (_, T)) = P T 916 | ex (Free (_, T)) = P T 917 | ex (Var (_, T)) = P T 918 | ex (Bound _) = false 919 | ex (Abs (_, T, t)) = P T orelse ex t 920 | ex (t $ u) = ex t orelse ex u; 921 in ex end; 922 923fun exists_subterm P = 924 let 925 fun ex tm = P tm orelse 926 (case tm of 927 t $ u => ex t orelse ex u 928 | Abs (_, _, t) => ex t 929 | _ => false); 930 in ex end; 931 932fun exists_Const P = exists_subterm (fn Const c => P c | _ => false); 933 934 935(* contraction *) 936 937fun could_beta_contract (Abs _ $ _) = true 938 | could_beta_contract (t $ u) = could_beta_contract t orelse could_beta_contract u 939 | could_beta_contract (Abs (_, _, b)) = could_beta_contract b 940 | could_beta_contract _ = false; 941 942fun could_eta_contract (Abs (_, _, _ $ Bound 0)) = true 943 | could_eta_contract (Abs (_, _, b)) = could_eta_contract b 944 | could_eta_contract (t $ u) = could_eta_contract t orelse could_eta_contract u 945 | could_eta_contract _ = false; 946 947fun could_beta_eta_contract (Abs _ $ _) = true 948 | could_beta_eta_contract (Abs (_, _, _ $ Bound 0)) = true 949 | could_beta_eta_contract (Abs (_, _, b)) = could_beta_eta_contract b 950 | could_beta_eta_contract (t $ u) = could_beta_eta_contract t orelse could_beta_eta_contract u 951 | could_beta_eta_contract _ = false; 952 953 954(* dest abstraction *) 955 956fun dest_abs (x, T, body) = 957 let 958 fun name_clash (Free (y, _)) = (x = y) 959 | name_clash (t $ u) = name_clash t orelse name_clash u 960 | name_clash (Abs (_, _, t)) = name_clash t 961 | name_clash _ = false; 962 in 963 if name_clash body then 964 dest_abs (singleton (Name.variant_list [x]) x, T, body) (*potentially slow*) 965 else (x, subst_bound (Free (x, T), body)) 966 end; 967 968 969(* dummy patterns *) 970 971fun dummy_pattern T = Const ("Pure.dummy_pattern", T); 972val dummy = dummy_pattern dummyT; 973val dummy_prop = dummy_pattern propT; 974 975fun is_dummy_pattern (Const ("Pure.dummy_pattern", _)) = true 976 | is_dummy_pattern _ = false; 977 978fun no_dummy_patterns tm = 979 if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm 980 else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]); 981 982fun free_dummy_patterns (Const ("Pure.dummy_pattern", T)) used = 983 let val [x] = Name.invent used Name.uu 1 984 in (Free (Name.internal x, T), Name.declare x used) end 985 | free_dummy_patterns (Abs (x, T, b)) used = 986 let val (b', used') = free_dummy_patterns b used 987 in (Abs (x, T, b'), used') end 988 | free_dummy_patterns (t $ u) used = 989 let 990 val (t', used') = free_dummy_patterns t used; 991 val (u', used'') = free_dummy_patterns u used'; 992 in (t' $ u', used'') end 993 | free_dummy_patterns a used = (a, used); 994 995fun replace_dummy Ts (Const ("Pure.dummy_pattern", T)) i = 996 (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1) 997 | replace_dummy Ts (Abs (x, T, t)) i = 998 let val (t', i') = replace_dummy (T :: Ts) t i 999 in (Abs (x, T, t'), i') end 1000 | replace_dummy Ts (t $ u) i = 1001 let 1002 val (t', i') = replace_dummy Ts t i; 1003 val (u', i'') = replace_dummy Ts u i'; 1004 in (t' $ u', i'') end 1005 | replace_dummy _ a i = (a, i); 1006 1007val replace_dummy_patterns = replace_dummy []; 1008 1009fun show_dummy_patterns (Var (("_dummy_", _), T)) = dummy_pattern T 1010 | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u 1011 | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t) 1012 | show_dummy_patterns a = a; 1013 1014 1015(* display variables *) 1016 1017fun string_of_vname (x, i) = 1018 let 1019 val idx = string_of_int i; 1020 val dot = 1021 (case rev (Symbol.explode x) of 1022 _ :: "\<^sub>" :: _ => false 1023 | c :: _ => Symbol.is_digit c 1024 | _ => true); 1025 in 1026 if dot then "?" ^ x ^ "." ^ idx 1027 else if i <> 0 then "?" ^ x ^ idx 1028 else "?" ^ x 1029 end; 1030 1031fun string_of_vname' (x, ~1) = x 1032 | string_of_vname' xi = string_of_vname xi; 1033 1034end; 1035 1036structure Basic_Term: BASIC_TERM = Term; 1037open Basic_Term; 1038