include "utilities/lists.ma".
include "common/Globalenvs.ma".
include "common/IO.ma".
include "common/SmallstepExec.ma".
include "joint/Joint.ma".
include "joint/BEMem.ma".

(* CSC: external functions never fail (??) and always return something of the
   size of one register, both in the frontend and in the backend.
   Is this reasonable??? In OCaml it always return a list, but in the frontend
   only the head is kept (or Undef if the list is empty) ??? *)

definition address ≝ beval × beval. (* CSC: only pointers to XRAM or code memory *)

definition eq_address: address → address → bool ≝
 λaddr1,addr2.
  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).

record sem_params: Type[1] ≝
 { p:> params
 ; framesT: Type[0]
 ; regsT: Type[0] (* regs = pseudo-registers + hw registers *)
 
 ; pop_frame_: framesT → res framesT
 ; save_frame_: framesT → regsT → framesT
 ; greg_store_: generic_reg p → beval → regsT → res regsT
 ; greg_retrieve_: regsT → generic_reg p → res beval
 ; acca_store_: acc_a_reg p → beval → regsT → res regsT
 ; acca_retrieve_: regsT → acc_a_reg p → res beval
 ; accb_store_: acc_b_reg p → beval → regsT → res regsT
 ; accb_retrieve_: regsT → acc_b_reg p → res beval
 ; dpl_store_: dpl_reg p → beval → regsT → res regsT
 ; dpl_retrieve_: regsT → dpl_reg p → res beval
 ; dph_store_: dph_reg p → beval → regsT → res regsT
 ; dph_retrieve_: regsT → dph_reg p → res beval
 ; pair_reg_move_: regsT → pair_reg p → regsT
 
 ; init_locals : localsT p → regsT
 ; pointer_of_label: label → Σp:pointer. ptype p = Code
 }.

definition address_of_label: sem_params → label → address.
 #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label p l)))
 cases (beval_pair_of_pointer (pointer_of_label p l)) in ⊢ (???% → ?)
  [ #res #_ @res
  | #msg cases (pointer_of_label p l) * * #q #com #off #E1 #E2 destruct ]
qed. 

record state (p: sem_params): Type[0] ≝
 { st_frms: framesT p
 ; pc: address
 ; sp: pointer
 ; carry: beval
 ; regs: regsT p
 ; m: bemem
 }.

definition genv ≝ λglobals,pre,p. (genv_t Genv) (joint_function globals pre p).

record sem_params2 (globals: list ident): Type[1] ≝
 { sparams:> sem_params
 ; pre_sem_params:> sem_params_ sparams globals
 
 ; fetch_statement: state sparams → res (joint_statement sparams globals)
 ; fetch_external_args: external_function → state sparams → res (list val)
 ; set_result: list val → state sparams → res (state sparams)
 ; fetch_result: state sparams → nat → res val

 ; exec_extended: genv … pre_sem_params → extend_statements sparams → state sparams → IO io_out io_in (trace × (state sparams))
 }.

definition set_m: ∀p. bemem → state p → state p ≝
 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) (regs … st) m.

definition set_regs: ∀p. regsT p → state p → state p ≝
 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) regs (m … st).

definition set_sp: ∀p. pointer → state p → state p ≝
 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (carry … st) (regs … st) (m … st).

definition set_carry: ∀p. beval → state p → state p ≝
 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) carry (regs … st) (m … st).

definition set_pc: ∀p. address → state p → state p ≝
 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (carry … st) (regs … st) (m … st).

definition set_frms: ∀p. framesT p → state p → state p ≝
 λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st).

definition goto: ∀p:sem_params. label → state p → state p ≝
 λp,l,st. set_pc … (address_of_label p l) st.

definition greg_store: ∀p:sem_params. generic_reg p → beval → state p → res (state p) ≝
 λp,dst,v,st.
  do regs  ← greg_store_ … dst v (regs … st);
  OK ? (set_regs … regs st).

definition greg_retrieve: ∀p:sem_params. state p → generic_reg p → res beval ≝
 λp,st,dst.greg_retrieve_ … (regs … st) dst.

definition acca_store: ∀p:sem_params. acc_a_reg p → beval → state p → res (state p) ≝
 λp,dst,v,st.
  do regs ← acca_store_ … dst v (regs … st);
  OK ? (set_regs … regs st).

definition acca_retrieve: ∀p:sem_params. state p → acc_a_reg p → res beval ≝
 λp,st,dst.acca_retrieve_ … (regs … st) dst.

definition accb_store: ∀p:sem_params. acc_b_reg p → beval → state p → res (state p) ≝
 λp,dst,v,st.
  do regs ← accb_store_ … dst v (regs … st);
  OK ? (set_regs … regs st).

