1 | include "joint/Joint_paolo.ma". |
---|
2 | include "joint/blocks.ma". |
---|
3 | include "utilities/hide.ma". |
---|
4 | |
---|
5 | (* general type of functions generating fresh things *) |
---|
6 | definition freshT ≝ λpars : params.λg.state_monad (joint_internal_function pars g). |
---|
7 | |
---|
8 | include alias "basics/lists/list.ma". |
---|
9 | let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ) |
---|
10 | on n : |
---|
11 | freshT pars globals (Σl : list A. |l| = n) ≝ |
---|
12 | match n return λx.freshT … (Σl.|l| = x) with |
---|
13 | [ O ⇒ return «[ ], ?» |
---|
14 | | S n' ⇒ |
---|
15 | ! regs' ← repeat_fresh … fresh n'; |
---|
16 | ! reg ← fresh ; |
---|
17 | return «reg::regs',?» |
---|
18 | ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed. |
---|
19 | |
---|
20 | definition fresh_label: |
---|
21 | ∀g_pars,globals.freshT globals g_pars label ≝ |
---|
22 | λg_pars,globals,def. |
---|
23 | let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in |
---|
24 | 〈set_luniverse … def luniverse, r〉. |
---|
25 | |
---|
26 | (* insert into a graph a block of instructions *) |
---|
27 | let rec adds_graph_list |
---|
28 | (g_pars: graph_params) |
---|
29 | (globals: list ident) |
---|
30 | (insts: list (joint_seq g_pars globals)) |
---|
31 | (src : label) on insts : state_monad (joint_internal_function g_pars globals) label ≝ |
---|
32 | match insts with |
---|
33 | [ nil ⇒ return src |
---|
34 | | cons instr others ⇒ |
---|
35 | ! mid ← fresh_label … ; |
---|
36 | ! def ← state_get … ; |
---|
37 | !_ state_set … (add_graph … src (sequential … instr mid) def) ; |
---|
38 | adds_graph_list g_pars globals others mid |
---|
39 | ]. |
---|
40 | |
---|
41 | definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with |
---|
42 | [ inl _ ⇒ true |
---|
43 | | inr _ ⇒ false |
---|
44 | ]. |
---|
45 | definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with |
---|
46 | [ inl _ ⇒ true |
---|
47 | | inr _ ⇒ false |
---|
48 | ]. |
---|
49 | |
---|
50 | definition adds_graph : |
---|
51 | ∀g_pars : graph_params. |
---|
52 | ∀globals: list ident. |
---|
53 | ∀b : seq_block g_pars globals (joint_step g_pars globals) + |
---|
54 | seq_block g_pars globals (joint_fin_step g_pars). |
---|
55 | label → if is_inl … b then label else unit → |
---|
56 | joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝ |
---|
57 | λg_pars,globals,insts,src. |
---|
58 | match insts return λx.if is_inl … x then ? else ? → ? → ? with |
---|
59 | [ inl b ⇒ λdst,def. |
---|
60 | let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in |
---|
61 | add_graph … mid (sequential … (\snd b) dst) def |
---|
62 | | inr b ⇒ λdst,def. |
---|
63 | let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in |
---|
64 | add_graph … mid (final … (\snd b)) def |
---|
65 | ]. |
---|
66 | |
---|
67 | (* preserves first statement if a cost label (should be an invariant) *) |
---|
68 | definition insert_prologue ≝ |
---|
69 | λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals). |
---|
70 | λdef : joint_internal_function g_pars globals. |
---|
71 | let entry ≝ joint_if_entry … def in |
---|
72 | match stmt_at … entry |
---|
73 | return λx.match x with [None ⇒ false | Some _ ⇒ true] → ? |
---|
74 | with |
---|
75 | [ Some s ⇒ λ_. |
---|
76 | match s with |
---|
77 | [ sequential s' next ⇒ |
---|
78 | match s' with |
---|
79 | [ step_seq s'' ⇒ |
---|
80 | match s'' with |
---|
81 | [ COST_LABEL _ ⇒ |
---|
82 | adds_graph ?? (inl … (s'' :: insts)) entry next def |
---|
83 | | _ ⇒ |
---|
84 | let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in |
---|
85 | add_graph … tmp s def' |
---|
86 | ] |
---|
87 | | _ ⇒ |
---|
88 | let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in |
---|
89 | add_graph … tmp s def' |
---|
90 | ] |
---|
91 | | _ ⇒ |
---|
92 | let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in |
---|
93 | add_graph … tmp s def' |
---|
94 | ] |
---|
95 | | None ⇒ Ⓧ |
---|
96 | ] (pi2 … entry). |
---|
97 | |
---|
98 | definition insert_epilogue ≝ |
---|
99 | λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals). |
---|
100 | λdef : joint_internal_function g_pars globals. |
---|
101 | let exit ≝ joint_if_exit … def in |
---|
102 | match stmt_at … exit |
---|
103 | return λx.match x with [None ⇒ false | Some _ ⇒ true] → ? |
---|
104 | with |
---|
105 | [ Some s ⇒ λ_. |
---|
106 | let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in |
---|
107 | let def'' ≝ add_graph … tmp s def' in |
---|
108 | set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp |
---|
109 | | None ⇒ Ⓧ |
---|
110 | ] (pi2 … exit). |
---|
111 | whd in match def''; >graph_code_has_point // |
---|
112 | qed. |
---|
113 | |
---|
114 | definition b_adds_graph : |
---|
115 | ∀g_pars: graph_params. |
---|
116 | ∀globals: list ident. |
---|
117 | (* fresh register creation *) |
---|
118 | freshT g_pars globals (localsT … g_pars) → |
---|
119 | ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) + |
---|
120 | bind_seq_block g_pars globals (joint_fin_step g_pars). |
---|
121 | label → if is_inl … b then label else unit → |
---|
122 | joint_internal_function g_pars globals→ |
---|
123 | joint_internal_function g_pars globals ≝ |
---|
124 | λg_pars,globals,fresh_r,insts,src. |
---|
125 | match insts return λx.if is_inl … x then ? else ? → ? → ? with |
---|
126 | [ inl b ⇒ λdst,def. |
---|
127 | let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in |
---|
128 | adds_graph … (inl … stmts) src dst def |
---|
129 | | inr b ⇒ λdst,def. |
---|
130 | let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in |
---|
131 | adds_graph … (inr … stmts) src dst def |
---|
132 | ]. |
---|
133 | |
---|
134 | (* translation with inline fresh register allocation *) |
---|
135 | definition b_graph_translate : |
---|
136 | ∀src_g_pars,dst_g_pars : graph_params. |
---|
137 | ∀globals: list ident. |
---|
138 | (* fresh register creation *) |
---|
139 | freshT dst_g_pars globals (localsT dst_g_pars) → |
---|
140 | (* initialized function definition with empty graph *) |
---|
141 | joint_internal_function dst_g_pars globals → |
---|
142 | (* functions dictating the translation *) |
---|
143 | (label → joint_step src_g_pars globals → |
---|
144 | bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) → |
---|
145 | (label → joint_fin_step src_g_pars → |
---|
146 | bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) → |
---|
147 | (* source function *) |
---|
148 | joint_internal_function src_g_pars globals → |
---|
149 | (* destination function *) |
---|
150 | joint_internal_function dst_g_pars globals ≝ |
---|
151 | λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def. |
---|
152 | let f : label → joint_statement (src_g_pars : params) globals → |
---|
153 | joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ |
---|
154 | λlbl,stmt,def. |
---|
155 | match stmt with |
---|
156 | [ sequential inst next ⇒ |
---|
157 | b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def |
---|
158 | | final inst ⇒ |
---|
159 | b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def |
---|
160 | ] in |
---|
161 | foldi … f (joint_if_code … def) empty. |
---|
162 | |
---|
163 | (* translation without register allocation *) |
---|
164 | definition graph_translate : |
---|
165 | ∀src_g_pars,dst_g_pars : graph_params. |
---|
166 | ∀globals: list ident. |
---|
167 | (* initialized function definition with empty graph *) |
---|
168 | joint_internal_function dst_g_pars globals → |
---|
169 | (* functions dictating the translation *) |
---|
170 | (label → joint_step src_g_pars globals → |
---|
171 | seq_block dst_g_pars globals (joint_step dst_g_pars globals)) → |
---|
172 | (label → joint_fin_step src_g_pars → |
---|
173 | seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) → |
---|
174 | (* source function *) |
---|
175 | joint_internal_function src_g_pars globals → |
---|
176 | (* destination function *) |
---|
177 | joint_internal_function dst_g_pars globals ≝ |
---|
178 | λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def. |
---|
179 | let f : label → joint_statement (src_g_pars : params) globals → |
---|
180 | joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ |
---|
181 | λlbl,stmt,def. |
---|
182 | match stmt with |
---|
183 | [ sequential inst next ⇒ |
---|
184 | adds_graph … (inl … (trans_step lbl inst)) lbl next def |
---|
185 | | final inst ⇒ |
---|
186 | adds_graph … (inr … (trans_fin_step lbl inst)) lbl it def |
---|
187 | ] in |
---|
188 | foldi … f (joint_if_code … def) empty. |
---|
189 | |
---|
190 | (* |
---|
191 | let rec add_translates |
---|
192 | (pars1: params1) (globals: list ident) |
---|
193 | (translate_list: list ?) (start_lbl: label) (dest_lbl: label) |
---|
194 | (def: joint_internal_function … (graph_params pars1 globals)) |
---|
195 | on translate_list ≝ |
---|
196 | match translate_list with |
---|
197 | [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def |
---|
198 | | cons trans translate_list ⇒ |
---|
199 | match translate_list with |
---|
200 | [ nil ⇒ trans start_lbl dest_lbl def |
---|
201 | | _ ⇒ |
---|
202 | let 〈tmp_lbl, def〉 ≝ fresh_label … def in |
---|
203 | let def ≝ trans start_lbl tmp_lbl def in |
---|
204 | add_translates pars1 globals translate_list tmp_lbl dest_lbl def]]. |
---|
205 | |
---|
206 | definition adds_graph ≝ |
---|
207 | λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals). |
---|
208 | add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list). |
---|
209 | *) |
---|