1 | include "joint/TranslateUtils.ma". |
---|
2 | include "utilities/hide.ma". |
---|
3 | |
---|
4 | definition graph_to_lin_statement : |
---|
5 | ∀p : unserialized_params.∀globals. |
---|
6 | joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝ |
---|
7 | λp,globals,stmt.match stmt return λ_.joint_statement (mk_lin_params ?) ? with |
---|
8 | [ sequential c _ ⇒ sequential … c it |
---|
9 | | final c ⇒ final … c |
---|
10 | ]. |
---|
11 | |
---|
12 | lemma graph_to_lin_labels : |
---|
13 | ∀p : unserialized_params.∀globals,s. |
---|
14 | stmt_labels … (graph_to_lin_statement p globals s) = |
---|
15 | stmt_explicit_labels … s. |
---|
16 | #p#globals * [//] * // |
---|
17 | qed. |
---|
18 | |
---|
19 | (* discard all elements passing test, return first element failing it *) |
---|
20 | (* and the rest of the list, if any. *) |
---|
21 | let rec chop A (test : A → bool) (l : list A) on l : option (A × (list A)) ≝ |
---|
22 | match l with |
---|
23 | [ nil ⇒ None ? |
---|
24 | | cons x l' ⇒ if test x then chop A test l' else return 〈x, l'〉 |
---|
25 | ]. |
---|
26 | |
---|
27 | lemma chop_ok : ∀A,f,l. |
---|
28 | match chop A f l with |
---|
29 | [ Some pr ⇒ |
---|
30 | let x ≝ \fst pr in |
---|
31 | let post ≝ \snd pr in |
---|
32 | ∃pre.All ? (λx.bool_to_Prop (f x)) pre ∧ |
---|
33 | l = pre @ x :: post ∧ ¬bool_to_Prop (f x) |
---|
34 | | None ⇒ All A (λx.bool_to_Prop (f x)) l |
---|
35 | ]. |
---|
36 | #A #f #l elim l |
---|
37 | [ % |
---|
38 | | #hd #tl #IH whd in match (chop ???); |
---|
39 | elim (true_or_false_Prop (f hd)) #H >H normalize nodelta |
---|
40 | [ lapply IH elim (chop ???) normalize nodelta |
---|
41 | [ #G %{H G} |
---|
42 | | #pr * #pre ** #H1 #H2 #H3 %{(hd :: pre)} %{H3} % |
---|
43 | [ %{H H1} |
---|
44 | | >H2 % |
---|
45 | ] |
---|
46 | ] |
---|
47 | | %{[ ]} %{H} %% |
---|
48 | ] |
---|
49 | ] |
---|
50 | qed. |
---|
51 | |
---|
52 | unification hint 0 ≔ p, globals; |
---|
53 | lp ≟ lin_params_to_params p, |
---|
54 | sp ≟ stmt_pars lp, |
---|
55 | js ≟ joint_statement sp globals, |
---|
56 | lo ≟ labelled_obj LabelTag js |
---|
57 | (*----------------------------*)⊢ |
---|
58 | list lo ≡ codeT lp globals. |
---|
59 | |
---|
60 | |
---|
61 | definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals. |
---|
62 | λentry : label. |
---|
63 | (Σ〈visited' : identifier_map LabelTag ℕ, |
---|
64 | required' : identifier_set LabelTag, |
---|
65 | generated' : codeT (mk_lin_params p) globals〉.'hide ( |
---|
66 | And (And (And (And |
---|
67 | (lookup ?? visited' entry = Some ? 0) |
---|
68 | (required' ⊆ visited')) |
---|
69 | (∃last.stmt_at … generated' 0 = Some ? (final … last))) |
---|
70 | (code_forall_labels … (λl.bool_to_Prop (l∈required')) (rev … generated'))) |
---|
71 | (∀l,n.lookup ?? visited' l = Some ? n → |
---|
72 | And (bool_to_Prop (code_has_label … (rev ? generated') l)) |
---|
73 | (∃s.And (And |
---|
74 | (lookup … g l = Some ? s) |
---|
75 | (nth_opt … n (rev … generated') = Some ? 〈Some ? l, graph_to_lin_statement … s〉)) |
---|
76 | (opt_All ? |
---|
77 | (λnext.Or (lookup … visited' next = Some ? (S n)) |
---|
78 | (nth_opt … (S n) (rev … generated') = Some ? 〈None ?, GOTO … next〉)) |
---|
79 | (stmt_implicit_label … s)))))). |
---|
80 | |
---|
81 | unification hint 0 ≔ tag ⊢ identifier_set tag ≡ identifier_map tag unit. |
---|
82 | |
---|
83 | include alias "common/Identifiers.ma". |
---|
84 | |
---|
85 | lemma lookup_safe_elim : ∀tag,A.∀P : A → Prop.∀m,i,prf. |
---|
86 | (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf). |
---|
87 | #tag #A #P #m #i #prf #H @H @lookup_eq_safe qed. |
---|
88 | |
---|
89 | let rec graph_visit |
---|
90 | (p : unserialized_params) |
---|
91 | (globals: list ident) |
---|
92 | (g : codeT (mk_graph_params p) globals) |
---|
93 | (* = graph (joint_statement (mk_graph_params p) globals *) |
---|
94 | (required: identifier_set LabelTag) |
---|
95 | (visited: identifier_map LabelTag ℕ) (* the reversed index of labels in the new code *) |
---|
96 | (generated: codeT (mk_lin_params p) globals) |
---|
97 | (* ≝ list ((option label)×(joint_statement (mk_lin_params p) globals)) *) |
---|
98 | (visiting: list label) |
---|
99 | (gen_length : ℕ) |
---|
100 | (n: nat) |
---|
101 | (entry : label) |
---|
102 | (g_prf : code_closed … g) |
---|
103 | (required_prf1 : ∀i.i∈required → Or (In ? visiting i) (bool_to_Prop (i∈visited))) |
---|
104 | (required_prf2 : code_forall_labels … (λl.bool_to_Prop (l ∈ required)) (rev … generated)) |
---|
105 | (generated_prf1 : ∀l,n.lookup … visited l = Some ? n → hide_Prop ( |
---|
106 | And (bool_to_Prop (code_has_label … (rev ? generated) l)) |
---|
107 | (∃s.And (And |
---|
108 | (lookup … g l = Some ? s) |
---|
109 | (nth_opt ? n (rev … generated) = Some ? 〈Some ? l, graph_to_lin_statement … s〉)) |
---|
110 | (opt_All ? (λnext.match lookup … visited next with |
---|
111 | [ Some n' ⇒ Or (n' = S n) (nth_opt ? (S n) (rev ? generated) = Some ? 〈None ?, GOTO … next〉) |
---|
112 | | None ⇒ And (nth_opt ? 0 visiting = Some ? next) (S n = gen_length) ]) (stmt_implicit_label … s))))) |
---|
113 | (generated_prf2 : ∀l.lookup … visited l = None ? → does_not_occur … l (rev ? generated)) |
---|
114 | (generated_prf3 : (∃last.stmt_at … generated 0 = Some ? (final … last)) ∨ |
---|
115 | (¬All ? (λx.bool_to_Prop (x∈visited)) visiting)) |
---|
116 | (visiting_prf : All … (λl.bool_to_Prop (l∈g)) visiting) |
---|
117 | (gen_length_prf : gen_length = length ? generated) |
---|
118 | (entry_prf : Or (And (And (visiting = [entry]) (gen_length = 0)) (Not (bool_to_Prop (entry∈visited)))) |
---|
119 | (lookup … visited entry = Some ? 0)) |
---|
120 | (n_prf : le (id_map_size … g) (plus n (id_map_size … visited))) |
---|
121 | on n |
---|
122 | : graph_visit_ret_type … g entry ≝ |
---|
123 | match chop ? (λx.x∈visited) visiting |
---|
124 | return λx.? → graph_visit_ret_type … g entry with |
---|
125 | [ None ⇒ λH. |
---|
126 | «〈visited, required, generated〉, ?» |
---|
127 | | Some pr ⇒ λH. |
---|
128 | let vis_hd ≝ \fst pr in |
---|
129 | let vis_tl ≝ \snd pr in |
---|
130 | match n return λx.? → graph_visit_ret_type … g entry with |
---|
131 | [ O ⇒ λn_prf'.⊥ |
---|
132 | | S n' ⇒ λn_prf'. |
---|
133 | (* add the label to the visited ones *) |
---|
134 | let visited' ≝ add … visited vis_hd gen_length in |
---|
135 | (* take l's statement *) |
---|
136 | let hd_vis_in_g ≝ (hide_prf ? ?) in |
---|
137 | let statement ≝ lookup_safe ?? g vis_hd hd_vis_in_g in |
---|
138 | (* translate it to its linear version *) |
---|
139 | let translated_statement ≝ graph_to_lin_statement p globals statement in |
---|
140 | (* add the translated statement to the code (which will be reversed later) *) |
---|
141 | let generated' ≝ 〈Some … vis_hd, translated_statement〉 :: generated in |
---|
142 | let required' ≝ union_set ??? (set_from_list … (stmt_explicit_labels … statement)) required in |
---|
143 | (* put successors in the visiting worklist *) |
---|
144 | let visiting' ≝ stmt_labels … statement @ vis_tl in |
---|
145 | (* finally, check the implicit successor *) |
---|
146 | (* if it has been already visited, we need to add a GOTO *) |
---|
147 | let add_req_gen ≝ |
---|
148 | match stmt_implicit_label … statement |
---|
149 | with |
---|
150 | [ Some next ⇒ |
---|
151 | if next ∈ visited' then |
---|
152 | 〈1, {(next)}, [〈None label, (GOTO … next : joint_statement ??)〉]〉 |
---|
153 | else 〈0, ∅, [ ]〉 |
---|
154 | | None ⇒ 〈0, ∅, [ ]〉 |
---|
155 | ] in |
---|
156 | (* prepare a common utility to deal with add_req_gen *) |
---|
157 | let add_req_gen_prf : |
---|
158 | ∀P : (ℕ × (identifier_set LabelTag) × (codeT (mk_lin_params p) globals)) → Prop. |
---|
159 | (opt_All ? (λnext.¬bool_to_Prop (next ∈ visited')) (stmt_implicit_label … statement) → |
---|
160 | P 〈0,∅,[ ]〉) → |
---|
161 | (∀next.stmt_implicit_label … statement = Some ? next → |
---|
162 | next ∈ visited' → |
---|
163 | P 〈1, {(next)}, [〈None ?, GOTO (mk_lin_params p) next〉]〉) → |
---|
164 | P add_req_gen ≝ hide_prf ?? in |
---|
165 | graph_visit ??? |
---|
166 | (union_set ??? (\snd (\fst add_req_gen)) required') |
---|
167 | visited' |
---|
168 | (\snd add_req_gen @ generated') |
---|
169 | visiting' |
---|
170 | (plus (\fst (\fst add_req_gen)) (S gen_length)) |
---|
171 | n' entry g_prf ????????? |
---|
172 | ] n_prf |
---|
173 | ] (chop_ok ? (λx.x∈visited) visiting). |
---|
174 | whd |
---|
175 | [ (* base case, visiting is all visited *) |
---|
176 | %[%[%[%]]] |
---|
177 | [ elim entry_prf |
---|
178 | [ ** #eq_visiting #gen_length_O #entry_vis >eq_visiting in H; * >entry_vis * |
---|
179 | | // |
---|
180 | ] |
---|
181 | | #l #l_req |
---|
182 | elim (required_prf1 … l_req) #G |
---|
183 | [ @(All_In … H G) |
---|
184 | | assumption |
---|
185 | ] |
---|
186 | | cases generated_prf3 [//] |
---|
187 | * #ABS @⊥ @ABS assumption |
---|
188 | | assumption |
---|
189 | | #l #n #H elim (generated_prf1 … H) |
---|
190 | #H1 * #s ** #H2 #H3 #H4 |
---|
191 | % [assumption] %{s} % |
---|
192 | [% assumption |
---|
193 | | @(opt_All_mp … H4) -l #l |
---|
194 | lapply (in_map_domain … visited l) |
---|
195 | elim (true_or_false_Prop (l∈visited)) #l_vis >l_vis |
---|
196 | normalize nodelta [ * #n' ] #EQlookup >EQlookup |
---|
197 | normalize nodelta * |
---|
198 | [ #EQn' % >EQn' % |
---|
199 | | #H %2{H} |
---|
200 | | #H' lapply (All_nth … H … H') >l_vis * |
---|
201 | ] |
---|
202 | ] |
---|
203 | ] |
---|
204 | (* first, close goals where add_gen_req plays no role *) |
---|
205 | |13: (* vis_hd is in g *) |
---|
206 | elim H #pre ** #_ #H2 #_ |
---|
207 | @(All_split … visiting_prf … H2) |
---|
208 | |2: (* n = 0 absrud *) |
---|
209 | elim H #pre ** #_ #H2 #H3 |
---|
210 | @(absurd … n_prf') |
---|
211 | @lt_to_not_le |
---|
212 | lapply (add_size … visited vis_hd 0 (* dummy value *)) |
---|
213 | >H3 normalize nodelta |
---|
214 | whd in match (lt ? ?); |
---|
215 | whd in match (1 + ?); |
---|
216 | #EQ <EQ @subset_card @add_subset |
---|
217 | [ @(All_split ? (λx.bool_to_Prop (x∈g)) ????? H2) @(All_mp … visiting_prf) |
---|
218 | #a elim g #gm whd in ⊢ (?→?%); #H >(lookup_eq_safe … H) % |
---|
219 | | #l #H |
---|
220 | elim (generated_prf1 … (lookup_eq_safe … H)) #_ * #s ** #s_in_g #_ #_ |
---|
221 | whd in ⊢ (?%); >s_in_g % |
---|
222 | ] |
---|
223 | |8: |
---|
224 | elim H #pre ** #_ #H2 #_ |
---|
225 | @All_append |
---|
226 | [ elim(g_prf … vis_hd statement ?) [2:@lookup_eq_safe] #G1 #G2 |
---|
227 | @(All_append … G1) |
---|
228 | whd in G2; lapply G2 elim statement normalize nodelta #s [2: #_ %] |
---|
229 | #l #G' %{G'} % |
---|
230 | | >H2 in visiting_prf; |
---|
231 | #H' lapply (All_append_r … H') -H' * #_ // |
---|
232 | ] |
---|
233 | |10: |
---|
234 | elim H #pre ** #_ #H2 #H3 -add_req_gen_prf |
---|
235 | %2 elim entry_prf |
---|
236 | [ ** >H2 cases pre |
---|
237 | [2: #x' #pre' #ABS normalize in ABS; destruct(ABS) |
---|
238 | cases pre' in e0; [2: #x'' #pre''] #ABS' normalize in ABS'; destruct(ABS') |
---|
239 | |1: #EQ normalize in EQ; destruct(EQ) |
---|
240 | #eq_gen_length #_ |
---|
241 | >lookup_add_hit >eq_gen_length % |
---|
242 | ] |
---|
243 | | #lookup_entry cut (entry ≠ vis_hd) |
---|
244 | [ % whd in match vis_hd; #entry_vis_hd <entry_vis_hd in H3; |
---|
245 | whd in ⊢ (?(?%)→?); >lookup_entry * #ABS @ABS % ] |
---|
246 | #entry_not_vis_hd >(lookup_add_miss ?????? entry_not_vis_hd) assumption |
---|
247 | ] |
---|
248 | |11: |
---|
249 | elim H #pre ** #_ #_ #H3 |
---|
250 | >commutative_plus |
---|
251 | >add_size >H3 normalize nodelta |
---|
252 | whd in match (1 + ?); |
---|
253 | >commutative_plus |
---|
254 | assumption |
---|
255 | |12: (* add_req_gen utility *) |
---|
256 | #P whd in match add_req_gen; |
---|
257 | elim (stmt_implicit_label ???) |
---|
258 | [ #H #_ @H % ] |
---|
259 | #next normalize nodelta elim (true_or_false_Prop (next ∈ visited')) #next_vis |
---|
260 | >next_vis normalize nodelta |
---|
261 | [ #_ #H @H [% | assumption] |
---|
262 | | #H #_ @H whd >next_vis % * |
---|
263 | ] |
---|
264 | | elim H #pre ** #H1 #H2 #_ |
---|
265 | #i >mem_set_union |
---|
266 | #H elim (orb_Prop_true … H) -H |
---|
267 | [ @add_req_gen_prf [ #_ >mem_set_empty * ] |
---|
268 | #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption |
---|
269 | | >mem_set_union |
---|
270 | #H elim (orb_Prop_true … H) -H |
---|
271 | [ #i_expl %1 @Exists_append_l @Exists_append_r |
---|
272 | @mem_list_as_set |
---|
273 | @i_expl |
---|
274 | | (* i was already required *) |
---|
275 | #i_req |
---|
276 | elim (required_prf1 … i_req) |
---|
277 | [ >H2 #H elim (Exists_append … H) -H |
---|
278 | [ (* i in preamble → i∈visited *) |
---|
279 | #i_pre %2 >mem_set_add @orb_Prop_r |
---|
280 | lapply (All_In … H1 i_pre) #H @H |
---|
281 | | * |
---|
282 | [ (* i is vis_hd *) |
---|
283 | #eq_i >eq_i %2 @mem_set_add_id |
---|
284 | | (* i in vis_tl → i∈visiting' *) |
---|
285 | #i_post % @Exists_append_r assumption |
---|
286 | ] |
---|
287 | ] |
---|
288 | | (* i in visited *) |
---|
289 | #i_vis %2 >mem_set_add @orb_Prop_r assumption |
---|
290 | ] |
---|
291 | ] |
---|
292 | ] |
---|
293 | |4,5,6: change with reverse in match rev; |
---|
294 | >reverse_append whd in match (reverse ??); >rev_append_def |
---|
295 | >associative_append |
---|
296 | [ #pt #s |
---|
297 | @(leb_elim (S pt) (|generated|)) #cmp |
---|
298 | whd in match (stmt_at ????); |
---|
299 | [ >nth_opt_append_l [2: >length_reverse assumption ] |
---|
300 | change with (stmt_at ???? = ? → ?) |
---|
301 | #EQ lapply(required_prf2 … EQ) @All_mp |
---|
302 | #l #l_req >mem_set_union @orb_Prop_r |
---|
303 | >mem_set_union @orb_Prop_r @l_req |
---|
304 | | >nth_opt_append_r [2: >length_reverse @not_lt_to_le assumption ] |
---|
305 | cases (pt - ?) |
---|
306 | [ whd in match (nth_opt ???); whd in ⊢ (??%?→?); |
---|
307 | #EQ destruct(EQ) whd |
---|
308 | >graph_to_lin_labels in ⊢ (???%); |
---|
309 | whd in match required'; |
---|
310 | generalize in match (stmt_explicit_labels … statement); |
---|
311 | #l @list_as_set_All |
---|
312 | #i >mem_set_union >mem_set_union |
---|
313 | #i_l @orb_Prop_r @orb_Prop_l @i_l |
---|
314 | | @add_req_gen_prf |
---|
315 | [ #_ | #next #_ #next_vis * |
---|
316 | [ whd in ⊢ (??%?→?); |
---|
317 | #EQ' destruct(EQ') whd %{I} >mem_set_union |
---|
318 | @orb_Prop_l @mem_set_add_id ]] |
---|
319 | #n whd in ⊢ (??%?→?); #ABS destruct(ABS) |
---|
320 | ] |
---|
321 | ] |
---|
322 | | elim H #pre ** #H1 #H2 #H3 |
---|
323 | #i whd in match visited'; |
---|
324 | @(eq_identifier_elim … i vis_hd) |
---|
325 | [ #EQi >EQi -i #pos |
---|
326 | >lookup_add_hit #EQpos (* too slow: destruct(EQpos) *) |
---|
327 | cut (gen_length = pos) |
---|
328 | [1,3,5: (* BUG: -graph_visit *) -visited destruct(EQpos) %] |
---|
329 | -EQpos #EQpos <EQpos -pos |
---|
330 | % |
---|
331 | [ >lin_code_has_label |
---|
332 | @add_req_gen_prf |
---|
333 | [ #_ |
---|
334 | | #next #_ #next_vis |
---|
335 | change with (? @ ([?] @ [?])) in match (? @ [? ; ?]); |
---|
336 | <associative_append >occurs_exactly_once_None |
---|
337 | ] |
---|
338 | >occurs_exactly_once_Some_eq >eq_identifier_refl |
---|
339 | normalize nodelta |
---|
340 | @generated_prf2 |
---|
341 | lapply (in_map_domain … visited vis_hd) |
---|
342 | >H3 normalize nodelta // |
---|
343 | | %{statement} |
---|
344 | % [ % ] |
---|
345 | [ @lookup_eq_safe |
---|
346 | | <associative_append @nth_opt_append_hit_l |
---|
347 | >nth_opt_append_r |
---|
348 | >rev_length |
---|
349 | <gen_length_prf |
---|
350 | [<minus_n_n] % |
---|
351 | | @add_req_gen_prf |
---|
352 | [ lapply (refl … (stmt_implicit_label ?? statement)) |
---|
353 | cases (stmt_implicit_label ???) in ⊢ (???%→%); |
---|
354 | [#_ #_ %] |
---|
355 | #next #K change with (¬bool_to_Prop (?∈?)→?) #next_vis |
---|
356 | | #next #K >K #next_vis |
---|
357 | ] whd |
---|
358 | >mem_set_add in next_vis; |
---|
359 | @eq_identifier_elim |
---|
360 | [1,3: #EQnext >EQnext * [#ABS elim(ABS I)] |
---|
361 | >lookup_add_hit |
---|
362 | |*: #NEQ >(lookup_add_miss … visited … NEQ) |
---|
363 | change with (?∈?) in match (false∨?); |
---|
364 | #next_vis lapply(in_map_domain … visited next) >next_vis |
---|
365 | whd in ⊢ (% → ?); [2: * #s ] |
---|
366 | #EQlookup >EQlookup |
---|
367 | ] whd |
---|
368 | [1,2: %2 <associative_append |
---|
369 | >nth_opt_append_r >append_length >rev_length >commutative_plus |
---|
370 | <gen_length_prf |
---|
371 | [1,3: <minus_n_n ] % |
---|
372 | | % [2: %] @nth_opt_append_hit_l whd in match (stmt_labels … statement); |
---|
373 | >K % |
---|
374 | ] |
---|
375 | ] |
---|
376 | ] |
---|
377 | | #NEQ #n_i >(lookup_add_miss … visited … NEQ) |
---|
378 | #Hlookup elim (generated_prf1 … Hlookup) |
---|
379 | #G1 * #s ** #G2 #G3 #G4 |
---|
380 | % |
---|
381 | [ >lin_code_has_label <associative_append |
---|
382 | >occurs_exactly_once_append |
---|
383 | @orb_Prop_l @andb_Prop |
---|
384 | [ >occurs_exactly_once_Some_eq |
---|
385 | >eq_identifier_false [2: % #ABS >ABS in NEQ; * #ABS' @ABS' % ] |
---|
386 | normalize nodelta >lin_code_has_label in G1; #K @K |
---|
387 | | @add_req_gen_prf |
---|
388 | [ #_ % | #next #_ #_ % ] |
---|
389 | ] |
---|
390 | | %{s} |
---|
391 | % [ % ] |
---|
392 | [ assumption |
---|
393 | | @nth_opt_append_hit_l assumption |
---|
394 | | @(opt_All_mp … G4) |
---|
395 | #x |
---|
396 | @(eq_identifier_elim … x vis_hd) #Heq |
---|
397 | [ >Heq |
---|
398 | lapply (in_map_domain … visited vis_hd) |
---|
399 | >H3 normalize nodelta in ⊢ (%→?); |
---|
400 | #EQlookup >EQlookup * #nth_opt_visiting #gen_length_eq |
---|
401 | >lookup_add_hit %1 >gen_length_eq % |
---|
402 | | >(lookup_add_miss ?????? Heq) |
---|
403 | lapply (in_map_domain … visited x) |
---|
404 | elim (true_or_false_Prop (x∈visited)) #x_vis >x_vis |
---|
405 | normalize nodelta in ⊢ (%→?); [ * #n' ] |
---|
406 | #EQlookupx >EQlookupx whd in ⊢ (%→%); * |
---|
407 | [ #G %1{G} |
---|
408 | | #G %2 @nth_opt_append_hit_l |
---|
409 | assumption |
---|
410 | | #G elim(absurd ?? Heq) |
---|
411 | (* BUG (but useless): -required -g -generated *) |
---|
412 | >H2 in G; lapply H1 cases pre |
---|
413 | [ #_ |
---|
414 | | #hd #tl * #hd_vis #_ |
---|
415 | ] normalize #EQ' destruct(EQ') |
---|
416 | [ % |
---|
417 | | >x_vis in hd_vis; * |
---|
418 | ] |
---|
419 | ] |
---|
420 | ] |
---|
421 | ] |
---|
422 | ] |
---|
423 | ] |
---|
424 | | #i whd in match visited'; |
---|
425 | @(eq_identifier_elim … i vis_hd) #Heq |
---|
426 | [ >Heq >lookup_add_hit #ABS destruct(ABS) ] |
---|
427 | >(lookup_add_miss ?????? Heq) |
---|
428 | #i_n_vis |
---|
429 | >does_not_occur_append @andb_Prop |
---|
430 | [ @generated_prf2 assumption |
---|
431 | | change with (bool_to_Prop (¬eq_identifier ??? ∧ ?)) |
---|
432 | >eq_identifier_false [2: % #ABS <ABS in Heq; * #ABS' @ABS' % ] |
---|
433 | @add_req_gen_prf [ #_ | #next #_ #_ ] % |
---|
434 | ] |
---|
435 | ] |
---|
436 | | @add_req_gen_prf |
---|
437 | [ #K | #next #K #next_vis %1 %{(GOTO … next)} % ] |
---|
438 | whd in match generated'; whd in match translated_statement; |
---|
439 | lapply K whd in match visiting'; |
---|
440 | whd in match (stmt_labels ???); cases statement #last |
---|
441 | [2: #_ %1 %{last} % ] #next whd in ⊢ (%→?); #next_vis |
---|
442 | %2 % * >next_vis * |
---|
443 | | whd in match generated'; |
---|
444 | @add_req_gen_prf [ #_ | #next #_ #_ ] normalize >gen_length_prf % |
---|
445 | ] |
---|
446 | qed. |
---|
447 | |
---|
448 | (* CSC: The branch compression (aka tunneling) optimization is not implemented |
---|
449 | in Matita *) |
---|
450 | definition branch_compress |
---|
451 | ≝ λp: graph_params.λglobals.λg:codeT p globals. |
---|
452 | λentry : Σl.bool_to_Prop (code_has_label … g l).g. |
---|
453 | |
---|
454 | lemma branch_compress_closed : ∀p,globals,g,l.code_closed ?? g → |
---|
455 | code_closed … (branch_compress p globals g l). |
---|
456 | #p#globals#g#l#H @H qed. |
---|
457 | |
---|
458 | lemma branch_compress_has_entry : ∀p,globals,g,l. |
---|
459 | code_has_label … (branch_compress p globals g l) l. |
---|
460 | #p#globals#g*#l#l_prf @l_prf qed. |
---|
461 | |
---|
462 | definition filter_labels ≝ λtag,A.λtest : identifier tag → bool.λc : list (labelled_obj tag A). |
---|
463 | map ?? |
---|
464 | (λs. let 〈l_opt,x〉 ≝ s in |
---|
465 | 〈! l ← l_opt ; if test l then return l else None ?, x〉) c. |
---|
466 | |
---|
467 | lemma does_not_occur_filter_labels : |
---|
468 | ∀tag,A,test,id,c. |
---|
469 | does_not_occur ?? id (filter_labels tag A test c) = |
---|
470 | (does_not_occur ?? id c ∨ ¬ test id). |
---|
471 | #tag #A #test #id #c elim c |
---|
472 | [ // |
---|
473 | | ** [2: #lbl] #s #tl #IH |
---|
474 | whd in match (filter_labels ????); normalize nodelta |
---|
475 | whd in match (does_not_occur ????) in ⊢ (??%%); |
---|
476 | [2: @IH] |
---|
477 | normalize in match (! l ← ? ; ?); >IH |
---|
478 | @(eq_identifier_elim ?? lbl id) #Heq [<Heq] |
---|
479 | elim (test lbl) normalize nodelta |
---|
480 | change with (eq_identifier ???) in match (instruction_matches_identifier ????); |
---|
481 | [1,2: >eq_identifier_refl [2: >commutative_orb] normalize % |
---|
482 | |*: >(eq_identifier_false ??? Heq) normalize nodelta % |
---|
483 | ] |
---|
484 | ] |
---|
485 | qed. |
---|
486 | |
---|
487 | lemma occurs_exactly_once_filter_labels : |
---|
488 | ∀tag,A,test,id,c. |
---|
489 | occurs_exactly_once ?? id (filter_labels tag A test c) = |
---|
490 | (occurs_exactly_once ?? id c ∧ test id). |
---|
491 | #tag #A #test #id #c elim c |
---|
492 | [ // |
---|
493 | | ** [2: #lbl] #s #tl #IH |
---|
494 | whd in match (filter_labels ????); normalize nodelta |
---|
495 | whd in match (occurs_exactly_once ????) in ⊢ (??%%); |
---|
496 | [2: @IH] |
---|
497 | normalize in match (! l ← ? ; ?); >IH |
---|
498 | >does_not_occur_filter_labels |
---|
499 | @(eq_identifier_elim ?? lbl id) #Heq [<Heq] |
---|
500 | elim (test lbl) normalize nodelta |
---|
501 | change with (eq_identifier ???) in match (instruction_matches_identifier ????); |
---|
502 | [1,2: >eq_identifier_refl >commutative_andb [ >(commutative_andb ? true) >commutative_orb | >(commutative_andb ? false)] normalize % |
---|
503 | |*: >(eq_identifier_false ??? Heq) normalize nodelta % |
---|
504 | ] |
---|
505 | ] |
---|
506 | qed. |
---|
507 | |
---|
508 | lemma nth_opt_filter_labels : ∀tag,A,test,instrs,n. |
---|
509 | nth_opt ? n (filter_labels tag A test instrs) = |
---|
510 | ! 〈lopt, s〉 ← nth_opt ? n instrs ; |
---|
511 | return 〈 ! lbl ← lopt; if test lbl then return lbl else None ?, s〉. |
---|
512 | #tag #A #test #instrs elim instrs |
---|
513 | [ * [2: #n'] % |
---|
514 | | * #lopt #s #tl #IH * [2: #n'] |
---|
515 | whd in match (filter_labels ????); normalize nodelta |
---|
516 | whd in match (nth_opt ???) in ⊢ (??%%); [>IH] % |
---|
517 | ] |
---|
518 | qed. |
---|
519 | |
---|
520 | lemma stmt_at_filter_labels : ∀p : lin_params.∀globals,test.∀c : codeT p globals. |
---|
521 | ∀i.stmt_at p globals (filter_labels ?? test c) i = stmt_at p globals c i. |
---|
522 | #p#globals#test #c#i |
---|
523 | whd in ⊢ (??%%); >nth_opt_filter_labels |
---|
524 | elim (nth_opt ???); // |
---|
525 | qed. |
---|
526 | |
---|
527 | lemma option_bind_inverse : ∀A,B.∀m : option A.∀f : A → option B.∀r. |
---|
528 | ! x ← m ; f x = return r → |
---|
529 | ∃x.m = return x ∧ f x = return r. |
---|
530 | #A #B * normalize [2:#x] #f #r #EQ destruct |
---|
531 | %{x} %{EQ} % |
---|
532 | qed. |
---|
533 | |
---|
534 | lemma nth_opt_reverse_hit : |
---|
535 | ∀A,l,n.n < |l| → nth_opt A n (reverse ? l) = nth_opt A (|l| - (S n)) l. |
---|
536 | #A #l elim l |
---|
537 | [ #n #ABS normalize in ABS; @⊥ -A /2 by absurd/ |
---|
538 | | #hd #tl #IH #n #lim whd in match (reverse ??); >rev_append_def |
---|
539 | @(leb_elim (S n) (|tl|)) #H |
---|
540 | [ >nth_opt_append_l [2: >length_reverse @H ] |
---|
541 | >(IH … H) >(minus_Sn_m … H) % |
---|
542 | | >(le_to_le_to_eq … (le_S_S_to_le … lim) (not_lt_to_le … H)) |
---|
543 | >nth_opt_append_r >length_reverse [2: % ] |
---|
544 | <minus_n_n <minus_n_n % |
---|
545 | ] |
---|
546 | ] |
---|
547 | qed. |
---|
548 | |
---|
549 | lemma nth_opt_reverse_hit_inv : |
---|
550 | ∀A,l,n.n < |l| → nth_opt A (|l| - (S n)) (reverse ? l) = nth_opt A n l. |
---|
551 | #A #l #n #H <(reverse_reverse ? l) in ⊢ (???%); @sym_eq |
---|
552 | <length_reverse @nth_opt_reverse_hit >length_reverse @H |
---|
553 | qed. |
---|
554 | |
---|
555 | definition linearise_code: |
---|
556 | ∀p : unserialized_params.∀globals. |
---|
557 | ∀g : codeT (mk_graph_params p) globals.code_closed … g → |
---|
558 | ∀entry : (Σl.bool_to_Prop (code_has_label … g l)). |
---|
559 | (Σc : codeT (mk_lin_params p) globals. |
---|
560 | code_closed … c ∧ |
---|
561 | ∃ sigma : identifier_map LabelTag ℕ. |
---|
562 | lookup … sigma entry = Some ? 0 ∧ |
---|
563 | ∀l,n.lookup … sigma l = Some ? n → |
---|
564 | ∃s. lookup … g l = Some ? s ∧ |
---|
565 | opt_Exists ? |
---|
566 | (λls.let 〈lopt, ts〉 ≝ ls in |
---|
567 | opt_All ? (eq ? l) lopt ∧ |
---|
568 | ts = graph_to_lin_statement … s ∧ |
---|
569 | opt_All ? |
---|
570 | (λnext.Or (lookup … sigma next = Some ? (S n)) |
---|
571 | (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) |
---|
572 | (stmt_implicit_label … s)) (nth_opt … n c)) |
---|
573 | ≝ |
---|
574 | λp,globals,g,g_prf,entry_sig. |
---|
575 | let g ≝ branch_compress (mk_graph_params p) ? g entry_sig in |
---|
576 | let g_prf ≝ branch_compress_closed … g entry_sig g_prf in |
---|
577 | match graph_visit p globals g ∅ (empty_map …) [ ] [entry_sig] 0 (|g|) |
---|
578 | (entry_sig) g_prf ????????? |
---|
579 | with |
---|
580 | [ mk_Sig triple H ⇒ |
---|
581 | let sigma ≝ \fst (\fst triple) in |
---|
582 | let required ≝ \snd (\fst triple) in |
---|
583 | let crev ≝ \snd triple in |
---|
584 | let lbld_code ≝ rev ? crev in |
---|
585 | mk_Sig ?? (filter_labels … (λl.l∈required) lbld_code) ? ]. |
---|
586 | [ (* done later *) |
---|
587 | | #i >mem_set_empty * |
---|
588 | |3,4: #a #b whd in ⊢ (??%?→?); #ABS destruct(ABS) |
---|
589 | | #l #_ % |
---|
590 | | %2 % * >mem_set_empty * |
---|
591 | | % [2: %] @(branch_compress_has_entry … g entry_sig) |
---|
592 | | % |
---|
593 | | % % [% %] cases (pi1 … entry_sig) normalize #_ % // |
---|
594 | | >commutative_plus change with (? ≤ |g|) % |
---|
595 | ] |
---|
596 | lapply (refl … triple) |
---|
597 | generalize in match triple in ⊢ (???%→%); ** |
---|
598 | #visited #required #generated #EQtriple |
---|
599 | >EQtriple in H ⊢ %; normalize nodelta **** |
---|
600 | #entry_O #req_vis #last_fin #labels_in_req #sigma_prop |
---|
601 | % >EQtriple |
---|
602 | [ #i #s |
---|
603 | >stmt_at_filter_labels #EQ |
---|
604 | % |
---|
605 | [ @stmt_forall_labels_explicit |
---|
606 | @(All_mp … (labels_in_req … EQ)) |
---|
607 | #l #l_req >lin_code_has_label |
---|
608 | >occurs_exactly_once_filter_labels >l_req |
---|
609 | >commutative_andb whd in ⊢ (?%); |
---|
610 | elim (sigma_prop ?? (lookup_eq_safe … (req_vis … l_req))) |
---|
611 | >lin_code_has_label #H #_ @H |
---|
612 | | lapply EQ cases s #s' [2: #_ % ] |
---|
613 | * -EQ #EQ change with (bool_to_Prop (code_has_point ????)) |
---|
614 | whd in match (point_of_succ ???); |
---|
615 | >lin_code_has_point @leb_elim [ #_ % ] >length_map >length_reverse |
---|
616 | #INEQ |
---|
617 | cut (|generated| = S i) |
---|
618 | [ @(le_to_le_to_eq … (not_lt_to_le … INEQ) ) |
---|
619 | elim (option_bind_inverse ????? EQ) #x * #EQ1 #EQ2 |
---|
620 | <length_reverse |
---|
621 | @(nth_opt_hit_length … EQ1) |
---|
622 | ] #EQ_length |
---|
623 | elim last_fin #fin #EQ' |
---|
624 | lapply EQ whd in match (stmt_at ????); |
---|
625 | >nth_opt_reverse_hit >EQ_length [2: % ] <minus_n_n |
---|
626 | change with (stmt_at ???? = ? → ?) |
---|
627 | >EQ' #ABS destruct(ABS) |
---|
628 | ] |
---|
629 | ] |
---|
630 | %{visited} % [assumption] |
---|
631 | #lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup) |
---|
632 | #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in |
---|
633 | % [2: % [ assumption ] |] |
---|
634 | >nth_opt_filter_labels in ⊢ (???%); |
---|
635 | >nth_opt_is_stmt >m_return_bind whd >m_return_bind |
---|
636 | % [ % ] |
---|
637 | [ elim (lbl ∈ required) % |
---|
638 | | % |
---|
639 | | lapply succ_is_in |
---|
640 | lapply (refl … (stmt_implicit_label … stmt)) |
---|
641 | cases (stmt_implicit_label … stmt) in ⊢ (???%→%); [#_ #_ %] |
---|
642 | #next #EQ_next * |
---|
643 | [ #H %1{H} ] |
---|
644 | #H %2 |
---|
645 | >nth_opt_filter_labels >H % |
---|
646 | ] |
---|
647 | qed. |
---|
648 | |
---|
649 | (* Paolo: for now I'm leaving the closed graph stuff out, waiting for it to |
---|
650 | be done on all passes *) |
---|
651 | definition linearise_int_fun : |
---|
652 | ∀p : unserialized_params. |
---|
653 | ∀globals. |
---|
654 | joint_internal_function (mk_graph_params p) globals → |
---|
655 | joint_internal_function (mk_lin_params p) globals |
---|
656 | (* ∃sigma : identifier_map LabelTag ℕ. |
---|
657 | let g ≝ joint_if_code ?? (pi1 … fin) in |
---|
658 | let c ≝ joint_if_code ?? (pi1 … fout) in |
---|
659 | let entry ≝ joint_if_entry ?? (pi1 … fin) in |
---|
660 | lookup … sigma entry = Some ? 0 ∧ |
---|
661 | ∀l,n.lookup … sigma l = Some ? n → |
---|
662 | ∃s. lookup … g l = Some ? s ∧ |
---|
663 | opt_Exists ? |
---|
664 | (λls.let 〈lopt, ts〉 ≝ ls in |
---|
665 | opt_All ? (eq ? l) lopt ∧ |
---|
666 | ts = graph_to_lin_statement … s ∧ |
---|
667 | opt_All ? |
---|
668 | (λnext.Or (lookup … sigma next = Some ? (S n)) |
---|
669 | (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) |
---|
670 | (stmt_implicit_label … s)) (nth_opt … n c)*) ≝ |
---|
671 | λp,globals,f_in. |
---|
672 | mk_joint_internal_function (mk_lin_params p) globals |
---|
673 | (joint_if_luniverse ?? f_in) (joint_if_runiverse ?? f_in) |
---|
674 | (joint_if_result ?? f_in) (joint_if_params ?? f_in) (joint_if_locals ?? f_in) |
---|
675 | (joint_if_stacksize ?? f_in) |
---|
676 | (linearise_code p globals (joint_if_code … f_in) |
---|
677 | (match daemon in False with [ ]) |
---|
678 | (joint_if_entry … f_in)) |
---|
679 | 0 0 (* exit is dummy! *). |
---|
680 | elim (linearise_code ?????) #c * #code_closed |
---|
681 | @hide_prf |
---|
682 | * #sigma * #O_in #sigma_prop |
---|
683 | >lin_code_has_point |
---|
684 | elim (sigma_prop … O_in) #s * #_ |
---|
685 | cases c |
---|
686 | [1,3: * |
---|
687 | |*: #hd #tl #_ % |
---|
688 | ] |
---|
689 | qed. |
---|