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

Separate out null values from integer zeros.

File:
1 edited

Legend:

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

    r481 r484  
    44 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
    55#v ty r;
    6 ncases v; ##[ ##2: #i ##| ##3: #f ##| ##4: #sp b of ##]
    7 nwhd; ##[ ##4: #H; nwhd in H:(??%?); ndestruct ##]
    8 ncases ty; ##[ ##2,11,20: #sz sg ##| ##3,12,21: #sz ##| ##4,13,22: #sp ty ##| ##5,14,23: #sp ty n ##| ##6,15,24: #args rty ##| ##7,8,16,17,25,26: #id fs ##| ##9,18,27: #r id ##]
     6ncases v; ##[ ##| #i ##| #f ##| #r1 ##| #r b of ##]
     7ncases ty; ##[ ##2,11,20,29,38: #sz sg ##| ##3,12,21,30,39: #sz ##| ##4,13,22,31,40: #r ty ##| ##5,14,23,32,41: #r ty n ##| ##6,15,24,33,42: #args rty ##| ##7,8,16,17,25,26,34,35,43,44: #id fs ##| ##9,18,27,36,45: #r id ##]
    98#H; nwhd in H:(??%?); ndestruct;
    10 ##[ ##1,4: nlapply (eq_spec i zero); nelim (eq i zero);
    11   ##[ ##1,3: #e; nrewrite > e; napply bool_of_val_false; //;
    12   ##| ##2,4: #ne; napply bool_of_val_true; /2/;
    13   ##]
    14 ##| ##3: nelim (eq_dec f Fzero);
     9##[ nlapply (eq_spec i zero); nelim (eq i zero);
     10  ##[ #e; nrewrite > e; napply bool_of_val_false; //;
     11  ##| #ne; napply bool_of_val_true; /2/;
     12  ##]
     13##| nelim (eq_dec f Fzero);
    1514  ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); napply bool_of_val_false; //;
    1615  ##| #ne; nrewrite > (Feq_zero_false …); //; napply bool_of_val_true; /2/;
    1716  ##]
    18 ##| ##2,5: napply bool_of_val_true; //
     17##| napply bool_of_val_false; //
     18##| napply bool_of_val_true; //
    1919##] nqed.
    2020
     
    3636##[ #e; nrewrite > e;
    3737    ncases ty; ##[ ##| #sz sg ##| #fs ##| #sp ty ##| #sp ty n ##| #args rty ##| #id fs ##| #id fs ##| #r id ##]
    38     nwhd in ⊢ (??%? → ?); ##[ ##1,3,7,8,9: #H; ndestruct ##]
    39     ncases ty'; ##[ ##2,11,20,29: #sz' sg' ##| ##3,12,21,30: #sz' ##| ##4,13,22,31: #sp' ty' ##| ##5,14,23,32: #sp' ty' n' ##| ##6,15,24,33: #args' res' ##| ##7,8,16,17,25,26,34,35: #id' fs' ##| ##9,18,27,36: #r id' ##]
    40     nwhd in ⊢ (??%? → ?); #H; ndestruct (H);
    41     ##[ ##1,5,9: napply cast_ip_z ##| ##*: napply cast_pp_z ##] //;
     38    nwhd in ⊢ (??%? → ?); #H; ndestruct;
     39    ncases ty' in H ⊢ %; ##[ ##| #sz sg ##| #fs ##| #sp ty ##| #sp ty n ##| #args rty ##| #id fs ##| #id fs ##| #r id ##]
     40    nwhd in ⊢ (??%? → ?); #H; ndestruct (H); napply cast_ip_z; //;
    4241##| #_; nwhd in ⊢ (??%? → ?); #H; ndestruct
    4342##]
     
    8180                    ##| ##*: #e; nwhd in e:(??%?); ndestruct
    8281                    ##]
     82##| #r; ncases ty; ##[ ##3: #x; ##| ##2,4,6,7,8,9: #x y; ##| ##5: #x y z; ##]
     83    nwhd in ⊢ (??%? → ?); #H; ndestruct; ncases (eq_region_dec r ?) in H;
     84    nwhd in ⊢ (? → ??%? → ?); #H1 H2; ndestruct;
     85    ncases ty' in H2; nnormalize; ntry #a; ntry #b; ntry #c; ntry #d; ndestruct;
     86    napply cast_pp_z; //;
    8387##| #sp b of; nwhd in ⊢ (??%? → ?); #e;
    8488    nelim (bind_inversion ????? e); #s; *; #es e';
    8589    nelim (bind_inversion ????? e'); #u; *; #eu e'';
    8690    nelim (bind_inversion ????? e''); #s'; *; #es' e''';
    87     ncut (type_space ty s);
     91    ncut (type_region ty s);
    8892    ##[ ncases ty in es:(??%?) ⊢ %; ##[ #e; ##| ##3: #a e; ##| ##2,4,6,7,8,9: #a b e; ##| #a b c e; ##]
    8993        nwhd in e:(??%?); ndestruct; //;
    9094    ##| #Hty;
    91         ncut (type_space ty' s');
     95        ncut (type_region ty' s');
    9296        ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3: #a e; ##| ##2,4,6,7,8,9: #a b e; ##| #a b c e; ##]
    9397            nwhd in e:(??%?); ndestruct; //;
    9498        ##| #Hty';
    95             ncut (s = sp). nelim (ms_eq_dec sp s) in eu; //; nnormalize; #_; #e; ndestruct.
     99            ncut (s = sp). nelim (eq_region_dec sp s) in eu; //; nnormalize; #_; #e; ndestruct.
    96100            #e; nrewrite < e;
    97101            nwhd in match (is_pointer_compat ??) in e''';
Note: See TracChangeset for help on using the changeset viewer.