include "utilities/lists.ma".
include "common/Globalenvs.ma".
include "common/IO.ma".
include "common/SmallstepExec.ma".
include "joint/Joint.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) ??? *)

(* CSC: carries are values and booleans are not values; so we use integers.
   But why using values at all? To have undef? *)
(* CSC: ???????????? *)
*)
axiom smerge: val → val → res val.
(* CSC: ???????????? In OCaml: IntValue.Int32.merge
   Note also that the translation can fail; so it should be a res int! *)
axiom smerge2: list val → int.
(* CSC: I have a byte, I need a value, but it is complex to do so *)
axiom val_of_Byte: Byte → val.
axiom Byte_of_val: val → res Byte.
(*
axiom val_of_nat: nat → val.
(* Map from the front-end memory model to the back-end memory model *)
*)
axiom represent_block: block → val × val.
(* CSC: fixed size chunk *)
axiom chunk: memory_chunk.
axiom val_of_memory_chunk: memory_chunk → val. (* CSC: only to shift the sp *)
axiom address: Type[0].
axiom val_of_address: address → val. (* CSC: only to shift the sp *)
axiom address_of_val: val → address. (* CSC: only to shift the sp *)
(*
axiom addr_sub: address → nat → address.
axiom addr_add: address → nat → address.
*)
(* CSC: ??? *)
axiom address_of_label: mem → label → address.
axiom address_chunks_of_label: mem → label → Byte × Byte.
axiom label_of_address_chunks: Byte → Byte → label.
axiom address_of_address_chunks: Byte → Byte → address.
(*
axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *)
*)
(*
axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
axiom hwreg_retrieve : mRegisterMap → Register → res val.
axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
*)

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 → val → regsT → res regsT
 ; greg_retrieve_: regsT → generic_reg p → res val
 ; acca_store_: acc_a_reg p → val → regsT → res regsT
 ; acca_retrieve_: regsT → acc_a_reg p → res val
 ; accb_store_: acc_b_reg p → val → regsT → res regsT
 ; accb_retrieve_: regsT → acc_b_reg p → res val
 ; dpl_store_: dpl_reg p → val → regsT → res regsT
 ; dpl_retrieve_: regsT → dpl_reg p → res val
 ; dph_store_: dph_reg p → val → regsT → res regsT
 ; dph_retrieve_: regsT → dph_reg p → res val
 ; pair_reg_move_: regsT → pair_reg p → regsT
 }.

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

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
 ; exec_extended: genv … pre_sem_params → extend_statements sparams → state sparams → IO io_out io_in (trace × (state sparams))
 }.

definition set_m: ∀p. mem → 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. address → 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. val → 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).

(* CSC: was build_state in RTL *)
definition goto: ∀p:sem_params. label → state p → state p ≝
 λp,l,st. set_pc … (address_of_label … (m … st) l) st.

definition greg_store: ∀p:sem_params. generic_reg p → val → state p → res (state p) ≝
 λp,dst,v,st.
  (*CSC: monadic notation missing here *)
  bind ?? (greg_store_ … dst v (regs … st)) (λregs.
  OK ? (set_regs … regs st)).

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

definition acca_store: ∀p:sem_params. acc_a_reg p → val → state p → res (state p) ≝
 λp,dst,v,st.
  (*CSC: monadic notation missing here *)
  bind ?? (acca_store_ … dst v (regs … st)) (λregs.
  OK ? (set_regs … regs st)).

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

definition accb_store: ∀p:sem_params. acc_b_reg p → val → state p → res (state p) ≝
 λp,dst,v,st.
  (*CSC: monadic notation missing here *)
  bind ?? (accb_store_ … dst v (regs … st)) (λregs.
  OK ? (set_regs … regs st)).

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

definition dpl_store: ∀p:sem_params. dpl_reg p → val → state p → res (state p) ≝
 λp,dst,v,st.
  (*CSC: monadic notation missing here *)
  bind ?? (dpl_store_ … dst v (regs … st)) (λregs.
  OK ? (set_regs … regs st)).

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

