- Timestamp:
- Oct 16, 2011, 7:42:25 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/joint_LTL_LIN_semantics.ma
r1383 r1384 28 28 definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e. 29 29 definition ltl_lin_pop_frame: 30 ∀succT,succ,pointer_of_label. state … (ltl_lin_sem_params succT succ pointer_of_label) → res ( (state … (ltl_lin_sem_params … succ pointer_of_label)) × address) ≝31 λ_.λ_.λ_. fetch_ra ….30 ∀succT,succ,pointer_of_label. state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝ 31 λ_.λ_.λ_.λt.OK … t. 32 32 definition ltl_lin_save_frame: 33 33 ∀succT,succ,pointer_of_label. address → nat → unit → nat → unit → state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝ … … 55 55 λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals. 56 56 mk_more_sem_params2 … (ltl_lin_more_sem_params1 … succ pointer_of_label) 57 (fetch globals) (ltl_lin_fetch_result …) (ltl_lin_fetch_external_args …) 57 (fetch globals) (load_ra …) (ltl_lin_fetch_result …) 58 (ltl_lin_fetch_external_args …) 58 59 (ltl_lin_set_result …) (ltl_lin_exec_extended …). 59 60
Note: See TracChangeset
for help on using the changeset viewer.