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