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

Last change on this file since 249 was 249, checked in by mulligan, 10 years ago

More work on defining fundamental datatypes.

File size: 2.3 KB
RevLine 
[248]1include "Universes.ma".
2include "Equality.ma".
[249]3include "Either.ma".
[248]4include "BitVector.ma".
[249]5include "String.ma".
[248]6
[249]7ninductive Direct: Type[0] ≝
8  DIRECT: Byte → Direct.
9ninductive Indirect: Type[0] ≝
10  INDIRECT: Bit → Indirect.
11ninductive ExtIndirect: Type[0] ≝
12  EXTINDIRECT: Bit → ExtIndirect.
13ninductive Register: Type[0] ≝
14  REGISTER: Bit → Bit → Bit → Register.
15ninductive AccumulatorA: Type[0] ≝
16  ACCUMULATORA: AccumulatorA.
17ninductive AccumulatorB: Type[0] ≝
18  ACCUMULATORB: AccumulatorB.
19ninductive DPointer: Type[0] ≝
20  DPOINTER: DPointer.
21ninductive Data: Type[0] ≝
22  DATA: Byte → Data.
23ninductive Data16: Type[0] ≝
24  DATA16: Word → Data16.
25ninductive AccumulatorDPointer: Type[0] ≝
26  ACCUMULATORDPOINTER: AccumulatorDPointer.
27ninductive AccumulatorProgramCounter: Type[0] ≝
28  ACCUMULATORPROGRAMCOUNTER: AccumulatorProgramCounter.
29ninductive ExternalIndirectDPointer: Type[0] ≝
30  EXTERNALINDIRECTDPOINTER: ExternalIndirectDPointer.
31ninductive IndirectDPointer: Type[0] ≝
32  INDIRECTDPOINTER: IndirectDPointer.
33ninductive Carry: Type[0] ≝
34  CARRY: Carry.
35ninductive BitAddress: Type[0] ≝
36  BIT: Bit → BitAddress.
37ninductive ComplementBitAddress: Type[0] ≝
38  COMPLEMENTBITADDRESS: Bit → ComplementBitAddress.
39ninductive Relative: Type[0] ≝
40  RELATIVE: Byte → Relative.
41ninductive Address11: Type[0] ≝
42  ADDRESS11: Word11 → Address11.
43ninductive Address16: Type[0] ≝
44  ADDRESS16: Word → Address16.
45
46ninductive Union2 (A: Type[0]) (B: Type[0]): Type[0] ≝
47  U2: A → B → Union2 A B.
48 
49ninductive Union3 (A: Type[0]) (B: Type[0]) (C: Type[0]): Type[0] ≝
50  U3: A → B → C → Union3 A B C.
51 
52ninductive Union6 (A: Type[0]) (B: Type[0])
53                  (C: Type[0]) (D: Type[0])
54                  (E: Type[0]) (F: Type[0]): Type[0] ≝
55  U6: A → B → C → D → E → F → Union6 A B C D E F.
56
57ninductive Jump (A: Type[0]): Type[0] ≝
58  JC: A → Jump A
59| JNC: A → Jump A
60| JB: Bit → A → Jump A
61| JNB: Bit → A → Jump A
62| JBC: Bit → A → Jump A
63| JZ: A → Jump A
64| JNZ: A → Jump A
65| CJNE: (Cartesian (Union2 (Cartesian AccumulatorA (Either Direct Data)) (Cartesian (Either Register Indirect) Data)) A) → Jump A
66| DJNZ: Cartesian (Either Register Direct) A → Jump A.
67
68ndefinition Preamble ≝ List (Cartesian String Nat).
Note: See TracBrowser for help on using the repository browser.