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