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

Last change on this file since 363 was 357, checked in by sacerdot, 10 years ago
  • stupid bug fixed in BitVectorTrie?
  • dependencies minimized, dead code removed
File size: 7.3 KB
RevLine 
[249]1include "Either.ma".
[357]2include "BitVector.ma".
[264]3include "String.ma".
[248]4
[256]5ninductive addressing_mode: Type[0] ≝
6  DIRECT: Byte → addressing_mode
7| INDIRECT: Bit → addressing_mode
[262]8| EXT_INDIRECT: Bit → addressing_mode
[316]9| REGISTER: BitVector (S (S (S Z))) → addressing_mode
[262]10| ACC_A: addressing_mode
11| ACC_B: addressing_mode
12| DPTR: addressing_mode
[256]13| DATA: Byte → addressing_mode
14| DATA16: Word → addressing_mode
[262]15| ACC_DPTR: addressing_mode
16| ACC_PC: addressing_mode
17| EXT_INDIRECT_DPTR: addressing_mode
18| INDIRECT_DPTR: addressing_mode
[256]19| CARRY: addressing_mode
[283]20| BIT_ADDR: Byte → addressing_mode
21| N_BIT_ADDR: Byte → addressing_mode
[256]22| RELATIVE: Byte → addressing_mode
[262]23| ADDR11: Word11 → addressing_mode
24| ADDR16: Word → addressing_mode.
[256]25
[262]26ninductive addressing_mode_tag : Type[0] ≝
27  direct: addressing_mode_tag
28| indirect: addressing_mode_tag
29| ext_indirect: addressing_mode_tag
30| register: addressing_mode_tag
31| acc_a: addressing_mode_tag
32| acc_b: addressing_mode_tag
33| dptr: addressing_mode_tag
34| data: addressing_mode_tag
35| data16: addressing_mode_tag
36| acc_dptr: addressing_mode_tag
37| acc_pc: addressing_mode_tag
38| ext_indirect_dptr: addressing_mode_tag
39| indirect_dptr: addressing_mode_tag
40| carry: addressing_mode_tag
41| bit_addr: addressing_mode_tag
42| n_bit_addr: addressing_mode_tag
43| relative: addressing_mode_tag
44| addr11: addressing_mode_tag
45| addr16: addressing_mode_tag.
46
[256]47(* to avoid expansion... *)
[262]48nlet rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
[256]49  match d with
[262]50   [ direct ⇒ match A with [ DIRECT _ ⇒ true | _ ⇒ false ]
51   | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]
52   | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ]
[316]53   | register ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]
[262]54   | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ]
55   | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ]
56   | dptr ⇒ match A with [ DPTR ⇒ true | _ ⇒ false ]
[260]57   | data ⇒ match A with [ DATA _ ⇒ true | _ ⇒ false ]
[262]58   | data16 ⇒ match A with [ DATA16 _ ⇒ true | _ ⇒ false ]
59   | acc_dptr ⇒ match A with [ ACC_DPTR ⇒ true | _ ⇒ false ]
60   | acc_pc ⇒ match A with [ ACC_PC ⇒ true | _ ⇒ false ]
61   | ext_indirect_dptr ⇒ match A with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
62   | indirect_dptr ⇒ match A with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
63   | carry ⇒ match A with [ CARRY ⇒ true | _ ⇒ false ]
64   | bit_addr ⇒ match A with [ BIT_ADDR _ ⇒ true | _ ⇒ false ]
65   | n_bit_addr ⇒ match A with [ N_BIT_ADDR _ ⇒ true | _ ⇒ false ]
66   | relative ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ]
67   | addr11 ⇒ match A with [ ADDR11 _ ⇒ true | _ ⇒ false ]
68   | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ]].
[256]69
[262]70nlet rec is_in n (l: Vector addressing_mode_tag (S n)) (A:addressing_mode) on l : Bool ≝
71 match l return λm.λ_:Vector addressing_mode_tag m .∀K:m=S n.Bool with
[256]72  [ Empty ⇒ λK.⊥
[262]73  | Cons m he (tl: Vector addressing_mode_tag m) ⇒ λ_.
[256]74     match m return λz.m = z → Bool with
75      [ Z ⇒ λ_.is_a he A
76      | S p ⇒ λK.is_a he A ∨ is_in p (? tl) A] (?: m=m)] (?: S n = S n).
[262]77(* CSC: cast not working here: why? *)
[256]78##[##4: #x; ncases K; napply x ]
79//; ndestruct.
80nqed.
81
[262]82ndefinition bool_to_Prop ≝
83 λb. match b with [ true ⇒ True | false ⇒ False ].
84
85nrecord subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
[256]86 { subaddressing_modeel:> addressing_mode;
[262]87   subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
[256]88 }.
89
[262]90ncoercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0]
91 ≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0].
[256]92
93ncoercion mk_subaddressing_mode :
[262]94 ∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode.
95  ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l
96 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
[256]97
[262]98ninductive jump (A: Type[0]): Type[0] ≝
99  JC: A → jump A
100| JNC: A → jump A
[293]101| JB: [[bit_addr]] → A → jump A
102| JNB: [[bit_addr]] → A → jump A
103| JBC: [[bit_addr]] → A → jump A
[262]104| JZ: A → jump A
105| JNZ: A → jump A
106| CJNE:
[293]107   [[acc_a]] × [[direct; data]] ⊎ [[register; indirect]] × [[data]] → A → jump A
[262]108| DJNZ: [[register ; direct]] → A → jump A.
[249]109
[262]110ninductive preinstruction (A: Type[0]) : Type[0] ≝
[278]111   ADD: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
112 | ADDC: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
113 | SUBB: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
114 | INC: [[ acc_a ; register ; direct ; indirect ; dptr ]] → preinstruction A
115 | DEC: [[ acc_a ; register ; direct ; indirect ]] → preinstruction A
116 | MUL: [[acc_a]] → [[acc_b]] → preinstruction A
117 | DIV: [[acc_a]] → [[acc_b]] → preinstruction A
118 | DA: [[acc_a]] → preinstruction A
[262]119
120 (* logical operations *)
121 | ANL:
122   [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
123   [[direct]] × [[ acc_a ; data ]] ⊎
[278]124   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
[262]125 | ORL:
126   [[acc_a]] × [[ register ; data ; direct ; indirect ]] ⊎
127   [[direct]] × [[ acc_a ; data ]] ⊎
[278]128   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
[262]129 | XRL:
130   [[acc_a]] × [[ data ; register ; direct ; indirect ]] ⊎
[278]131   [[direct]] × [[ acc_a ; data ]] → preinstruction A
132 | CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
133 | CPL: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
134 | RL: [[acc_a]] → preinstruction A
135 | RLC: [[acc_a]] → preinstruction A
136 | RR: [[acc_a]] → preinstruction A
137 | RRC: [[acc_a]] → preinstruction A
138 | SWAP: [[acc_a]] → preinstruction A
[262]139
140 (* data transfer *)
141 | MOV:
142    [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
143    [[ register ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
144    [[direct]] × [[ acc_a ; register ; direct ; indirect ; data ]] ⊎
145    [[dptr]] × [[data16]] ⊎
146    [[carry]] × [[bit_addr]] ⊎
[278]147    [[bit_addr]] × [[carry]] → preinstruction A
[297]148 | MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → preinstruction A
[262]149 | MOVX:
150    [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
[278]151    [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] → preinstruction A
152 | SETB: [[ carry ; bit_addr ]] → preinstruction A
153 | PUSH: [[direct]] → preinstruction A
154 | POP: [[direct]] → preinstruction A
155 | XCH: [[acc_a]] → [[ register ; direct ; indirect ]] → preinstruction A
156 | XCHD: [[acc_a]] → [[indirect]] → preinstruction A
[262]157
158 (* program branching *)
159 | Jump: jump A → preinstruction A
[278]160 | ACALL: [[addr11]] → preinstruction A
161 | LCALL: [[addr16]] → preinstruction A
[262]162 | RET: preinstruction A
163 | RETI: preinstruction A
[278]164 | AJMP: [[addr11]] → preinstruction A
165 | LJMP: [[addr16]] → preinstruction A
166 | SJMP: [[relative]] → preinstruction A
167 | JMP: [[indirect_dptr]] → preinstruction A
[262]168 | NOP: preinstruction A.
169
[264]170ndefinition instruction ≝ preinstruction [[relative]].
[262]171
[264]172ninductive labelled_instruction: Type[0] ≝
173   Instruction: instruction → labelled_instruction
174 | Cost: String → labelled_instruction
175 | Jmp: String → labelled_instruction
176 | Call: String → labelled_instruction
[278]177 | Mov: [[dptr]] → String → labelled_instruction
[264]178 | WithLabel: preinstruction String → labelled_instruction.
[256]179
[264]180ndefinition preamble ≝ List (String × Nat).
[256]181
[283]182ndefinition assembly_program ≝ preamble × (List labelled_instruction).
Note: See TracBrowser for help on using the repository browser.