Changeset 249


Ignore:
Timestamp:
Nov 22, 2010, 1:55:07 PM (9 years ago)
Author:
mulligan
Message:

More work on defining fundamental datatypes.

Location:
Deliverables/D4.1/Matita
Files:
2 added
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/ASM.ma

    r248 r249  
    11include "Universes.ma".
    22include "Equality.ma".
     3include "Either.ma".
    34include "BitVector.ma".
     5include "String.ma".
    46
    5 ninductive AddressingMode: Type[0] ≝
    6   Direct: Byte → AddressingMode
    7 | Indirect: Bit → AddressingMode
    8 | ExtIndirect: Bit → AddressingMode
    9 | Register: Bit → Bit → Bit → AddressingMode
    10 | AccumulatorA: AddressingMode
    11 | AccumulatorB: AddressingMode
    12 | DPointer: AddressingMode
    13 | Data: Byte → AddressingMode
    14 | Data16: Word → AddressingMode
    15 | AccumulatorDPointer: AddressingMode
    16 | AccumulatorProgramCounter: AddressingMode
    17 | ExternalIndirectDPointer: AddressingMode
    18 | IndirectDPointer: AddressingMode
    19 | Carry: AddressingMode
    20 | Bit: Bit → AddressingMode
    21 | ComplementBit: Bit → AddressingMode
    22 | Relative: Byte → AddressingMode
    23 | Address11: Word11 → AddressingMode
    24 | Address16: Word → AddressingMode.
     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 TracChangeset for help on using the changeset viewer.