include "utilities/BitVectorTrieSet.ma".
include "utilities/state.ma".

include "ASM/Util.ma".
include "ASM/ASM.ma".

include "LIN/LIN.ma".

(* utilities to provide Identifier's and addresses  *)
record ASM_universe : Type[0] :=
{ id_univ : universe ASMTag
; current_funct : ident
; ident_map : identifier_map SymbolTag Identifier
; label_map : identifier_map SymbolTag (identifier_map LabelTag Identifier)
; fresh_cost_label: Pos
}.

definition report_cost:
 costlabel → state_monad ASM_universe unit ≝
 λcl,u.
  let clw ≝ word_of_identifier … cl in
  if leb (fresh_cost_label … u) clw then
   〈mk_ASM_universe … (id_univ … u) (current_funct … u) (ident_map … u)
    (label_map … u) (succ clw), it〉  
  else
   〈u,it〉.

definition Identifier_of_label :
  label → state_monad ASM_universe Identifier ≝
λl,u.
let current ≝ current_funct … u in
let lmap ≝ lookup_def … (label_map … u) current (empty_map …) in
let 〈id, univ, lmap〉 ≝
  match lookup … lmap l with
  [ Some id ⇒ 〈id, id_univ … u, lmap〉
  | None ⇒
    let 〈id, univ〉 ≝ fresh … (id_univ … u) in
    〈id, univ, add … lmap l id〉
  ] in
〈mk_ASM_universe … univ current (ident_map … u) (add … (label_map … u) current lmap)
  (fresh_cost_label … u), id〉.

definition Identifier_of_ident :
  ident → state_monad ASM_universe Identifier ≝
λi,u.
let imap ≝ ident_map … u in
let res ≝ match lookup … imap i with
  [ Some id ⇒ 〈id, id_univ … u, imap〉
  | None ⇒
    let 〈id, univ〉 ≝ fresh … (id_univ … u) in
    〈id, univ, add … imap i id〉
  ] in
let id ≝ \fst (\fst res) in
let univ ≝ \snd (\fst res) in
let imap ≝ \snd res in
〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u)
  (fresh_cost_label … u), id〉.

definition new_ASM_universe :
∀p : joint_program LIN.ASM_universe ≝
λp.
mk_ASM_universe (mk_universe … one)
  (an_identifier … one (* dummy *))
  (empty_map …) (empty_map …) one.
(*@hide_prf normalize nodelta
cases p -p * #vars #functs #main #cost_init
#i #H
normalize nodelta
letin init_val ≝ (〈empty_map SymbolTag Identifier, mk_universe ASMTag one〉)
cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars))
[ %2{H} ] -H
lapply i -i lapply init_val -init_val
whd in match prog_var_names; normalize nodelta
elim vars -vars
[2: ** #id #r #v #tl #IH ] #init_val #i
[2: * [2: * ] #H @H ]
* [2: #H cases (orb_Prop_true … H) -H ] #H
@IH
[ %1 cases init_val normalize nodelta #init_map #off
  >(proj1 ?? (eqb_true ???) H) @pair_elim #lft #rgt #_ @mem_set_add_id
| %2{H}
| %1 cases init_val in H; normalize nodelta #init_map #off #H
  @pair_elim #lft #rgt #_
  >mem_set_add @orb_Prop_r @H
]
qed.
*)

definition start_funct_translation :
  ∀globals,functions.(ident × (joint_function LIN globals functions)) →
    state_monad ASM_universe unit ≝
  λg,functs,id_f,u.
    〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u)
      (fresh_cost_label … u), it〉.

definition ASM_fresh :
  state_monad ASM_universe Identifier ≝
λu.let 〈id, univ〉 ≝ fresh … (id_univ … u) in
〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u)
  (fresh_cost_label … u), id〉.

