--- a/Admin/Benchmarks/HOL-datatype/Brackin.thy Fri Aug 27 10:49:12 1999 +0200
+++ b/Admin/Benchmarks/HOL-datatype/Brackin.thy Fri Aug 27 10:54:31 1999 +0200
@@ -2,7 +2,7 @@
ID: $Id$
*)
-Brackin = Main +
+theory Brackin = Main:
(* ------------------------------------------------------------------------- *)
(* A couple from Steve Brackin's work. *)
@@ -16,31 +16,31 @@
datatype
('a, 'b, 'c) TY1 =
NoF__
- | Fk__ 'a (('a, 'b, 'c) TY2)
+ | Fk__ 'a "('a, 'b, 'c) TY2"
and
('a, 'b, 'c) TY2 =
Ta__ bool
| Td__ bool
- | Tf__ (('a, 'b, 'c) TY1)
+ | 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)
+ | 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)
+ | 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)
+ | 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/Admin/Benchmarks/HOL-datatype/Instructions.thy Fri Aug 27 10:49:12 1999 +0200
+++ b/Admin/Benchmarks/HOL-datatype/Instructions.thy Fri Aug 27 10:54:31 1999 +0200
@@ -2,7 +2,7 @@
ID: $Id$
*)
-Instructions = Main +
+theory Instructions = Main:
(* ------------------------------------------------------------------------- *)
(* Example from Konrad: 68000 instruction set. *)
@@ -117,8 +117,8 @@
| MOVEtoUSP AddressingMode
| MOVEfromUSP AddressingMode
| MOVEA Size AddressingMode AddressRegister
- | MOVEMto Size AddressingMode (DataOrAddressRegister list)
- | MOVEMfrom Size (DataOrAddressRegister list) AddressingMode
+ | MOVEMto Size AddressingMode "DataOrAddressRegister list"
+ | MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
| MOVEP Size AddressingMode AddressingMode
| MOVEQ nat DataRegister
| MULS AddressingMode DataRegister
--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML Fri Aug 27 10:49:12 1999 +0200
+++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML Fri Aug 27 10:54:31 1999 +0200
@@ -1,10 +1,16 @@
-(* Title: Admin/Benchmarks/HOL-datatype/Brackin.thy
+(* Title: Admin/Benchmarks/HOL-datatype/ROOT.ML
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";
+val tests = ["Brackin", "Instructions", "SML", "Verilog"];
+
+set Toplevel.trace;
+
+warning "\nset quick_and_dirty\n"; set quick_and_dirty;
+seq time_use_thy tests;
+
+warning "\nreset quick_and_dirty\n"; reset quick_and_dirty;
+seq remove_thy tests;
+seq time_use_thy tests;
--- a/Admin/Benchmarks/HOL-datatype/SML.thy Fri Aug 27 10:49:12 1999 +0200
+++ b/Admin/Benchmarks/HOL-datatype/SML.thy Fri Aug 27 10:54:31 1999 +0200
@@ -2,7 +2,7 @@
ID: $Id$
*)
-SML = Main +
+theory SML = Main:
(* ------------------------------------------------------------------------- *)
(* Example from Myra: part of the syntax of SML. *)
@@ -30,44 +30,44 @@
label = LABEL string
datatype
- 'a nonemptylist = Head_and_tail 'a ('a list)
+ 'a nonemptylist = Head_and_tail 'a "'a list"
datatype
- 'a long = BASE 'a | QUALIFIED strid ('a long)
+ '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)
+ | 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)
+ | 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
+ | 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)
+ conbind_e = CONBIND_e con "conbind_e option"
and
- datbind_e = DATBIND_e conbind_e (datbind_e option)
+ 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)
+ 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)
+ | 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)
+ exprow_e = EXPROW_e label exp_e "exprow_e option"
and
exp_e = ATEXPexp_e atexp_e
| APPexp_e exp_e atexp_e
@@ -75,7 +75,7 @@
| RAISEexp_e exp_e
| FNexp_e match_e
and
- match_e = MATCH_e mrule_e (match_e option)
+ match_e = MATCH_e mrule_e "match_e option"
and
mrule_e = MRULE_e pat_e exp_e
and
@@ -84,11 +84,11 @@
| ABSTYPEdec_e datbind_e dec_e
| EXCEPTdec_e exbind_e
| LOCALdec_e dec_e dec_e
- | OPENdec_e ((strid long) nonemptylist)
+ | 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)
+ valbind_e = PLAINvalbind_e pat_e exp_e "valbind_e option"
| RECvalbind_e valbind_e
end
--- a/Admin/Benchmarks/HOL-datatype/Verilog.thy Fri Aug 27 10:49:12 1999 +0200
+++ b/Admin/Benchmarks/HOL-datatype/Verilog.thy Fri Aug 27 10:54:31 1999 +0200
@@ -2,7 +2,7 @@
ID: $Id$
*)
-Verilog = Main +
+theory Verilog = Main:
(* ------------------------------------------------------------------------- *)
(* Example from Daryl: a Verilog grammar. *)
@@ -10,7 +10,7 @@
datatype
Source_text
- = module string (string list) (Module_item list)
+ = module string "string list" "Module_item list"
| Source_textMeta string
and
Module_item
@@ -21,10 +21,10 @@
| 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)
+ = 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
@@ -34,15 +34,15 @@
| 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)
+ 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)
+ | seq_block "string option" "Statement list"
| StatementMeta string
and
Statement_or_null
@@ -55,7 +55,7 @@
| ClockMeta string
and
Case_item
- = case_item (Expression list) Statement_or_null
+ = case_item "Expression list" Statement_or_null
| default_case_item Statement_or_null
| Case_itemMeta string
and
@@ -112,14 +112,14 @@
and
Number
= decimal string
- | based (string option) string
+ | based "string option" string
| NumberMeta string
and
Concatenation
- = concatenation (Expression list) | ConcatenationMeta string
+ = concatenation "Expression list" | ConcatenationMeta string
and
Multiple_concatenation
- = multiple_concatenation Expression (Expression list)
+ = multiple_concatenation Expression "Expression list"
| Multiple_concatenationMeta string
and
meta