- Timestamp:
- Oct 17, 2011, 1:40:13 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/joint_LTL_LIN_semantics.ma
r1384 r1385 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)) ≝ 31 λ_.λ_.λ_.λt.OK … t. 30 ∀succT,succ,pointer_of_label,codeT,lookup. 31 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) → 32 state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝ 33 λ_.λ_.λ_.λ_.λ_.λ_.λ_.λt.OK … t. 32 34 definition ltl_lin_save_frame: 33 35 ∀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)) ≝ … … 37 39 λsuccT,succ,pointer_of_label. 38 40 mk_more_sem_params1 ? ltl_lin_params1 (ltl_lin_more_sem_params succT succ pointer_of_label) 39 ltl_lin_init_locals (ltl_lin_ pop_frame …) (ltl_lin_save_frame …).41 ltl_lin_init_locals (ltl_lin_save_frame …). 40 42 41 43 (*CSC: XXXXX, for is_final only *) 42 axiom ltl_lin_fetch_result: ∀succT,succ,pointer_of_label.state (ltl_lin_sem_params succT succ pointer_of_label) → res (list beval). 44 axiom ltl_lin_fetch_result: 45 ∀succT,succ,pointer_of_label,codeT,lookup. 46 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) → 47 state (ltl_lin_sem_params succT succ pointer_of_label) → res (list beval). 43 48 44 49 (*CSC: XXXX, for external functions only*) … … 55 60 λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals. 56 61 mk_more_sem_params2 … (ltl_lin_more_sem_params1 … succ pointer_of_label) 57 (fetch globals) (load_ra …) (ltl_lin_fetch_result …) 58 (ltl_lin_fetch_external_args …) 59 (ltl_lin_set_result …) (ltl_lin_exec_extended …). 62 (fetch globals) (load_ra …) (ltl_lin_fetch_result …) (ltl_lin_pop_frame …) 63 (ltl_lin_fetch_external_args …) (ltl_lin_set_result …) (ltl_lin_exec_extended …). 60 64 61 65 definition ltl_lin_fullexec ≝
Note: See TracChangeset
for help on using the changeset viewer.