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

Last change on this file since 262 was 262, checked in by sacerdot, 9 years ago
  • new notation ...? for vectors to reduce ambiguity
  • preinstruction type ported to Matita
File size: 10.6 KB
Line 
1include "Universes.ma".
2include "Plogic/equality.ma".
3include "Either.ma".
4include "BitVector.ma".
5include "BitVectorTrie.ma".
6
7interpretation "Cartesian" 'product A B = (Cartesian A B).
8notation "hvbox(a break ⊎ b)"
9 left associative with precedence 50
10for @{ 'disjoint_union $a $b }.
11interpretation "Either" 'disjoint_union A B = (Either A B).
12interpretation "Bool" 'or a b = (inclusive_disjunction a b).
13
14ninductive addressing_mode: Type[0] ≝
15  DIRECT: Byte → addressing_mode
16| INDIRECT: Bit → addressing_mode
17| EXT_INDIRECT: Bit → addressing_mode
18| REGISTER: Bit → Bit → Bit → addressing_mode
19| ACC_A: addressing_mode
20| ACC_B: addressing_mode
21| DPTR: addressing_mode
22| DATA: Byte → addressing_mode
23| DATA16: Word → addressing_mode
24| ACC_DPTR: addressing_mode
25| ACC_PC: addressing_mode
26| EXT_INDIRECT_DPTR: addressing_mode
27| INDIRECT_DPTR: addressing_mode
28| CARRY: addressing_mode
29| BIT_ADDR: Bit → addressing_mode
30| N_BIT_ADDR: Bit → addressing_mode
31| RELATIVE: Byte → addressing_mode
32| ADDR11: Word11 → addressing_mode
33| ADDR16: Word → addressing_mode.
34
35ninductive addressing_mode_tag : Type[0] ≝
36  direct: addressing_mode_tag
37| indirect: addressing_mode_tag
38| ext_indirect: addressing_mode_tag
39| register: addressing_mode_tag
40| acc_a: addressing_mode_tag
41| acc_b: addressing_mode_tag
42| dptr: addressing_mode_tag
43| data: addressing_mode_tag
44| data16: addressing_mode_tag
45| acc_dptr: addressing_mode_tag
46| acc_pc: addressing_mode_tag
47| ext_indirect_dptr: addressing_mode_tag
48| indirect_dptr: addressing_mode_tag
49| carry: addressing_mode_tag
50| bit_addr: addressing_mode_tag
51| n_bit_addr: addressing_mode_tag
52| relative: addressing_mode_tag
53| addr11: addressing_mode_tag
54| addr16: addressing_mode_tag.
55
56(* to avoid expansion... *)
57nlet rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
58  match d with
59   [ direct ⇒ match A with [ DIRECT _ ⇒ true | _ ⇒ false ]
60   | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]
61   | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ]
62   | register ⇒ match A with [ REGISTER _ _ _ ⇒ true | _ ⇒ false ]
63   | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ]
64   | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ]
65   | dptr ⇒ match A with [ DPTR ⇒ true | _ ⇒ false ]
66   | data ⇒ match A with [ DATA _ ⇒ true | _ ⇒ false ]
67   | data16 ⇒ match A with [ DATA16 _ ⇒ true | _ ⇒ false ]
68   | acc_dptr ⇒ match A with [ ACC_DPTR ⇒ true | _ ⇒ false ]
69   | acc_pc ⇒ match A with [ ACC_PC ⇒ true | _ ⇒ false ]
70   | ext_indirect_dptr ⇒ match A with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
71   | indirect_dptr ⇒ match A with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
72   | carry ⇒ match A with [ CARRY ⇒ true | _ ⇒ false ]
73   | bit_addr ⇒ match A with [ BIT_ADDR _ ⇒ true | _ ⇒ false ]
74   | n_bit_addr ⇒ match A with [ N_BIT_ADDR _ ⇒ true | _ ⇒ false ]
75   | relative ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ]
76   | addr11 ⇒ match A with [ ADDR11 _ ⇒ true | _ ⇒ false ]
77   | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ]].
78
79nlet rec is_in n (l: Vector addressing_mode_tag (S n)) (A:addressing_mode) on l : Bool ≝
80 match l return λm.λ_:Vector addressing_mode_tag m .∀K:m=S n.Bool with
81  [ Empty ⇒ λK.⊥
82  | Cons m he (tl: Vector addressing_mode_tag m) ⇒ λ_.
83     match m return λz.m = z → Bool with
84      [ Z ⇒ λ_.is_a he A
85      | S p ⇒ λK.is_a he A ∨ is_in p (? tl) A] (?: m=m)] (?: S n = S n).
86(* CSC: cast not working here: why? *)
87##[##4: #x; ncases K; napply x ]
88//; ndestruct.
89nqed.
90
91ndefinition bool_to_Prop ≝
92 λb. match b with [ true ⇒ True | false ⇒ False ].
93
94nrecord subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
95 { subaddressing_modeel:> addressing_mode;
96   subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
97 }.
98
99ncoercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0]
100 ≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0].
101
102ncoercion mk_subaddressing_mode :
103 ∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode.
104  ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l
105 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
106
107ninductive jump (A: Type[0]): Type[0] ≝
108  JC: A → jump A
109| JNC: A → jump A
110| JB: Bit → A → jump A
111| JNB: Bit → A → jump A
112| JBC: Bit → A → jump A
113| JZ: A → jump A
114| JNZ: A → jump A
115| CJNE:
116   [[acc_a]] × [[direct; data]] ⊎
117   [[register; indirect]] × [[data]] → A → jump A
118| DJNZ: [[register ; direct]] → A → jump A.
119
120ninductive preinstruction (A: Type[0]) : Type[0] ≝
121   ADD: [[acc_a]] × [[ register ; direct ; indirect ; data ]] -> preinstruction A
122 | ADDC: [[acc_a]] × [[ register ; direct ; indirect ; data ]] -> preinstruction A
123 | SUBB: [[acc_a]] × [[ register ; direct ; indirect ; data ]] -> preinstruction A
124 | INC: [[ acc_a ; register ; direct ; indirect ; dptr ]] -> preinstruction A
125 | DEC: [[ acc_a ; register ; direct ; indirect ]] -> preinstruction A
126 | MUL: [[acc_a]] × [[acc_b]] -> preinstruction A
127 | DIV: [[acc_a]] × [[acc_b]] -> preinstruction A
128 | DA: [[acc_a]] -> preinstruction A
129
130 (* logical operations *)
131 | ANL:
132   [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
133   [[direct]] × [[ acc_a ; data ]] ⊎
134   [[carry]] × [[ bit_addr ; n_bit_addr]] -> preinstruction A
135 | ORL:
136   [[acc_a]] × [[ register ; data ; direct ; indirect ]] ⊎
137   [[direct]] × [[ acc_a ; data ]] ⊎
138   [[carry]] × [[ bit_addr ; n_bit_addr]] -> preinstruction A
139 | XRL:
140   [[acc_a]] × [[ data ; register ; direct ; indirect ]] ⊎
141   [[direct]] × [[ acc_a ; data ]] -> preinstruction A
142 | CLR: [[ acc_a ; carry ; bit_addr ]] -> preinstruction A
143 | CPL: [[ acc_a ; carry ; bit_addr ]] -> preinstruction A
144 | RL: [[acc_a]] -> preinstruction A
145 | RLC: [[acc_a]] -> preinstruction A
146 | RR: [[acc_a]] -> preinstruction A
147 | RRC: [[acc_a]] -> preinstruction A
148 | SWAP: [[acc_a]] -> preinstruction A
149
150 (* data transfer *)
151 | MOV:
152    [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
153    [[ register ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
154    [[direct]] × [[ acc_a ; register ; direct ; indirect ; data ]] ⊎
155    [[dptr]] × [[data16]] ⊎
156    [[carry]] × [[bit_addr]] ⊎
157    [[bit_addr]] × [[carry]] -> preinstruction A
158 | MOVC: [[acc_a]] × [[ acc_dptr ; acc_pc ]] -> preinstruction A
159 | MOVX:
160    [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
161    [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] -> preinstruction A
162 | SETB: [[ carry ; bit_addr ]] -> preinstruction A
163 | PUSH: [[direct]] -> preinstruction A
164 | POP: [[direct]] -> preinstruction A
165 | XCH: [[acc_a]] × [[ register ; direct ; indirect ]] -> preinstruction A
166 | XCHD: [[acc_a]] × [[indirect]] -> preinstruction A
167
168 (* program branching *)
169 | Jump: jump A → preinstruction A
170 | ACALL: [[addr11]] -> preinstruction A
171 | LCALL: [[addr16]] -> preinstruction A
172 | RET: preinstruction A
173 | RETI: preinstruction A
174 | AJMP: [[addr11]] -> preinstruction A
175 | LJMP: [[addr16]] -> preinstruction A
176 | SJMP: [[relative]] -> preinstruction A
177 | JMP: [[indirect_dptr]] -> preinstruction A
178 | NOP: preinstruction A.
179
180
181ndefinition xxx: jump Nat.
182 napply (DJNZ ? (REGISTER [true] [true] [true]) Z).
183 napply I;
184nqed.
185
186naxiom bar: addressing_mode → Nat.
187
188ndefinition barj ≝
189 λA.λf:A → Nat.λJ:Jump A.
190  match J with
191   [ DJNZ arg1 arg2 ⇒ f arg2 + bar arg1
192   | _ ⇒ (Z: Nat)].
193   
194ndefinition PreInstruction ≝ λA: Type[0]. Jump A.
195
196ndefinition Instruction ≝ PreInstruction [rel].
197
198nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ {
199   elem:> A;
200   witness: T elem
201}.
202
203interpretation "Sigma" 'sigma T = (Sigma ? T).
204
205naxiom daemon: False.
206
207naxiom decode_register: Vector Bool (S (S (S Z))) → [reg].
208naxiom decode_direct:   Vector Bool (S (S (S Z))) → [direct].
209
210ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction))
211 ≝
212 [mk_Cartesian ??
213   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
214     (λl.
215       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
216             (mk_subaddressing_mode ? ?    (decode_register l) ?));
217  mk_Cartesian ??
218   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
219     (λl.
220       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
221             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
222ncases daemon.
223nqed.
224
225
226naxiom decode_register: List Bool → [reg].
227naxiom decode_direct: List Bool → [direct].
228
229ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction))
230 ≝
231 [mk_Cartesian ??
232   [ false; false; true; false; true]
233     (λl.
234       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
235             (mk_subaddressing_mode ? ?    (decode_register l) ?));
236  mk_Cartesian ??
237   [ false; false; true; false; true]
238     (λl.
239       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
240             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
241ncases daemon.
242nqed.
243
244
245ndefinition decode_tbl1:
246 List (List Bool × Σaddr:all_types. [addr] → Instruction)
247 ≝
248 [mk_Cartesian ??
249   [ false; false; true; false; true]
250   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
251     reg
252     (λa.
253       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
254             (mk_subaddressing_mode ? ? a ?))) ].
255ncases daemon.
256nqed.
257             
258ndefinition decode_tbl2:
259 List (List Bool × Σaddr:all_types. [addr] → Instruction)
260 ≝
261 [mk_Cartesian ??
262   [ false; false; true; false; false; true; false; true]
263   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
264     direct
265     (λa.
266       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
267             (mk_subaddressing_mode ? ?     a ?))) ].
268ncases daemon.
269nqed.
270
271ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2.
272
273decode_addr_mode; ∀addr:all_types. List Bool → [addr].
274
275decode ≝
276 λl:List Bit.
277  List.iter
278   (fun l0 addr mk_f →
279     match split_prefix l l0 with
280      [ None ⇒ ...
281      | Some r ⇒ mk_f (decode_addr_mode r) ]
282     
283   ) decode_tbl
284
285encode ≝
286
287ndefinition decode_tbl:
288 List (List Bool × Σaddr:all_types. [addr] → Instruction)
289 ≝
290 [mk_Cartesian ??
291   [ False; False; True; False; True]
292   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
293     reg
294     (λa:subaddressing_mode ? [reg].
295       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
296             (mk_subaddressing_mode ? ?     a ?)));
297  mk_Cartesian ??
298   [ False; False; True; False; False; True; False; True]
299   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
300     direct
301     (λa:subaddressing_mode ? [direct].
302       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
303             (mk_subaddressing_mode ? ?     a ?)))
304 ].
305nnormalize;
306 
307 ].
Note: See TracBrowser for help on using the repository browser.