include "joint/semanticsUtils.ma".
include "ERTLptr/ERTLptr.ma". (* CSC: syntax.ma in RTLabs *)
include "ERTL/ERTL_semantics.ma".
include alias "common/Identifiers.ma".

definition ertlptr_save_frame:
 call_kind → unit  → state_pc ERTL_state → res (state … ERTL_state) ≝
 λk.λ_.λst.
 ! st' ← match k with
  [ ID ⇒ push_ra … st (pc … st)
  | PTR ⇒ return (st : state ?)
  ] ;
 ! frms ← opt_to_res ? [MSG FrameErrorOnPush] (st_frms … st');
  return
   (set_frms ERTL_state (〈\fst (regs ERTL_state st'), pc_block (pc … st)〉 :: frms)
    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).

definition eval_ertlptr_seq:
 ∀F.∀globals. genv_gen F globals →
  ertlptr_seq → ident → state ERTL_state →
   res (state ERTL_state) ≝
 λF,globals,ge,stm,id,st.
  match stm with
   [ ertlptr_ertl seq ⇒ eval_ertl_seq F globals ge seq id st
   | LOW_ADDRESS r l ⇒  ! pc_lab ← gen_pc_from_label … ge id l;
                        let 〈addrl,addrh〉 ≝ beval_pair_of_pc pc_lab in
                        ps_reg_store_status r addrl st
   | HIGH_ADDRESS r l ⇒ ! pc_lab ← gen_pc_from_label … ge id l;
                        let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
                        ps_reg_store_status r addrh st
   ].

definition ERTLptr_sem_uns ≝ 
λF. mk_sem_unserialized_params ERTLptr ?
  (* st_pars            ≝ *) ERTL_state
  (* acca_store_        ≝ *) ps_reg_store
  (* acca_retrieve_     ≝ *) ps_reg_retrieve
  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
  (* accb_store_        ≝ *) ps_reg_store
  (* accb_retrieve_     ≝ *) ps_reg_retrieve
  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
  (* dpl_store_         ≝ *) ps_reg_store
  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
  (* dph_store_         ≝ *) ps_reg_store
  (* dph_retrieve_      ≝ *) ps_reg_retrieve
  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
  (* pair_reg_move_     ≝ *) ertl_eval_move
  (* save_frame         ≝ *) ertlptr_save_frame
  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
  (* fetch_external_args≝ *) ertl_fetch_external_args
  (* set_result         ≝ *) ertl_set_result
  (* call_args_for_main ≝ *) 0
  (* call_dest_for_main ≝ *) it
  (* read_result        ≝ *) (λ_.λ_.λ_.
     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.eval_ertlptr_seq F gl ge stm id)
  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.ertl_pop_frame).
  
definition ERTLptr_semantics ≝
  mk_sem_graph_params ERTLptr ERTLptr_sem_uns ERTLptr_premain.