Ignore:
Timestamp:
Jan 28, 2011, 2:41:49 PM (8 years ago)
Author:
campbell
Message:

Separate out null values from integer zeros.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/CexecComplete.ma

    r481 r484  
    4949##] nqed.
    5050
    51 nlemma ms_eq_dec_true: ∀s. ms_eq_dec s s = inl ???.
     51nlemma eq_region_dec_true: ∀s. eq_region_dec s s = inl ???.
    5252##[ #s; ncases s; napply refl;
    5353##| ##skip
     
    100100    nelim H1; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #tys1 ty1; nletin sp1 ≝ Code ##]
    101101    nwhd in ⊢ (??%?);
    102     ##[ ##1,2: nrewrite > (ms_eq_dec_true …); nwhd in ⊢ (??%?); ##]
     102    ##[ ##1,2: nrewrite > (eq_region_dec_true …); nwhd in ⊢ (??%?); ##]
    103103    nelim H2 in H3 ⊢ %; ##[ ##1,4,7: #sp2 ty2 ##| ##2,5,8: #sp2 ty2 n2 ##| ##3,6,9: #tys2 ty2; nletin sp2 ≝ Code ##]
    104104    #H3; nwhd in ⊢ (??%?);
    105105    nrewrite > (is_pointer_compat_true …); //;
    106 ##| #m sz si ty'' H; ncases H; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #args rty ##] napply refl;
    107 ##| #m t t' H H'; ncases H; ncases H'; //;
     106##| #m sz si ty'' r H; ncases H; //;
     107##| #m t t' r r' H H'; ncases H; ntry #a; ntry #b; ntry #c; ncases H'; ntry #d; ntry #e; ntry #f;
     108    nwhd in ⊢ (??%?); ntry napply refl; nrewrite > eq_region_dec_true; napply refl;
    108109##] nqed.
    109110
     
    125126  ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
    126127  ##| #p b i i0 s; @ true; @; //
    127   ##| #i p t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
    128   ##| #p b i p0 t0; @ true; @; //
    129128  ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //;
    130129  ##| #i s; @ false; @; //;
    131   ##| #p t; @ false; @; //;
     130  ##| #r r' t; @ false; @; //;
    132131  ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //;
    133132  ##]
     
    138137  ##[ #i is s ne; nwhd; nrewrite > (eq_false … ne); //;
    139138  ##| #p b i i0 s; //
    140   ##| #i p t ne; nwhd; nrewrite > (eq_false … ne); //;
    141   ##| #p b i p0 t0; //
    142139  ##| #f s ne; nwhd; nrewrite > (Feq_zero_false … ne); //;
    143140  ##]
     
    147144#v ty H; nelim H;
    148145  ##[ #i s; //;
    149   ##| #p t; //;
     146  ##| #r r' t; //;
    150147  ##| #s; nwhd; nrewrite > (Feq_zero_true …); //;
    151148  ##]
Note: See TracChangeset for help on using the changeset viewer.