Changeset 1377 for src/ERTL


Ignore:
Timestamp:
Oct 14, 2011, 7:22:59 PM (8 years ago)
Author:
sacerdot
Message:

pop_frame now incorporates the fetch_result (that made sense only for RTL).
pop_frame and save_frame are now also more symmetric

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1372 r1377  
    4343(*CSC: could we use here a dependent type to avoid the Error case? *)
    4444axiom EmptyStack: String.
    45 definition ertl_pop_frame: list beval → state … ertl_sem_params → res (state … ertl_sem_params) ≝
    46  λ_.λst.
     45definition ertl_pop_frame: state … ertl_sem_params → res ((state … ertl_sem_params) × address) ≝
     46 λst.
     47  do 〈st,ra〉 ← fetch_ra … st;
    4748  let frms ≝ st_frms ? st in
    4849  match frms with
    4950  [ nil ⇒ Error ? [MSG EmptyStack]
    5051  | cons hd tl ⇒
    51      OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
    52 
    53 definition ertl_save_frame: nat → nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
    54  λ_.λ_.λ_.λ_.λst.
     52     OK … (〈set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st),ra〉) ].
     53
     54definition ertl_save_frame:
     55 address → nat → nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
     56 λl.λ_.λ_.λ_.λ_.λst.
     57  do st ← save_ra … st l ;
    5558  OK …
    5659   (set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st))
Note: See TracChangeset for help on using the changeset viewer.