definition dph_store: ∀p:sem_params. dph_reg p → val → state p → res (state p) ≝
 λp,dst,v,st.
  (*CSC: monadic notation missing here *)
  bind ?? (dph_store_ … dst v (regs … st)) (λregs.
  OK ? (set_regs … regs st)).

definition dph_retrieve: ∀p:sem_params. state p → dph_reg p → res val ≝
 λ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) ≝
 (* CSC: monadic notation missing here *)
 λp,st.
  bind ?? (pop_frame_ p (st_frms … st)) (λframes.
  OK ? (mk_state ? frames (pc … st) (sp … st) (carry … st) (regs … st) (m … st))).

axiom FailedStore: String.

definition push: ∀p. state p → Byte → res (state p) ≝
 λp,st,v.
  let sp ≝ val_of_address (sp … st) in
  (*CSC: no monadic notation here *)
  bind ?? (opt_to_res ? (msg FailedStore) (storev chunk (m … st) sp (val_of_Byte v)))
   (λm.
    let sp ≝ address_of_val (add sp (val_of_memory_chunk chunk)) in
    OK ? (set_m ? m (set_sp … sp st))).


definition pop: ∀p. state p → res (state p × Byte) ≝
 λp,st.
  let sp ≝ val_of_address (sp … st) in
  let sp ≝ sub sp (val_of_memory_chunk chunk) in
  let st ≝ set_sp … (address_of_val sp) st in
  (*CSC: no monadic notation here *)
  bind ?? (opt_to_res ? (msg FailedStore) (loadv chunk (m … st) sp))
   (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).

definition save_ra : ∀p. state p → label → res (state p) ≝
 λp,st,l.
  let 〈addrl,addrh〉 ≝ address_chunks_of_label … (m … st) l in
  (* No monadic notation here *)
  bind ?? (push … st addrl) (λst.push … st addrh).

definition fetch_ra : ∀p.state p → res (state p × label) ≝
 λp,st.
  (* No monadic notation here *)
  bind ?? (pop … st) (λres. let 〈st,addrh〉 ≝ res in
  bind ?? (pop … st) (λres. let 〈st,addrl〉 ≝ res in
   OK ? 〈st, label_of_address_chunks addrl addrh〉)).

(*CSC: To be implemented *)
axiom fetch_statement: ∀p.∀globals: list ident. state p → res (joint_statement p globals).
(*
axiom fetch_function: ∀globals: list ident. state → res (ltl_internal_function globals). (* CSC *)
*)

(*
definition init_locals : ∀p.list register → regsT p ≝
foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
*)

(*
definition reg_store ≝
λreg,v,locals. update RegisterTag val locals reg v.

axiom BadRegister : String.

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

axiom MissingSymbol : String.

axiom FailedLoad : String.

axiom BadFunction : String.

(*CSC: to be implemented *)
axiom fetch_external_args: ∀p. external_function → state p → res (list val). (* ≝
 λfn,st.
  let registerno ≝ ? fn in
  ! vs ←
   mmap …
    (λr. hwreg_retrieve (regs st) r) (prefix … registersno RegisterParameters);
  (* CSC: HERE WE NEED TO RETRIEVE THE REMAINING REGISTERS FROM THE STACK! *)
  ?.
*)


(*CSC: to be implemented; fails if the first list is longer *)
axiom fold_left2_first_not_longer:
 ∀A,B,C:Type[0]. ∀f:(C → A → B → res C).
  ∀acc:C. ∀l1:list A. ∀l2: list B.
   res C.

(* CSC: the list should be a vector or have an upper bounded length *)
(*CSC: XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX *)
axiom set_result: ∀p. list val → state p → res (state p).
(* λp,vs,st.
  (* CSC: monadic notation not used *)
  bind ?? ( 
   fold_left2_first_not_longer …
    (λregs,v,reg. hwreg_store reg v regs) (regs … st) vs RegisterRets)
  (λregs.OK ? (set_regs … regs st)).
*)

(*CSC: XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX *)
axiom fetch_result: ∀p. state p → nat → res (list val).
(*
definition fetch_result: state → nat → res (list val) ≝
 λst,registersno.
  let retregs ≝ prefix … registersno RegisterRets in
  mmap … (λr. hwreg_retrieve (regs st) r) retregs.

definition framesize: list ident → state → res nat ≝
  λglobals: list ident.
  λst.
  (* CSC: monadic notation missing here *)
    bind ?? (fetch_function globals st) (λf.
    OK ? (ltl_if_stacksize globals f)).

definition get_hwsp : state → res address ≝
 λst.
  (* CSC: monadic notation missing here *)
  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λspl.
  (* CSC: monadic notation missing here *)
  bind ?? (Byte_of_val spl) (λspl.
  (* CSC: monadic notation missing here *)
  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λsph.
  (* CSC: monadic notation missing here *)
  bind ?? (Byte_of_val sph) (λsph.
  OK ? (address_of_address_chunks spl sph))))).

