1(* ===================================================================== *) 2(* FILE : Term.sml *) 3(* DESCRIPTION : ML-style typed lambda terms (no ML "let" though). *) 4(* *) 5(* AUTHOR : (c) Konrad Slind, University of Calgary *) 6(* DATE : August 26, 1991 *) 7(* Modified : September 22, 1997, Ken Larsen (functor removal) *) 8(* Rewritten : 1999, Bruno Barras, to use explicit substitutions *) 9(* Modified : July 2000, Konrad Slind, for Moscow ML 2.00 *) 10(* ===================================================================== *) 11 12structure Term :> Term = 13struct 14 15open Feedback Lib Subst KernelTypes 16 17val kernelid = "stdknl" 18 19type 'a set = 'a HOLset.set; 20 21val ERR = mk_HOL_ERR "Term"; 22val WARN = HOL_WARNING "Term"; 23 24val --> = Type.-->; infixr 3 -->; 25 26infix |-> ##; 27 28(*--------------------------------------------------------------------------- 29 Create the signature for HOL terms 30 ---------------------------------------------------------------------------*) 31 32 33val termsig = KernelSig.new_table() 34fun prim_delete_const kn = ignore (KernelSig.retire_name(termsig, kn)) 35fun prim_new_const (k as {Thy,Name}) ty = let 36 val hty = if Type.polymorphic ty then POLY ty else GRND ty 37 val id = KernelSig.insert(termsig, k, hty) 38in 39 Const(id, hty) 40end 41fun del_segment s = KernelSig.del_segment(termsig, s) 42 43 44 45 46(*---------------------------------------------------------------------------* 47 * Builtin constants. These are in every HOL signature, and it is * 48 * convenient to nail them down here. * 49 *---------------------------------------------------------------------------*) 50 51local 52 open KernelSig Type 53 val eq_ty = POLY (alpha --> alpha --> bool) 54 val hil_ty = POLY ((alpha --> bool) --> alpha) 55 val imp_ty = GRND (bool --> bool --> bool) 56in 57 val eq_id = insert(termsig,{Name = "=", Thy = "min"}, eq_ty) 58 val hil_id = insert(termsig,{Name = "@", Thy = "min"}, hil_ty) 59 val imp_id = insert(termsig,{Name = "==>", Thy = "min"}, imp_ty) 60 61 val eqc = Const (eq_id,eq_ty) 62 val equality = eqc 63 val hil = Const (hil_id,hil_ty) 64 val imp = Const (imp_id,imp_ty) 65end 66 67(*---------------------------------------------------------------------------* 68 Useful functions to hide explicit substitutions 69 Important invariant: never delay subst on atoms, and compose Clos. 70 Therefore, in Clos{Env,Body}, Body is either a Comb or an Abs. 71 This invariant is enforced if we always use mk_clos instead of Clos. 72 ---------------------------------------------------------------------------*) 73 74fun mk_clos (s, Bv i) = 75 (case (Subst.exp_rel(s,i)) 76 of (0, SOME t) => t 77 | (k, SOME t) => mk_clos (Subst.shift(k,Subst.id), t) 78 | (v, NONE) => Bv v) 79 | mk_clos (s, t as Fv _) = t 80 | mk_clos (s, t as Const _) = t 81 | mk_clos (s,Clos(Env,Body)) = Clos(Subst.comp mk_clos (s,Env), Body) 82 | mk_clos (s,t) = Clos(s, t) 83; 84 85(*--------------------------------------------------------------------------- 86 Propagate substitutions so that we are sure the head of the term is 87 not a delayed substitution. 88 ---------------------------------------------------------------------------*) 89 90fun push_clos (Clos(E, Comb(f,x))) = Comb(mk_clos(E,f), mk_clos(E,x)) 91 | push_clos (Clos(E, Abs(v,M))) = Abs(v, mk_clos (Subst.lift(1,E),M)) 92 | push_clos _ = raise ERR "push_clos" "not a subst" 93; 94 95(*---------------------------------------------------------------------------* 96 * Computing the type of a term. * 97 *---------------------------------------------------------------------------*) 98 99local fun lookup 0 (ty::_) = ty 100 | lookup n (_::rst) = lookup (n-1) rst 101 | lookup _ [] = raise ERR "type_of" "lookup" 102 fun ty_of (Fv(_,Ty)) _ = Ty 103 | ty_of (Const(_,GRND Ty)) _ = Ty 104 | ty_of (Const(_,POLY Ty)) _ = Ty 105 | ty_of (Bv i) E = lookup i E 106 | ty_of (Comb(Rator, _)) E = snd(Type.dom_rng(ty_of Rator E)) 107 | ty_of (t as Clos _) E = ty_of (push_clos t) E 108 | ty_of (Abs(Fv(_,Ty),Body)) E = Ty --> ty_of Body (Ty::E) 109 | ty_of _ _ = raise ERR "type_of" "term construction" 110in 111fun type_of tm = ty_of tm [] 112end; 113 114 115(*--------------------------------------------------------------------------- 116 Discriminators 117 ---------------------------------------------------------------------------*) 118 119fun is_bvar (Bv _) = true | is_bvar _ = false; 120fun is_var (Fv _) = true | is_var _ = false; 121fun is_const(Const _) = true | is_const _ = false; 122fun is_comb(Comb _) = true | is_comb(Clos(_,Comb _)) = true | is_comb _ = false 123fun is_abs(Abs _) = true | is_abs(Clos(_,Abs _)) = true | is_abs _ = false; 124 125 126(*---------------------------------------------------------------------------* 127 * The type variables of a lambda term. Tail recursive (from Ken Larsen). * 128 *---------------------------------------------------------------------------*) 129 130local fun tyV (Fv(_,Ty)) k = k (Type.type_vars Ty) 131 | tyV (Bv _) k = k [] 132 | tyV (Const(_,GRND _)) k = k [] 133 | tyV (Const(_,POLY Ty)) k = k (Type.type_vars Ty) 134 | tyV (Comb(Rator,Rand)) k = tyV Rand (fn q1 => 135 tyV Rator(fn q2 => k (union q2 q1))) 136 | tyV (Abs(Bvar,Body)) k = tyV Body (fn q1 => 137 tyV Bvar (fn q2 => k (union q2 q1))) 138 | tyV (t as Clos _) k = tyV (push_clos t) k 139in 140fun type_vars_in_term tm = tyV tm Lib.I 141end; 142 143(*---------------------------------------------------------------------------* 144 * The free variables of a lambda term. Tail recursive (from Ken Larsen). * 145 *---------------------------------------------------------------------------*) 146 147local fun FV (v as Fv _) A k = k (Lib.insert v A) 148 | FV (Comb(f,x)) A k = FV f A (fn q => FV x q k) 149 | FV (Abs(_,Body)) A k = FV Body A k 150 | FV (t as Clos _) A k = FV (push_clos t) A k 151 | FV _ A k = k A 152in 153fun free_vars tm = FV tm [] Lib.I 154end; 155 156(*---------------------------------------------------------------------------* 157 * The free variables of a lambda term, in textual order. * 158 *---------------------------------------------------------------------------*) 159 160fun free_vars_lr tm = 161 let fun FV ((v as Fv _)::t) A = FV t (Lib.insert v A) 162 | FV (Bv _::t) A = FV t A 163 | FV (Const _::t) A = FV t A 164 | FV (Comb(M,N)::t) A = FV (M::N::t) A 165 | FV (Abs(_,M)::t) A = FV (M::t) A 166 | FV ((M as Clos _)::t) A = FV (push_clos M::t) A 167 | FV [] A = rev A 168 in 169 FV [tm] [] 170 end; 171 172(*---------------------------------------------------------------------------* 173 * The set of all variables in a term, represented as a list. * 174 *---------------------------------------------------------------------------*) 175 176local fun vars (v as Fv _) A = Lib.insert v A 177 | vars (Comb(Rator,Rand)) A = vars Rand (vars Rator A) 178 | vars (Abs(Bvar,Body)) A = vars Body (vars Bvar A) 179 | vars (t as Clos _) A = vars (push_clos t) A 180 | vars _ A = A 181in 182fun all_vars tm = vars tm [] 183end; 184 185fun free_varsl tm_list = itlist (union o free_vars) tm_list [] 186fun all_varsl tm_list = itlist (union o all_vars) tm_list []; 187 188(*--------------------------------------------------------------------------- 189 Support for efficient sets of variables 190 ---------------------------------------------------------------------------*) 191 192fun var_compare (Fv(s1,ty1), Fv(s2,ty2)) = 193 (case String.compare (s1,s2) 194 of EQUAL => Type.compare (ty1,ty2) 195 | x => x) 196 | var_compare _ = raise ERR "var_compare" "variables required"; 197 198val empty_varset = HOLset.empty var_compare 199 200(* ---------------------------------------------------------------------- 201 A total ordering on terms that respects alpha equivalence. 202 Fv < Bv < Const < Comb < Abs 203 ---------------------------------------------------------------------- *) 204 205fun fast_term_eq (t1:term) (t2:term) = Portable.pointer_eq (t1,t2) 206 207fun compare (p as (t1,t2)) = 208 if fast_term_eq t1 t2 then EQUAL else 209 case p of 210 (t1 as Clos _, t2) => compare (push_clos t1, t2) 211 | (t1, t2 as Clos _) => compare (t1, push_clos t2) 212 | (u as Fv _, v as Fv _) => var_compare (u,v) 213 | (Fv _, _) => LESS 214 | (Bv _, Fv _) => GREATER 215 | (Bv i, Bv j) => Int.compare (i,j) 216 | (Bv _, _) => LESS 217 | (Const _, Fv _) => GREATER 218 | (Const _, Bv _) => GREATER 219 | (Const(c1,ty1), 220 Const(c2,ty2)) => (case KernelSig.id_compare (c1, c2) 221 of EQUAL => Type.compare (to_hol_type ty1, 222 to_hol_type ty2) 223 | x => x) 224 | (Const _, _) => LESS 225 | (Comb(M,N),Comb(P,Q)) => (case compare (M,P) 226 of EQUAL => compare (N,Q) 227 | x => x) 228 | (Comb _, Abs _) => LESS 229 | (Comb _, _) => GREATER 230 | (Abs(Fv(_, ty1),M), 231 Abs(Fv(_, ty2),N)) => (case Type.compare(ty1,ty2) 232 of EQUAL => compare (M,N) 233 | x => x) 234 | (Abs _, _) => GREATER; 235 236val empty_tmset = HOLset.empty compare 237fun term_eq t1 t2 = compare(t1,t2) = EQUAL 238 239(* ---------------------------------------------------------------------- 240 All "atoms" (variables (bound or free) and constants). 241 242 Does not respect alpha-equivalence 243 ---------------------------------------------------------------------- *) 244 245fun all_atomsl tlist A = 246 case tlist of 247 [] => A 248 | t::ts => 249 let 250 in 251 case t of 252 Fv _ => all_atomsl ts (HOLset.add(A,t)) 253 | Const _ => all_atomsl ts (HOLset.add(A,t)) 254 | Comb(Rator,Rand) => all_atomsl (Rator::Rand::ts) A 255 | Abs(v,body) => all_atomsl (body::ts) (HOLset.add(A,v)) 256 | Clos _ => all_atomsl (push_clos t::ts) A 257 | Bv _ => all_atomsl ts A 258 end 259 260fun all_atoms t = all_atomsl [t] empty_tmset 261 262(*--------------------------------------------------------------------------- 263 Free variables of a term. Tail recursive. Returns a set. 264 ---------------------------------------------------------------------------*) 265 266fun FVL [] A = A 267 | FVL ((v as Fv _)::rst) A = FVL rst (HOLset.add(A,v)) 268 | FVL (Comb(Rator,Rand)::rst) A = FVL (Rator::Rand::rst) A 269 | FVL (Abs(_,Body)::rst) A = FVL (Body::rst) A 270 | FVL ((t as Clos _)::rst) A = FVL (push_clos t::rst) A 271 | FVL (_::rst) A = FVL rst A 272 273 274(* ---------------------------------------------------------------------- 275 free_in tm M : does tm occur free in M? 276 ---------------------------------------------------------------------- *) 277 278fun free_in tm = 279 let fun f1 (Comb(Rator,Rand)) = (f2 Rator) orelse (f2 Rand) 280 | f1 (Abs(_,Body)) = f2 Body 281 | f1 (t as Clos _) = f2 (push_clos t) 282 | f1 _ = false 283 and f2 t = term_eq t tm orelse f1 t 284 in f2 285 end; 286 287(*--------------------------------------------------------------------------- 288 The following are used in Thm to check side conditions (e.g., 289 does variable v occur free in the assumptions). 290 ---------------------------------------------------------------------------*) 291 292fun var_occurs M = 293 let val v = (case M of Fv v => v | _ => raise ERR "" "") 294 fun occ (Fv u) = (v=u) 295 | occ (Bv _) = false 296 | occ (Const _) = false 297 | occ (Comb(Rator,Rand)) = occ Rand orelse occ Rator 298 | occ (Abs(_,Body)) = occ Body 299 | occ (t as Clos _) = occ (push_clos t) 300 in occ end 301 handle HOL_ERR _ => raise ERR "var_occurs" "not a variable"; 302 303 304(*---------------------------------------------------------------------------* 305 * Making variables * 306 *---------------------------------------------------------------------------*) 307 308val mk_var = Fv 309 310fun inST s = not(null(KernelSig.listName termsig s)) 311 312fun mk_primed_var (Name,Ty) = 313 let val next = Lexis.nameStrm Name 314 fun spin s = if inST s then spin (next()) else s 315 in mk_var(spin Name, Ty) 316 end; 317 318(*---------------------------------------------------------------------------* 319 * "genvars" are a Lisp-style "gensym" for HOL variables. * 320 *---------------------------------------------------------------------------*) 321 322local val genvar_prefix = "%%genvar%%" 323 fun num2name i = genvar_prefix^Int.toString i 324 val num_stream = Portable.make_counter{init=0,inc=1} 325in 326fun genvar ty = Fv(num2name(num_stream()), ty) 327 328fun genvars ty = 329 let fun gen acc n = if n <= 0 then rev acc else gen (genvar ty::acc) (n-1) 330 in gen [] 331 end 332 333fun is_genvar (Fv(Name,_)) = String.isPrefix genvar_prefix Name 334 | is_genvar _ = false; 335end; 336 337 338(*---------------------------------------------------------------------------* 339 * Given a variable and a list of variables, if the variable does not exist * 340 * on the list, then return the variable. Otherwise, rename the variable and * 341 * try again. Note well that the variant uses only the name of the variable * 342 * as a basis for testing equality. Experience has shown that basing the * 343 * comparison on both the name and the type of the variable resulted in * 344 * needlessly confusing formulas occasionally being displayed in interactive * 345 * sessions. * 346 *---------------------------------------------------------------------------*) 347 348fun gen_variant P caller = 349 let fun var_name _ (Fv(Name,_)) = Name 350 | var_name caller _ = raise ERR caller "not a variable" 351 fun vary vlist (Fv(Name,Ty)) = 352 let val next = Lexis.nameStrm Name 353 val L = map (var_name caller) vlist 354 fun away s = if mem s L then away (next()) else s 355 fun loop name = 356 let val s = away name 357 in if P s then loop (next()) else s 358 end 359 in mk_var(loop Name, Ty) 360 end 361 | vary _ _ = raise ERR caller "2nd argument should be a variable" 362 in vary 363 end; 364 365val variant = gen_variant inST "variant" 366val prim_variant = gen_variant (K false) "prim_variant"; 367 368 369(*---------------------------------------------------------------------------* 370 * Making constants. * 371 * * 372 * We grab the constant scheme from the signature. If it is ground, then * 373 * we just return the scheme. Thus there will only be one copy of any * 374 * ground constant. If it is polymorphic, we match its type against the * 375 * given type. If the match is the identity substitution, we just return * 376 * the constant. If the match moves some variables, then we check that the * 377 * instance is ground (and then return GRND); otherwise the type is still * 378 * polymorphic. * 379 *---------------------------------------------------------------------------*) 380 381val decls = map (Const o #2) o KernelSig.listName termsig 382 383fun prim_mk_const (knm as {Name,Thy}) = 384 case KernelSig.peek(termsig, knm) 385 of SOME c => Const c 386 | NONE => raise ERR "prim_mk_const" 387 (Lib.quote Name^" not found in theory "^Lib.quote Thy) 388 389fun ground x = Lib.all (fn {redex,residue} => not(Type.polymorphic residue)) x; 390 391fun create_const errstr (const as (_,GRND pat)) Ty = 392 if Ty=pat then Const const 393 else raise ERR "create_const" "not a type match" 394 | create_const errstr (const as (r,POLY pat)) Ty = 395 ((case Type.raw_match_type pat Ty ([],[]) 396 of ([],_) => Const const 397 | (S,[]) => Const(r, if ground S then GRND Ty else POLY Ty) 398 | (S, _) => Const(r,POLY Ty)) 399 handle HOL_ERR _ => raise ERR errstr 400 (String.concat["Not a type instance: ", KernelSig.id_toString r])) 401 402 403fun mk_thy_const {Thy,Name,Ty} = let 404 val knm = {Thy=Thy,Name=Name} 405in 406 case KernelSig.peek(termsig, knm) of 407 NONE => raise ERR "mk_thy_const" (KernelSig.name_toString knm^" not found") 408 | SOME c => create_const "mk_thy_const" c Ty 409end 410 411fun first_decl fname Name = 412 case KernelSig.listName termsig Name 413 of [] => raise ERR fname (Name^" not found") 414 | [(_, const)] => const 415 | (_, const) :: _ => 416 (WARN fname (Lib.quote Name^": more than one possibility"); 417 const) 418 419val current_const = first_decl "current_const"; 420fun mk_const(Name,Ty) = create_const"mk_const" (first_decl"mk_const" Name) Ty; 421 422fun all_consts() = map (Const o #2) (KernelSig.listItems termsig) 423fun thy_consts s = map (Const o #2) (KernelSig.listThy termsig s) 424 425fun same_const (Const(id1,_)) (Const(id2,_)) = id1 = id2 426 | same_const _ _ = false 427 428(*---------------------------------------------------------------------------* 429 * Making applications * 430 *---------------------------------------------------------------------------*) 431 432local val INCOMPAT_TYPES = Lib.C ERR "incompatible types" 433 fun lmk_comb err = 434 let fun loop (A,_) [] = A 435 | loop (A,typ) (tm::rst) = 436 let val (ty1,ty2) = with_exn Type.dom_rng typ err 437 in if type_of tm = ty1 438 then loop(Comb(A,tm),ty2) rst 439 else raise err 440 end 441 in fn (f,L) => loop(f, type_of f) L 442 end 443 val mk_comb0 = lmk_comb (INCOMPAT_TYPES "mk_comb") 444in 445 446fun mk_comb(r as (Abs(Fv(_,Ty),_), Rand)) = 447 if type_of Rand = Ty then Comb r else raise INCOMPAT_TYPES "mk_comb" 448 | mk_comb(r as (Clos(_,Abs(Fv(_,Ty),_)), Rand)) = 449 if type_of Rand = Ty then Comb r else raise INCOMPAT_TYPES "mk_comb" 450 | mk_comb(Rator,Rand) = mk_comb0 (Rator,[Rand]) 451 452val list_mk_comb = lmk_comb (INCOMPAT_TYPES "list_mk_comb") 453end; 454 455 456fun dest_var (Fv v) = v 457 | dest_var _ = raise ERR "dest_var" "not a var" 458 459 460(*---------------------------------------------------------------------------* 461 * Alpha conversion * 462 *---------------------------------------------------------------------------*) 463 464fun rename_bvar s t = 465 case t of 466 Abs(Fv(_, Ty), Body) => Abs(Fv(s,Ty), Body) 467 | Clos(_, Abs _) => rename_bvar s (push_clos t) 468 | _ => raise ERR "rename_bvar" "not an abstraction"; 469 470 471local 472 fun EQ(t1,t2) = fast_term_eq t1 t2 473 fun subsEQ(s1,s2) = s1 = s2 474in 475fun aconv t1 t2 = EQ(t1,t2) orelse 476 case(t1,t2) 477 of (Comb(M,N),Comb(P,Q)) => aconv N Q andalso aconv M P 478 | (Abs(Fv(_,ty1),M), 479 Abs(Fv(_,ty2),N)) => ty1=ty2 andalso aconv M N 480 | (Clos(e1,b1), 481 Clos(e2,b2)) => (subsEQ(e1,e2) andalso EQ(b1,b2)) 482 orelse aconv (push_clos t1) (push_clos t2) 483 | (Clos _, _) => aconv (push_clos t1) t2 484 | (_, Clos _) => aconv t1 (push_clos t2) 485 | (M,N) => (M=N) 486end; 487 488 489(*---------------------------------------------------------------------------* 490 * Beta-reduction. Non-renaming. * 491 *---------------------------------------------------------------------------*) 492 493fun beta_conv (Comb(Abs(_,Body), Bv 0)) = Body 494 | beta_conv (Comb(Abs(_,Body), Rand)) = 495 let fun subs((tm as Bv j),i) = if i=j then Rand else tm 496 | subs(Comb(Rator,Rand),i) = Comb(subs(Rator,i),subs(Rand,i)) 497 | subs(Abs(v,Body),i) = Abs(v,subs(Body,i+1)) 498 | subs (tm as Clos _,i) = subs(push_clos tm,i) 499 | subs (tm,_) = tm 500 in 501 subs (Body,0) 502 end 503 | beta_conv (Comb(x as Clos _, Rand)) = beta_conv (Comb(push_clos x, Rand)) 504 | beta_conv (x as Clos _) = beta_conv (push_clos x) 505 | beta_conv _ = raise ERR "beta_conv" "not a beta-redex"; 506 507 508(*---------------------------------------------------------------------------* 509 * Beta-reduction without propagation of the explicit substitution * 510 * until the next abstraction. * 511 *---------------------------------------------------------------------------*) 512 513fun lazy_beta_conv (Comb(Abs(_,Body),Rand)) = 514 mk_clos(Subst.cons(Subst.id,Rand), Body) 515 | lazy_beta_conv (Comb(Clos(Env, Abs(_,Body)),Rand)) = 516 mk_clos(Subst.cons(Env,Rand), Body) 517 | lazy_beta_conv (t as Clos _) = lazy_beta_conv (push_clos t) 518 | lazy_beta_conv _ = raise ERR "lazy_beta_conv" "not a beta-redex"; 519 520 521(*---------------------------------------------------------------------------* 522 * Eta-conversion * 523 *---------------------------------------------------------------------------*) 524 525local fun pop (tm as Bv i, k) = 526 if i=k then raise ERR "eta_conv" "not an eta-redex" else tm 527 | pop (Comb(Rator,Rand),k) = Comb(pop(Rator,k), pop(Rand,k)) 528 | pop (Abs(v,Body), k) = Abs(v,pop(Body, k+1)) 529 | pop (tm as Clos _, k) = pop (push_clos tm, k) 530 | pop (tm,k) = tm 531 fun eta_body (Comb(Rator,Bv 0)) = pop (Rator,0) 532 | eta_body (tm as Clos _) = eta_body (push_clos tm) 533 | eta_body _ = raise ERR "eta_conv" "not an eta-redex" 534in 535fun eta_conv (Abs(_,Body)) = eta_body Body 536 | eta_conv (tm as Clos _) = eta_conv (push_clos tm) 537 | eta_conv _ = raise ERR "eta_conv" "not an eta-redex" 538end; 539 540 541(*---------------------------------------------------------------------------* 542 * Replace arbitrary subterms in a term. Non-renaming. * 543 *---------------------------------------------------------------------------*) 544 545val emptysubst:(term,term)Binarymap.dict = Binarymap.mkDict compare 546local 547 open Binarymap 548 fun addb [] A = A 549 | addb ({redex,residue}::t) (A,b) = 550 addb t (if type_of redex = type_of residue 551 then (insert(A,redex,residue), 552 is_var redex andalso b) 553 else raise ERR "subst" "redex has different type than residue") 554in 555fun subst [] = I 556 | subst theta = 557 let val (fmap,b) = addb theta (emptysubst, true) 558 fun vsubs (v as Fv _) = (case peek(fmap,v) of NONE => v | SOME y => y) 559 | vsubs (Comb(Rator,Rand)) = Comb(vsubs Rator, vsubs Rand) 560 | vsubs (Abs(Bvar,Body)) = Abs(Bvar,vsubs Body) 561 | vsubs (c as Clos _) = vsubs (push_clos c) 562 | vsubs tm = tm 563 fun subs tm = 564 case peek(fmap,tm) 565 of SOME residue => residue 566 | NONE => 567 (case tm 568 of Comb(Rator,Rand) => Comb(subs Rator, subs Rand) 569 | Abs(Bvar,Body) => Abs(Bvar,subs Body) 570 | Clos _ => subs(push_clos tm) 571 | _ => tm) 572 in 573 (if b then vsubs else subs) 574 end 575end 576 577(*---------------------------------------------------------------------------* 578 * Instantiate type variables in a term * 579 *---------------------------------------------------------------------------*) 580 581fun inst [] tm = tm 582 | inst theta tm = 583 let fun 584 inst1 (bv as Bv _) = bv 585 | inst1 (c as Const(_, GRND _)) = c 586 | inst1 (c as Const(r, POLY Ty)) = 587 (case Type.ty_sub theta Ty 588 of SAME => c 589 | DIFF ty => Const(r,(if Type.polymorphic ty then POLY else GRND)ty)) 590 | inst1 (v as Fv(Name,Ty)) = 591 (case Type.ty_sub theta Ty of SAME => v | DIFF ty => Fv(Name, ty)) 592 | inst1 (Comb(Rator,Rand)) = Comb(inst1 Rator, inst1 Rand) 593 | inst1 (Abs(Bvar,Body)) = Abs(inst1 Bvar, inst1 Body) 594 | inst1 (t as Clos _) = inst1(push_clos t) 595 in 596 inst1 tm 597 end; 598 599fun dest_comb (Comb r) = r 600 | dest_comb (t as Clos _) = dest_comb (push_clos t) 601 | dest_comb _ = raise ERR "dest_comb" "not a comb" 602 603 604(*--------------------------------------------------------------------------- 605 Making abstractions. list_mk_binder is a relatively 606 efficient version for making terms with many consecutive 607 abstractions. 608 ---------------------------------------------------------------------------*) 609 610local val FORMAT = ERR "list_mk_binder" 611 "expected first arg to be a constant of type :(<ty>_1 -> <ty>_2) -> <ty>_3" 612 fun check_opt NONE = Lib.I 613 | check_opt (SOME c) = 614 if not(is_const c) then raise FORMAT 615 else case total (fst o Type.dom_rng o fst o Type.dom_rng o type_of) c 616 of NONE => raise FORMAT 617 | SOME ty => (fn abs => 618 let val dom = fst(Type.dom_rng(type_of abs)) 619 in mk_comb (inst[ty |-> dom] c, abs) 620 end) 621in 622fun list_mk_binder opt = 623 let val f = check_opt opt 624 in fn (vlist,tm) 625 => if not (all is_var vlist) then raise ERR "list_mk_binder" "" 626 else 627 let open Redblackmap 628 val varmap0 = mkDict compare 629 fun enum [] _ A = A 630 | enum (h::t) i (vmap,rvs) = let val vmap' = insert (vmap,h,i) 631 in enum t (i-1) (vmap',h::rvs) 632 end 633 val (varmap, rvlist) = enum vlist (length vlist - 1) (varmap0, []) 634 fun lookup v vmap = case peek (vmap,v) of NONE => v | SOME i => Bv i 635 fun increment vmap = transform (fn x => x+1) vmap 636 fun bind (v as Fv _) vmap k = k (lookup v vmap) 637 | bind (Comb(M,N)) vmap k = bind M vmap (fn m => 638 bind N vmap (fn n => k (Comb(m,n)))) 639 | bind (Abs(v,M)) vmap k = bind M (increment vmap) 640 (fn q => k (Abs(v,q))) 641 | bind (t as Clos _) vmap k = bind (push_clos t) vmap k 642 | bind tm vmap k = k tm 643 in 644 rev_itlist (fn v => fn M => f(Abs(v,M))) rvlist (bind tm varmap I) 645 end 646 handle e => raise wrap_exn "Term" "list_mk_binder" e 647 end 648end; 649 650val list_mk_abs = list_mk_binder NONE; 651 652fun mk_abs(Bvar as Fv _, Body) = 653 let fun bind (v as Fv _) i = if v=Bvar then Bv i else v 654 | bind (Comb(Rator,Rand)) i = Comb(bind Rator i, bind Rand i) 655 | bind (Abs(Bvar,Body)) i = Abs(Bvar, bind Body (i+1)) 656 | bind (t as Clos _) i = bind (push_clos t) i 657 | bind tm _ = tm (* constant *) 658 in 659 Abs(Bvar, bind Body 0) 660 end 661 | mk_abs _ = raise ERR "mk_abs" "Bvar not a variable" 662 663 664(*--------------------------------------------------------------------------- 665 Taking terms apart 666 667 These operations are all easy, except for taking apart multiple 668 abstractions. It can happen, via beta-conversion or substitution, 669 or instantiation, that a free variable is bound by the scope. One 670 of the tasks of strip_abs is to sort the resulting mess out. 671 strip_abs works by first classifying all the free variables in the 672 body as being captured by the prefix bindings or not. Each capturing 673 prefix binder is then renamed until it doesn't capture. Then we go 674 through the body and replace the dB indices of the prefix with the 675 corresponding free variables. These may in fact fall under another 676 binder; the renaming of that will, if necessary, get done if that 677 binder is taken apart (by a subsequent dest/strip_binder). 678 ---------------------------------------------------------------------------*) 679 680local fun peel f (t as Clos _) A = peel f (push_clos t) A 681 | peel f tm A = 682 case f tm of 683 SOME(Abs(v,M)) => peel f M (v::A) 684 | otherwise => (A,tm) 685 datatype occtype = PREFIX of int | BODY 686 fun array_to_revlist A = 687 let val top = Array.length A - 1 688 fun For i B = if i>top then B else For (i+1) (Array.sub(A,i)::B) 689 in For 0 [] 690 end 691 val vi_empty = HOLset.empty (fn ((v1,i1),(v2,i2)) => var_compare(v1,v2)) 692 fun add_vi viset vi = 693 if HOLset.member(viset,vi) then viset else HOLset.add(viset,vi) 694 fun trypush_clos (x as Clos _) = push_clos x 695 | trypush_clos t = t 696in 697fun strip_binder opt = 698 let val f = 699 case opt of 700 NONE => (fn (t as Abs _) => SOME t 701 | (t as Clos(_, Abs _)) => SOME (push_clos t) 702 | other => NONE) 703 | SOME c => (fn t => let val (rator,rand) = dest_comb t 704 in if same_const rator c 705 then SOME (trypush_clos rand) 706 else NONE 707 end handle HOL_ERR _ => NONE) 708 in fn tm => 709 let 710 val (prefixl,body) = peel f tm [] 711 val AV = ref (Redblackmap.mkDict String.compare) : ((string,occtype)Redblackmap.dict) ref 712 fun peekInsert (key,data) = 713 let open Redblackmap 714 in case peek (!AV,key) 715 of SOME data' => SOME data' 716 | NONE => (AV := insert(!AV,key,data); NONE) 717 end 718 val prefix = Array.fromList prefixl 719 val vmap = curry Array.sub prefix 720 val (insertAVbody,insertAVprefix,lookAV,dupls) = 721 let open Redblackmap (* AV is red-black map of (var,occtype) elems *) 722 fun insertl [] _ dupls = dupls 723 | insertl (x::rst) i dupls = 724 let val n = fst(dest_var x) 725 in case peekInsert (n,PREFIX i) 726 of NONE => insertl rst (i+1) (dupls) 727 | SOME _ => insertl rst (i+1) ((x,i)::dupls) 728 end 729 val dupls = insertl prefixl 0 [] 730 in ((fn s => (AV := insert (!AV,s,BODY))), (* insertAVbody *) 731 (fn (s,i) => (AV := insert (!AV,s,PREFIX i))), (* insertAVprefix *) 732 (fn s => peek (!AV,s)), (* lookAV *) 733 dupls) 734 end 735 fun variantAV n = 736 let val next = Lexis.nameStrm n 737 fun loop s = case lookAV s of NONE => s | SOME _ => loop (next()) 738 in loop n 739 end 740 fun CVs (v as Fv(n,_)) capt k = 741 (case lookAV n 742 of SOME (PREFIX i) => k (add_vi capt (vmap i,i)) 743 | SOME BODY => k capt 744 | NONE => (insertAVbody n; k capt)) 745 | CVs(Comb(M,N)) capt k = CVs N capt (fn c => CVs M c k) 746 | CVs(Abs(_,M)) capt k = CVs M capt k 747 | CVs(t as Clos _) capt k = CVs (push_clos t) capt k 748 | CVs tm capt k = k capt 749 fun unclash insert [] = () 750 | unclash insert ((v,i)::rst) = 751 let val (n,ty) = dest_var v 752 val n' = variantAV n 753 val v' = mk_var(n',ty) 754 in Array.update(prefix,i,v') 755 ; insert (n',i) 756 ; unclash insert rst 757 end 758 fun unbind (v as Bv i) j k = k (vmap(i-j) handle Subscript => v) 759 | unbind (Comb(M,N)) j k = unbind M j (fn m => 760 unbind N j (fn n => k(Comb(m,n)))) 761 | unbind (Abs(v,M)) j k = unbind M (j+1) (fn q => k(Abs(v,q))) 762 | unbind (t as Clos _) j k = unbind (push_clos t) j k 763 | unbind tm j k = k tm 764 in 765 unclash insertAVprefix (List.rev dupls) 766 ; unclash (insertAVbody o fst) (HOLset.listItems(CVs body vi_empty I)) 767 ; (array_to_revlist prefix, unbind body 0 I) 768 end 769 end 770end; 771 772val strip_abs = strip_binder NONE; 773 774local exception CLASH 775in 776fun dest_abs(Abs(Bvar as Fv(Name,Ty), Body)) = 777 let fun dest (v as (Bv j), i) = if i=j then Bvar else v 778 | dest (v as Fv(s,_), _) = if Name=s then raise CLASH else v 779 | dest (Comb(Rator,Rand),i) = Comb(dest(Rator,i),dest(Rand,i)) 780 | dest (Abs(Bvar,Body),i) = Abs(Bvar, dest(Body,i+1)) 781 | dest (t as Clos _, i) = dest (push_clos t, i) 782 | dest (tm,_) = tm 783 in (Bvar, dest(Body,0)) 784 handle CLASH => 785 dest_abs(Abs(variant (free_vars Body) Bvar, Body)) 786 end 787 | dest_abs (t as Clos _) = dest_abs (push_clos t) 788 | dest_abs _ = raise ERR "dest_abs" "not a lambda abstraction" 789end; 790 791local 792open KernelSig 793in 794fun break_abs(Abs(_,Body)) = Body 795 | break_abs(t as Clos _) = break_abs (push_clos t) 796 | break_abs _ = raise ERR "break_abs" "not an abstraction"; 797 798fun dest_thy_const (Const(id,ty)) = 799 let val {Name,Thy} = name_of_id id 800 in {Thy=Thy, Name=Name, Ty=to_hol_type ty} 801 end 802 | dest_thy_const _ = raise ERR"dest_thy_const" "not a const" 803 804fun break_const (Const p) = (I##to_hol_type) p 805 | break_const _ = raise ERR "break_const" "not a const" 806 807fun dest_const (Const(id,ty)) = (name_of id, to_hol_type ty) 808 | dest_const _ = raise ERR "dest_const" "not a const" 809end 810 811(*--------------------------------------------------------------------------- 812 Derived destructors 813 ---------------------------------------------------------------------------*) 814 815fun rator (Comb(Rator,_)) = Rator 816 | rator (Clos(Env, Comb(Rator,_))) = mk_clos(Env,Rator) 817 | rator _ = raise ERR "rator" "not a comb" 818 819fun rand (Comb(_,Rand)) = Rand 820 | rand (Clos(Env, Comb(_,Rand))) = mk_clos(Env,Rand) 821 | rand _ = raise ERR "rand" "not a comb" 822 823val bvar = fst o dest_abs; 824val body = snd o dest_abs; 825 826 827(*--------------------------------------------------------------------------- 828 Matching (first order, modulo alpha conversion) of terms, including 829 sets of variables and type variables to avoid binding. 830 ---------------------------------------------------------------------------*) 831 832local 833 fun MERR s = raise ERR "raw_match_term" s 834 fun free (Bv i) n = i<n 835 | free (Comb(Rator,Rand)) n = free Rand n andalso free Rator n 836 | free (Abs(_,Body)) n = free Body (n+1) 837 | free (t as Clos _) n = free (push_clos t) n 838 | free _ _ = true 839 fun lookup x ids = 840 let fun look [] = if HOLset.member(ids,x) then SOME x else NONE 841 | look ({redex,residue}::t) = if x=redex then SOME residue else look t 842 in look end 843 fun bound_by_scope scoped M = if scoped then not (free M 0) else false 844 val tymatch = Type.raw_match_type 845 open KernelSig 846in 847fun RM [] theta = theta 848 | RM (((v as Fv(n,Ty)),tm,scoped)::rst) ((S1 as (tmS,Id)),tyS) 849 = if bound_by_scope scoped tm 850 then MERR "Attempt to capture bound variable" 851 else RM rst 852 ((case lookup v Id tmS 853 of NONE => if v=tm then (tmS,HOLset.add(Id,v)) 854 else ((v |-> tm)::tmS,Id) 855 | SOME tm' => if aconv tm' tm then S1 856 else MERR ("double bind on variable "^ 857 Lib.quote n)), 858 tymatch Ty (type_of tm) tyS) 859 | RM ((Const(c1,ty1),Const(c2,ty2),_)::rst) (tmS,tyS) 860 = RM rst 861 (if c1 <> c2 then 862 let val n1 = id_toString c1 863 val n2 = id_toString c2 864 in 865 MERR ("Different constants: "^n1^" and "^n2) 866 end 867 else 868 case (ty1,ty2) 869 of (GRND _, POLY _) => MERR"ground const vs. polymorphic const" 870 | (GRND pat,GRND obj) => if pat=obj then (tmS,tyS) 871 else MERR"const-const with different (ground) types" 872 | (POLY pat,GRND obj) => (tmS, tymatch pat obj tyS) 873 | (POLY pat,POLY obj) => (tmS, tymatch pat obj tyS)) 874 | RM ((Abs(Fv(_,ty1),M),Abs(Fv(_,ty2),N),_)::rst) (tmS,tyS) 875 = RM ((M,N,true)::rst) (tmS, tymatch ty1 ty2 tyS) 876 | RM ((Comb(M,N),Comb(P,Q),s)::rst) S = RM ((M,P,s)::(N,Q,s)::rst) S 877 | RM ((Bv i,Bv j,_)::rst) S = if i=j then RM rst S 878 else MERR "Bound var doesn't match" 879 | RM (((pat as Clos _),ob,s)::t) S = RM ((push_clos pat,ob,s)::t) S 880 | RM ((pat,(ob as Clos _),s)::t) S = RM ((pat,push_clos ob,s)::t) S 881 | RM all others = MERR "different constructors" 882end 883 884fun raw_match tyfixed tmfixed pat ob (tmS,tyS) 885 = RM [(pat,ob,false)] ((tmS,tmfixed), (tyS,tyfixed)); 886 887fun norm_subst ((tmS,_),(tyS,_)) = 888 let val Theta = inst tyS 889 fun del A [] = A 890 | del A ({redex,residue}::rst) = 891 del (let val redex' = Theta(redex) 892 in if residue=redex' then A else (redex' |-> residue)::A 893 end) rst 894 in (del [] tmS,tyS) 895 end 896 897fun match_terml tyfixed tmfixed pat ob = 898 norm_subst (raw_match tyfixed tmfixed pat ob ([],[])) 899 900val match_term = match_terml [] empty_varset; 901 902(*--------------------------------------------------------------------------- 903 Must know that ty is the type of tm1 and tm2. 904 ---------------------------------------------------------------------------*) 905 906fun prim_mk_eq ty tm1 tm2 = Comb(Comb(inst [Type.alpha |-> ty] eqc, tm1), tm2) 907 908(*--------------------------------------------------------------------------- 909 Must know that tm1 and tm2 both have type "bool" 910 ---------------------------------------------------------------------------*) 911 912fun prim_mk_imp tm1 tm2 = Comb(Comb(imp, tm1),tm2); 913 914(*--------------------------------------------------------------------------- 915 Take an equality apart, and return the type of the operands 916 ---------------------------------------------------------------------------*) 917 918local val err = ERR "dest_eq_ty" "" 919in 920fun dest_eq_ty t = 921 let val ((c,M),N) = with_exn ((dest_comb##I) o dest_comb) t err 922 in if same_const c eqc 923 then (M,N,fst(Type.dom_rng (type_of c))) 924 else raise err 925 end 926end; 927 928(*--------------------------------------------------------------------------- 929 Full propagation of substitutions. 930 ---------------------------------------------------------------------------*) 931 932local val subs_comp = Subst.comp mk_clos 933 fun vars_sigma_norm (s,t) = 934 case t of 935 Comb(Rator,Rand) => Comb(vars_sigma_norm(s, Rator), 936 vars_sigma_norm(s, Rand)) 937 | Bv i => 938 (case Subst.exp_rel(s,i) of 939 (0, SOME v) => vars_sigma_norm (Subst.id, v) 940 | (lams,SOME v) => vars_sigma_norm (Subst.shift(lams,Subst.id),v) 941 | (lams,NONE) => Bv lams) 942 | Abs(Bvar,Body) => Abs(Bvar, vars_sigma_norm (Subst.lift(1,s), Body)) 943 | Fv _ => t 944 | Clos(Env,Body) => vars_sigma_norm (subs_comp(s,Env), Body) 945 | _ => t (* i.e., a const *) 946in 947fun norm_clos tm = vars_sigma_norm(Subst.id,tm) 948end 949 950fun size acc tlist = 951 case tlist of 952 [] => acc 953 | t :: ts => let 954 in 955 case t of 956 Comb(t1,t2) => size (1 + acc) (t1 :: t2 :: ts) 957 | Abs(_, b) => size (1 + acc) (b :: ts) 958 | Clos _ => size acc (push_clos t :: ts) 959 | _ => size (1 + acc) ts 960 end 961fun term_size t = size 0 [t] 962 963(*---------------------------------------------------------------------------* 964 * Traverse a term, performing a given (side-effecting) operation at the * 965 * leaves. For our purposes, bound variables can be ignored. * 966 *---------------------------------------------------------------------------*) 967 968fun trav f = 969 let fun trv (a as Fv _) = f a 970 | trv (a as Const _) = f a 971 | trv (Comb(Rator,Rand)) = (trv Rator; trv Rand) 972 | trv (Abs(Bvar,Body)) = (trv Bvar; trv Body) 973 | trv _ = () 974 in 975 trv o norm_clos 976 end; 977 978(*---------------------------------------------------------------------------* 979 * Raw syntax prettyprinter for terms. * 980 *---------------------------------------------------------------------------*) 981 982val app = "@" 983val lam = "|" 984val dollar = "$" 985val percent = "%" 986datatype pptask = ppTM of term | ppLAM | ppAPP of int 987fun pp_raw_term index tm = let 988 fun mkAPP [] = [ppAPP 1] 989 | mkAPP (ppAPP n :: rest) = ppAPP (n + 1) :: rest 990 | mkAPP rest = ppAPP 1 :: rest 991 fun pp acc tasklist = 992 case tasklist of 993 [] => String.concat (List.rev acc) 994 | ppTM (Abs(Bvar, Body)) :: rest => 995 pp acc (ppTM Bvar :: ppTM Body :: ppLAM :: rest) 996 | ppTM (Comb(Rator, Rand)) :: rest => 997 pp acc (ppTM Rator :: ppTM Rand :: mkAPP rest) 998 | ppTM (Bv i) :: rest => 999 pp (dollar ^ Int.toString i :: acc) rest 1000 | ppTM a :: rest => 1001 pp (percent ^ Int.toString (index a) :: acc) rest 1002 | ppLAM :: rest => pp (lam :: acc) rest 1003 | ppAPP n :: rest => 1004 pp (app ^ (if n = 1 then "" else Int.toString n) :: acc) rest 1005in 1006 pp [] [ppTM tm] 1007end 1008 1009fun write_raw index tm = pp_raw_term index (norm_clos tm) 1010 1011(*---------------------------------------------------------------------------* 1012 * Fetching theorems from disk. The following parses the "raw" term * 1013 * representation found in exported theory files. * 1014 *---------------------------------------------------------------------------*) 1015 1016local 1017datatype lexeme 1018 = app of int 1019 | lamb 1020 | ident of int 1021 | bvar of int; 1022 1023local val numeric = Char.contains "0123456789" 1024in 1025fun take_numb ss0 = 1026 let val (ns, ss1) = Substring.splitl numeric ss0 1027 in case Int.fromString (Substring.string ns) 1028 of SOME i => (i,ss1) 1029 | NONE => raise ERR "take_numb" "" 1030 end 1031end; 1032 1033(* don't allow numbers to be split across fragments *) 1034 1035fun lexer ss1 = 1036 case Substring.getc ss1 of 1037 NONE => NONE 1038 | SOME (c,ss2) => 1039 case c of 1040 #"|" => SOME(lamb, ss2) 1041 | #"%" => let val (n,ss3) = take_numb ss2 in SOME(ident n, ss3) end 1042 | #"$" => let val (n,ss3) = take_numb ss2 in SOME(bvar n, ss3) end 1043 | #"@" => 1044 (let val (n,ss3) = take_numb ss2 in SOME(app n, ss3) end 1045 handle HOL_ERR _ => SOME (app 1, ss2)) 1046 | _ => raise ERR "raw lexer" "bad character"; 1047 1048in 1049fun read_raw tmv = let 1050 fun index i = Vector.sub(tmv, i) 1051 fun parse (stk,ss) = 1052 case (stk, lexer ss) of 1053 (_, SOME (bvar n, rst)) => parse (Bv n::stk,rst) 1054 | (_, SOME (ident n, rst)) => parse (index n::stk,rst) 1055 | (stk, SOME (app n, rst)) => doapps n stk rst 1056 | (bd::bv::stk, SOME(lam,rst)) => parse (Abs(bv,bd)::stk, rst) 1057 | (_, SOME(lam, _)) => raise ERR "read_raw" "lam: small stack" 1058 | ([tm], NONE) => tm 1059 | ([], NONE) => raise ERR "read_raw" "eof: empty stack" 1060 | (_, NONE) => raise ERR "read_raw" "eof: large stack" 1061 and doapps n stk rst = 1062 if n = 0 then parse (stk,rst) 1063 else 1064 case stk of 1065 x::f::stk => doapps (n - 1) (Comb(f,x)::stk) rst 1066 | _ => raise ERR "read_raw" "app: small stack" 1067 1068in 1069fn s => parse ([], Substring.full s) 1070end 1071end (* local *) 1072 1073(* ---------------------------------------------------------------------- 1074 Is a term up-to-date wrt the theory? 1075 ---------------------------------------------------------------------- *) 1076 1077fun uptodate_term t = let 1078 open Type 1079 fun recurse tmlist = 1080 case tmlist of 1081 [] => true 1082 | t::rest => let 1083 in 1084 case t of 1085 Fv(_, ty) => Type.uptodate_type ty andalso recurse rest 1086 | Const(info, ty) => KernelSig.uptodate_id info andalso 1087 uptodate_type (to_hol_type ty) andalso 1088 recurse rest 1089 | Comb(f,x) => recurse (f::x::rest) 1090 | Abs(v,bod) => recurse (v::bod::rest) 1091 | Bv _ => recurse rest 1092 | Clos _ => recurse (push_clos t :: rest) 1093 end 1094in 1095 recurse [t] 1096end 1097 1098datatype lambda = 1099 VAR of string * hol_type 1100 | CONST of {Name: string, Thy: string, Ty: hol_type} 1101 | COMB of term * term 1102 | LAMB of term * term 1103 1104fun dest_term M = 1105 case M of 1106 Const _ => CONST (dest_thy_const M) 1107 | Fv p => VAR p 1108 | Comb p => COMB p 1109 | Abs _ => LAMB (dest_abs M) 1110 | Clos _ => dest_term (push_clos M) 1111 | Bv _ => raise Fail "dest_term applied to bound variable" 1112 1113fun identical t1 t2 = 1114 t1 = t2 orelse 1115 case (t1,t2) of 1116 (Clos _, _) => identical (push_clos t1) t2 1117 | (_, Clos _) => identical t1 (push_clos t2) 1118 | (Const p1, Const p2) => p1 = p2 1119 | (Fv p1, Fv p2) => p1 = p2 1120 | (Bv i1, Bv i2) => i1 = i2 1121 | (Comb(t1,t2), Comb(ta,tb)) => identical t1 ta andalso identical t2 tb 1122 | (Abs(v1,t1), Abs (v2, t2)) => v1 = v2 andalso identical t1 t2 1123 | _ => false 1124 1125end (* Term *) 1126