include "RTL/RTLTailcall.ma".
include "utilities/RegisterSet.ma".
include "common/Identifiers.ma".
include "ERTL/ERTL.ma".
include "joint/TranslateUtils.ma".

include alias "basics/lists/list.ma".

definition save_hdws ≝
 λglobals,l.
  let save_hdws_internal ≝
   λdestr_srcr.λstart_lbl.
    let 〈destr, srcr〉 ≝ destr_srcr in
     adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈pseudo destr,hardware srcr〉) ] start_lbl
  in
   map ? ? save_hdws_internal l.

definition restore_hdws ≝
  λglobals,l.
   let restore_hdws_internal ≝
    λsrcr_destr: register × Register.
    λstart_lbl: label.
     let 〈srcr, destr〉 ≝ srcr_destr in
     adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈hardware destr, pseudo srcr〉) ] start_lbl
   in
    map ? ? restore_hdws_internal l.

definition get_params_hdw ≝
  λglobals.
  λparams: list register.
  match params with
  [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ GOTO … ] start_lbl]
  | _ ⇒
    let l ≝ zip_pottier ? ? params RegisterParams in
      save_hdws globals l ].

definition get_param_stack ≝
  λglobals.
  λoff: nat.
  λdestr.
  λstart_lbl, dest_lbl: label.
  λdef.
  let 〈def, addr1〉 ≝ fresh_reg … def in
  let 〈def, addr2〉 ≝ fresh_reg … def in
  let 〈def, tmpr〉 ≝ fresh_reg … def in
  let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in
  adds_graph ertl_params1 globals [
    sequential ertl_params_ … (extension … (ertl_st_ext_frame_size addr1));
    sequential ertl_params_ … (INT … tmpr int_offset);
    sequential ertl_params_ … (OP2 … Sub addr1 addr1 tmpr);
    sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉);
    sequential ertl_params_ … (OP2 … Add addr1 addr1 tmpr);
    sequential ertl_params_ … (INT … addr2 (bitvector_of_nat 8 0));
    sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
    sequential ertl_params_ … (OP2 … Addc addr2 addr2 tmpr);
    sequential ertl_params_ … (LOAD … destr addr1 addr2)
  ] start_lbl dest_lbl def.
  
definition get_params_stack ≝
  λglobals,params.
  match params with
  [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl ]
  | _ ⇒ mapi ? ? (get_param_stack globals) params ].

definition get_params ≝
  λglobals,params.
  let n ≝ min (length … params) (length … RegisterParams) in
  let 〈hdw_params, stack_params〉 ≝ list_split … n params in
  let hdw_params ≝ get_params_hdw globals hdw_params in
    hdw_params @ (get_params_stack … stack_params).

definition add_prologue ≝
  λglobals.
  λparams: list register.
  λsral.
  λsrah.
  λsregs.
  λdef.
  let start_lbl ≝ joint_if_entry … (ertl_params globals) def in
  let 〈tmp_lbl, def〉 ≝ fresh_label … def in
  match lookup … (joint_if_code … def) start_lbl
    return λx. x ≠ None ? → ertl_internal_function globals with
  [ None ⇒ λnone_absrd. ⊥
  | Some last_stmt ⇒ λsome_prf.
    let def ≝
      add_translates …
         ((adds_graph ertl_params1 … [
  		     sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame)
  		   ]) ::
         (adds_graph ertl_params1 … [
  		      sequential ertl_params_ … (POP … sral);
  		      sequential ertl_params_ … (POP … srah)
  		   ]) ::
         (save_hdws … sregs) @
         (get_params … params))
        start_lbl tmp_lbl def
    in
      add_graph … tmp_lbl last_stmt def
  ] ?.
[ cases start_lbl #x #H cases daemon (* @H *) (*CSC: XXXX, no Russell *)
| cases (none_absrd) /2/ ]
qed.

