Changeset 1385 for src/LIN

Timestamp:

Oct 17, 2011, 1:40:13 AM (8 years ago)

Author:

sacerdot

Message:

1. fetch_result and pop_frame now takes the genv in input
2. implementation of fetch_result for RTL completed All RTL axioms but the ones related to external functions are now closed.

File:

• src/LIN/joint_LTL_LIN_semantics.ma (modified) (3 diffs)

src/LIN/joint_LTL_LIN_semantics.ma

@@ -28 +28 @@
 definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
 definition ltl_lin_pop_frame:
- ∀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)) ≝
- λ_.λ_.λ_.λt.OK … t.
+ ∀succT,succ,pointer_of_label,codeT,lookup.
+ ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
+ state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝
+ λ_.λ_.λ_.λ_.λ_.λ_.λ_.λt.OK … t.
 definition ltl_lin_save_frame:
  ∀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.
  mk_more_sem_params1 ? ltl_lin_params1 (ltl_lin_more_sem_params succT succ pointer_of_label)
-  ltl_lin_init_locals (ltl_lin_pop_frame …) (ltl_lin_save_frame …).
+  ltl_lin_init_locals (ltl_lin_save_frame …).
 
 (*CSC: XXXXX, for is_final only *)
-axiom ltl_lin_fetch_result: ∀succT,succ,pointer_of_label.state (ltl_lin_sem_params succT succ pointer_of_label) → res (list beval).
+axiom ltl_lin_fetch_result:
+ ∀succT,succ,pointer_of_label,codeT,lookup.
+ ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
+ state (ltl_lin_sem_params succT succ pointer_of_label) → res (list beval).
 
 (*CSC: XXXX, for external functions only*)
@@ -55 +60 @@
  λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
   mk_more_sem_params2 … (ltl_lin_more_sem_params1 … succ pointer_of_label)
-   (fetch globals) (load_ra …) (ltl_lin_fetch_result …)
-   (ltl_lin_fetch_external_args …)
-   (ltl_lin_set_result …) (ltl_lin_exec_extended …).
+   (fetch globals) (load_ra …) (ltl_lin_fetch_result …) (ltl_lin_pop_frame …)
+   (ltl_lin_fetch_external_args …) (ltl_lin_set_result …) (ltl_lin_exec_extended …).
 
 definition ltl_lin_fullexec ≝