Changeset 1359 for src/LIN


Ignore:
Timestamp:
Oct 11, 2011, 6:00:03 PM (8 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/LIN/semantics.ma

    r1324 r1359  
    2626
    2727definition lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    28 definition lin_pop_frame: state … lin_sem_params → res (state … lin_sem_params) ≝ λst. OK … st.
    29 definition lin_save_frame: state … lin_sem_params → state … lin_sem_params ≝ λst.st.
     28definition lin_pop_frame: list beval → state … lin_sem_params → res (state … lin_sem_params) ≝ λ_.λst. OK … st.
     29definition lin_save_frame: unit → state … lin_sem_params → state … lin_sem_params ≝ λ_.λst.st.
    3030
    3131definition lin_more_sem_params1 : more_sem_params1 … lin_params1 ≝
     
    3737
    3838(*CSC: XXXXX, for is_final only *)
    39 axiom lin_fetch_result: state lin_sem_params → nat → res val.
     39axiom lin_fetch_result: state lin_sem_params → res (list beval).
    4040
    4141(*CSC: XXXX, for external functions only*)
Note: See TracChangeset for help on using the changeset viewer.