[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. |
---|
[2478] | 23 | *) |
---|
[2473] | 24 | |
---|
| 25 | definition is_function ≝ λF.λge : genv_t F. |
---|
| 26 | λi : ident.∃fd. |
---|
| 27 | ! bl ← find_symbol … ge i ; |
---|
| 28 | find_funct_ptr … ge bl = Some ? fd. |
---|
| 29 | |
---|
[2478] | 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. |
---|
| 38 | |
---|
[2473] | 39 | definition funct_of_ident : ∀F,ge. |
---|
| 40 | ident → option (Σi.is_function F ge i) |
---|
| 41 | ≝ λF,ge,i. |
---|
| 42 | match ? |
---|
| 43 | return λx.! bl ← find_symbol … ge i ; |
---|
| 44 | find_funct_ptr … ge bl = x → ? |
---|
| 45 | with |
---|
| 46 | [ Some fd ⇒ λprf.return «i, ex_intro ?? fd prf» |
---|
| 47 | | None ⇒ λ_.None ? |
---|
| 48 | ] (refl …). |
---|
| 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 | |
---|
| 63 | definition funct_of_block : ∀F,ge. |
---|
| 64 | block → option (Σi.is_function F ge i) ≝ |
---|
| 65 | λF,ge,bl. |
---|
| 66 | match find_funct_ptr … ge bl |
---|
| 67 | return λx.find_funct_ptr … ge bl = x → ? with |
---|
| 68 | [ Some fd ⇒ λprf.return mk_Sig |
---|
| 69 | ident (λi.is_function F ge i) |
---|
| 70 | (symbol_of_function_block … ge bl ?) |
---|
| 71 | (ex_intro … fd ?) |
---|
| 72 | | None ⇒ λ_.None ? |
---|
| 73 | ] (refl …). |
---|
| 74 | [ >(symbol_of_block_rev … (symbol_of_function_block_ok ? ge bl ?)) @prf |
---|
| 75 | | >prf % #ABS destruct(ABS) |
---|
| 76 | ] |
---|
| 77 | qed. |
---|
| 78 | |
---|
| 79 | definition block_of_funct ≝ λF,ge. |
---|
| 80 | λi : Σi.is_function F ge i. |
---|
| 81 | match find_symbol … ge i return λx.(∃fd.!bl ← x; ? = ?) → ? with |
---|
| 82 | [ Some bl ⇒ λ_.bl |
---|
| 83 | | None ⇒ λprf.⊥ |
---|
| 84 | ] (pi2 … i). |
---|
| 85 | cases prf #fd normalize #ABS destruct(ABS) |
---|
| 86 | qed. |
---|
| 87 | |
---|
| 88 | definition description_of_function : ∀F,ge.(Σi.is_function F ge i) → F ≝ |
---|
| 89 | λF,ge,i. |
---|
| 90 | match ! bl ← find_symbol … ge i ; |
---|
| 91 | find_funct_ptr … ge bl |
---|
| 92 | return λx.(∃fd.x = ?) → ? |
---|
| 93 | with |
---|
| 94 | [ Some fd ⇒ λ_.fd |
---|
| 95 | | None ⇒ λprf.⊥ |
---|
| 96 | ] (pi2 … i). |
---|
| 97 | cases prf #fd #ABS destruct |
---|
| 98 | qed. |
---|
| 99 | |
---|
| 100 | lemma description_of_internal_function : ∀F,ge,i,fn. |
---|
| 101 | description_of_function ? ge i = Internal F fn → is_internal_function … ge i. |
---|
| 102 | #F #ge * #i * #fd #EQ |
---|
| 103 | #fn whd in ⊢ (??%?→?); >EQ normalize nodelta #EQ' >EQ' in EQ; #EQ |
---|
| 104 | %{EQ} |
---|
| 105 | qed. |
---|
| 106 | |
---|
| 107 | definition int_funct_of_block : ∀F,ge. |
---|
| 108 | block → option (Σi.is_internal_function F ge i) ≝ |
---|
| 109 | λF,ge,bl. |
---|
| 110 | ! f ← funct_of_block … ge bl ; |
---|
| 111 | match ? |
---|
| 112 | return λx.description_of_function … f = x → option (Σi.is_internal_function … ge i) |
---|
| 113 | with |
---|
| 114 | [ Internal fn ⇒ λprf.return «pi1 … f, ?» |
---|
| 115 | | External fn ⇒ λ_.None ? |
---|
| 116 | ] (refl …). |
---|
| 117 | @(description_of_internal_function … prf) |
---|
| 118 | qed. |
---|
| 119 | |
---|
| 120 | lemma internal_function_is_function : ∀F,ge,i. |
---|
| 121 | is_internal_function F ge i → is_function … ge i. |
---|
| 122 | #F #ge #i * #fn #prf %{prf} qed. |
---|
| 123 | |
---|
| 124 | definition if_of_function : ∀F,ge.(Σi.is_internal_function F ge i) → F ≝ |
---|
| 125 | λF,ge,i. |
---|
| 126 | match ! bl ← find_symbol … ge i ; |
---|
| 127 | find_funct_ptr … ge bl |
---|
| 128 | return λx.(∃fn.x = ?) → ? |
---|
| 129 | with |
---|
| 130 | [ Some fd ⇒ |
---|
| 131 | match fd return λx.(∃fn.Some ? x = ?) → ? with |
---|
| 132 | [ Internal fn ⇒ λ_.fn |
---|
| 133 | | External _ ⇒ λprf.⊥ |
---|
| 134 | ] |
---|
| 135 | | None ⇒ λprf.⊥ |
---|
| 136 | ] (pi2 … i). |
---|
| 137 | cases prf #fn #ABS destruct |
---|
| 138 | qed. |
---|
| 139 | |
---|
| 140 | lemma if_propagate : |
---|
[2478] | 141 | ∀A_in,A_out. |
---|
[2473] | 142 | ∀trans. |
---|
[2478] | 143 | ∀prog_in : program (λvars.fundef (A_in vars)) ℕ. |
---|
| 144 | let prog_out : program (λvars.fundef (A_out vars)) ℕ ≝ |
---|
[2473] | 145 | transform_program … prog_in (λvars.transf_fundef … (trans vars)) in |
---|
| 146 | ∀i.is_internal_function_of_program … prog_in i → |
---|
| 147 | is_internal_function_of_program … prog_out i. |
---|
[2478] | 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. |
---|
[2473] | 156 | |
---|
| 157 | lemma block_of_funct_ident_is_code : ∀F,ge,i. |
---|
| 158 | block_region (block_of_funct F ge i) = Code. |
---|
| 159 | #F #ge * #i * #fd |
---|
| 160 | whd in ⊢ (?→??(?%)?); |
---|
| 161 | cases (find_symbol ???) |
---|
| 162 | [ #ABS normalize in ABS; destruct(ABS) ] |
---|
| 163 | #bl normalize nodelta >m_return_bind |
---|
| 164 | whd in ⊢ (??%?→?); cases (block_region bl) |
---|
| 165 | [ #ABS normalize in ABS; destruct(ABS) ] |
---|
| 166 | #_ % |
---|
| 167 | qed. |
---|
| 168 | |
---|
| 169 | lemma prog_if_of_function_transform : |
---|
[2478] | 170 | ∀A,B,trans.∀prog_in : program (λvars.fundef (A vars)) ℕ. |
---|
| 171 | let prog_out : program (λvars.fundef (B vars)) ℕ ≝ |
---|
[2473] | 172 | transform_program … prog_in (λvars.transf_fundef … (trans vars)) in |
---|
[2478] | 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 % |
---|
[2473] | 194 | qed. |
---|