1loadPath := HOLDIR^"/examples/dev/sw2/" :: !loadPath; 2app load ["regAlloc", "closure", "inline", "SALGen", "wordsLib"]; 3numLib.prefer_num(); 4quietdec :=true; 5open Normal inline closure regAlloc NormalTheory SALGen; 6quietdec := false; 7 8(* 9val normalize = Normal.normalize; 10val SSA_RULE = Normal.SSA_RULE; 11val expand_anonymous = inline.expand_anonymous; 12val expand_named = inline.expand_named; 13val optimize_norm = inline.optimize_norm; 14val close_one_by_one = closure.close_one_by_one; 15val close_all = closure.close_all; 16val closure_convert = closure.closure_convert; 17val regL = regAlloc.regL; 18val reg_alloc = regAlloc.reg_alloc; 19val certified_gen = SALGen.certified_gen; 20val fun_def = NormalTheory.fun_def; 21*) 22 23(*---------------------------------------------------------------------------*) 24(* Organize phases of compilation. *) 25(*---------------------------------------------------------------------------*) 26 27fun defname th = 28 fst(dest_const(fst(strip_comb(lhs(snd(strip_forall(concl th))))))); 29 30fun compenv comp = 31 let fun compile (env,[]) = PASS(rev env) 32 | compile (env,h::t) = 33 let val name = defname h 34 in 35 print ("Compiling "^name^" ... "); 36 case total comp (env,h) 37 of SOME def1 => (print "succeeded.\n"; compile(def1::env,t)) 38 | NONE => (print "failed.\n"; FAIL(env,h::t)) 39 end 40 in 41 compile 42 end; 43 44(*---------------------------------------------------------------------------*) 45(* Compile a list of definitions, accumulating the environment. *) 46(*---------------------------------------------------------------------------*) 47 48fun complist passes deflist = compenv passes ([],deflist); 49 50(*---------------------------------------------------------------------------*) 51(* Basic flattening via CPS and unique names *) 52(*---------------------------------------------------------------------------*) 53 54fun pass1 def = SSA_RULE (normalize def); 55 56(*---------------------------------------------------------------------------*) 57(* All previous, plus inlining and optimizations *) 58(*---------------------------------------------------------------------------*) 59 60fun pass2 (env,def) = 61 let val def1 = pass1 def 62 in 63 SSA_RULE (optimize_norm env def1) 64 end; 65 66(*---------------------------------------------------------------------------*) 67(* All previous, and closure conversion. *) 68(*---------------------------------------------------------------------------*) 69 70fun pass3 (env,def) = 71 let val def1 = pass2 (env,def) 72 in case total closure_convert def1 73 of SOME thm => SSA_RULE (optimize_norm env thm) 74 | NONE => def1 75 end; 76 77(*---------------------------------------------------------------------------*) 78(* All previous, and register allocation. *) 79(*---------------------------------------------------------------------------*) 80 81fun pass4 (env,def) = 82 let val def1 = pass3 (env,def) 83 in 84 reg_alloc def1 85 end; 86 87(*---------------------------------------------------------------------------*) 88(* Different pass4, in which some intermediate steps are skipped. *) 89(*---------------------------------------------------------------------------*) 90 91fun pass4a (env,def) = 92 let val def1 = pass1 def 93 val def2 = reg_alloc def1 94 in 95 def2 96 end; 97 98val compile1 = complist (fn (e,d) => pass1 d); 99val compile2 = complist pass2; 100val compile3 = complist pass3; 101val compile4 = complist pass4; 102val compile4a = complist pass4a; 103(* val compile5 = complist pass5; *) 104 105 106