definition save_return ≝
  λglobals.
  λret_regs.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef: ertl_internal_function globals.
  let 〈def, tmpr〉 ≝ fresh_reg … def in
  match reduce_strong ? ? RegisterSTS ret_regs with
  [ mk_Sig crl crl_proof ⇒
    let commonl ≝ \fst (\fst crl) in
    let commonr ≝ \fst (\snd crl) in
    let restl ≝ \snd (\fst crl) in
    let restr ≝ \snd (\snd crl) in
    let init_tmpr ≝ sequential ertl_params_ … (INT … tmpr (zero …)) in
    let f_save ≝ λst. λr. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo r〉) in
    let saves ≝ map2 … f_save commonl commonr crl_proof in
    let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) in
    let defaults ≝ map … f_default restl in
      adds_graph ertl_params1 ? (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
  ].

definition assign_result ≝
  λglobals.λstart_lbl: label.
  match reduce_strong ? ? RegisterRets RegisterSTS with
  [ mk_Sig crl crl_proof ⇒
    let commonl ≝ \fst (\fst crl) in
    let commonr ≝ \fst (\snd crl) in
    let f ≝ λret. λst. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) in
    let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
      adds_graph ertl_params1 … insts start_lbl
  ].

definition add_epilogue ≝
  λglobals.
  λret_regs.
  λsral.
  λsrah.
  λsregs.
  λdef.
  let start_lbl ≝ joint_if_exit … (ertl_params globals) def in
  let 〈tmp_lbl, def〉 ≝ fresh_label … def in
  match lookup … (joint_if_code … def) start_lbl
    return λx. x ≠ None ? → ertl_internal_function globals with
  [ None ⇒ λnone_absrd. ⊥
  | Some last_stmt ⇒ λsome_prf.
    let def ≝
      add_translates ertl_params1 … (
        [save_return globals ret_regs] @
        restore_hdws … sregs @
        [adds_graph ertl_params1 … [
          sequential ertl_params_ … (PUSH … srah);
          sequential ertl_params_ … (PUSH … sral)
        ]] @
        [adds_graph ertl_params1 … [
          sequential ertl_params_ … (extension … ertl_st_ext_del_frame)
        ]] @
        [assign_result globals]
      ) start_lbl tmp_lbl def
    in
    let def' ≝ add_graph … tmp_lbl last_stmt def in
      set_joint_if_exit … tmp_lbl def' ?
  ] ?.
[ cases start_lbl #x #H cases daemon (* @H *) (* CSC: XXXX *)
| cases (none_absrd) /2/
| cases daemon (* CSC: XXXXX *)
]
qed.
  

definition allocate_regs ≝
  λglobals.
  λrs.
  λsaved: rs_set rs.
  λdef.
   let allocate_regs_internal ≝
    λr: Register.
    λdef_sregs.
    let 〈def, sregs〉 ≝ def_sregs in
    let 〈def, r'〉 ≝ fresh_reg ertl_params0 globals def in
      〈def, 〈r', r〉 :: sregs〉
   in
    rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
   
definition add_pro_and_epilogue ≝
  λglobals.
  λparams.
  λret_regs.
  λdef.
  match fresh_regs_strong … globals def 2 with
  [ mk_Sig def_sra def_sra_proof ⇒
    let def ≝ \fst def_sra in
    let sra ≝ \snd def_sra in
    let sral ≝ nth_safe ? 0 sra ? in
    let srah ≝ nth_safe ? 1 sra ? in
    let 〈def, sregs〉 ≝ allocate_regs … register_list_set RegisterCalleeSaved def in
    let def ≝ add_prologue … params sral srah sregs def in
    let def ≝ add_epilogue … ret_regs sral srah sregs def in
      def
  ].
>def_sra_proof //
qed.

definition set_params_hdw ≝
  λglobals,params.
  match params with
  [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl]
  | _ ⇒
    let l ≝ zip_pottier ? ? params RegisterParams in
      restore_hdws globals l
  ].

