took out 'old_datatype' examples -- those just cause timeouts in Isatests
authorblanchet
Tue Sep 16 19:23:37 2014 +0200 (2014-09-16)
changeset 58351b3f7c69e9fcd
parent 58350 919149921e46
child 58352 37745650a3f4
took out 'old_datatype' examples -- those just cause timeouts in Isatests
src/HOL/Datatype_Examples/Instructions.thy
src/HOL/Datatype_Examples/SML.thy
src/HOL/Datatype_Examples/Verilog.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/Datatype_Examples/Instructions.thy	Tue Sep 16 19:23:37 2014 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,162 +0,0 @@
     1.4 -(*  Title:      HOL/Datatype_Examples/Instructions.thy
     1.5 -
     1.6 -Example from Konrad: 68000 instruction set.
     1.7 -*)
     1.8 -
     1.9 -theory Instructions imports Main begin
    1.10 -
    1.11 -datatype Size = Byte | Word | Long
    1.12 -
    1.13 -datatype DataRegister =
    1.14 -  RegD0
    1.15 -| RegD1
    1.16 -| RegD2
    1.17 -| RegD3
    1.18 -| RegD4
    1.19 -| RegD5
    1.20 -| RegD6
    1.21 -| RegD7
    1.22 -
    1.23 -datatype AddressRegister =
    1.24 -  RegA0
    1.25 -| RegA1
    1.26 -| RegA2
    1.27 -| RegA3
    1.28 -| RegA4
    1.29 -| RegA5
    1.30 -| RegA6
    1.31 -| RegA7
    1.32 -
    1.33 -datatype DataOrAddressRegister =
    1.34 -  data DataRegister
    1.35 -| address AddressRegister
    1.36 -
    1.37 -datatype Condition =
    1.38 -  Hi
    1.39 -| Ls
    1.40 -| Cc
    1.41 -| Cs
    1.42 -| Ne
    1.43 -| Eq
    1.44 -| Vc
    1.45 -| Vs
    1.46 -| Pl
    1.47 -| Mi
    1.48 -| Ge
    1.49 -| Lt
    1.50 -| Gt
    1.51 -| Le
    1.52 -
    1.53 -datatype AddressingMode =
    1.54 -  immediate nat
    1.55 -| direct DataOrAddressRegister
    1.56 -| indirect AddressRegister
    1.57 -| postinc AddressRegister
    1.58 -| predec AddressRegister
    1.59 -| indirectdisp nat AddressRegister
    1.60 -| indirectindex nat AddressRegister DataOrAddressRegister Size
    1.61 -| absolute nat
    1.62 -| pcdisp nat
    1.63 -| pcindex nat DataOrAddressRegister Size
    1.64 -
    1.65 -old_datatype M68kInstruction =
    1.66 -  ABCD AddressingMode AddressingMode
    1.67 -| ADD Size AddressingMode AddressingMode
    1.68 -| ADDA Size AddressingMode AddressRegister
    1.69 -| ADDI Size nat AddressingMode
    1.70 -| ADDQ Size nat AddressingMode
    1.71 -| ADDX Size AddressingMode AddressingMode
    1.72 -| AND Size AddressingMode AddressingMode
    1.73 -| ANDI Size nat AddressingMode
    1.74 -| ANDItoCCR nat
    1.75 -| ANDItoSR nat
    1.76 -| ASL Size AddressingMode DataRegister
    1.77 -| ASLW AddressingMode
    1.78 -| ASR Size AddressingMode DataRegister
    1.79 -| ASRW AddressingMode
    1.80 -| Bcc Condition Size nat
    1.81 -| BTST Size AddressingMode AddressingMode
    1.82 -| BCHG Size AddressingMode AddressingMode
    1.83 -| BCLR Size AddressingMode AddressingMode
    1.84 -| BSET Size AddressingMode AddressingMode
    1.85 -| BRA Size nat
    1.86 -| BSR Size nat
    1.87 -| CHK AddressingMode DataRegister
    1.88 -| CLR Size AddressingMode
    1.89 -| CMP Size AddressingMode DataRegister
    1.90 -| CMPA Size AddressingMode AddressRegister
    1.91 -| CMPI Size nat AddressingMode
    1.92 -| CMPM Size AddressRegister AddressRegister
    1.93 -| DBT DataRegister nat
    1.94 -| DBF DataRegister nat
    1.95 -| DBcc Condition DataRegister nat
    1.96 -| DIVS AddressingMode DataRegister
    1.97 -| DIVU AddressingMode DataRegister
    1.98 -| EOR Size DataRegister AddressingMode
    1.99 -| EORI Size nat AddressingMode
   1.100 -| EORItoCCR nat
   1.101 -| EORItoSR nat
   1.102 -| EXG DataOrAddressRegister DataOrAddressRegister
   1.103 -| EXT Size DataRegister
   1.104 -| ILLEGAL
   1.105 -| JMP AddressingMode
   1.106 -| JSR AddressingMode
   1.107 -| LEA AddressingMode AddressRegister
   1.108 -| LINK AddressRegister nat
   1.109 -| LSL Size AddressingMode DataRegister
   1.110 -| LSLW AddressingMode
   1.111 -| LSR Size AddressingMode DataRegister
   1.112 -| LSRW AddressingMode
   1.113 -| MOVE Size AddressingMode AddressingMode
   1.114 -| MOVEtoCCR AddressingMode
   1.115 -| MOVEtoSR AddressingMode
   1.116 -| MOVEfromSR AddressingMode
   1.117 -| MOVEtoUSP AddressingMode
   1.118 -| MOVEfromUSP AddressingMode
   1.119 -| MOVEA Size AddressingMode AddressRegister
   1.120 -| MOVEMto Size AddressingMode "DataOrAddressRegister list"
   1.121 -| MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
   1.122 -| MOVEP Size AddressingMode AddressingMode
   1.123 -| MOVEQ nat DataRegister
   1.124 -| MULS AddressingMode DataRegister
   1.125 -| MULU AddressingMode DataRegister
   1.126 -| NBCD AddressingMode
   1.127 -| NEG Size AddressingMode
   1.128 -| NEGX Size AddressingMode
   1.129 -| NOP
   1.130 -| NOT Size AddressingMode
   1.131 -| OR Size AddressingMode AddressingMode
   1.132 -| ORI Size nat AddressingMode
   1.133 -| ORItoCCR nat
   1.134 -| ORItoSR nat
   1.135 -| PEA AddressingMode
   1.136 -| RESET
   1.137 -| ROL Size AddressingMode DataRegister
   1.138 -| ROLW AddressingMode
   1.139 -| ROR Size AddressingMode DataRegister
   1.140 -| RORW AddressingMode
   1.141 -| ROXL Size AddressingMode DataRegister
   1.142 -| ROXLW AddressingMode
   1.143 -| ROXR Size AddressingMode DataRegister
   1.144 -| ROXRW AddressingMode
   1.145 -| RTE
   1.146 -| RTR
   1.147 -| RTS
   1.148 -| SBCD AddressingMode AddressingMode
   1.149 -| ST AddressingMode
   1.150 -| SF AddressingMode
   1.151 -| Scc Condition AddressingMode
   1.152 -| STOP nat
   1.153 -| SUB Size AddressingMode AddressingMode
   1.154 -| SUBA Size AddressingMode AddressingMode
   1.155 -| SUBI Size nat AddressingMode
   1.156 -| SUBQ Size nat AddressingMode
   1.157 -| SUBX Size AddressingMode AddressingMode
   1.158 -| SWAP DataRegister
   1.159 -| TAS AddressingMode
   1.160 -| TRAP nat
   1.161 -| TRAPV
   1.162 -| TST Size AddressingMode
   1.163 -| UNLK AddressRegister
   1.164 -
   1.165 -end
     2.1 --- a/src/HOL/Datatype_Examples/SML.thy	Tue Sep 16 19:23:37 2014 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,91 +0,0 @@
     2.4 -(*  Title:      HOL/Datatype_Examples/SML.thy
     2.5 -
     2.6 -Example from Myra: part of the syntax of SML.
     2.7 -*)
     2.8 -
     2.9 -theory SML imports Main begin
    2.10 -
    2.11 -datatype
    2.12 -  string = EMPTY_STRING | CONS_STRING nat string
    2.13 -
    2.14 -datatype
    2.15 -   strid = STRID string
    2.16 -
    2.17 -datatype
    2.18 -   var = VAR string
    2.19 -
    2.20 -datatype
    2.21 -   con = CON string
    2.22 -
    2.23 -datatype
    2.24 -   scon = SCINT nat | SCSTR string
    2.25 -
    2.26 -datatype
    2.27 -   excon = EXCON string
    2.28 -
    2.29 -datatype
    2.30 -   label = LABEL string
    2.31 -
    2.32 -datatype
    2.33 -  'a nonemptylist = Head_and_tail 'a "'a list"
    2.34 -
    2.35 -datatype
    2.36 -  'a long = BASE 'a | QUALIFIED strid "'a long"
    2.37 -
    2.38 -old_datatype
    2.39 -   atpat_e = WILDCARDatpat_e
    2.40 -           | SCONatpat_e scon
    2.41 -           | VARatpat_e var
    2.42 -           | CONatpat_e "con long"
    2.43 -           | EXCONatpat_e "excon long"
    2.44 -           | RECORDatpat_e "patrow_e option"
    2.45 -           | PARatpat_e pat_e
    2.46 -and
    2.47 -   patrow_e = DOTDOTDOT_e
    2.48 -            | PATROW_e label pat_e "patrow_e option"
    2.49 -and
    2.50 -   pat_e = ATPATpat_e atpat_e
    2.51 -         | CONpat_e "con long" atpat_e
    2.52 -         | EXCONpat_e "excon long" atpat_e
    2.53 -         | LAYEREDpat_e var pat_e
    2.54 -and
    2.55 -   conbind_e = CONBIND_e con "conbind_e option"
    2.56 -and
    2.57 -   datbind_e = DATBIND_e conbind_e "datbind_e option"
    2.58 -and
    2.59 -   exbind_e = EXBIND1_e excon "exbind_e option"
    2.60 -            | EXBIND2_e excon "excon long" "exbind_e option"
    2.61 -and
    2.62 -   atexp_e = SCONatexp_e scon
    2.63 -           | VARatexp_e "var long"
    2.64 -           | CONatexp_e "con long"
    2.65 -           | EXCONatexp_e "excon long"
    2.66 -           | RECORDatexp_e "exprow_e option"
    2.67 -           | LETatexp_e dec_e exp_e
    2.68 -           | PARatexp_e exp_e
    2.69 -and
    2.70 -   exprow_e = EXPROW_e label exp_e "exprow_e option"
    2.71 -and
    2.72 -   exp_e = ATEXPexp_e atexp_e
    2.73 -         | APPexp_e exp_e atexp_e
    2.74 -         | HANDLEexp_e exp_e match_e
    2.75 -         | RAISEexp_e exp_e
    2.76 -         | FNexp_e match_e
    2.77 -and
    2.78 -   match_e = MATCH_e mrule_e "match_e option"
    2.79 -and
    2.80 -   mrule_e = MRULE_e pat_e exp_e
    2.81 -and
    2.82 -   dec_e = VALdec_e valbind_e
    2.83 -         | DATATYPEdec_e datbind_e
    2.84 -         | ABSTYPEdec_e datbind_e dec_e
    2.85 -         | EXCEPTdec_e exbind_e
    2.86 -         | LOCALdec_e dec_e dec_e
    2.87 -         | OPENdec_e "strid long nonemptylist"
    2.88 -         | EMPTYdec_e
    2.89 -         | SEQdec_e dec_e dec_e
    2.90 -and
    2.91 -   valbind_e = PLAINvalbind_e pat_e exp_e "valbind_e option"
    2.92 -             | RECvalbind_e valbind_e
    2.93 -
    2.94 -end
     3.1 --- a/src/HOL/Datatype_Examples/Verilog.thy	Tue Sep 16 19:23:37 2014 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,138 +0,0 @@
     3.4 -(*  Title:      HOL/Datatype_Examples/Verilog.thy
     3.5 -
     3.6 -Example from Daryl: a Verilog grammar.
     3.7 -*)
     3.8 -
     3.9 -theory Verilog imports Main begin
    3.10 -
    3.11 -old_datatype
    3.12 -  Source_text
    3.13 -     = module string "string list" "Module_item list"
    3.14 -     | Source_textMeta string
    3.15 -and
    3.16 -  Module_item
    3.17 -     = "declaration" Declaration
    3.18 -     | initial Statement
    3.19 -     | always Statement
    3.20 -     | assign Lvalue Expression
    3.21 -     | Module_itemMeta string
    3.22 -and
    3.23 -  Declaration
    3.24 -     = reg_declaration "Range option" "string list"
    3.25 -     | net_declaration "Range option" "string list"
    3.26 -     | input_declaration "Range option" "string list"
    3.27 -     | output_declaration "Range option" "string list"
    3.28 -     | DeclarationMeta string
    3.29 -and
    3.30 -  Range = range Expression Expression | RangeMeta string
    3.31 -and
    3.32 -  Statement
    3.33 -     = clock_statement Clock Statement_or_null
    3.34 -     | blocking_assignment Lvalue Expression
    3.35 -     | non_blocking_assignment Lvalue Expression
    3.36 -     | conditional_statement
    3.37 -          Expression Statement_or_null "Statement_or_null option"
    3.38 -     | case_statement Expression "Case_item list"
    3.39 -     | while_loop Expression Statement
    3.40 -     | repeat_loop Expression Statement
    3.41 -     | for_loop
    3.42 -          Lvalue Expression Expression Lvalue Expression Statement
    3.43 -     | forever_loop Statement
    3.44 -     | disable string
    3.45 -     | seq_block "string option" "Statement list"
    3.46 -     | StatementMeta string
    3.47 -and
    3.48 -  Statement_or_null
    3.49 -     = statement Statement | null_statement | Statement_or_nullMeta string
    3.50 -and
    3.51 -  Clock
    3.52 -     = posedge string
    3.53 -     | negedge string
    3.54 -     | clock string
    3.55 -     | ClockMeta string
    3.56 -and
    3.57 -  Case_item
    3.58 -     = case_item "Expression list" Statement_or_null
    3.59 -     | default_case_item Statement_or_null
    3.60 -     | Case_itemMeta string
    3.61 -and
    3.62 -  Expression
    3.63 -     = plus Expression Expression
    3.64 -     | minus Expression Expression
    3.65 -     | lshift Expression Expression
    3.66 -     | rshift Expression Expression
    3.67 -     | lt Expression Expression
    3.68 -     | leq Expression Expression
    3.69 -     | gt Expression Expression
    3.70 -     | geq Expression Expression
    3.71 -     | logeq Expression Expression
    3.72 -     | logneq Expression Expression
    3.73 -     | caseeq Expression Expression
    3.74 -     | caseneq Expression Expression
    3.75 -     | bitand Expression Expression
    3.76 -     | bitxor Expression Expression
    3.77 -     | bitor Expression Expression
    3.78 -     | logand Expression Expression
    3.79 -     | logor Expression Expression
    3.80 -     | conditional Expression Expression Expression
    3.81 -     | positive Primary
    3.82 -     | negative Primary
    3.83 -     | lognot Primary
    3.84 -     | bitnot Primary
    3.85 -     | reducand Primary
    3.86 -     | reducxor Primary
    3.87 -     | reducor Primary
    3.88 -     | reducnand Primary
    3.89 -     | reducxnor Primary
    3.90 -     | reducnor Primary
    3.91 -     | primary Primary
    3.92 -     | ExpressionMeta string
    3.93 -and
    3.94 -  Primary
    3.95 -     = primary_number Number
    3.96 -     | primary_IDENTIFIER string
    3.97 -     | primary_bit_select string Expression
    3.98 -     | primary_part_select string Expression Expression
    3.99 -     | primary_gen_bit_select Expression Expression
   3.100 -     | primary_gen_part_select Expression Expression Expression
   3.101 -     | primary_concatenation Concatenation
   3.102 -     | primary_multiple_concatenation Multiple_concatenation
   3.103 -     | brackets Expression
   3.104 -     | PrimaryMeta string
   3.105 -and
   3.106 -  Lvalue
   3.107 -     = lvalue string
   3.108 -     | lvalue_bit_select string Expression
   3.109 -     | lvalue_part_select string Expression Expression
   3.110 -     | lvalue_concatenation Concatenation
   3.111 -     | LvalueMeta string
   3.112 -and
   3.113 -  Number
   3.114 -     = decimal string
   3.115 -     | based "string option" string
   3.116 -     | NumberMeta string
   3.117 -and
   3.118 -  Concatenation
   3.119 -     = concatenation "Expression list" | ConcatenationMeta string
   3.120 -and
   3.121 -  Multiple_concatenation
   3.122 -     = multiple_concatenation Expression "Expression list"
   3.123 -     | Multiple_concatenationMeta string
   3.124 -and
   3.125 -  meta
   3.126 -     = Meta_Source_text Source_text
   3.127 -     | Meta_Module_item Module_item
   3.128 -     | Meta_Declaration Declaration
   3.129 -     | Meta_Range Range
   3.130 -     | Meta_Statement Statement
   3.131 -     | Meta_Statement_or_null Statement_or_null
   3.132 -     | Meta_Clock Clock
   3.133 -     | Meta_Case_item Case_item
   3.134 -     | Meta_Expression Expression
   3.135 -     | Meta_Primary Primary
   3.136 -     | Meta_Lvalue Lvalue
   3.137 -     | Meta_Number Number
   3.138 -     | Meta_Concatenation Concatenation
   3.139 -     | Meta_Multiple_concatenation Multiple_concatenation
   3.140 -
   3.141 -end
     4.1 --- a/src/HOL/ROOT	Tue Sep 16 19:23:37 2014 +0200
     4.2 +++ b/src/HOL/ROOT	Tue Sep 16 19:23:37 2014 +0200
     4.3 @@ -755,10 +755,7 @@
     4.4      Misc_Primrec
     4.5    theories [condition = ISABELLE_FULL_TEST, timing]
     4.6      Brackin
     4.7 -    Instructions
     4.8      IsaFoR
     4.9 -    SML
    4.10 -    Verilog
    4.11  
    4.12  session "HOL-Word" (main) in Word = HOL +
    4.13    options [document_graph]