
wenzelm@45860: (*  Title:      HOL/Datatype_Benchmark/Instructions.thy
wenzelm@33695: 
wenzelm@33695: Example from Konrad: 68000 instruction set.
berghofe@7013: *)
berghofe@7013: 
haftmann@16417: theory Instructions imports Main begin
berghofe@7013: 
berghofe@7013: datatype Size = Byte | Word | Long
berghofe@7013: 
berghofe@7013: datatype DataRegister
berghofe@7013:               = RegD0
berghofe@7013:               | RegD1
berghofe@7013:               | RegD2
berghofe@7013:               | RegD3
berghofe@7013:               | RegD4
berghofe@7013:               | RegD5
berghofe@7013:               | RegD6
berghofe@7013:               | RegD7
berghofe@7013: 
berghofe@7013: datatype AddressRegister
berghofe@7013:               = RegA0
berghofe@7013:               | RegA1
berghofe@7013:               | RegA2
berghofe@7013:               | RegA3
berghofe@7013:               | RegA4
berghofe@7013:               | RegA5
berghofe@7013:               | RegA6
berghofe@7013:               | RegA7
berghofe@7013: 
berghofe@7013: datatype DataOrAddressRegister
berghofe@7013:               = data DataRegister
berghofe@7013:               | address AddressRegister
berghofe@7013: 
berghofe@7013: datatype Condition
berghofe@7013:               = Hi
berghofe@7013:               | Ls
berghofe@7013:               | Cc
berghofe@7013:               | Cs
berghofe@7013:               | Ne
berghofe@7013:               | Eq
berghofe@7013:               | Vc
berghofe@7013:               | Vs
berghofe@7013:               | Pl
berghofe@7013:               | Mi
berghofe@7013:               | Ge
berghofe@7013:               | Lt
berghofe@7013:               | Gt
berghofe@7013:               | Le
berghofe@7013: 
berghofe@7013: datatype AddressingMode
berghofe@7013:         = immediate nat
berghofe@7013:         | direct DataOrAddressRegister
berghofe@7013:         | indirect AddressRegister
berghofe@7013:         | postinc AddressRegister
berghofe@7013:         | predec AddressRegister
berghofe@7013:         | indirectdisp nat AddressRegister
berghofe@7013:         | indirectindex nat AddressRegister DataOrAddressRegister Size
berghofe@7013:         | absolute nat
berghofe@7013:         | pcdisp nat
berghofe@7013:         | pcindex nat DataOrAddressRegister Size
berghofe@7013: 
berghofe@7013: datatype M68kInstruction
berghofe@7013:     = ABCD AddressingMode AddressingMode
berghofe@7013:     | ADD Size AddressingMode AddressingMode
berghofe@7013:     | ADDA Size AddressingMode AddressRegister
berghofe@7013:     | ADDI Size nat AddressingMode
berghofe@7013:     | ADDQ Size nat AddressingMode
berghofe@7013:     | ADDX Size AddressingMode AddressingMode
berghofe@7013:     | AND Size AddressingMode AddressingMode
berghofe@7013:     | ANDI Size nat AddressingMode
berghofe@7013:     | ANDItoCCR nat
berghofe@7013:     | ANDItoSR nat
berghofe@7013:     | ASL Size AddressingMode DataRegister
berghofe@7013:     | ASLW AddressingMode
berghofe@7013:     | ASR Size AddressingMode DataRegister
berghofe@7013:     | ASRW AddressingMode
berghofe@7013:     | Bcc Condition Size nat
berghofe@7013:     | BTST Size AddressingMode AddressingMode
berghofe@7013:     | BCHG Size AddressingMode AddressingMode
berghofe@7013:     | BCLR Size AddressingMode AddressingMode
berghofe@7013:     | BSET Size AddressingMode AddressingMode
berghofe@7013:     | BRA Size nat
berghofe@7013:     | BSR Size nat
berghofe@7013:     | CHK AddressingMode DataRegister
berghofe@7013:     | CLR Size AddressingMode
berghofe@7013:     | CMP Size AddressingMode DataRegister
berghofe@7013:     | CMPA Size AddressingMode AddressRegister
berghofe@7013:     | CMPI Size nat AddressingMode
berghofe@7013:     | CMPM Size AddressRegister AddressRegister
berghofe@7013:     | DBT DataRegister nat
berghofe@7013:     | DBF DataRegister nat
berghofe@7013:     | DBcc Condition DataRegister nat
berghofe@7013:     | DIVS AddressingMode DataRegister
berghofe@7013:     | DIVU AddressingMode DataRegister
berghofe@7013:     | EOR Size DataRegister AddressingMode
berghofe@7013:     | EORI Size nat AddressingMode
berghofe@7013:     | EORItoCCR nat
berghofe@7013:     | EORItoSR nat
berghofe@7013:     | EXG DataOrAddressRegister DataOrAddressRegister
berghofe@7013:     | EXT Size DataRegister
berghofe@7013:     | ILLEGAL
berghofe@7013:     | JMP AddressingMode
berghofe@7013:     | JSR AddressingMode
berghofe@7013:     | LEA AddressingMode AddressRegister
berghofe@7013:     | LINK AddressRegister nat
berghofe@7013:     | LSL Size AddressingMode DataRegister
berghofe@7013:     | LSLW AddressingMode
berghofe@7013:     | LSR Size AddressingMode DataRegister
berghofe@7013:     | LSRW AddressingMode
berghofe@7013:     | MOVE Size AddressingMode AddressingMode
berghofe@7013:     | MOVEtoCCR AddressingMode
berghofe@7013:     | MOVEtoSR AddressingMode
berghofe@7013:     | MOVEfromSR AddressingMode
berghofe@7013:     | MOVEtoUSP AddressingMode
berghofe@7013:     | MOVEfromUSP AddressingMode
berghofe@7013:     | MOVEA Size AddressingMode AddressRegister
wenzelm@7373:     | MOVEMto Size AddressingMode "DataOrAddressRegister list"
wenzelm@7373:     | MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
berghofe@7013:     | MOVEP Size AddressingMode AddressingMode
berghofe@7013:     | MOVEQ nat DataRegister
berghofe@7013:     | MULS AddressingMode DataRegister
berghofe@7013:     | MULU AddressingMode DataRegister
berghofe@7013:     | NBCD AddressingMode
berghofe@7013:     | NEG Size AddressingMode
berghofe@7013:     | NEGX Size AddressingMode
berghofe@7013:     | NOP
berghofe@7013:     | NOT Size AddressingMode
berghofe@7013:     | OR Size AddressingMode AddressingMode
berghofe@7013:     | ORI Size nat AddressingMode
berghofe@7013:     | ORItoCCR nat
berghofe@7013:     | ORItoSR nat
berghofe@7013:     | PEA AddressingMode
berghofe@7013:     | RESET
berghofe@7013:     | ROL Size AddressingMode DataRegister
berghofe@7013:     | ROLW AddressingMode
berghofe@7013:     | ROR Size AddressingMode DataRegister
berghofe@7013:     | RORW AddressingMode
berghofe@7013:     | ROXL Size AddressingMode DataRegister
berghofe@7013:     | ROXLW AddressingMode
berghofe@7013:     | ROXR Size AddressingMode DataRegister
berghofe@7013:     | ROXRW AddressingMode
berghofe@7013:     | RTE
berghofe@7013:     | RTR
berghofe@7013:     | RTS
berghofe@7013:     | SBCD AddressingMode AddressingMode
berghofe@7013:     | ST AddressingMode
berghofe@7013:     | SF AddressingMode
berghofe@7013:     | Scc Condition AddressingMode
berghofe@7013:     | STOP nat
berghofe@7013:     | SUB Size AddressingMode AddressingMode
berghofe@7013:     | SUBA Size AddressingMode AddressingMode
berghofe@7013:     | SUBI Size nat AddressingMode
berghofe@7013:     | SUBQ Size nat AddressingMode
berghofe@7013:     | SUBX Size AddressingMode AddressingMode
berghofe@7013:     | SWAP DataRegister
berghofe@7013:     | TAS AddressingMode
berghofe@7013:     | TRAP nat
berghofe@7013:     | TRAPV
berghofe@7013:     | TST Size AddressingMode
berghofe@7013:     | UNLK AddressRegister
berghofe@7013: 
berghofe@7013: end




