Changeset 1312 for src/LTL/semantics.ma
- Timestamp:
- Oct 6, 2011, 10:35:29 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LTL/semantics.ma
r1303 r1312 2 2 include "LTL/LTL.ma". (* CSC: syntax.ma in RTLabs *) 3 3 4 definition ltl_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.5 definition ltl_pop_frame: unit → res unit ≝ λ_. OK … it.6 definition ltl_save_frame: unit → hw_register_env → unit ≝ λ_.λ_. it.7 8 4 definition ltl_more_sem_params: more_sem_params ltl_params_ := 9 5 mk_more_sem_params ltl_params_ 10 unit hw_register_env graph_succ_p ltl_pop_frame ltl_save_frame6 unit hw_register_env graph_succ_p 11 7 hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA) 12 8 (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB) … … 24 20 definition ltl_sem_params: sem_params ≝ mk_sem_params … ltl_more_sem_params. 25 21 22 definition ltl_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e. 23 definition ltl_pop_frame: state … ltl_sem_params → res (state … ltl_sem_params) ≝ λst. OK … st. 24 definition ltl_save_frame: state … ltl_sem_params → state … ltl_sem_params ≝ λst.st. 25 26 definition ltl_more_sem_params1 : more_sem_params1 … ltl_params1 ≝ 27 mk_more_sem_params1 ? ltl_params1 ltl_more_sem_params 28 ltl_init_locals ltl_pop_frame ltl_save_frame. 29 26 30 (*CSC: XXXXX, for is_final only *) 27 31 axiom ltl_fetch_result: state ltl_sem_params → nat → res val. … … 37 41 definition ltl_more_sem_params2: ∀globals. more_sem_params2 … (ltl_params globals) ≝ 38 42 λglobals. 39 mk_more_sem_params2 … ltl_more_sem_params ltl_init_locals43 mk_more_sem_params2 … ltl_more_sem_params1 40 44 (graph_fetch_statement …) ltl_fetch_result ltl_fetch_external_args ltl_set_result 41 45 (ltl_exec_extended …).
Note: See TracChangeset
for help on using the changeset viewer.