Changeset 1377 for src/ERTL/semantics.ma

Timestamp:

Oct 14, 2011, 7:22:59 PM (10 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:

• src/ERTL/semantics.ma (modified) (1 diff)

src/ERTL/semantics.ma

@@ -43 +43 @@
 (*CSC: could we use here a dependent type to avoid the Error case? *)
 axiom EmptyStack: String.
-definition ertl_pop_frame: list beval → state … ertl_sem_params → res (state … ertl_sem_params) ≝
- λ_.λst.
+definition ertl_pop_frame: state … ertl_sem_params → res ((state … ertl_sem_params) × address) ≝
+ λst.
+  do 〈st,ra〉 ← fetch_ra … st;
   let frms ≝ st_frms ? st in
   match frms with
   [ nil ⇒ Error ? [MSG EmptyStack]
   | cons hd tl ⇒
-     OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
-
-definition ertl_save_frame: nat → nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
- λ_.λ_.λ_.λ_.λst.
+     OK … (〈set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st),ra〉) ].
+
+definition ertl_save_frame:
+ address → nat → nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
+ λl.λ_.λ_.λ_.λ_.λst.
+  do st ← save_ra … st l ;
   OK …
    (set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st))