Changeset 1313 for src/RTL


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)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.