Changeset 2353 for src/Clight/Csyntax.ma


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

    r2176 r2353  
    194194  | Ssequence : statement → statement → statement  (**r sequence *)
    195195  | Sifthenelse : expr  → statement → statement → statement (**r conditional *)
    196   | Swhile : expr → statement → statement   (**r [while] loop *)
     196  | Swhile : expr → statement → option costlabel → statement   (**r [while] loop *)
    197197  | Sdowhile : expr → statement → statement (**r [do] loop *)
    198198  | Sfor: statement → expr → statement → statement → statement (**r [for] loop *)
     
    226226  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    227227  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    228   (Swh:∀e,s. P s → P (Swhile e s))
     228  (Swh:∀e,s,l. P s → P (Swhile e s l))
    229229  (Sdo:∀e,s. P s → P (Sdowhile e s))
    230230  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     
    249249    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    250250    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    251 | Swhile e s ⇒ Swh e s
     251| Swhile e s cl ⇒ Swh e s cl
    252252    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    253253| Sdowhile e s ⇒ Sdo e s
     
    275275  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    276276  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    277   (Swh:∀e,s. P s → P (Swhile e s))
     277  (Swh:∀e,s,l. P s → P (Swhile e s l))
    278278  (Sdo:∀e,s. P s → P (Sdowhile e s))
    279279  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
Note: See TracChangeset for help on using the changeset viewer.