author | huffman |
Fri, 13 Mar 2009 07:35:18 -0700 | |
changeset 30506 | 105ad9a68e51 |
parent 16417 | 9bc16273c2d4 |
child 33695 | bec342db1bf4 |
permissions | -rw-r--r-- |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
1 |
(* Title: Admin/Benchmarks/HOL-datatype/SML.thy |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
2 |
ID: $Id$ |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
3 |
*) |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
4 |
|
16417 | 5 |
theory SML imports Main begin |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
6 |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
7 |
(* ------------------------------------------------------------------------- *) |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
8 |
(* Example from Myra: part of the syntax of SML. *) |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
9 |
(* ------------------------------------------------------------------------- *) |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
10 |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
11 |
datatype |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
12 |
string = EMPTY_STRING | CONS_STRING nat string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
13 |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
14 |
datatype |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
15 |
strid = STRID string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
16 |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
17 |
datatype |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
18 |
var = VAR string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
19 |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
20 |
datatype |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
21 |
con = CON string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
22 |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
23 |
datatype |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
24 |
scon = SCINT nat | SCSTR string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
25 |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
26 |
datatype |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
27 |
excon = EXCON string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
28 |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
29 |
datatype |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
30 |
label = LABEL string |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
31 |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
32 |
datatype |
7373 | 33 |
'a nonemptylist = Head_and_tail 'a "'a list" |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
34 |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
35 |
datatype |
7373 | 36 |
'a long = BASE 'a | QUALIFIED strid "'a long" |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
37 |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
38 |
datatype |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
39 |
atpat_e = WILDCARDatpat_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
40 |
| SCONatpat_e scon |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
41 |
| VARatpat_e var |
7373 | 42 |
| CONatpat_e "con long" |
43 |
| EXCONatpat_e "excon long" |
|
44 |
| RECORDatpat_e "patrow_e option" |
|
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
45 |
| PARatpat_e pat_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
46 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
47 |
patrow_e = DOTDOTDOT_e |
7373 | 48 |
| PATROW_e label pat_e "patrow_e option" |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
49 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
50 |
pat_e = ATPATpat_e atpat_e |
7373 | 51 |
| CONpat_e "con long" atpat_e |
52 |
| EXCONpat_e "excon long" atpat_e |
|
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
53 |
| LAYEREDpat_e var pat_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
54 |
and |
7373 | 55 |
conbind_e = CONBIND_e con "conbind_e option" |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
56 |
and |
7373 | 57 |
datbind_e = DATBIND_e conbind_e "datbind_e option" |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
58 |
and |
7373 | 59 |
exbind_e = EXBIND1_e excon "exbind_e option" |
60 |
| EXBIND2_e excon "excon long" "exbind_e option" |
|
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
61 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
62 |
atexp_e = SCONatexp_e scon |
7373 | 63 |
| VARatexp_e "var long" |
64 |
| CONatexp_e "con long" |
|
65 |
| EXCONatexp_e "excon long" |
|
66 |
| RECORDatexp_e "exprow_e option" |
|
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
67 |
| LETatexp_e dec_e exp_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
68 |
| PARatexp_e exp_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
69 |
and |
7373 | 70 |
exprow_e = EXPROW_e label exp_e "exprow_e option" |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
71 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
72 |
exp_e = ATEXPexp_e atexp_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
73 |
| APPexp_e exp_e atexp_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
74 |
| HANDLEexp_e exp_e match_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
75 |
| RAISEexp_e exp_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
76 |
| FNexp_e match_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
77 |
and |
7373 | 78 |
match_e = MATCH_e mrule_e "match_e option" |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
79 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
80 |
mrule_e = MRULE_e pat_e exp_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
81 |
and |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
82 |
dec_e = VALdec_e valbind_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
83 |
| DATATYPEdec_e datbind_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
84 |
| ABSTYPEdec_e datbind_e dec_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
85 |
| EXCEPTdec_e exbind_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
86 |
| LOCALdec_e dec_e dec_e |
7373 | 87 |
| OPENdec_e "strid long nonemptylist" |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
88 |
| EMPTYdec_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
89 |
| SEQdec_e dec_e dec_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
90 |
and |
7373 | 91 |
valbind_e = PLAINvalbind_e pat_e exp_e "valbind_e option" |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
92 |
| RECvalbind_e valbind_e |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
93 |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
94 |
end |