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 | generalize in match (? : False); * |
---|
55 | qed. |
---|
56 | |
---|
57 | definition funct_of_block : ∀F,ge. |
---|
58 | block → option (Σi.is_function F ge i) ≝ |
---|
59 | λF,ge,bl. |
---|
60 | match find_funct_ptr … ge bl |
---|
61 | return λx.find_funct_ptr … ge bl = x → ? with |
---|
62 | [ Some fd ⇒ λprf.return mk_Sig |
---|
63 | ident (λi.is_function F ge i) |
---|
64 | (symbol_of_function_block … ge bl ?) |
---|
65 | (ex_intro … fd ?) |
---|
66 | | None ⇒ λ_.None ? |
---|
67 | ] (refl …). |
---|
68 | [ >(symbol_of_block_rev … (symbol_of_function_block_ok ? ge bl ?)) @prf |
---|
69 | | >prf % #ABS destruct(ABS) |
---|
70 | ] |
---|
71 | qed. |
---|
72 | |
---|
73 | definition block_of_funct ≝ λF,ge. |
---|
74 | λi : Σi.is_function F ge i. |
---|
75 | match find_symbol … ge i return λx.(∃fd.!bl ← x; ? = ?) → ? with |
---|
76 | [ Some bl ⇒ λ_.bl |
---|
77 | | None ⇒ λprf.⊥ |
---|
78 | ] (pi2 … i). |
---|
79 | cases prf #fd normalize #ABS destruct(ABS) |
---|
80 | qed. |
---|
81 | |
---|
82 | definition description_of_function : ∀F,ge.(Σi.is_function F ge i) → F ≝ |
---|
83 | λF,ge,i. |
---|
84 | match ! bl ← find_symbol … ge i ; |
---|
85 | find_funct_ptr … ge bl |
---|
86 | return λx.(∃fd.x = ?) → ? |
---|
87 | with |
---|
88 | [ Some fd ⇒ λ_.fd |
---|
89 | | None ⇒ λprf.⊥ |
---|
90 | ] (pi2 … i). |
---|
91 | cases prf #fd #ABS destruct |
---|
92 | qed. |
---|
93 | |
---|
94 | definition is_internal_function ≝ λF.λge : genv_t (fundef F). |
---|
95 | λi : ident.∃fd. |
---|
96 | ! bl ← find_symbol … ge i ; |
---|
97 | find_funct_ptr … ge bl = Some ? (Internal ? fd). |
---|
98 | |
---|
99 | lemma description_of_internal_function : ∀F,ge,i,fn. |
---|
100 | description_of_function ? ge i = Internal F fn → is_internal_function … ge i. |
---|
101 | #F #ge * #i * #fd #EQ |
---|
102 | #fn whd in ⊢ (??%?→?); >EQ normalize nodelta #EQ' >EQ' in EQ; #EQ |
---|
103 | %{EQ} |
---|
104 | qed. |
---|
105 | |
---|
106 | definition int_funct_of_block : ∀F,ge. |
---|
107 | block → option (Σi.is_internal_function F ge i) ≝ |
---|
108 | λF,ge,bl. |
---|
109 | ! f ← funct_of_block … ge bl ; |
---|
110 | match ? |
---|
111 | return λx.description_of_function … f = x → option (Σi.is_internal_function … ge i) |
---|
112 | with |
---|
113 | [ Internal fn ⇒ λprf.return «pi1 … f, ?» |
---|
114 | | External fn ⇒ λ_.None ? |
---|
115 | ] (refl …). |
---|
116 | @(description_of_internal_function … prf) |
---|
117 | qed. |
---|
118 | |
---|
119 | lemma internal_function_is_function : ∀F,ge,i. |
---|
120 | is_internal_function F ge i → is_function … ge i. |
---|
121 | #F #ge #i * #fn #prf %{prf} qed. |
---|
122 | |
---|
123 | definition if_of_function : ∀F,ge.(Σi.is_internal_function F ge i) → F ≝ |
---|
124 | λF,ge,i. |
---|
125 | match ! bl ← find_symbol … ge i ; |
---|
126 | find_funct_ptr … ge bl |
---|
127 | return λx.(∃fn.x = ?) → ? |
---|
128 | with |
---|
129 | [ Some fd ⇒ |
---|
130 | match fd return λx.(∃fn.Some ? x = ?) → ? with |
---|
131 | [ Internal fn ⇒ λ_.fn |
---|
132 | | External _ ⇒ λprf.⊥ |
---|
133 | ] |
---|
134 | | None ⇒ λprf.⊥ |
---|
135 | ] (pi2 … i). |
---|
136 | cases prf #fn #ABS destruct |
---|
137 | qed. |
---|
138 | |
---|
139 | lemma is_internal_function_of_program_ok : |
---|
140 | ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.∀i. |
---|
141 | is_internal_function … (globalenv ?? init prog) i → |
---|
142 | is_internal_function_of_program ?? prog i. |
---|
143 | #A #B #init #prog #i whd in ⊢ (%→%); * #ifn |
---|
144 | lapply (refl … (find_symbol … i)) |
---|
145 | [3: elim (find_symbol … i) in ⊢ (???%→%); |
---|
146 | [#_ #ABS normalize in ABS; destruct(ABS)] |
---|
147 | |*:] |
---|
148 | #bl #EQbl >m_return_bind #EQfind %{ifn} |
---|
149 | @(find_funct_ptr_symbol_inversion … EQbl EQfind) |
---|
150 | qed. |
---|
151 | |
---|
152 | lemma ok_is_internal_function_of_program : |
---|
153 | ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.∀i. |
---|
154 | is_internal_function_of_program … prog i → |
---|
155 | is_internal_function ? (globalenv ?? init prog) i. |
---|
156 | #A #B #init #prog #i whd in ⊢ (%→%); * #ifn #H |
---|
157 | elim (find_funct_ptr_exists … init … H) |
---|
158 | #bl * #EQ1 #EQ2 %{ifn} >EQ1 @EQ2 qed. |
---|
159 | |
---|
160 | lemma Exists_find : ∀A,B,P,f,l.(∀x.P x → f x ≠ None ?) → Exists ? P l → |
---|
161 | find A B f l ≠ None ?. |
---|
162 | #A #B #P #f #l #H elim l -l [ * ] normalize |
---|
163 | #hd #tl #IH * |
---|
164 | [ #Phd >(opt_to_opt_safe … (H … Phd)) normalize nodelta % #ABS destruct(ABS) |
---|
165 | | #Ptl elim (f hd) |
---|
166 | [ @(IH Ptl) |
---|
167 | | #x % normalize #ABS destruct(ABS) |
---|
168 | ] |
---|
169 | ] |
---|
170 | qed. |
---|
171 | |
---|
172 | definition prog_if_of_function : |
---|
173 | ∀F,V,prog. |
---|
174 | (Σi.is_internal_function_of_program F V prog i) → F ? ≝ |
---|
175 | λF,V,prog,i.opt_safe ? (find ?? |
---|
176 | (λpr.if eq_identifier ? (\fst pr) i then |
---|
177 | match \snd pr with |
---|
178 | [ Internal x ⇒ return x |
---|
179 | | External _ ⇒ None ? |
---|
180 | ] |
---|
181 | else None ?) |
---|
182 | (prog_funct … prog)) ?. |
---|
183 | @hide_prf |
---|
184 | cases i -i #i * #ifn #prf |
---|
185 | @(Exists_find … prf) |
---|
186 | * #i' #fn' #EQ destruct(EQ) >eq_identifier_refl normalize nodelta |
---|
187 | % normalize in ⊢ (??%?→?); #ABS destruct(ABS) |
---|
188 | qed. |
---|
189 | |
---|
190 | definition if_in_global_env_to_if_in_prog : |
---|
191 | ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B. |
---|
192 | (Σi.is_internal_function ? (globalenv ?? init prog) i) → |
---|
193 | Σi.is_internal_function_of_program ?? prog i ≝ |
---|
194 | λA,B,init,prog,f.«f, is_internal_function_of_program_ok … (pi2 … f)». |
---|
195 | |
---|
196 | lemma if_propagate : |
---|
197 | ∀A_in,A_out,B. |
---|
198 | ∀trans. |
---|
199 | ∀prog_in : program (λvars.fundef (A_in vars)) B. |
---|
200 | let prog_out : program (λvars.fundef (A_out vars)) B ≝ |
---|
201 | transform_program … prog_in (λvars.transf_fundef … (trans vars)) in |
---|
202 | ∀i.is_internal_function_of_program … prog_in i → |
---|
203 | is_internal_function_of_program … prog_out i. |
---|
204 | #A_in #A_out #B #trans #prog_in #ident |
---|
205 | * #ifn #H %{(trans … ifn)} |
---|
206 | @(Exists_map … H) * #id #fn #EQ destruct(EQ) % qed. |
---|
207 | |
---|
208 | lemma block_of_funct_ident_is_code : ∀F,ge,i. |
---|
209 | block_region (block_of_funct F ge i) = Code. |
---|
210 | #F #ge * #i * #fd |
---|
211 | whd in ⊢ (?→??(?%)?); |
---|
212 | cases (find_symbol ???) |
---|
213 | [ #ABS normalize in ABS; destruct(ABS) ] |
---|
214 | #bl normalize nodelta >m_return_bind |
---|
215 | whd in ⊢ (??%?→?); cases (block_region bl) |
---|
216 | [ #ABS normalize in ABS; destruct(ABS) ] |
---|
217 | #_ % |
---|
218 | qed. |
---|
219 | |
---|
220 | |
---|
221 | 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. |
---|
222 | #A #B #C #f #g #l elim l -l [%] #hd #tl #IH normalize >IH % qed. |
---|
223 | |
---|
224 | lemma find_bind : ∀A,B,C,f,g,l. |
---|
225 | find A C (λx.! y ← f x ; return g y) l = ! y ← find A B f l ; return g y. |
---|
226 | #A #B #C #f #g #l elim l -l |
---|
227 | [%] |
---|
228 | #hd #tl #IH |
---|
229 | whd in match (find ??? (hd::tl)) in ⊢ (??%%); |
---|
230 | cases (f hd) [ @IH ] #x % qed. |
---|
231 | |
---|
232 | lemma find_ext_eq : ∀A,B,f,g,l.(∀x.f x = g x) → find A B f l = find A B g l. |
---|
233 | #A #B #f #g #l #H elim l -l [%] #hd #tl #IH normalize >H >IH % qed. |
---|
234 | |
---|
235 | lemma prog_if_of_function_transform : |
---|
236 | ∀A,B,V,trans.∀prog_in : program (λvars.fundef (A vars)) V. |
---|
237 | let prog_out : program (λvars.fundef (B vars)) V≝ |
---|
238 | transform_program … prog_in (λvars.transf_fundef … (trans vars)) in |
---|
239 | ∀i1,i2.pi1 ?? i1 = pi1 ?? i2 → |
---|
240 | prog_if_of_function ?? prog_out i1 = trans … (prog_if_of_function ?? prog_in i2). |
---|
241 | #A #B #V #trans #prog * #i1 #i_prf1 * #i #i_prf2 #EQ |
---|
242 | change with (opt_safe ??? = ?) |
---|
243 | @opt_safe_elim #ifn >find_map |
---|
244 | cut (∀vars.∀x. |
---|
245 | if eq_identifier ? (\fst x) i1 then |
---|
246 | match transf_fundef … (trans vars) (\snd x) with |
---|
247 | [ Internal x ⇒ return x |
---|
248 | | _ ⇒ None ? |
---|
249 | ] else None ? = |
---|
250 | ! y ← if eq_identifier ? (\fst x) i1 then |
---|
251 | match \snd x with |
---|
252 | [ Internal x ⇒ return x |
---|
253 | | _ ⇒ None ? |
---|
254 | ] else None ? ; |
---|
255 | return trans vars y) |
---|
256 | [ #vars * #id * #fn whd in match transf_fundef; normalize nodelta |
---|
257 | cases (eq_identifier ???) % ] #H |
---|
258 | >(find_ext_eq … (H ?)) >find_bind |
---|
259 | #EQfind |
---|
260 | change with (? = trans ? (opt_safe ???)) |
---|
261 | @opt_safe_elim #ifn' #EQfind' destruct(EQ) |
---|
262 | >EQfind' in EQfind; >m_return_bind whd in ⊢ (??%?→?); #EQ destruct(EQ) % |
---|
263 | qed. |
---|