Ignore:
Timestamp:
Jan 25, 2011, 6:22:21 PM (8 years ago)
Author:
campbell
Message:

Tcomp_ptr should take the memory region and use that to calculate its size.

File:
1 edited

Legend:

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

    r399 r481  
    66ncases v; ##[ ##2: #i ##| ##3: #f ##| ##4: #sp b of ##]
    77nwhd; ##[ ##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: #id ##]
     8ncases 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 ##]
    99#H; nwhd in H:(??%?); ndestruct;
    1010##[ ##1,4: nlapply (eq_spec i zero); nelim (eq i zero);
     
    3535nlapply (eq_spec i zero); ncases (eq i zero);
    3636##[ #e; nrewrite > e;
    37     ncases ty; ##[ ##| #sz sg ##| #fs ##| #sp ty ##| #sp ty n ##| #args rty ##| #id fs ##| #id fs ##| #id ##]
     37    ncases ty; ##[ ##| #sz sg ##| #fs ##| #sp ty ##| #sp ty n ##| #args rty ##| #id fs ##| #id fs ##| #r id ##]
    3838    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: #id' ##]
     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' ##]
    4040    nwhd in ⊢ (??%? → ?); #H; ndestruct (H);
    4141    ##[ ##1,5,9: napply cast_ip_z ##| ##*: napply cast_pp_z ##] //;
     
    5050##| #i; ncases ty;
    5151  ##[ #H; nwhd in H:(??%?); ndestruct;
    52   ##| ##3,9: #a; #H; nwhd in H:(??%?); ndestruct;
    53   ##| ##7,8: #a b; #H; nwhd in H:(??%?); ndestruct;
     52  ##| ##3: #a; #H; nwhd in H:(??%?); ndestruct;
     53  ##| ##7,8,9: #a b; #H; nwhd in H:(??%?); ndestruct;
    5454  ##| #sz1 si1; ncases ty';
    5555    ##[ #H; nwhd in H:(??%?); ndestruct;
    56     ##| ##3,9: #a; #H; nwhd in H:(??%?); ndestruct; //
    57     ##| ##2,7,8: #a b; #H; nwhd in H:(??%?); ndestruct; //
     56    ##| ##3: #a; #H; nwhd in H:(??%?); ndestruct; //
     57    ##| ##2,7,8,9: #a b; #H; nwhd in H:(??%?); ndestruct; //
    5858    ##| ##4,5,6: ##[ #sp ty''; nletin t ≝ (Tpointer sp ty'')
    5959                 ##| #sp ty'' n; nletin t ≝ (Tarray sp ty'' n)
     
    7676        ##]
    7777  ##]
    78 ##| #f; ncases ty;  ##[ ##3,9: #x; ##| ##2,4,6,7,8: #x y; ##| ##5: #x y z; ##]
    79                     ##[ ncases ty'; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
     78##| #f; ncases ty;  ##[ ##3: #x; ##| ##2,4,6,7,8,9: #x y; ##| ##5: #x y z; ##]
     79                    ##[ ncases ty'; ##[ #e; ##| ##3: #a e; ##| ##2,4,6,7,8,9: #a b e; ##| #a b c e; ##]
    8080                        nwhd in e:(??%?); ndestruct; //;
    8181                    ##| ##*: #e; nwhd in e:(??%?); ndestruct
     
    8686    nelim (bind_inversion ????? e''); #s'; *; #es' e''';
    8787    ncut (type_space ty s);
    88     ##[ ncases ty in es:(??%?) ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
     88    ##[ ncases ty in es:(??%?) ⊢ %; ##[ #e; ##| ##3: #a e; ##| ##2,4,6,7,8,9: #a b e; ##| #a b c e; ##]
    8989        nwhd in e:(??%?); ndestruct; //;
    9090    ##| #Hty;
    9191        ncut (type_space ty' s');
    92         ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
     92        ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3: #a e; ##| ##2,4,6,7,8,9: #a b e; ##| #a b c e; ##]
    9393            nwhd in e:(??%?); ndestruct; //;
    9494        ##| #Hty';
Note: See TracChangeset for help on using the changeset viewer.