use new datatypes for benchmarks
authorblanchet
Thu Sep 11 19:18:23 2014 +0200 (2014-09-11)
changeset 583078172bbb37b06
parent 58306 117ba6cbe414
child 58308 0ccba1b6d00b
use new datatypes for benchmarks
src/HOL/Datatype_Benchmark/Brackin.thy
src/HOL/Datatype_Benchmark/Instructions.thy
     1.1 --- a/src/HOL/Datatype_Benchmark/Brackin.thy	Thu Sep 11 18:54:36 2014 +0200
     1.2 +++ b/src/HOL/Datatype_Benchmark/Brackin.thy	Thu Sep 11 19:18:23 2014 +0200
     1.3 @@ -1,17 +1,17 @@
     1.4  (*  Title:      HOL/Datatype_Benchmark/Brackin.thy
     1.5  
     1.6 -A couple from Steve Brackin's work.
     1.7 +A couple of datatypes from Steve Brackin's work.
     1.8  *)
     1.9  
    1.10  theory Brackin imports Main begin
    1.11  
    1.12 -old_datatype T =
    1.13 +datatype T =
    1.14      X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
    1.15      X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
    1.16      X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
    1.17      X32 | X33 | X34
    1.18  
    1.19 -old_datatype ('a, 'b, 'c) TY1 =
    1.20 +datatype ('a, 'b, 'c) TY1 =
    1.21        NoF
    1.22      | Fk 'a "('a, 'b, 'c) TY2"
    1.23  and ('a, 'b, 'c) TY2 =
     2.1 --- a/src/HOL/Datatype_Benchmark/Instructions.thy	Thu Sep 11 18:54:36 2014 +0200
     2.2 +++ b/src/HOL/Datatype_Benchmark/Instructions.thy	Thu Sep 11 19:18:23 2014 +0200
     2.3 @@ -5,9 +5,9 @@
     2.4  
     2.5  theory Instructions imports Main begin
     2.6  
     2.7 -old_datatype Size = Byte | Word | Long
     2.8 +datatype Size = Byte | Word | Long
     2.9  
    2.10 -old_datatype DataRegister =
    2.11 +datatype DataRegister =
    2.12    RegD0
    2.13  | RegD1
    2.14  | RegD2
    2.15 @@ -17,7 +17,7 @@
    2.16  | RegD6
    2.17  | RegD7
    2.18  
    2.19 -old_datatype AddressRegister =
    2.20 +datatype AddressRegister =
    2.21    RegA0
    2.22  | RegA1
    2.23  | RegA2
    2.24 @@ -27,11 +27,11 @@
    2.25  | RegA6
    2.26  | RegA7
    2.27  
    2.28 -old_datatype DataOrAddressRegister =
    2.29 +datatype DataOrAddressRegister =
    2.30    data DataRegister
    2.31  | address AddressRegister
    2.32  
    2.33 -old_datatype Condition =
    2.34 +datatype Condition =
    2.35    Hi
    2.36  | Ls
    2.37  | Cc
    2.38 @@ -47,7 +47,7 @@
    2.39  | Gt
    2.40  | Le
    2.41  
    2.42 -old_datatype AddressingMode =
    2.43 +datatype AddressingMode =
    2.44    immediate nat
    2.45  | direct DataOrAddressRegister
    2.46  | indirect AddressRegister
    2.47 @@ -59,7 +59,7 @@
    2.48  | pcdisp nat
    2.49  | pcindex nat DataOrAddressRegister Size
    2.50  
    2.51 -old_datatype M68kInstruction =
    2.52 +datatype M68kInstruction =
    2.53    ABCD AddressingMode AddressingMode
    2.54  | ADD Size AddressingMode AddressingMode
    2.55  | ADDA Size AddressingMode AddressRegister