Some rather large datatype examples (from John Harrison).
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Benchmarks/HOL-datatype/Brackin.thy Fri Jul 16 12:02:06 1999 +0200
@@ -0,0 +1,46 @@
+(* Title: Admin/Benchmarks/HOL-datatype/Brackin.thy
+ ID: $Id$
+*)
+
+Brackin = Main +
+
+(* ------------------------------------------------------------------------- *)
+(* A couple from Steve Brackin's work. *)
+(* ------------------------------------------------------------------------- *)
+
+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/Admin/Benchmarks/HOL-datatype/Instructions.thy Fri Jul 16 12:02:06 1999 +0200
@@ -0,0 +1,165 @@
+(* Title: Admin/Benchmarks/HOL-datatype/Instructions.thy
+ ID: $Id$
+*)
+
+Instructions = Main +
+
+(* ------------------------------------------------------------------------- *)
+(* Example from Konrad: 68000 instruction set. *)
+(* ------------------------------------------------------------------------- *)
+
+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/Admin/Benchmarks/HOL-datatype/ROOT.ML Fri Jul 16 12:02:06 1999 +0200
@@ -0,0 +1,10 @@
+(* Title: Admin/Benchmarks/HOL-datatype/Brackin.thy
+ ID: $Id$
+
+Some rather large datatype examples (from John Harrison).
+*)
+
+time_use_thy "Brackin";
+time_use_thy "Instructions";
+time_use_thy "SML";
+time_use_thy "Verilog";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Benchmarks/HOL-datatype/SML.thy Fri Jul 16 12:02:06 1999 +0200
@@ -0,0 +1,94 @@
+(* Title: Admin/Benchmarks/HOL-datatype/SML.thy
+ ID: $Id$
+*)
+
+SML = Main +
+
+(* ------------------------------------------------------------------------- *)
+(* Example from Myra: part of the syntax of SML. *)
+(* ------------------------------------------------------------------------- *)
+
+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/Admin/Benchmarks/HOL-datatype/Verilog.thy Fri Jul 16 12:02:06 1999 +0200
@@ -0,0 +1,141 @@
+(* Title: Admin/Benchmarks/HOL-datatype/Verilog.thy
+ ID: $Id$
+*)
+
+Verilog = Main +
+
+(* ------------------------------------------------------------------------- *)
+(* Example from Daryl: a Verilog grammar. *)
+(* ------------------------------------------------------------------------- *)
+
+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