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