definition register_address: Register → [[ acc_a; direct; registr ]] ≝
  λr: Register.
    match r with
    [ Register00 ⇒ REGISTER [[ false; false; false ]]
    | Register01 ⇒ REGISTER [[ false; false; true ]]
    | Register02 ⇒ REGISTER [[ false; true; false ]]
    | Register03 ⇒ REGISTER [[ false; true; true ]]
    | Register04 ⇒ REGISTER [[ true; false; false ]]
    | Register05 ⇒ REGISTER [[ true; false; true ]]
    | Register06 ⇒ REGISTER [[ true; true; false ]]
    | Register07 ⇒ REGISTER [[ true; true; true ]]
    | RegisterA ⇒ ACC_A
    | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
    | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 130)
    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 131)
    | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r)) 
    ]. @I qed.

definition vector_cast :
∀A,n,m.A → Vector A n → Vector A m ≝
λA,n,m,dflt,v.
If leb n m then with prf do
  replicate … (m - n) dflt @@ v ⌈Vector ?? ↦ ?⌉
else with prf do
  \snd (vsplit … (v ⌈Vector ?? ↦ Vector ? (n - m + m)⌉)).
lapply prf @(leb_elim n)
[2,3: #_ * #abs elim (abs I) ]
#H #_ >commutative_plus_faster @eq_f [@sym_eq] @(minus_to_plus … (refl …))
[ assumption ]
@(transitive_le … (not_le_to_lt … H)) %2 %1
qed.

definition arg_address : hdw_argument → 
  [[ acc_a ; direct ; registr ; data ]] ≝
  λa.
  match a
  with
  [ Reg r ⇒ (register_address r : [[ acc_a ; direct ; registr ; data ]])
  | Imm v ⇒ (DATA v : [[ acc_a ; direct ; registr ; data ]])
  ].
  [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector ] @I
qed.

definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).

definition data_of_int ≝ λbv. DATA bv.
definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).

(* TODO: check and change to free bit *)
definition asm_other_bit ≝ BIT_ADDR (zero_byte).
definition one_word : Word ≝ bv_zero 15 @@ [[ true ]].

