include "joint/semantics.ma".
include alias "common/Identifiers.ma".

(*** Store/retrieve on pseudo-registers ***)

axiom BadRegister : String.

definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.

definition reg_retrieve : register_env beval → register → res beval ≝
 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).

(*** Store/retrieve on hardware registers ***)

definition init_hw_register_env: address → hw_register_env ≝
 λaddr.
  let 〈dpl,dph〉 ≝ addr in
  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
   hwreg_store RegisterDPL dpl env.

(****************************************************************************)

definition graph_pointer_of_label0:
 pointer → label → Σp:pointer. ptype p = Code ≝
 λoldpc,l.
  mk_pointer 
   (mk_block Code (block_id (pblock oldpc))) (mk_offset (pos (word_of_identifier … l))). 
// qed.

definition graph_pointer_of_label:
 ∀params1.∀globals. genv … (graph_params params1 globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝
 λ_.λ_.λ_.λoldpc,l.
  OK ? (graph_pointer_of_label0 oldpc l). 

definition graph_label_of_pointer: pointer → res label ≝
 λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).

(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
 But I can't use it directly because this one uses a concrete definition of
 pointer_of_label and it is used to istantiate the more_sem_params record
 where the abstract version is declared as a field. Is there a better way
 to organize the code? *)
definition graph_succ_p: label → address → res address ≝
 λl,old.
  do ptr ← pointer_of_address old ;
  let newptr ≝ graph_pointer_of_label0 ptr l in
  address_of_pointer newptr.

axiom BadProgramCounter: String.

definition graph_fetch_function:
 ∀params1,sem_params,globals.
  genv … (graph_params params1 globals) →
   state sem_params → res (joint_internal_function … (graph_params params1 globals)) ≝
 λparams1,sem_params,globals,ge,st.
  do p ← code_pointer_of_address (pc … st) ;
  let b ≝ pblock p in
  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
  match def with
  [ Internal def' ⇒ OK … def'
  | External _ ⇒ Error … [MSG BadProgramCounter]].

definition graph_fetch_statement:
 ∀params1,sem_params,globals.
  genv … (graph_params params1 globals) →
   state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
 λparams1,sem_params,globals,ge,st.
  do p ← code_pointer_of_address (pc … st) ;
  do f ← graph_fetch_function … ge st ;
  do l ← graph_label_of_pointer p;
  opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).