source: src/ASM/ASM.ma @ 780

Last change on this file since 780 was 757, checked in by mulligan, 10 years ago

Lots more fixing to get both front and backends using same conventions and types.

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