--- /dev/null
+include "ASM/BitVector.ma".
+
+definition Identifier ≝ Word.
+
+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: Identifier → pseudo_instruction
+ | Jmp: Identifier → pseudo_instruction
+ | Call: Identifier → pseudo_instruction
+ | Mov: [[dptr]] → Identifier → pseudo_instruction.
+
+definition labelled_instruction ≝ option Identifier × pseudo_instruction.
+definition preamble ≝ list (Identifier × nat).
+definition assembly_program ≝ list instruction.
+definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).
projects / helm.git / blobdiff