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 *)

    13 (* list-data-structure

    14 nominal_datatype tkind =

    15   KStar

    16 | KFun "tkind" "tkind"

    17 and ckind =

    18   CKEq "ty" "ty"

    19 and ty =

    20   TVar "tvar"

    21 | TC "string"

    22 | TApp "ty" "ty"

    23 | TFun "string" "ty list"

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

    25 | TEq "ty" "ty" "ty"

    26 and co =

    27   CC "string"

    28 | CApp "co" "co"

    29 | CFun "string" "co list"

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

    31 | CEq "co" "co" "co"

    32 | CSym "co"

    33 | CCir "co" "co"

    34 | CLeft "co"

    35 | CRight "co"

    36 | CSim "co"

    37 | CRightc "co"

    38 | CLeftc "co"

    39 | CCoe "co" "co"

    40 

    41 abbreviation

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

    43 

    44 nominal_datatype trm =

    45   Var "var"

    46 | C "string"

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

    48 | APP "trm" "ty"

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

    50 | App "trm" "trm"

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

    52 | Case "trm" "assoc list"

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

    54 and assoc =

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

    56 and pat =

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

    58 binder

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

    60 where

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

    62 *)

    63 

    64 end

    65 

    66 

    67