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 (globals : list ident) : Type[0] :=
{ id_univ : universe ASMTag
; current_funct : ident
; ident_map : identifier_map SymbolTag Identifier
; label_map : identifier_map SymbolTag (identifier_map LabelTag Identifier)
; address_map : identifier_map SymbolTag Word
; globals_are_in : ∀i : ident.i ∈ globals → i ∈ address_map
}.

definition new_ASM_universe :
∀p : joint_program LIN.ASM_universe (prog_var_names … p) ≝
λp.
  let globals_addr_internal ≝
   λres_offset : identifier_map SymbolTag Word × Z.
   λx_size: ident × region × nat.
    let 〈res, offset〉 ≝ res_offset in
    let 〈x, region, size〉 ≝ x_size in
      〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat size〉 in
  let addresses ≝ foldl … globals_addr_internal 〈empty_map …, OZ〉 (prog_vars … p) in
mk_ASM_universe ? (mk_universe … one)
  (an_identifier … one (* dummy *))
  (empty_map …) (empty_map …)
  (\fst addresses) ?.
@hide_prf
normalize nodelta
cases p -p #vars #functs #main
#i #H
letin init_val ≝ (〈empty_map ? Word, OZ〉)
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 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) @mem_set_add_id
| %2{H}
| %1 cases init_val in H; normalize nodelta #init_map #off #H
  >mem_set_add @orb_Prop_r @H
]
qed.

definition Identifier_of_label :
  ∀globals.label → state_monad (ASM_universe globals) Identifier ≝
λg,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)
  (address_map … u) (globals_are_in … u), id〉.

definition Identifier_of_ident :
  ∀globals.ident → state_monad (ASM_universe globals) Identifier ≝
λg,i,u.
let imap ≝ ident_map … u in
let 〈id, univ, imap〉 ≝
  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
〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u)
  (address_map … u) (globals_are_in … u), id〉.

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

definition address_of_ident :
  ∀globals,i.i ∈ globals → state_monad (ASM_universe globals) [[ data16 ]] ≝
λglobals,i,prf,u.
〈u, DATA16 (lookup_safe … (globals_are_in … u … prf))〉. @I qed.

definition ASM_fresh :
  ∀globals.state_monad (ASM_universe globals) Identifier ≝
λg,u.let 〈id, univ〉 ≝ fresh … (id_univ … u) in
〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u)
  (address_map … u) (globals_are_in … 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 82)
    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
    | _ ⇒ 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 translate_statements :
  ∀globals.
  joint_statement LIN globals →
  state_monad (ASM_universe globals) 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 reg lbl ⇒
            ! lbl' ← Identifier_of_label … lbl ;
            return MovSuccessor (register_address reg) LOW lbl'
          | HIGH_ADDRESS reg lbl ⇒
            ! lbl' ← Identifier_of_label … lbl ;
            return MovSuccessor (register_address reg) HIGH lbl'
          ]
        | 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 addr proof _ _ ⇒
          ! addr' ← address_of_ident … proof ;
          return Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, addr'〉)))))
        | 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 … INDIRECT_DPTR)
        ]
      | COST_LABEL 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 globals 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.
  λid_def : ident × (joint_function LIN globals).
  !_ 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 [ ]
    ].

definition get_symboltable :
  ∀globals.state_monad (ASM_universe globals) (list (Identifier × ident)) ≝
  λglobals,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
     ! code ← foldl … add_translation (return [ ]) (prog_funct … p) ;
     ! exit_label ← ASM_fresh … ;
     ! main ← Identifier_of_ident … (prog_main … p) ;
     ! symboltable ← get_symboltable … ;
     return
      (let code ≝ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: 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 [ ] code code_ok symboltable exit_label ? ?))).
cases daemon
qed.