Changeset 264 for Deliverables/D4.1/Matita/ASM.ma
- Timestamp:
- Nov 23, 2010, 5:05:07 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/ASM.ma
r262 r264 1 include "Universes.ma".2 include "Plogic/equality.ma".3 1 include "Either.ma". 4 include "BitVector.ma".5 2 include "BitVectorTrie.ma". 3 include "String.ma". 6 4 7 5 interpretation "Cartesian" 'product A B = (Cartesian A B). … … 178 176 | NOP: preinstruction A. 179 177 178 ndefinition instruction ≝ preinstruction [[relative]]. 180 179 181 ndefinition xxx: jump Nat. 182 napply (DJNZ ? (REGISTER [true] [true] [true]) Z). 183 napply I; 184 nqed. 180 ninductive labelled_instruction: Type[0] ≝ 181 Instruction: instruction → labelled_instruction 182 | Cost: String → labelled_instruction 183 | Jmp: String → labelled_instruction 184 | Call: String → labelled_instruction 185 | Mov: [[dptr]] × String → labelled_instruction 186 | WithLabel: preinstruction String → labelled_instruction. 185 187 186 n axiom bar: addressing_mode → Nat.188 ndefinition preamble ≝ List (String × Nat). 187 189 188 ndefinition 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 194 ndefinition PreInstruction ≝ λA: Type[0]. Jump A. 195 196 ndefinition Instruction ≝ PreInstruction [rel]. 197 198 nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ { 199 elem:> A; 200 witness: T elem 201 }. 202 203 interpretation "Sigma" 'sigma T = (Sigma ? T). 204 205 naxiom daemon: False. 206 207 naxiom decode_register: Vector Bool (S (S (S Z))) → [reg]. 208 naxiom decode_direct: Vector Bool (S (S (S Z))) → [direct]. 209 210 ndefinition 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) ?)) ]. 222 ncases daemon. 223 nqed. 224 225 226 naxiom decode_register: List Bool → [reg]. 227 naxiom decode_direct: List Bool → [direct]. 228 229 ndefinition 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) ?)) ]. 241 ncases daemon. 242 nqed. 243 244 245 ndefinition 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 ?))) ]. 255 ncases daemon. 256 nqed. 257 258 ndefinition 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 ?))) ]. 268 ncases daemon. 269 nqed. 270 271 ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2. 272 273 decode_addr_mode; ∀addr:all_types. List Bool → [addr]. 274 275 decode ≝ 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 285 encode ≝ 286 287 ndefinition 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 ]. 305 nnormalize; 306 307 ]. 190 ndefinition assembly_program ≝ preamble × (List labelled_instruction).
Note: See TracChangeset
for help on using the changeset viewer.