# HG changeset patch # User blanchet # Date 1410888217 -7200 # Node ID b3f7c69e9fcdb235b3c2f7a802be3a0405143e76 # Parent 919149921e467293634de992fc8a1f03f24cf2fc took out 'old_datatype' examples -- those just cause timeouts in Isatests diff -r 919149921e46 -r b3f7c69e9fcd src/HOL/Datatype_Examples/Instructions.thy --- a/src/HOL/Datatype_Examples/Instructions.thy Tue Sep 16 19:23:37 2014 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,162 +0,0 @@ -(* Title: HOL/Datatype_Examples/Instructions.thy - -Example from Konrad: 68000 instruction set. -*) - -theory Instructions imports Main begin - -datatype Size = Byte | Word | Long - -datatype DataRegister = - RegD0 -| RegD1 -| RegD2 -| RegD3 -| RegD4 -| RegD5 -| RegD6 -| RegD7 - -datatype AddressRegister = - RegA0 -| RegA1 -| RegA2 -| RegA3 -| RegA4 -| RegA5 -| RegA6 -| RegA7 - -datatype DataOrAddressRegister = - data DataRegister -| address AddressRegister - -datatype Condition = - Hi -| Ls -| Cc -| Cs -| Ne -| Eq -| Vc -| Vs -| Pl -| Mi -| Ge -| Lt -| Gt -| Le - -datatype AddressingMode = - immediate nat -| direct DataOrAddressRegister -| indirect AddressRegister -| postinc AddressRegister -| predec AddressRegister -| indirectdisp nat AddressRegister -| indirectindex nat AddressRegister DataOrAddressRegister Size -| absolute nat -| pcdisp nat -| pcindex nat DataOrAddressRegister Size - -old_datatype M68kInstruction = - ABCD AddressingMode AddressingMode -| ADD Size AddressingMode AddressingMode -| ADDA Size AddressingMode AddressRegister -| ADDI Size nat AddressingMode -| ADDQ Size nat AddressingMode -| ADDX Size AddressingMode AddressingMode -| AND Size AddressingMode AddressingMode -| ANDI Size nat AddressingMode -| ANDItoCCR nat -| ANDItoSR nat -| ASL Size AddressingMode DataRegister -| ASLW AddressingMode -| ASR Size AddressingMode DataRegister -| ASRW AddressingMode -| Bcc Condition Size nat -| BTST Size AddressingMode AddressingMode -| BCHG Size AddressingMode AddressingMode -| BCLR Size AddressingMode AddressingMode -| BSET Size AddressingMode AddressingMode -| BRA Size nat -| BSR Size nat -| CHK AddressingMode DataRegister -| CLR Size AddressingMode -| CMP Size AddressingMode DataRegister -| CMPA Size AddressingMode AddressRegister -| CMPI Size nat AddressingMode -| CMPM Size AddressRegister AddressRegister -| DBT DataRegister nat -| DBF DataRegister nat -| DBcc Condition DataRegister nat -| DIVS AddressingMode DataRegister -| DIVU AddressingMode DataRegister -| EOR Size DataRegister AddressingMode -| EORI Size nat AddressingMode -| EORItoCCR nat -| EORItoSR nat -| EXG DataOrAddressRegister DataOrAddressRegister -| EXT Size DataRegister -| ILLEGAL -| JMP AddressingMode -| JSR AddressingMode -| LEA AddressingMode AddressRegister -| LINK AddressRegister nat -| LSL Size AddressingMode DataRegister -| LSLW AddressingMode -| LSR Size AddressingMode DataRegister -| LSRW AddressingMode -| MOVE Size AddressingMode AddressingMode -| MOVEtoCCR AddressingMode -| MOVEtoSR AddressingMode -| MOVEfromSR AddressingMode -| MOVEtoUSP AddressingMode -| MOVEfromUSP AddressingMode -| MOVEA Size AddressingMode AddressRegister -| MOVEMto Size AddressingMode "DataOrAddressRegister list" -| MOVEMfrom Size "DataOrAddressRegister list" AddressingMode -| MOVEP Size AddressingMode AddressingMode -| MOVEQ nat DataRegister -| MULS AddressingMode DataRegister -| MULU AddressingMode DataRegister -| NBCD AddressingMode -| NEG Size AddressingMode -| NEGX Size AddressingMode -| NOP -| NOT Size AddressingMode -| OR Size AddressingMode AddressingMode -| ORI Size nat AddressingMode -| ORItoCCR nat -| ORItoSR nat -| PEA AddressingMode -| RESET -| ROL Size AddressingMode DataRegister -| ROLW AddressingMode -| ROR Size AddressingMode DataRegister -| RORW AddressingMode -| ROXL Size AddressingMode DataRegister -| ROXLW AddressingMode -| ROXR Size AddressingMode DataRegister -| ROXRW AddressingMode -| RTE -| RTR -| RTS -| SBCD AddressingMode AddressingMode -| ST AddressingMode -| SF AddressingMode -| Scc Condition AddressingMode -| STOP nat -| SUB Size AddressingMode AddressingMode -| SUBA Size AddressingMode AddressingMode -| SUBI Size nat AddressingMode -| SUBQ Size nat AddressingMode -| SUBX Size AddressingMode AddressingMode -| SWAP DataRegister -| TAS AddressingMode -| TRAP nat -| TRAPV -| TST Size AddressingMode -| UNLK AddressRegister - -end diff -r 919149921e46 -r b3f7c69e9fcd src/HOL/Datatype_Examples/SML.thy --- a/src/HOL/Datatype_Examples/SML.thy Tue Sep 16 19:23:37 2014 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,91 +0,0 @@ -(* Title: HOL/Datatype_Examples/SML.thy - -Example from Myra: part of the syntax of SML. -*) - -theory SML imports Main begin - -datatype - string = EMPTY_STRING | CONS_STRING nat string - -datatype - strid = STRID string - -datatype - var = VAR string - -datatype - con = CON string - -datatype - scon = SCINT nat | SCSTR string - -datatype - excon = EXCON string - -datatype - label = LABEL string - -datatype - 'a nonemptylist = Head_and_tail 'a "'a list" - -datatype - 'a long = BASE 'a | QUALIFIED strid "'a long" - -old_datatype - atpat_e = WILDCARDatpat_e - | SCONatpat_e scon - | VARatpat_e var - | CONatpat_e "con long" - | EXCONatpat_e "excon long" - | RECORDatpat_e "patrow_e option" - | PARatpat_e pat_e -and - patrow_e = DOTDOTDOT_e - | PATROW_e label pat_e "patrow_e option" -and - pat_e = ATPATpat_e atpat_e - | CONpat_e "con long" atpat_e - | EXCONpat_e "excon long" atpat_e - | LAYEREDpat_e var pat_e -and - conbind_e = CONBIND_e con "conbind_e option" -and - datbind_e = DATBIND_e conbind_e "datbind_e option" -and - exbind_e = EXBIND1_e excon "exbind_e option" - | EXBIND2_e excon "excon long" "exbind_e option" -and - atexp_e = SCONatexp_e scon - | VARatexp_e "var long" - | CONatexp_e "con long" - | EXCONatexp_e "excon long" - | RECORDatexp_e "exprow_e option" - | LETatexp_e dec_e exp_e - | PARatexp_e exp_e -and - exprow_e = EXPROW_e label exp_e "exprow_e option" -and - exp_e = ATEXPexp_e atexp_e - | APPexp_e exp_e atexp_e - | HANDLEexp_e exp_e match_e - | RAISEexp_e exp_e - | FNexp_e match_e -and - match_e = MATCH_e mrule_e "match_e option" -and - mrule_e = MRULE_e pat_e exp_e -and - dec_e = VALdec_e valbind_e - | DATATYPEdec_e datbind_e - | ABSTYPEdec_e datbind_e dec_e - | EXCEPTdec_e exbind_e - | LOCALdec_e dec_e dec_e - | OPENdec_e "strid long nonemptylist" - | EMPTYdec_e - | SEQdec_e dec_e dec_e -and - valbind_e = PLAINvalbind_e pat_e exp_e "valbind_e option" - | RECvalbind_e valbind_e - -end diff -r 919149921e46 -r b3f7c69e9fcd src/HOL/Datatype_Examples/Verilog.thy --- a/src/HOL/Datatype_Examples/Verilog.thy Tue Sep 16 19:23:37 2014 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,138 +0,0 @@ -(* Title: HOL/Datatype_Examples/Verilog.thy - -Example from Daryl: a Verilog grammar. -*) - -theory Verilog imports Main begin - -old_datatype - Source_text - = module string "string list" "Module_item list" - | Source_textMeta string -and - Module_item - = "declaration" Declaration - | initial Statement - | always Statement - | assign Lvalue Expression - | Module_itemMeta string -and - Declaration - = reg_declaration "Range option" "string list" - | net_declaration "Range option" "string list" - | input_declaration "Range option" "string list" - | output_declaration "Range option" "string list" - | DeclarationMeta string -and - Range = range Expression Expression | RangeMeta string -and - Statement - = clock_statement Clock Statement_or_null - | blocking_assignment Lvalue Expression - | non_blocking_assignment Lvalue Expression - | conditional_statement - Expression Statement_or_null "Statement_or_null option" - | case_statement Expression "Case_item list" - | while_loop Expression Statement - | repeat_loop Expression Statement - | for_loop - Lvalue Expression Expression Lvalue Expression Statement - | forever_loop Statement - | disable string - | seq_block "string option" "Statement list" - | StatementMeta string -and - Statement_or_null - = statement Statement | null_statement | Statement_or_nullMeta string -and - Clock - = posedge string - | negedge string - | clock string - | ClockMeta string -and - Case_item - = case_item "Expression list" Statement_or_null - | default_case_item Statement_or_null - | Case_itemMeta string -and - Expression - = plus Expression Expression - | minus Expression Expression - | lshift Expression Expression - | rshift Expression Expression - | lt Expression Expression - | leq Expression Expression - | gt Expression Expression - | geq Expression Expression - | logeq Expression Expression - | logneq Expression Expression - | caseeq Expression Expression - | caseneq Expression Expression - | bitand Expression Expression - | bitxor Expression Expression - | bitor Expression Expression - | logand Expression Expression - | logor Expression Expression - | conditional Expression Expression Expression - | positive Primary - | negative Primary - | lognot Primary - | bitnot Primary - | reducand Primary - | reducxor Primary - | reducor Primary - | reducnand Primary - | reducxnor Primary - | reducnor Primary - | primary Primary - | ExpressionMeta string -and - Primary - = primary_number Number - | primary_IDENTIFIER string - | primary_bit_select string Expression - | primary_part_select string Expression Expression - | primary_gen_bit_select Expression Expression - | primary_gen_part_select Expression Expression Expression - | primary_concatenation Concatenation - | primary_multiple_concatenation Multiple_concatenation - | brackets Expression - | PrimaryMeta string -and - Lvalue - = lvalue string - | lvalue_bit_select string Expression - | lvalue_part_select string Expression Expression - | lvalue_concatenation Concatenation - | LvalueMeta string -and - Number - = decimal string - | based "string option" string - | NumberMeta string -and - Concatenation - = concatenation "Expression list" | ConcatenationMeta string -and - Multiple_concatenation - = multiple_concatenation Expression "Expression list" - | Multiple_concatenationMeta string -and - meta - = Meta_Source_text Source_text - | Meta_Module_item Module_item - | Meta_Declaration Declaration - | Meta_Range Range - | Meta_Statement Statement - | Meta_Statement_or_null Statement_or_null - | Meta_Clock Clock - | Meta_Case_item Case_item - | Meta_Expression Expression - | Meta_Primary Primary - | Meta_Lvalue Lvalue - | Meta_Number Number - | Meta_Concatenation Concatenation - | Meta_Multiple_concatenation Multiple_concatenation - -end diff -r 919149921e46 -r b3f7c69e9fcd src/HOL/ROOT --- a/src/HOL/ROOT Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/ROOT Tue Sep 16 19:23:37 2014 +0200 @@ -755,10 +755,7 @@ Misc_Primrec theories [condition = ISABELLE_FULL_TEST, timing] Brackin - Instructions IsaFoR - SML - Verilog session "HOL-Word" (main) in Word = HOL + options [document_graph]