Changeset 1630


Ignore:
Timestamp:
Dec 19, 2011, 2:48:36 PM (8 years ago)
Author:
campbell
Message:

Remainder of freshness in Clight to Cminor pass.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1629 r1630  
    12031203  ∀tmpuniverse:universe SymbolTag.
    12041204  ∀globals:list (ident×region×type).
     1205    globals_fresh_for_univ ? globals tmpuniverse →
    12051206  ∀f:clight_fundef.
    1206     globals_fresh_for_univ ? globals tmpuniverse →
    12071207    fd_fresh_for_univ f tmpuniverse →
    12081208  res (fundef internal_function) ≝
    1209 λtmpuniverse,globals,f,Fglobals.
     1209λtmpuniverse,globals,Fglobals,f.
    12101210match f return λf. fd_fresh_for_univ f ? → ? with
    12111211[ CL_Internal fn ⇒ λFf. do fn' ← translate_function tmpuniverse globals fn Fglobals Ff; OK ? (Internal ? fn')
     
    12161216   generation.  Cheating a bit - we only need the new identifiers to be fresh
    12171217   for individual functions. *)
     1218
     1219let 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) ≝
     1221match 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.
    12181228
    12191229definition clight_to_cminor : clight_program → res Cminor_program ≝
     
    12231233  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
    12241234  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)).
     1240cases (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  
    11include "basics/lists/list.ma".
     2
     3lemma 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.
    28
    39(* An alternative form of All that can be easier to use sometimes. *)
     
    3238| #ha #ta #IH * [ // | #hb #tb #H * #H1 #H2 % [ @H @H1 | @(IH … H2) @H ] ]
    3339] qed.
     40
     41let 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 ≝
     42match 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.