definition set_param_stack ≝
  λglobals.
  λoff.
  λsrcr.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef: ertl_internal_function globals.
  let 〈def, addr1〉 ≝ fresh_reg … def in
  let 〈def, addr2〉 ≝ fresh_reg … def in
  let 〈def, tmpr〉 ≝ fresh_reg … def in
  let 〈ignore, int_off〉 ≝ half_add ? off int_size in
    adds_graph ertl_params1 … [
      sequential ertl_params_ … (INT … addr1 int_off);
      sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉);
      sequential ertl_params_ … (CLEAR_CARRY …);
      sequential ertl_params_ … (OP2 … Sub addr1 tmpr addr1);
      sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
      sequential ertl_params_ … (INT … addr2 (zero ?));
      sequential ertl_params_ … (OP2 … Sub addr2 tmpr addr2);
      sequential ertl_params_ … (STORE … addr1 addr2 srcr)
    ] start_lbl dest_lbl def.    

definition set_params_stack ≝
  λglobals,params.
  match params with
  [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO …] start_lbl]
  | _ ⇒
    let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in
      mapi ? ? f params].

definition set_params ≝
  λglobals,params.
  let n ≝ min (|params|) (|RegisterParams|) in
  let hdw_stack_params ≝ split ? params n ? in
  let hdw_params ≝ \fst hdw_stack_params in
  let stack_params ≝ \snd hdw_stack_params in
    set_params_hdw globals hdw_params @ set_params_stack globals stack_params.
normalize nodelta /2/
qed.

definition fetch_result ≝
  λglobals.
  λret_regs.
  λstart_lbl: label.
  match reduce_strong ? ? RegisterSTS RegisterRets with
  [ mk_Sig crl first_crl_proof ⇒
    let commonl ≝ \fst (\fst crl) in
    let commonr ≝ \fst (\snd crl) in
    let f_save ≝ λst. λret. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) in
    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
    match reduce_strong ? ? ret_regs RegisterSTS with
    [ mk_Sig crl second_crl_proof ⇒
      let commonl ≝ \fst (\fst crl) in
      let commonr ≝ \fst (\snd crl) in
      let f_restore ≝ λr. λst. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) in
      let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
        adds_graph ertl_params1 … (saves @ restores) start_lbl]].
[@second_crl_proof | @first_crl_proof]
qed.

definition translate_call_id ≝
  λglobals,f.
  λargs.
  λret_regs.
  λstart_lbl.
  λdest_lbl.
  λdef.
  let nb_args ≝ |args| in
    add_translates ertl_params1 globals (
      set_params … args @ [
      adds_graph ertl_params1 … [ sequential ertl_params_ … (CALL_ID … f nb_args it) ];
      fetch_result … ret_regs
      ]
    ) start_lbl dest_lbl def.

