theory ExCoreHaskell

imports "Parser"

begin

(* core haskell *)

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

ML {* val _ = cheat_bn_eqvt := true *}

ML {* val _ = cheat_bn_rsp := true *}

ML {* val _ = cheat_const_rsp := true *}

ML {* val _ = cheat_alpha_bn_rsp := true *}

atom_decl var

atom_decl tvar

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

nominal_datatype tkind =

  KStar

| KFun "tkind" "tkind"

and ckind =

  CKEq "ty" "ty"

and ty =

  TVar "tvar"

| TC "char"

| TApp "ty" "ty"

| TFun "char" "ty_lst"

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

| TEq "ty" "ty" "ty"

and ty_lst =

  TsNil

| TsCons "ty" "ty_lst"

and co =

  CC "char"

| CApp "co" "co"

| CFun "char" "co_lst"

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

| CEq "co" "co" "co"

| CSym "co"

| CCir "co" "co"

| CLeft "co"

| CRight "co"

| CSim "co"

| CRightc "co"

| CLeftc "co"

| CCoe "co" "co"

and co_lst =

  CsNil

| CsCons "co" "co_lst"

and trm =

  Var "var"

| C "char"

| LAMT tv::"tvar" "tkind" t::"trm" bind tv in t

| LAMC tv::"tvar" "ckind" t::"trm" bind tv in t

| APP "trm" "ty"

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

| App "trm" "trm"

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

| Case "trm" "assoc_lst"

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

and assoc_lst =

  ANil

| ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t

and pat =

  K "char" "tvtk_lst" "tvck_lst" "vt_lst"

and vt_lst =

  VTNil

| VTCons "var" "ty" "vt_lst"

and tvtk_lst =

  TVTKNil

| TVTKCons "tvar" "tkind" "tvtk_lst"

and tvck_lst =

  TVCKNil

| TVCKCons "tvar" "ckind" "tvck_lst"

binder

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

and bv_vt :: "vt_lst \<Rightarrow> atom set"

and bv_tvtk :: "tvtk_lst \<Rightarrow> atom set"

and bv_tvck :: "tvck_lst \<Rightarrow> atom set"

where

  "bv (K s tvts tvcs vs) = (bv_tvtk tvts) \<union> (bv_tvck tvcs) \<union> (bv_vt vs)"

| "bv_vt VTNil = {}"

| "bv_vt (VTCons v k t) = {atom v} \<union> bv_vt t"

| "bv_tvtk TVTKNil = {}"

| "bv_tvtk (TVTKCons v k t) = {atom v} \<union> bv_tvtk t"

| "bv_tvck TVCKNil = {}"

| "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t"

end