Changeset 1630
 Timestamp:
 Dec 19, 2011, 2:48:36 PM (9 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminor.ma
r1629 r1630 1203 1203 ∀tmpuniverse:universe SymbolTag. 1204 1204 ∀globals:list (ident×region×type). 1205 globals_fresh_for_univ ? globals tmpuniverse → 1205 1206 ∀f:clight_fundef. 1206 globals_fresh_for_univ ? globals tmpuniverse →1207 1207 fd_fresh_for_univ f tmpuniverse → 1208 1208 res (fundef internal_function) ≝ 1209 λtmpuniverse,globals, f,Fglobals.1209 λtmpuniverse,globals,Fglobals,f. 1210 1210 match f return λf. fd_fresh_for_univ f ? → ? with 1211 1211 [ CL_Internal fn ⇒ λFf. do fn' ← translate_function tmpuniverse globals fn Fglobals Ff; OK ? (Internal ? fn') … … 1216 1216 generation. Cheating a bit  we only need the new identifiers to be fresh 1217 1217 for individual functions. *) 1218 1219 let rec map_partial_All (A,B:Type[0]) (P:A → Prop) (f:∀a:A. P a → res B) 1220 (l:list A) (H:All A P l) on l : res (list B) ≝ 1221 match l return λl. All A P l → ? with 1222 [ nil ⇒ λ_. OK (list B) (nil B) 1223  cons hd tl ⇒ λH. 1224 do b_hd ← f hd (proj1 … H); 1225 do b_tl ← map_partial_All A B P f tl (proj2 … H); 1226 OK (list B) (cons B b_hd b_tl) 1227 ] H. 1218 1228 1219 1229 definition clight_to_cminor : clight_program → res Cminor_program ≝ … … 1223 1233 let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in 1224 1234 let globals ≝ fun_globals @ var_globals in 1225 transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)). 1235 do fns ← map_partial_All ??? (λx,H. do f ← translate_fundef tmpuniverse globals ? (\snd x) H; OK ? 〈\fst x, f〉) (prog_funct ?? p) ?; 1236 OK ? (mk_program ?? 1237 (map ?? (λv. 〈\fst v, \fst (\snd v)〉) (prog_vars ?? p)) 1238 fns 1239 (prog_main ?? p)). 1240 cases (prog_fresh p) * #H1 #H2 #H3 1241 [ @(All_mp … H1) #x * // 1242  @All_append 1243 [ elim (prog_funct ?? p) in H1 ⊢ %; // * #id #fd #tl #IH * * #Hhd1 #Hhd2 #Htl % // @IH @Htl 1244  whd in H3; elim (prog_vars ?? p) in H3 ⊢ %; // #hd #tl #IH * #Hhd #Htl % /2/ 1245 ] 1246 ] qed. 1247 1248 (* It'd be nice to go back to some generic thing like 1249 1250 transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)). 1251 1252 rather than the messier definition above. 1253 *) 
src/utilities/lists.ma
r1628 r1630 1 1 include "basics/lists/list.ma". 2 3 lemma All_append : ∀A,P,l,r. All A P l → All A P r → All A P (l@r). 4 #A #P #l elim l 5 [ // 6  #hd #tl #IH #r * #H1 #H2 #H3 % // @IH // 7 ] qed. 2 8 3 9 (* An alternative form of All that can be easier to use sometimes. *) … … 32 38  #ha #ta #IH * [ //  #hb #tb #H * #H1 #H2 % [ @H @H1  @(IH … H2) @H ] ] 33 39 ] qed. 40 41 let rec map_All (A,B:Type[0]) (P:A → Prop) (f:∀a. P a → B) (l:list A) (H:All A P l) on l : list B ≝ 42 match l return λl. All A P l → ? with 43 [ nil ⇒ λ_. nil B 44  cons hd tl ⇒ λH. cons B (f hd (proj1 … H)) (map_All A B P f tl (proj2 … H)) 45 ] H. 46
Note: See TracChangeset
for help on using the changeset viewer.