source: Deliverables/D4.1/Matita/ASM.ma @ 290

include "Either.ma".
include "BitVectorTrie.ma".
include "String.ma".

ninductive addressing_mode: Type[0] ≝
  DIRECT: Byte → addressing_mode
| INDIRECT: Bit → addressing_mode
| EXT_INDIRECT: Bit → addressing_mode
| REGISTER: Bit → Bit → Bit → 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.

ninductive addressing_mode_tag : Type[0] ≝
  direct: addressing_mode_tag
| indirect: addressing_mode_tag
| ext_indirect: addressing_mode_tag
| register: 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.

(* to avoid expansion... *)
nlet 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 ]
   | register ⇒ 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 ]].

nlet rec is_in n (l: Vector addressing_mode_tag (S n)) (A:addressing_mode) on l : Bool ≝
 match l return λm.λ_:Vector addressing_mode_tag m .∀K:m=S n.Bool with
  [ Empty ⇒ λK.⊥
  | Cons m he (tl: Vector addressing_mode_tag m) ⇒ λ_.
     match m return λz.m = z → Bool with
      [ Z ⇒ λ_.is_a he A
      | S p ⇒ λK.is_a he A ∨ is_in p (? tl) A] (?: m=m)] (?: S n = S n).
(* CSC: cast not working here: why? *)
##[##4: #x; ncases K; napply x ]
//; ndestruct.
nqed.

ndefinition bool_to_Prop ≝
 λb. match b with [ true ⇒ True | false ⇒ False ].

nrecord 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)
 }.

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

ncoercion 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 ? ?.

ninductive jump (A: Type[0]): Type[0] ≝
  JC: A → jump A
| JNC: A → jump A
| JB: Bit → A → jump A
| JNB: Bit → A → jump A
| JBC: Bit → A → jump A
| JZ: A → jump A
| JNZ: A → jump A
| CJNE:
   [[acc_a]] × [[direct; data]] ⊎
   [[register; indirect]] × [[data]] → A → jump A
| DJNZ: [[register ; direct]] → A → jump A.

ninductive preinstruction (A: Type[0]) : Type[0] ≝
   ADD: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
 | ADDC: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
 | SUBB: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
 | INC: [[ acc_a ; register ; direct ; indirect ; dptr ]] → preinstruction A
 | DEC: [[ acc_a ; register ; direct ; indirect ]] → preinstruction A
 | MUL: [[acc_a]] → [[acc_b]] → preinstruction A
 | DIV: [[acc_a]] → [[acc_b]] → preinstruction A
 | DA: [[acc_a]] → preinstruction A

 (* logical operations *)
 | ANL:
   [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
   [[direct]] × [[ acc_a ; data ]] ⊎
   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
 | ORL:
   [[acc_a]] × [[ register ; data ; direct ; indirect ]] ⊎
   [[direct]] × [[ acc_a ; data ]] ⊎
   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
 | XRL:
   [[acc_a]] × [[ data ; register ; 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]] × [[ register ; direct ; indirect ; data ]] ⊎
    [[ register ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
    [[direct]] × [[ acc_a ; register ; direct ; indirect ; data ]] ⊎
    [[dptr]] × [[data16]] ⊎
    [[carry]] × [[bit_addr]] ⊎
    [[bit_addr]] × [[carry]] → preinstruction A
 | MOVC: [[acc_a]] × [[ acc_dptr ; acc_pc ]] → 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]] → [[ register ; direct ; indirect ]] → preinstruction A
 | XCHD: [[acc_a]] → [[indirect]] → preinstruction A

 (* program branching *)
 | Jump: jump A → preinstruction A
 | ACALL: [[addr11]] → preinstruction A
 | LCALL: [[addr16]] → preinstruction A
 | RET: preinstruction A
 | RETI: preinstruction A
 | AJMP: [[addr11]] → preinstruction A
 | LJMP: [[addr16]] → preinstruction A
 | SJMP: [[relative]] → preinstruction A
 | JMP: [[indirect_dptr]] → preinstruction A
 | NOP: preinstruction A.

ndefinition instruction ≝ preinstruction [[relative]].

ninductive labelled_instruction: Type[0] ≝
   Instruction: instruction → labelled_instruction
 | Cost: String → labelled_instruction
 | Jmp: String → labelled_instruction
 | Call: String → labelled_instruction
 | Mov: [[dptr]] → String → labelled_instruction
 | WithLabel: preinstruction String → labelled_instruction.

ndefinition preamble ≝ List (String × Nat).

ndefinition assembly_program ≝ preamble × (List labelled_instruction).