include "basics/lists/list.ma".
include "common/Globalenvs.ma".
include "common/IO.ma".
include "common/SmallstepExec.ma".
include "joint/BEMem.ma".
include "joint/Joint.ma".
include "ASM/I8051bis.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) ??? *)

record more_sem_params (p:params_): Type[1] ≝
 { framesT: Type[0]
 ; empty_framesT: framesT
 ; regsT: Type[0]
 ; empty_regsT: address → regsT (* Stack pointer *)
 ; call_args_for_main: call_args p
 ; call_dest_for_main: call_dest p

 ; 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 → res regsT
 }.

record sem_params: Type[1] ≝
 { spp :> params_
 ; more_sem_pars :> more_sem_params spp
 }.

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

(*
definition empty_state: ∀p. more_sem_params p → state p ≝
 mk_state … (empty_framesT …) 
*)

definition genv ≝ λglobals.λp:params globals. genv_t (joint_function globals p).

record more_sem_params1 (globals: list ident) (p: params globals) : Type[1] ≝
 { more_sparams :> more_sem_params p

 (*CSC: XXXX succ_pc, pointer_of_label and fetch_statement all deal with fetching
   should we take 'em out in a different record to simplify the code? *)
 ; succ_pc: succ p → address → res address
 ; pointer_of_label: genv … p → pointer → label → res (Σp:pointer. ptype p = Code)
 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)

 ; fetch_ra: state (mk_sem_params … more_sparams) → res ((state (mk_sem_params … more_sparams)) × address)
 ; result_regs: genv globals p → state (mk_sem_params … more_sparams) → res (list (generic_reg p))

 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
   (*CSC: save_frame returns a res only because we can call a function with the wrong number and
     type of arguments. To be fixed using a dependent type *)
 ; save_frame: address → nat → paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
 ; pop_frame: genv globals p → state (mk_sem_params … more_sparams) → res ((state (mk_sem_params … more_sparams)))

 ; fetch_external_args: external_function → state (mk_sem_params … more_sparams) → res (list val)
 ; set_result: list val → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
 }.

record sem_params1 (globals: list ident): Type[1] ≝
 { p1:> params globals
 ; more_sparams1:> more_sem_params1 globals p1
 }.

record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
 { more_sparams_1 :> more_sem_params1 … p
 ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams_1) → succ p → state (mk_sem_params … more_sparams_1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams_1)))
 }.

record sem_params2 (globals: list ident): Type[1] ≝
 { p2:> params globals
 ; more_sparams2:> more_sem_params2 globals p2
 }.

definition sem_params_of_sem_params1 ≝ λglobals. λsp1: sem_params1 globals. mk_sem_params sp1 sp1.
coercion sem_params_of_sem_params1 : ∀globals. ∀_x:sem_params1 globals. sem_params
 ≝ sem_params_of_sem_params1 on _x: sem_params1 ? to sem_params.

definition sem_params1_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params1 … sp2 sp2.
coercion sem_params1_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params1 globals
 ≝ sem_params1_of_sem_params2 on _x: sem_params2 ? to sem_params1 ?.

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

definition set_regs: ∀p:sem_params. regsT ? p → state p → state p ≝
 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … 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 (isp … st) (carry … st) (regs … st) (m … st).

definition set_isp: ∀p. pointer → state p → state p ≝
 λp,isp,st. mk_state … (st_frms … st) (pc … st) (sp … st) isp (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) (isp … 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) (isp … st) (carry … st) (regs … st) (m … st).

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


definition address_of_label: ∀globals. ∀p:sem_params1 globals. genv globals p → pointer → label → res address ≝
 λglobals,p,ge,ptr,l.
  do newptr ← pointer_of_label … p ge … ptr l ;
  OK … (address_of_code_pointer newptr).

definition goto: ∀globals. ∀p:sem_params1 globals. genv globals p → label → state p → res (state p) ≝
 λglobals,p,ge,l,st.
  do oldpc ← pointer_of_address (pc … st) ;
  do newpc ← address_of_label … ge oldpc l ;
  OK … (set_pc … newpc st).

