1structure ANF :> ANF = 2struct 3 4(* For interactive use: 5 6 loadPath := 7 (concat Globals.HOLDIR "/examples/dev/sw") :: 8 !loadPath; 9 10app load ["pairLib", "cpsSyntax", "wordsLib"]; 11 quietdec := true; 12 open pairLib pairTheory PairRules pairSyntax cpsTheory cpsSyntax; 13 quietdec := false; 14*) 15open HolKernel Parse boolLib bossLib 16 pairLib pairSyntax pairTheory PairRules cpsTheory cpsSyntax; 17 18type env = (term * (bool * thm * thm * thm)) list; 19 20val _ = (Globals.priming := SOME ""); 21 22 23 24(*---------------------------------------------------------------------------*) 25(* Ensure that each let-bound variable name in a term is different than the *) 26(* others. *) 27(*---------------------------------------------------------------------------*) 28 29fun std_bvars stem tm = 30 let open Lib 31 fun num2name i = stem^Lib.int_to_string i 32 val nameStrm = Lib.mk_istream (fn x => x+1) 0 num2name 33 fun next_name () = state(next nameStrm) 34 fun trav M = 35 if is_comb M then 36 let val (M1,M2) = dest_comb M 37 val M1' = trav M1 38 val M2' = trav M2 39 in mk_comb(M1',M2') 40 end else 41 if is_abs M then 42 let val (v,N) = dest_abs(rename_bvar (next_name()) M) 43 in mk_abs(v,trav N) 44 end 45 else M 46 in 47 trav tm 48 end; 49 50fun STD_BVARS_CONV stem tm = 51 let val tm' = std_bvars stem tm 52 in Thm.ALPHA tm tm' 53 end; 54 55val STD_BVARS = CONV_RULE o STD_BVARS_CONV; 56val STD_BVARS_TAC = CONV_TAC o STD_BVARS_CONV; 57 58(*---------------------------------------------------------------------------*) 59(* Compiler frontend ... largely pinched from examples/dev/compile.sml *) 60(*---------------------------------------------------------------------------*) 61 62(*****************************************************************************) 63(* Error reporting function *) 64(*****************************************************************************) 65 66val ERR = mk_HOL_ERR "ANF"; 67 68(*****************************************************************************) 69(* List of definitions (useful for rewriting) *) 70(*****************************************************************************) 71 72val SimpThms = [Seq_def,Par_def,Ite_def,Rec_def]; 73 74(*****************************************************************************) 75(* An expression is just a HOL term built using expressions defined earlier *) 76(* in a program (see description of programs below) and Seq, Par, *) 77(* Ite and Rec: *) 78(* *) 79(* expr := Seq expr expr *) 80(* | Par expr expr *) 81(* | Ite expr expr expr *) 82(* | Rec expr expr expr *) 83(* *) 84(*****************************************************************************) 85 86(*****************************************************************************) 87(* Convert_CONV ``\(x1,...,xn). tm[x1,...,xn]`` returns a theorem *) 88(* *) 89(* |- (\(x1,...,xn). tm[x1,...,xn]) = p *) 90(* *) 91(* where p is a combinatory expression built from the combinators *) 92(* Seq, Par and Ite. An example is: *) 93(* *) 94(* - Convert_CONV ``\(x,y). if x < y then y-x else x-y``; *) 95(* > val it = *) 96(* |- (\(x,y). (if x < y then y - x else x - y)) = *) 97(* Ite (Seq (Par (\(x,y). x) (\(x,y). y)) (UNCURRY $<)) *) 98(* (Seq (Par (\(x,y). y) (\(x,y). x)) (UNCURRY $-)) *) 99(* (Seq (Par (\(x,y). x) (\(x,y). y)) (UNCURRY $-)) *) 100(* *) 101(* Notice that curried operators are uncurried. *) 102(* *) 103(*****************************************************************************) 104 105val LET_SEQ_PAR_THM = Q.prove 106(`!f1 f2 f3. Seq (Par f1 f2) f3 = \x. let v = f2 x in f3 (f1 x,v)`, 107 RW_TAC std_ss [Seq_def, Par_def, LET_DEF]); 108 109val SEQ_PAR_I_THM = Q.prove 110(`!f2 f3. Seq (Par (\x.x) f2) f3 = \x. let v = f2 x in f3 (x,v)`, 111 RW_TAC std_ss [LET_SEQ_PAR_THM,combinTheory.I_THM]); 112 113 114fun is_word_literal tm = 115 ((is_comb tm) andalso 116 let val (c,args) = strip_comb tm 117 val {Name,Thy,Ty} = dest_thy_const c 118 in Name = "n2w" andalso numSyntax.is_numeral (hd args) 119 end) 120 handle HOL_ERR _ => raise ERR "is_word_literal" ""; 121 122 123fun Convert_CONV f = 124 let val (args,t) = 125 dest_pabs f 126 handle HOL_ERR _ 127 => (print_term f; print"\n"; 128 print "is not an abstraction\n"; 129 raise ERR "Convert_CONV" "not an abstraction") 130 in 131 if not(free_vars f = []) 132 then (print_term f; print "\n"; 133 print "has free variables: "; 134 map (fn t => (print_term t; print " "))(rev(free_vars f)); print "\n"; 135 raise ERR "Convert_CONV" "disallowed free variables") 136 else if is_var t orelse is_word_literal t orelse numSyntax.is_numeral t orelse is_const t 137 then REFL f 138 else if is_pair t 139 then let val (t1,t2) = dest_pair t 140 val f1 = mk_pabs(args,t1) 141 val f2 = mk_pabs(args,t2) 142 val th1 = PBETA_CONV (mk_comb(f1,args)) 143 val th2 = PBETA_CONV (mk_comb(f2,args)) 144 val th3 = ISPECL [f1,f2] Par_def 145 val ptm = mk_pabs(args, mk_pair(mk_comb(f1,args),mk_comb(f2,args))) 146 val th4 = TRANS th3 (PALPHA (rhs(concl th3)) ptm) 147 val th5 = CONV_RULE 148 (RHS_CONV 149 (PABS_CONV 150 (RAND_CONV(REWR_CONV th2) 151 THENC RATOR_CONV(RAND_CONV(REWR_CONV th1))))) 152 th4 153 val th6 = GSYM th5 154 in 155 if aconv (lhs(concl th6)) f 156 then CONV_RULE 157 (RHS_CONV 158 ((RAND_CONV Convert_CONV) 159 THENC (RATOR_CONV(RAND_CONV Convert_CONV)))) 160 th6 161 else (print "bad Par case\n"; 162 raise ERR "Convert_CONV" "shouldn't happen") 163 end 164 else if is_cond t 165 then let val (b,t1,t2) = dest_cond t 166 val fb = mk_pabs(args,b) 167 val f1 = mk_pabs(args,t1) 168 val f2 = mk_pabs(args,t2) 169 val thb = PBETA_CONV (mk_comb(fb,args)) 170 val th1 = PBETA_CONV (mk_comb(f1,args)) 171 val th2 = PBETA_CONV (mk_comb(f2,args)) 172 val th3 = ISPECL [fb,f1,f2] Ite_def 173 val ptm = mk_pabs 174 (args, 175 mk_cond(mk_comb(fb,args),mk_comb(f1,args),mk_comb(f2,args))) 176 val th4 = TRANS th3 (PALPHA (rhs(concl th3)) ptm) 177 val th5 = CONV_RULE 178 (RHS_CONV 179 (PABS_CONV 180 (RAND_CONV(REWR_CONV th2) 181 THENC RATOR_CONV(RAND_CONV(REWR_CONV th1)) 182 THENC RATOR_CONV(RATOR_CONV(RAND_CONV(REWR_CONV thb)))))) 183 th4 184 val th6 = GSYM th5 185 in 186 if aconv (lhs(concl th6)) f 187 then CONV_RULE 188 (RHS_CONV 189 ((RAND_CONV Convert_CONV) 190 THENC (RATOR_CONV(RAND_CONV Convert_CONV)) 191 THENC (RATOR_CONV(RATOR_CONV(RAND_CONV Convert_CONV))))) 192 th6 193 else (print "bad Ite case\n"; 194 raise ERR "Convert_CONV" "shouldn't happen") 195 end 196 else if is_let t (* t = LET (\v. N) M *) 197 then let val (v,M,N) = dest_plet t 198 val f1 = mk_pabs(args,args) 199 val f2 = mk_pabs(args,M) 200 val f3 = mk_pabs(mk_pair(args,v),N) 201 val th1 = ISPECL [f1,f2,f3] LET_SEQ_PAR_THM 202 val th2 = CONV_RULE(RHS_CONV(SIMP_CONV std_ss [LAMBDA_PROD])) th1 203 val th3 = TRANS th2 (SYM (QCONV (SIMP_CONV std_ss [LAMBDA_PROD]) f)) 204 val th4 = SYM th3 205 in 206 if aconv (lhs(concl th4)) f 207 then CONV_RULE 208 (RHS_CONV 209 ((RAND_CONV Convert_CONV) 210 THENC (RATOR_CONV(RAND_CONV (RAND_CONV Convert_CONV))))) 211 th4 212 else (print "bad let case\n"; 213 raise ERR "Convert_CONV" "shouldn't happen") 214 end 215 else if is_comb t 216 then let val th0 = (REWR_CONV (GSYM UNCURRY_DEF) ORELSEC REFL) t 217 val (t1,t2) = dest_comb(rhs(concl th0)) 218 val f1 = mk_pabs(args,t1) 219 val f2 = mk_pabs(args,t2) 220 val th1 = ISPECL [f2,t1] Seq_def 221 val ptm = mk_pabs(args, mk_comb(t1,mk_comb(f2,args))) 222 val th2 = TRANS th1 (PALPHA (rhs(concl th1)) ptm) 223 val th3 = PBETA_CONV(mk_comb(f2,args)) 224 val th4 = GSYM(CONV_RULE(RHS_CONV(PABS_CONV(RAND_CONV(REWR_CONV th3))))th2) 225 val th5 = CONV_RULE(LHS_CONV(PABS_CONV(REWR_CONV(GSYM th0)))) th4 226 in 227 if aconv (lhs(concl th5)) f 228 then CONV_RULE 229 (RHS_CONV 230 (RATOR_CONV(RAND_CONV Convert_CONV))) 231 th5 232 else (print "bad Seq case\n"; 233 raise ERR "Convert_CONV" "shouldn't happen") 234 end 235 else (print_term f; print "\n"; 236 print "shouldn't get this case (not first-order)!\n"; 237 raise ERR "Convert_CONV" "shouldn't happen") 238 end; 239 240(*****************************************************************************) 241(* Predicate to test whether a term occurs in another term *) 242(*****************************************************************************) 243 244fun occurs_in t1 t2 = can (find_term (aconv t1)) t2; 245 246(*****************************************************************************) 247(* Convert (|- f x = e) returns a theorem *) 248(* *) 249(* |- f = p *) 250(* *) 251(* where p is a combinatory expression built from the combinators Seq, Par *) 252(* and Ite. *) 253(*****************************************************************************) 254fun Convert defth = 255 let val (lt,rt) = 256 dest_eq(concl(SPEC_ALL defth)) 257 handle HOL_ERR _ 258 => (print "not an equation\n"; 259 raise ERR "Convert" "not an equation") 260 val (func,args) = 261 dest_comb lt 262 handle HOL_ERR _ => 263 (print "lhs not a comb\n"; 264 raise ERR "Convert" "lhs not a comb") 265 val _ = if not(is_const func) 266 then (print_term func; print " is not a constant\n"; 267 raise ERR "Convert" "rator of lhs not a constant") 268 else () 269 val _ = if not(subtract (free_vars rt) (free_vars lt) = []) 270 then (print "definition rhs has unbound variables: "; 271 map (fn t => (print_term t; print " ")) 272 (rev(subtract (free_vars rt) (free_vars lt))); 273 print "\n"; 274 raise ERR "Convert" "definition rhs has unbound variables") 275 else () 276 in 277 let val f = mk_pabs(args,rt) 278 val th1 = Convert_CONV f 279 val th2 = PABS args (SPEC_ALL defth) 280 val th3 = TRANS th2 th1 281 in 282 CONV_RULE (LHS_CONV PETA_CONV) th3 283 end 284 end; 285 286 287(*****************************************************************************) 288(* RecConvert (|- f x = if f1 x then f2 x else f(f3 x)) *) 289(* (|- TOTAL(f1,f2,f3)) *) 290(* *) 291(* returns a theorem *) 292(* *) 293(* |- f = Rec(p1,p2,p3) *) 294(* *) 295(* where p1, p2 and p3 are combinatory expressions built from the *) 296(* combinators Seq, Par and Ite. *) 297(* *) 298(* For example, given: *) 299(* *) 300(* FactIter; *) 301(* > val it = *) 302(* |- FactIter (n,acc) = *) 303(* (if n = 0 then (n,acc) else FactIter (n - 1,n * acc)) *) 304(* *) 305(* - FactIter_TOTAL; *) 306(* > val it = *) 307(* |- TOTAL *) 308(* ((\(n,acc). n = 0), *) 309(* (\(n,acc). (n,acc)), *) 310(* (\(n,acc). (n-1, n*acc))) *) 311(* *) 312(* then: *) 313(* *) 314(* - RecConvert FactIter FactIter_TOTAL; *) 315(* > val it = *) 316(* |- FactIter = *) 317(* Rec (Seq (Par (\(n,acc). n) (\(n,acc). 0)) (UNCURRY $=)) *) 318(* (Par (\(n,acc). n) (\(n,acc). acc)) *) 319(* (Par (Seq (Par (\(n,acc). n) (\(n,acc). 1)) (UNCURRY $-)) *) 320(* (Seq (Par (\(n,acc). n) (\(n,acc). acc)) (UNCURRY $* ))) *) 321(* *) 322(*****************************************************************************) 323 324val I_DEF_ALT = Q.prove(`I = \x.x`,SIMP_TAC std_ss [FUN_EQ_THM]); 325val Rec_INTRO_ALT = REWRITE_RULE[I_DEF_ALT] Rec_INTRO; 326val Seq_o = Q.prove(`!f g. f o g = Seq g f`, 327 SIMP_TAC std_ss [combinTheory.o_DEF,Seq_def]); 328 329fun RecConvert defth = 330 let val (lt,rt) = 331 dest_eq(concl(SPEC_ALL defth)) 332 handle HOL_ERR _ 333 => (print "not an equation\n"; 334 raise ERR "RecConvert" "not an equation") 335 val (func,args) = 336 dest_comb lt 337 handle HOL_ERR _ => 338 (print "lhs not a comb\n"; 339 raise ERR "RecConvert" "lhs not a comb") 340 val _ = if not(is_const func) 341 then (print_term func; print " is not a constant\n"; 342 raise ERR "RecConvert" "rator of lhs not a constant") 343 else () 344 val (b,t1,t2) = 345 dest_cond rt 346 handle HOL_ERR _ 347 => (print "rhs not a conditional\n"; 348 raise ERR "RecConvert" "rhs not a conditional") 349 val _ = if not(subtract (free_vars rt) (free_vars lt) = []) 350 then (print "definition rhs has unbound variables: "; 351 map (fn t => (print_term t; print " ")) 352 (rev(subtract (free_vars rt) (free_vars lt))); 353 print "\n"; 354 raise ERR "RecConvert" "definition rhs has unbound variables") 355 else() 356 in 357 if (is_comb t2 358 andalso aconv (rator t2) func 359 andalso not(occurs_in func b) 360 andalso not(occurs_in func t1) 361 andalso not(occurs_in func (rand t2))) 362 then 363 let val fb = mk_pabs(args,b) 364 val f1 = mk_pabs(args,t1) 365 val f2 = mk_pabs(args,rand t2) 366 val thm = ISPECL[func,fb,f1,f2] Rec_INTRO 367 val M = fst(dest_imp(concl thm)) 368 val (v,body) = dest_forall M 369 val M' = rhs(concl(DEPTH_CONV PBETA_CONV 370 (mk_pforall(args,subst [v |-> args]body)))) 371 val MeqM' = prove(mk_eq(M,M'), 372 Ho_Rewrite.REWRITE_TAC[LAMBDA_PROD] 373 THEN PBETA_TAC THEN REFL_TAC) 374 val thm1 = PURE_REWRITE_RULE[MeqM'] thm 375 val thm2 = PGEN args defth 376 val thm3 = MP thm1 thm2 377 val N = fst(dest_imp(concl thm3)) 378 val (R,tm) = dest_exists N 379 val (tm1,tm2) = dest_conj tm 380 val (v,body) = dest_forall tm2 381 val tm2' = rhs(concl(DEPTH_CONV PBETA_CONV 382 (mk_pforall(args,subst [v |-> args]body)))) 383 val N' = mk_exists(R,mk_conj(tm1,tm2')) 384 val NeqN' = prove(mk_eq(N,N'), 385 Ho_Rewrite.REWRITE_TAC[LAMBDA_PROD] 386 THEN PBETA_TAC THEN REFL_TAC) 387 val thm4 = PURE_REWRITE_RULE[NeqN'] thm3 388 val thm5 = UNDISCH thm4 389 val thm6 = CONV_RULE (RHS_CONV 390 (RAND_CONV Convert_CONV THENC 391 RATOR_CONV(RAND_CONV Convert_CONV) THENC 392 RATOR_CONV(RATOR_CONV(RAND_CONV Convert_CONV)))) 393 thm5 394 in thm6 395 end 396 else if occurs_in func rt 397 then (print "definition of: "; print_term func; 398 print " is not tail recursive"; print "\n"; 399 raise ERR "RecConvert" "not tail recursive") 400 else raise ERR "RecConvert" "this shouldn't happen" 401 end; 402 403(*---------------------------------------------------------------------------*) 404(* Convert a possibly (tail) recursive equation to combinator form, either *) 405(* by calling Convert or RecConvert. *) 406(*---------------------------------------------------------------------------*) 407 408fun toComb def = 409 let val (l,r) = dest_eq(snd(strip_forall(concl def))) 410 val (func,args) = dest_comb l 411 val is_recursive = Lib.can (find_term (aconv func)) r 412(* val comb_exp_thm = if is_recursive then RecConvert def else Convert def *) 413 val comb_exp_thm = Convert def 414 in 415 (is_recursive,lhs(concl comb_exp_thm), args, comb_exp_thm) 416 end; 417 418(*---------------------------------------------------------------------------*) 419(* Takes theorem |- f = <combinator-form> , where f is not a recursive *) 420(* function, and returns the CPS-ed version of <combinator-form>. Actually, *) 421(* the returned value is in "A-Normal" form (uses lets). *) 422(*---------------------------------------------------------------------------*) 423 424val LET_ID = METIS_PROVE [] ``!f M. (LET M (\x. x)) = M (\x. x)`` 425 426fun REPAIR_SYNTAX_RESTRICTIONS_CONV t = 427 if (is_comb t) then 428 let 429 val (f, args) = strip_comb t; 430 val {Name,Thy,Ty} = dest_thy_const f; 431 in 432 if ((Name = "UNCURRY") andalso (Thy = "pair") andalso 433 (length args = 2)) then 434 let 435 val pair = (el 2 args); 436 val (l, r) = dest_pair pair; 437 val is_word_l = is_word_literal l; 438 val is_word_r = is_word_literal r; 439 440 val _ = if (is_word_l andalso is_word_r) then 441 (raise (ERR "" "Can't repair syntax")) 442 else () 443 in 444 if (is_word_l orelse is_word_r) then 445 let 446 val oper = el 1 args; 447 val {Name,Thy,Ty} = dest_thy_const oper; 448 449 val _ = if (not ((Thy="words") orelse (Name = "=" andalso (Thy="min")))) then 450 raise (ERR "" "Can't repair syntax") 451 else () 452 453 val _ = if ((Name = "word_mul")) then 454 raise (ERR "" "Can't repair syntax") 455 else () 456 457 458 fun COMM_OPER_CONV t = 459 (CURRY_CONV THENC 460 ONCE_REWRITE_CONV [wordsTheory.WORD_ADD_COMM, 461 wordsTheory.WORD_OR_COMM, 462 wordsTheory.WORD_AND_COMM, 463 wordsTheory.WORD_XOR_COMM, 464 EQ_SYM_EQ 465 ] THENC 466 UNCURRY_CONV) t 467 in 468 if (is_word_l) then 469 if ((Name = "word_add") orelse 470 (Name = "word_or") orelse 471 (Name = "word_and") orelse 472 (Name = "word_xor") orelse 473 (Name = "=")) then 474 COMM_OPER_CONV t 475 else 476 raise (ERR "" "Can't repair syntax") 477 else REFL t 478 end 479 else 480 REFL t 481 end 482 else 483 (COMB_CONV REPAIR_SYNTAX_RESTRICTIONS_CONV) t 484 end 485 else if (is_abs t) then 486 (ABS_CONV REPAIR_SYNTAX_RESTRICTIONS_CONV) t 487 else 488 REFL t; 489 490fun VAR_LET_CONV t = 491 let open pairSyntax 492 val (_,tm) = dest_let t; 493 in 494 if is_vstruct tm orelse 495 ((is_word_literal tm orelse numSyntax.is_numeral tm)) 496 497 then 498 (REWR_CONV LET_THM THENC GEN_BETA_CONV THENC REPAIR_SYNTAX_RESTRICTIONS_CONV) t 499 else raise ERR "VAR_LET_CONV" "" 500 end; 501 502fun LET_UNCURRY_CONV t = 503 let open pairSyntax 504 val (_,tm) = dest_let t; 505 val (f, _) = strip_comb tm 506 val {Name,Thy,Ty} = dest_thy_const f; 507 val _ = if (((Name = "UNCURRY") andalso (Thy = "pair")) orelse 508 ((Name = "COND") andalso (Thy = "bool"))) 509 then raise UNCHANGED else () 510 in 511 (RAND_CONV UNCURRY_CONV) t 512 end; 513 514(*val t = rhs (concl (SPEC_ALL thm16)) 515 val thm17 = CONV_RULE (DEPTH_CONV VAR_LET_CONV) thm16*) 516 517 518fun ELIM_PAIR_LET_CONV t = 519let 520 val (body, value) = dest_let t; 521in 522 if (is_vstruct value) then 523 (REWR_CONV LET_THM THENC GEN_BETA_CONV) t 524 else 525 let 526 val thm = CURRY_CONV (liteLib.mk_icomb (body, value)) 527 val rhs_thm = rhs (concl thm); 528 val (body, v1) = dest_comb rhs_thm 529 val (body, v2) = dest_comb body 530 val (varlist, body) = strip_pabs body; 531 532 val body = mk_let (mk_pabs(el 2 varlist, body), v1); 533 val body = mk_let (mk_pabs(el 1 varlist, body), v2); 534 val thm = prove (mk_eq (t, body), 535 CONV_TAC (DEPTH_CONV let_CONV) THEN REWRITE_TAC[]) 536 in 537 thm 538 end 539end; 540 541 542val CPS_REWRITES = prove (`` 543 (!f1 f2. Seq f1 f2 = \arg. let z1 = f1 arg in 544 let z2 = f2 z1 in 545 z2) /\ 546 (!f1 f2. Par f1 f2 = \arg. let z1 = f1 arg in 547 let z2 = f2 arg in 548 (z1, z2)) /\ 549 (!f1 f2 f3. Ite f1 f2 f3 = \arg. 550 let (z1 = f1 arg) in 551 (if z1 then 552 let z2 = f2 arg in z2 553 else 554 let z3 = f3 arg in z3))``, 555 SIMP_TAC std_ss [Seq_def, Par_def, Ite_def, LET_THM]) 556 557val LET_PAIR = prove (`` 558 !f y. (let (x = (y:('a # 'b))) in f x) = 559 let x1 = FST y in 560 let x2 = SND y in 561 f (x1,x2)``, 562 563 Cases_on `y` THEN 564 SIMP_TAC std_ss [LET_THM]); 565 566val LET_LET = prove (`` 567 !f1 f2 z. (let (x = let y = z in f1 y) in f2 x) = 568 let y = z in 569 let x = f1 y in 570 f2 x``, 571 572 SIMP_TAC std_ss [LET_THM]) 573 574 575(* 576fun old_ANFof (args,thm) = 577 let 578 val thm1 = Q.AP_TERM `CPS` thm 579 val thm2 = REWRITE_RULE [CPS_SEQ_INTRO, CPS_PAR_INTRO,(* CPS_REC_INTRO, *) 580 CPS_ITE_INTRO] thm1 581 val thm3 = CONV_RULE (DEPTH_CONV (REWR_CONV CPS_SEQ_def ORELSEC 582 REWR_CONV CPS_PAR_def ORELSEC 583 REWR_CONV CPS_ITE_def 584(* ORELSEC REWR_CONV CPS_REC_def *))) thm2 585 val thm4 = CONV_RULE (DEPTH_CONV (REWR_CONV UNCPS)) thm3 586 val thm5 = CONV_RULE (LAND_CONV (REWR_CONV CPS_def)) thm4 587 val thm6 = CONV_RULE (REPEATC (STRIP_QUANT_CONV (HO_REWR_CONV FUN_EQ_THM))) 588 thm5 589 val x = mk_var("x",fst (dom_rng (type_of (fst (dest_forall (concl thm6)))))) 590 val thm7 = ISPEC (mk_abs(x,x)) thm6 591 val thm8 = BETA_RULE thm7 592 val thm9 = BETA_RULE thm8 593 val thm10 = SIMP_RULE bool_ss [LET_ID] thm9 594 val thm11 = SIMP_RULE bool_ss [pairTheory.FORALL_PROD] thm10 595 val thm12 = PBETA_RULE thm11 596 val thm13 = SIMP_RULE bool_ss [pairTheory.LAMBDA_PROD] thm12 597 val thm14 = PURE_REWRITE_RULE [FST,SND] thm13 598 val thm15 = CONV_RULE (DEPTH_CONV ELIM_PAIR_LET_CONV) thm14 599 val thm16 = STD_BVARS "v" thm15 600 val thm17 = CONV_RULE (DEPTH_CONV VAR_LET_CONV) thm16 601in 602 thm17 603end 604 605*) 606 607(*val (args,thm) = (args,const_eq_comb) *) 608fun ANFof (args,thm) = 609 let val thm1 = CONV_RULE (REPEATC (STRIP_QUANT_CONV (HO_REWR_CONV FUN_EQ_THM))) 610 thm 611 val thm2 = SIMP_RULE bool_ss [pairTheory.FORALL_PROD] thm1 612 val thm3 = SIMP_RULE std_ss [CPS_REWRITES, LET_LET] thm2 613 val thm4 = PBETA_RULE thm3 614 val thm5 = SIMP_RULE std_ss [LET_PAIR] thm4 615 val thm6 = CONV_RULE (DEPTH_CONV LET_UNCURRY_CONV) thm5 616 val thm7 = STD_BVARS "v" thm6 617 val thm8 = CONV_RULE (DEPTH_CONV VAR_LET_CONV) thm7 618 val thm9 = STD_BVARS "v" thm8 619 in thm8 620 end; 621 622 623(*---------------------------------------------------------------------------*) 624(* Given an environment and a possibly (tail) recursive definition, convert *) 625(* to combinator form, then to A-Normal form and add the result to the *) 626(* environment. *) 627(*---------------------------------------------------------------------------*) 628fun toANF env def = 629 let val (is_recursive,func,args,const_eq_comb) = toComb def 630 val anf = STD_BVARS "v" (ANFof (args,const_eq_comb)) 631(* val old_anf = STD_BVARS "v" (old_ANFof (args,const_eq_comb))*) 632 in 633 (func,(is_recursive,def,anf,const_eq_comb))::env 634 end; 635 636 637end 638 639