definition translate_stmt :
 ∀globals: list ident. label → rtlntc_statement globals → ertl_internal_function globals → ertl_internal_function globals
 ≝
  λglobals.
  λlbl.
  λstmt.
  λdef.
  match stmt with
  [ GOTO lbl' ⇒ add_graph … lbl (GOTO … lbl') def
  | RETURN ⇒ add_graph … lbl (RETURN …) def
  | sequential seq lbl' ⇒
     match seq with
      [ PUSH _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
      | POP _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
      | CALL_ID f args ret_regs ⇒
         translate_call_id … f args ret_regs lbl lbl' def
      | MOVE rs ⇒
         let 〈r1,r2〉 ≝ rs in
         let rs ≝ 〈pseudo r1, pseudo r2〉 in
          add_graph ertl_params1 ? lbl (sequential … (MOVE … rs) lbl') def
      | extension ext ⇒
         match ext with
          [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *)
          | rtlntc_st_ext_stack_address r1 r2 ⇒
             adds_graph ertl_params1 … [
              sequential ertl_params_ … (MOVE … 〈pseudo r1, hardware RegisterSPL〉);
              sequential ertl_params_ … (MOVE … 〈pseudo r2, hardware RegisterSPH〉)
             ] lbl lbl' def]
      (*CSC: everything is just copied to re-type it from now on;
        the problem is call_id that takes different parameters, but that is pattern-matched
        above. It could be made nicer at the cost of making all the rest of the code uglier *)
      | COST_LABEL cost_lbl ⇒ add_graph ertl_params1 … lbl (sequential … (COST_LABEL … cost_lbl) lbl') def
      | ADDRESS x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (sequential … (ADDRESS … x prf r1 r2) lbl') def
      | INT r i ⇒  add_graph ertl_params1 … lbl (sequential … (INT … r i) lbl') def
      | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
          add_graph ertl_params1 … lbl (sequential … (OPACCS … op destr1 destr2 srcr1 srcr2) lbl') def
      | OP1 op1 destr srcr ⇒
        add_graph ertl_params1 … lbl (sequential … (OP1 … op1 destr srcr) lbl') def
      | OP2 op2 destr srcr1 srcr2 ⇒
        add_graph ertl_params1 … lbl (sequential … (OP2 … op2 destr srcr1 srcr2) lbl') def
      | CLEAR_CARRY ⇒
        add_graph ertl_params1 … lbl (sequential … (CLEAR_CARRY …) lbl') def
      | SET_CARRY ⇒
        add_graph ertl_params1 … lbl (sequential … (SET_CARRY …) lbl') def
      | LOAD destr addr1 addr2 ⇒
        add_graph ertl_params1 … lbl (sequential … (LOAD … destr addr1 addr2) lbl') def
      | STORE addr1 addr2 srcr ⇒
        add_graph ertl_params1 … lbl (sequential … (STORE … addr1 addr2 srcr) lbl') def
      | COND srcr lbl_true ⇒
        add_graph ertl_params1 … lbl (sequential … (COND … srcr lbl_true) lbl') def
      | COMMENT msg ⇒
        add_graph ertl_params1 … lbl (sequential … (COMMENT … msg) lbl') def
      ]].
  @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)
qed.

(* hack with empty graphs used here *)
definition translate_funct_internal ≝
  λglobals.λdef:rtlntc_internal_function globals.
  let nb_params ≝ |joint_if_params ?? def| in
  let added_stacksize ≝ max 0 (minus nb_params (|RegisterParams|)) in
  let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in
  let entry' ≝ joint_if_entry … def in
  let exit' ≝ joint_if_exit … def in
  let graph' ≝ add ? ? (empty_map ? ?) entry' (GOTO … entry') in
  let graph' ≝ add ? ? graph' exit' (GOTO … exit') in
  let def' ≝
    mk_joint_internal_function globals (ertl_params globals)
      (joint_if_luniverse … def) (joint_if_runiverse … def) (joint_if_result … def) (*CSC: different from OCaml code where joint_if_result is unit*)
      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
      graph' ? ? in
  let def' ≝ foldi ? ? ? (translate_stmt globals) (joint_if_code … def) def' in
   add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
whd in match ertl_params; (* CSC: Matita's bug here; not enough/too much reduction
                                 makes the next application fail. Why? *)    
%
 [ @entry' | @graph_add_lookup @graph_add
 | @exit'  | @graph_add ]
qed.

definition generate ≝
  λglobals.
  λstmt.
  λdef: joint_internal_function … (ertl_params globals).
  let 〈entry, def〉 ≝ fresh_label … def in
  let graph ≝ add … (joint_if_code … def) entry stmt in
   set_joint_if_graph … (ertl_params globals) graph def ??.
  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
    *) cases daemon (*CSC: XXX *)
  ]
qed.

let rec find_and_remove_first_cost_label_internal (globals: list ident)
  (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat)
    on num_nodes ≝
  match num_nodes with
  [ O ⇒ 〈None ?, def〉
  | S num_nodes' ⇒
    match lookup … (joint_if_code … def) lbl with
    [ None ⇒ 〈None ?, def〉
    | Some stmt ⇒ 
      match stmt with
      [ sequential inst lbl ⇒
         match inst with
          [ COST_LABEL cost_lbl ⇒
             〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉
          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
      | RETURN ⇒ 〈None …, def〉
      | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
      ]]].
    
definition find_and_remove_first_cost_label ≝
  λglobals,def.  
    find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)).

definition move_first_cost_label_up_internal ≝
  λglobals,def.
  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in
  match cost_label with
  [ None ⇒ def
  | Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
  ].

definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).

definition rtl_to_ertl : rtl_program → ertl_program ≝
 λp.
  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
    transform_program ??? p (transf_fundef ?? (translate_funct …)).