include "LTL/LTL.ma".
include "ERTL/Interference.ma".
include "ASM/Arithmetic.ma".
include "joint/TranslateUtils.ma".

(* Note: translation is complicated by having to preserve the carry bit and
  wanting to do it with as less boilerplate as possible. It could be somewhat
  simplified if constant and copy propagation was to be done after this pass:
  those optimisations would take care of the boilerplate for us.*)

coercion Reg_to_dec : ∀r:Register.decision ≝ decision_colour on _r : Register to decision.

inductive arg_decision : Type[0] ≝
  | arg_decision_colour : Register → arg_decision
  | arg_decision_spill : ℕ → arg_decision
  | arg_decision_imm : Byte → arg_decision.

coercion Reg_to_arg_dec : ∀r:Register.arg_decision ≝ arg_decision_colour on _r : Register to arg_decision.

(* Paolo: I'm changing the following: before, spilled registers were
  assigned stack addresses going from SP + #frame_size - #stack_params
  excluded down to SP included. I am turning it upside down, so that
  the offset does not need the stack size to be computed *)

definition preserve_carry_bit :
  ∀globals.bool → list (joint_seq LTL globals) → list (joint_seq LTL globals) ≝
  λglobals,do_it,steps.
  if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps.

(* for notation *)
definition A ≝ it.

coercion beval_of_byte : ∀b : Byte.beval ≝ BVByte on _b : Byte to beval.

(* spill should be byte-based from the start *)
definition set_dp_by_offset :
  ∀globals.nat → list (joint_seq LTL globals) ≝
  λglobals,off.
  [ A ← byte_of_nat off
  ; A ← A .Add. RegisterSPL
  ; RegisterDPL ← A
  ; A ← zero_byte
  ; A ← A .Addc. RegisterSPH
  ; RegisterDPH ← A
  ].

definition get_stack:
 ∀globals.Register → nat → list (joint_seq LTL globals) ≝
 λglobals,r,off.
 set_dp_by_offset ? off @
 [ LOAD … A it it ] @
 if eq_Register r RegisterA then [ ] else [ r ← A ].

definition set_stack_not_a :
 ∀globals.nat → Register → list (joint_seq LTL globals) ≝
 λglobals,off,r.
 set_dp_by_offset ? off @
 [ A ← r
 ; STORE … it it A ].

definition set_stack_a :
 ∀globals.nat → list (joint_seq LTL globals) ≝
 λglobals,off.
 [ RegisterST1 ← A ] @
 set_stack_not_a ? off RegisterST1.

definition set_stack :
 ∀globals.nat → Register → list (joint_seq LTL globals) ≝
 λglobals,off,r.
 if eq_Register r RegisterA then
   set_stack_a ? off
 else
   set_stack_not_a ? off r.
 
definition set_stack_int :
  ∀globals.nat → Byte →  list (joint_seq LTL globals) ≝
  λglobals,off,int.
  set_dp_by_offset ? off @
  [ A ← int
  ; STORE … it it A ].

definition move :
  ∀globals.bool → decision → arg_decision → list (joint_seq LTL globals) ≝
  λglobals,carry_lives_after,dst,src.
  match dst with
  [ decision_colour dstr ⇒
    match src with
    [ arg_decision_colour srcr ⇒
      if eq_Register dstr srcr then [ ] else
      if eq_Register dstr RegisterA then [ A ← srcr ] else
      if eq_Register srcr RegisterA then [ dstr ← A ] else
      [ A ← srcr ; dstr ← A]
    | arg_decision_spill srco ⇒
      preserve_carry_bit ? carry_lives_after
        (get_stack ? dstr srco)
    | arg_decision_imm int ⇒
      [ A ← int ] @
      if eq_Register dstr RegisterA then [ ] else
      [ dstr ← A ]
    ]
  | decision_spill dsto ⇒
    match src with
    [ arg_decision_colour srcr ⇒
      preserve_carry_bit ? carry_lives_after
        (set_stack ? dsto srcr)
    | arg_decision_spill srco ⇒
      if eqb srco dsto then [ ] else
      preserve_carry_bit ? carry_lives_after
        (get_stack ? RegisterA srco @
         set_stack ? dsto RegisterA)
    | arg_decision_imm int ⇒
      preserve_carry_bit ? carry_lives_after
        (set_stack_int ? dsto int)
    ]
  ].

