source: src/ASM/new-matita-development/ASM.ma @ 688

Last change on this file since 688 was 475, checked in by mulligan, 10 years ago

Matita interpreter ported to latest version of matita (the one with the tabs). To use, this directory must be copied into the /lib directory in the matita directory.

File size: 8.4 KB
Line 
1include "cerco/BitVector.ma".
2include "cerco/String.ma".
3
4inductive addressing_mode: Type[0] ≝
5  DIRECT: Byte → addressing_mode
6| INDIRECT: Bit → addressing_mode
7| EXT_INDIRECT: Bit → addressing_mode
8| REGISTER: BitVector (S (S (S O))) → addressing_mode
9| ACC_A: addressing_mode
10| ACC_B: addressing_mode
11| DPTR: addressing_mode
12| DATA: Byte → addressing_mode
13| DATA16: Word → addressing_mode
14| ACC_DPTR: addressing_mode
15| ACC_PC: addressing_mode
16| EXT_INDIRECT_DPTR: addressing_mode
17| INDIRECT_DPTR: addressing_mode
18| CARRY: addressing_mode
19| BIT_ADDR: Byte → addressing_mode
20| N_BIT_ADDR: Byte → addressing_mode
21| RELATIVE: Byte → addressing_mode
22| ADDR11: Word11 → addressing_mode
23| ADDR16: Word → addressing_mode.
24
25inductive addressing_mode_tag : Type[0] ≝
26  direct: addressing_mode_tag
27| indirect: addressing_mode_tag
28| ext_indirect: addressing_mode_tag
29| register: 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      | register ⇒ match b with [ register ⇒ 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   | register ⇒ 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
100definition bool_to_Prop ≝
101 λb. match b with [ true ⇒ True | false ⇒ False ].
102
103record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
104{
105  subaddressing_modeel:> addressing_mode;
106  subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
107}.
108
109coercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0]
110 ≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0].
111
112coercion mk_subaddressing_mode :
113 ∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode.
114  ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l
115 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
116
117inductive jump (A: Type[0]): Type[0] ≝
118  JC: A → jump A
119| JNC: A → jump A
120| JB: [[bit_addr]] → A → jump A
121| JNB: [[bit_addr]] → A → jump A
122| JBC: [[bit_addr]] → A → jump A
123| JZ: A → jump A
124| JNZ: A → jump A
125| CJNE:
126   [[acc_a]] × [[direct; data]] ⊎ [[register; indirect]] × [[data]] → A → jump A
127| DJNZ: [[register ; direct]] → A → jump A.
128
129inductive preinstruction (A: Type[0]) : Type[0] ≝
130  ADD: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
131| ADDC: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
132| SUBB: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
133| INC: [[ acc_a ; register ; direct ; indirect ; dptr ]] → preinstruction A
134| DEC: [[ acc_a ; register ; direct ; indirect ]] → preinstruction A
135| MUL: [[acc_a]] → [[acc_b]] → preinstruction A
136| DIV: [[acc_a]] → [[acc_b]] → preinstruction A
137| DA: [[acc_a]] → preinstruction A
138
139 (* logical operations *)
140| ANL:
141   [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
142   [[direct]] × [[ acc_a ; data ]] ⊎
143   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
144| ORL:
145   [[acc_a]] × [[ register ; data ; direct ; indirect ]] ⊎
146   [[direct]] × [[ acc_a ; data ]] ⊎
147   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
148| XRL:
149   [[acc_a]] × [[ data ; register ; direct ; indirect ]] ⊎
150   [[direct]] × [[ acc_a ; data ]] → preinstruction A
151| CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
152| CPL: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
153| RL: [[acc_a]] → preinstruction A
154| RLC: [[acc_a]] → preinstruction A
155| RR: [[acc_a]] → preinstruction A
156| RRC: [[acc_a]] → preinstruction A
157| SWAP: [[acc_a]] → preinstruction A
158
159 (* data transfer *)
160| MOV:
161    [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
162    [[ register ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
163    [[direct]] × [[ acc_a ; register ; direct ; indirect ; data ]] ⊎
164    [[dptr]] × [[data16]] ⊎
165    [[carry]] × [[bit_addr]] ⊎
166    [[bit_addr]] × [[carry]] → preinstruction A
167| MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → preinstruction A
168| MOVX:
169    [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
170    [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] → preinstruction A
171| SETB: [[ carry ; bit_addr ]] → preinstruction A
172| PUSH: [[direct]] → preinstruction A
173| POP: [[direct]] → preinstruction A
174| XCH: [[acc_a]] → [[ register ; direct ; indirect ]] → preinstruction A
175| XCHD: [[acc_a]] → [[indirect]] → preinstruction A
176
177 (* program branching *)
178| Jump: jump A → preinstruction A
179| ACALL: [[addr11]] → preinstruction A
180| LCALL: [[addr16]] → preinstruction A
181| RET: preinstruction A
182| RETI: preinstruction A
183| AJMP: [[addr11]] → preinstruction A
184| LJMP: [[addr16]] → preinstruction A
185| SJMP: [[relative]] → preinstruction A
186| JMP: [[indirect_dptr]] → preinstruction A
187| NOP: preinstruction A.
188
189definition instruction ≝ preinstruction [[relative]].
190
191inductive labelled_instruction: Type[0] ≝
192  Instruction: instruction → labelled_instruction
193| Cost: String → labelled_instruction
194| Jmp: String → labelled_instruction
195| Call: String → labelled_instruction
196| Mov: [[dptr]] → String → labelled_instruction
197| Label: String → labelled_instruction
198| WithLabel: jump String → labelled_instruction.
199
200definition preamble ≝ list (String × nat).
201
202definition assembly_program ≝ preamble × (list labelled_instruction).
Note: See TracBrowser for help on using the repository browser.