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