definition arg_is_spilled : arg_decision → bool ≝
  λx.match x with [ arg_decision_spill _ ⇒ true | _ ⇒ false ].
definition is_spilled : decision → bool ≝
  λx.match x with [ decision_spill _ ⇒ true | _ ⇒ false ].

definition newframe :
  ∀globals.ℕ → list (joint_seq LTL globals) ≝
  λglobals,stack_sz.
  [ CLEAR_CARRY …
  ; A ← RegisterSPL
  ; A ← A .Sub. byte_of_nat stack_sz
  ; RegisterSPL ← A
  ; A ← RegisterSPH
  ; A ← A .Sub. zero_byte
  ; RegisterSPH ← A
  ].

definition delframe :
  ∀globals.ℕ → list (joint_seq LTL globals) ≝
  λglobals,stack_sz.
  [ A ← RegisterSPL
  ; A ← A .Add. byte_of_nat stack_sz
  ; RegisterSPL ← A
  ; A ← RegisterSPH
  ; A ← A .Addc. zero_byte
  ; RegisterSPH ← A
  ].

definition commutative : Op2 → bool ≝
λop.match op with
[ Add ⇒ true
| Addc ⇒ true
| Or ⇒ true
| Xor ⇒ true
| And ⇒ true
| _ ⇒ false
].

definition uses_carry : Op2 → bool ≝
λop.match op with
[ Addc ⇒ true
| Sub ⇒ true
| _ ⇒ false
].

definition sets_carry : Op2 → bool ≝
λop.match op with
[ Add ⇒ true
| Addc ⇒ true
| Sub ⇒ true
| _ ⇒ false
].