definition translate_statements :
  ∀globals.
  joint_statement LIN globals →
  state_monad ASM_universe pseudo_instruction ≝
  λglobals,statement.
  match statement with
  [ final instr ⇒
    match instr with
    [ GOTO lbl ⇒
      ! lbl' ← Identifier_of_label … lbl ;
      return Jmp (toASM_ident ? lbl')
    | RETURN ⇒ return Instruction (RET ?)
    | TAILCALL abs _ _ ⇒ Ⓧabs
    ]
  | sequential instr _ ⇒
      match instr with
      [ step_seq instr' ⇒
        match instr' with
        [ extension_seq ext ⇒
          match ext with
          [ SAVE_CARRY ⇒
            return Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))
          | RESTORE_CARRY ⇒
            return Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
          | LOW_ADDRESS lbl ⇒
            ! lbl' ← Identifier_of_label … lbl ;
            return Mov (inr ?? 〈register_address RegisterA, LOW〉) lbl' one_word
          | HIGH_ADDRESS lbl ⇒
            ! lbl' ← Identifier_of_label … lbl ;
            return Mov (inr ?? 〈register_address RegisterA, HIGH〉) lbl' one_word
          ]
        | COMMENT comment ⇒ return Comment comment
        | POP _ ⇒ return Instruction (POP ? accumulator_address)
        | PUSH _ ⇒ return Instruction (PUSH ? accumulator_address)
        | CLEAR_CARRY ⇒ return Instruction (CLR ? CARRY)
        | OPACCS accs _ _ _ _ ⇒
          return match accs with
          [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
          | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
          ]
        | OP1 op1 _ _ ⇒
          return match op1 with
          [ Cmpl ⇒ Instruction (CPL ? ACC_A)
          | Inc ⇒ Instruction (INC ? ACC_A)
          | Rl ⇒ Instruction (RL ? ACC_A)
          ]
        | OP2 op2 _ _ reg ⇒
          return match arg_address … reg
          return λx.is_in … [[ acc_a;
                                 direct;
                                 registr;
                                 data ]] x → ? with
          [ ACC_A ⇒ λacc_a: True.
            match op2 with
            [ Add ⇒ Instruction (ADD ? ACC_A accumulator_address)
            | Addc ⇒ Instruction (ADDC ? ACC_A accumulator_address)
            | Sub ⇒ Instruction (SUBB ? ACC_A accumulator_address)
            | Xor ⇒ Instruction (CLR ? ACC_A)
            | _ ⇒ Instruction (NOP ?)
            ]
          | DIRECT d ⇒ λdirect1: True.
            match op2 with
            [ Add ⇒ Instruction (ADD ? ACC_A (DIRECT d))
            | Addc ⇒ Instruction (ADDC ? ACC_A (DIRECT d))
            | Sub ⇒ Instruction (SUBB ? ACC_A (DIRECT d))
            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
            ]
          | REGISTER r ⇒ λregister1: True.
            match op2 with
            [ Add ⇒ Instruction (ADD ? ACC_A (REGISTER r))
            | Addc ⇒ Instruction (ADDC ? ACC_A (REGISTER r))
            | Sub ⇒ Instruction (SUBB ? ACC_A (REGISTER r))
            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
            ]
          | DATA b ⇒ λdata : True.
            match op2 with
            [ Add ⇒ Instruction (ADD ? ACC_A (DATA b))
            | Addc ⇒ Instruction (ADDC ? ACC_A (DATA b))
            | Sub ⇒ Instruction (SUBB ? ACC_A (DATA b))
            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉))
            ]
          | _ ⇒ Ⓧ
          ] (subaddressing_modein …)
        | LOAD _ _ _ ⇒ return Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
        | STORE _ _ _ ⇒ return Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
        | ADDRESS id proof off _ _ ⇒
          ! Id ← Identifier_of_ident … id ;
          return (Mov (inl ?? DPTR) Id off)
        | SET_CARRY ⇒
          return Instruction (SETB ? CARRY)
        | MOVE regs ⇒
          return match regs with
          [ to_acc _ reg ⇒
            match register_address reg return λx.is_in … [[ acc_a;
                                                              direct;
                                                              registr]] x → ? with
           [ REGISTER r ⇒ λregister9: True.
             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
           | DIRECT d ⇒ λdirect9: True.
             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
           | ACC_A ⇒ λacc_a: True.
             Instruction (NOP ?)
           | _ ⇒ Ⓧ
           ] (subaddressing_modein …)
         | from_acc reg _ ⇒
            match register_address reg return λx.is_in … [[ acc_a;
                                                              direct;
                                                              registr ]] x → ? with
            [ REGISTER r ⇒ λregister8: True.
             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
            | ACC_A ⇒ λacc: True.
             Instruction (NOP ?)
            | DIRECT d ⇒ λdirect8: True.
             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
            | _ ⇒ Ⓧ
            ] (subaddressing_modein …)
          | int_to_reg reg b ⇒
            match register_address reg return λx.is_in … [[ acc_a;
                                                              direct;
                                                              registr ]] x → ? with
            [ REGISTER r ⇒ λregister7: True.
              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉))))))
            | ACC_A ⇒ λacc: True.
               if eq_bv … (bv_zero …) b then
                  Instruction (CLR ? ACC_A)
               else
                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
            | DIRECT d ⇒ λdirect7: True.
              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉)))))
            | _ ⇒ Ⓧ
            ] (subaddressing_modein …)
          | int_to_acc _ b ⇒
            if eq_bv … (bv_zero …) b then
              Instruction (CLR ? ACC_A)
            else
              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
          ]
        ]
      | CALL f _ _ ⇒
        match f with
        [ inl id ⇒
          ! id' ← Identifier_of_ident … id ;
          return Call (toASM_ident ? id')
        | inr _ ⇒
          return Instruction (JMP … ACC_DPTR)
        ]
      | COST_LABEL lbl ⇒
         !_ report_cost … lbl ;
         return Cost lbl
      | COND _ lbl ⇒
        ! l ← Identifier_of_label … lbl;
        return Instruction (JNZ ? l)
      ]
    | FCOND _ _ lbl_true lbl_false ⇒
      ! l1 ← Identifier_of_label … lbl_true;
      ! l2 ← Identifier_of_label … lbl_false;
      return Jnz ACC_A l1 l2
    ].
  try @I
qed.


