# HG changeset patch
# User berghofe
# Date 932119326 -7200
# Node ID 8a7fb425e04ab97729ecbbc84c0ce94123230f23
# Parent  ae9dac5af9d13d040e6b6e3f1c17480b77921ce1
Some rather large datatype examples (from John Harrison).

diff -r ae9dac5af9d1 -r 8a7fb425e04a Admin/Benchmarks/HOL-datatype/Brackin.thy
--- /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
diff -r ae9dac5af9d1 -r 8a7fb425e04a Admin/Benchmarks/HOL-datatype/Instructions.thy
--- /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
diff -r ae9dac5af9d1 -r 8a7fb425e04a Admin/Benchmarks/HOL-datatype/ROOT.ML
--- /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";
diff -r ae9dac5af9d1 -r 8a7fb425e04a Admin/Benchmarks/HOL-datatype/SML.thy
--- /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
diff -r ae9dac5af9d1 -r 8a7fb425e04a Admin/Benchmarks/HOL-datatype/Verilog.thy
--- /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