definition translate_op2 :
  ∀globals.bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
  λglobals,carry_lives_after,op,dst,arg1,arg2.
  (* this won't preserve the carry bit if op does not set it: left to next function *)
  (* if op uses carry bit (⇒ it sets it too) it must be preserved before the op *)
  (preserve_carry_bit ?
    (uses_carry op ∧ (arg_is_spilled arg1 ∨ arg_is_spilled arg2))
    (move ? false RegisterB arg2 @
     move ? false RegisterA arg1) @
    [ A ← A .op. RegisterB ] @
    (* it op sets the carry bit and it is needed afterwards it must be preserved here *)
    move ? (sets_carry op ∧ carry_lives_after) dst RegisterA).

definition translate_op2_smart :
  ∀globals.bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
  λglobals,carry_lives_after,op,dst,arg1,arg2.
  (* if op does not set carry bit (⇒ it does not use it either) then it must be
    preserved *)
  preserve_carry_bit ?
    (¬sets_carry op ∧ carry_lives_after ∧
      (arg_is_spilled arg1 ∨ arg_is_spilled arg2 ∨ is_spilled dst))
    (match arg2 with
    [ arg_decision_colour arg2r ⇒
      move ? (uses_carry op) RegisterA arg1 @
      [ A ← A .op. arg2r ] @
      move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
    | arg_decision_imm arg2i ⇒
      move ? (uses_carry op) RegisterA arg1 @
      [ A ← A .op. arg2i ] @
      move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
    | _ ⇒
      if commutative op then
        match arg1 with
        [ arg_decision_colour arg1r ⇒
          move ? (uses_carry op) RegisterA arg2 @
          [ A ← A .op. arg1r ] @
          move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
        | arg_decision_imm arg1i ⇒
          move ? (uses_carry op) RegisterA arg2 @
          [ A ← A .op. arg1i ] @
          move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
        | _ ⇒
          translate_op2 ? carry_lives_after op dst arg1 arg2
        ]
      else
        translate_op2 ? carry_lives_after op dst arg1 arg2
    ]).

definition dec_to_arg_dec : decision → arg_decision ≝
  λd.match d with
  [ decision_colour r ⇒ arg_decision_colour r
  | decision_spill n ⇒ arg_decision_spill n
  ].

coercion dec_arg_dec : ∀d:decision.arg_decision ≝ dec_to_arg_dec on _d : decision to arg_decision.

definition translate_op1 :
  ∀globals.bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝
  λglobals,carry_lives_after,op,dst,arg.
  let preserve_carry ≝ carry_lives_after ∧ (is_spilled dst ∨ is_spilled arg) in
  preserve_carry_bit ? preserve_carry
    (move ? false RegisterA arg @
     OP1 … op it it ::
     move ? false dst RegisterA).

definition translate_opaccs :
  ∀globals.bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
  λglobals,carry_lives_after,op,dst1,dst2,arg1,arg2.
  (* OPACCS always has dead carry bit and sets it to zero *)
  move ? false RegisterB arg2 @
  move ? false RegisterA arg1 @
  OPACCS … op it it it it ::
  move ? false dst1 RegisterA @
  move ? false dst2 RegisterB @
  if carry_lives_after ∧ (is_spilled dst1 ∨ is_spilled dst2) then
    [CLEAR_CARRY ??]
  else [ ].

(* does not preserve carry bit *)
definition move_to_dp :
  ∀globals.arg_decision → arg_decision → list (joint_seq LTL globals) ≝
  λglobals,arg1,arg2.
  if ¬arg_is_spilled arg1 then
    move ? false RegisterDPH arg2 @
    (* does not change dph because arg1 is not spilled *)
    move ? false RegisterDPL arg1
  else if ¬arg_is_spilled arg2 then
    move ? false RegisterDPL arg1 @
    (* does not change dpl because arg2 is not spilled *)
    move ? false RegisterDPH arg2
  else
    (* using B as temporary, as moving spilled registers tampers with DPTR *)
    move ? false RegisterB arg1 @
    move ? false RegisterDPH arg2 @
    move ? false RegisterDPL RegisterB.

definition translate_store :  
  ∀globals.bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
  λglobals,carry_lives_after,addr1,addr2,src.
  (* requires src != RegisterA and RegisterB *)
  preserve_carry_bit ? (carry_lives_after ∧
    (arg_is_spilled addr1 ∨ arg_is_spilled addr1 ∨ arg_is_spilled src))
    (let move_to_dptr ≝ move_to_dp ? addr1 addr2 in
     (if arg_is_spilled src then
        move ? false RegisterST0 src @
        move_to_dptr @
        [ A ← RegisterST0]
      else move_to_dptr) @
     [STORE … it it A]). 

definition translate_load :  
  ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
  λglobals,carry_lives_after,dst,addr1,addr2.
  preserve_carry_bit ? (carry_lives_after ∧
    (is_spilled dst ∨ arg_is_spilled addr1 ∨ arg_is_spilled addr1))
    (move_to_dp ? addr1 addr2 @
     [ LOAD … A it it ] @
     move ? false dst RegisterA).

definition translate_address :
  ∀globals.bool → ∀i.member ? (eq_identifier ?) i globals → decision → decision →
  list (joint_seq LTL globals) ≝
  λglobals,carry_lives_after,id,prf,addr1,addr2.
  preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2))
    (ADDRESS LTL ? id prf it it ::
     move ? false addr1 RegisterDPL @
     move ? false addr2 RegisterDPH).

