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
18| REGISTER: Bit → Bit → Bit → 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] ≝
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(*
72  ∀p:?(*match is_in ? l a return λ_.Prop with [True ⇒ True | False ⇒ False]*).subaddressing_mode n l
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
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.
125             (mk_subaddressing_mode ? ?    (decode_register l) ?));
126  mk_Cartesian ??
127   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
128     (λl.
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.
144             (mk_subaddressing_mode ? ?    (decode_register l) ?));
145  mk_Cartesian ??
146   [ false; false; true; false; true]
147     (λl.
149             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
150ncases daemon.
151nqed.
152
153
154ndefinition decode_tbl1:
156 ≝
157 [mk_Cartesian ??
158   [ false; false; true; false; true]
160     reg
161     (λa.
163             (mk_subaddressing_mode ? ? a ?))) ].
164ncases daemon.
165nqed.
166
167ndefinition decode_tbl2:
169 ≝
170 [mk_Cartesian ??
171   [ false; false; true; false; false; true; false; true]
173     direct
174     (λa.
176             (mk_subaddressing_mode ? ?     a ?))) ].
177ncases daemon.
178nqed.
179
180ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2.
181
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:
198 ≝
199 [mk_Cartesian ??
200   [ False; False; True; False; True]
202     reg