1 | include "joint/Joint_paolo.ma". |
---|
2 | include "utilities/bindLists.ma". |
---|
3 | |
---|
4 | (* general type of functions generating fresh things *) |
---|
5 | (* type T is the syntactic type of the generated things *) |
---|
6 | (* (sig for RTLabs registers, unit in others ) *) |
---|
7 | definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function … g pars). |
---|
8 | |
---|
9 | definition rtl_ertl_fresh_reg: |
---|
10 | ∀inst_pars,funct_pars,globals. |
---|
11 | freshT globals (rtl_ertl_params inst_pars funct_pars) register ≝ |
---|
12 | λinst_pars,var_pars,globals,def. |
---|
13 | let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in |
---|
14 | 〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉. |
---|
15 | |
---|
16 | include alias "basics/lists/list.ma". |
---|
17 | let rec rtl_ertl_fresh_regs inst_pars funct_pars globals (n : ℕ) on n : |
---|
18 | freshT globals (rtl_ertl_params inst_pars funct_pars) |
---|
19 | (Σl : list register. |l| = n) ≝ |
---|
20 | let ret_type ≝ (Σl : list register. |l| = n) in |
---|
21 | match n return λx.x = n → freshT … ret_type with |
---|
22 | [ O ⇒ λeq'.return (mk_Sig … [ ] ?) |
---|
23 | | S n' ⇒ λeq'. |
---|
24 | ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n'; |
---|
25 | ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals; |
---|
26 | return (mk_Sig … (reg :: regs') ?) |
---|
27 | ](refl …). <eq' normalize [//] elim regs' #l #eql >eql // |
---|
28 | qed. |
---|
29 | |
---|
30 | definition fresh_label: |
---|
31 | ∀g_pars,globals.freshT globals g_pars label ≝ |
---|
32 | λg_pars,globals,def. |
---|
33 | let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in |
---|
34 | 〈set_luniverse … def luniverse, r〉. |
---|
35 | |
---|
36 | (* insert into a graph a block of instructions *) |
---|
37 | let rec adds_graph |
---|
38 | (g_pars: graph_params) |
---|
39 | (globals: list ident) |
---|
40 | (insts: list (joint_step g_pars globals)) |
---|
41 | (src : label) |
---|
42 | (dest : label) |
---|
43 | (def: joint_internal_function … g_pars) on insts ≝ |
---|
44 | match insts with |
---|
45 | [ nil ⇒ add_graph … src (GOTO … dest) def |
---|
46 | | cons instr others ⇒ |
---|
47 | match others with |
---|
48 | [ nil ⇒ (* only one instruction *) |
---|
49 | add_graph … src (sequential … instr dest) def |
---|
50 | | _ ⇒ (* need to generate label *) |
---|
51 | let 〈def, tmp_lbl〉 ≝ fresh_label … def in |
---|
52 | adds_graph g_pars globals others tmp_lbl dest |
---|
53 | (add_graph … src (sequential … instr tmp_lbl) def) |
---|
54 | ] |
---|
55 | ]. |
---|
56 | |
---|
57 | definition b_adds_graph : |
---|
58 | ∀g_pars: graph_params. |
---|
59 | ∀globals: list ident. |
---|
60 | (* fresh register creation *) |
---|
61 | freshT globals g_pars (localsT … g_pars) → |
---|
62 | ∀insts: bind_list (localsT … g_pars) (joint_step g_pars globals). |
---|
63 | ∀src : label. |
---|
64 | ∀dest : label. |
---|
65 | joint_internal_function globals g_pars → |
---|
66 | joint_internal_function globals g_pars ≝ |
---|
67 | λg_pars,globals,fresh_r,insts,src,dest,def. |
---|
68 | let 〈def', stmts〉 ≝ bcompile … fresh_r insts def in |
---|
69 | adds_graph … stmts src dest def'. |
---|
70 | |
---|
71 | (* translation with inline fresh register allocation *) |
---|
72 | definition b_graph_translate : |
---|
73 | ∀src_g_pars,dst_g_pars : graph_params. |
---|
74 | ∀globals: list ident. |
---|
75 | (* fresh register creation *) |
---|
76 | freshT globals dst_g_pars (localsT dst_g_pars) → |
---|
77 | (* function dictating the translation *) |
---|
78 | (label → joint_step src_g_pars globals → |
---|
79 | bind_list (localsT dst_g_pars) (joint_step dst_g_pars globals) |
---|
80 | (* this can be added to allow redirections: × label *)) → |
---|
81 | (label → ext_fin_stmt src_g_pars → |
---|
82 | bind_new (localsT dst_g_pars) |
---|
83 | ((list (joint_step dst_g_pars globals)) |
---|
84 | × |
---|
85 | (joint_statement dst_g_pars globals))) → |
---|
86 | (* initialized function definition with empty graph *) |
---|
87 | joint_internal_function globals dst_g_pars → |
---|
88 | (* source function *) |
---|
89 | joint_internal_function globals src_g_pars → |
---|
90 | (* destination function *) |
---|
91 | joint_internal_function globals dst_g_pars ≝ |
---|
92 | λsrc_g_pars,dst_g_pars,globals,fresh_reg,trans,trans',empty,def. |
---|
93 | let f : label → joint_statement (src_g_pars : params) globals → |
---|
94 | joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝ |
---|
95 | λlbl,stmt,def. |
---|
96 | match stmt with |
---|
97 | [ sequential inst next ⇒ b_adds_graph … fresh_reg (trans lbl inst) lbl next def |
---|
98 | | GOTO next ⇒ add_graph … lbl (GOTO … next) def |
---|
99 | | RETURN ⇒ add_graph … lbl (RETURN …) def |
---|
100 | | extension_fin c ⇒ |
---|
101 | let 〈def', p〉 ≝ bcompile … fresh_reg (trans' lbl c) def in |
---|
102 | let 〈insts, fin〉 ≝ p in |
---|
103 | let 〈def'', tmp_lbl〉 ≝ fresh_label … def' in |
---|
104 | adds_graph … insts lbl tmp_lbl (add_graph … tmp_lbl fin def) |
---|
105 | ] in |
---|
106 | foldi … f (joint_if_code … def) empty. |
---|
107 | |
---|
108 | (* translation without register allocation *) |
---|
109 | definition graph_translate : |
---|
110 | ∀src_g_pars,dst_g_pars : graph_params. |
---|
111 | ∀globals: list ident. |
---|
112 | (* function dictating the translation *) |
---|
113 | (label → joint_step src_g_pars globals → |
---|
114 | list (joint_step dst_g_pars globals)) → |
---|
115 | (label → ext_fin_stmt src_g_pars → |
---|
116 | (list (joint_step dst_g_pars globals)) |
---|
117 | × |
---|
118 | (joint_statement dst_g_pars globals)) → |
---|
119 | (* initialized function definition with empty graph *) |
---|
120 | joint_internal_function … dst_g_pars → |
---|
121 | (* source function *) |
---|
122 | joint_internal_function … src_g_pars → |
---|
123 | (* destination function *) |
---|
124 | joint_internal_function … dst_g_pars ≝ |
---|
125 | λsrc_g_pars,dst_g_pars,globals,trans,trans',empty,def. |
---|
126 | let f : label → joint_statement (src_g_pars : params) globals → |
---|
127 | joint_internal_function … dst_g_pars → joint_internal_function … dst_g_pars ≝ |
---|
128 | λlbl,stmt,def. |
---|
129 | match stmt with |
---|
130 | [ sequential inst next ⇒ |
---|
131 | adds_graph dst_g_pars globals (trans lbl inst) lbl next def |
---|
132 | | GOTO next ⇒ add_graph … lbl (GOTO … next) def |
---|
133 | | RETURN ⇒ add_graph … lbl (RETURN …) def |
---|
134 | | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in |
---|
135 | let 〈def, tmp_lbl〉 ≝ fresh_label … def in |
---|
136 | adds_graph … l lbl tmp_lbl (add_graph … tmp_lbl fin def) |
---|
137 | ] in |
---|
138 | foldi ??? f (joint_if_code ?? def) empty. |
---|
139 | |
---|
140 | definition graph_to_lin_statement : |
---|
141 | ∀p : unserialized_params.∀globals. |
---|
142 | joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝ |
---|
143 | λp,globals,stmt.match stmt return λ_.joint_statement (mk_lin_params p) globals with |
---|
144 | [ sequential c _ ⇒ sequential … c it |
---|
145 | | GOTO l ⇒ GOTO … l |
---|
146 | | RETURN ⇒ RETURN … |
---|
147 | | extension_fin c ⇒ extension_fin … c |
---|
148 | ]. |
---|
149 | |
---|
150 | lemma graph_to_lin_labels : |
---|
151 | ∀p : unserialized_params.∀globals,s. |
---|
152 | stmt_labels … (graph_to_lin_statement p globals s) = |
---|
153 | stmt_explicit_labels … s. |
---|
154 | #p#globals * // |
---|
155 | qed. |
---|
156 | |
---|
157 | (* in order to make the coercion from lists to sets to work, one needs these hints *) |
---|
158 | unification hint 0 ≔ ; |
---|
159 | X ≟ identifier LabelTag |
---|
160 | ⊢ |
---|
161 | list label ≡ list X. |
---|
162 | |
---|
163 | unification hint 0 ≔ ; |
---|
164 | X ≟ identifier RegisterTag |
---|
165 | ⊢ |
---|
166 | list register ≡ list X. |
---|
167 | |
---|
168 | |
---|
169 | definition hide_prf : ∀P : Prop.P → P ≝ λP,prf.prf. |
---|
170 | definition hide_Prop : Prop → Prop ≝ λP.P. |
---|
171 | |
---|
172 | interpretation "hide proof" 'hide p = (hide_prf ? p). |
---|
173 | interpretation "hide Prop" 'hide p = (hide_Prop p). |
---|
174 | |
---|
175 | (* discard all elements failing test, return first element succeeding it *) |
---|
176 | (* and the rest of the list, if any. *) |
---|
177 | let rec chop A (test : A → bool) (l : list A) on l : option (A × (list A)) ≝ |
---|
178 | match l with |
---|
179 | [ nil ⇒ None ? |
---|
180 | | cons x l' ⇒ if test x then return 〈x, l'〉 else chop A test l' |
---|
181 | ]. |
---|
182 | |
---|
183 | lemma chop_hit : ∀A,f,l,pr. chop A f l = Some ? pr → |
---|
184 | let x ≝ \fst pr in |
---|
185 | let post ≝ \snd pr in |
---|
186 | ∃pre.All ? (λx.Not (bool_to_Prop (f x))) pre ∧ l = pre @ x :: post ∧ bool_to_Prop (f x). |
---|
187 | #A#f#l elim l |
---|
188 | [ normalize * #x #post #EQ destruct |
---|
189 | | #y #l' #Hi * #x #post |
---|
190 | normalize elim (true_or_false_Prop (f y)) #fy >fy normalize |
---|
191 | #EQ |
---|
192 | [ destruct >fy %{[ ]} /3 by refl, conj, I/ |
---|
193 | | elim (Hi … EQ) #pre ** #prefalse #chopd #fx |
---|
194 | %{(y :: pre)} %[%[%{fy prefalse}| >chopd %]|@fx] |
---|
195 | ] |
---|
196 | ] |
---|
197 | qed. |
---|
198 | |
---|
199 | lemma chop_miss : ∀A,f,l. chop A f l = None ? → All A (λx.Not (bool_to_Prop (f x))) l. |
---|
200 | #A#f#l elim l |
---|
201 | [ normalize #_ % |
---|
202 | | #y #l' #Hi normalize |
---|
203 | elim (true_or_false_Prop (f y)) #fy >fy normalize |
---|
204 | #EQ |
---|
205 | [ destruct |
---|
206 | | /3 by conj, nmk/ |
---|
207 | ] |
---|
208 | ] |
---|
209 | qed. |
---|
210 | |
---|
211 | unification hint 0 ≔ p, globals; |
---|
212 | lp ≟ lin_params_to_params p, |
---|
213 | sp ≟ stmt_pars lp, |
---|
214 | js ≟ joint_statement sp globals, |
---|
215 | lo ≟ labelled_obj LabelTag js |
---|
216 | (*----------------------------*)⊢ |
---|
217 | list lo ≡ codeT lp globals. |
---|
218 | |
---|
219 | definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals. |
---|
220 | λentry : label. |
---|
221 | (Σ〈visited' : identifier_map LabelTag ℕ, |
---|
222 | required' : identifier_set LabelTag, |
---|
223 | generated' : codeT (mk_lin_params p) globals〉.'hide ( |
---|
224 | And (And (And (lookup ?? visited' entry = Some ? 0) (required' ⊆ visited')) |
---|
225 | (code_forall_labels … (λl.bool_to_Prop (l∈required')) generated')) |
---|
226 | (∀l,n.lookup ?? visited' l = Some ? n → |
---|
227 | And (code_has_label … (rev ? generated') l) |
---|
228 | (∃s.And (And |
---|
229 | (lookup … g l = Some ? s) |
---|
230 | (nth_opt … n (rev … generated') = Some ? 〈Some ? l, graph_to_lin_statement … s〉)) |
---|
231 | (opt_All ? |
---|
232 | (λnext.Or (lookup … visited' next = Some ? (S n)) |
---|
233 | (nth_opt … (S n) (rev … generated') = Some ? 〈None ?, GOTO … next〉)) |
---|
234 | (stmt_implicit_label … s)))))). |
---|
235 | |
---|
236 | unification hint 0 ≔ tag ⊢ identifier_set tag ≡ identifier_map tag unit. |
---|
237 | |
---|
238 | let rec graph_visit |
---|
239 | (p : unserialized_params) |
---|
240 | (globals: list ident) |
---|
241 | (g : codeT (mk_graph_params p) globals) |
---|
242 | (* = graph (joint_statement (mk_graph_params p) globals *) |
---|
243 | (required: identifier_set LabelTag) |
---|
244 | (visited: identifier_map LabelTag ℕ) (* the reversed index of labels in the new code *) |
---|
245 | (generated: codeT (mk_lin_params p) globals) |
---|
246 | (* ≝ list ((option label)×(joint_statement (mk_lin_params p) globals)) *) |
---|
247 | (visiting: list label) |
---|
248 | (gen_length : ℕ) |
---|
249 | (n: nat) |
---|
250 | (entry : label) |
---|
251 | (g_prf : code_closed … g) |
---|
252 | (required_prf1 : ∀i.i∈required → Or (In ? visiting i) (bool_to_Prop (i ∈ visited))) |
---|
253 | (required_prf2 : code_forall_labels … (λl.bool_to_Prop (l ∈ required)) generated) |
---|
254 | (generated_prf1 : ∀l,n.lookup … visited l = Some ? n → hide_Prop ( |
---|
255 | And (code_has_label … (rev ? generated) l) |
---|
256 | (∃s.And (And |
---|
257 | (lookup … g l = Some ? s) |
---|
258 | (nth_opt ? n (rev … generated) = Some ? 〈Some ? l, graph_to_lin_statement … s〉)) |
---|
259 | (opt_All ? (λnext.match lookup … visited next with |
---|
260 | [ Some n' ⇒ Or (n' = S n) (nth_opt ? (S n) (rev ? generated) = Some ? 〈None ?, GOTO … next〉) |
---|
261 | | None ⇒ And (nth_opt ? 0 visiting = Some ? next) (S n = gen_length) ]) (stmt_implicit_label … s))))) |
---|
262 | (generated_prf2 : ∀l.lookup … visited l = None ? → does_not_occur … l (rev ? generated)) |
---|
263 | (visiting_prf : All … (λl.lookup … g l ≠ None ?) visiting) |
---|
264 | (gen_length_prf : gen_length = length ? generated) |
---|
265 | (entry_prf : Or (And (And (visiting = [entry]) (gen_length = 0)) (Not (bool_to_Prop (entry∈visited)))) |
---|
266 | (lookup … visited entry = Some ? 0)) |
---|
267 | (n_prf : le (id_map_size … g) (plus n (id_map_size … visited))) |
---|
268 | on n |
---|
269 | : graph_visit_ret_type … g entry ≝ |
---|
270 | match chop ? (λx.¬x∈visited) visiting |
---|
271 | return λx.chop ? (λx.¬x∈visited) visiting = x → graph_visit_ret_type … g entry with |
---|
272 | [ None ⇒ λeq_chop. |
---|
273 | let H ≝ chop_miss … eq_chop in |
---|
274 | mk_Sig … 〈visited, required, generated〉 ? |
---|
275 | | Some pr ⇒ λeq_chop. |
---|
276 | let vis_hd ≝ \fst pr in |
---|
277 | let vis_tl ≝ \snd pr in |
---|
278 | let H ≝ chop_hit ???? eq_chop in |
---|
279 | match n return λx.x = n → graph_visit_ret_type … g entry with |
---|
280 | [ O ⇒ λeq_n.⊥ |
---|
281 | | S n' ⇒ λeq_n. |
---|
282 | (* add the label to the visited ones *) |
---|
283 | let visited' ≝ add … visited vis_hd gen_length in |
---|
284 | (* take l's statement *) |
---|
285 | let statement ≝ opt_safe … (lookup ?? g vis_hd) (hide_prf ? ?) in |
---|
286 | (* translate it to its linear version *) |
---|
287 | let translated_statement ≝ graph_to_lin_statement p globals statement in |
---|
288 | (* add the translated statement to the code (which will be reversed later) *) |
---|
289 | let generated' ≝ 〈Some … vis_hd, translated_statement〉 :: generated in |
---|
290 | let required' ≝ stmt_explicit_labels … statement ∪ required in |
---|
291 | (* put successors in the visiting worklist *) |
---|
292 | let visiting' ≝ stmt_labels … statement @ vis_tl in |
---|
293 | (* finally, check the implicit successor *) |
---|
294 | (* if it has been already visited, we need to add a GOTO *) |
---|
295 | let add_req_gen ≝ match stmt_implicit_label … statement with |
---|
296 | [ Some next ⇒ |
---|
297 | if next ∈ visited' then 〈1, {(next)}, [〈None label, GOTO … next〉]〉 else 〈0, ∅, [ ]〉 |
---|
298 | | None ⇒ 〈0, ∅, [ ]〉 |
---|
299 | ] in |
---|
300 | graph_visit ??? |
---|
301 | (\snd (\fst add_req_gen) ∪ required') |
---|
302 | visited' |
---|
303 | (\snd add_req_gen @ generated') |
---|
304 | visiting' |
---|
305 | (\fst (\fst add_req_gen) + S(gen_length)) |
---|
306 | n' entry g_prf ???????? |
---|
307 | ] (refl …) |
---|
308 | ] (refl …). |
---|
309 | whd |
---|
310 | [ (* base case, visiting is all visited *) |
---|
311 | %[ |
---|
312 | %[ |
---|
313 | %[ |
---|
314 | elim entry_prf |
---|
315 | [ ** #eq_visiting #gen_length_O #entry_vis >eq_visiting in H; * >entry_vis |
---|
316 | * #ABS elim (ABS I) |
---|
317 | | // |
---|
318 | ] |
---|
319 | | #l #l_req |
---|
320 | elim (required_prf1 … l_req) #G |
---|
321 | [ lapply (All_In … H G) #H >(notb_false ? H) % |
---|
322 | | assumption |
---|
323 | ] |
---|
324 | ] |
---|
325 | | assumption |
---|
326 | ] |
---|
327 | | #l #n #H elim (generated_prf1 … H) |
---|
328 | #H1 * #s ** #H2 #H3 #H4 |
---|
329 | % [assumption] %{s} % |
---|
330 | [% assumption |
---|
331 | | @(opt_All_mp … H4) -l #l |
---|
332 | lapply (in_map_domain … visited l) |
---|
333 | elim (true_or_false (l∈visited)) #l_vis >l_vis |
---|
334 | normalize nodelta [ * #n' ] #EQlookup >EQlookup |
---|
335 | normalize nodelta * |
---|
336 | [ #EQn' % >EQn' % |
---|
337 | | #H %2{H} |
---|
338 | | #H' lapply (All_nth … H … H') >l_vis * #ABS elim (ABS I) |
---|
339 | ] |
---|
340 | ] |
---|
341 | ] |
---|
342 | |*: (* unpack H in all other cases *) elim H #pre ** #H1 #H2 #H3 ] |
---|
343 | (* first, close goals where add_gen_req plays no role *) |
---|
344 | [10: (* vis_hd is in g *) @(All_split … visiting_prf … H2) |
---|
345 | |1: (* n = 0 absrud *) |
---|
346 | @(absurd … n_prf) |
---|
347 | @lt_to_not_le |
---|
348 | <eq_n |
---|
349 | lapply (add_size … visited vis_hd 0 (* dummy value *)) |
---|
350 | >(notb_true … H3) |
---|
351 | whd in match (if ? then ? else ?); |
---|
352 | whd in match (? + ?); |
---|
353 | whd in match (lt ? ?); |
---|
354 | #EQ <EQ @subset_card @add_subset |
---|
355 | [ @(All_split ? (λx.bool_to_Prop (x∈g)) ????? H2) @(All_mp … visiting_prf) |
---|
356 | #a elim g #gm whd in ⊢ (?→?%); #H >(opt_to_opt_safe … H) % |
---|
357 | | #l #H lapply (mem_map_domain … H) -H #H lapply(opt_to_opt_safe … H) |
---|
358 | generalize in match (opt_safe ???); #n #l_is_n |
---|
359 | elim (generated_prf1 … l_is_n) #_ * #s ** #s_in_g #_ #_ lapply s_in_g -s_in_g |
---|
360 | elim g #mg whd in ⊢ (?→?%); #H >H whd % |
---|
361 | ] |
---|
362 | |6: |
---|
363 | @All_append |
---|
364 | [ @(g_prf … vis_hd) <opt_to_opt_safe % |
---|
365 | | >H2 in visiting_prf; |
---|
366 | #H' lapply (All_append_r … H') -H' * #_ // |
---|
367 | ] |
---|
368 | |8: |
---|
369 | %2 elim entry_prf |
---|
370 | [ ** >H2 cases pre |
---|
371 | [2: #x' #pre' #ABS normalize in ABS; destruct(ABS) |
---|
372 | cases pre' in e0; [2: #x'' #pre''] #ABS' normalize in ABS'; destruct(ABS') |
---|
373 | |1: #EQ normalize in EQ; destruct(EQ) #eq_gen_length #_ |
---|
374 | >lookup_add_hit >eq_gen_length % |
---|
375 | ] |
---|
376 | | #lookup_entry cut (entry ≠ vis_hd) |
---|
377 | [ % whd in match vis_hd; #entry_vis_hd <entry_vis_hd in H3; #entry_vis |
---|
378 | lapply (in_map_domain … visited entry) >(notb_true … entry_vis) |
---|
379 | normalize nodelta >lookup_entry #ABS destruct(ABS)] |
---|
380 | #entry_not_vis_hd >(lookup_add_miss ?????? entry_not_vis_hd) assumption |
---|
381 | ] |
---|
382 | |9: |
---|
383 | >commutative_plus |
---|
384 | >add_size >(notb_true … H3) normalize nodelta |
---|
385 | whd in match (? + ?); |
---|
386 | >commutative_plus |
---|
387 | change with (? ≤ S(?) + ?) |
---|
388 | >eq_n assumption |
---|
389 | |*: (* where add_gen_req does matter, expand the three possible cases *) |
---|
390 | lapply (refl … add_req_gen) |
---|
391 | whd in ⊢ (???%→?); |
---|
392 | lapply (refl … (stmt_implicit_label … statement)) |
---|
393 | (* BUG *) |
---|
394 | [ generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%); |
---|
395 | | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%); |
---|
396 | | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%); |
---|
397 | | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%); |
---|
398 | | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%); |
---|
399 | ] |
---|
400 | *[2,4,6,8,10: #next] |
---|
401 | #EQimpl |
---|
402 | whd in ⊢ (???%→?); |
---|
403 | [1,2,3,4,5: elim (true_or_false_Prop … (next∈visited')) #next_vis >next_vis |
---|
404 | whd in ⊢ (???%→?);] |
---|
405 | #EQ_req_gen >EQ_req_gen |
---|
406 | (* these are the cases, reordering them *) |
---|
407 | [1,2,11: | 3,4,12: | 5,6,13: | 7,8,14: |9,10,15: ] |
---|
408 | [1,2,3: #i >mem_set_union |
---|
409 | [ #H elim (orb_Prop_true … H) -H |
---|
410 | [ #H >(mem_set_singl_to_eq … H) %2{next_vis}] |
---|
411 | |*: >mem_set_empty whd in match (false ∨ ?); |
---|
412 | ] |
---|
413 | >mem_set_union |
---|
414 | #H elim(orb_Prop_true … H) -H |
---|
415 | [1,3,5: (* i is an explicit successor *) |
---|
416 | #i_succ |
---|
417 | (* if it's visited it's ok *) |
---|
418 | elim(true_or_false_Prop (i ∈visited')) #i_vis >i_vis |
---|
419 | [1,3,5: %2 % |
---|
420 | |*: % |
---|
421 | @Exists_append_l |
---|
422 | whd in match (stmt_labels ???); |
---|
423 | @Exists_append_r |
---|
424 | @mem_list_as_set |
---|
425 | @i_succ |
---|
426 | ] |
---|
427 | |2,4,6: (* i was already required *) |
---|
428 | #i_req |
---|
429 | elim (required_prf1 … i_req) |
---|
430 | [1,3,5: >H2 #H elim (Exists_append … H) -H |
---|
431 | [1,3,5: (* i in preamble → i∈visited *) |
---|
432 | #i_pre %2 >mem_set_add @orb_Prop_r |
---|
433 | lapply (All_In … H1 i_pre) |
---|
434 | #H >(notb_false … H) % |
---|
435 | |*: * |
---|
436 | [1,3,5: (* i is vis_hd *) |
---|
437 | #eq_i >eq_i %2 @mem_set_add_id |
---|
438 | |*: (* i in vis_tl → i∈visiting' *) |
---|
439 | #i_post % @Exists_append_r assumption |
---|
440 | ] |
---|
441 | ] |
---|
442 | |*: #i_vis %2 >mem_set_add @orb_Prop_r assumption |
---|
443 | ] |
---|
444 | ] |
---|
445 | |4,5,6: |
---|
446 | [% [ whd % [ >mem_set_union >mem_set_add_id % | %]]] |
---|
447 | whd in match (? @ ?); % |
---|
448 | [1,3,5: |
---|
449 | whd |
---|
450 | >graph_to_lin_labels |
---|
451 | change with (All ?? (stmt_explicit_labels ?? statement)) |
---|
452 | whd in match required'; |
---|
453 | generalize in match (stmt_explicit_labels … statement); |
---|
454 | #l @list_as_set_All |
---|
455 | #i >mem_set_union >mem_set_union |
---|
456 | #i_l @orb_Prop_r @orb_Prop_l @i_l |
---|
457 | |*: @(All_mp … required_prf2) |
---|
458 | * #l_opt #s @All_mp |
---|
459 | #l #l_req >mem_set_union @orb_Prop_r |
---|
460 | >mem_set_union @orb_Prop_r @l_req |
---|
461 | ] |
---|
462 | |7,8,9: |
---|
463 | #i whd in match visited'; |
---|
464 | @(eq_identifier_elim … i vis_hd) |
---|
465 | [1,3,5: #EQi >EQi #pos |
---|
466 | >lookup_add_hit #EQpos cut (gen_length = pos) |
---|
467 | [1,3,5: (* BUG: -graph_visit *) -visited destruct(EQpos) %] |
---|
468 | -EQpos #EQpos <EQpos -pos |
---|
469 | % |
---|
470 | [1,3,5: whd in match (rev ? ?); |
---|
471 | >rev_append_def |
---|
472 | whd |
---|
473 | [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]); |
---|
474 | <associative_append >occurs_exactly_once_None] |
---|
475 | >occurs_exactly_once_Some_eq >eq_identifier_refl |
---|
476 | normalize nodelta |
---|
477 | @generated_prf2 |
---|
478 | lapply (in_map_domain … visited vis_hd) |
---|
479 | >(notb_true … H3) normalize nodelta // |
---|
480 | |*: %{statement} |
---|
481 | % |
---|
482 | [1,3,5: % |
---|
483 | [1,3,5: |
---|
484 | change with (? = Some ? (opt_safe ???)) |
---|
485 | @opt_safe_elim #s // |
---|
486 | |*: whd in match (rev ? ?); |
---|
487 | >rev_append_def |
---|
488 | [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]); |
---|
489 | <associative_append @nth_opt_append_hit_l ] |
---|
490 | >nth_opt_append_r |
---|
491 | >rev_length |
---|
492 | <gen_length_prf |
---|
493 | [1,3,5: <minus_n_n] % |
---|
494 | ] |
---|
495 | |*: >EQimpl whd [3: %] |
---|
496 | >mem_set_add in next_vis; |
---|
497 | @eq_identifier_elim |
---|
498 | [1,3: #EQnext >EQnext * [2: #ABS elim(ABS I)] |
---|
499 | >lookup_add_hit |
---|
500 | |*: #NEQ >(lookup_add_miss … visited … NEQ) |
---|
501 | whd in match (false ∨ ?); |
---|
502 | #next_vis lapply(in_map_domain … visited next) >next_vis |
---|
503 | whd in ⊢ (% → ?); [ * #s ] |
---|
504 | #EQlookup >EQlookup |
---|
505 | ] whd |
---|
506 | [1,2: %2 |
---|
507 | >rev_append >nth_opt_append_r |
---|
508 | >rev_length whd in match generated'; |
---|
509 | whd in match (|? :: ?|); <gen_length_prf |
---|
510 | [1,3: <minus_n_n ] % |
---|
511 | |*: % [2: %] @nth_opt_append_hit_l whd in match (stmt_labels … statement); |
---|
512 | >EQimpl % |
---|
513 | ] |
---|
514 | ] |
---|
515 | ] |
---|
516 | |*: |
---|
517 | #NEQ #n_i >(lookup_add_miss … visited … NEQ) |
---|
518 | #Hlookup elim (generated_prf1 … Hlookup) |
---|
519 | #G1 * #s ** #G2 #G3 #G4 |
---|
520 | % |
---|
521 | [1,3,5: whd in match (rev ??); |
---|
522 | >rev_append_def whd |
---|
523 | [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]); |
---|
524 | <associative_append >occurs_exactly_once_None] |
---|
525 | >occurs_exactly_once_Some_eq |
---|
526 | >eq_identifier_false |
---|
527 | [2,4,6: % #ABS >ABS in NEQ; * #ABS' @ABS' %] |
---|
528 | normalize nodelta |
---|
529 | assumption |
---|
530 | |*: %{s} |
---|
531 | % |
---|
532 | [1,3,5: % |
---|
533 | [1,3,5: assumption |
---|
534 | |*: whd in match (rev ??); >rev_append_def |
---|
535 | [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]); |
---|
536 | <associative_append @nth_opt_append_hit_l ] |
---|
537 | @nth_opt_append_hit_l assumption |
---|
538 | ] |
---|
539 | |*: @(opt_All_mp … G4) |
---|
540 | #x |
---|
541 | @(eq_identifier_elim … x vis_hd) #Heq |
---|
542 | [1,3,5: >Heq |
---|
543 | lapply (in_map_domain … visited vis_hd) |
---|
544 | >(notb_true … H3) |
---|
545 | normalize nodelta #EQlookup >EQlookup normalize nodelta |
---|
546 | * #nth_opt_visiting #gen_length_eq |
---|
547 | >lookup_add_hit normalize nodelta % |
---|
548 | >gen_length_eq % |
---|
549 | |*: >(lookup_add_miss ?????? Heq) |
---|
550 | lapply (in_map_domain … visited x) |
---|
551 | elim (true_or_false_Prop (x∈visited)) #x_vis >x_vis normalize nodelta |
---|
552 | [1,3,5: * #n'] #EQlookupx >EQlookupx normalize nodelta * |
---|
553 | [1,3,5: #G %{G} |
---|
554 | |2,4,6: #G %2 whd in match (rev ??); >rev_append_def |
---|
555 | [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]); |
---|
556 | <associative_append @nth_opt_append_hit_l ] |
---|
557 | @nth_opt_append_hit_l assumption |
---|
558 | |*: #G elim(absurd ?? Heq) |
---|
559 | (* BUG (but useless): -required -g -generated *) |
---|
560 | >H2 in G; #G |
---|
561 | lapply (refl … (nth_opt ? 0 pre)) |
---|
562 | (* BUG *) |
---|
563 | [generalize in ⊢ (???%→?); |
---|
564 | |generalize in ⊢ (???%→?); |
---|
565 | |generalize in ⊢ (???%→?); |
---|
566 | ] * |
---|
567 | [1,3,5: #G' >(nth_opt_append_miss_l … G') in G; |
---|
568 | change with (Some ? vis_hd = ? → ?) |
---|
569 | #EQvis_hd' destruct(EQvis_hd') % |
---|
570 | |*: #lbl'' #G' >(nth_opt_append_hit_l ? pre ??? G') in G; |
---|
571 | #EQlbl'' destruct(EQlbl'') lapply (All_nth … H1 … G') |
---|
572 | >x_vis * #ABS elim (ABS I) |
---|
573 | ] |
---|
574 | ] |
---|
575 | ] |
---|
576 | ] |
---|
577 | ] |
---|
578 | ] |
---|
579 | |10,11,12: |
---|
580 | #i whd in match visited'; |
---|
581 | lapply (in_map_domain … visited' i) |
---|
582 | >mem_set_add |
---|
583 | elim (true_or_false_Prop (eq_identifier … vis_hd i)) #i_vis_hd |
---|
584 | >eq_identifier_sym >i_vis_hd |
---|
585 | [2,4,6: elim(true_or_false (i∈visited)) #i_vis >i_vis] |
---|
586 | [1,3,5,7,8,9: change with ((∃_.?) → ?); * #n #EQlook >EQlook #ABS destruct(ABS)] |
---|
587 | #_ #EQlookup >lookup_add_miss in EQlookup; |
---|
588 | [2,4,6: % #ABS >ABS in i_vis_hd; >eq_identifier_refl *] |
---|
589 | #EQlookup |
---|
590 | [1,2,3: @EQlookup %] |
---|
591 | whd in match (rev ??); >rev_append_def |
---|
592 | [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]); |
---|
593 | <associative_append >does_not_occur_None] |
---|
594 | >(does_not_occur_Some ?????? (i_vis_hd)) |
---|
595 | @generated_prf2 assumption |
---|
596 | |13,14,15: |
---|
597 | whd in match generated'; normalize <gen_length_prf % |
---|
598 | ] |
---|
599 | ] |
---|
600 | qed. |
---|
601 | |
---|
602 | (* CSC: The branch compression (aka tunneling) optimization is not implemented |
---|
603 | in Matita *) |
---|
604 | definition branch_compress |
---|
605 | ≝ λp: graph_params.λglobals.λg:codeT p globals. |
---|
606 | λentry : Σl.code_has_label … g l.g. |
---|
607 | |
---|
608 | lemma branch_compress_closed : ∀p,globals,g,l.code_closed ?? g → |
---|
609 | code_closed … (branch_compress p globals g l). |
---|
610 | #p#globals#g#l#H @H qed. |
---|
611 | |
---|
612 | lemma branch_compress_has_entry : ∀p,globals,g,l. |
---|
613 | code_has_label … (branch_compress p globals g l) l. |
---|
614 | #p#globals#g*#l#l_prf @l_prf qed. |
---|
615 | |
---|
616 | definition filter_labels ≝ λtag,A.λtest : identifier tag → bool.λc : list (labelled_obj tag A). |
---|
617 | map ?? |
---|
618 | (λs. let 〈l_opt,x〉 ≝ s in |
---|
619 | 〈! l ← l_opt ; if test l then return l else None ?, x〉) c. |
---|
620 | |
---|
621 | lemma does_not_occur_filter_labels : |
---|
622 | ∀tag,A,test,id,c. |
---|
623 | does_not_occur ?? id (filter_labels tag A test c) = |
---|
624 | (does_not_occur ?? id c ∨ ¬ test id). |
---|
625 | #tag #A #test #id #c elim c |
---|
626 | [ // |
---|
627 | | ** [2: #lbl] #s #tl #IH |
---|
628 | whd in match (filter_labels ????); normalize nodelta |
---|
629 | whd in match (does_not_occur ????) in ⊢ (??%%); |
---|
630 | [2: @IH] |
---|
631 | normalize in match (! l ← ? ; ?); >IH |
---|
632 | @(eq_identifier_elim ?? lbl id) #Heq [<Heq] |
---|
633 | elim (test lbl) normalize nodelta |
---|
634 | change with (eq_identifier ???) in match (instruction_matches_identifier ????); |
---|
635 | [1,2: >eq_identifier_refl [2: >commutative_orb] normalize % |
---|
636 | |*: >(eq_identifier_false ??? Heq) normalize nodelta % |
---|
637 | ] |
---|
638 | ] |
---|
639 | qed. |
---|
640 | |
---|
641 | lemma occurs_exactly_once_filter_labels : |
---|
642 | ∀tag,A,test,id,c. |
---|
643 | occurs_exactly_once ?? id (filter_labels tag A test c) = |
---|
644 | (occurs_exactly_once ?? id c ∧ test id). |
---|
645 | #tag #A #test #id #c elim c |
---|
646 | [ // |
---|
647 | | ** [2: #lbl] #s #tl #IH |
---|
648 | whd in match (filter_labels ????); normalize nodelta |
---|
649 | whd in match (occurs_exactly_once ????) in ⊢ (??%%); |
---|
650 | [2: @IH] |
---|
651 | normalize in match (! l ← ? ; ?); >IH |
---|
652 | >does_not_occur_filter_labels |
---|
653 | @(eq_identifier_elim ?? lbl id) #Heq [<Heq] |
---|
654 | elim (test lbl) normalize nodelta |
---|
655 | change with (eq_identifier ???) in match (instruction_matches_identifier ????); |
---|
656 | [1,2: >eq_identifier_refl >commutative_andb [ >(commutative_andb ? true) >commutative_orb | >(commutative_andb ? false)] normalize % |
---|
657 | |*: >(eq_identifier_false ??? Heq) normalize nodelta % |
---|
658 | ] |
---|
659 | ] |
---|
660 | qed. |
---|
661 | |
---|
662 | lemma nth_opt_filter_labels : ∀tag,A,test,instrs,n. |
---|
663 | nth_opt ? n (filter_labels tag A test instrs) = |
---|
664 | ! 〈lopt, s〉 ← nth_opt ? n instrs ; |
---|
665 | return 〈 ! lbl ← lopt; if test lbl then return lbl else None ?, s〉. |
---|
666 | #tag #A #test #instrs elim instrs |
---|
667 | [ * [2: #n'] % |
---|
668 | | * #lopt #s #tl #IH * [2: #n'] |
---|
669 | whd in match (filter_labels ????); normalize nodelta |
---|
670 | whd in match (nth_opt ???) in ⊢ (??%%); [>IH] % |
---|
671 | ] |
---|
672 | qed. |
---|
673 | |
---|
674 | definition linearize_code: |
---|
675 | ∀p : unserialized_params.∀globals. |
---|
676 | ∀g : codeT (mk_graph_params p) globals.code_closed … g → |
---|
677 | ∀entry : (Σl. code_has_label … g l). |
---|
678 | (Σc : codeT (mk_lin_params p) globals. |
---|
679 | code_closed … c ∧ |
---|
680 | ∃ sigma : identifier_map LabelTag ℕ. |
---|
681 | lookup … sigma entry = Some ? 0 ∧ |
---|
682 | ∀l,n.lookup … sigma l = Some ? n → |
---|
683 | ∃s. lookup … g l = Some ? s ∧ |
---|
684 | opt_Exists ? |
---|
685 | (λls.let 〈lopt, ts〉 ≝ ls in |
---|
686 | opt_All ? (eq ? l) lopt ∧ |
---|
687 | ts = graph_to_lin_statement … s ∧ |
---|
688 | opt_All ? |
---|
689 | (λnext.Or (lookup … sigma next = Some ? (S n)) |
---|
690 | (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) |
---|
691 | (stmt_implicit_label … s)) (nth_opt … n c)) |
---|
692 | ≝ |
---|
693 | λp,globals,g,g_prf,entry_sig. |
---|
694 | let g ≝ branch_compress (mk_graph_params p) ? g entry_sig in |
---|
695 | let g_prf ≝ branch_compress_closed … g entry_sig g_prf in |
---|
696 | let entry_sig' ≝ mk_Sig ?? entry_sig (branch_compress_has_entry … g entry_sig) in |
---|
697 | match graph_visit p globals g ∅ (empty_map …) [ ] [entry_sig] 0 (|g|) |
---|
698 | (entry_sig) g_prf ???????? |
---|
699 | with |
---|
700 | [ mk_Sig triple H ⇒ |
---|
701 | let sigma ≝ \fst (\fst triple) in |
---|
702 | let required ≝ \snd (\fst triple) in |
---|
703 | let crev ≝ \snd triple in |
---|
704 | let lbld_code ≝ rev ? crev in |
---|
705 | mk_Sig ?? (filter_labels … (λl.l∈required) lbld_code) ? ]. |
---|
706 | [ (* done later *) |
---|
707 | | #i >mem_set_empty * |
---|
708 | | % |
---|
709 | |#l #n normalize in ⊢ (%→?); #ABS destruct(ABS) |
---|
710 | | #l #_ % |
---|
711 | | % [2: %] @(pi2 … entry_sig') |
---|
712 | | % |
---|
713 | | % % [% %] cases (pi1 … entry_sig) normalize #_ % // |
---|
714 | | >commutative_plus change with (? ≤ |g|) % |
---|
715 | ] |
---|
716 | lapply (refl … triple) |
---|
717 | generalize in match triple in ⊢ (???%→%); ** |
---|
718 | #visited #required #generated #EQtriple |
---|
719 | >EQtriple in H ⊢ %; normalize nodelta *** |
---|
720 | #entry_O #req_vis #labels_in_req #sigma_prop |
---|
721 | % >EQtriple |
---|
722 | [ (* code closed *) |
---|
723 | @All_map |
---|
724 | [2: @All_rev |
---|
725 | @(All_mp … labels_in_req) #ls #H @H |
---|
726 | |1: (* side-effect close *) |
---|
727 | |3: * #lopt #s @All_mp |
---|
728 | #lbl #lbl_req whd in match (code_has_label ????); |
---|
729 | >occurs_exactly_once_filter_labels |
---|
730 | @andb_Prop [2: assumption] |
---|
731 | lapply (in_map_domain … visited lbl) |
---|
732 | >(req_vis … lbl_req) * #n #eq_lookup |
---|
733 | elim (sigma_prop ?? eq_lookup) #H #_ @H |
---|
734 | ] |
---|
735 | ] |
---|
736 | %{visited} % [assumption] |
---|
737 | #lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup) |
---|
738 | #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in |
---|
739 | % [2: % [ assumption ] |] |
---|
740 | >nth_opt_filter_labels in ⊢ (???%); |
---|
741 | >nth_opt_is_stmt |
---|
742 | whd in match (! 〈lopt, s〉 ← Some ??; ?); |
---|
743 | whd |
---|
744 | whd in match (! lbl0 ← Some ??; ?); |
---|
745 | % [ % [ elim (lbl ∈ required) ] % ] |
---|
746 | whd |
---|
747 | lapply (refl … (stmt_implicit_label … stmt)) |
---|
748 | generalize in match (stmt_implicit_label … stmt) in ⊢ (???%→%); * [2: #next] |
---|
749 | #eq_impl_lbl normalize nodelta [2: %] |
---|
750 | >eq_impl_lbl in succ_is_in; whd in match (opt_All ???); * #H |
---|
751 | [ %{H} |
---|
752 | | %2 >nth_opt_filter_labels >H |
---|
753 | whd in match (! 〈lopt, s〉 ← ?; ?); |
---|
754 | whd in match (! lbl0 ← ?; ?); |
---|
755 | % |
---|
756 | ] |
---|
757 | qed. |
---|
758 | |
---|
759 | definition graph_linearize : |
---|
760 | ∀p : unserialized_params. |
---|
761 | ∀globals. ∀fin : joint_closed_internal_function globals (mk_graph_params p). |
---|
762 | Σfout : joint_closed_internal_function globals (mk_lin_params p). |
---|
763 | ∃sigma : identifier_map LabelTag ℕ. |
---|
764 | let g ≝ joint_if_code ?? (pi1 … fin) in |
---|
765 | let c ≝ joint_if_code ?? (pi1 … fout) in |
---|
766 | let entry ≝ joint_if_entry ?? (pi1 … fin) in |
---|
767 | lookup … sigma entry = Some ? 0 ∧ |
---|
768 | ∀l,n.lookup … sigma l = Some ? n → |
---|
769 | ∃s. lookup … g l = Some ? s ∧ |
---|
770 | opt_Exists ? |
---|
771 | (λls.let 〈lopt, ts〉 ≝ ls in |
---|
772 | opt_All ? (eq ? l) lopt ∧ |
---|
773 | ts = graph_to_lin_statement … s ∧ |
---|
774 | opt_All ? |
---|
775 | (λnext.Or (lookup … sigma next = Some ? (S n)) |
---|
776 | (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) |
---|
777 | (stmt_implicit_label … s)) (nth_opt … n c) ≝ |
---|
778 | λp,globals,f_sig. |
---|
779 | mk_Sig ?? (match f_sig with |
---|
780 | [ mk_Sig f f_prf ⇒ |
---|
781 | mk_joint_internal_function globals (mk_lin_params p) |
---|
782 | (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) |
---|
783 | (joint_if_result ?? f) (joint_if_params ?? f) (joint_if_locals ?? f) |
---|
784 | (joint_if_stacksize ?? f) |
---|
785 | (linearize_code p globals (joint_if_code … f) f_prf (joint_if_entry … f)) |
---|
786 | (mk_Sig ?? it I) (mk_Sig ?? it I) |
---|
787 | ]) ?. |
---|
788 | elim f_sig |
---|
789 | normalize nodelta #f_in #f_in_prf |
---|
790 | elim (linearize_code ?????) |
---|
791 | #f_out * #f_out_closed #H assumption |
---|
792 | qed. |
---|
793 | |
---|
794 | |
---|
795 | |
---|
796 | |
---|
797 | (* |
---|
798 | let rec add_translates |
---|
799 | (pars1: params1) (globals: list ident) |
---|
800 | (translate_list: list ?) (start_lbl: label) (dest_lbl: label) |
---|
801 | (def: joint_internal_function … (graph_params pars1 globals)) |
---|
802 | on translate_list ≝ |
---|
803 | match translate_list with |
---|
804 | [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def |
---|
805 | | cons trans translate_list ⇒ |
---|
806 | match translate_list with |
---|
807 | [ nil ⇒ trans start_lbl dest_lbl def |
---|
808 | | _ ⇒ |
---|
809 | let 〈tmp_lbl, def〉 ≝ fresh_label … def in |
---|
810 | let def ≝ trans start_lbl tmp_lbl def in |
---|
811 | add_translates pars1 globals translate_list tmp_lbl dest_lbl def]]. |
---|
812 | |
---|
813 | definition adds_graph ≝ |
---|
814 | λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals). |
---|
815 | add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list). |
---|
816 | *) |
---|