Ignore:
Timestamp:
Oct 9, 2012, 3:10:07 PM (8 years ago)
Author:
campbell
Message:

Revert "Put the post-loop cost label into the Clight while statement ..."
Rely on the Cminor to RTLabs stage ignoring Cminor skips instead.
This reverts commit 2353.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2387 r2391  
    7878| Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2
    7979| Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2
    80 | Swhile e body _ ⇒ switch_free body
     80| Swhile e body ⇒ switch_free body
    8181| Sdowhile e body ⇒ switch_free body
    8282| Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3
     
    249249  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
    250250  ret 〈Sifthenelse e s1' s2', acc1 @ acc2, fvs'', u''〉
    251 | Swhile e body cl
     251| Swhile e body
    252252  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
    253   ret 〈Swhile e body' cl, acc, fvs', u'〉
     253  ret 〈Swhile e body', acc, fvs', u'〉
    254254| Sdowhile e body ⇒
    255255  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
     
    318318  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
    319319  〈fvs @ fvs', u''〉
    320 | Swhile e body cl
     320| Swhile e body
    321321  mk_fresh_variables body u
    322322| Sdowhile e body ⇒
     
    367367  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    368368  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    369   (Swh:∀e,s,cl. P s → P (Swhile e s cl))
     369  (Swh:∀e,s. P s → P (Swhile e s))
    370370  (Sdo:∀e,s. P s → P (Sdowhile e s))
    371371  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     
    390390    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    391391    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    392 | Swhile e s cl ⇒ Swh e s cl
     392| Swhile e s ⇒ Swh e s
    393393    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    394394| Sdowhile e s ⇒ Sdo e s
     
    416416  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    417417  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    418   (Swh:∀e,s,cl. P s → P (Swhile e s cl))
     418  (Swh:∀e,s. P s → P (Swhile e s))
    419419  (Sdo:∀e,s. P s → P (Sdowhile e s))
    420420  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     
    472472         (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
    473473         (ret_u statement s2')))} % try //
    474 | 6: #e #s #cl #H #u0 #u1 #post normalize
     474| 6: #e #s #H #u0 #u1 #post normalize
    475475     elim (H u0 u1 post) #s1' * normalize
    476476     cases (mk_fresh_variables s u0) #fvs #u'
    477477     #Heq1 #Heq1_fvs >Heq1 normalize nodelta
    478      %{(mk_swret statement (Swhile e (ret_st statement s1') cl) (ret_acc statement s1')
     478     %{(mk_swret statement (Swhile e (ret_st statement s1')) (ret_acc statement s1')
    479479        (ret_fvs statement s1') (ret_u statement s1'))} % try //
    480480| 7: #e #s #H #u0 #u1 #post normalize
     
    628628| Sifthenelse e s1 s2 ⇒
    629629  max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2))
    630 | Swhile e body _
     630| Swhile e body
    631631  max_id (max_of_expr e) (max_of_statement body)
    632632| Sdowhile e body ⇒
     
    712712| Ssequence sub1 sub2 ⇒ P sub1 ∧ P sub2
    713713| Sifthenelse e sub1 sub2 ⇒ P sub1 ∧ P sub2
    714 | Swhile e sub _ ⇒ Q e ∧ P sub
     714| Swhile e sub ⇒ Q e ∧ P sub
    715715| Sdowhile e sub ⇒ Q e ∧ P sub
    716716| Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3
     
    21942194    switch_removal s fvs u = Some ? result →
    21952195    switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k')
    2196 | swc_while : ∀fvs,e,s,optlab,k,k',u,result.
    2197     fresh_for_statement (Swhile e s optlab) u →
     2196| swc_while : ∀fvs,e,s,k,k',u,result.
     2197    fresh_for_statement (Swhile e s) u →
    21982198    switch_cont_sim fvs k k' →
    21992199    switch_removal s fvs u = Some ? result →
    2200     switch_cont_sim fvs (Kwhile e s optlab k) (Kwhile e (ret_st ? result) optlab k')
     2200    switch_cont_sim fvs (Kwhile e s k) (Kwhile e (ret_st ? result) k')
    22012201| swc_dowhile : ∀fvs,e,s,k,k',u,result.
    22022202    fresh_for_statement (Sdowhile e s) u →
     
    28012801qed. *)
    28022802
    2803 lemma while_fresh_lift : ∀e,s,cl,u.
    2804    fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s cl) u.
    2805 #e #s #cl * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ???));
     2803lemma while_fresh_lift : ∀e,s,u.
     2804   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u.
     2805#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ??));
    28062806cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
    28072807cases (leb e s) try /2/
Note: See TracChangeset for help on using the changeset viewer.