--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/ExCoreHaskell.thy	Tue Mar 23 09:06:28 2010 +0100
@@ -0,0 +1,67 @@
+theory ExCoreHaskell
+imports "Parser"
+begin
+
+(* core haskell *)
+
+ML {* val _ = recursive := false  *}
+
+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 "string"
+| TApp "ty" "ty"
+| TFun "string" "ty list"
+| TAll tv::"tvar" "tkind" T::"ty"  bind tv in T
+| TEq "ty" "ty" "ty"
+and co =
+  CC "string"
+| CApp "co" "co"
+| CFun "string" "co list"
+| 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
+
+
+