definition build_translated_statement ≝
  λglobals.
  λstatement: lin_statement globals.
  ! stmt ← translate_statements globals (\snd statement) ;
  match \fst statement with
  [ Some lbl ⇒
    ! lbl' ← Identifier_of_label … lbl ;
    return 〈Some ? lbl', stmt〉
  | None ⇒
    return 〈None ?, stmt〉
  ].

definition translate_code ≝
  λglobals.
  λcode: list (lin_statement globals).
    m_list_map … (build_translated_statement globals) code.

definition translate_fun_def ≝
  λglobals,functions.
  λid_def : ident × (joint_function LIN globals functions).
  !_ start_funct_translation … id_def ;
  (* ^ modify current function id ^ *)
  match \snd id_def with
    [ Internal int ⇒
      let code ≝ joint_if_code … int in
      ! id ← Identifier_of_ident … (\fst id_def) ;
      ! code' ← translate_code … code ;
      match code' with
      [ nil ⇒ return [〈Some ? id, Instruction (RET ?)〉] (* impossible, but whatever *)
      | cons hd tl ⇒
        match \fst hd with
        [ None ⇒ return (〈Some ? id, \snd hd〉 :: tl)
        | _ ⇒ return (〈Some ? id, Instruction (NOP ?)〉 :: hd :: tl) (* should never happen *)
        ]
      ]
    | External _ ⇒ return [ ]
    ].

record init_mutable : Type[0] ≝
{ virtual_dptr : Identifier × Z
; actual_dptr : Identifier × Z
; built_code : list (list labelled_instruction)
; built_preamble : list (Identifier × Word)
}.

definition store_byte_or_Identifier :
  (Byte ⊎ (word_side × Identifier)) → init_mutable → init_mutable ≝
λby,mut.
match mut with
[ mk_init_mutable virt act acc1 acc2 ⇒
  let pre ≝
    if eq_identifier … (\fst virt) (\fst act) then
      let off ≝ \snd virt - \snd act in
      if eqZb off OZ then [ ]
      else if eqZb off 1 then [ 〈None ?, Instruction (INC ? DPTR)〉 ]
      else [ 〈None ?, Mov (inl … DPTR) (\fst virt) (bitvector_of_Z … (\snd virt))〉 ]
    else [ 〈None ?, Mov (inl … DPTR) (\fst virt) (bitvector_of_Z … (\snd virt))〉 ] in
  let post ≝ match by with
    [ inl by ⇒
      〈None ?, Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ?
                               〈ACC_A, DATA by〉))))))〉
    | inr si_id ⇒
      〈None ?, Mov (inr ?? 〈ACC_A, \fst si_id〉) (\snd si_id) (bv_zero ?)〉
    ] in
  mk_init_mutable 〈\fst virt, Zsucc (\snd virt)〉 virt
    ((pre @
      [ post ;
       〈None ?, Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))〉 ]) ::
     acc1)
    acc2  
]. @I qed.


definition do_store_init_data :
  state_monad ASM_universe init_mutable → init_data →
  state_monad ASM_universe init_mutable ≝
λm_mut,data.
! mut ← m_mut ;
let store_byte ≝ λby.store_byte_or_Identifier (inl … by) in
let store_Identifier ≝ λside,id.store_byte_or_Identifier (inr … 〈side, id〉) in
match data with
[ Init_int8 n ⇒
  return store_byte n mut
| Init_int16 n ⇒ 
  let 〈by0, by1〉 ≝ vsplit ? 8 8 n in
  return store_byte by1 (store_byte by0 mut)
| Init_int32 n ⇒ 
  let 〈by0, n〉 ≝ vsplit ? 8 24 n in
  let 〈by1, n〉 ≝ vsplit ? 8 16 n in
  let 〈by2, by3〉 ≝ vsplit ? 8 8 n in
  return store_byte by3 (store_byte by2 (store_byte by1 (store_byte by0 mut)))
| Init_addrof symb ofs ⇒
  ! id ← Identifier_of_ident … symb ;
  return store_Identifier HIGH id (store_Identifier LOW id mut)
| Init_space n ⇒
  let 〈virt_id, virt_off〉 ≝ virtual_dptr mut in
  return mk_init_mutable 〈virt_id, n + virt_off〉 (actual_dptr mut)
    (built_code mut) (built_preamble mut)
| Init_null ⇒
  let z ≝ bv_zero ? in
  return store_byte z (store_byte z mut)
].

