author  berghofe 
Fri, 16 Jul 1999 12:02:06 +0200  
changeset 7013  8a7fb425e04a 
child 7373  776d888472aa 
permissions  rwrr 
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

1 
(* Title: Admin/Benchmarks/HOLdatatype/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 

8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

5 
SML = Main + 
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 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

33 
'a nonemptylist = Head_and_tail 'a ('a list) 
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 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

36 
'a long = BASE 'a  QUALIFIED strid ('a long) 
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 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

42 
 CONatpat_e (con long) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

43 
 EXCONatpat_e (excon long) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

44 
 RECORDatpat_e (patrow_e option) 
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 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

48 
 PATROW_e label pat_e (patrow_e option) 
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 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

51 
 CONpat_e (con long) atpat_e 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

52 
 EXCONpat_e (excon long) atpat_e 
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 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

55 
conbind_e = CONBIND_e con (conbind_e option) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

56 
and 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

57 
datbind_e = DATBIND_e conbind_e (datbind_e option) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

58 
and 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

59 
exbind_e = EXBIND1_e excon (exbind_e option) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

60 
 EXBIND2_e excon (excon long) (exbind_e option) 
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 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

63 
 VARatexp_e (var long) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

64 
 CONatexp_e (con long) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

65 
 EXCONatexp_e (excon long) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

66 
 RECORDatexp_e (exprow_e option) 
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 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

70 
exprow_e = EXPROW_e label exp_e (exprow_e option) 
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 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

78 
match_e = MATCH_e mrule_e (match_e option) 
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 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

87 
 OPENdec_e ((strid long) nonemptylist) 
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 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

91 
valbind_e = PLAINvalbind_e pat_e exp_e (valbind_e option) 
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 