Changeset 1384 for src/ERTL/semantics.ma

Timestamp:

Oct 16, 2011, 7:42:25 PM (9 years ago)

Author:

sacerdot

Message:

• fetch_ra taken out of pop_frame again since it is used uniformly and it is also required for is_final
• fetch_ra made abstract since it gets a different implementation in RTL
• old fetch_ra renamed into load_ra (to match the save_ra name)

File:

• src/ERTL/semantics.ma (modified) (2 diffs)

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: state … ertl_sem_params → res ((state … ertl_sem_params) × address) ≝
+definition ertl_pop_frame: state … ertl_sem_params → res (state … ertl_sem_params) ≝
  λ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),ra〉) ].
+     OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
 
 definition ertl_save_frame:
@@ -118 +117 @@
  λglobals.
   mk_more_sem_params2 … ertl_more_sem_params1
-   (graph_fetch_statement …) ertl_fetch_result ertl_fetch_external_args ertl_set_result
-    (ertl_exec_extended …).
+   (graph_fetch_statement …) (load_ra …) ertl_fetch_result
+    ertl_fetch_external_args ertl_set_result (ertl_exec_extended …).
 
 definition ertl_fullexec ≝