Changeset 2478


Ignore:
Timestamp:
Nov 20, 2012, 2:28:06 PM (7 years ago)
Author:
tranquil
Message:

unified is_internal_function_of_program and is_internal_function

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/extraGlobalenvs.ma

    r2476 r2478  
    22include "common/Globalenvs.ma".
    33
    4 (* TODO: need this for global env *)
     4(*
    55axiom find_funct_ptr_symbol_inversion:
    66    ∀F,V,init. ∀p: program F V.
     
    2121    In ? (prog_vars ?? p) 〈〈id, r〉, v〉 →
    2222    ∃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*)
    2724
    2825definition is_function ≝ λF.λge : genv_t F.
     
    3027    ! bl ← find_symbol … ge i ;
    3128    find_funct_ptr … ge bl = Some ? fd.
     29
     30definition 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
     35definition 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.
    3238
    3339definition funct_of_ident : ∀F,ge.
     
    9298qed.
    9399
    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 
    99100lemma description_of_internal_function : ∀F,ge,i,fn.
    100101  description_of_function ? ge i = Internal F fn → is_internal_function … ge i.
     
    137138qed.
    138139
    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 
    196140lemma if_propagate :
    197 ∀A_in,A_out,B.
     141∀A_in,A_out.
    198142∀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)) .
     144let prog_out : program (λvars.fundef (A_out vars))
    201145  transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
    202146∀i.is_internal_function_of_program … prog_in i →
    203147is_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
     150inversion (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) %
     155qed.
    207156
    208157lemma block_of_funct_ident_is_code : ∀F,ge,i.
     
    218167qed.
    219168
    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 
    235169lemma 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))
    238172    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)
     178cut (∀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
     184whd in ⊢ (??%?); @aux
     185[2: #prf #EQ generalize in match (? : False); * ]
     186#fd * #ifn #EQ1 #EQ destruct normalize nodelta
     187whd in ⊢ (???(??%)); @aux
     188[2: #prf #EQ generalize in match (? : False); * ]
     189#fd' * #ifn' #EQ1' #EQ' destruct normalize nodelta
     190inversion (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 %
    263194qed.
Note: See TracChangeset for help on using the changeset viewer.