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