Changeset 1359 for src/ERTL


Ignore:
Timestamp:
Oct 11, 2011, 6:00:03 PM (9 years ago)
Author:
sacerdot
Message:
  1. more work on the RTL semantics
  2. changes to joint/semantics to accomodate the RTL one
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1329 r1359  
    11include "joint/SemanticUtils.ma".
    22include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
     3include alias "common/Identifiers.ma".
    34
    45definition ps_reg_store ≝
     
    4243(*CSC: could we use here a dependent type to avoid the Error case? *)
    4344axiom EmptyStack: String.
    44 definition ertl_pop_frame: state … ertl_sem_params → res (state … ertl_sem_params) ≝
    45  λst.
     45definition ertl_pop_frame: list beval → state … ertl_sem_params → res (state … ertl_sem_params) ≝
     46 λ_.λst.
    4647  let frms ≝ st_frms ? st in
    4748  match frms with
     
    5051     OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
    5152
    52 definition ertl_save_frame: state … ertl_sem_params → state … ertl_sem_params ≝
    53  λst.
     53definition ertl_save_frame: unit → state … ertl_sem_params → state … ertl_sem_params ≝
     54 λ_.λst.
    5455  set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st)) st.
    5556
     
    5960
    6061(*CSC: XXXXX, for is_final only *)
    61 axiom ertl_fetch_result: state ertl_sem_params → nat → res val.
     62axiom ertl_fetch_result: state ertl_sem_params → res (list beval).
    6263
    6364(*CSC: XXXX, for external functions only*)
Note: See TracChangeset for help on using the changeset viewer.