definition next: ∀globals. ∀p:sem_params1 globals. succ … p → state p → res (state p) ≝
 λglobals,p,l,st.
  do l' ← succ_pc … p l (pc … st) ;
  OK … (set_pc … 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 → res (state p) ≝
 λp,st,rs.
  do regs ← pair_reg_move_ … (regs … st) rs;
  OK … (set_regs … regs st).

axiom FailedStore: String.

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

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

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

definition load_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.
axiom BadPointer : String.

definition eval_call_block:
 ∀globals.∀p:sem_params1 globals. genv globals p → state p →
  block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
 λglobals,p,ge,st,b,args,dest,ra.
  ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr … ge b) : IO ???;
    match fd with
    [ Internal fn ⇒
      ! st ← save_frame … ra (joint_if_stacksize … fn) (joint_if_params … fn) args dest st ;
      let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
      let l' ≝ joint_if_entry … fn in
      let st ≝ set_regs p regs st in
      let pointer_in_fn ≝ mk_pointer (mk_block Code (block_id b)) zero_offset in
      ! newpc ← address_of_label … ge pointer_in_fn l' ;
      let st ≝ set_pc … newpc st in
       return 〈 E0, st〉
    | External fn ⇒
      ! params ← fetch_external_args … fn st : IO ???;
      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
      ! 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. To be
         fixed once we fully implement external functions. *)
      let vs ≝ [mk_val ? evres] in
      ! st ← set_result … vs st;
      let st ≝ set_pc … ra st in
        return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
     ].
(*% qed.*)

definition eval_call_id:
 ∀globals.∀p:sem_params1 globals. genv globals p → state p →
  ident → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
 λglobals,p,ge,st,id,args,dest,ra.
  ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
  eval_call_block … ge st b args dest ra.

definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
 λglobals,p,ge,st.
  ! s ← fetch_statement … ge st : IO ???;
  match s return λ_. IO ??? with
    [ GOTO l ⇒
       ! st ← goto … p ge l st ;
       return 〈E0, st〉
    | sequential seq l ⇒
      match seq return λ_. IO ??? with
      [ extension c ⇒ exec_extended … p ge c l st
      | COST_LABEL cl ⇒
         ! st ← next … p l st ;
         return 〈Echarge cl, st〉
      | COMMENT c ⇒
         ! st ← next … p l st ;
         return 〈E0, st〉
      | INT dest v ⇒
         ! st ← greg_store p dest (BVByte v) st;
         ! st ← next … p l st ;
          return 〈E0, st〉
      | LOAD dst addrl addrh ⇒
        ! vaddrh ← dph_retrieve … st addrh;
        ! vaddrl ← dpl_retrieve … st addrl;
        ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
        ! st ← acca_store p … dst v st;
        ! st ← next … p l st ;
          return 〈E0, st〉
      | STORE addrl addrh src ⇒
        ! vaddrh ← dph_retrieve … st addrh;
        ! vaddrl ← dpl_retrieve … st addrl;
        ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
        ! v ← acca_retrieve … st src;
        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
        let st ≝ set_m … m' st in
        ! st ← next … p l st ;
          return 〈E0, st〉
      | COND src ltrue ⇒
        ! v ← acca_retrieve … st src;
        ! b ← bool_of_beval v;
        if b then
         ! st ← goto … p ge ltrue st ;
         return 〈E0, st〉
        else
         ! st ← next … p l st ;
         return 〈E0, st〉
      | ADDRESS ident prf ldest hdest ⇒
        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol … ge ident);
        ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer addr zero_offset);
        ! st ← dpl_store p ldest laddr st;
        ! st ← dph_store p hdest haddr st;
        ! st ← next … p l st ;
          return 〈E0, st〉
      | OP1 op dacc_a sacc_a ⇒
        ! v ← acca_retrieve … st sacc_a;
        ! v ← Byte_of_val v;
          let v' ≝ BVByte (op1 eval op v) in
        ! st ← acca_store p dacc_a v' st;
        ! st ← next … p l st ;
          return 〈E0, st〉
      | OP2 op dacc_a sacc_a src ⇒
        ! v1 ← acca_retrieve … st sacc_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 p dacc_a v' st;
          let st ≝ set_carry … carry st in
        ! st ← next … p l st ;
          return 〈E0, st〉
      | CLEAR_CARRY ⇒
        ! st ← next … p l (set_carry … BVfalse st) ;
         return 〈E0, st〉
      | SET_CARRY ⇒
        ! st ← next … p l (set_carry … BVtrue st) ;
         return 〈E0, st〉
      | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
        ! v1 ← acca_retrieve … st sacc_a_reg;
        ! v1 ← Byte_of_val v1;
        ! v2 ← accb_retrieve … st sacc_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 p dacc_a_reg v1' st;
        ! st ← accb_store p dacc_b_reg v2' st;
        ! st ← next … p l st ;
          return 〈E0, st〉
      | POP dst ⇒
        ! 〈st,v〉 ← pop … st;
        ! st ← acca_store p dst v st;
        ! st ← next … p l st ;
          return 〈E0, st〉
      | PUSH src ⇒
        ! v ← acca_retrieve … st src;
        ! st ← push … st v;
        ! st ← next … p l st ;
          return 〈E0, st〉
      | MOVE dst_src ⇒
        ! st ← pair_reg_move … st dst_src ;
        ! st ← next … p l st ;
          return 〈E0, st〉
      | CALL_ID id args dest ⇒
        ! ra ← succ_pc … p l (pc … st) : IO ???;          
          eval_call_id … p ge st id args dest ra ]
    | RETURN ⇒
      ! 〈st,ra〉 ← fetch_ra … st;
      ! st ← pop_frame … ge st;
        return 〈E0,set_pc … ra st〉].
