# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1267093800 -3600
# Node ID fc8f5897b00a591d13df379e00f196fda3d86cfd
# Parent  853abc14c5c67b8c3826831bcb366822c31cda8f
first attempt to make sense out of the core-haskell definition

diff -r 853abc14c5c6 -r fc8f5897b00a Nominal/Test.thy
--- a/Nominal/Test.thy	Thu Feb 25 08:40:52 2010 +0100
+++ b/Nominal/Test.thy	Thu Feb 25 11:30:00 2010 +0100
@@ -24,17 +24,17 @@
 
 text {* example 2 *}
 
-nominal_datatype trm =
+nominal_datatype trm' =
   Var "name"
-| App "trm" "trm"
-| Lam x::"name" t::"trm"        bind x in t 
-| Let p::"pat" "trm" t::"trm"   bind "f p" in t
-and pat =
+| App "trm'" "trm'"
+| Lam x::"name" t::"trm'"        bind x in t 
+| Let p::"pat'" "trm'" t::"trm'"   bind "f p" in t
+and pat' =
   PN
 | PS "name"
 | PD "name" "name"
 binder
-  f::"pat \<Rightarrow> name set"
+  f::"pat' \<Rightarrow> name set"
 where 
   "f PN = {}"
 | "f (PS x) = {x}"
@@ -61,12 +61,12 @@
 thm f0_raw.simps
 
 text {* example type schemes *}
-datatype ty = 
+datatype t = 
   Var "name" 
-| Fun "ty" "ty"
+| Fun "t" "t"
 
 nominal_datatype tyS = 
-  All xs::"name list" ty::"ty" bind xs in ty
+  All xs::"name list" ty::"t" bind xs in ty
 
 
 
@@ -195,6 +195,63 @@
   "bv9 (Var9 x) = {}"
 | "bv9 (Lam9 x b) = {atom x}"
 
+
+(* core haskell *)
+
+atom_decl var
+atom_decl tvar
+atom_decl co
+
+datatype sort = 
+  TY tvar
+| CO co
+
+datatype kind = 
+  KStar
+| KFun kind kind
+| KEq kind kind
+
+(* there are types, coercion types and regular types *)
+nominal_datatype ty =
+  TVar tvar
+| TFun string "ty list"
+| TAll tvar kind ty --"some binding"
+| TSym ty
+| TCir ty ty
+| TApp ty ty
+| TLeft ty
+| TRight ty
+| TEq ty
+| TRightc ty
+| TLeftc ty
+| TCoe ty ty
+
+typedecl ty --"hack since ty is not yet defined"
+
+abbreviation 
+  "atoms A \<equiv> atom ` A"
+
+nominal_datatype trm =
+  Var var
+| LAM tv::tvar kind t::trm   bind v 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)))"
+
+
+thm bv_raw.simps
+
 end