1 | include "joint/Joint.ma". |
---|
2 | include "joint/blocks.ma". |
---|
3 | include "utilities/hide.ma". |
---|
4 | include "utilities/deqsets.ma". |
---|
5 | |
---|
6 | (* general type of functions generating fresh things *) |
---|
7 | definition freshT ≝ λpars : params.λg.state_monad (joint_internal_function pars g). |
---|
8 | |
---|
9 | include alias "basics/lists/list.ma". |
---|
10 | let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ) |
---|
11 | on n : |
---|
12 | freshT pars globals (Σl : list A. |l| = n) ≝ |
---|
13 | match n return λx.freshT … (Σl.|l| = x) with |
---|
14 | [ O ⇒ return «[ ], ?» |
---|
15 | | S n' ⇒ |
---|
16 | ! regs' ← repeat_fresh … fresh n'; |
---|
17 | ! reg ← fresh ; |
---|
18 | return «reg::regs',?» |
---|
19 | ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed. |
---|
20 | |
---|
21 | definition fresh_label: |
---|
22 | ∀g_pars,globals.freshT globals g_pars label ≝ |
---|
23 | λg_pars,globals,def. |
---|
24 | let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in |
---|
25 | 〈set_luniverse … def luniverse, r〉. |
---|
26 | |
---|
27 | (* insert into a graph a block of instructions *) |
---|
28 | let rec adds_graph_list |
---|
29 | (g_pars: graph_params) |
---|
30 | (globals: list ident) |
---|
31 | (insts: list (joint_seq g_pars globals)) |
---|
32 | (src : label) on insts : state_monad (joint_internal_function g_pars globals) label ≝ |
---|
33 | match insts with |
---|
34 | [ nil ⇒ return src |
---|
35 | | cons instr others ⇒ |
---|
36 | ! mid ← fresh_label … ; |
---|
37 | ! def ← state_get … ; |
---|
38 | !_ state_set … (add_graph … src (sequential … instr mid) def) ; |
---|
39 | adds_graph_list g_pars globals others mid |
---|
40 | ]. |
---|
41 | |
---|
42 | definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with |
---|
43 | [ inl _ ⇒ true |
---|
44 | | inr _ ⇒ false |
---|
45 | ]. |
---|
46 | definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with |
---|
47 | [ inl _ ⇒ true |
---|
48 | | inr _ ⇒ false |
---|
49 | ]. |
---|
50 | |
---|
51 | definition adds_graph : |
---|
52 | ∀g_pars : graph_params. |
---|
53 | ∀globals: list ident. |
---|
54 | ∀b : seq_block g_pars globals (joint_step g_pars globals) + |
---|
55 | seq_block g_pars globals (joint_fin_step g_pars). |
---|
56 | label → if is_inl … b then label else unit → |
---|
57 | joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝ |
---|
58 | λg_pars,globals,insts,src. |
---|
59 | match insts return λx.if is_inl … x then ? else ? → ? → ? with |
---|
60 | [ inl b ⇒ λdst,def. |
---|
61 | let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in |
---|
62 | add_graph … mid (sequential … (\snd b) dst) def |
---|
63 | | inr b ⇒ λdst,def. |
---|
64 | let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in |
---|
65 | add_graph … mid (final … (\snd b)) def |
---|
66 | ]. |
---|
67 | |
---|
68 | (* ignoring register allocation for now *) |
---|
69 | |
---|
70 | definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝ |
---|
71 | λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def). |
---|
72 | |
---|
73 | lemma present_to_memb : ∀tag,A,l,m.present tag A m l → bool_to_Prop (l∈m). |
---|
74 | #tag #A * #l * #m whd in ⊢ (%→?%); |
---|
75 | elim (lookup tag ???) |
---|
76 | [ * #ABS elim (ABS ?) % |
---|
77 | | #a #_ % |
---|
78 | ] qed. |
---|
79 | |
---|
80 | lemma memb_to_present : ∀tag,A,l,m.l∈m → present tag A m l. |
---|
81 | #tag #A * #l * #m whd in ⊢ (?%→%); |
---|
82 | elim (lookup tag ???) |
---|
83 | [ * | #a * % #ABS destruct(ABS) ] qed. |
---|
84 | |
---|
85 | (* |
---|
86 | lemma All_fresh_not_memb : ∀tag,u,l,id,u'. |
---|
87 | All (identifier tag) (λid'.¬fresh_for_univ tag id' u) l → |
---|
88 | 〈id, u'〉 = fresh tag u → |
---|
89 | ¬id ∈ l. |
---|
90 | #tag #u #l elim l [2: #hd #tl #IH] #id #u' * |
---|
91 | [ #hd_fresh #tl_fresh #EQfresh |
---|
92 | whd in ⊢ (?(?%)); |
---|
93 | change with (eq_identifier ???) in match (?==?); |
---|
94 | >eq_identifier_sym |
---|
95 | >(eq_identifier_false … (fresh_distinct … hd_fresh EQfresh)) |
---|
96 | normalize nodelta @(IH … tl_fresh EQfresh) |
---|
97 | | #_ % |
---|
98 | ] |
---|
99 | qed. |
---|
100 | *) |
---|
101 | |
---|
102 | lemma fresh_was_fresh : ∀tag,id,id',u,u'. |
---|
103 | 〈id,u'〉 = fresh tag u → |
---|
104 | fresh_for_univ tag id' u' → |
---|
105 | id' ≠ id → |
---|
106 | fresh_for_univ tag id' u. |
---|
107 | #tag * #id * #id' * #u * #u' |
---|
108 | normalize #EQfresh destruct |
---|
109 | #H #NEQ |
---|
110 | elim (le_to_or_lt_eq … H) |
---|
111 | [ (* not recompiling... /2 by monotonic_pred/ *) /2/ ] |
---|
112 | #H >(succ_injective … H) in NEQ; |
---|
113 | * #G elim (G (refl …)) |
---|
114 | qed. |
---|
115 | |
---|
116 | (* use Russell? *) |
---|
117 | axiom adds_graph_list_ok : |
---|
118 | ∀g_pars,globals,b,src,def. |
---|
119 | fresh_for_univ … src (joint_if_luniverse … def) → |
---|
120 | luniverse_ok ?? def → |
---|
121 | let 〈def', dst〉 ≝ adds_graph_list g_pars globals b src def in |
---|
122 | luniverse_ok ?? def' ∧ |
---|
123 | ∃l.bool_to_Prop (uniqueb … l) ∧ |
---|
124 | All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧ |
---|
125 | fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ |
---|
126 | src ~❨b,l❩~> dst in joint_if_code … def'. |
---|
127 | (* |
---|
128 | #p #g #l elim l -l |
---|
129 | [ #src #def #_ #Hdef whd |
---|
130 | %{Hdef} %{[ ]} %%% ] |
---|
131 | #hd #tl #IH #src #def #src_fresh #Hdef |
---|
132 | whd in match (adds_graph_list ?????); |
---|
133 | whd in match (fresh_label ???); |
---|
134 | @(pair_elim … (fresh ??)) normalize nodelta |
---|
135 | #mid #luniverse' #EQfresh |
---|
136 | whd in ⊢ (match % with [ _ ⇒ ?]); |
---|
137 | letin def' ≝ (add_graph p g src (sequential … hd mid) (set_luniverse … def luniverse')) |
---|
138 | cut (joint_if_code p g (set_luniverse p g def luniverse') = joint_if_code … def) |
---|
139 | [ % ] #EQ_aux |
---|
140 | lapply (IH mid def' ??) |
---|
141 | [ #l whd in match def'; #Hpres |
---|
142 | lapply (present_to_memb … Hpres) -Hpres |
---|
143 | >mem_set_add @eq_identifier_elim |
---|
144 | [ #EQ destruct(EQ) * |
---|
145 | | #NEQ change with (? ∈ joint_if_code p ??) in ⊢ (?%→?); >EQ_aux |
---|
146 | #l_in |
---|
147 | ] |
---|
148 | @(fresh_remains_fresh … (sym_eq … EQfresh)) |
---|
149 | [2: @Hdef @memb_to_present ] assumption |
---|
150 | | whd in match def'; |
---|
151 | cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 |
---|
152 | whd in match (set_luniverse ????); |
---|
153 | @(fresh_is_fresh … (sym_eq … EQfresh)) |
---|
154 | ] |
---|
155 | elim (adds_graph_list ?????) #def'' #mid' normalize nodelta |
---|
156 | * #Hdef'' * #l ** #Hl1 #Hl2 #Hl3 %{Hdef''} %{(mid::l)} |
---|
157 | % [ % ] |
---|
158 | [ whd in ⊢ (?%); |
---|
159 | cut (Not (bool_to_Prop (mid∈l))) |
---|
160 | [ % #H elim (All_memb … Hl2 H) |
---|
161 | whd in match (joint_if_luniverse ???); |
---|
162 | #G #_ @(absurd ?? G) |
---|
163 | @ (fresh_is_fresh … (sym_eq … EQfresh)) |
---|
164 | | #H >H assumption |
---|
165 | ] |
---|
166 | | % |
---|
167 | [ % |
---|
168 | [ |
---|
169 | normalize #H10 #H11 |
---|
170 | |
---|
171 | >(All_fresh_not_memb … (sym_eq … EQfresh)) |
---|
172 | [ assumption ] |
---|
173 | @(All_mp … Hl2) #lbl * |
---|
174 | cases def in EQfresh; #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 |
---|
175 | normalize #EQfresh #H #lbl_not_mid |
---|
176 | lapply(fresh_remains_fresh … H (sym_eq … EQfresh)) |
---|
177 | |
---|
178 | elim (true_or_false_Prop (mid∈l)) #mid_l >mid_l |
---|
179 | [ normalize |
---|
180 | *) |
---|
181 | |
---|
182 | (* preserves first statement if a cost label (should be an invariant) *) |
---|
183 | definition insert_prologue ≝ |
---|
184 | λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals). |
---|
185 | λdef : joint_internal_function g_pars globals. |
---|
186 | let entry ≝ joint_if_entry … def in |
---|
187 | match stmt_at … entry |
---|
188 | return λx.match x with [None ⇒ false | Some _ ⇒ true] → ? |
---|
189 | with |
---|
190 | [ Some s ⇒ λ_. |
---|
191 | match s with |
---|
192 | [ sequential s' next ⇒ |
---|
193 | match s' with |
---|
194 | [ step_seq s'' ⇒ |
---|
195 | match s'' with |
---|
196 | [ COST_LABEL _ ⇒ |
---|
197 | adds_graph ?? (inl … (s'' :: insts)) entry next def |
---|
198 | | _ ⇒ |
---|
199 | let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in |
---|
200 | add_graph … tmp s def' |
---|
201 | ] |
---|
202 | | _ ⇒ |
---|
203 | let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in |
---|
204 | add_graph … tmp s def' |
---|
205 | ] |
---|
206 | | _ ⇒ |
---|
207 | let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in |
---|
208 | add_graph … tmp s def' |
---|
209 | ] |
---|
210 | | None ⇒ Ⓧ |
---|
211 | ] (pi2 … entry). |
---|
212 | |
---|
213 | definition insert_epilogue ≝ |
---|
214 | λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals). |
---|
215 | λdef : joint_internal_function g_pars globals. |
---|
216 | let exit ≝ joint_if_exit … def in |
---|
217 | match stmt_at … exit |
---|
218 | return λx.match x with [None ⇒ false | Some _ ⇒ true] → ? |
---|
219 | with |
---|
220 | [ Some s ⇒ λ_. |
---|
221 | let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in |
---|
222 | let def'' ≝ add_graph … tmp s def' in |
---|
223 | set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp |
---|
224 | | None ⇒ Ⓧ |
---|
225 | ] (pi2 … exit). |
---|
226 | whd in match def''; >graph_code_has_point // |
---|
227 | qed. |
---|
228 | |
---|
229 | definition b_adds_graph : |
---|
230 | ∀g_pars: graph_params. |
---|
231 | ∀globals: list ident. |
---|
232 | (* fresh register creation *) |
---|
233 | freshT g_pars globals (localsT … g_pars) → |
---|
234 | ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) + |
---|
235 | bind_seq_block g_pars globals (joint_fin_step g_pars). |
---|
236 | label → if is_inl … b then label else unit → |
---|
237 | joint_internal_function g_pars globals→ |
---|
238 | joint_internal_function g_pars globals ≝ |
---|
239 | λg_pars,globals,fresh_r,insts,src. |
---|
240 | match insts return λx.if is_inl … x then ? else ? → ? → ? with |
---|
241 | [ inl b ⇒ λdst,def. |
---|
242 | let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in |
---|
243 | adds_graph … (inl … stmts) src dst def |
---|
244 | | inr b ⇒ λdst,def. |
---|
245 | let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in |
---|
246 | adds_graph … (inr … stmts) src dst def |
---|
247 | ]. |
---|
248 | |
---|
249 | |
---|
250 | |
---|
251 | (* translation with inline fresh register allocation *) |
---|
252 | definition b_graph_translate : |
---|
253 | ∀src_g_pars,dst_g_pars : graph_params. |
---|
254 | ∀globals: list ident. |
---|
255 | (* fresh register creation *) |
---|
256 | freshT dst_g_pars globals (localsT dst_g_pars) → |
---|
257 | (* initialized function definition with empty graph *) |
---|
258 | joint_internal_function dst_g_pars globals → |
---|
259 | (* functions dictating the translation *) |
---|
260 | (label → joint_step src_g_pars globals → |
---|
261 | bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) → |
---|
262 | (label → joint_fin_step src_g_pars → |
---|
263 | bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) → |
---|
264 | (* source function *) |
---|
265 | joint_internal_function src_g_pars globals → |
---|
266 | (* destination function *) |
---|
267 | joint_internal_function dst_g_pars globals ≝ |
---|
268 | λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def. |
---|
269 | let f : label → joint_statement (src_g_pars : params) globals → |
---|
270 | joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ |
---|
271 | λlbl,stmt,def. |
---|
272 | match stmt with |
---|
273 | [ sequential inst next ⇒ |
---|
274 | b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def |
---|
275 | | final inst ⇒ |
---|
276 | b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def |
---|
277 | | FCOND abs _ _ _ ⇒ Ⓧabs |
---|
278 | ] in |
---|
279 | foldi … f (joint_if_code … def) empty. |
---|
280 | |
---|
281 | (* translation without register allocation *) |
---|
282 | definition graph_translate : |
---|
283 | ∀src_g_pars,dst_g_pars : graph_params. |
---|
284 | ∀globals: list ident. |
---|
285 | (* initialized function definition with empty graph *) |
---|
286 | joint_internal_function dst_g_pars globals → |
---|
287 | (* functions dictating the translation *) |
---|
288 | (label → joint_step src_g_pars globals → |
---|
289 | seq_block dst_g_pars globals (joint_step dst_g_pars globals)) → |
---|
290 | (label → joint_fin_step src_g_pars → |
---|
291 | seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) → |
---|
292 | (* source function *) |
---|
293 | joint_internal_function src_g_pars globals → |
---|
294 | (* destination function *) |
---|
295 | joint_internal_function dst_g_pars globals ≝ |
---|
296 | λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def. |
---|
297 | let f : label → joint_statement (src_g_pars : params) globals → |
---|
298 | joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ |
---|
299 | λlbl,stmt,def. |
---|
300 | match stmt with |
---|
301 | [ sequential inst next ⇒ |
---|
302 | adds_graph … (inl … (trans_step lbl inst)) lbl next def |
---|
303 | | final inst ⇒ |
---|
304 | adds_graph … (inr … (trans_fin_step lbl inst)) lbl it def |
---|
305 | | FCOND abs _ _ _ ⇒ Ⓧabs |
---|
306 | ] in |
---|
307 | foldi … f (joint_if_code … def) empty. |
---|
308 | |
---|
309 | definition init_graph_if ≝ |
---|
310 | λg_pars : graph_params.λglobals. |
---|
311 | λluniverse,runiverse,ret,params,locals,stack_size,entry,exit. |
---|
312 | let graph ≝ add ? ? (empty_map ? (joint_statement ??)) entry (GOTO … exit) in |
---|
313 | let graph ≝ add ? ? graph exit (RETURN …) in |
---|
314 | mk_joint_internal_function g_pars globals |
---|
315 | luniverse runiverse ret params locals stack_size |
---|
316 | graph entry exit. |
---|
317 | >graph_code_has_point @map_mem_prop |
---|
318 | [@graph_add_lookup] @graph_add |
---|
319 | qed. |
---|
320 | |
---|
321 | |
---|
322 | (* |
---|
323 | let rec add_translates |
---|
324 | (pars1: params1) (globals: list ident) |
---|
325 | (translate_list: list ?) (start_lbl: label) (dest_lbl: label) |
---|
326 | (def: joint_internal_function … (graph_params pars1 globals)) |
---|
327 | on translate_list ≝ |
---|
328 | match translate_list with |
---|
329 | [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def |
---|
330 | | cons trans translate_list ⇒ |
---|
331 | match translate_list with |
---|
332 | [ nil ⇒ trans start_lbl dest_lbl def |
---|
333 | | _ ⇒ |
---|
334 | let 〈tmp_lbl, def〉 ≝ fresh_label … def in |
---|
335 | let def ≝ trans start_lbl tmp_lbl def in |
---|
336 | add_translates pars1 globals translate_list tmp_lbl dest_lbl def]]. |
---|
337 | |
---|
338 | definition adds_graph ≝ |
---|
339 | λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals). |
---|
340 | add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list). |
---|
341 | *) |
---|