definition set_hwsp : address → state → res state ≝
 λsp,st.
  let 〈spl,sph〉 ≝ address_chunks_of_address sp in
  (* CSC: monadic notation missing here *)  
  bind ?? (hwreg_store RegisterSPL (val_of_Byte spl) (regs st)) (λregs.
  (* CSC: monadic notation missing here *)  
  bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs.
  OK ? (set_regs regs st))).
*)

(*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 p globals 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 (val_of_Byte v) st;
          ret ? 〈E0, goto … l st〉
      | joint_instr_load dst addrl addrh ⇒
        ! vaddrh ← dph_retrieve … st addrh;
        ! vaddrl ← dpl_retrieve … st addrl;
        ! vaddr ← smerge vaddrl vaddrh;
        ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (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 ← smerge vaddrl vaddrh;
        ! v ← acca_retrieve … st src;
        ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m … st) vaddr v);
          ret ? 〈E0, goto … l (set_m … m' st)〉
      | joint_instr_cond src ltrue ⇒
        ! v ← acca_retrieve … st src;
        ! b ← eval_bool_of_val 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);
          let 〈laddr,haddr〉 ≝ represent_block addr in
        ! 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' ≝ val_of_Byte (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 ← eval_bool_of_val (carry … st);
          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
          let v' ≝ val_of_Byte v' in
          let carry ≝ 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 … Vfalse st)〉
      | joint_instr_set_carry ⇒ ret ? 〈E0, goto … l (set_carry … Vtrue 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' ≝ val_of_Byte v1' in
          let v2' ≝ val_of_Byte 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 (val_of_Byte v) st;
          ret ? 〈E0, goto … l st〉
      | joint_instr_push src ⇒
        ! v ← acca_retrieve … st src;
        ! v ← Byte_of_val v; 
        ! 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
              (*CSC: XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
              let regs ≝ init_locals … (ertl_if_locals globals fn) in *) let regs ≝ regs … st 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;
        let pc ≝ address_of_address_chunks pcl pch in
        ret ? 〈E0,set_pc … pc st〉
    | joint_st_extension c ⇒ exec_extended … p ge c st
    ].

definition is_final: ∀p. list ident → label → nat → state p → option ((*CSC: why not res*) int) ≝
  λp.λglobals: list ident.
  λexit.
  λregistersno.
  λst.
 (* CSC: monadic notation missing here *)
  match fetch_statement … globals st with
  [ Error _ ⇒ None ?
  | OK s ⇒
    match s with
      [ joint_st_return ⇒
        match fetch_ra … st with
         [ Error _ ⇒ None ?
         | OK st_l ⇒
           let 〈st,l〉 ≝ st_l in
           match label_eq l exit with
           [ inl _ ⇒
             (* CSC: monadic notation missing here *)
             match fetch_result … st registersno with
             [ Error _ ⇒ None ?
             | OK vals ⇒ Some ? (smerge2 vals)
             ]
           | inr _ ⇒ None ?
           ]
         ]
      | _ ⇒ None ?
      ]
  ].

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

(* CSC: XXX the program type does not fit with the globalenv and init_mem
definition make_initial_state : rtl_program → res (genv × state) ≝
λ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 RTL_fullexec : fullexec io_out io_in ≝
  mk_fullexec … RTL_exec ? make_initial_state.
*)