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

Last change on this file since 367 was 367, checked in by mulligan, 9 years ago

Added decidable equality for addressing_mode_tags.

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