1structure Term :> Term = 2struct 3 4open Feedback Lib KernelTypes Type 5 6val kernelid = "expknl" 7 8infixr --> |-> 9 10val ERR = mk_HOL_ERR "Term" 11val WARN = HOL_WARNING "Term" 12 13(* used internally to avoid term rebuilding during substitution and 14 type instantiation *) 15exception Unchanged 16 17fun qcomb2 con (f, g) (x, y) = 18 let val fx = f x 19 in 20 let val gy = g y 21 in 22 con (fx, gy) 23 end handle Unchanged => con (fx, y) 24 end handle Unchanged => let val gy = g y in con (x, gy) end 25 26(* apply a function f under "constructor" con, handling Unchanged *) 27fun qcomb con f = qcomb2 con (f, f) 28 29type 'a set = 'a HOLset.set 30 31val compare_key = KernelSig.name_compare 32val compare_cinfo = KernelSig.id_compare 33 34val c2string = KernelSig.id_toString 35val id2string = KernelSig.name_toString 36 37val const_table = KernelSig.new_table() 38 39fun prim_delete_const kn = ignore (KernelSig.retire_name(const_table, kn)) 40 41fun inST s = not (null (KernelSig.listName const_table s)) 42 43fun prim_new_const (k as {Thy,Name}) ty = let 44 val id = KernelSig.insert(const_table, k, ty) 45in 46 Const(id, ty) 47end 48 49fun uptodate_term tm = let 50 fun recurse tmlist = 51 case tmlist of 52 [] => true 53 | tm :: rest => let 54 in 55 case tm of 56 Var(s, ty) => uptodate_type ty andalso recurse rest 57 | Const(info, ty) => KernelSig.uptodate_id info andalso 58 uptodate_type ty andalso 59 recurse rest 60 | App(f, x) => recurse (f::x::rest) 61 | Abs(v, body) => recurse (v::body::rest) 62 end 63in 64 recurse [tm] 65end 66 67fun thy_consts s = let 68 fun f (k, info as (_, ty), acc) = 69 if #Thy k = s andalso Type.uptodate_type ty then Const info :: acc 70 else acc 71in 72 KernelSig.foldl f [] const_table 73end 74 75fun del_segment s = KernelSig.del_segment(const_table, s) 76 77fun prim_decls s = KernelSig.listName const_table s 78 79fun decls s = let 80 fun foldthis (k,cinfo as (_, v),acc) = 81 if #Name k = s andalso Type.uptodate_type v then Const cinfo::acc else acc 82in 83 KernelSig.foldl foldthis [] const_table 84end 85 86fun all_consts () = let 87 fun foldthis (_,cinfo as (_, v),acc) = 88 if Type.uptodate_type v then Const cinfo :: acc else acc 89in 90 KernelSig.foldl foldthis [] const_table 91end 92 93 94fun type_of t = let 95 fun ty_of t k = 96 case t of 97 Var(_, ty) => k ty 98 | App(t1, t2) => ty_of t1 (fn ty => k (#2 (dom_rng ty))) 99 | Const(_, ty) => k ty 100 | Abs(Var(_, ty1), t) => ty_of t (fn tty => k (ty1 --> tty)) 101 | _ => raise Fail "Catastrophic invariant failure" 102in 103 ty_of t Lib.I 104end 105 106 107(* discriminators *) 108fun is_var (Var _) = true | is_var _ = false 109fun is_const (Const _) = true | is_const _ = false 110fun is_abs (Abs _) = true | is_abs _ = false 111fun is_comb (App _) = true | is_comb _ = false 112 113fun same_const t1 t2 = 114 case (t1, t2) of 115 (Const(r1, _), Const(r2, _)) => r1 = r2 116 | _ => false 117 118(* constructors - variables *) 119val mk_var = Var 120 121local val genvar_prefix = "%%genvar%%" 122 fun num2name i = genvar_prefix^Lib.int_to_string i 123 val nameStrm = Lib.mk_istream (fn x => x+1) 0 num2name 124in 125fun genvar ty = Var(state(next nameStrm), ty) 126 127fun genvars ty = 128 let fun gen acc n = if n <= 0 then rev acc else gen (genvar ty::acc) (n-1) 129 in gen [] 130 end 131 132fun is_genvar (Var(Name,_)) = String.isPrefix genvar_prefix Name 133 | is_genvar _ = false; 134end; 135 136(* constructors - constants *) 137fun mk_const(s, ty) = 138 case prim_decls s of 139 [] => raise ERR "mk_const" ("No constant with name "^s) 140 | [(_, (id,basety))] => if can (match_type basety) ty then 141 Const (id, ty) 142 else raise ERR "mk_const" 143 ("Not a type instance: "^c2string id) 144 | (_, (id,basety))::_ => 145 if can (match_type basety) ty then 146 (WARN "mk_const" (s^": more than one possibility"); Const (id,ty)) 147 else raise ERR "mk_const" ("Not a type instance: "^ c2string id) 148 149fun prim_mk_const (k as {Thy, Name}) = 150 case KernelSig.peek(const_table, k) of 151 NONE => raise ERR "prim_mk_const" ("No such constant: "^id2string k) 152 | SOME x => Const x 153 154fun mk_thy_const {Thy,Name,Ty} = let 155 val k = {Thy = Thy, Name = Name} 156in 157 case KernelSig.peek(const_table, k) of 158 NONE => raise ERR "mk_thy_const" ("No such constant: "^id2string k) 159 | SOME (id,basety) => if can (match_type basety) Ty then 160 Const(id, Ty) 161 else raise ERR "mk_thy_const" 162 ("Not a type instance: "^id2string k) 163end 164 165(* constructors - applications *) 166local val INCOMPAT_TYPES = Lib.C ERR "incompatible types" 167 fun lmk_comb err = 168 let fun loop (A,_) [] = A 169 | loop (A,typ) (tm::rst) = 170 let val (ty1,ty2) = with_exn Type.dom_rng typ err 171 in if type_of tm = ty1 172 then loop(App(A,tm),ty2) rst 173 else raise err 174 end 175 in fn (f,L) => loop(f, type_of f) L 176 end 177 val lmk_comb = (fn err => (* Profile.profile "lmk_comb" *)(lmk_comb err)) 178 val mk_comb0 = lmk_comb (INCOMPAT_TYPES "mk_comb") 179in 180 181fun mk_comb(r as (Abs(Var(_,Ty),_), Rand)) = 182 if type_of Rand = Ty then App r else raise INCOMPAT_TYPES "mk_comb" 183 | mk_comb(Rator,Rand) = mk_comb0 (Rator,[Rand]) 184 185val list_mk_comb = lmk_comb (INCOMPAT_TYPES "list_mk_comb") 186end; 187 188 189(* constructors - abstractions *) 190fun mk_abs(v, body) = 191 if is_var v then Abs(v, body) 192 else raise ERR "mk_abs" "Arg 1 not a variable" 193 194 195(* destructors *) 196 197fun dest_var (Var p) = p 198 | dest_var _ = raise ERR "dest_var" "Term not a variable" 199 200fun dest_const(Const(r, ty)) = (KernelSig.name_of r, ty) 201 | dest_const _ = raise ERR "dest_const" "Term not a constant" 202 203fun dest_thy_const t = let 204 open KernelSig 205in 206 case t of 207 Const(r, ty) => {Thy = seg_of r, Name = name_of r, Ty = ty} 208 | _ => raise ERR "dest_thy_const" "Term not a constant" 209end 210 211fun dest_comb(App p) = p 212 | dest_comb _ = raise ERR "dest_comb" "Term not a comb" 213 214val rator = #1 o dest_comb 215val rand = #2 o dest_comb 216 217fun dest_abs(Abs p) = p 218 | dest_abs _ = raise ERR "dest_abs" "Term not an abstraction" 219val bvar = #1 o dest_abs 220val body = #2 o dest_abs 221 222fun strip_binder binder = let 223 val f = case binder of 224 NONE => (fn t => if is_abs t then SOME t else NONE) 225 | SOME c => (fn t => let 226 val (rator, rand) = dest_comb t 227 in 228 if same_const rator c andalso is_abs rand then 229 SOME rand 230 else NONE 231 end handle HOL_ERR _ => NONE) 232 fun recurse acc t = 233 case f t of 234 NONE => (List.rev acc, t) 235 | SOME abs => let 236 val (v, body) = dest_abs abs 237 in 238 recurse (v::acc) body 239 end 240in 241 recurse [] 242end 243 244val strip_abs = strip_binder NONE 245 246(* free variable calculations *) 247 248fun var_compare p = 249 case p of 250 (Var(s1, ty1), Var(s2, ty2)) => let 251 in 252 case String.compare(s1, s2) of 253 EQUAL => Type.compare(ty1, ty2) 254 | x => x 255 end 256 | _ => raise ERR "var_compare" "variables required" 257 258val empty_varset = HOLset.empty var_compare 259 260local 261fun FV (v as Var _) A k = k (Lib.insert v A) 262 | FV (App(f, x)) A k = FV f A (fn q => FV x q k) 263 | FV (Abs(v, bdy)) A k = 264 if mem v A then FV bdy A k 265 else FV bdy A (fn q => k (Lib.set_diff q [v])) 266 | FV _ A k = k A 267in 268fun free_vars tm = FV tm [] Lib.I 269end 270 271fun free_vars_lr tm = let 272 fun FV (v as Var _) A = Lib.insert v A 273 | FV (App(f, x)) A = FV x (FV f A) 274 | FV (Abs(v, body)) A = if Lib.mem v A 275 then FV body A 276 else Lib.set_diff (FV body A) [v] 277 | FV _ A = A 278in 279 List.rev (FV tm []) 280end 281 282 283fun safe_delete(s, i) = HOLset.delete(s, i) handle HOLset.NotFound => s 284 285datatype FVaction = FVTM of term | DELvar of term 286 287fun FVL0 tlist acc = 288 case tlist of 289 [] => acc 290 | (FVTM t::ts) => let 291 in 292 case t of 293 (v as Var _) => FVL0 ts (HOLset.add(acc, v)) 294 | Const _ => FVL0 ts acc 295 | App(f, x) => FVL0 (FVTM f :: FVTM x :: ts) acc 296 | Abs(v, bdy) => 297 if HOLset.member(acc, v) then FVL0 (FVTM bdy :: ts) acc 298 else FVL0 (FVTM bdy :: DELvar v :: ts) acc 299 end 300 | DELvar v :: ts => FVL0 ts (safe_delete(acc, v)) 301 302fun FVL tlist = FVL0 (map FVTM tlist) 303 304 305local 306 fun vars (v as Var _) A = Lib.insert v A 307 | vars (App(f, x)) A = vars x (vars f A) 308 | vars (Abs(v, bdy)) A = vars bdy (vars v A) 309 | vars _ A = A 310in 311fun all_vars tm = vars tm [] 312end 313 314fun free_varsl tm_list = itlist (union o free_vars) tm_list [] 315fun all_varsl tm_list = itlist (union o all_vars) tm_list [] 316 317(* term comparison *) 318fun fast_term_eq t1 t2 = Portable.pointer_eq (t1,t2) 319structure Map = Binarymap 320val empty_env = Map.mkDict var_compare 321fun compare p = let 322 open Map 323 fun cmp n (E as (env1, env2)) (p as (t1,t2)) = 324 if n = 0 andalso fast_term_eq t1 t2 then EQUAL 325 else 326 case p of 327 (v1 as Var _, v2 as Var _) => let 328 in 329 case (peek(env1, v1), peek(env2, v2)) of 330 (NONE, NONE) => var_compare(v1, v2) 331 | (SOME _, NONE) => GREATER 332 | (NONE, SOME _) => LESS 333 | (SOME i, SOME j) => Int.compare(j, i) 334 (* flipping i & j deliberate; mimics deBruijn implementation's 335 behaviour, which would number variables in reverse order 336 from that done here *) 337 end 338 | (Var _, _) => LESS 339 | (_, Var _) => GREATER 340 | (Const(cid1, ty1), Const(cid2, ty2)) => let 341 in 342 case compare_cinfo(cid1, cid2) of 343 EQUAL => Type.compare(ty1, ty2) 344 | x => x 345 end 346 | (Const _, _) => LESS 347 | (_, Const _) => GREATER 348 | (App(M, N), App(P, Q)) => let 349 in 350 case cmp n E (M, P) of 351 EQUAL => cmp n E (N, Q) 352 | x => x 353 end 354 | (App _, Abs _) => LESS 355 | (Abs _, App _) => GREATER 356 | (Abs(v1, bdy1), Abs(v2, bdy2)) => let 357 in 358 case Type.compare(type_of v1, type_of v2) of 359 EQUAL => cmp (n + 1) (insert(env1, v1, n), insert(env2, v2, n)) 360 (bdy1, bdy2) 361 | x => x 362 end 363in 364 cmp 0 (empty_env, empty_env) p 365end 366 367val empty_tmset = HOLset.empty compare 368 369(* ---------------------------------------------------------------------- 370 All "atoms" (variables (bound or free) and constants). 371 372 Does not respect alpha-equivalence 373 ---------------------------------------------------------------------- *) 374 375fun all_atomsl tlist A = 376 case tlist of 377 [] => A 378 | t::ts => 379 let 380 in 381 case t of 382 Var _ => all_atomsl ts (HOLset.add(A,t)) 383 | Const _ => all_atomsl ts (HOLset.add(A,t)) 384 | App(Rator,Rand) => all_atomsl (Rator::Rand::ts) A 385 | Abs(v,body) => all_atomsl (body::ts) (HOLset.add(A,v)) 386 end 387 388fun all_atoms t = all_atomsl [t] empty_tmset 389 390 391fun aconv t1 t2 = compare(t1, t2) = EQUAL 392 393val term_eq = aconv 394 395fun free_in M N = let 396 val Mfvs = FVL [M] empty_varset 397 fun recurse t = 398 if compare(M, t) = EQUAL then true 399 else 400 case t of 401 Var _ => false 402 | Const _ => false 403 | App(f, x) => recurse f orelse recurse x 404 | Abs(v, bdy) => not (HOLset.member(Mfvs, v)) andalso 405 recurse bdy 406in 407 recurse N 408end 409 410fun var_occurs M = let 411 val v = case M of 412 Var v => v 413 | _ => raise ERR "var_occurs" "Term not a variable" 414 fun occ (Var u) = (v = u) 415 | occ (Const _) = false 416 | occ (App(f, x)) = occ f orelse occ x 417 | occ (Abs(Var u, body)) = u <> v andalso occ body 418 | occ (Abs _) = raise Fail "catastrophic invariant failure" 419in 420 occ 421end 422 423fun type_vars_in_term t = let 424 fun tyv t k = 425 case t of 426 Var(_, ty) => k (Type.type_vars ty) 427 | Const(_, ty) => k (Type.type_vars ty) 428 | App(f, x) => tyv f (fn fq => tyv x (fn xq => k (union fq xq))) 429 | Abs(x, b) => tyv x (fn xq => tyv b (fn bq => k (union xq bq))) 430in 431 tyv t Lib.I 432end 433 434(* two different substs; monomorphism restriction bites again; later code 435 gives these different types *) 436val emptyvsubst = Map.mkDict compare 437val emptysubst = Map.mkDict compare 438 439val empty_stringset = HOLset.empty String.compare 440 441(* it's hard to calculate free names simply by traversing a term because 442 of the situation where \x:ty1. body has x:ty1 and x:ty2 as free variables 443 in body. So, though it may be slightly less efficient, my solution here 444 is to just calculate the free variables and then calculate the image of 445 this set under name extraction *) 446val free_names = let 447 fun fold_name (v, acc) = HOLset.add(acc, #1 (dest_var v)) 448in 449 (fn t => HOLset.foldl fold_name empty_stringset (FVL [t] empty_varset)) 450end 451 452(* jrh's caml light HOL Light code 453let vsubst = 454 let mk_qcomb = qcomb(fun (x,y) -> Comb(x,y)) in 455 let rec vsubst theta tm = 456 match tm with 457 Var(_,_) -> (try snd(rev_assoc tm theta) 458 with Failure _ -> raise Unchanged) 459 | Const(_,_) -> raise Unchanged 460 | Comb(f,x) -> mk_qcomb (vsubst theta) (f,x) 461 | Abs(_,_) -> fst(vasubst theta tm) 462 and vasubst theta tm = 463 match tm with 464 Var(_,_) -> (try snd(rev_assoc tm theta),[tm] 465 with Failure _ -> raise Unchanged) 466 | Const(_,_) -> raise Unchanged 467 | Comb(l,r) -> (try let l',vs = vasubst theta l in 468 try let r',vt = vasubst theta r in 469 Comb(l',r'),union vs vt 470 with Unchanged -> Comb(l',r),vs 471 with Unchanged -> 472 let r',vt = vasubst theta r in Comb(l,r'),vt) 473 | Abs(v,bod) -> let theta' = filter (prefix<> v o snd) theta in 474 if theta' = [] then raise Unchanged else 475 let bod',vs = vasubst theta' bod in 476 let tms = map 477 (eval o fst o C rev_assoc theta') vs in 478 if exists (mem v) tms then 479 let fvs = itlist union tms (subtract (frees bod) vs) in 480 let v' = variant fvs v in 481 let bod',vars' = vasubst 482 (((eager [v'],v'),v)::theta') bod in 483 Abs(v',bod'),subtract vars' [v] 484 else 485 Abs(v,bod'),vs in 486 fun theta -> 487 if theta = [] then (fun tm -> tm) else 488 let atheta = map 489 (fun (t,x) -> if type_of t = snd(dest_var x) 490 then (lazy frees t,t),x 491 else failwith "vsubst: Bad substitution list") theta in 492 qtry(vsubst atheta);; 493*) 494 495fun set_name_variant nmset n = let 496 fun loop n = if HOLset.member(nmset, n) then loop (n ^ "'") else n 497in 498 loop n 499end 500 501 502local 503 open Map 504 505 datatype fvinfo = FVI of { current : term HOLset.set, 506 is_full : bool, 507 left : fvinfo option, (* also used for Abs *) 508 right : fvinfo option } 509 fun leaf (s, b) = 510 FVI {current = s, is_full = b, left = NONE, right = NONE} 511 fun current (FVI r) = #current r 512 fun is_full (FVI r) = #is_full r 513 fun left (FVI r) = valOf (#left r) 514 fun right (FVI r) = valOf (#right r) 515 (* computes a tree with information about the set of free variables in tm, 516 returns early when all redexes in theta have become bound *) 517 fun calculate_fvinfo theta_opt tm = 518 case tm of 519 Var _ => leaf (HOLset.singleton var_compare tm, true) 520 | Const _ => leaf (empty_varset, true) 521 | App (f, x) => 522 let 523 val fvs = calculate_fvinfo theta_opt f 524 val xvs = calculate_fvinfo theta_opt x 525 in 526 FVI {current = HOLset.union (current fvs, current xvs), 527 is_full = is_full fvs andalso is_full xvs, 528 left = SOME fvs, right = SOME xvs} 529 end 530 | Abs (v, body) => 531 let 532 val theta'_opt = Option.map 533 (fn theta => #1 (remove (theta, v)) handle NotFound => theta) 534 theta_opt 535 in 536 if isSome theta'_opt andalso numItems (valOf theta'_opt) = 0 then 537 (* return early *) 538 leaf (empty_varset, false) 539 else 540 let 541 val bodyvs = calculate_fvinfo theta'_opt body 542 in 543 FVI {current = safe_delete (current bodyvs, v), 544 is_full = is_full bodyvs, 545 left = SOME bodyvs, right = NONE} 546 end 547 end 548 (* expands a (possibly partial) tree with information about the set of free 549 variables in tm into a tree with full information *) 550 fun expand_partial_fvinfo tm fvi = 551 if is_full fvi then 552 raise Unchanged 553 else 554 case tm of 555 App (f, x) => 556 qcomb2 (fn (fvs, xvs) => 557 FVI {current = HOLset.union (current fvs, current xvs), 558 is_full = true, 559 left = SOME fvs, right = SOME xvs}) 560 (expand_partial_fvinfo f, expand_partial_fvinfo x) 561 (left fvi, right fvi) 562 | Abs (v, body) => 563 let 564 val bodyvs = expand_partial_fvinfo body (left fvi) 565 handle Option => calculate_fvinfo NONE body 566 in 567 FVI {current = safe_delete (current bodyvs, v), 568 is_full = true, 569 left = SOME bodyvs, right = NONE} 570 end 571 | _ => raise Fail "expand_partial_fvinfo: catastrophic invariant failure" 572 573 fun filtertheta theta fvset = let 574 (* Removes entries in theta for things not in fvset. theta likely to 575 be much smaller than fvset, so fold over that rather than the 576 other *) 577 fun foldthis (k,v,acc) = if HOLset.member(fvset, k) then insert(acc, k, v) 578 else acc 579 in 580 foldl foldthis emptyvsubst theta 581 end 582 583 fun augvsubst theta fvi tm = 584 case tm of 585 Var _ => (case peek (theta, tm) of NONE => raise Unchanged 586 | SOME (_, t) => t) 587 | Const _ => raise Unchanged 588 | App p => qcomb2 App 589 (augvsubst theta (left fvi), augvsubst theta (right fvi)) p 590 | Abs (v, body) => let 591 val theta' = #1 (remove (theta, v)) handle NotFound => theta 592 val _ = if numItems theta' = 0 then raise Unchanged else () 593 val (vname, vty) = dest_var v 594 val currentfvs = current fvi 595 val body_fvi = left fvi 596 (* first calculate the new names we are about to introduce into 597 the term *) 598 fun foldthis (k, v, acc) = 599 if HOLset.member (currentfvs, k) then 600 HOLset.union (acc, Susp.force (#1 v)) 601 else acc 602 val newnames = foldl foldthis empty_stringset theta' 603 in 604 if HOLset.member (newnames, vname) then 605 let 606 (* now need to vary v, avoiding both newnames, and also the 607 existing free-names of the whole term. *) 608 val body_fvi = expand_partial_fvinfo body body_fvi 609 handle Unchanged => body_fvi 610 val bodyfvs = current body_fvi 611 fun foldthis (fv, acc) = HOLset.add (acc, #1 (dest_var fv)) 612 val allfreenames = HOLset.foldl foldthis newnames bodyfvs 613 val new_vname = set_name_variant allfreenames vname 614 val new_v = mk_var (new_vname, vty) 615 val new_theta = 616 if HOLset.member (bodyfvs, v) then 617 let 618 val singleton = HOLset.singleton String.compare new_vname 619 in 620 insert (theta', v, 621 (Susp.delay (fn () => singleton), new_v)) 622 end 623 else theta' 624 in 625 Abs (new_v, augvsubst new_theta body_fvi body) 626 end 627 else 628 Abs (v, augvsubst theta' body_fvi body) 629 end 630 631 fun vsubst theta tm = 632 case tm of 633 Var _ => (case peek(theta, tm) of NONE => raise Unchanged 634 | SOME (_, t) => t) 635 | Const _ => raise Unchanged 636 | App p => qcomb App (vsubst theta) p 637 | Abs _ => let 638 val fvi = calculate_fvinfo (SOME theta) tm 639 val theta' = filtertheta theta (current fvi) 640 in 641 if numItems theta' = 0 then raise Unchanged 642 else augvsubst theta' fvi tm 643 end 644 645 fun ssubst theta t = 646 (* only used to substitute in fresh variables (genvars), so no 647 capture check -- potentially incorrect (because there is no 648 guarantee that genvars are actually fresh) *) 649 if numItems theta = 0 then raise Unchanged 650 else 651 case peek(theta, t) of 652 SOME v => v 653 | NONE => let 654 in 655 case t of 656 App p => qcomb App (ssubst theta) p 657 | Abs(v, body) => let 658 fun modify_theta (k,value,newtheta) = 659 if free_in v k then newtheta 660 else insert(newtheta, k, value) 661 val newtheta = foldl modify_theta emptysubst theta 662 in 663 Abs(v, ssubst newtheta body) 664 end 665 | _ => raise Unchanged 666 end 667 668 fun vsubst_insert (map, k, v) = 669 insert (map, k, (Susp.delay (fn () => free_names v), v)) 670in 671 672(* Due to the missing capture check in ssubst, subst can produce wrong results 673 (with accidental variable capture) unless all redexes in theta are 674 variables. 675 676 Therefore, all calls to subst that occur in Thm must ensure this 677 precondition. *) 678 679fun subst theta = 680 if null theta then I 681 else if List.all (is_var o #redex) theta then let 682 fun foldthis ({redex, residue}, acc) = let 683 val _ = type_of redex = type_of residue 684 orelse raise ERR "vsubst" "Bad substitution list" 685 in 686 if redex = residue then acc 687 else vsubst_insert (acc, redex, residue) 688 end 689 val atheta = List.foldl foldthis emptyvsubst theta 690 in 691 if numItems atheta = 0 then I 692 else (fn tm => vsubst atheta tm handle Unchanged => tm) 693 end 694 else let 695 fun foldthis ({redex,residue}, (theta1, theta2)) = let 696 val _ = type_of redex = type_of residue 697 orelse raise ERR "vsubst" "Bad substitution list" 698 val gv = genvar (type_of redex) 699 in 700 (insert (theta1, redex, gv), vsubst_insert (theta2, gv, residue)) 701 end 702 val (theta1, theta2) = 703 List.foldl foldthis (emptysubst, emptyvsubst) theta 704 in 705 (fn tm => vsubst theta2 (ssubst theta1 tm) 706 handle Unchanged => tm) 707 end 708 709end (* local *) 710 711 712(*---------------------------------------------------------------------------* 713 * Instantiate type variables in a term * 714 *---------------------------------------------------------------------------*) 715 716local 717 exception NeedToRename of term 718 structure Map = struct open Redblackmap end 719 fun inst1 theta ctxt t = 720 case t of 721 (c as Const(r, ty)) => (case ty_sub theta ty of 722 SAME => raise Unchanged 723 | DIFF ty => Const(r, ty)) 724 | (v as Var(name,ty0)) => let 725 val (changed, nv) = case ty_sub theta ty0 of 726 SAME => (false, v) 727 | DIFF ty => (true, Var(name, ty)) 728 in 729 case Map.peek (ctxt, nv) of 730 SOME oldtype => if oldtype = ty0 then () 731 else raise NeedToRename nv 732 | NONE => (); 733 if changed then nv 734 else raise Unchanged 735 end 736 | App p => qcomb App (inst1 theta ctxt) p 737 | Abs (v as Var(n, ty), body) => let 738 in 739 let 740 val (changed, v') = case ty_sub theta ty of 741 SAME => (false, v) 742 | DIFF ty' => (true, Var(n, ty')) 743 in let 744 val body' = SOME (inst1 theta (Map.insert(ctxt,v',ty)) body) 745 handle Unchanged => NONE 746 in 747 case (body', changed) of 748 (SOME t, _) => Abs(v', t) 749 | (NONE, true) => Abs(v', body) 750 | (NONE, false) => raise Unchanged 751 end handle e as NeedToRename v'' => 752 if v' = v'' then let 753 val free_names = free_names t 754 val new_name = set_name_variant free_names n 755 val newv = Var(new_name, ty) 756 in 757 inst1 theta ctxt (Abs(newv, subst [v |-> newv] body)) 758 end 759 else raise e 760 end 761 end 762 | Abs _ => raise Fail "inst1: catastrophic invariant failure!" 763in 764 765fun inst [] tm = tm 766 | inst theta tm = inst1 theta (Map.mkDict compare) tm handle Unchanged => tm 767end 768 769val inst : (hol_type, hol_type) Lib.subst -> term -> term = inst 770 771 772local 773 val FORMAT = ERR "list_mk_binder" 774 "expected first arg to be a constant of type :(<ty>_1 -> <ty>_2) -> <ty>_3" 775 fun check_opt NONE = Lib.I 776 | check_opt (SOME c) = 777 if not(is_const c) then raise FORMAT 778 else case total (fst o Type.dom_rng o fst o Type.dom_rng o type_of) c of 779 NONE => raise FORMAT 780 | SOME ty => (fn abs => 781 let val dom = fst(Type.dom_rng(type_of abs)) 782 in mk_comb (inst[ty |-> dom] c, abs) 783 end) 784in 785fun list_mk_binder binder = let 786 val f = check_opt binder 787 (* As of Mosml2.00, List.foldr is clearly not tail recursive, and you can 788 blow the stack with big lists here. Thus, the reversing of the list and 789 the use of foldl instead, relying on the fact that it's hard to imagine 790 not writing foldl tail-recursively *) 791in 792 fn (vlist, tm) => List.foldl (f o mk_abs) tm (List.rev vlist) 793end 794end (* local *) 795 796val list_mk_abs = list_mk_binder NONE 797 798 799fun beta_conv (App (Abs (v, body), x)) = 800 if x = v then body else subst [v |-> x] body 801 | beta_conv (App _) = 802 raise ERR "beta_conv" "LHS not an abstraction" 803 | beta_conv _ = 804 raise ERR "beta_conv" "Term not an application" 805 806val lazy_beta_conv = beta_conv 807 808fun eta_conv (Abs (x, App (f, x'))) = 809 if x = x' andalso not (free_in x f) then 810 f 811 else raise ERR "eta_conv" "Term not an eta-redex" 812 | eta_conv _ = 813 raise ERR "eta_conv" "Term not an eta-redex" 814 815 816(*---------------------------------------------------------------------------* 817 * Given a variable and a list of variables, if the variable does not exist * 818 * on the list, then return the variable. Otherwise, rename the variable and * 819 * try again. Note well that the variant uses only the name of the variable * 820 * as a basis for testing equality. Experience has shown that basing the * 821 * comparison on both the name and the type of the variable resulted in * 822 * needlessly confusing formulas occasionally being displayed in interactive * 823 * sessions. * 824 *---------------------------------------------------------------------------*) 825 826fun gen_variant P caller = 827 let fun var_name _ (Var(Name,_)) = Name 828 | var_name caller _ = raise ERR caller "not a variable" 829 fun vary vlist (Var(Name,Ty)) = 830 let val L = map (var_name caller) vlist 831 fun loop s = 832 if mem s L orelse P s then loop (s ^ "'") 833 else s 834 in mk_var(loop Name, Ty) 835 end 836 | vary _ _ = raise ERR caller "2nd argument should be a variable" 837 in vary 838 end; 839 840val variant = gen_variant inST "variant" 841val prim_variant = gen_variant (K false) "prim_variant"; 842 843fun numvariant avoids (Var(Name,Ty)) = 844 let 845 fun var_name (Var(Name,_)) = Name 846 | var_name _ = 847 raise ERR "numvariant" "Avoids list contains non-variable" 848 val nms = map var_name avoids 849 fun vary s = let val s' = Lexis.tmvar_vary s 850 in 851 if inST s' then vary s' else s' 852 end 853 in 854 mk_var(Lexis.gen_variant vary nms Name, Ty) 855 end 856 | numvariant _ _ = 857 raise ERR "numvariant" "2nd argument should be a variable" 858 859fun mk_primed_var p = gen_variant inST "mk_primed_var" [] (mk_var p) 860 861 862(* In the name-carrying implementation this operation is no longer constant 863 time *) 864fun rename_bvar newname t = 865 case t of 866 Abs(v, body) => let 867 val (nm, ty) = dest_var v 868 val newvar0 = mk_var(newname, ty) 869 val newvar = variant (free_vars t) newvar0 870 in 871 Abs(newvar, subst [v |-> newvar] body) 872 end 873 | _ => raise ERR "rename_bvar" "Term not an abstraction" 874 875 876 877(* ---------------------------------------------------------------------- 878 Matching 879 ---------------------------------------------------------------------- *) 880 881fun lookup x ids = let 882 fun look [] = if HOLset.member(ids, x) then SOME x else NONE 883 | look ({redex,residue}::t) = if x = redex then SOME residue else look t 884in 885 look 886end 887 888fun bvar_free (bvmap, tm) = let 889 (* return true if none of the free variables occur as keys in bvmap *) 890 fun recurse bs t = 891 case t of 892 v as Var _ => HOLset.member(bs, v) orelse 893 not (isSome (Map.peek(bvmap, v))) 894 | Const _ => true 895 | App(f,x) => recurse bs f andalso recurse bs x 896 | Abs(v, body) => recurse (HOLset.add(bs, v)) body 897in 898 Map.numItems bvmap = 0 orelse recurse empty_varset tm 899end 900 901fun MERR s = raise ERR "raw_match_term" s 902 903fun add_id v {ids, patbvars, obbvars, theta, n} = 904 {ids = HOLset.add(ids, v), patbvars = patbvars, obbvars = obbvars, n = n, 905 theta = theta} 906fun add_binding v tm {ids, patbvars, obbvars, theta, n} = 907 {ids = ids, patbvars = patbvars, obbvars = obbvars, n = n, 908 theta = (v |-> tm) :: theta} 909 910type tminfo = {ids : term HOLset.set, n : int, 911 patbvars : (term,int)Map.dict, 912 obbvars : (term,int)Map.dict, 913 theta : (term,term) Lib.subst} 914 915datatype tmpair = TMP of term * term 916 | BVrestore of {patbvars : (term,int)Map.dict, 917 obbvars : (term,int)Map.dict, 918 n : int} 919 920fun RM patobs (theta0 as (tminfo, tyS)) = 921 case patobs of 922 [] => theta0 923 | TMP po::rest => let 924 in 925 case po of 926 (v as Var(_, ty), tm) => let 927 in 928 case Map.peek(#patbvars tminfo, v) of 929 NONE => (* var on left not bound *) let 930 in 931 if bvar_free (#obbvars tminfo, tm) then 932 RM rest ((case lookup v (#ids tminfo) (#theta tminfo) of 933 NONE => if v = tm then add_id v tminfo 934 else add_binding v tm tminfo 935 | SOME tm' => if aconv tm' tm then tminfo 936 else MERR "double bind"), 937 Type.raw_match_type ty (type_of tm) tyS) 938 else 939 MERR "Attempt to capture bound variable" 940 end 941 | SOME i => if is_var tm andalso 942 Map.peek(#obbvars tminfo, tm) = SOME i 943 then 944 RM rest theta0 945 else MERR "Bound var doesn't match" 946 end 947 | (Const(c1, ty1), Const(c2, ty2)) => 948 if c1 <> c2 then MERR ("Different constants: "^c2string c1^" and "^ 949 c2string c2) 950 else RM rest (tminfo, Type.raw_match_type ty1 ty2 tyS) 951 | (App(f1, x1), App(f2, x2)) => 952 RM (TMP (f1, f2) :: TMP (x1, x2) :: rest) theta0 953 | (Abs(x1, bdy1), Abs(x2, bdy2)) => let 954 val tyS' = Type.raw_match_type (type_of x1) (type_of x2) tyS 955 val {ids, patbvars, obbvars, n, theta} = tminfo 956 in 957 RM (TMP (bdy1, bdy2) :: 958 BVrestore {patbvars = patbvars, obbvars = obbvars, n = n} :: 959 rest) 960 ({ids = #ids tminfo, n = n + 1, theta = theta, 961 patbvars = Map.insert(patbvars, x1, n), 962 obbvars = Map.insert(obbvars, x2, n)}, tyS') 963 end 964 | _ => MERR "different constructors" 965 end 966 | BVrestore{patbvars, obbvars, n} :: rest => let 967 val {ids, theta, ...} = tminfo 968 in 969 RM rest ({ids = ids, theta = theta, patbvars = patbvars, 970 obbvars = obbvars, n = n}, tyS) 971 end 972 973(* tyfixed: list of type variables that mustn't be instantiated 974 tmfixed: set of term variables that mustn't be instantiated 975 pat : term "pattern" to match 976 theta0 : an existing matching 977*) 978 979fun postRM (tmtheta : tminfo, tyS) = ((#theta tmtheta, #ids tmtheta), tyS) 980 981val empty_intsubst = Map.mkDict compare 982 983fun raw_match tyfixed tmfixed pat ob (tmS, tyS) = 984 postRM (RM [TMP (pat, ob)] ({ids = tmfixed, n = 0, theta = tmS, 985 patbvars = empty_intsubst, 986 obbvars = empty_intsubst}, 987 (tyS, tyfixed))) 988 989(* val raw_match0 = raw_match 990fun raw_match tyf tmf pat ob = 991 Profile.profile "raw_match" (raw_match0 tyf tmf pat ob) *) 992 993fun norm_subst ((tmS,_),(tyS,_)) = 994 let val Theta = inst tyS 995 fun del A [] = A 996 | del A ({redex,residue}::rst) = 997 del (let val redex' = Theta(redex) 998 in if residue=redex' then A else (redex' |-> residue)::A 999 end) rst 1000 in (del [] tmS,tyS) 1001 end 1002 1003fun match_terml tyfixed tmfixed pat ob = 1004 norm_subst (raw_match tyfixed tmfixed pat ob ([],[])) 1005 1006val match_term = match_terml [] empty_varset; 1007 1008fun size acc tlist = 1009 case tlist of 1010 [] => acc 1011 | t :: ts => let 1012 in 1013 case t of 1014 Var _ => size (1 + acc) ts 1015 | Const _ => size (1 + acc) ts 1016 | App(t1, t2) => size (1 + acc) (t1 :: t2 :: ts) 1017 | Abs(_, b) => size (1 + acc) (b :: ts) 1018 end 1019 1020fun term_size t = size 0 [t] 1021 1022 1023 1024 1025val imp = let 1026 val k = {Name = "==>", Thy = "min"} 1027in 1028 prim_new_const k (bool --> bool --> bool) 1029end 1030 1031val equality = let 1032 val k = {Name = "=", Thy = "min"} 1033in 1034 prim_new_const k (alpha --> alpha --> bool) 1035end 1036 1037val select = let 1038 val k = {Name = "@", Thy = "min"} 1039in 1040 prim_new_const k ((alpha --> bool) --> alpha) 1041end 1042 1043fun dest_eq_ty t = let 1044 val (fx, y) = dest_comb t 1045 val (f, x) = dest_comb fx 1046in 1047 if same_const f equality then (x, y, type_of x) 1048 else raise ERR "dest_eq_ty" "Term not an equality" 1049end 1050 1051fun prim_mk_eq ty t1 t2 = 1052 App(App(inst [alpha |-> ty] equality, t1), t2) 1053 1054(*val prim_mk_eq = 1055 (fn ty => fn t1 => Profile.profile "prim_mk_eq" (prim_mk_eq ty t1)) *) 1056 1057fun prim_mk_imp t1 t2 = App(App(imp, t1), t2) 1058 1059(* val prim_mk_imp = (fn t1 => Profile.profile "prim_mk_imp" (prim_mk_imp t1))*) 1060 1061(* ---------------------------------------------------------------------- 1062 dest_term and the lambda type 1063 ---------------------------------------------------------------------- *) 1064 1065datatype lambda = 1066 VAR of string * hol_type 1067 | CONST of {Name: string, Thy: string, Ty: hol_type} 1068 | COMB of term * term 1069 | LAMB of term * term 1070 1071fun dest_term M = 1072 case M of 1073 Const _ => CONST (dest_thy_const M) 1074 | Var p => VAR p 1075 | App p => COMB p 1076 | Abs p => LAMB p 1077 1078fun identical t1 t2 = t1 = t2 1079 1080(*---------------------------------------------------------------------------* 1081 * Raw syntax prettyprinter for terms. * 1082 *---------------------------------------------------------------------------*) 1083 1084val app = "@" 1085val lam = "|" 1086val percent = "%" 1087 1088datatype pptask = ppTM of term | ppLAM | ppAPP of int 1089fun pp_raw_term index tm = let 1090 fun mkAPP (ppAPP n :: rest) = ppAPP (n + 1) :: rest 1091 | mkAPP rest = ppAPP 1 :: rest 1092 fun pp acc tasklist = 1093 case tasklist of 1094 [] => String.concat (List.rev acc) 1095 | ppTM (Abs(Bvar, Body)) :: rest => 1096 pp acc (ppTM Bvar :: ppTM Body :: ppLAM :: rest) 1097 | ppTM (App(Rator, Rand)) :: rest => 1098 pp acc (ppTM Rator :: ppTM Rand :: mkAPP rest) 1099 | ppTM vc :: rest => 1100 pp (percent ^ Int.toString (index vc) :: acc) rest 1101 | ppLAM :: rest => pp ("|" :: acc) rest 1102 | ppAPP n :: rest => 1103 pp ("@" ^ (if n = 1 then "" else Int.toString n) :: acc) rest 1104in 1105 pp [] [ppTM tm] 1106end 1107val write_raw = pp_raw_term 1108 1109local 1110datatype tok = lam | id of int | app of int 1111open StringCvt 1112 1113fun readtok (c : (char, cs) reader) cs = let 1114 val intread = Int.scan DEC c 1115in 1116 case c cs of 1117 NONE => NONE 1118 | SOME (#"|",cs') => SOME (lam,cs') 1119 | SOME (#"@",cs') => 1120 (case intread cs' of 1121 NONE => SOME (app 1,cs') 1122 | SOME (i,cs'') => SOME (app i, cs'')) 1123 | SOME (c,cs') => (case intread cs' of 1124 NONE => NONE 1125 | SOME (i,cs'') => SOME(id i, cs'')) 1126end 1127 1128fun parse tmv c cs0 = let 1129 fun adv cs = case readtok c cs of NONE => (NONE, cs) 1130 | SOME (t, cs') => (SOME t, cs') 1131 fun parse_term stk cur = 1132 case (stk, cur) of 1133 ([t], (NONE,cs)) => SOME (t, cs) 1134 | ([], (NONE, _)) => raise Fail "raw_parse.eof: empty stack" 1135 | (_, (NONE, _)) => raise Fail "raw_parse.eof: large stack" 1136 | (body :: bvar :: stk, (SOME lam, cs')) => 1137 parse_term (Abs(bvar,body) :: stk) (adv cs') 1138 | (_, (SOME lam, _)) => raise Fail "raw_parse.abs: short stack" 1139 | (stk, (SOME (app i), cs')) => doapp i stk cs' 1140 | (stk, (SOME (id i), cs')) => 1141 parse_term (Vector.sub(tmv, i) :: stk) (adv cs') 1142 and doapp i stk cs = 1143 if i = 0 then parse_term stk (adv cs) 1144 else 1145 case stk of 1146 x :: f :: stk => doapp (i - 1) (App(f,x) :: stk) cs 1147 | _ => raise Fail "raw_parse.app: short stack" 1148in 1149 parse_term [] (adv cs0) 1150end 1151 1152 1153in 1154 1155fun read_raw tmv s = 1156 valOf (scanString (parse tmv) s) 1157 1158end (* local *) 1159 1160end (* struct *) 1161