Context Navigation

linearise.ma @ 2557

Last change on this file since 2557 was 2547, checked in by tranquil, 8 years ago
going on in proof of linearise simplified by use of monadic functional relations
File size: 33.0 KB

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

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format