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/switchRemoval.ma

    r2332 r2353  
    7777| Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2
    7878| Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2
    79 | Swhile e body ⇒ switch_free body
     79| Swhile e body _ ⇒ switch_free body
    8080| Sdowhile e body ⇒ switch_free body
    8181| Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3
     
    248248  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
    249249  ret 〈Sifthenelse e s1' s2', acc1 @ acc2, fvs'', u''〉
    250 | Swhile e body
     250| Swhile e body cl
    251251  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
    252   ret 〈Swhile e body', acc, fvs', u'〉
     252  ret 〈Swhile e body' cl, acc, fvs', u'〉
    253253| Sdowhile e body ⇒
    254254  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
     
    317317  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
    318318  〈fvs @ fvs', u''〉
    319 | Swhile e body
     319| Swhile e body cl
    320320  mk_fresh_variables body u
    321321| Sdowhile e body ⇒
     
    366366  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    367367  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    368   (Swh:∀e,s. P s → P (Swhile e s))
     368  (Swh:∀e,s,cl. P s → P (Swhile e s cl))
    369369  (Sdo:∀e,s. P s → P (Sdowhile e s))
    370370  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     
    389389    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    390390    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    391 | Swhile e s ⇒ Swh e s
     391| Swhile e s cl ⇒ Swh e s cl
    392392    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    393393| Sdowhile e s ⇒ Sdo e s
     
    415415  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    416416  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    417   (Swh:∀e,s. P s → P (Swhile e s))
     417  (Swh:∀e,s,cl. P s → P (Swhile e s cl))
    418418  (Sdo:∀e,s. P s → P (Sdowhile e s))
    419419  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     
    471471         (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
    472472         (ret_u statement s2')))} % try //
    473 | 6: #e #s #H #u0 #u1 #post normalize
     473| 6: #e #s #cl #H #u0 #u1 #post normalize
    474474     elim (H u0 u1 post) #s1' * normalize
    475475     cases (mk_fresh_variables s u0) #fvs #u'
    476476     #Heq1 #Heq1_fvs >Heq1 normalize nodelta
    477      %{(mk_swret statement (Swhile e (ret_st statement s1')) (ret_acc statement s1')
     477     %{(mk_swret statement (Swhile e (ret_st statement s1') cl) (ret_acc statement s1')
    478478        (ret_fvs statement s1') (ret_u statement s1'))} % try //
    479479| 7: #e #s #H #u0 #u1 #post normalize
     
    627627| Sifthenelse e s1 s2 ⇒
    628628  max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2))
    629 | Swhile e body
     629| Swhile e body _
    630630  max_id (max_of_expr e) (max_of_statement body)
    631631| Sdowhile e body ⇒
     
    711711| Ssequence sub1 sub2 ⇒ P sub1 ∧ P sub2
    712712| Sifthenelse e sub1 sub2 ⇒ P sub1 ∧ P sub2
    713 | Swhile e sub ⇒ Q e ∧ P sub
     713| Swhile e sub _ ⇒ Q e ∧ P sub
    714714| Sdowhile e sub ⇒ Q e ∧ P sub
    715715| Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3
     
    14151415    switch_removal s fvs u = Some ? result →
    14161416    switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k')
    1417 | swc_while : ∀fvs,e,s,k,k',u,result.
    1418     fresh_for_statement (Swhile e s) u →
     1417| swc_while : ∀fvs,e,s,cl,k,k',u,result.
     1418    fresh_for_statement (Swhile e s cl) u →
    14191419    switch_cont_sim fvs k k' →
    14201420    switch_removal s fvs u = Some ? result →
    1421     switch_cont_sim fvs (Kwhile e s k) (Kwhile e (ret_st ? result) k')
     1421    switch_cont_sim fvs (Kwhile e s cl k) (Kwhile e (ret_st ? result) cl k')
    14221422| swc_dowhile : ∀fvs,e,s,k,k',u,result.
    14231423    fresh_for_statement (Sdowhile e s) u →
     
    20482048qed. *)
    20492049
    2050 lemma while_fresh_lift : ∀e,s,u.
    2051    fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u.
    2052 #e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ??));
     2050lemma while_fresh_lift : ∀e,s,cl,u.
     2051   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s cl) u.
     2052#e #s #cl * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ???));
    20532053cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
    20542054cases (leb e s) try /2/
Note: See TracChangeset for help on using the changeset viewer.