definition do_store_global :
    state_monad ASM_universe init_mutable →
  (ident × region × (list init_data)) →
    state_monad ASM_universe init_mutable ≝
  λm_mut,id_reg_data.! mut ← m_mut ;
  let 〈id, reg, data〉 ≝ id_reg_data in
  ! Id ← Identifier_of_ident … id ;
  let mut ≝ mk_init_mutable 〈Id, OZ〉 (actual_dptr … mut) (built_code mut)
    (〈Id, bitvector_of_nat … (size_init_data_list … data)〉 :: built_preamble mut) in
  foldl … do_store_init_data (return mut) data.

let rec reversed_flatten_aux A acc (l : list (list A)) on l : list A ≝
match l with
[ nil ⇒ acc
| cons hd tl ⇒ reversed_flatten_aux … (hd @ acc) tl
].

definition translate_premain : ∀p : lin_program.Identifier →
  state_monad ASM_universe (list labelled_instruction × (list (Identifier × Word))) ≝
  λp : lin_program.λexit_label.
  ! main ← Identifier_of_ident … (prog_main … p) ;
  ! u ← state_get … ;
  (* setting this as actual_dptr will force loading of the correct dptr *)
  let dummy_dptr : Identifier × Z ≝ 〈an_identifier … one, -1〉 in
  let mut ≝ mk_init_mutable dummy_dptr dummy_dptr [ ] [ ] in
  ! globals_init ← foldl … do_store_global (return mut) (prog_vars … p) ;
  let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … (-(S (globals_stacksize … p)))) in
  let init_isp ≝
    (* initial stack pointer set to 2Fh in order to use addressable bits *)
    DATA (zero 2 @@ [[true;false]] @@ maximum 4) in
  let isp_direct ≝
    (* 81h = 10000001b *)
    DIRECT (true ::: bv_zero 6 @@ [[ true ]]) in
  let reg_spl ≝ REGISTER [[ true ; true ; false ]] (* RegisterSPL = Register06 *) in
  let reg_sph ≝ REGISTER [[ true ; true ; true ]] (* RegisterSPH = Register07 *) in
  return 〈[
    〈None ?, Cost (init_cost_label … p)〉 ;
    (* initialize the internal stack pointer past the addressable bits *)
    〈None ?, Instruction
    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
      〈isp_direct, init_isp〉)))))〉 ;
    (* initialize our stack pointer past the globals *)
    〈None ?, Instruction
    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
      〈reg_spl, DATA spl〉))))))〉 ;
    〈None ?, Instruction
    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
      〈reg_sph, DATA sph〉))))))〉 ] @
  reversed_flatten_aux … [ ] (built_code globals_init) @
  [ 〈None ?, Call main〉 ;
    〈Some ? exit_label, Cost (an_identifier … (fresh_cost_label … u))〉 ;
    〈None ?, Jmp exit_label〉], built_preamble globals_init〉. @I qed.

definition get_symboltable :
  state_monad ASM_universe (list (Identifier × ident)) ≝
  λu.
  let imap ≝ ident_map … u in
  let f ≝ λiold,inew.cons ? 〈inew, iold〉 in
  〈u, foldi ??? f imap [ ]〉.

definition lin_to_asm : lin_program → option pseudo_assembly_program ≝
  λp.
  state_run ?? (new_ASM_universe p)
    (let add_translation ≝
      λacc,id_def.
      ! code ← translate_fun_def … id_def ;
      ! acc ← acc ;
      return (code @ acc) in
     ! exit_label ← ASM_fresh … ;
     ! code ← foldl … add_translation (return [ ]) (prog_funct … p) ;
     ! symboltable ← get_symboltable … ;
     ! 〈init, preamble〉 ← translate_premain p exit_label;
     return
       (
        let code ≝
        init @ code in
        ! code_ok ← code_size_opt code ;  
        (* atm no data identifier is used in the code, so preamble must be empty *)
        return
          (mk_pseudo_assembly_program preamble code code_ok symboltable exit_label ? ?))).
cases daemon
qed.