Changeset 1312 for src/LIN/semantics.ma
- Timestamp:
- Oct 6, 2011, 10:35:29 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/semantics.ma
r1304 r1312 1 1 include "joint/SemanticUtils.ma". 2 2 include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *) 3 4 definition lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.5 definition lin_pop_frame: unit → res unit ≝ λ_. OK … it.6 definition lin_save_frame: unit → hw_register_env → unit ≝ λ_.λ_. it.7 3 8 4 (*CSC: XXXX*) … … 13 9 definition lin_more_sem_params: more_sem_params lin_params_ := 14 10 mk_more_sem_params lin_params_ 15 unit hw_register_env lin_succ_pc lin_pop_frame lin_save_frame11 unit hw_register_env lin_succ_pc 16 12 hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA) 17 13 (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB) … … 28 24 pointer_of_label. 29 25 definition lin_sem_params: sem_params ≝ mk_sem_params … lin_more_sem_params. 26 27 definition 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. 30 31 definition lin_more_sem_params1 : more_sem_params1 … lin_params1 ≝ 32 mk_more_sem_params1 ? lin_params1 lin_more_sem_params 33 lin_init_locals lin_pop_frame lin_save_frame. 30 34 31 35 (*CSC: XXXXXXXXXX *) … … 45 49 definition lin_more_sem_params2: ∀globals. more_sem_params2 … (lin_params globals) ≝ 46 50 λglobals. 47 mk_more_sem_params2 … lin_more_sem_params lin_init_locals51 mk_more_sem_params2 … lin_more_sem_params1 48 52 (lin_fetch_statement …) lin_fetch_result lin_fetch_external_args lin_set_result 49 53 (lin_exec_extended …).
Note: See TracChangeset
for help on using the changeset viewer.