--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Benchmarks/HOL-datatype/SML.thy Fri Jul 16 12:02:06 1999 +0200
@@ -0,0 +1,94 @@
+(* Title: Admin/Benchmarks/HOL-datatype/SML.thy
+ ID: $Id$
+*)
+
+SML = Main +
+
+(* ------------------------------------------------------------------------- *)
+(* Example from Myra: part of the syntax of SML. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype
+ string = EMPTY_STRING | CONS_STRING nat string
+
+datatype
+ strid = STRID string
+
+datatype
+ var = VAR string
+
+datatype
+ con = CON string
+
+datatype
+ scon = SCINT nat | SCSTR string
+
+datatype
+ excon = EXCON string
+
+datatype
+ label = LABEL string
+
+datatype
+ 'a nonemptylist = Head_and_tail 'a ('a list)
+
+datatype
+ '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)
+ | PARatpat_e pat_e
+and
+ patrow_e = DOTDOTDOT_e
+ | 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
+ | LAYEREDpat_e var pat_e
+and
+ conbind_e = CONBIND_e con (conbind_e option)
+and
+ 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)
+and
+ atexp_e = SCONatexp_e scon
+ | 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)
+and
+ exp_e = ATEXPexp_e atexp_e
+ | APPexp_e exp_e atexp_e
+ | HANDLEexp_e exp_e match_e
+ | RAISEexp_e exp_e
+ | FNexp_e match_e
+and
+ match_e = MATCH_e mrule_e (match_e option)
+and
+ mrule_e = MRULE_e pat_e exp_e
+and
+ dec_e = VALdec_e valbind_e
+ | DATATYPEdec_e datbind_e
+ | ABSTYPEdec_e datbind_e dec_e
+ | EXCEPTdec_e exbind_e
+ | LOCALdec_e dec_e dec_e
+ | 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)
+ | RECvalbind_e valbind_e
+
+end