- Timestamp:
- Oct 6, 2011, 10:35:29 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/semantics.ma
r1303 r1312 4 4 (*CSC: XXXXX *) 5 5 axiom ertl_init_locals : list register → (register_env beval) × hw_register_env → (register_env beval) × hw_register_env. 6 axiom ertl_pop_frame: unit → res unit. 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)). 7 8 axiom ertl_save_frame: unit → (register_env beval) × hw_register_env → unit. 8 9 … … 25 26 definition ertl_more_sem_params: more_sem_params ertl_params_ := 26 27 mk_more_sem_params ertl_params_ 27 unit(*framesT*) ((register_env beval) × hw_register_env) graph_succ_p ertl_pop_frame ertl_save_frame28 (list (register_env beval)) ((register_env beval) × hw_register_env) graph_succ_p ertl_pop_frame ertl_save_frame 28 29 ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve 29 30 ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
Note: See TracChangeset
for help on using the changeset viewer.