src/HOL/Datatype_Benchmark/SML.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 45860 93eda35a8377
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     1 (*  Title:      HOL/Datatype_Benchmark/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