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