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