 Timestamp:
 Oct 19, 2012, 11:18:52 AM (9 years ago)
 Location:
 src/Clight
 Files:

 3 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminor.ma
r2391 r2407 1174 1174 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with 1175 1175 [ ASTint _ _ ⇒ λe1'. 1176 (* TODO: this is a little different from the prototype and CompCert, is it OK? *)1177 1176 let 〈labels, ul1〉 as E1 ≝ mklabels ul in 1178 1177 let 〈entry, exit〉 as E2 ≝ labels in … … 1213 1212 (St_label exit St_skip) 1214 1213 in 1215 (* TODO: this is a little different from the prototype and CompCert, is it OK? *)1216 1214 OK ? «〈fgens2, converted_loop〉, ?» 1217 1215  _ ⇒ λ_.Error ? (msg TypeMismatch) … … 1222 1220 [ ASTint _ _ ⇒ λe1'. 1223 1221 let 〈labels, ul1〉 as E ≝ mklabels ul in 1224 let 〈entry, exit〉 as E2 ≝ labels in 1225 do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls flag rettyp s1; 1226 do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) lbls (ConvertTo entry exit) rettyp s2; 1227 do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) lbls (ConvertTo entry exit) rettyp s3; 1228 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 1222 let 〈continue, exit〉 as E2 ≝ labels in 1223 let 〈entry, ul2〉 ≝ generate_fresh_label … ul1 in 1224 do «fgens2, s1', H1» ← translate_statement vars uv ul2 lbls flag rettyp s1; 1225 (* The choice of flag is arbitrary  Clight's semantics give no meaning 1226 to continue or break in s2 because in C it must be an expression. *) 1227 do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) lbls flag rettyp s2; 1228 do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) lbls (ConvertTo continue exit) rettyp s3; 1229 1229 let converted_loop ≝ 1230 1230 St_seq … … 1232 1232 (St_label entry 1233 1233 (St_seq 1234 (St_ifthenelse ?? e1' (St_seq s3' (St_ seq s2' (St_goto entry))) St_skip)1234 (St_ifthenelse ?? e1' (St_seq s3' (St_label continue (St_seq s2' (St_goto entry)))) St_skip) 1235 1235 (St_label exit St_skip) 1236 1236 )) … … 1389 1389  @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t 1390 1390 #H @(Htmps_pres3 … H) 1391  % // 1391 1392  whd #l #H normalize in H; 1392 1393 cases (Exists_append … H) #Hcase … … 1399 1400 [ 1: @(proj1 … Hlabel) 1400 1401  2: normalize >append_nil >append_nil >append_cons 1401 @Exists_append_r @Exists_append_l @Exists_append_r 1402 @Exists_append_r @Exists_append_l @Exists_append_r %2 1402 1403 @(proj2 … Hlabel) 1403 1404 ] … … 1422 1423  2: #H %1 %2 assumption 1423 1424  3: #H <H %1 %1 normalize 1424 @Exists_append_r whd %1 // 1425  4: * [ 1: #H <H %1 %1 normalize 1426 @Exists_append_r @(Exists_add ?? (nil ?)) 1427 @Exists_append_r @Exists_append_r 1428 whd %1 // 1429  2: * ] 1430 ] 1431  @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1432 #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?)) 1433 @Exists_append_r @Exists_append_l @Exists_append_l 1434 @Exists_append_r @Exists_append_l assumption 1435  2: #H %1 %2 assumption 1436  3: #H <H %1 %1 normalize 1437 @Exists_append_r whd %1 // 1425 @Exists_append_r %2 @Exists_append_l @Exists_append_l 1426 @Exists_append_r %1 % 1438 1427  4: * [ 1: #Eq <Eq %1 %1 whd normalize 1439 1428 @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r 1440 1429 @Exists_append_r whd %1 // 1441 1430  2: * ] 1431 ] 1432  % %1 normalize @Exists_append_r %2 @Exists_append_l @Exists_append_l 1433 @Exists_append_r % % 1434  @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1435 #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?)) 1436 @Exists_append_r @Exists_append_l @Exists_append_l 1437 @Exists_append_r %2 @Exists_append_l assumption 1438  2: #H %1 %2 assumption 1439  3: /2/ 1442 1440 ] 1443 1441  whd %1 %1 normalize /2/
Note: See TracChangeset
for help on using the changeset viewer.