include "ASM/BitVector.ma".
include "common/Identifiers.ma".
include "common/CostLabel.ma".
include "common/LabelledObjects.ma".

axiom ASMTag : String.
definition Identifier ≝ identifier ASMTag.
definition toASM_ident : ∀tag. identifier tag → Identifier ≝ λt,i. match i with [ an_identifier id ⇒ an_identifier ASMTag id ].

inductive addressing_mode: Type[0] ≝
  DIRECT: Byte → addressing_mode
| INDIRECT: Bit → addressing_mode
| EXT_INDIRECT: Bit → addressing_mode
| REGISTER: BitVector 3 → addressing_mode
| ACC_A: addressing_mode
| ACC_B: addressing_mode
| DPTR: addressing_mode
| DATA: Byte → addressing_mode
| DATA16: Word → addressing_mode
| ACC_DPTR: addressing_mode
| ACC_PC: addressing_mode
| EXT_INDIRECT_DPTR: addressing_mode
| INDIRECT_DPTR: addressing_mode
| CARRY: addressing_mode
| BIT_ADDR: Byte → addressing_mode
| N_BIT_ADDR: Byte → addressing_mode
| RELATIVE: Byte → addressing_mode
| ADDR11: Word11 → addressing_mode
| ADDR16: Word → addressing_mode.

(* dpm: renamed register to registr to avoid clash with brian's types *)
inductive addressing_mode_tag : Type[0] ≝
  direct: addressing_mode_tag
| indirect: addressing_mode_tag
| ext_indirect: addressing_mode_tag
| registr: addressing_mode_tag
| acc_a: addressing_mode_tag
| acc_b: addressing_mode_tag
| dptr: addressing_mode_tag
| data: addressing_mode_tag
| data16: addressing_mode_tag
| acc_dptr: addressing_mode_tag
| acc_pc: addressing_mode_tag
| ext_indirect_dptr: addressing_mode_tag
| indirect_dptr: addressing_mode_tag
| carry: addressing_mode_tag
| bit_addr: addressing_mode_tag
| n_bit_addr: addressing_mode_tag
| relative: addressing_mode_tag
| addr11: addressing_mode_tag
| addr16: addressing_mode_tag.

definition eq_a ≝
  λa, b: addressing_mode_tag.
    match a with
      [ direct ⇒ match b with [ direct ⇒ true | _ ⇒ false ]
      | indirect ⇒ match b with [ indirect ⇒ true | _ ⇒ false ]
      | ext_indirect ⇒ match b with [ ext_indirect ⇒ true | _ ⇒ false ]
      | registr ⇒ match b with [ registr ⇒ true | _ ⇒ false ]
      | acc_a ⇒ match b with [ acc_a ⇒ true | _ ⇒ false ]
      | acc_b ⇒ match b with [ acc_b ⇒ true | _ ⇒ false ]
      | dptr ⇒ match b with [ dptr ⇒ true | _ ⇒ false ]
      | data ⇒ match b with [ data ⇒ true | _ ⇒ false ]
      | data16 ⇒ match b with [ data16 ⇒ true | _ ⇒ false ]
      | acc_dptr ⇒ match b with [ acc_dptr ⇒ true | _ ⇒ false ]
      | acc_pc ⇒ match b with [ acc_pc ⇒ true | _ ⇒ false ]
      | ext_indirect_dptr ⇒ match b with [ ext_indirect_dptr ⇒ true | _ ⇒ false ]
      | indirect_dptr ⇒ match b with [ indirect_dptr ⇒ true | _ ⇒ false ]
      | carry ⇒ match b with [ carry ⇒ true | _ ⇒ false ]
      | bit_addr ⇒ match b with [ bit_addr ⇒ true | _ ⇒ false ]
      | n_bit_addr ⇒ match b with [ n_bit_addr ⇒ true | _ ⇒ false ]
      | relative ⇒ match b with [ relative ⇒ true | _ ⇒ false ]
      | addr11 ⇒ match b with [ addr11 ⇒ true | _ ⇒ false ]
      | addr16 ⇒ match b with [ addr16 ⇒ true | _ ⇒ false ]
      ].

(* to avoid expansion... *)
let rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
  match d with
   [ direct ⇒ match A with [ DIRECT _ ⇒ true | _ ⇒ false ]
   | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]
   | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ]
   | registr ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]
   | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ]
   | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ]
   | dptr ⇒ match A with [ DPTR ⇒ true | _ ⇒ false ]
   | data ⇒ match A with [ DATA _ ⇒ true | _ ⇒ false ]
   | data16 ⇒ match A with [ DATA16 _ ⇒ true | _ ⇒ false ]
   | acc_dptr ⇒ match A with [ ACC_DPTR ⇒ true | _ ⇒ false ]
   | acc_pc ⇒ match A with [ ACC_PC ⇒ true | _ ⇒ false ]
   | ext_indirect_dptr ⇒ match A with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
   | indirect_dptr ⇒ match A with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
   | carry ⇒ match A with [ CARRY ⇒ true | _ ⇒ false ]
   | bit_addr ⇒ match A with [ BIT_ADDR _ ⇒ true | _ ⇒ false ]
   | n_bit_addr ⇒ match A with [ N_BIT_ADDR _ ⇒ true | _ ⇒ false ]
   | relative ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ]
   | addr11 ⇒ match A with [ ADDR11 _ ⇒ true | _ ⇒ false ]
   | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ]
   ].


let rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : bool ≝
 match l return λm.λ_:Vector addressing_mode_tag m.bool with
  [ VEmpty ⇒ false
  | VCons m he (tl: Vector addressing_mode_tag m) ⇒
     is_a he A ∨ is_in ? tl A ].

record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
{
  subaddressing_modeel:> addressing_mode;
  subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
}.

coercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0]
 ≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0].

coercion mk_subaddressing_mode :
 ∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode.
  ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l
 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
 
inductive preinstruction (A: Type[0]) : Type[0] ≝
  ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
| ADDC: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
| SUBB: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
| INC: [[ acc_a ; registr ; direct ; indirect ; dptr ]] → preinstruction A
| DEC: [[ acc_a ; registr ; direct ; indirect ]] → preinstruction A
| MUL: [[acc_a]] → [[acc_b]] → preinstruction A
| DIV: [[acc_a]] → [[acc_b]] → preinstruction A
| DA: [[acc_a]] → preinstruction A

(* conditional jumps *)
| JC: A → preinstruction A
| JNC: A → preinstruction A
| JB: [[bit_addr]] → A → preinstruction A
| JNB: [[bit_addr]] → A → preinstruction A
| JBC: [[bit_addr]] → A → preinstruction A
| JZ: A → preinstruction A
| JNZ: A → preinstruction A
| CJNE:
   [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → preinstruction A
| DJNZ: [[registr ; direct]] → A → preinstruction A
 (* logical operations *)
| ANL:
   [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
   [[direct]] × [[ acc_a ; data ]] ⊎
   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
| ORL:
   [[acc_a]] × [[ registr ; data ; direct ; indirect ]] ⊎
   [[direct]] × [[ acc_a ; data ]] ⊎
   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
| XRL:
   [[acc_a]] × [[ data ; registr ; direct ; indirect ]] ⊎
   [[direct]] × [[ acc_a ; data ]] → preinstruction A
| CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
| CPL: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
| RL: [[acc_a]] → preinstruction A
| RLC: [[acc_a]] → preinstruction A
| RR: [[acc_a]] → preinstruction A
| RRC: [[acc_a]] → preinstruction A
| SWAP: [[acc_a]] → preinstruction A

 (* data transfer *)
| MOV:
    [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
    [[ registr ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
    [[direct]] × [[ acc_a ; registr ; direct ; indirect ; data ]] ⊎
    [[dptr]] × [[data16]] ⊎
    [[carry]] × [[bit_addr]] ⊎
    [[bit_addr]] × [[carry]] → preinstruction A
| MOVX: 
    [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
    [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] → preinstruction A
| SETB: [[ carry ; bit_addr ]] → preinstruction A
| PUSH: [[direct]] → preinstruction A
| POP: [[direct]] → preinstruction A
| XCH: [[acc_a]] → [[ registr ; direct ; indirect ]] → preinstruction A
| XCHD: [[acc_a]] → [[indirect]] → preinstruction A

 (* program branching *)
| RET: preinstruction A
| RETI: preinstruction A
| NOP: preinstruction A.

inductive instruction: Type[0] ≝
  | ACALL: [[addr11]] → instruction
  | LCALL: [[addr16]] → instruction
  | AJMP: [[addr11]] → instruction
  | LJMP: [[addr16]] → instruction
  | SJMP: [[relative]] → instruction
  | JMP: [[indirect_dptr]] → instruction
  | MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → instruction
  | RealInstruction: preinstruction [[ relative ]] → instruction.
  
coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝
  RealInstruction on _p: preinstruction ? to instruction.

inductive pseudo_instruction: Type[0] ≝
  | Instruction: preinstruction Identifier → pseudo_instruction
  | Comment: String → pseudo_instruction
  | Cost: costlabel → pseudo_instruction
  | Jmp: Identifier → pseudo_instruction
  | Call: Identifier → pseudo_instruction
  | Mov: [[dptr]] → Identifier → pseudo_instruction.

definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction.
definition preamble ≝ (identifier_map SymbolTag nat) × (list (Identifier × Word)).
definition assembly_program ≝ list instruction.
definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).