(*cases addr //
qed.*)

definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. genv … p → address → state p → option int ≝
 λglobals,p,ge,exit,st.res_to_opt ? (
  do s ← fetch_statement … ge st;
  match s with
   [ RETURN ⇒
      do 〈st,ra〉 ← fetch_ra … st;
      if eq_address ra exit then
       do regs ← result_regs … ge st ;
       do vals ← mmap … (λreg.greg_retrieve … st reg) regs ;
       Word_of_list_beval vals
      else
       Error ? []
   | _ ⇒ Error ? []]).

record evaluation_parameters : Type[1] ≝
 { globals: list ident
 ; sparams2: sem_params2 globals
 ; exit: address
 ; genv2: genv globals sparams2
 }.

definition joint_exec: trans_system io_out io_in ≝
  mk_trans_system … evaluation_parameters (λG. state (sparams2 G))
   (λG.is_final (globals G) (sparams2 G) (genv2 G) (exit G))
   (λG.eval_statement (globals G) (sparams2 G) (genv2 G)).

definition make_global :
 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
  joint_program pars → evaluation_parameters
≝
 λpars,sparams.
 (* Invariant: a -1 block is unused in common/Globalenvs *)
 let b ≝ mk_block Code (-1) in
 let ptr ≝ mk_pointer b zero_offset in
 let addr ≝ address_of_code_pointer ptr in
  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) addr (globalenv_noinit … p)).
% qed.

axiom ExternalMain: String.
definition make_initial_state :
 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
 ∀p: joint_program … pars. res (state (mk_sem_params (pars (prog_var_names … p)) (sparams p))) ≝
λpars,sparams,p.
  let sem_globals ≝ make_global pars sparams p in
  let ge ≝ genv2 sem_globals in
  let m ≝ alloc_mem … p in
  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
  let dummy_pc ≝ mk_pointer (mk_block Code (-1)) zero_offset in
  let spp ≝ mk_pointer spb (offset_of_Z external_ram_size) in
  let ispp ≝ mk_pointer ispb (offset_of_Z 47) in
  do sp ← address_of_pointer spp ;
  let main ≝ prog_main … p in
  let st0 ≝ mk_state … (empty_framesT …) sp ispp dummy_pc BVfalse (empty_regsT … sp) m in
  let trace_state ≝
   eval_call_id … (mk_sem_params1 … (sparams …)) ge st0 main (call_args_for_main … (sparams …))
    (call_dest_for_main … (sparams …)) (exit sem_globals) in
  match trace_state with
  [ Value tr_st ⇒ OK … (\snd tr_st) (* E0 trace thrown away *)
  | Wrong msg ⇒ Error … msg
  | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
  ].
(*[3: % | cases ispb | cases spb] *; #r #off #E >E %
qed.*)

definition joint_fullexec :
 ∀pars:∀globals.params globals.
 ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
 fullexec io_out io_in ≝
 λpars,sparams.
  mk_fullexec ??? joint_exec (make_global pars sparams) (make_initial_state pars sparams).