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

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

Work on ASM.ma file.

File size: 6.7 KB
Line 
1include "Universes.ma".
2include "Equality.ma".
3include "Either.ma".
4include "BitVector.ma".
5include "BitVectorTrie.ma".
6
7ninductive all_types : Type[0] ≝
8   reg: all_types | direct: all_types | indirect:all_types | data:all_types
9   | acc: all_types | rel: all_types.
10
11interpretation "Cartesian" 'product A B = (Cartesian A B).
12interpretation "Either" 'plus A B = (Either A B).
13
14ninductive addressing_mode: Type[0] ≝
15  DIRECT: Byte → addressing_mode
16| INDIRECT: Bit → addressing_mode
17| EXTINDIRECT: Bit → addressing_mode
18| REGISTER: Bit → Bit → Bit → addressing_mode
19| ACCUMULATORA: addressing_mode
20| ACCUMULATORB: addressing_mode
21| DPOINTER: addressing_mode
22| DATA: Byte → addressing_mode
23| DATA16: Word → addressing_mode
24| ACCUMULATORDPOINTER: addressing_mode
25| ACCUMULATORPROGRAMCOUNTER: addressing_mode
26| EXTERNALINDIRECTDPOINTER: addressing_mode
27| INDIRECTDPOINTER: addressing_mode
28| CARRY: addressing_mode
29| BIT: Bit → addressing_mode
30| COMPLEMENTBITADDRESS: Bit → addressing_mode
31| RELATIVE: Byte → addressing_mode
32| ADDRESS11: Word11 → addressing_mode
33| ADDRESS16: Word → addressing_mode.
34
35(* to avoid expansion... *)
36nlet rec is_a (d:all_types) (A:addressing_mode) on d ≝
37  match d with
38   [ reg ⇒ match A with [ REGISTER _ _ _ ⇒ True | _ ⇒ False ]
39   | data ⇒ match A with [ DATA _ ⇒ True | _ ⇒ False ]
40   | rel ⇒ match A with [ RELATIVE _ ⇒ True | _ ⇒ False ]
41   | acc ⇒ match A with [ ACCUMULATORA ⇒ True | _ ⇒ False ]
42   | direct ⇒ match A with [ DIRECT _ ⇒ True | _ ⇒ False ]
43   | indirect ⇒ match A with [ INDIRECT _ ⇒ True | _ ⇒ False ]].
44
45interpretation "Bool" 'or a b = (inclusive_disjunction a b).
46
47nlet rec is_in n (l: Vector all_types (S n)) (A:addressing_mode) on l : Bool ≝
48 match l return λm.λ_:Vector all_types m .∀K:m=S n.Bool with
49  [ Empty ⇒ λK.⊥
50  | Cons m he (tl: Vector all_types m) ⇒ λ_.
51     match m return λz.m = z → Bool with
52      [ Z ⇒ λ_.is_a he A
53      | S p ⇒ λK.is_a he A ∨ is_in p (? tl) A] (?: m=m)] (?: S n = S n).
54##[##4: #x; ncases K; napply x ]
55//; ndestruct.
56nqed.
57
58nrecord subaddressing_mode (n) (l: Vector all_types (S n)) : Type[0] ≝
59 { subaddressing_modeel:> addressing_mode;
60   subaddressing_modein:
61    match is_in ? l subaddressing_modeel with [ True ⇒ (? : Prop) | False ⇒ (? : Prop) ]
62 }.
63##[ napply True | napply False ]
64nqed.
65
66ncoercion subaddressing_mode : ∀n.∀l:Vector all_types (S n).Type[0]
67 ≝ subaddressing_mode on _l: Vector all_types (S ?) to Type[0].
68
69(*
70ncoercion mk_subaddressing_mode :
71 ∀n.∀l:Vector all_types (S n).∀a:addressing_mode.
72  ∀p:?(*match is_in ? l a return λ_.Prop with [True ⇒ True | False ⇒ False]*).subaddressing_mode n l
73 ≝ mk_subaddressing_mode on _a:addressing_mode to subaddressing_mode ? ?.
74*)
75
76ninductive Jump (A: Type[0]): Type[0] ≝
77  JC: A → Jump A
78| JNC: A → Jump A
79| JB: Bit → A → Jump A
80| JNB: Bit → A → Jump A
81| JBC: Bit → A → Jump A
82| JZ: A → Jump A
83| JNZ: A → Jump A
84| CJNE: (([acc] × [direct; data]) + [reg; indirect] × [data]) → A → Jump A
85| DJNZ: [reg ; direct] → A → Jump A
86| ADD: [acc] → [reg; direct; indirect; data] → Jump A.
87
88ndefinition xxx: Jump Nat.
89 napply (DJNZ ? (mk_subaddressing_mode ?? (REGISTER [True] [True] [True]) ?) (Z: Nat)).
90 napply I;
91nqed.
92
93naxiom bar: addressing_mode → Nat.
94
95ndefinition barj ≝
96 λA.λf:A → Nat.λJ:Jump A.
97  match J with
98   [ DJNZ arg1 arg2 ⇒ f arg2 + bar arg1
99   | _ ⇒ (Z: Nat)].
100   
101ndefinition PreInstruction ≝ λA: Type[0]. Jump A.
102
103ndefinition Instruction ≝ PreInstruction [rel].
104
105nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ {
106   elem:> A;
107   witness: T elem
108}.
109
110interpretation "Sigma" 'sigma T = (Sigma ? T).
111
112ndefinition true: Bool ≝ True.
113ndefinition false: Bool ≝ False.
114naxiom daemon: False.
115
116naxiom decode_register: Vector Bool (S (S (S Z))) → [reg].
117naxiom decode_direct:   Vector Bool (S (S (S Z))) → [direct].
118
119ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction))
120 ≝
121 [mk_Cartesian ??
122   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
123     (λl.
124       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
125             (mk_subaddressing_mode ? ?    (decode_register l) ?));
126  mk_Cartesian ??
127   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
128     (λl.
129       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
130             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
131ncases daemon.
132nqed.
133
134
135naxiom decode_register: List Bool → [reg].
136naxiom decode_direct: List Bool → [direct].
137
138ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction))
139 ≝
140 [mk_Cartesian ??
141   [ false; false; true; false; true]
142     (λl.
143       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
144             (mk_subaddressing_mode ? ?    (decode_register l) ?));
145  mk_Cartesian ??
146   [ false; false; true; false; true]
147     (λl.
148       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
149             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
150ncases daemon.
151nqed.
152
153
154ndefinition decode_tbl1:
155 List (List Bool × Σaddr:all_types. [addr] → Instruction)
156 ≝
157 [mk_Cartesian ??
158   [ false; false; true; false; true]
159   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
160     reg
161     (λa.
162       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
163             (mk_subaddressing_mode ? ? a ?))) ].
164ncases daemon.
165nqed.
166             
167ndefinition decode_tbl2:
168 List (List Bool × Σaddr:all_types. [addr] → Instruction)
169 ≝
170 [mk_Cartesian ??
171   [ false; false; true; false; false; true; false; true]
172   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
173     direct
174     (λa.
175       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
176             (mk_subaddressing_mode ? ?     a ?))) ].
177ncases daemon.
178nqed.
179
180ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2.
181
182decode_addr_mode; ∀addr:all_types. List Bool → [addr].
183
184decode ≝
185 λl:List Bit.
186  List.iter
187   (fun l0 addr mk_f →
188     match split_prefix l l0 with
189      [ None ⇒ ...
190      | Some r ⇒ mk_f (decode_addr_mode r) ]
191     
192   ) decode_tbl
193
194encode ≝
195
196ndefinition decode_tbl:
197 List (List Bool × Σaddr:all_types. [addr] → Instruction)
198 ≝
199 [mk_Cartesian ??
200   [ False; False; True; False; True]
201   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
202     reg
203     (λa:subaddressing_mode ? [reg].
204       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
205             (mk_subaddressing_mode ? ?     a ?)));
206  mk_Cartesian ??
207   [ False; False; True; False; False; True; False; True]
208   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
209     direct
210     (λa:subaddressing_mode ? [direct].
211       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
212             (mk_subaddressing_mode ? ?     a ?)))
213 ].
214nnormalize;
215 
216 ].
Note: See TracBrowser for help on using the repository browser.