author  wenzelm 
Tue, 24 Jul 2007 19:44:32 +0200  
changeset 23961  9e7e1e309ebd 
parent 16417  9bc16273c2d4 
child 33695  bec342db1bf4 
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 

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 