1 theory ExCoreHaskell

     2 imports "Parser"

     3 begin

     4 

     5 (* core haskell *)

     6 

     7 ML {* val _ = recursive := false  *}

     8 

     9 atom_decl var

    10 atom_decl tvar

    11 

    12 (* there are types, coercion types and regular types list-data-structure *)

    13 nominal_datatype tkind =

    14   KStar

    15 | KFun "tkind" "tkind"

    16 and ckind =

    17   CKEq "ty" "ty"

    18 and ty =

    19   TVar "tvar"

    20 | TC "string"

    21 | TApp "ty" "ty"

    22 | TFun "string" "ty_lst"

    23 | TAll tv::"tvar" "tkind" T::"ty"  bind tv in T

    24 | TEq "ty" "ty" "ty"

    25 and ty_lst =

    26   TsNil

    27 | TsCons "ty" "ty_lst"

    28 and co =

    29   CC "string"

    30 | CApp "co" "co"

    31 | CFun "string" "co_lst"

    32 | CAll tv::"tvar" "ckind" C::"co"  bind tv in C

    33 | CEq "co" "co" "co"

    34 | CSym "co"

    35 | CCir "co" "co"

    36 | CLeft "co"

    37 | CRight "co"

    38 | CSim "co"

    39 | CRightc "co"

    40 | CLeftc "co"

    41 | CCoe "co" "co"

    42 and co_lst =

    43   CsNil

    44 | CsCons "co" "co_lst"

    45 

    46 (*

    47 abbreviation

    48   "atoms A \<equiv> atom ` A"

    49 

    50 nominal_datatype trm =

    51   Var "var"

    52 | C "string"

    53 | LAM tv::"tvar" "kind" t::"trm"   bind tv in t

    54 | APP "trm" "ty"

    55 | Lam v::"var" "ty" t::"trm"       bind v in t

    56 | App "trm" "trm"

    57 | Let x::"var" "ty" "trm" t::"trm" bind x in t

    58 | Case "trm" "assoc list"

    59 | Cast "trm" "ty"                   --"ty is supposed to be a coercion type only"

    60 and assoc =

    61   A p::"pat" t::"trm" bind "bv p" in t

    62 and pat =

    63   K "string" "(tvar \<times> kind) list" "(var \<times> ty) list"

    64 binder

    65  bv :: "pat \<Rightarrow> atom set"

    66 where

    67  "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"

    68 *)

    69 

    70 end

    71 

    72 

    73