definition translate_step:
  ∀globals.∀after : valuation register_lattice.
  coloured_graph after →
  ℕ → label → joint_step ERTL globals → seq_block LTL globals (joint_step LTL globals) ≝
  λglobals,after,grph,stack_sz,lbl,s.
  let lookup ≝ λr.colouring … grph (inl … r) in
  let lookup_arg ≝ λa.match a with
    [ Reg r ⇒ lookup r
    | Imm b ⇒ arg_decision_imm b
    ] in
  let carry_lives_after ≝ hlives RegisterCarry (after lbl) in
  let move ≝ move globals carry_lives_after in
  match s with
  [ step_seq s' ⇒
    match s' return λ_.seq_block LTL globals (joint_step LTL globals) with
    [ COMMENT c ⇒ COMMENT … c
    | COST_LABEL cost_lbl ⇒ COST_LABEL … cost_lbl
    | POP r ⇒
      POP … A ::
      move (lookup r) RegisterA
    | PUSH a ⇒
      move RegisterA (lookup_arg a) @
      [ PUSH … A ]
    | STORE addr1 addr2 srcr ⇒
      translate_store ? carry_lives_after
        (lookup_arg addr1)
        (lookup_arg addr2)
        (lookup_arg srcr)
    | LOAD dstr addr1 addr2 ⇒
      translate_load ? carry_lives_after
        (lookup dstr)
        (lookup_arg addr1)
        (lookup_arg addr2)
    | CLEAR_CARRY ⇒ CLEAR_CARRY …
    | SET_CARRY ⇒ CLEAR_CARRY …
    | OP2 op dst arg1 arg2 ⇒
      translate_op2_smart ? carry_lives_after op
        (lookup dst)
        (lookup_arg arg1)
        (lookup_arg arg2)
    | OP1 op dst arg ⇒
      translate_op1 ? carry_lives_after op
        (lookup dst)
        (lookup arg)
    | MOVE pair_regs ⇒
      let lookup_move_dst ≝ λx.match x return λ_.decision with
        [ PSD r ⇒ lookup r
        | HDW r ⇒ r
        ] in
      let dst ≝ lookup_move_dst (\fst pair_regs) in
      let src ≝
        match \snd pair_regs return λ_.arg_decision with
        [ Reg r ⇒ lookup_move_dst r
        | Imm b ⇒ arg_decision_imm b
        ] in
      move dst src
    | ADDRESS lbl prf dpl dph ⇒
      translate_address ? carry_lives_after
        lbl prf (lookup dpl) (lookup dph)
    | OPACCS op dst1 dst2 arg1 arg2 ⇒
      translate_opaccs ? carry_lives_after op
        (lookup dst1) (lookup dst2)
        (lookup_arg arg1) (lookup_arg arg2)
    | extension_seq ext ⇒
      match ext with
      [ ertl_new_frame ⇒ newframe ? stack_sz
      | ertl_del_frame ⇒ delframe ? stack_sz
      | ertl_frame_size r ⇒
        move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
      ]
    | CALL f n_args _ ⇒
      match f with
      [ inl f ⇒ [ CALL LTL ? (inl … f) n_args it ]
      | inr dp ⇒
        let 〈dpl, dph〉 ≝ dp in
        move_to_dp … (lookup_arg dpl) (lookup_arg dph) @
        [ CALL LTL ? (inr … 〈it, it〉) n_args it ]
      ]
    ]
  | COND r ltrue ⇒
    〈move RegisterA (lookup r),COND … it ltrue〉
  ].

definition translate_fin_step:
  ∀globals.label → joint_fin_step ERTL → seq_block LTL globals (joint_fin_step LTL) ≝
  λglobals,lbl,s.
  match s return λ_.seq_block LTL globals (joint_fin_step LTL) with
  [ RETURN ⇒ RETURN ?
  | GOTO l ⇒ GOTO ? l
  | TAILCALL abs _ _ ⇒ Ⓧabs
  ].

definition translate_internal: ∀globals: list ident.
  joint_closed_internal_function ERTL globals →
  joint_closed_internal_function LTL globals ≝
  λglobals,int_fun.
  (* initialize graph *)
  let entry ≝ pi1 … (joint_if_entry … int_fun) in
  let exit ≝ pi1 … (joint_if_exit … int_fun) in
  (* colour registers *)
  let after ≝ analyse_liveness globals int_fun in
  let coloured_graph ≝ build after in
  (* compute new stack size *)
  let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
  (* initialize internal function *)
  let init ≝ init_graph_if LTL globals
    (joint_if_luniverse … int_fun)
    (joint_if_runiverse … int_fun)
    it it [ ] stack_sz entry exit in
  graph_translate … 
    init
    (translate_step … coloured_graph stack_sz)
    (translate_fin_step …)
    int_fun.
cases daemon (* TODO *) qed.

definition ertl_to_ltl: ertl_program → ltl_program ≝
  λp.transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).