Changeset 1313 for src/ERTL/semantics.ma


Ignore:
Timestamp:
Oct 6, 2011, 10:55:33 PM (9 years ago)
Author:
sacerdot
Message:

(E)RTL semantics ported to new data type for save/pop frame (but not implemented
yet)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1312 r1313  
    11include "joint/SemanticUtils.ma".
    22include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
    3 
    4 (*CSC: XXXXX *)
    5 axiom ertl_init_locals : list register → (register_env beval) × hw_register_env → (register_env beval) × hw_register_env.
    6 NON BASTA: DEBBO RIPRISTINARE IL LOCAL_ENV E IN RTL TANTE COSE!
    7 axiom ertl_pop_frame: list (register_env beval) → res (list (register_env beval)).
    8 axiom ertl_save_frame: unit → (register_env beval) × hw_register_env → unit.
    93
    104definition ps_reg_store ≝
     
    2620definition ertl_more_sem_params: more_sem_params ertl_params_ :=
    2721 mk_more_sem_params ertl_params_
    28   (list (register_env beval)) ((register_env beval) × hw_register_env) graph_succ_p ertl_pop_frame ertl_save_frame
     22  (list (register_env beval)) ((register_env beval) × hw_register_env) graph_succ_p
    2923   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
    3024    ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
     
    4034definition ertl_sem_params: sem_params ≝ mk_sem_params … ertl_more_sem_params.
    4135
     36(*CSC: XXXXX *)
     37axiom ertl_init_locals : list register → (register_env beval) × hw_register_env → (register_env beval) × hw_register_env.
     38axiom ertl_pop_frame: state … ertl_sem_params → res (state … ertl_sem_params).
     39axiom ertl_save_frame: state … ertl_sem_params → state … ertl_sem_params.
     40
     41definition ertl_more_sem_params1 : more_sem_params1 … ertl_params1 ≝
     42 mk_more_sem_params1 ? ertl_params1 ertl_more_sem_params
     43  ertl_init_locals ertl_pop_frame ertl_save_frame.
     44
    4245(*CSC: XXXXX, for is_final only *)
    4346axiom ertl_fetch_result: state ertl_sem_params → nat → res val.
     
    5154definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
    5255 λglobals.
    53   mk_more_sem_params2 … ertl_more_sem_params ertl_init_locals
     56  mk_more_sem_params2 … ertl_more_sem_params1
    5457   (graph_fetch_statement …) ertl_fetch_result ertl_fetch_external_args ertl_set_result
    5558    (ertl_exec_extended …).
Note: See TracChangeset for help on using the changeset viewer.