1 | include "joint/Joint_paolo.ma". |
---|
2 | include "utilities/bind_new.ma". |
---|
3 | |
---|
4 | definition uncurry_helper : ∀A,B,C : Type[0].(A → B → C) → (A×B) → C ≝ |
---|
5 | λA,B,C,f,p.f (\fst p) (\snd p). |
---|
6 | |
---|
7 | inductive stmt_type : Type[0] ≝ |
---|
8 | | SEQ : stmt_type |
---|
9 | | FIN : stmt_type. |
---|
10 | |
---|
11 | definition stmt_type_if : ∀A : Type[1].stmt_type → A → A → A ≝ |
---|
12 | λA,t,x,y.match t with [ SEQ ⇒ x | FIN ⇒ y ]. |
---|
13 | |
---|
14 | definition block_cont ≝ λp : params.λglobals,ty. |
---|
15 | (list (joint_step p globals)) × |
---|
16 | (stmt_type_if ? ty (joint_step p) (joint_fin_step p) globals). |
---|
17 | |
---|
18 | definition Skip : ∀p,globals.block_cont p globals SEQ ≝ |
---|
19 | λp,globals.〈[ ], NOOP …〉. |
---|
20 | |
---|
21 | definition instr_block ≝ λp : params.λglobals,ty. |
---|
22 | bind_new (localsT p) (block_cont p globals ty). |
---|
23 | unification hint 0 ≔ p, globals, ty; |
---|
24 | B ≟ block_cont p globals ty, R ≟ localsT p |
---|
25 | (*---------------------------------------*)⊢ |
---|
26 | instr_block p globals ty ≡ bind_new R B. |
---|
27 | |
---|
28 | definition block_cont_append : |
---|
29 | ∀p,g,ty. |
---|
30 | ∀b1 : block_cont p g SEQ. |
---|
31 | ∀b2 : block_cont p g ty. |
---|
32 | block_cont p g ty ≝ |
---|
33 | λp,globals,ty,b1,b2.〈\fst b1 @ \snd b1 :: \fst b2, \snd b2〉. |
---|
34 | |
---|
35 | definition block_cont_cons ≝ λp,g,ty,x.λb : block_cont p g ty.〈x :: \fst b,\snd b〉. |
---|
36 | |
---|
37 | interpretation "block contents cons" 'cons x b = (block_cont_cons ??? x b). |
---|
38 | interpretation "block contents append" 'append b1 b2 = (block_cont_append ??? b1 b2). |
---|
39 | |
---|
40 | definition step_to_block : ∀p : params.∀g. |
---|
41 | joint_step p g → block_cont p g SEQ ≝ λp,g,s.〈[ ], s〉. |
---|
42 | |
---|
43 | definition fin_step_to_block : ∀p : params.∀g. |
---|
44 | joint_fin_step p g → block_cont p g FIN ≝ λp,g,s.〈[ ], s〉. |
---|
45 | |
---|
46 | coercion block_from_step : ∀p : params.∀g.∀s : joint_step p g. |
---|
47 | block_cont p g SEQ ≝ step_to_block on _s : joint_step ?? to block_cont ?? SEQ. |
---|
48 | |
---|
49 | coercion block_from_fin_step : ∀p : params.∀g.∀s : joint_fin_step p g. |
---|
50 | block_cont p g FIN ≝ fin_step_to_block |
---|
51 | on _s : joint_fin_step ?? to block_cont ?? FIN. |
---|
52 | |
---|
53 | definition block_cons : |
---|
54 | ∀p : params.∀globals,ty. |
---|
55 | joint_step p globals → instr_block p globals ty → instr_block p globals ty |
---|
56 | ≝ λp,globals,ty,x.m_map … (block_cont_cons … x). |
---|
57 | |
---|
58 | definition block_append : |
---|
59 | ∀p : params.∀globals,ty. |
---|
60 | instr_block p globals SEQ → instr_block p globals ty → instr_block p globals ty ≝ |
---|
61 | λp,globals,ty.m_bin_op … (block_cont_append …). |
---|
62 | |
---|
63 | interpretation "instruction block cons" 'cons x b = (block_cons ??? x b). |
---|
64 | interpretation "instruction block append" 'append b1 b2 = (block_append ??? b1 b2). |
---|
65 | |
---|
66 | let rec is_block_instance (p : params) g ty (b : instr_block p g ty) (l : list (localsT p)) (b' : block_cont p g ty) on b : Prop ≝ |
---|
67 | match b with |
---|
68 | [ bret B ⇒ |
---|
69 | match l with |
---|
70 | [ nil ⇒ B = b' |
---|
71 | | cons _ _ ⇒ False |
---|
72 | ] |
---|
73 | | bnew f ⇒ |
---|
74 | match l with |
---|
75 | [ nil ⇒ False |
---|
76 | | cons r l' ⇒ |
---|
77 | is_block_instance p g ty (f r) l' b' |
---|
78 | ] |
---|
79 | ]. |
---|
80 | |
---|
81 | lemma is_block_instance_append : ∀p,globals,ty,b1,b2,l1,l2,b1',b2'. |
---|
82 | is_block_instance p globals SEQ b1 l1 b1' → |
---|
83 | is_block_instance p globals ty b2 l2 b2' → |
---|
84 | is_block_instance p globals ty (b1 @ b2) (l1 @ l2) (b1' @ b2'). |
---|
85 | #p#globals#ty #b1 elim b1 |
---|
86 | [ #B1 | #f1 #IH1 ] #b2 * [2,4: #r1 #l1' ] #l2 #b1' #b2' [1,4: *] |
---|
87 | normalize in ⊢ (%→?); |
---|
88 | [ @IH1 |
---|
89 | | #EQ destruct(EQ) lapply b2' -b2' lapply l2 -l2 elim b2 |
---|
90 | [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2' [1,4: *] |
---|
91 | normalize in ⊢ (%→?); [2: //] #H2 |
---|
92 | change with (is_block_instance ??? ('new ?) (r2 :: ?) ?) whd |
---|
93 | @(IH2 … H2) |
---|
94 | ] |
---|
95 | qed. |
---|
96 | |
---|
97 | definition tunnel_step : ∀p,g.codeT p g → relation (code_point p) ≝ |
---|
98 | λp,g,c,x,y.∃l.stmt_at … c x = Some ? (GOTO … l) ∧ point_of_label … c l = Some ? y. |
---|
99 | |
---|
100 | notation > "x ~~> y 'in' c" with precedence 56 for @{'tunnel_step $c $x $y}. |
---|
101 | notation < "hvbox(x ~~> y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_step $c $x $y}. |
---|
102 | interpretation "tunnel step in code" 'tunnel_step c x y = (tunnel_step ?? c x y). |
---|
103 | |
---|
104 | let rec tunnel_through p g (c : codeT p g) x through y on through : Prop ≝ |
---|
105 | match through with |
---|
106 | [ nil ⇒ x = y |
---|
107 | | cons hd tl ⇒ x ~~> hd in c ∧ tunnel_through … hd tl y |
---|
108 | ]. |
---|
109 | |
---|
110 | definition tunnel ≝ λp,g,c,x,y.∃through.tunnel_through p g c x through y. |
---|
111 | |
---|
112 | notation > "x ~~>^* y 'in' c" with precedence 56 for @{'tunnel $c $x $y}. |
---|
113 | notation < "hvbox(x \nbsp ~~>^* \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel $c $x $y}. |
---|
114 | interpretation "tunnel in code" 'tunnel c x y = (tunnel ?? c x y). |
---|
115 | |
---|
116 | lemma tunnel_refl : ∀p,g.∀c : codeT p g.reflexive ? (tunnel p g c). |
---|
117 | #p #g #c #x %{[]} % qed. |
---|
118 | |
---|
119 | lemma tunnel_trans : ∀p,g.∀c : codeT p g. |
---|
120 | transitive ? (tunnel p g c). |
---|
121 | #p#g#c #x#y#z * #l1 #H1 * #l2 #H2 %{(l1@l2)} |
---|
122 | lapply H1 -H1 lapply x -x elim l1 -l1 |
---|
123 | [ #x #H1 >H1 @H2 |
---|
124 | | #hd #tl #IH #x * #H11 #H12 |
---|
125 | %{H11} @IH @H12 |
---|
126 | ] qed. |
---|
127 | |
---|
128 | definition tunnel_plus ≝ λp,g.λc : codeT p g.λx,y. |
---|
129 | ∃mid.x ~~> mid in c ∧ mid ~~>^* y in c. |
---|
130 | |
---|
131 | notation > "x ~~>^+ y 'in' c" with precedence 56 for @{'tunnel_plus $c $x $y}. |
---|
132 | notation < "hvbox(x \nbsp ~~>^+ \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_plus $c $x $y}. |
---|
133 | interpretation "tunnel in code" 'tunnel_plus c x y = (tunnel_plus ?? c x y). |
---|
134 | |
---|
135 | lemma tunnel_plus_to_star : ∀p,g.∀c : codeT p g.∀x,y.x ~~>^+ y in c → x ~~>^* y in c. |
---|
136 | #p #g #c #x #y * #mid * #H1 * #through #H2 %{(mid :: through)} |
---|
137 | %{H1 H2} qed. |
---|
138 | |
---|
139 | lemma tunnel_plus_trans : ∀p,g.∀c : codeT p g.transitive ? (tunnel_plus p g c). |
---|
140 | #p #g #c #x #y #z * #mid * #H1 #H2 |
---|
141 | #H3 %{mid} %{H1} @(tunnel_trans … H2) /2 by tunnel_plus_to_star/ |
---|
142 | qed. |
---|
143 | |
---|
144 | lemma tunnel_tunnel_plus : ∀p,g.∀c : codeT p g.∀x,y,z. |
---|
145 | x ~~>^* y in c → y ~~>^+ z in c → x ~~>^+ z in c. |
---|
146 | #p #g #c #x #y #z * #through |
---|
147 | lapply x -x elim through |
---|
148 | [ #x #H1 >H1 // |
---|
149 | | #hd #tl #IH #x * #H1 #H2 #H3 |
---|
150 | %{hd} %{H1} @(tunnel_trans ???? y) |
---|
151 | [ %{tl} assumption | /2 by tunnel_plus_to_star/] |
---|
152 | ] |
---|
153 | qed. |
---|
154 | |
---|
155 | lemma tunnel_plus_tunnel : ∀p,g.∀c : codeT p g.∀x,y,z. |
---|
156 | x ~~>^+ y in c → y ~~>^* z in c → x ~~>^+ z in c. |
---|
157 | #p #g #c #x #y #z * #mid * #H1 #H2 #H3 %{mid} %{H1} |
---|
158 | @(tunnel_trans … H2 H3) |
---|
159 | qed. |
---|
160 | |
---|
161 | let rec seq_list_in_code (p : params) g (c : codeT p g) |
---|
162 | src l dst on l : Prop ≝ |
---|
163 | match l with |
---|
164 | [ nil ⇒ src = dst |
---|
165 | | cons hd tl ⇒ |
---|
166 | ∃n.stmt_at … c src = Some ? (sequential … hd n) ∧ |
---|
167 | seq_list_in_code p g c (point_of_succ … src n) tl dst |
---|
168 | ]. |
---|
169 | |
---|
170 | (* |
---|
171 | definition seq_block_cont_to_list : ∀p,g.block_cont p g SEQ → list (joint_step p g) ≝ |
---|
172 | λp,g,b.\fst b @ [\snd b]. |
---|
173 | |
---|
174 | coercion list_from_seq_block_cont : ∀p,g.∀b:block_cont p g SEQ.list (joint_step p g) ≝ |
---|
175 | seq_block_cont_to_list on _b : block_cont ?? SEQ to list (joint_step ??). |
---|
176 | *) |
---|
177 | |
---|
178 | definition unit_deqset: DeqSet ≝ mk_DeqSet unit (λ_.λ_.true) ?. |
---|
179 | * * /2/ |
---|
180 | qed. |
---|
181 | |
---|
182 | definition block_cont_in_code : ∀p,g.codeT p g → ∀ty. |
---|
183 | code_point p → block_cont p g ty → stmt_type_if ? ty (code_point p) unit_deqset → Prop ≝ |
---|
184 | λp,g.λc : codeT p g.λty,src,b,dst. |
---|
185 | ∃mid.seq_list_in_code p g c src (\fst b) mid ∧ |
---|
186 | match ty |
---|
187 | return λx.stmt_type_if ? x ??? → |
---|
188 | stmt_type_if ? x ? unit_deqset → Prop |
---|
189 | with |
---|
190 | [ SEQ ⇒ λs,dst. |
---|
191 | ∃n.stmt_at … c mid = Some ? (sequential … s n) ∧ |
---|
192 | point_of_succ … mid n = dst |
---|
193 | | FIN ⇒ λs.λ_.stmt_at … c mid = Some ? (final … s) |
---|
194 | ] (\snd b) dst. |
---|
195 | |
---|
196 | |
---|
197 | notation > "x ~❨ B ❩~> y 'in' c" with precedence 56 for |
---|
198 | @{'block_in_code $c $x $B $y}. |
---|
199 | |
---|
200 | notation < "hvbox(x ~❨ B ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for |
---|
201 | @{'block_in_code $c $x $B $y}. |
---|
202 | |
---|
203 | interpretation "block cont in code" 'block_in_code c x B y = |
---|
204 | (block_cont_in_code ?? c ? x B y). |
---|
205 | |
---|
206 | lemma seq_list_in_code_append : ∀p,g.∀c : codeT p g.∀x,l1,y,l2,z. |
---|
207 | seq_list_in_code p g c x l1 y → |
---|
208 | seq_list_in_code p g c y l2 z → |
---|
209 | seq_list_in_code p g c x (l1@l2) z. |
---|
210 | #p#g#c#x#l1 lapply x -x |
---|
211 | elim l1 [2: #hd #tl #IH] #x #y #l2 #z normalize in ⊢ (%→?); |
---|
212 | [ * #n * #EQ1 #H #G %{n} %{EQ1} @(IH … H G) |
---|
213 | | #EQ destruct(EQ) // |
---|
214 | ] |
---|
215 | qed. |
---|
216 | |
---|
217 | lemma block_cont_in_code_append : ∀p,g.∀c : codeT p g.∀ty,x. |
---|
218 | ∀B1 : block_cont p g SEQ.∀y.∀B2 : block_cont p g ty.∀z. |
---|
219 | x ~❨B1❩~> y in c → y ~❨B2❩~> z in c → x ~❨B1@B2❩~> z in c. |
---|
220 | #p#g#c #ty #x * whd in match stmt_type_if in ⊢ (?→%→%→?); normalize nodelta |
---|
221 | #l1 #s1 #y * #l2 #s2 #z * normalize nodelta |
---|
222 | #mid1 * #H1 * #n * #EQ1 #EQ2 * #mid2 * #H2 #H3 |
---|
223 | %{mid2} % |
---|
224 | [ whd in match (〈?,?〉@?); |
---|
225 | @(seq_list_in_code_append … H1) |
---|
226 | %{n} %{EQ1} >EQ2 assumption |
---|
227 | | assumption |
---|
228 | ] |
---|
229 | qed. |
---|
230 | |
---|
231 | definition instr_block_in_function : |
---|
232 | ∀p,g.∀fn : joint_internal_function g p.∀ty. |
---|
233 | instr_block p g ty → |
---|
234 | code_point p → |
---|
235 | ? → Prop ≝ |
---|
236 | λp,g,fn,ty,B,src,dst. |
---|
237 | ∃vars,B'. |
---|
238 | All ? (In ? (joint_if_locals … fn)) vars ∧ |
---|
239 | is_block_instance … B vars B' ∧ |
---|
240 | src ~❨B'❩~> dst in joint_if_code … fn. |
---|
241 | |
---|
242 | interpretation "instr block in function" 'block_in_code fn x B y = |
---|
243 | (instr_block_in_function ?? fn ? B x y). |
---|
244 | |
---|
245 | lemma instr_block_in_function_trans : |
---|
246 | ∀p,g.∀fn : joint_internal_function g p.∀ty,src. |
---|
247 | ∀B1 : instr_block p g SEQ. |
---|
248 | ∀mid.∀B2 : instr_block p g ty.∀dst. |
---|
249 | src ~❨B1❩~> mid in fn → |
---|
250 | mid ~❨B2❩~> dst in fn → |
---|
251 | src ~❨B1@B2❩~> dst in fn. |
---|
252 | #p#g#fn#ty#src#B1#mid#B2#dst |
---|
253 | * #vars1 * #b1 ** #vars1_ok #b1B1 #b1_in |
---|
254 | * #vars2 * #b2 ** #vars2_ok #b2B2 #b2_in |
---|
255 | %{(vars1@vars2)} %{(b1 @ b2)} |
---|
256 | /4 by All_append, conj, is_block_instance_append, block_cont_in_code_append/ |
---|
257 | qed. |
---|