src/HOL/Datatype_Benchmark/Instructions.thy
author blanchet
Thu, 11 Sep 2014 18:54:36 +0200
changeset 58305 57752a91eec4
parent 45860 93eda35a8377
child 58307 8172bbb37b06
permissions -rw-r--r--
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45860
93eda35a8377 more visible benchmarks;
wenzelm
parents: 33695
diff changeset
     1
(*  Title:      HOL/Datatype_Benchmark/Instructions.thy
33695
bec342db1bf4 eliminated obsolete CVS Ids;
wenzelm
parents: 16417
diff changeset
     2
bec342db1bf4 eliminated obsolete CVS Ids;
wenzelm
parents: 16417
diff changeset
     3
Example from Konrad: 68000 instruction set.
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
     4
*)
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
     5
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 7373
diff changeset
     6
theory Instructions imports Main begin
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
     7
58305
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
     8
old_datatype Size = Byte | Word | Long
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
     9
58305
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    10
old_datatype DataRegister =
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    11
  RegD0
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    12
| RegD1
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    13
| RegD2
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    14
| RegD3
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    15
| RegD4
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    16
| RegD5
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    17
| RegD6
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    18
| RegD7
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    19
58305
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    20
old_datatype AddressRegister =
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    21
  RegA0
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    22
| RegA1
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    23
| RegA2
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    24
| RegA3
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    25
| RegA4
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    26
| RegA5
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    27
| RegA6
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    28
| RegA7
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    29
58305
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    30
old_datatype DataOrAddressRegister =
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    31
  data DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    32
| address AddressRegister
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    33
58305
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    34
old_datatype Condition =
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    35
  Hi
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    36
| Ls
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    37
| Cc
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    38
| Cs
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    39
| Ne
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    40
| Eq
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    41
| Vc
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    42
| Vs
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    43
| Pl
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    44
| Mi
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    45
| Ge
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    46
| Lt
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    47
| Gt
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    48
| Le
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    49
58305
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    50
old_datatype AddressingMode =
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    51
  immediate nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    52
| direct DataOrAddressRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    53
| indirect AddressRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    54
| postinc AddressRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    55
| predec AddressRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    56
| indirectdisp nat AddressRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    57
| indirectindex nat AddressRegister DataOrAddressRegister Size
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    58
| absolute nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    59
| pcdisp nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    60
| pcindex nat DataOrAddressRegister Size
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    61
58305
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    62
old_datatype M68kInstruction =
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    63
  ABCD AddressingMode AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    64
| ADD Size AddressingMode AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    65
| ADDA Size AddressingMode AddressRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    66
| ADDI Size nat AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    67
| ADDQ Size nat AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    68
| ADDX Size AddressingMode AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    69
| AND Size AddressingMode AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    70
| ANDI Size nat AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    71
| ANDItoCCR nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    72
| ANDItoSR nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    73
| ASL Size AddressingMode DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    74
| ASLW AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    75
| ASR Size AddressingMode DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    76
| ASRW AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    77
| Bcc Condition Size nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    78
| BTST Size AddressingMode AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    79
| BCHG Size AddressingMode AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    80
| BCLR Size AddressingMode AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    81
| BSET Size AddressingMode AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    82
| BRA Size nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    83
| BSR Size nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    84
| CHK AddressingMode DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    85
| CLR Size AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    86
| CMP Size AddressingMode DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    87
| CMPA Size AddressingMode AddressRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    88
| CMPI Size nat AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    89
| CMPM Size AddressRegister AddressRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    90
| DBT DataRegister nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    91
| DBF DataRegister nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    92
| DBcc Condition DataRegister nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    93
| DIVS AddressingMode DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    94
| DIVU AddressingMode DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    95
| EOR Size DataRegister AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    96
| EORI Size nat AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    97
| EORItoCCR nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    98
| EORItoSR nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
    99
| EXG DataOrAddressRegister DataOrAddressRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   100
| EXT Size DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   101
| ILLEGAL
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   102
| JMP AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   103
| JSR AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   104
| LEA AddressingMode AddressRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   105
| LINK AddressRegister nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   106
| LSL Size AddressingMode DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   107
| LSLW AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   108
| LSR Size AddressingMode DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   109
| LSRW AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   110
| MOVE Size AddressingMode AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   111
| MOVEtoCCR AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   112
| MOVEtoSR AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   113
| MOVEfromSR AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   114
| MOVEtoUSP AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   115
| MOVEfromUSP AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   116
| MOVEA Size AddressingMode AddressRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   117
| MOVEMto Size AddressingMode "DataOrAddressRegister list"
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   118
| MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   119
| MOVEP Size AddressingMode AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   120
| MOVEQ nat DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   121
| MULS AddressingMode DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   122
| MULU AddressingMode DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   123
| NBCD AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   124
| NEG Size AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   125
| NEGX Size AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   126
| NOP
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   127
| NOT Size AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   128
| OR Size AddressingMode AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   129
| ORI Size nat AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   130
| ORItoCCR nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   131
| ORItoSR nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   132
| PEA AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   133
| RESET
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   134
| ROL Size AddressingMode DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   135
| ROLW AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   136
| ROR Size AddressingMode DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   137
| RORW AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   138
| ROXL Size AddressingMode DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   139
| ROXLW AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   140
| ROXR Size AddressingMode DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   141
| ROXRW AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   142
| RTE
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   143
| RTR
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   144
| RTS
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   145
| SBCD AddressingMode AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   146
| ST AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   147
| SF AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   148
| Scc Condition AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   149
| STOP nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   150
| SUB Size AddressingMode AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   151
| SUBA Size AddressingMode AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   152
| SUBI Size nat AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   153
| SUBQ Size nat AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   154
| SUBX Size AddressingMode AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   155
| SWAP DataRegister
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   156
| TAS AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   157
| TRAP nat
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   158
| TRAPV
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   159
| TST Size AddressingMode
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 45860
diff changeset
   160
| UNLK AddressRegister
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
   161
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
   162
end