Changeset 1380 for src/LTL/semantics.ma

Timestamp:

Oct 14, 2011, 10:25:03 PM (9 years ago)

Author:

sacerdot

Message:

LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma.
Very cool.

File:

• src/LTL/semantics.ma (modified) (1 diff)

src/LTL/semantics.ma

@@ -1 @@
-include "joint/SemanticUtils.ma".
+include "LIN/joint_LTL_LIN_semantics.ma".
 include "LTL/LTL.ma". (* CSC: syntax.ma in RTLabs *)
 
-definition ltl_more_sem_params: more_sem_params ltl_params_ :=
- mk_more_sem_params ltl_params_
-  unit hw_register_env graph_succ_p
-   hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
-    (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
-    (λ_.hwreg_store RegisterDPL) (λe.λ_.hwreg_retrieve e RegisterDPL)
-    (λ_.hwreg_store RegisterDPH) (λe.λ_.hwreg_retrieve e RegisterDPH)
-     (λlocals,dest_src.
-       match dest_src with
-       [ from_acc reg ⇒
-          do v ← hwreg_retrieve locals RegisterA ;
-          hwreg_store reg v locals
-       | to_acc reg ⇒
-          do v ← hwreg_retrieve locals reg ;
-          hwreg_store RegisterA v locals ])
-     pointer_of_label.
-definition ltl_sem_params: sem_params ≝ mk_sem_params … ltl_more_sem_params.
-
-definition ltl_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
-definition ltl_pop_frame: state … ltl_sem_params → res ((state … ltl_sem_params) × address) ≝
- fetch_ra ….
-definition ltl_save_frame:
- address → nat → unit → nat → unit → state … ltl_sem_params → res (state … ltl_sem_params) ≝
- λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
-
-definition ltl_more_sem_params1 : more_sem_params1 … ltl_lin_params1 ≝
- mk_more_sem_params1 ? ltl_lin_params1 ltl_more_sem_params
-  ltl_init_locals ltl_pop_frame ltl_save_frame.
-
-(*CSC: XXXXX, for is_final only *)
-axiom ltl_fetch_result: state ltl_sem_params → res (list beval).
-
-(*CSC: XXXX, for external functions only*)
-axiom ltl_fetch_external_args: external_function → state ltl_sem_params → res (list val).
-axiom ltl_set_result: list val → state ltl_sem_params → res (state ltl_sem_params).
-
-definition ltl_exec_extended: ∀globals. genv globals (ltl_params globals) → False → label → state ltl_sem_params → IO io_out io_in (trace × (state ltl_sem_params))
- ≝ λglobals,ge,abs. ⊥.
-@abs qed.
-
-definition ltl_more_sem_params2: ∀globals. more_sem_params2 … (ltl_params globals) ≝
- λglobals.
-  mk_more_sem_params2 … ltl_more_sem_params1
-   (graph_fetch_statement …) ltl_fetch_result ltl_fetch_external_args ltl_set_result
-    (ltl_exec_extended …).
-
 definition ltl_fullexec ≝
- joint_fullexec … (λp. ltl_more_sem_params2 (prog_var_names … p)).
-
+ ltl_lin_fullexec … (graph_succ_p …) … (graph_fetch_statement … (ltl_lin_sem_params …)).
 
 (*