Changeset 2353 for src/Clight/toCminor.ma
 Timestamp:
 Sep 26, 2012, 6:14:38 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminor.ma
r2252 r2353 51 51 gather_mem_vars_stmt s1 ∪ 52 52 gather_mem_vars_stmt s2 53  Swhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪54 gather_mem_vars_stmt s153  Swhile e1 s1 _ ⇒ gather_mem_vars_expr e1 ∪ 54 gather_mem_vars_stmt s1 55 55  Sdowhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪ 56 56 gather_mem_vars_stmt s1 … … 926 926 [ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2 927 927  Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2 928  Swhile _ s ⇒ labels_defined s928  Swhile _ s _ ⇒ labels_defined s 929 929  Sdowhile _ s ⇒ labels_defined s 930 930  Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3 … … 1124 1124 axiom ReturnMismatch : String. 1125 1125 1126 definition optional_cost : option costlabel → stmt → stmt ≝ 1127 λo,s. match o with [ Some l ⇒ St_cost l s  None ⇒ s ]. 1128 1126 1129 let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (rettyp:option typ) (s:statement) on s 1127 1130 : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) ≝ … … 1166 1169  _ ⇒ λ_.Error ? (msg TypeMismatch) 1167 1170 ] e1' 1168  Swhile e1 s1 ⇒1171  Swhile e1 s1 cl ⇒ 1169 1172 do e1' ← translate_expr vars e1; 1170 1173 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with … … 1176 1179 let converted_loop ≝ 1177 1180 St_label entry 1178 (St_seq 1179 (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) St_skip) 1180 (St_label exit St_skip)) 1181 (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) (St_label exit (optional_cost cl St_skip))) 1181 1182 in 1182 1183 OK ? «〈fgens2, converted_loop〉, ?» … … 1339 1340  3,6: #H %2 assumption ] ] 1340 1341 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I try assumption 1341 [ 1,7,17: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) 1342 [ 1,10,20: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) 1343  cases cl normalize /3/ 1342 1344  (*2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) // 1343 *) 2,8: whd #l #H normalize in H;1345 *) 3,11: whd #l #H normalize in H; 1344 1346 elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label) 1345 1347 @conj … … 1347 1349  2,4: whd @or_intror normalize @Exists_append_l @Exists_append_l try @Exists_append_l 1348 1350 @(proj2 … Hlabel) ] 1349  27: whd %2 %2 whd /2/ 1350  28: whd %2 whd /2/ 1351  3,14: whd %1 %1 normalize /2/ 1352  4,10: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1351  30: whd %2 %2 whd /2/ 1352  31: whd %2 whd /2/ 1353  cases cl normalize /3/ 1354  5,17: whd %1 %1 normalize /2/ 1355  6,13: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1353 1356 #l * try * [ 1,5: #H %1 %1 normalize %2 @Exists_append_l @Exists_append_l try @Exists_append_l @H 1354 1357  2,6: #H %1 %2 assumption … … 1358 1361  2,4: * ] 1359 1362 ] 1360  5: normalize %1 %1 %1 // 1361  6,12: normalize %1 %1 %2 @Exists_append_r normalize /2/ 1362  9,11: whd %1 %1 normalize /2/ 1363  13: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct //  whd /2/ ] 1363  7: normalize %1 %1 %1 // 1364  8,15: normalize %1 %1 %2 @Exists_append_r normalize /2/ 1365  cases cl normalize /3/ 1366  12,14: whd %1 %1 normalize /2/ 1367  16: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct //  whd /2/ ] 1364 1368  2: #H elim (Hlabels_tr1 label H) 1365 1369 #lab * #Hlookup #Hdef @(ex_intro … lab) @conj 1366 1370 [ 1: //  2: whd %2 assumption ] 1367 1371 ] 1368  1 5: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)1372  18: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1369 1373 #l * try * [ 1: #H %1 %1 normalize %2 @H 1370 1374  2: #H %1 %2 assumption 1371 1375  3: #H %2 assumption ] 1372  1 6: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t1376  19: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t 1373 1377 #H @(Htmps_pres3 … (Htmps_pres2 … H)) 1374  18: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t1378  21: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t 1375 1379 #H @(Htmps_pres3 … H) 1376  19: whd #l #H normalize in H;1380  22: whd #l #H normalize in H; 1377 1381 cases (Exists_append … H) #Hcase 1378 1382 [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj … … 1395 1399 ] 1396 1400 ] 1397  2 0: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))1398  2 1: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)1401  23: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H))) 1402  24: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1399 1403 #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H 1400 1404  2: #H %1 %2 assumption 1401 1405  3: #H %2 assumption ] 1402  2 2: whd %1 %1 normalize /2/1403  2 3: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)1406  25: whd %1 %1 normalize /2/ 1407  26: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1404 1408 #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?)) 1405 1409 @Exists_append_r @Exists_append_l @Exists_append_l … … 1414 1418  2: * ] 1415 1419 ] 1416  2 4: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)1420  27: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1417 1421 #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?)) 1418 1422 @Exists_append_r @Exists_append_l @Exists_append_l … … 1426 1430  2: * ] 1427 1431 ] 1428  2 5: whd %1 %1 normalize /2/1429  2 6: whd %1 %1 normalize1432  28: whd %1 %1 normalize /2/ 1433  29: whd %1 %1 normalize 1430 1434 @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r 1431 1435 whd %1 // 1432  29: whd %1 %2 whd @(ex_intro … l) @E1436  32: whd %1 %2 whd @(ex_intro … l) @E 1433 1437 ] qed. 1434 1438
Note: See TracChangeset
for help on using the changeset viewer.