Changeset 1312 for src/LIN/semantics.ma


Ignore:
Timestamp:
Oct 6, 2011, 10:35:29 PM (8 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/semantics.ma

    r1304 r1312  
    11include "joint/SemanticUtils.ma".
    22include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *)
    3 
    4 definition lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    5 definition lin_pop_frame: unit → res unit ≝ λ_. OK … it.
    6 definition lin_save_frame: unit → hw_register_env → unit ≝ λ_.λ_. it.
    73
    84(*CSC: XXXX*)
     
    139definition lin_more_sem_params: more_sem_params lin_params_ :=
    1410 mk_more_sem_params lin_params_
    15   unit hw_register_env lin_succ_pc lin_pop_frame lin_save_frame
     11  unit hw_register_env lin_succ_pc
    1612   hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
    1713    (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
     
    2824     pointer_of_label.
    2925definition lin_sem_params: sem_params ≝ mk_sem_params … lin_more_sem_params.
     26
     27definition lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
     28definition lin_pop_frame: state … lin_sem_params → res (state … lin_sem_params) ≝ λst. OK … st.
     29definition lin_save_frame: state … lin_sem_params → state … lin_sem_params ≝ λst.st.
     30
     31definition lin_more_sem_params1 : more_sem_params1 … lin_params1 ≝
     32 mk_more_sem_params1 ? lin_params1 lin_more_sem_params
     33  lin_init_locals lin_pop_frame lin_save_frame.
    3034
    3135(*CSC: XXXXXXXXXX *)
     
    4549definition lin_more_sem_params2: ∀globals. more_sem_params2 … (lin_params globals) ≝
    4650 λglobals.
    47   mk_more_sem_params2 … lin_more_sem_params lin_init_locals
     51  mk_more_sem_params2 … lin_more_sem_params1
    4852   (lin_fetch_statement …) lin_fetch_result lin_fetch_external_args lin_set_result
    4953    (lin_exec_extended …).
Note: See TracChangeset for help on using the changeset viewer.