Changeset 1377 for src/ERTL/semantics.ma
- Timestamp:
- Oct 14, 2011, 7:22:59 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/semantics.ma
r1372 r1377 43 43 (*CSC: could we use here a dependent type to avoid the Error case? *) 44 44 axiom EmptyStack: String. 45 definition ertl_pop_frame: list beval → state … ertl_sem_params → res (state … ertl_sem_params) ≝ 46 λ_.λst. 45 definition ertl_pop_frame: state … ertl_sem_params → res ((state … ertl_sem_params) × address) ≝ 46 λst. 47 do 〈st,ra〉 ← fetch_ra … st; 47 48 let frms ≝ st_frms ? st in 48 49 match frms with 49 50 [ nil ⇒ Error ? [MSG EmptyStack] 50 51 | 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 54 definition 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 ; 55 58 OK … 56 59 (set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st))
Note: See TracChangeset
for help on using the changeset viewer.