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

Last change on this file since 260 was 260, checked in by sacerdot, 9 years ago
  • Minimal changes to make it compile with the standard distribution of Matita once this directory is substituted to nlibrary
  • ambiguity reduced by lower-casing booleans
File size: 6.7 KB
Line 
1include "Universes.ma".
2include "Plogic/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
112naxiom daemon: False.
113
114naxiom decode_register: Vector Bool (S (S (S Z))) → [reg].
115naxiom decode_direct:   Vector Bool (S (S (S Z))) → [direct].
116
117ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction))
118 ≝
119 [mk_Cartesian ??
120   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
121     (λl.
122       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
123             (mk_subaddressing_mode ? ?    (decode_register l) ?));
124  mk_Cartesian ??
125   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
126     (λl.
127       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
128             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
129ncases daemon.
130nqed.
131
132
133naxiom decode_register: List Bool → [reg].
134naxiom decode_direct: List Bool → [direct].
135
136ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction))
137 ≝
138 [mk_Cartesian ??
139   [ false; false; true; false; true]
140     (λl.
141       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
142             (mk_subaddressing_mode ? ?    (decode_register l) ?));
143  mk_Cartesian ??
144   [ false; false; true; false; true]
145     (λl.
146       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
147             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
148ncases daemon.
149nqed.
150
151
152ndefinition decode_tbl1:
153 List (List Bool × Σaddr:all_types. [addr] → Instruction)
154 ≝
155 [mk_Cartesian ??
156   [ false; false; true; false; true]
157   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
158     reg
159     (λa.
160       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
161             (mk_subaddressing_mode ? ? a ?))) ].
162ncases daemon.
163nqed.
164             
165ndefinition decode_tbl2:
166 List (List Bool × Σaddr:all_types. [addr] → Instruction)
167 ≝
168 [mk_Cartesian ??
169   [ false; false; true; false; false; true; false; true]
170   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
171     direct
172     (λa.
173       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
174             (mk_subaddressing_mode ? ?     a ?))) ].
175ncases daemon.
176nqed.
177
178ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2.
179
180decode_addr_mode; ∀addr:all_types. List Bool → [addr].
181
182decode ≝
183 λl:List Bit.
184  List.iter
185   (fun l0 addr mk_f →
186     match split_prefix l l0 with
187      [ None ⇒ ...
188      | Some r ⇒ mk_f (decode_addr_mode r) ]
189     
190   ) decode_tbl
191
192encode ≝
193
194ndefinition decode_tbl:
195 List (List Bool × Σaddr:all_types. [addr] → Instruction)
196 ≝
197 [mk_Cartesian ??
198   [ False; False; True; False; True]
199   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
200     reg
201     (λa:subaddressing_mode ? [reg].
202       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
203             (mk_subaddressing_mode ? ?     a ?)));
204  mk_Cartesian ??
205   [ False; False; True; False; False; True; False; True]
206   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
207     direct
208     (λa:subaddressing_mode ? [direct].
209       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
210             (mk_subaddressing_mode ? ?     a ?)))
211 ].
212nnormalize;
213 
214 ].
Note: See TracBrowser for help on using the repository browser.