[2473] | 1 | include "common/AST.ma". |
---|
| 2 | include "common/Globalenvs.ma". |
---|
| 3 | |
---|
[2478] | 4 | (* |
---|
[2473] | 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_function ≝ λF.λge : genv_t F. |
---|
| 25 | λi : ident.∃fd. |
---|
| 26 | ! bl ← find_symbol … ge i ; |
---|
| 27 | find_funct_ptr … ge bl = Some ? fd. |
---|
| 28 | |
---|
[2478] | 29 | definition is_internal_function ≝ λF.λge : genv_t (fundef F). |
---|
| 30 | λi : ident.∃fd. |
---|
| 31 | ! bl ← find_symbol … ge i ; |
---|
| 32 | find_funct_ptr … ge bl = Some ? (Internal ? fd). |
---|
| 33 | |
---|
| 34 | definition is_internal_function_of_program : |
---|
| 35 | ∀A.program (λvars.fundef (A vars)) ℕ → ident → Prop ≝ |
---|
| 36 | λA,prog,i.is_internal_function … (globalenv_noinit … prog) i. |
---|
| 37 | |
---|
[2473] | 38 | definition funct_of_ident : ∀F,ge. |
---|
| 39 | ident → option (Σi.is_function F ge i) |
---|
| 40 | ≝ λF,ge,i. |
---|
| 41 | match ? |
---|
| 42 | return λx.! bl ← find_symbol … ge i ; |
---|
| 43 | find_funct_ptr … ge bl = x → ? |
---|
| 44 | with |
---|
| 45 | [ Some fd ⇒ λprf.return «i, ex_intro ?? fd prf» |
---|
| 46 | | None ⇒ λ_.None ? |
---|
| 47 | ] (refl …). |
---|
[2590] | 48 | *) |
---|
[2473] | 49 | |
---|
| 50 | lemma symbol_of_function_block_ok : |
---|
| 51 | ∀F,ge,b,prf.symbol_for_block F ge b = Some ? (symbol_of_function_block F ge b prf). |
---|
| 52 | #F #ge #b #FFP |
---|
| 53 | cut (∀A,B : Type[0].∀P : B → Prop.∀x : option A.∀c1,c2. |
---|
| 54 | (∀v.∀prf : x = Some ? v.P (c1 v prf)) → |
---|
| 55 | (∀prf:x = None ?.P (c2 prf)) → |
---|
| 56 | P (match x return λy.x = y → ? with |
---|
| 57 | [ Some v ⇒ λprf.c1 v prf | None ⇒ λprf.c2 prf] |
---|
| 58 | (refl …))) [ #A #B #P * // ] #aux |
---|
[2474] | 59 | whd in ⊢ (???(??%)); @aux [//] #H |
---|
| 60 | generalize in match (? : False); * |
---|
| 61 | qed. |
---|
[2473] | 62 | |
---|
[2590] | 63 | (* |
---|
[2473] | 64 | definition funct_of_block : ∀F,ge. |
---|
| 65 | block → option (Σi.is_function F ge i) ≝ |
---|
| 66 | λF,ge,bl. |
---|
| 67 | match find_funct_ptr … ge bl |
---|
| 68 | return λx.find_funct_ptr … ge bl = x → ? with |
---|
| 69 | [ Some fd ⇒ λprf.return mk_Sig |
---|
| 70 | ident (λi.is_function F ge i) |
---|
| 71 | (symbol_of_function_block … ge bl ?) |
---|
| 72 | (ex_intro … fd ?) |
---|
| 73 | | None ⇒ λ_.None ? |
---|
| 74 | ] (refl …). |
---|
| 75 | [ >(symbol_of_block_rev … (symbol_of_function_block_ok ? ge bl ?)) @prf |
---|
| 76 | | >prf % #ABS destruct(ABS) |
---|
| 77 | ] |
---|
| 78 | qed. |
---|
| 79 | |
---|
| 80 | definition block_of_funct ≝ λF,ge. |
---|
| 81 | λi : Σi.is_function F ge i. |
---|
| 82 | match find_symbol … ge i return λx.(∃fd.!bl ← x; ? = ?) → ? with |
---|
| 83 | [ Some bl ⇒ λ_.bl |
---|
| 84 | | None ⇒ λprf.⊥ |
---|
| 85 | ] (pi2 … i). |
---|
| 86 | cases prf #fd normalize #ABS destruct(ABS) |
---|
| 87 | qed. |
---|
| 88 | |
---|
| 89 | definition description_of_function : ∀F,ge.(Σi.is_function F ge i) → F ≝ |
---|
| 90 | λF,ge,i. |
---|
| 91 | match ! bl ← find_symbol … ge i ; |
---|
| 92 | find_funct_ptr … ge bl |
---|
| 93 | return λx.(∃fd.x = ?) → ? |
---|
| 94 | with |
---|
| 95 | [ Some fd ⇒ λ_.fd |
---|
| 96 | | None ⇒ λprf.⊥ |
---|
| 97 | ] (pi2 … i). |
---|
| 98 | cases prf #fd #ABS destruct |
---|
| 99 | qed. |
---|
| 100 | |
---|
| 101 | lemma description_of_internal_function : ∀F,ge,i,fn. |
---|
| 102 | description_of_function ? ge i = Internal F fn → is_internal_function … ge i. |
---|
| 103 | #F #ge * #i * #fd #EQ |
---|
| 104 | #fn whd in ⊢ (??%?→?); >EQ normalize nodelta #EQ' >EQ' in EQ; #EQ |
---|
| 105 | %{EQ} |
---|
| 106 | qed. |
---|
| 107 | |
---|
| 108 | definition int_funct_of_block : ∀F,ge. |
---|
| 109 | block → option (Σi.is_internal_function F ge i) ≝ |
---|
| 110 | λF,ge,bl. |
---|
| 111 | ! f ← funct_of_block … ge bl ; |
---|
| 112 | match ? |
---|
| 113 | return λx.description_of_function … f = x → option (Σi.is_internal_function … ge i) |
---|
| 114 | with |
---|
| 115 | [ Internal fn ⇒ λprf.return «pi1 … f, ?» |
---|
| 116 | | External fn ⇒ λ_.None ? |
---|
| 117 | ] (refl …). |
---|
| 118 | @(description_of_internal_function … prf) |
---|
| 119 | qed. |
---|
| 120 | |
---|
| 121 | lemma internal_function_is_function : ∀F,ge,i. |
---|
| 122 | is_internal_function F ge i → is_function … ge i. |
---|
| 123 | #F #ge #i * #fn #prf %{prf} qed. |
---|
| 124 | |
---|
| 125 | definition if_of_function : ∀F,ge.(Σi.is_internal_function F ge i) → F ≝ |
---|
| 126 | λF,ge,i. |
---|
| 127 | match ! bl ← find_symbol … ge i ; |
---|
| 128 | find_funct_ptr … ge bl |
---|
| 129 | return λx.(∃fn.x = ?) → ? |
---|
| 130 | with |
---|
| 131 | [ Some fd ⇒ |
---|
| 132 | match fd return λx.(∃fn.Some ? x = ?) → ? with |
---|
| 133 | [ Internal fn ⇒ λ_.fn |
---|
| 134 | | External _ ⇒ λprf.⊥ |
---|
| 135 | ] |
---|
| 136 | | None ⇒ λprf.⊥ |
---|
| 137 | ] (pi2 … i). |
---|
| 138 | cases prf #fn #ABS destruct |
---|
| 139 | qed. |
---|
| 140 | |
---|
| 141 | lemma if_propagate : |
---|
[2478] | 142 | ∀A_in,A_out. |
---|
[2473] | 143 | ∀trans. |
---|
[2478] | 144 | ∀prog_in : program (λvars.fundef (A_in vars)) ℕ. |
---|
| 145 | let prog_out : program (λvars.fundef (A_out vars)) ℕ ≝ |
---|
[2473] | 146 | transform_program … prog_in (λvars.transf_fundef … (trans vars)) in |
---|
| 147 | ∀i.is_internal_function_of_program … prog_in i → |
---|
| 148 | is_internal_function_of_program … prog_out i. |
---|
[2478] | 149 | #A_in #A_out #trans #prog_in #ident |
---|
| 150 | * #ifn |
---|
| 151 | inversion (find_symbol ???) [ #_ #ABS whd in ABS : (??%%); destruct(ABS) ] |
---|
| 152 | #bl #EQfind >m_return_bind #EQfunct_ptr |
---|
| 153 | %{(trans … ifn)} |
---|
| 154 | >find_symbol_transf >EQfind >m_return_bind |
---|
| 155 | >(find_funct_ptr_transf … EQfunct_ptr) % |
---|
| 156 | qed. |
---|
[2473] | 157 | |
---|
| 158 | lemma block_of_funct_ident_is_code : ∀F,ge,i. |
---|
| 159 | block_region (block_of_funct F ge i) = Code. |
---|
| 160 | #F #ge * #i * #fd |
---|
| 161 | whd in ⊢ (?→??(?%)?); |
---|
| 162 | cases (find_symbol ???) |
---|
| 163 | [ #ABS normalize in ABS; destruct(ABS) ] |
---|
| 164 | #bl normalize nodelta >m_return_bind |
---|
| 165 | whd in ⊢ (??%?→?); cases (block_region bl) |
---|
| 166 | [ #ABS normalize in ABS; destruct(ABS) ] |
---|
| 167 | #_ % |
---|
| 168 | qed. |
---|
| 169 | |
---|
| 170 | lemma prog_if_of_function_transform : |
---|
[2478] | 171 | ∀A,B,trans.∀prog_in : program (λvars.fundef (A vars)) ℕ. |
---|
| 172 | let prog_out : program (λvars.fundef (B vars)) ℕ ≝ |
---|
[2473] | 173 | transform_program … prog_in (λvars.transf_fundef … (trans vars)) in |
---|
[2478] | 174 | ∀i_out : Σi.is_internal_function_of_program … prog_out i. |
---|
| 175 | ∀i_in : Σi.is_internal_function_of_program … prog_in i. |
---|
| 176 | pi1 … i_out = pi1 … i_in → |
---|
| 177 | if_of_function … i_out = trans … (if_of_function … i_in). |
---|
| 178 | #A #B #trans #prog * #i1 #i_prf1 * #i2 #i_prf2 #EQ destruct(EQ) |
---|
| 179 | cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop. |
---|
| 180 | ∀m.∀prf : Q m.∀f1,f2. |
---|
| 181 | (∀x,prf.m = Some ? x → P (f1 x prf)) → |
---|
| 182 | (∀prf.m = None ? → P (f2 prf)) → |
---|
| 183 | P (match m return λx.Q x → ? with [ Some x ⇒ f1 x | None ⇒ f2 ] prf)) |
---|
| 184 | [ #A #B #Q #P * /2 by / ] #aux |
---|
| 185 | whd in ⊢ (??%?); @aux |
---|
| 186 | [2: #prf #EQ generalize in match (? : False); * ] |
---|
| 187 | #fd * #ifn #EQ1 #EQ destruct normalize nodelta |
---|
| 188 | whd in ⊢ (???(??%)); @aux |
---|
| 189 | [2: #prf #EQ generalize in match (? : False); * ] |
---|
| 190 | #fd' * #ifn' #EQ1' #EQ' destruct normalize nodelta |
---|
| 191 | inversion (find_symbol ???) in EQ'; [ #_ #ABS whd in ABS: (??%%); destruct ] |
---|
| 192 | #bl #EQfind >m_return_bind #EQfunct |
---|
| 193 | >find_symbol_transf in EQ; >EQfind >m_return_bind |
---|
| 194 | >(find_funct_ptr_transf … EQfunct) #EQ'' destruct % |
---|
[2570] | 195 | qed. |
---|
[2590] | 196 | *) |
---|
[2570] | 197 | |
---|
| 198 | include alias "common/PositiveMap.ma". |
---|
| 199 | |
---|
| 200 | lemma add_functs_functions_miss : ∀F. ∀ge : genv_t F.∀ l.∀ id. |
---|
| 201 | id < (nextfunction ? ge) → |
---|
| 202 | lookup_opt … id (functions ? ge) = None ? → |
---|
| 203 | lookup_opt … id (functions … (add_functs F ge l)) = None ?. |
---|
| 204 | #F #ge #l #id whd in match add_functs; normalize nodelta |
---|
| 205 | elim l -l [ #_ normalize //] |
---|
| 206 | * #id1 #f1 #tl #IND #H #H1 whd in match (foldr ?????); |
---|
| 207 | >lookup_opt_insert_miss [ inversion(lookup_opt ? ? ?) [ #_ %] |
---|
| 208 | #f1 #H3 <(drop_fn_lfn … f1 H3) @(IND H H1) |
---|
| 209 | | cut(nextfunction F ge ≤ nextfunction F (foldr … (add_funct F) ge tl)) |
---|
| 210 | [elim tl [normalize //] |
---|
| 211 | #x #tl2 whd in match (foldr ?????) in ⊢ (? → %); #H %2{H} ] |
---|
| 212 | #H2 lapply(transitive_le … H H2) @lt_to_not_eq |
---|
| 213 | qed. |
---|
| 214 | |
---|
| 215 | lemma add_globals_functions_miss : ∀F,V,init. ∀gem : genv_t F × mem.∀ id,l. |
---|
| 216 | lookup_opt … id (functions ? (\fst gem)) = None ? → |
---|
| 217 | lookup_opt … id (functions … (\fst (add_globals F V init gem l))) = None ?. |
---|
| 218 | #F #V #init * #ge #m #id #l lapply ge -ge lapply m -m elim l [ #ge #m #H @H] |
---|
| 219 | ** #x1 #x2 #x3 #tl whd in match add_globals; |
---|
| 220 | normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta |
---|
[2608] | 221 | cases(alloc m ? ? (*x2*)) #m1 #bl1 normalize nodelta @IND whd in match add_symbol; |
---|
[2570] | 222 | normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %] |
---|
| 223 | #f1 #H3 <(drop_fn_lfn … f1 H3) assumption |
---|
| 224 | qed. |
---|
| 225 | |
---|
| 226 | |
---|
| 227 | lemma globalenv_no_minus_one : |
---|
| 228 | ∀F,V,i,p. |
---|
[2608] | 229 | find_funct_ptr … (globalenv F V i p) (mk_block (*Code*) (-1)) = None ?. |
---|
[2570] | 230 | #F #V #i #p |
---|
| 231 | whd in match find_funct_ptr; normalize nodelta |
---|
| 232 | whd in match globalenv; |
---|
| 233 | whd in match globalenv_allocmem; normalize nodelta |
---|
| 234 | @add_globals_functions_miss @add_functs_functions_miss normalize // |
---|
| 235 | qed. |
---|
| 236 | |
---|
[2590] | 237 | lemma globalenv_no_zero : |
---|
| 238 | ∀F,V,i,p. |
---|
[2608] | 239 | find_funct_ptr … (globalenv F V i p) (mk_block (*Code*) OZ) = None ?. // |
---|
[2590] | 240 | qed. |
---|
[2570] | 241 | |
---|
[2783] | 242 | lemma symbol_for_block_match: |
---|
| 243 | ∀M:matching.∀initV,initW. |
---|
| 244 | (∀v,w. match_var_entry M v w → |
---|
| 245 | size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → |
---|
| 246 | ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). |
---|
| 247 | ∀MATCH:match_program … M p p'. |
---|
| 248 | ∀b: block. |
---|
| 249 | symbol_for_block … (globalenv … initW p') b = |
---|
| 250 | symbol_for_block … (globalenv … initV p) b. |
---|
| 251 | * #A #B #V #W #match_fn #match_var #initV #initW #H |
---|
| 252 | #p #p' * #Mvars #Mfn #Mmain |
---|
| 253 | #b |
---|
| 254 | whd in match symbol_for_block; normalize nodelta |
---|
| 255 | whd in match globalenv in ⊢ (???%); normalize nodelta |
---|
| 256 | whd in match (globalenv_allocmem ????); |
---|
| 257 | change with (add_globals ?????) in match (foldl ?????); |
---|
| 258 | >(proj1 … (add_globals_match … initW … Mvars)) |
---|
| 259 | [ % |*:] |
---|
| 260 | [ * #idr #v * #idr' #w #MVE % |
---|
| 261 | [ inversion MVE |
---|
| 262 | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % |
---|
| 263 | | @(H … MVE) |
---|
| 264 | ] |
---|
| 265 | | @(matching_fns_get_same_blocks … Mfn) |
---|
| 266 | #f #g @match_funct_entry_id |
---|
| 267 | ] |
---|
| 268 | qed. |
---|
| 269 | |
---|
| 270 | lemma symbol_for_block_transf : |
---|
| 271 | ∀A,B,V,init.∀prog_in : program A V. |
---|
| 272 | ∀trans : ∀vars.A vars → B vars. |
---|
| 273 | let prog_out ≝ transform_program … prog_in trans in |
---|
| 274 | ∀bl. |
---|
| 275 | symbol_for_block … (globalenv … init prog_out) bl = |
---|
| 276 | symbol_for_block … (globalenv … init prog_in) bl. |
---|
| 277 | #A #B #V #iV #p #tf @(symbol_for_block_match … (transform_program_match … tf ?)) |
---|
| 278 | #v0 #w0 * // |
---|
| 279 | qed. |
---|
| 280 | |
---|
| 281 | lemma vars_irrelevant_to_find_funct_ptr_inv : |
---|
| 282 | ∀F,G,V,W. |
---|
| 283 | ∀P:F → G → Prop. |
---|
| 284 | ∀init,init',b,vars,vars',ge,ge',m,m',f. |
---|
| 285 | (find_funct_ptr G ge' b = Some ? f → ∃f'. find_funct_ptr F ge b = Some ? f' ∧ P f' f) → |
---|
| 286 | symbols F ge = symbols G ge' → |
---|
| 287 | nextblock m = nextblock m' → |
---|
| 288 | All2 … (λx,y. \fst x = \fst y) vars vars' → |
---|
| 289 | find_funct_ptr G (\fst (add_globals G W init' 〈ge',m'〉 vars')) b = Some ? f → |
---|
| 290 | ∃f'.find_funct_ptr F (\fst (add_globals F V init 〈ge,m〉 vars)) b = Some ? f' ∧ P f' f. |
---|
| 291 | #F #G #V #W #P #init #init' |
---|
| 292 | * * [ 2,3(*,5,6*): #blk ] [ 2: | 1,3: #vars #vars' #ge #ge' #m #m' #f #H1 #H2 #H3 #H4 #H5 whd in H5:(??%?); destruct ] |
---|
| 293 | #vars elim vars |
---|
| 294 | [ * [ #ge #ge' #m #m' #f #H #_ #_ #_ @H |
---|
| 295 | | #x #tl #ge #ge' #m #m' #f #_ #_ #_ * |
---|
| 296 | ] |
---|
| 297 | | * * #id #r #v #tl #IH * |
---|
| 298 | [ #ge #ge' #m #m' #f #_ #_ #_ * |
---|
| 299 | | * * #id' #r' #v' #tl' |
---|
| 300 | #ge #ge' #m #m' #f #FFP1 #Esym #Enext * #E destruct #MATCH |
---|
| 301 | whd in match (add_globals ?????); whd in match (add_globals F ????); |
---|
| 302 | whd in ⊢ (??(??(???(????%?))?)? → ??(λ_.?(??(??(???(????%?))?)?)?)); |
---|
| 303 | @(alloc_pair … Enext) #m1 #m2 #b #Enext' |
---|
| 304 | whd in ⊢ (??(??(???(????%?))?)? → ??(λ_.?(??(??(???(????%?))?)?)?)); |
---|
| 305 | #FFP |
---|
| 306 | @(IH … MATCH FFP) |
---|
| 307 | [ whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
| 308 | whd in ⊢ (??(???%)? → ??(λ_.?(??(???%)?)?)); |
---|
| 309 | >Esym |
---|
| 310 | cases ( lookup SymbolTag block (symbols G ge') id') |
---|
| 311 | [ @FFP1 |
---|
| 312 | | * * (* * *) try @FFP1 #p try @FFP1 |
---|
| 313 | normalize |
---|
| 314 | cases (decidable_eq_pos blk p) |
---|
| 315 | [ #E destruct >lookup_opt_pm_set_hit #E destruct |
---|
| 316 | | #NE >(lookup_opt_pm_set_miss … NE) >(lookup_opt_pm_set_miss … NE) |
---|
| 317 | @FFP1 |
---|
| 318 | ] |
---|
| 319 | ] |
---|
| 320 | | whd in match (add_symbol ????); whd in match (drop_fn ???); |
---|
| 321 | whd in match (add_symbol ????); whd in match (drop_fn ???); |
---|
| 322 | >Esym % |
---|
| 323 | | assumption |
---|
| 324 | ] |
---|
| 325 | ] |
---|
| 326 | ] qed. |
---|
| 327 | |
---|
| 328 | lemma All2_swap : ∀ A,B,P,l1,l2. All2 A B P l1 l2 → |
---|
| 329 | All2 B A (λx,y.P y x) l2 l1. |
---|
| 330 | #A #B #P #l1 elim l1 [* [ #_ @I] #b #tlb *] |
---|
| 331 | #a #tl_a #IH * [ *] #b #tl_b * #H #H1 whd % [assumption] |
---|
| 332 | @IH assumption |
---|
| 333 | qed. |
---|
| 334 | |
---|
| 335 | lemma find_funct_ptr_All2_inv : ∀A,B,V,W,b,p. |
---|
| 336 | ∀initV,initW,p',P.∀f : B (prog_var_names B W p'). |
---|
| 337 | All2 ?? (λx,y. \fst x = \fst y ∧ P (\snd x) (\snd y)) (prog_funct ?? p) (prog_funct … p') → |
---|
| 338 | All2 … (λx,y. \fst x = \fst y) (prog_vars ?? p) (prog_vars ?? p') → |
---|
| 339 | find_funct_ptr … (globalenv B W initW p') b = Some ? f → |
---|
| 340 | ∃f'. find_funct_ptr … (globalenv A V initV p) b = Some ? f' ∧ P f' f. |
---|
| 341 | #A #B #V #W #b * #vars #fns #main #initV #initW * #vars' #fns' #main' #P #f |
---|
| 342 | #Mfns |
---|
| 343 | cases b * (* * *) [ 2,3 (*,5,6*) (*,8,9,11,12,14,15,17,18*): #bp ] |
---|
| 344 | [ 2: (*12:*) | *: #_ #F whd in F:(??%?); destruct ] |
---|
| 345 | whd in match (globalenv ????); whd in match (globalenv_allocmem ????); |
---|
| 346 | whd in match (globalenv ????); whd in match (globalenv_allocmem ????); |
---|
| 347 | @vars_irrelevant_to_find_funct_ptr_inv |
---|
| 348 | [ letin varnames ≝ (map ??? vars) |
---|
| 349 | generalize in match fns in Mfns ⊢ %; |
---|
| 350 | elim fns' |
---|
| 351 | [ #fns #Mfns whd in ⊢ (??%? → ?); #E destruct |
---|
| 352 | | * #id #fn #tl #IH * * #id' #fn' #tl' * * #E #Phd destruct #Mtl |
---|
| 353 | whd in ⊢ (??%? → ?); |
---|
| 354 | whd in match (functions ??); |
---|
| 355 | change with (add_functs ???) in match (foldr ?????); |
---|
| 356 | cases (ge_add_functs ?? tl tl' ?) [2: @(All2_mp … (All2_swap … Mtl)) * #idA #a * #idB #b * // ] |
---|
| 357 | #SYMS #NEXT |
---|
| 358 | cases (decidable_eq_pos bp (nextfunction … (add_functs ? (empty ?) tl))) |
---|
| 359 | [ #E destruct >lookup_opt_insert_hit #E destruct |
---|
| 360 | %{fn'} % // whd in ⊢ (??%?); |
---|
| 361 | whd in match (functions ??); |
---|
| 362 | change with (add_functs ???) in match (foldr ???? tl'); |
---|
| 363 | >NEXT >lookup_opt_insert_hit @refl |
---|
| 364 | | #NE >lookup_opt_insert_miss // |
---|
| 365 | #FFP cases (IH tl' Mtl ?) |
---|
| 366 | [ #fn'' * #FFP' #P' %{fn''} % |
---|
| 367 | [ whd in ⊢ (??%?); |
---|
| 368 | >lookup_opt_insert_miss [2: <NEXT // ] |
---|
| 369 | lapply (lookup_drop_fn_different ????? FFP) |
---|
| 370 | >SYMS |
---|
| 371 | #L >lookup_drop_fn_irrelevant // @FFP' |
---|
| 372 | | @P' |
---|
| 373 | ] |
---|
| 374 | | @(drop_fn_lfn … FFP) |
---|
| 375 | ] |
---|
| 376 | ] |
---|
| 377 | ] |
---|
| 378 | | cases (ge_add_functs ?? fns fns' ?) [2: @(All2_mp … Mfns) * #idA #a * #idB #b * // ] |
---|
| 379 | #S #_ @S |
---|
| 380 | | @refl |
---|
| 381 | ] qed. |
---|
| 382 | |
---|
| 383 | lemma find_funct_ptr_match_inv: |
---|
| 384 | ∀M:matching.∀initV,initW. |
---|
| 385 | ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). |
---|
| 386 | ∀MATCH:match_program … M p p'. |
---|
| 387 | ∀b: block. ∀tf: m_B M (prog_var_names … p'). |
---|
| 388 | find_funct_ptr … (globalenv … initW p') b = Some ? tf → |
---|
| 389 | ∃f : m_A M (prog_var_names … p). |
---|
| 390 | find_funct_ptr … (globalenv … initV p) b = Some ? f ∧ |
---|
| 391 | match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉). |
---|
| 392 | [ 2: >(matching_vars … (mp_vars … MATCH)) % ] |
---|
| 393 | * #A #B #V #W #match_fn #match_var #initV #initW |
---|
| 394 | #p #p' * #Mvars #Mfn #Mmain |
---|
| 395 | #b #f #FFP @(find_funct_ptr_All2_inv A B V W ????????? FFP) |
---|
| 396 | [ lapply (matching_vars … (mk_matching A B V W match_fn match_var) … Mvars) |
---|
| 397 | #E |
---|
| 398 | @(All2_mp … Mfn) |
---|
| 399 | * #id #f * #id' #f' |
---|
| 400 | <E in f' ⊢ %; #f' -Mmain -b -Mfn -Mvars -initV -initW -E |
---|
| 401 | normalize #H @(match_funct_entry_inv … H) |
---|
| 402 | #vs #id1 #f1 #f2 #M % // |
---|
| 403 | | @(All2_mp … Mvars) |
---|
| 404 | * #x #x' * #y #y' #M inversion M #id #r #v1 #v2 #M' #E1 #E2 #_ destruct // |
---|
| 405 | qed. |
---|
| 406 | |
---|
| 407 | lemma find_funct_ptr_transf_none : |
---|
| 408 | ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs). |
---|
| 409 | ∀b: block. |
---|
| 410 | find_funct_ptr ? (globalenv … iV p) b = None ? → |
---|
| 411 | find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = None ?. |
---|
| 412 | #A #B #V #iV #p #transf #b #EQf inversion(find_funct_ptr ???) [#_ %] |
---|
| 413 | #tf #EQtf |
---|
| 414 | cases (find_funct_ptr_match_inv … (transform_program_match … transf ?) … EQtf) |
---|
| 415 | [2: @iV] #f * #EQf' #_ >EQf in EQf'; #ABS destruct |
---|
| 416 | qed. |
---|
| 417 | |
---|
| 418 | lemma find_funct_ptr_transf_commute : |
---|
| 419 | ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs). |
---|
| 420 | ∀b: block. |
---|
| 421 | find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = |
---|
| 422 | ! f ← find_funct_ptr ? (globalenv … iV p) b; |
---|
| 423 | return transf … f. |
---|
| 424 | #A #B #V #iV #p #transf #bl inversion(find_funct_ptr ? (globalenv … iV p) bl) |
---|
| 425 | [ #EQ >(find_funct_ptr_transf_none … transf … EQ) %] |
---|
| 426 | #f #EQ >(find_funct_ptr_transf … transf … EQ) % |
---|
| 427 | qed. |
---|
| 428 | |
---|
| 429 | |
---|
| 430 | |
---|
| 431 | |
---|
| 432 | |
---|
| 433 | |
---|