1 | include "common/AST.ma". |
---|
2 | include "common/Globalenvs.ma". |
---|
3 | |
---|
4 | (* TODO: need this for global env *) |
---|
5 | axiom find_funct_ptr_symbol_inversion: |
---|
6 | ∀F,V,init. ∀p: program F V. |
---|
7 | ∀id: ident. ∀b: block. ∀f: F ?. |
---|
8 | find_symbol ? (globalenv ?? init p) id = Some ? b → |
---|
9 | find_funct_ptr ? (globalenv ?? init p) b = Some ? f → |
---|
10 | In … (prog_funct ?? p) 〈id, f〉. |
---|
11 | |
---|
12 | axiom find_funct_ptr_exists: |
---|
13 | ∀F,V,init. ∀p: program F V. ∀id: ident. ∀f: F ?. |
---|
14 | In … (prog_funct ?? p) 〈id, f〉 → |
---|
15 | ∃b. find_symbol ? (globalenv ?? init p) id = Some ? b |
---|
16 | ∧ find_funct_ptr ? (globalenv ?? init p) b = Some ? f. |
---|
17 | |
---|
18 | axiom find_symbol_exists: |
---|
19 | ∀F,V,init. ∀p: program F V. |
---|
20 | ∀id: ident. ∀r,v. |
---|
21 | In ? (prog_vars ?? p) 〈〈id, r〉, v〉 → |
---|
22 | ∃b. find_symbol ? (globalenv ?? init p) id = Some ? b. |
---|
23 | |
---|
24 | definition is_internal_function_of_program : |
---|
25 | ∀A,B.program (λvars.fundef (A vars)) B → ident → Prop ≝ |
---|
26 | λA,B,prog,i.∃ifd.In … (prog_funct ?? prog) 〈i, Internal ? ifd〉. |
---|
27 | |
---|
28 | definition is_function ≝ λF.λge : genv_t F. |
---|
29 | λi : ident.∃fd. |
---|
30 | ! bl ← find_symbol … ge i ; |
---|
31 | find_funct_ptr … ge bl = Some ? fd. |
---|
32 | |
---|
33 | definition funct_of_ident : ∀F,ge. |
---|
34 | ident → option (Σi.is_function F ge i) |
---|
35 | ≝ λF,ge,i. |
---|
36 | match ? |
---|
37 | return λx.! bl ← find_symbol … ge i ; |
---|
38 | find_funct_ptr … ge bl = x → ? |
---|
39 | with |
---|
40 | [ Some fd ⇒ λprf.return «i, ex_intro ?? fd prf» |
---|
41 | | None ⇒ λ_.None ? |
---|
42 | ] (refl …). |
---|
43 | |
---|
44 | lemma symbol_of_function_block_ok : |
---|
45 | ∀F,ge,b,prf.symbol_for_block F ge b = Some ? (symbol_of_function_block F ge b prf). |
---|
46 | #F #ge #b #FFP |
---|
47 | cut (∀A,B : Type[0].∀P : B → Prop.∀x : option A.∀c1,c2. |
---|
48 | (∀v.∀prf : x = Some ? v.P (c1 v prf)) → |
---|
49 | (∀prf:x = None ?.P (c2 prf)) → |
---|
50 | P (match x return λy.x = y → ? with |
---|
51 | [ Some v ⇒ λprf.c1 v prf | None ⇒ λprf.c2 prf] |
---|
52 | (refl …))) [ #A #B #P * // ] #aux |
---|
53 | whd in ⊢ (???(??%)); @aux [//] #H @⊥ |
---|
54 | (* cut and paste from global env *) |
---|
55 | whd in H:(??%?); |
---|
56 | cases b in FFP H ⊢ %; * * -b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP | *: * #H cases (H (refl ??)) ] |
---|
57 | cases (functions_inv … ge b FFP) |
---|
58 | #id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b))) |
---|
59 | lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b))) |
---|
60 | cases (find ????) |
---|
61 | [ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ * | * #H' cases (H' (refl ??)) ] |
---|
62 | | * #id' #b' #_ normalize #_ #E destruct |
---|
63 | ] qed. |
---|
64 | |
---|
65 | definition funct_of_block : ∀F,ge. |
---|
66 | block → option (Σi.is_function F ge i) ≝ |
---|
67 | λF,ge,bl. |
---|
68 | match find_funct_ptr … ge bl |
---|
69 | return λx.find_funct_ptr … ge bl = x → ? with |
---|
70 | [ Some fd ⇒ λprf.return mk_Sig |
---|
71 | ident (λi.is_function F ge i) |
---|
72 | (symbol_of_function_block … ge bl ?) |
---|
73 | (ex_intro … fd ?) |
---|
74 | | None ⇒ λ_.None ? |
---|
75 | ] (refl …). |
---|
76 | [ >(symbol_of_block_rev … (symbol_of_function_block_ok ? ge bl ?)) @prf |
---|
77 | | >prf % #ABS destruct(ABS) |
---|
78 | ] |
---|
79 | qed. |
---|
80 | |
---|
81 | definition block_of_funct ≝ λF,ge. |
---|
82 | λi : Σi.is_function F ge i. |
---|
83 | match find_symbol … ge i return λx.(∃fd.!bl ← x; ? = ?) → ? with |
---|
84 | [ Some bl ⇒ λ_.bl |
---|
85 | | None ⇒ λprf.⊥ |
---|
86 | ] (pi2 … i). |
---|
87 | cases prf #fd normalize #ABS destruct(ABS) |
---|
88 | qed. |
---|
89 | |
---|
90 | definition description_of_function : ∀F,ge.(Σi.is_function F ge i) → F ≝ |
---|
91 | λF,ge,i. |
---|
92 | match ! bl ← find_symbol … ge i ; |
---|
93 | find_funct_ptr … ge bl |
---|
94 | return λx.(∃fd.x = ?) → ? |
---|
95 | with |
---|
96 | [ Some fd ⇒ λ_.fd |
---|
97 | | None ⇒ λprf.⊥ |
---|
98 | ] (pi2 … i). |
---|
99 | cases prf #fd #ABS destruct |
---|
100 | qed. |
---|
101 | |
---|
102 | definition is_internal_function ≝ λF.λge : genv_t (fundef F). |
---|
103 | λi : ident.∃fd. |
---|
104 | ! bl ← find_symbol … ge i ; |
---|
105 | find_funct_ptr … ge bl = Some ? (Internal ? fd). |
---|
106 | |
---|
107 | lemma description_of_internal_function : ∀F,ge,i,fn. |
---|
108 | description_of_function ? ge i = Internal F fn → is_internal_function … ge i. |
---|
109 | #F #ge * #i * #fd #EQ |
---|
110 | #fn whd in ⊢ (??%?→?); >EQ normalize nodelta #EQ' >EQ' in EQ; #EQ |
---|
111 | %{EQ} |
---|
112 | qed. |
---|
113 | |
---|
114 | definition int_funct_of_block : ∀F,ge. |
---|
115 | block → option (Σi.is_internal_function F ge i) ≝ |
---|
116 | λF,ge,bl. |
---|
117 | ! f ← funct_of_block … ge bl ; |
---|
118 | match ? |
---|
119 | return λx.description_of_function … f = x → option (Σi.is_internal_function … ge i) |
---|
120 | with |
---|
121 | [ Internal fn ⇒ λprf.return «pi1 … f, ?» |
---|
122 | | External fn ⇒ λ_.None ? |
---|
123 | ] (refl …). |
---|
124 | @(description_of_internal_function … prf) |
---|
125 | qed. |
---|
126 | |
---|
127 | lemma internal_function_is_function : ∀F,ge,i. |
---|
128 | is_internal_function F ge i → is_function … ge i. |
---|
129 | #F #ge #i * #fn #prf %{prf} qed. |
---|
130 | |
---|
131 | definition if_of_function : ∀F,ge.(Σi.is_internal_function F ge i) → F ≝ |
---|
132 | λF,ge,i. |
---|
133 | match ! bl ← find_symbol … ge i ; |
---|
134 | find_funct_ptr … ge bl |
---|
135 | return λx.(∃fn.x = ?) → ? |
---|
136 | with |
---|
137 | [ Some fd ⇒ |
---|
138 | match fd return λx.(∃fn.Some ? x = ?) → ? with |
---|
139 | [ Internal fn ⇒ λ_.fn |
---|
140 | | External _ ⇒ λprf.⊥ |
---|
141 | ] |
---|
142 | | None ⇒ λprf.⊥ |
---|
143 | ] (pi2 … i). |
---|
144 | cases prf #fn #ABS destruct |
---|
145 | qed. |
---|
146 | |
---|
147 | lemma is_internal_function_of_program_ok : |
---|
148 | ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.∀i. |
---|
149 | is_internal_function … (globalenv ?? init prog) i → |
---|
150 | is_internal_function_of_program ?? prog i. |
---|
151 | #A #B #init #prog #i whd in ⊢ (%→%); * #ifn |
---|
152 | lapply (refl … (find_symbol … i)) |
---|
153 | [3: elim (find_symbol … i) in ⊢ (???%→%); |
---|
154 | [#_ #ABS normalize in ABS; destruct(ABS)] |
---|
155 | |*:] |
---|
156 | #bl #EQbl >m_return_bind #EQfind %{ifn} |
---|
157 | @(find_funct_ptr_symbol_inversion … EQbl EQfind) |
---|
158 | qed. |
---|
159 | |
---|
160 | lemma ok_is_internal_function_of_program : |
---|
161 | ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.∀i. |
---|
162 | is_internal_function_of_program … prog i → |
---|
163 | is_internal_function ? (globalenv ?? init prog) i. |
---|
164 | #A #B #init #prog #i whd in ⊢ (%→%); * #ifn #H |
---|
165 | elim (find_funct_ptr_exists … init … H) |
---|
166 | #bl * #EQ1 #EQ2 %{ifn} >EQ1 @EQ2 qed. |
---|
167 | |
---|
168 | lemma Exists_find : ∀A,B,P,f,l.(∀x.P x → f x ≠ None ?) → Exists ? P l → |
---|
169 | find A B f l ≠ None ?. |
---|
170 | #A #B #P #f #l #H elim l -l [ * ] normalize |
---|
171 | #hd #tl #IH * |
---|
172 | [ #Phd >(opt_to_opt_safe … (H … Phd)) normalize nodelta % #ABS destruct(ABS) |
---|
173 | | #Ptl elim (f hd) |
---|
174 | [ @(IH Ptl) |
---|
175 | | #x % normalize #ABS destruct(ABS) |
---|
176 | ] |
---|
177 | ] |
---|
178 | qed. |
---|
179 | |
---|
180 | definition prog_if_of_function : |
---|
181 | ∀F,V,prog. |
---|
182 | (Σi.is_internal_function_of_program F V prog i) → F ? ≝ |
---|
183 | λF,V,prog,i.opt_safe ? (find ?? |
---|
184 | (λpr.if eq_identifier ? (\fst pr) i then |
---|
185 | match \snd pr with |
---|
186 | [ Internal x ⇒ return x |
---|
187 | | External _ ⇒ None ? |
---|
188 | ] |
---|
189 | else None ?) |
---|
190 | (prog_funct … prog)) ?. |
---|
191 | @hide_prf |
---|
192 | cases i -i #i * #ifn #prf |
---|
193 | @(Exists_find … prf) |
---|
194 | * #i' #fn' #EQ destruct(EQ) >eq_identifier_refl normalize nodelta |
---|
195 | % normalize in ⊢ (??%?→?); #ABS destruct(ABS) |
---|
196 | qed. |
---|
197 | |
---|
198 | definition if_in_global_env_to_if_in_prog : |
---|
199 | ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B. |
---|
200 | (Σi.is_internal_function ? (globalenv ?? init prog) i) → |
---|
201 | Σi.is_internal_function_of_program ?? prog i ≝ |
---|
202 | λA,B,init,prog,f.«f, is_internal_function_of_program_ok … (pi2 … f)». |
---|
203 | |
---|
204 | coercion if_in_prog_from_if_in_global_env nocomposites : |
---|
205 | ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B. |
---|
206 | ∀f:Σi.is_internal_function ? (globalenv ?? init prog) i. |
---|
207 | Σi.is_internal_function_of_program ?? prog i ≝ |
---|
208 | if_in_global_env_to_if_in_prog |
---|
209 | on _f : Sig ident (λi.is_internal_function ?? i) |
---|
210 | to Sig ident (λi.is_internal_function_of_program ??? i). |
---|
211 | |
---|
212 | lemma if_propagate : |
---|
213 | ∀A_in,A_out,B. |
---|
214 | ∀trans. |
---|
215 | ∀prog_in : program (λvars.fundef (A_in vars)) B. |
---|
216 | let prog_out : program (λvars.fundef (A_out vars)) B ≝ |
---|
217 | transform_program … prog_in (λvars.transf_fundef … (trans vars)) in |
---|
218 | ∀i.is_internal_function_of_program … prog_in i → |
---|
219 | is_internal_function_of_program … prog_out i. |
---|
220 | #A_in #A_out #B #trans #prog_in #ident |
---|
221 | * #ifn #H %{(trans … ifn)} |
---|
222 | @(Exists_map … H) * #id #fn #EQ destruct(EQ) % qed. |
---|
223 | |
---|
224 | lemma block_of_funct_ident_is_code : ∀F,ge,i. |
---|
225 | block_region (block_of_funct F ge i) = Code. |
---|
226 | #F #ge * #i * #fd |
---|
227 | whd in ⊢ (?→??(?%)?); |
---|
228 | cases (find_symbol ???) |
---|
229 | [ #ABS normalize in ABS; destruct(ABS) ] |
---|
230 | #bl normalize nodelta >m_return_bind |
---|
231 | whd in ⊢ (??%?→?); cases (block_region bl) |
---|
232 | [ #ABS normalize in ABS; destruct(ABS) ] |
---|
233 | #_ % |
---|
234 | qed. |
---|
235 | |
---|
236 | |
---|
237 | lemma find_map : ∀A,B,C,f,g,l.find B C f (map A B g l) = find A C (λx.f (g x)) l. |
---|
238 | #A #B #C #f #g #l elim l -l [%] #hd #tl #IH normalize >IH % qed. |
---|
239 | |
---|
240 | lemma find_bind : ∀A,B,C,f,g,l. |
---|
241 | find A C (λx.! y ← f x ; return g y) l = ! y ← find A B f l ; return g y. |
---|
242 | #A #B #C #f #g #l elim l -l |
---|
243 | [%] |
---|
244 | #hd #tl #IH |
---|
245 | whd in match (find ??? (hd::tl)) in ⊢ (??%%); |
---|
246 | cases (f hd) [ @IH ] #x % qed. |
---|
247 | |
---|
248 | lemma find_ext_eq : ∀A,B,f,g,l.(∀x.f x = g x) → find A B f l = find A B g l. |
---|
249 | #A #B #f #g #l #H elim l -l [%] #hd #tl #IH normalize >H >IH % qed. |
---|
250 | |
---|
251 | lemma prog_if_of_function_transform : |
---|
252 | ∀A,B,V,trans.∀prog_in : program (λvars.fundef (A vars)) V. |
---|
253 | let prog_out : program (λvars.fundef (B vars)) V≝ |
---|
254 | transform_program … prog_in (λvars.transf_fundef … (trans vars)) in |
---|
255 | ∀i,prf1,prf2. |
---|
256 | prog_if_of_function ?? prog_out «i,prf1» = trans … (prog_if_of_function ?? prog_in «i,prf2»). |
---|
257 | #A #B #V #trans #prog #i #i_prf #i_prf' |
---|
258 | change with (opt_safe ??? = ?) |
---|
259 | @opt_safe_elim #ifn >find_map |
---|
260 | cut (∀vars.∀x. |
---|
261 | if eq_identifier ? (\fst x) i then |
---|
262 | match transf_fundef … (trans vars) (\snd x) with |
---|
263 | [ Internal x ⇒ return x |
---|
264 | | _ ⇒ None ? |
---|
265 | ] else None ? = |
---|
266 | ! y ← if eq_identifier ? (\fst x) i then |
---|
267 | match \snd x with |
---|
268 | [ Internal x ⇒ return x |
---|
269 | | _ ⇒ None ? |
---|
270 | ] else None ? ; |
---|
271 | return trans vars y) |
---|
272 | [ #vars * #id * #fn whd in match transf_fundef; normalize nodelta |
---|
273 | cases (eq_identifier ???) % ] #H |
---|
274 | >(find_ext_eq … (H ?)) >find_bind |
---|
275 | #EQfind |
---|
276 | change with (? = trans ? (opt_safe ???)) |
---|
277 | @opt_safe_elim #ifn' #EQfind' |
---|
278 | >EQfind' in EQfind; >m_return_bind whd in ⊢ (??%?→?); #EQ destruct(EQ) % |
---|
279 | qed. |
---|