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

    r2176 r2353  
    383383    >(yields_eq ??? (bool_of_false ?? H2))
    384384    @refl
    385 | #f #e #s #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
    386     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    387     >(yields_eq ??? (bool_of_false ?? H2))
    388     @refl
    389 | #f #e #s #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
    390     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    391     >(yields_eq ??? (bool_of_true ?? H2))
    392     @refl
    393 | #f #s1 #e #s2 #k #env #m #H cases H; #es1 >es1 @refl
    394 | 13,14: #f #e #s #k #env #m @refl
     385| #f #e #s #cl #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     386    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     387    >(yields_eq ??? (bool_of_false ?? H2))
     388    @refl
     389| #f #e #s #cl #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     390    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     391    >(yields_eq ??? (bool_of_true ?? H2))
     392    @refl
     393| #f #s1 #e #s2 #cl #k #env #m #H cases H; #es1 >es1 @refl
     394| 13,14: #f #e #s [#cl] #k #env #m @refl
    395395| #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?);
    396396    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     
    424424    [ #H1 #H2 whd in ⊢ (??%?); >H2 @refl
    425425    | #s' #k' whd in ⊢ (% → ?); *;
    426     | 3,4: #e' #s' #k' whd in ⊢ (% → ?); *;
     426    | 3,4: #e' #s' [#cl] #k' whd in ⊢ (% → ?); *;
    427427    | 5,6: #e' #s1' #s2' #k' whd in ⊢ (% → ?); *;
    428428    | #k' whd in ⊢ (% → ?); *;
Note: See TracChangeset for help on using the changeset viewer.