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