1 theory SystemFOmega

     2 imports "../Nominal2"

     3 begin

     4 

     5 text {*

     6   System from the F-ing paper by Rossberg, Russo and 

     7   Dreyer, TLDI'10

     8 *}

     9 

    10 

    11 atom_decl var

    12 atom_decl tvar

    13 atom_decl label

    14 

    15 nominal_datatype kind =

    16   \<Omega> | KFun kind kind

    17 

    18 nominal_datatype ty =

    19   TVar tvar

    20 | TFun ty ty

    21 | TAll a::tvar kind t::ty bind a in t

    22 | TEx  a::tvar kind t::ty bind a in t

    23 | TLam a::tvar kind t::ty bind a in t

    24 | TApp ty ty

    25 | TRec trec

    26 and trec =

    27   TRNil

    28 | TRCons label ty trec 

    29 

    30 nominal_datatype trm =

    31   Var var

    32 | Lam x::var ty t::trm bind x in t

    33 | App trm trm

    34 | Dot trm label

    35 | LAM a::tvar kind t::trm bind a in t

    36 | APP trm ty

    37 | Pack ty trm

    38 | Unpack a::tvar x::var trm t::trm bind a x in t

    39 | Rec rec 

    40 and rec =

    41   RNil

    42 | RCons label trm rec

    43 

    44 

    45 

    46 

    47 end

    48 

    49 

    50 

    51