Changeset 152


Ignore:
Timestamp:
Oct 6, 2010, 2:20:22 PM (9 years ago)
Author:
campbell
Message:

Force whd form for memory during execution

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r127 r152  
    875875  | S n' ⇒ Some ? (
    876876      ! 〈t,s'〉 ← exec_step ge s;:
    877       ! 〈t',s''〉 ← exec_steps n' ge s';:
     877(*      ! 〈t,s'〉 ← match s with
     878                 [ State f s k e m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (State f s k e (mk_mem c n p)) ]
     879                 | Callstate fd args k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Callstate fd args k (mk_mem c n p)) ]
     880                 | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Returnstate r k (mk_mem c n p)) ]
     881                 ] ;:*)
     882      ! 〈t',s''〉 ← match s' with
     883                 [ State f s k e m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (State f s k e (mk_mem c n p)) ]
     884                 | Callstate fd args k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Callstate fd args k (mk_mem c n p)) ]
     885                 | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Returnstate r k (mk_mem c n p)) ]
     886                 ] ;:
     887(*      ! 〈t',s''〉 ← exec_steps n' ge s';:*)
    878888      ret ? 〈t ⧺ t',s''〉)
    879889  ]
    880890]. nwhd; /2/;
    881 napply sig_bindIO2_OK; #t s' H1;
     891napply sig_bindIO2_OK; #t s'; ncases s'; ##[ #f st k e m; ##| #fd args k m; ##| #r k m; ##]
     892nwhd in ⊢ (? → ?????(??????%?));
     893ncases m; #mc mn mp; #H1;
     894nwhd in ⊢ (?????(??????%?));
    882895napply sig_bindIO2_OK; #t' s'' IH;
    883896nwhd; napply (star_step … IH); //;
Note: See TracChangeset for help on using the changeset viewer.