 Timestamp:
 Nov 20, 2012, 2:28:06 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/extraGlobalenvs.ma
r2476 r2478 2 2 include "common/Globalenvs.ma". 3 3 4 (* TODO: need this for global env *)4 (* 5 5 axiom find_funct_ptr_symbol_inversion: 6 6 ∀F,V,init. ∀p: program F V. … … 21 21 In ? (prog_vars ?? p) 〈〈id, r〉, v〉 → 22 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〉. 23 *) 27 24 28 25 definition is_function ≝ λF.λge : genv_t F. … … 30 27 ! bl ← find_symbol … ge i ; 31 28 find_funct_ptr … ge bl = Some ? fd. 29 30 definition is_internal_function ≝ λF.λge : genv_t (fundef F). 31 λi : ident.∃fd. 32 ! bl ← find_symbol … ge i ; 33 find_funct_ptr … ge bl = Some ? (Internal ? fd). 34 35 definition is_internal_function_of_program : 36 ∀A.program (λvars.fundef (A vars)) ℕ → ident → Prop ≝ 37 λA,prog,i.is_internal_function … (globalenv_noinit … prog) i. 32 38 33 39 definition funct_of_ident : ∀F,ge. … … 92 98 qed. 93 99 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 100 lemma description_of_internal_function : ∀F,ge,i,fn. 100 101 description_of_function ? ge i = Internal F fn → is_internal_function … ge i. … … 137 138 qed. 138 139 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 ⊢ (%→%); * #ifn144 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 #H157 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 [ * ] normalize163 #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 then177 match \snd pr with178 [ Internal x ⇒ return x179  External _ ⇒ None ?180 ]181 else None ?)182 (prog_funct … prog)) ?.183 @hide_prf184 cases i i #i * #ifn #prf185 @(Exists_find … prf)186 * #i' #fn' #EQ destruct(EQ) >eq_identifier_refl normalize nodelta187 % 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 140 lemma if_propagate : 197 ∀A_in,A_out ,B.141 ∀A_in,A_out. 198 142 ∀trans. 199 ∀prog_in : program (λvars.fundef (A_in vars)) B.200 let prog_out : program (λvars.fundef (A_out vars)) B≝143 ∀prog_in : program (λvars.fundef (A_in vars)) ℕ. 144 let prog_out : program (λvars.fundef (A_out vars)) ℕ ≝ 201 145 transform_program … prog_in (λvars.transf_fundef … (trans vars)) in 202 146 ∀i.is_internal_function_of_program … prog_in i → 203 147 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. 148 #A_in #A_out #trans #prog_in #ident 149 * #ifn 150 inversion (find_symbol ???) [ #_ #ABS whd in ABS : (??%%); destruct(ABS) ] 151 #bl #EQfind >m_return_bind #EQfunct_ptr 152 %{(trans … ifn)} 153 >find_symbol_transf >EQfind >m_return_bind 154 >(find_funct_ptr_transf … EQfunct_ptr) % 155 qed. 207 156 208 157 lemma block_of_funct_ident_is_code : ∀F,ge,i. … … 218 167 qed. 219 168 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 l227 [%]228 #hd #tl #IH229 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 169 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≝170 ∀A,B,trans.∀prog_in : program (λvars.fundef (A vars)) ℕ. 171 let prog_out : program (λvars.fundef (B vars)) ℕ ≝ 238 172 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) % 173 ∀i_out : Σi.is_internal_function_of_program … prog_out i. 174 ∀i_in : Σi.is_internal_function_of_program … prog_in i. 175 pi1 … i_out = pi1 … i_in → 176 if_of_function … i_out = trans … (if_of_function … i_in). 177 #A #B #trans #prog * #i1 #i_prf1 * #i2 #i_prf2 #EQ destruct(EQ) 178 cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop. 179 ∀m.∀prf : Q m.∀f1,f2. 180 (∀x,prf.m = Some ? x → P (f1 x prf)) → 181 (∀prf.m = None ? → P (f2 prf)) → 182 P (match m return λx.Q x → ? with [ Some x ⇒ f1 x  None ⇒ f2 ] prf)) 183 [ #A #B #Q #P * /2 by / ] #aux 184 whd in ⊢ (??%?); @aux 185 [2: #prf #EQ generalize in match (? : False); * ] 186 #fd * #ifn #EQ1 #EQ destruct normalize nodelta 187 whd in ⊢ (???(??%)); @aux 188 [2: #prf #EQ generalize in match (? : False); * ] 189 #fd' * #ifn' #EQ1' #EQ' destruct normalize nodelta 190 inversion (find_symbol ???) in EQ'; [ #_ #ABS whd in ABS: (??%%); destruct ] 191 #bl #EQfind >m_return_bind #EQfunct 192 >find_symbol_transf in EQ; >EQfind >m_return_bind 193 >(find_funct_ptr_transf … EQfunct) #EQ'' destruct % 263 194 qed.
Note: See TracChangeset
for help on using the changeset viewer.