Changeset 1313


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

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

Location:
src
Files:
2 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 …).
  • src/RTL/semantics.ma

    r1303 r1313  
    99include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
    1010
    11 (*CSC: XXXXX *)
    12 axiom rtl_init_locals : list register → register_env beval → register_env beval.
    13 axiom rtl_pop_frame: unit → res unit.
    14 axiom rtl_save_frame: unit → register_env beval → unit.
    15 
    1611definition rtl_more_sem_params: more_sem_params rtl_params_ :=
    1712 mk_more_sem_params rtl_params_
    18   unit(*framesT*) (register_env beval) graph_succ_p rtl_pop_frame rtl_save_frame
     13  unit(*framesT*) (register_env beval) graph_succ_p
    1914   reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve
    2015    reg_store reg_retrieve reg_store reg_retrieve
     
    2520definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
    2621
     22(*CSC: XXXXX *)
     23axiom rtl_init_locals : list register → register_env beval → register_env beval.
     24axiom rtl_pop_frame: state … rtl_sem_params → res (state … rtl_sem_params).
     25axiom rtl_save_frame: state … rtl_sem_params → state … rtl_sem_params.
     26
     27definition rtl_more_sem_params1 : more_sem_params1 … rtl_params1 ≝
     28 mk_more_sem_params1 ? rtl_params1 rtl_more_sem_params
     29  rtl_init_locals rtl_pop_frame rtl_save_frame.
     30
     31
    2732(*CSC: XXXXX, for is_final only *)
    2833axiom rtl_fetch_result: state rtl_sem_params → nat → res val.
     
    3641definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
    3742 λglobals.
    38   mk_more_sem_params2 … rtl_more_sem_params rtl_init_locals
     43  mk_more_sem_params2 … rtl_more_sem_params1
    3944   (graph_fetch_statement …) rtl_fetch_result rtl_fetch_external_args rtl_set_result
    4045    (rtl_exec_extended …).
Note: See TracChangeset for help on using the changeset viewer.