Changeset 2391 for src/Clight/toCminor.ma
 Timestamp:
 Oct 9, 2012, 3:10:07 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminor.ma
r2389 r2391 51 51 gather_mem_vars_stmt s1 ∪ 52 52 gather_mem_vars_stmt s2 53  Swhile e1 s1 _⇒ gather_mem_vars_expr e1 ∪54 53  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 1129 1126 let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (rettyp:option typ) (s:statement) on s 1130 1127 : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) ≝ … … 1173 1170 but the behaviour of the next stage means that we can put in Cminor skips and 1174 1171 goto labels before the cost label. *) 1175  Swhile e1 s1 cl⇒1172  Swhile e1 s1 ⇒ 1176 1173 do e1' ← translate_expr vars e1; 1177 1174 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with … … 1183 1180 let converted_loop ≝ 1184 1181 St_label entry 1185 (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) (St_label exit (optional_cost cl St_skip))) 1182 (St_seq 1183 (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) St_skip) 1184 (St_label exit St_skip)) 1186 1185 in 1187 1186 OK ? «〈fgens2, converted_loop〉, ?» … … 1354 1353  3,6: #H %2 assumption ] ] 1355 1354 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I try assumption 1356 [ 1,10,22: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) 1357  cases cl normalize /3/ 1358  (*2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) // 1359 *) 3,11: whd #l #H normalize in H; 1360 elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label) 1361 @conj 1362 [ 1,3: @(proj1 … Hlabel) 1363  2,4: whd @or_intror normalize in ⊢ (???%); 1364 [ @Exists_append_l @Exists_append_l  %2 @Exists_append_l @Exists_append_l @Exists_append_l ] 1365 @(proj2 … Hlabel) ] 1366  cases cl normalize /3/ 1367  5,13,16: whd %1 %1 normalize /2/ 1368  6,15: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1355 [ 1,7,19: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) 1356  2,8: whd #l #H normalize in H; 1357 elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label) 1358 @conj 1359 [ 1,3: @(proj1 … Hlabel) 1360  2,4: whd @or_intror normalize in ⊢ (???%); 1361 [ @Exists_append_l @Exists_append_l @Exists_append_l  %2 @Exists_append_l @Exists_append_l @Exists_append_l ] 1362 @(proj2 … Hlabel) ] 1363  whd %1 %1 normalize /2/ 1364  4,12: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1369 1365 #l * try * [ 1,5: #H %1 %1 normalize %2 [ 2: %2 ] @Exists_append_l @Exists_append_l try @Exists_append_l @H 1370 1366  2,6: #H %1 %2 assumption … … 1374 1370  2,4: * ] 1375 1371 ] 1376  7: normalize %1 %1 %1 // 1377  8,14: normalize %1 %1 %2 [ @Exists_append_r normalize /2/  %1 % ] 1378  cases cl normalize /3/ 1372  normalize %1 %1 %1 // 1373  6,11: normalize %1 %1 %2 [ @Exists_append_r normalize /2/  %1 % ] 1379 1374  whd %1 %1 normalize %2 %1 % 1375  10,13: normalize %1 %1 %1 % 1380 1376  normalize %1 %1 %2 %2 /2/ 1381 1377  whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct //  whd /2/ ]
Note: See TracChangeset
for help on using the changeset viewer.