Ignore:
Timestamp:
Sep 26, 2012, 6:14:38 PM (7 years ago)
Author:
campbell
Message:

Put the post-loop cost label into the Clight while statement to get rid
of extra skips. (Soon to be followed by other loop constructs.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2252 r2353  
    5151                         gather_mem_vars_stmt s1 ∪
    5252                         gather_mem_vars_stmt s2
    53 | Swhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
    54                  gather_mem_vars_stmt s1
     53| Swhile e1 s1 _ ⇒ gather_mem_vars_expr e1 ∪
     54                   gather_mem_vars_stmt s1
    5555| Sdowhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
    5656                   gather_mem_vars_stmt s1
     
    926926[ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2
    927927| Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2
    928 | Swhile _ s ⇒ labels_defined s
     928| Swhile _ s _ ⇒ labels_defined s
    929929| Sdowhile _ s ⇒ labels_defined s
    930930| Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
     
    11241124axiom ReturnMismatch : String.
    11251125
     1126definition optional_cost : option costlabel → stmt → stmt ≝
     1127λo,s. match o with [ Some l ⇒ St_cost l s | None ⇒ s ].
     1128
    11261129let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (rettyp:option typ) (s:statement) on s
    11271130  : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) ≝
     
    11661169    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    11671170    ] e1'
    1168 | Swhile e1 s1
     1171| Swhile e1 s1 cl
    11691172    do e1' ← translate_expr vars e1;
    11701173    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
     
    11761179        let converted_loop ≝
    11771180          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)))
    11811182        in         
    11821183          OK ? «〈fgens2, converted_loop〉, ?»
     
    13391340                | 3,6: #H %2 assumption ] ]
    13401341try @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/
    13421344| (*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;
    13441346         elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label)
    13451347         @conj
     
    13471349         | 2,4: whd @or_intror normalize @Exists_append_l @Exists_append_l try @Exists_append_l
    13481350              @(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)
    13531356   #l * try * [ 1,5: #H %1 %1 normalize %2 @Exists_append_l @Exists_append_l try @Exists_append_l @H
    13541357              | 2,6: #H %1 %2 assumption
     
    13581361                                               | 2,4: * ]
    13591362              ]
    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/ ]
    13641368                   | 2: #H elim (Hlabels_tr1 label H)
    13651369                         #lab * #Hlookup #Hdef @(ex_intro … lab) @conj
    13661370                         [ 1: // | 2: whd %2 assumption ]
    13671371                   ]
    1368 | 15: @(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)
    13691373   #l * try * [ 1: #H %1 %1 normalize %2 @H
    13701374              | 2: #H %1 %2 assumption
    13711375              | 3: #H %2 assumption ]
    1372 | 16: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
     1376| 19: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
    13731377   #H @(Htmps_pres3 … (Htmps_pres2 … H))
    1374 | 18: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
     1378| 21: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
    13751379   #H @(Htmps_pres3 … H)
    1376 | 19: whd #l #H normalize in H;
     1380| 22: whd #l #H normalize in H;
    13771381      cases (Exists_append … H) #Hcase
    13781382      [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
     
    13951399        ]
    13961400      ]
    1397 | 20: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
    1398 | 21: @(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)
    13991403   #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H
    14001404              | 2: #H %1 %2 assumption
    14011405              | 3: #H %2 assumption ]
    1402 | 22: whd %1 %1 normalize /2/
    1403 | 23: @(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)
    14041408   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
    14051409                   @Exists_append_r @Exists_append_l @Exists_append_l
     
    14141418                     | 2: * ]
    14151419              ]
    1416 | 24: @(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)
    14171421   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
    14181422                   @Exists_append_r @Exists_append_l @Exists_append_l                   
     
    14261430                     | 2: * ]
    14271431              ]
    1428 | 25: whd %1 %1 normalize /2/
    1429 | 26: whd %1 %1 normalize
     1432| 28: whd %1 %1 normalize /2/
     1433| 29: whd %1 %1 normalize
    14301434      @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r
    14311435      whd %1 //
    1432 | 29: whd %1 %2 whd @(ex_intro … l) @E
     1436| 32: whd %1 %2 whd @(ex_intro … l) @E
    14331437] qed.
    14341438
Note: See TracChangeset for help on using the changeset viewer.