definition accb_retrieve: ∀p:sem_params. state p → acc_b_reg p → res beval ≝
 λp,st,dst.accb_retrieve_ … (regs … st) dst.

definition dpl_store: ∀p:sem_params. dpl_reg p → beval → state p → res (state p) ≝
 λp,dst,v,st.
  do regs ← dpl_store_ … dst v (regs … st);
  OK ? (set_regs … regs st).

definition dpl_retrieve: ∀p:sem_params. state p → dpl_reg p → res beval ≝
 λp,st,dst.dpl_retrieve_ … (regs … st) dst.

definition dph_store: ∀p:sem_params. dph_reg p → beval → state p → res (state p) ≝
 λp,dst,v,st.
  do regs ← dph_store_ … dst v (regs … st);
  OK ? (set_regs … regs st).

definition dph_retrieve: ∀p:sem_params. state p → dph_reg p → res beval ≝
 λp,st,dst.dph_retrieve_ … (regs … st) dst.

definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → state p ≝
 λp,st,rs.set_regs … (pair_reg_move_ … (regs … st) rs) st.

definition save_frame: ∀p:sem_params. state p → state p ≝
 λp,st. set_frms … (save_frame_ ? (st_frms ? st) (regs … st)) st.

(* removes the top frame from the frames list *)
definition pop_frame: ∀p. state p → res (state p) ≝
 λp,st.
  do frames ← pop_frame_ p (st_frms … st);
  OK ? (mk_state ? frames (pc … st) (sp … st) (carry … st) (regs … st) (m … st)).

axiom FailedStore: String.

definition push: ∀p. state p → beval → res (state p) ≝
 λp,st,v.
  let sp ≝ sp … st in
  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) sp v);
  let sp ≝ shift_pointer … sp [[false;false;false;false;false;false;false;true]] in
  OK … (set_m … m (set_sp … sp st)).

definition pop: ∀p. state p → res (state p × beval) ≝
 λp,st.
  let sp ≝ sp ? st in
  let sp ≝ neg_shift_pointer ? sp [[false;false;false;false;false;false;false;true]] in
  let st ≝ set_sp … sp st in
  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) sp);
  OK ? 〈st,v〉.

definition save_ra : ∀p. state p → label → res (state p) ≝
 λp,st,l.
  let 〈addrl,addrh〉 ≝ address_of_label p l in
  do st ← push … st addrl;
  push … st addrh.

definition fetch_ra : ∀p.state p → res (state p × address) ≝
 λp,st.
  do 〈st,addrh〉 ← pop … st;
  do 〈st,addrl〉 ← pop … st;
  OK ? 〈st, 〈addrl,addrh〉〉.

axiom MissingSymbol : String.
axiom FailedLoad : String.
axiom BadFunction : String.

(*CSC: move elsewhere *)
definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
 λA,P,c. match c with [ dp w _ ⇒ w ].
coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.

definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv … (pre_sem_params … p) → state p → IO io_out io_in (trace × (state p)) ≝
  λglobals,p. λge,st.
  ! s ← fetch_statement globals p st;
  match s with
    [ joint_st_goto l ⇒ ret ? 〈E0, goto … l st〉
    | joint_st_sequential seq l ⇒
      match seq with
      [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto … l st〉
      | joint_instr_comment c ⇒ ret ? 〈E0, goto … l st〉
      | joint_instr_int dest v ⇒
        ! st ← greg_store … dest (BVByte v) st;
          ret ? 〈E0, goto … l st〉
      | joint_instr_load dst addrl addrh ⇒
        ! vaddrh ← dph_retrieve … st addrh;
        ! vaddrl ← dpl_retrieve … st addrl;
        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
        ! st ← acca_store … dst v st;
          ret ? 〈E0, goto … l st〉
      | joint_instr_store addrl addrh src ⇒
        ! vaddrh ← dph_retrieve … st addrh;
        ! vaddrl ← dpl_retrieve … st addrl;
        ! vaddr ← pointer_of_bevals [vaddrl;vaddrh];
        ! v ← acca_retrieve … st src;
        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
          ret ? 〈E0, goto … l (set_m … m' st)〉
      | joint_instr_cond src ltrue ⇒
        ! v ← acca_retrieve … st src;
        ! b ← bool_of_beval v;
          ret ? 〈E0, goto … (if b then ltrue else l) st〉
      | joint_instr_address ident prf ldest hdest ⇒
        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
        ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer (block_region addr) addr ? zero_offset);
        ! st ← dpl_store … ldest laddr st;
        ! st ← dph_store … hdest haddr st;
          ret ? 〈E0, goto … l st〉
      | joint_instr_op1 op acc_a ⇒
        ! v ← acca_retrieve … st acc_a;
        ! v ← Byte_of_val v;
          let v' ≝ BVByte (op1 eval op v) in
        ! st ← acca_store … acc_a v' st;
          ret ? 〈E0, goto … l st〉
      | joint_instr_op2 op acc_a src ⇒
        ! v1 ← acca_retrieve … st acc_a;
        ! v1 ← Byte_of_val v1;
        ! v2 ← greg_retrieve … st src;
        ! v2 ← Byte_of_val v2;
        ! carry ← bool_of_beval (carry … st);
          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
          let v' ≝ BVByte v' in
          let carry ≝ beval_of_bool carry in
        ! st ← acca_store … acc_a v' st;
          ret ? 〈E0, goto … l (set_carry … carry st)〉
      | joint_instr_clear_carry ⇒ ret ? 〈E0, goto … l (set_carry … BVfalse st)〉
      | joint_instr_set_carry ⇒ ret ? 〈E0, goto … l (set_carry … BVtrue st)〉
      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
        ! v1 ← acca_retrieve … st acc_a_reg;
        ! v1 ← Byte_of_val v1;
        ! v2 ← accb_retrieve … st acc_b_reg;
        ! v2 ← Byte_of_val v2;
          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
          let v1' ≝ BVByte v1' in
          let v2' ≝ BVByte v2' in
        ! st ← acca_store … acc_a_reg v1' st;
        ! st ← accb_store … acc_b_reg v2' st;
          ret ? 〈E0, goto … l st〉
      | joint_instr_pop dst ⇒
        ! 〈st,v〉 ← pop … st;
        ! st ← acca_store … dst v st;
          ret ? 〈E0, goto … l st〉
      | joint_instr_push src ⇒
        ! v ← acca_retrieve … st src;
        ! st ← push … st v;
          ret ? 〈E0, goto … l st〉
      | joint_instr_move dst_src ⇒
          ret ? 〈E0, goto … l (pair_reg_move … st dst_src)〉
      | joint_instr_call_id id argsno ⇒
        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
          match fd with
          [ Internal fn ⇒
            ! st ← save_ra … st l;
              let st ≝ save_frame … st in
              let regs ≝ init_locals p (joint_if_locals … fn) in
              let l' ≝ joint_if_entry … fn in
             ret ? 〈 E0, goto … l' (set_regs … regs st)〉
          | External fn ⇒
            ! params ← fetch_external_args … fn st;
            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
            (* CSC: XXX bug here; I think I should split it into Byte-long
               components; instead I am making a singleton out of it *)
              let vs ≝ [mk_val ? evres] in
            ! st ← set_result … vs st; 
              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto … l st〉
          ]]
    | joint_st_return ⇒
      ! st ← pop_frame … st;
      ! 〈st,pch〉 ← pop … st;
      ! 〈st,pcl〉 ← pop … st;
        ret ? 〈E0,set_pc … 〈pcl,pch〉 st〉
    | joint_st_extension c ⇒ exec_extended … p ge c st ].
cases addr //
qed.

definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option int ≝
  λglobals,p,exit,registersno,st. res_to_opt … (
  do s ← fetch_statement … st;
  match s with
   [ joint_st_return ⇒
      do 〈st,l〉 ← fetch_ra … st;
      if eq_address l exit then
       do val ← fetch_result globals p st registersno;
       match val with
        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. OK ? i) (Error ? [])
        | _ ⇒ Error ? []]
      else
       Error ? []
   | _ ⇒ Error ? []]).

definition joint_exec: ∀globals:list ident. sem_params2 globals → address → nat → execstep io_out io_in ≝
  λglobals,p.
  λexit.
  λregistersno.
  mk_execstep … (is_final globals p exit registersno) (m p) (eval_statement globals p).

(* CSC: XXX the program type does not fit with the globalenv and init_mem *)
axiom make_initial_state : ∀globals:list ident.∀sparams: sem_params2 globals. joint_program … (pre_sem_params … sparams) → res ((genv … (pre_sem_params … sparams)) × (state sparams)).(* ≝
λp.
  do ge ← globalenv Genv ?? p;
  do m ← init_mem Genv ?? p;
  let main ≝ rtl_pr_main ?? p in
  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
*)

definition joint_fullexec :
 ∀globals:list ident. ∀sparams:sem_params2 globals. joint_program globals sparams (pre_sem_params … sparams) → fullexec io_out io_in ≝
 λglobals,p,program.
  let exit ≝ ? in
  let registersno ≝ ? in
  mk_fullexec ?? (joint_exec ? p exit registersno) ? (make_initial_state … p).