Changeset 1312 for src/LIN/semantics.ma

Timestamp:

Oct 6, 2011, 10:35:29 PM (9 years ago)

Author:

sacerdot

Message:

Type of frame operations (pop_frame/save_frame) generalized to take in account
the RTL semantics. LTL and LIN semantics fixed. Fixing of ERTL/RTL still to
be done.

File:

• src/LIN/semantics.ma (modified) (4 diffs)

src/LIN/semantics.ma

@@ -1 +1 @@
 include "joint/SemanticUtils.ma".
 include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *)
-
-definition lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
-definition lin_pop_frame: unit → res unit ≝ λ_. OK … it.
-definition lin_save_frame: unit → hw_register_env → unit ≝ λ_.λ_. it.
 
 (*CSC: XXXX*)
@@ -13 +9 @@
 definition lin_more_sem_params: more_sem_params lin_params_ :=
  mk_more_sem_params lin_params_
-  unit hw_register_env lin_succ_pc lin_pop_frame lin_save_frame
+  unit hw_register_env lin_succ_pc
    hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
     (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
@@ -28 +24 @@
      pointer_of_label.
 definition lin_sem_params: sem_params ≝ mk_sem_params … lin_more_sem_params.
+
+definition lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
+definition lin_pop_frame: state … lin_sem_params → res (state … lin_sem_params) ≝ λst. OK … st.
+definition lin_save_frame: state … lin_sem_params → state … lin_sem_params ≝ λst.st.
+
+definition lin_more_sem_params1 : more_sem_params1 … lin_params1 ≝
+ mk_more_sem_params1 ? lin_params1 lin_more_sem_params
+  lin_init_locals lin_pop_frame lin_save_frame.
 
 (*CSC: XXXXXXXXXX *)
@@ -45 +49 @@
 definition lin_more_sem_params2: ∀globals. more_sem_params2 … (lin_params globals) ≝
  λglobals.
-  mk_more_sem_params2 … lin_more_sem_params lin_init_locals
+  mk_more_sem_params2 … lin_more_sem_params1
    (lin_fetch_statement …) lin_fetch_result lin_fetch_external_args lin_set_result
     (lin_exec_extended …).