--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF_Examples/Brackin.thy Thu Sep 11 19:20:23 2014 +0200
@@ -0,0 +1,41 @@
+(* Title: HOL/Datatype_Benchmark/Brackin.thy
+
+A couple of datatypes from Steve Brackin's work.
+*)
+
+theory Brackin imports Main begin
+
+datatype T =
+ X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
+ X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
+ X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
+ X32 | X33 | X34
+
+datatype ('a, 'b, 'c) TY1 =
+ NoF
+ | Fk 'a "('a, 'b, 'c) TY2"
+and ('a, 'b, 'c) TY2 =
+ Ta bool
+ | Td bool
+ | Tf "('a, 'b, 'c) TY1"
+ | Tk bool
+ | Tp bool
+ | App 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
+ | Pair "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
+and ('a, 'b, 'c) TY3 =
+ NoS
+ | Fresh "('a, 'b, 'c) TY2"
+ | Trustworthy 'a
+ | PrivateKey 'a 'b 'c
+ | PublicKey 'a 'b 'c
+ | Conveyed 'a "('a, 'b, 'c) TY2"
+ | Possesses 'a "('a, 'b, 'c) TY2"
+ | Received 'a "('a, 'b, 'c) TY2"
+ | Recognizes 'a "('a, 'b, 'c) TY2"
+ | NeverMalFromSelf 'a 'b "('a, 'b, 'c) TY2"
+ | Sends 'a "('a, 'b, 'c) TY2" 'b
+ | SharedSecret 'a "('a, 'b, 'c) TY2" 'b
+ | Believes 'a "('a, 'b, 'c) TY3"
+ | And "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF_Examples/Instructions.thy Thu Sep 11 19:20:23 2014 +0200
@@ -0,0 +1,162 @@
+(* Title: HOL/Datatype_Benchmark/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
+
+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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF_Examples/SML.thy Thu Sep 11 19:20:23 2014 +0200
@@ -0,0 +1,91 @@
+(* Title: HOL/Datatype_Benchmark/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"
+
+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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF_Examples/Verilog.thy Thu Sep 11 19:20:23 2014 +0200
@@ -0,0 +1,138 @@
+(* Title: HOL/Datatype_Benchmark/Verilog.thy
+
+Example from Daryl: a Verilog grammar.
+*)
+
+theory Verilog imports Main begin
+
+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
--- a/src/HOL/Datatype_Benchmark/Brackin.thy Thu Sep 11 19:18:23 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(* Title: HOL/Datatype_Benchmark/Brackin.thy
-
-A couple of datatypes from Steve Brackin's work.
-*)
-
-theory Brackin imports Main begin
-
-datatype T =
- X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
- X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
- X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
- X32 | X33 | X34
-
-datatype ('a, 'b, 'c) TY1 =
- NoF
- | Fk 'a "('a, 'b, 'c) TY2"
-and ('a, 'b, 'c) TY2 =
- Ta bool
- | Td bool
- | Tf "('a, 'b, 'c) TY1"
- | Tk bool
- | Tp bool
- | App 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
- | Pair "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
-and ('a, 'b, 'c) TY3 =
- NoS
- | Fresh "('a, 'b, 'c) TY2"
- | Trustworthy 'a
- | PrivateKey 'a 'b 'c
- | PublicKey 'a 'b 'c
- | Conveyed 'a "('a, 'b, 'c) TY2"
- | Possesses 'a "('a, 'b, 'c) TY2"
- | Received 'a "('a, 'b, 'c) TY2"
- | Recognizes 'a "('a, 'b, 'c) TY2"
- | NeverMalFromSelf 'a 'b "('a, 'b, 'c) TY2"
- | Sends 'a "('a, 'b, 'c) TY2" 'b
- | SharedSecret 'a "('a, 'b, 'c) TY2" 'b
- | Believes 'a "('a, 'b, 'c) TY3"
- | And "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
-
-end
--- a/src/HOL/Datatype_Benchmark/Instructions.thy Thu Sep 11 19:18:23 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,162 +0,0 @@
-(* Title: HOL/Datatype_Benchmark/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
-
-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
--- a/src/HOL/Datatype_Benchmark/SML.thy Thu Sep 11 19:18:23 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-(* Title: HOL/Datatype_Benchmark/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"
-
-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
--- a/src/HOL/Datatype_Benchmark/Verilog.thy Thu Sep 11 19:18:23 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,138 +0,0 @@
-(* Title: HOL/Datatype_Benchmark/Verilog.thy
-
-Example from Daryl: a Verilog grammar.
-*)
-
-theory Verilog imports Main begin
-
-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
--- a/src/HOL/ROOT Thu Sep 11 19:18:23 2014 +0200
+++ b/src/HOL/ROOT Thu Sep 11 19:20:23 2014 +0200
@@ -749,7 +749,11 @@
Misc_Primcorec
Misc_Primrec
theories [condition = ISABELLE_FULL_TEST]
+ Brackin
+ Instructions
IsaFoR_Datatypes
+ SML
+ Verilog
session "HOL-Word" (main) in Word = HOL +
options [document_graph]