source: src/common/extraGlobalenvs.ma @ 2473

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

put some generic stuff we need in the back end in extraGlobalenvs (with some axioms that are
in the commented section of Globalenvs)
linearise now has a full spec

File size: 9.5 KB
Line 
1include "common/AST.ma".
2include "common/Globalenvs.ma".
3
4(* TODO: need this for global env *)
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
24definition 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〉.
27
28definition is_function ≝ λF.λge : genv_t F.
29  λi : ident.∃fd.
30    ! bl ← find_symbol … ge i ;
31    find_funct_ptr … ge bl = Some ? fd.
32
33definition funct_of_ident : ∀F,ge.
34  ident → option (Σi.is_function F ge i)
35≝ λF,ge,i.
36match ?
37return λx.! bl ← find_symbol … ge i ;
38    find_funct_ptr … ge bl = x → ?
39with
40[ Some fd ⇒ λprf.return «i, ex_intro ?? fd prf»
41| None ⇒ λ_.None ?
42] (refl …).
43
44lemma symbol_of_function_block_ok :
45  ∀F,ge,b,prf.symbol_for_block F ge b = Some ? (symbol_of_function_block F ge b prf).
46#F #ge #b #FFP
47cut (∀A,B : Type[0].∀P : B → Prop.∀x : option A.∀c1,c2.
48  (∀v.∀prf : x = Some ? v.P (c1 v prf)) →
49  (∀prf:x = None ?.P (c2 prf)) →
50  P (match x return λy.x = y → ? with
51     [ Some v ⇒ λprf.c1 v prf | None ⇒ λprf.c2 prf]
52     (refl …))) [ #A #B #P * // ] #aux
53whd in ⊢ (???(??%)); @aux [//] #H @⊥
54(* cut and paste from global env *)
55whd in H:(??%?);
56cases b in FFP H ⊢ %; * * -b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP | *: * #H cases (H (refl ??)) ]
57cases (functions_inv … ge b FFP)
58#id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
59lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
60cases (find ????)
61[ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ * | * #H' cases (H' (refl ??)) ]
62| * #id' #b' #_ normalize #_ #E destruct
63] qed.
64
65definition funct_of_block : ∀F,ge.
66  block → option  (Σi.is_function F ge i) ≝
67λF,ge,bl.
68   match find_funct_ptr … ge bl
69   return λx.find_funct_ptr … ge bl = x → ? with
70   [ Some fd ⇒ λprf.return mk_Sig
71        ident (λi.is_function F ge i)
72        (symbol_of_function_block … ge bl ?)
73        (ex_intro … fd ?)
74   | None ⇒ λ_.None ?
75   ] (refl …).
76[ >(symbol_of_block_rev … (symbol_of_function_block_ok ? ge bl ?)) @prf
77| >prf % #ABS destruct(ABS)
78]
79qed.
80
81definition block_of_funct ≝ λF,ge.
82  λi : Σi.is_function F ge i.
83  match find_symbol … ge i return λx.(∃fd.!bl ← x; ? = ?) → ? with
84  [ Some bl ⇒ λ_.bl
85  | None ⇒ λprf.⊥
86  ] (pi2 … i).
87cases prf #fd normalize #ABS destruct(ABS)
88qed.
89
90definition description_of_function : ∀F,ge.(Σi.is_function F ge i) → F ≝
91λF,ge,i.
92match ! bl ← find_symbol … ge i ;
93        find_funct_ptr … ge bl
94return λx.(∃fd.x = ?) → ?
95with
96[ Some fd ⇒ λ_.fd
97| None ⇒ λprf.⊥
98] (pi2 … i).
99cases prf #fd #ABS destruct
100qed.
101
102definition is_internal_function ≝ λF.λge : genv_t (fundef F).
103  λi : ident.∃fd.
104    ! bl ← find_symbol … ge i ;
105    find_funct_ptr … ge bl = Some ? (Internal ? fd).
106
107lemma description_of_internal_function : ∀F,ge,i,fn.
108  description_of_function ? ge i = Internal F fn → is_internal_function … ge i.
109#F #ge * #i * #fd #EQ
110#fn whd in ⊢ (??%?→?); >EQ normalize nodelta #EQ' >EQ' in EQ; #EQ
111%{EQ}
112qed.
113
114definition int_funct_of_block : ∀F,ge.
115  block → option (Σi.is_internal_function F ge i) ≝
116  λF,ge,bl.
117  ! f ← funct_of_block … ge bl ;
118  match ?
119  return λx.description_of_function … f = x → option (Σi.is_internal_function … ge i)
120  with
121  [ Internal fn ⇒ λprf.return «pi1 … f, ?»
122  | External fn ⇒ λ_.None ?
123  ] (refl …).
124@(description_of_internal_function … prf)
125qed.
126
127lemma internal_function_is_function : ∀F,ge,i.
128  is_internal_function F ge i → is_function … ge i.
129#F #ge #i * #fn #prf %{prf} qed.
130
131definition if_of_function : ∀F,ge.(Σi.is_internal_function F ge i) → F ≝
132λF,ge,i.
133match ! bl ← find_symbol … ge i ;
134        find_funct_ptr … ge bl
135return λx.(∃fn.x = ?) → ?
136with
137[ Some fd ⇒
138  match fd return λx.(∃fn.Some ? x = ?) → ? with
139  [ Internal fn ⇒ λ_.fn
140  | External _ ⇒ λprf.⊥
141  ]
142| None ⇒ λprf.⊥
143] (pi2 … i).
144cases prf #fn #ABS destruct
145qed.
146
147lemma is_internal_function_of_program_ok :
148  ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.∀i.
149  is_internal_function … (globalenv ?? init prog) i →
150  is_internal_function_of_program ?? prog i.
151#A #B #init #prog #i whd in ⊢ (%→%); * #ifn
152lapply (refl … (find_symbol … i))
153[3: elim (find_symbol … i) in ⊢ (???%→%);
154  [#_ #ABS normalize in ABS; destruct(ABS)]
155|*:]
156#bl #EQbl >m_return_bind #EQfind %{ifn}
157@(find_funct_ptr_symbol_inversion … EQbl EQfind)
158qed.
159
160lemma ok_is_internal_function_of_program :
161  ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.∀i.
162  is_internal_function_of_program … prog i →
163  is_internal_function ? (globalenv ?? init prog) i.
164#A #B #init #prog #i whd in ⊢ (%→%); * #ifn #H
165elim (find_funct_ptr_exists … init … H)
166#bl * #EQ1 #EQ2 %{ifn} >EQ1 @EQ2 qed.
167
168lemma Exists_find : ∀A,B,P,f,l.(∀x.P x → f x ≠ None ?) → Exists ? P l →
169  find A B f l ≠ None ?.
170#A #B #P #f #l #H elim l -l [ * ] normalize
171#hd #tl #IH *
172[ #Phd >(opt_to_opt_safe … (H … Phd)) normalize nodelta % #ABS destruct(ABS)
173| #Ptl elim (f hd)
174  [ @(IH Ptl)
175  | #x % normalize #ABS destruct(ABS)
176  ]
177]
178qed.
179
180definition prog_if_of_function :
181  ∀F,V,prog.
182  (Σi.is_internal_function_of_program F V prog i) → F ? ≝
183λF,V,prog,i.opt_safe ? (find ??
184  (λpr.if eq_identifier ? (\fst pr) i then
185    match \snd pr with
186    [ Internal x ⇒ return x
187    | External _ ⇒ None ?
188    ]
189  else None ?)
190  (prog_funct … prog)) ?.
191@hide_prf
192cases i -i #i * #ifn #prf
193@(Exists_find … prf)
194* #i' #fn' #EQ destruct(EQ) >eq_identifier_refl normalize nodelta
195% normalize in ⊢ (??%?→?); #ABS destruct(ABS)
196qed.
197
198definition if_in_global_env_to_if_in_prog :
199  ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.
200  (Σi.is_internal_function ? (globalenv ?? init prog) i) →
201  Σi.is_internal_function_of_program ?? prog i ≝
202  λA,B,init,prog,f.«f, is_internal_function_of_program_ok … (pi2 … f)».
203
204coercion if_in_prog_from_if_in_global_env nocomposites :
205  ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.
206  ∀f:Σi.is_internal_function ? (globalenv ?? init prog) i.
207  Σi.is_internal_function_of_program ?? prog i ≝
208  if_in_global_env_to_if_in_prog
209  on _f : Sig ident (λi.is_internal_function ?? i)
210  to Sig ident (λi.is_internal_function_of_program ??? i).
211
212lemma if_propagate :
213∀A_in,A_out,B.
214∀trans.
215∀prog_in : program (λvars.fundef (A_in vars)) B.
216let prog_out : program (λvars.fundef (A_out vars)) B ≝
217  transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
218∀i.is_internal_function_of_program … prog_in i →
219is_internal_function_of_program … prog_out i.
220#A_in #A_out #B #trans #prog_in #ident
221* #ifn #H %{(trans … ifn)}
222@(Exists_map … H) * #id #fn #EQ destruct(EQ) % qed.
223
224lemma block_of_funct_ident_is_code : ∀F,ge,i.
225  block_region (block_of_funct F ge i) = Code.
226#F #ge * #i * #fd
227whd in ⊢ (?→??(?%)?);
228cases (find_symbol ???)
229[ #ABS normalize in ABS; destruct(ABS) ]
230#bl normalize nodelta >m_return_bind
231whd in ⊢ (??%?→?); cases (block_region bl)
232[ #ABS normalize in ABS; destruct(ABS) ]
233#_ %
234qed.
235
236
237lemma 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.
238#A #B #C #f #g #l elim l -l [%] #hd #tl #IH normalize >IH % qed.
239
240lemma find_bind : ∀A,B,C,f,g,l.
241  find A C (λx.! y ← f x ; return g y) l = ! y ← find A B f l ; return g y.
242#A #B #C #f #g #l elim l -l
243[%]
244#hd #tl #IH
245whd in match (find ??? (hd::tl)) in ⊢ (??%%);
246cases (f hd) [ @IH ] #x % qed.
247
248lemma find_ext_eq : ∀A,B,f,g,l.(∀x.f x = g x) → find A B f l = find A B g l.
249#A #B #f #g #l #H elim l -l [%] #hd #tl #IH normalize >H >IH % qed.
250
251lemma prog_if_of_function_transform :
252  ∀A,B,V,trans.∀prog_in : program (λvars.fundef (A vars)) V.
253  let prog_out : program (λvars.fundef (B vars)) V≝
254    transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
255  ∀i,prf1,prf2.
256  prog_if_of_function ?? prog_out «i,prf1» = trans … (prog_if_of_function ?? prog_in «i,prf2»).
257#A #B #V #trans #prog #i #i_prf #i_prf'
258change with (opt_safe ??? = ?)
259@opt_safe_elim #ifn >find_map
260cut (∀vars.∀x.
261  if eq_identifier ? (\fst x) i then
262    match transf_fundef … (trans vars) (\snd x) with
263    [ Internal x ⇒ return x
264    | _ ⇒ None ?
265    ] else None ? =
266  ! y ← if eq_identifier ? (\fst x) i then
267        match \snd x with
268        [ Internal x ⇒ return x
269        | _ ⇒ None ?
270        ] else None ? ;
271  return trans vars y)
272[ #vars * #id * #fn whd in match transf_fundef; normalize nodelta
273  cases (eq_identifier ???) % ] #H
274>(find_ext_eq … (H ?)) >find_bind
275#EQfind
276change with (? = trans ? (opt_safe ???))
277@opt_safe_elim #ifn' #EQfind'
278>EQfind' in EQfind; >m_return_bind whd in ⊢ (??%?→?); #EQ destruct(EQ) %
279qed.
Note: See TracBrowser for help on using the repository browser.