 Timestamp:
 Dec 19, 2011, 2:48:35 PM (8 years ago)
 Location:
 src/Clight
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/fresh.ma
r1628 r1629 7 7 8 8 include "Clight/Csyntax.ma". 9 include "utilities/lists.ma". 9 10 10 11 definition max_id : ident → ident → ident ≝ … … 59 60 ]. 60 61 62 definition globals_fresh_for_univ : ∀V:Type[0]. list (ident × region × V) → universe SymbolTag → Prop ≝ 63 λV,gl,u. All ? (λv. fresh_for_univ ? (\fst (\fst v)) u) gl. 64 61 65 definition prog_fresh_for_univ : clight_program → universe SymbolTag → Prop ≝ 62 66 λp,u. 63 67 All ? (λifd. fresh_for_univ ? (\fst ifd) u ∧ fd_fresh_for_univ (\snd ifd) u) (prog_funct ?? p) ∧ 64 68 fresh_for_univ ? (prog_main ?? p) u ∧ 65 All ? (λv. fresh_for_univ ? (\fst (\fst v)) u) (prog_vars ?? p).69 globals_fresh_for_univ ? (prog_vars ?? p) u. 66 70 67 71 (* And they match up. *) 
src/Clight/toCminor.ma
r1627 r1629 3 3 include "Clight/TypeComparison.ma". 4 4 include "basics/lists/list.ma". 5 include "Clight/fresh.ma". 5 6 6 7 (* Identify local variables that must be allocated memory. *) … … 137 138 qed. 138 139 140 lemma characterise_vars_src : ∀gl,f,vars,n. 141 characterise_vars gl f = 〈vars,n〉 → 142 ∀id. present ?? vars id → 143 (∃r,ty. lookup' vars id = OK ? 〈Global r,ty〉 ∧ Exists ? (λx.x = 〈〈id,r〉,ty〉) gl) ∨ 144 ∃t.local_id vars id t. 145 #globals #f 146 whd in ⊢ (∀_.∀_.??%? → ?); 147 elim (fn_params f @ fn_vars f) 148 [ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #H %1 149 elim globals in H ⊢ %; 150 [ normalize * #H cases (H (refl ??)) 151  * * #id #rg #ty #tl #IH #H 152 cases (identifier_eq ? i id) 153 [ #E <E %{rg} %{ty} % [ whd in ⊢ (??%?); >lookup_add_hit //  %1 // ] 154  #NE cases (IH ?) 155 [ #rg' * #ty' * #H1 #H2 %{rg'} %{ty'} % 156 [ whd in ⊢ (??%?); >lookup_add_miss [ @H1  @NE ] 157  %2 @H2 158 ] 159  whd in H ⊢ %; >lookup_add_miss in H; // 160 ] 161 ] 162 ] 163  * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i 164 #H >(contract_pair var_types nat ?) in E; 165 whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?); 166 cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?); 167 #H' lapply (extract_pair ???????? H') H' * #m0 * #n0 * #EQ #EQ2 168 cases (identifier_eq ? i id) 169 [ 1,3: #E' <E' in EQ2:%; #EQ2 %2 %{(typ_of_type ty)} 170 destruct (EQ2) whd whd in ⊢ (match % with [_ ⇒ ?  _ ⇒ ?]); 171 >lookup_add_hit @refl 172  *: #NE cases (IH m0 n0 ? i ?) 173 [ 1,5: * #rg' * #ty' * #H1 #H2 %1 %{rg'} %{ty'} % // 174 destruct (EQ2) whd in ⊢ (??%?); >lookup_add_miss try @NE @H1 175  2,6: * #t #H1 %2 %{t} destruct (EQ2) whd whd in ⊢ (match % with [_ ⇒ ?_ ⇒ ?]); 176 >lookup_add_miss // 177  3,7: <EQ @refl 178  *: destruct (EQ2) whd in H; >lookup_add_miss in H; // 179 ] 180 ] 181 ] qed. 182 183 139 184 lemma characterise_vars_all : ∀l,f,vars,n. 140 185 characterise_vars l f = 〈vars,n〉 → … … 168 213 ] 169 214 ] 215 ] qed. 216 217 lemma characterise_vars_fresh : ∀gl,f,vars,n,u. 218 characterise_vars gl f = 〈vars,n〉 → 219 globals_fresh_for_univ ? gl u → 220 fn_fresh_for_univ f u → 221 fresh_map_for_univ … vars u. 222 #gl #f #vars #n #u #CH #GL #FN 223 #id #H 224 cases (characterise_vars_src … CH … H) 225 [ * #rg * #ty * #H1 #H2 226 cases (Exists_All … H2 GL) * * #id' #rg' #ty' * #E #H destruct // 227  * #t #H lapply (characterise_vars_all … CH id t H) #EX 228 cases (Exists_All … EX FN) * #id' #ty' * * #E1 #E2 #H' H destruct // 170 229 ] qed. 171 230 … … 1099 1158 ] qed. 1100 1159 1101 definition translate_function : universe SymbolTag → list (ident×region×type) → function → res internal_function ≝ 1102 λtmpuniverse, globals, f. 1160 definition translate_function : 1161 ∀tmpuniverse:universe SymbolTag. 1162 ∀globals:list (ident×region×type). 1163 ∀f:function. 1164 globals_fresh_for_univ ? globals tmpuniverse → 1165 fn_fresh_for_univ f tmpuniverse → 1166 res internal_function ≝ 1167 λtmpuniverse, globals, f, Fglobals, Ffn. 1103 1168 do «lbls, Ilbls» ← build_label_env (fn_body f); 1104 1169 let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in … … 1113 1178 s ?). 1114 1179 [ // 1115  (* FIXME *) cases daemon1180  @(characterise_vars_fresh … (sym_eq … E)) // 1116 1181  cases Is * #S #L #TP 1117 1182 @(stmt_P_mp ???? S) … … 1135 1200 ] qed. 1136 1201 1137 definition translate_fundef : universe SymbolTag → list (ident×region×type) → clight_fundef → res (fundef internal_function) ≝ 1138 λtmpuniverse,globals,f. 1139 match f with 1140 [ CL_Internal fn ⇒ do fn' ← translate_function tmpuniverse globals fn; OK ? (Internal ? fn') 1141  CL_External fn argtys retty ⇒ OK ? (External ? (mk_external_function fn (signature_of_type argtys retty))) 1202 definition translate_fundef : 1203 ∀tmpuniverse:universe SymbolTag. 1204 ∀globals:list (ident×region×type). 1205 ∀f:clight_fundef. 1206 globals_fresh_for_univ ? globals tmpuniverse → 1207 fd_fresh_for_univ f tmpuniverse → 1208 res (fundef internal_function) ≝ 1209 λtmpuniverse,globals,f,Fglobals. 1210 match f return λf. fd_fresh_for_univ f ? → ? with 1211 [ CL_Internal fn ⇒ λFf. do fn' ← translate_function tmpuniverse globals fn Fglobals Ff; OK ? (Internal ? fn') 1212  CL_External fn argtys retty ⇒ λ_. OK ? (External ? (mk_external_function fn (signature_of_type argtys retty))) 1142 1213 ]. 1143 1214 … … 1145 1216 generation. Cheating a bit  we only need the new identifiers to be fresh 1146 1217 for individual functions. *) 1147 include "Clight/fresh.ma".1148 1218 1149 1219 definition clight_to_cminor : clight_program → res Cminor_program ≝
Note: See TracChangeset
for help on using the changeset viewer.