source: src/common/extraGlobalenvs.ma @ 2540

Last change on this file since 2540 was 2478, checked in by tranquil, 7 years ago

unified is_internal_function_of_program and is_internal_function

File size: 6.4 KB
Line 
1include "common/AST.ma".
2include "common/Globalenvs.ma".
3
4(*
5axiom 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
12axiom 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
18axiom 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
25definition 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
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.
38
39definition funct_of_ident : ∀F,ge.
40  ident → option (Σi.is_function F ge i)
41≝ λF,ge,i.
42match ?
43return λx.! bl ← find_symbol … ge i ;
44    find_funct_ptr … ge bl = x → ?
45with
46[ Some fd ⇒ λprf.return «i, ex_intro ?? fd prf»
47| None ⇒ λ_.None ?
48] (refl …).
49
50lemma 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
53cut (∀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
59whd in ⊢ (???(??%)); @aux [//] #H
60generalize in match (? : False); *
61qed.
62
63definition 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]
77qed.
78
79definition 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).
85cases prf #fd normalize #ABS destruct(ABS)
86qed.
87
88definition description_of_function : ∀F,ge.(Σi.is_function F ge i) → F ≝
89λF,ge,i.
90match ! bl ← find_symbol … ge i ;
91        find_funct_ptr … ge bl
92return λx.(∃fd.x = ?) → ?
93with
94[ Some fd ⇒ λ_.fd
95| None ⇒ λprf.⊥
96] (pi2 … i).
97cases prf #fd #ABS destruct
98qed.
99
100lemma 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}
105qed.
106
107definition 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)
118qed.
119
120lemma 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
124definition if_of_function : ∀F,ge.(Σi.is_internal_function F ge i) → F ≝
125λF,ge,i.
126match ! bl ← find_symbol … ge i ;
127        find_funct_ptr … ge bl
128return λx.(∃fn.x = ?) → ?
129with
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).
137cases prf #fn #ABS destruct
138qed.
139
140lemma if_propagate :
141∀A_in,A_out.
142∀trans.
143∀prog_in : program (λvars.fundef (A_in vars)) ℕ.
144let prog_out : program (λvars.fundef (A_out vars)) ℕ ≝
145  transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
146∀i.is_internal_function_of_program … prog_in i →
147is_internal_function_of_program … prog_out i.
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.
156
157lemma block_of_funct_ident_is_code : ∀F,ge,i.
158  block_region (block_of_funct F ge i) = Code.
159#F #ge * #i * #fd
160whd in ⊢ (?→??(?%)?);
161cases (find_symbol ???)
162[ #ABS normalize in ABS; destruct(ABS) ]
163#bl normalize nodelta >m_return_bind
164whd in ⊢ (??%?→?); cases (block_region bl)
165[ #ABS normalize in ABS; destruct(ABS) ]
166#_ %
167qed.
168
169lemma prog_if_of_function_transform :
170  ∀A,B,trans.∀prog_in : program (λvars.fundef (A vars)) ℕ.
171  let prog_out : program (λvars.fundef (B vars)) ℕ ≝
172    transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
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 %
194qed.
Note: See TracBrowser for help on using the repository browser.