theory ExCoreHaskell

imports "Parser"

begin

(* core haskell *)

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

atom_decl var

atom_decl tvar

nominal_datatype tkind =

  KStar

| KFun "tkind" "tkind"

and ckind =

  CKEq "ty" "ty"

and ty =

  TVar "tvar"

| TC "string"

| TApp "ty" "ty"

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

| TEq "ty" "ty" "ty"

and co =

  CC "string"

| CApp "co" "co"

| 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"

abbreviation

  "atoms A \<equiv> atom ` A"

nominal_datatype trm =

  Var "var"

| C "string"

| LAM tv::"tvar" "kind" 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 list"

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

and assoc =

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

and pat =

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

binder

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

where

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

*)

end