Ignore:
Timestamp:
Nov 22, 2010, 2:40:22 PM (9 years ago)
Author:
campbell
Message:

Begin separating soundness from executable semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIOcomplete.ma

    r239 r250  
    6161
    6262ntheorem the_initial_state:
    63   ∀p,s. initial_state p s → yieldsIO ?? (make_initial_state p) s.
     63  ∀p,s. initial_state p s → yieldsIObare ? (make_initial_state p) s.
    6464#p s; ncases p; #fns main globs H;
    65 napply remove_io_sig;
    6665ninversion H;
    6766#b f e1 e2 e3;
     67nwhd in ⊢ (??%?);
    6868nrewrite > e1;
    6969nwhd in ⊢ (??%?);
     
    8484
    8585nlemma cast_complete: ∀m,v,ty,ty',v'.
    86   cast m v ty ty' v' → yields ?? (exec_cast m v ty ty') v'.
     86  cast m v ty ty' v' → yieldsbare ? (exec_cast m v ty ty') v'.
    8787#m v ty ty' v' H;
    8888nelim H;
     
    9191##| #m i sz sz' sg; napply refl;
    9292##| #m f sz sz'; napply refl;
    93 ##| #m sp sp' ty ty' b ofs H1 H2 H3; napply remove_res_sig;
     93##| #m sp sp' ty ty' b ofs H1 H2 H3;
    9494    nelim H1; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #tys1 ty1; nletin sp1 ≝ Code ##]
    9595    nwhd in ⊢ (??%?);
Note: See TracChangeset for help on using the changeset viewer.