include "LIN/joint_LTL_LIN.ma".
include "joint/SemanticUtils.ma".

(*CSC: re-organize to take succ_pc out of lin_more_sem_params? *)
definition ltl_lin_more_sem_params: ∀succT,succ,pointer_of_label. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
 λsuccT,succ,pointer_of_label.
 mk_more_sem_params ?
  unit hw_register_env succ
   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_lin_sem_params:
 ∀succT,succ,pointer_of_label. sem_params ≝
 λsuccT,succ,pointer_of_label.mk_sem_params … (ltl_lin_more_sem_params succT succ pointer_of_label).


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)) × address) ≝
 λ_.λ_.λ_.fetch_ra ….
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)) ≝
 λ_.λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.

definition ltl_lin_more_sem_params1 : ∀succT,succ,pointer_of_label.more_sem_params1 … ltl_lin_params1 ≝
 λ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 …).

(*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).

(*CSC: XXXX, for external functions only*)
axiom ltl_lin_fetch_external_args: ∀succT,succ,pointer_of_label.external_function → state (ltl_lin_sem_params succT succ pointer_of_label) → res (list val).
axiom ltl_lin_set_result: ∀succT,succ,pointer_of_label.list val → state (ltl_lin_sem_params succT succ pointer_of_label) → res (state (ltl_lin_sem_params … succ pointer_of_label)).

definition ltl_lin_exec_extended: ∀succT,succ,pointer_of_label.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params succT succ pointer_of_label) → IO io_out io_in (trace × (state (ltl_lin_sem_params … succ pointer_of_label)))
 ≝ λsuccT,succ,pointer_of_label,p,globals,ge,abs. ⊥.
@abs qed.

definition ltl_lin_more_sem_params2:
 ∀succT,succ,pointer_of_label,codeT,lookup,fetch.
 ∀globals. more_sem_params2 … (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) ≝
 λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
  mk_more_sem_params2 … (ltl_lin_more_sem_params1 … succ pointer_of_label)
   (fetch globals) (ltl_lin_fetch_result …) (ltl_lin_fetch_external_args …)
   (ltl_lin_set_result …) (ltl_lin_exec_extended …).

definition ltl_lin_fullexec ≝
 λsuccT,succ,pointer_of_label,codeT,lookup,fetch.
  joint_fullexec … (λp. ltl_lin_more_sem_params2 succT succ pointer_of_label codeT lookup fetch (prog_var_names … p)).