--- a/Nominal/Parser.thy	Thu Feb 25 12:30:50 2010 +0100
+++ b/Nominal/Parser.thy	Thu Feb 25 12:32:15 2010 +0100
@@ -11,24 +11,21 @@
 
 Nominal-Datatype-part:
 
-1st Arg: string list  
-         ^^^^^^^^^^^
-         strings of the types to be defined
 
-2nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list
+1nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                type(s) to be defined             constructors list
                (ty args, name, syn)              (name, typs, syn)
 
 Binder-Function-part:
 
-3rd Arg: (binding * typ option * mixfix) list 
+2rd Arg: (binding * typ option * mixfix) list 
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^    
             binding function(s)           
               to be defined               
             (name, type, syn)             
 
-4th Arg:  term list 
+3th Arg:  term list 
           ^^^^^^^^^
           the equations of the binding functions
           (Trueprop equations)
@@ -39,13 +36,15 @@
 (* nominal datatype parser *)
 local
   structure P = OuterParse
+
+  fun tuple ((x, y, z), u) = (x, y, z, u)
 in
 
 val _ = OuterKeyword.keyword "bind"
 val anno_typ = Scan.option (P.name --| P.$$$ "::") -- P.typ
 
 (* binding specification *)
-(* should use and_list *)
+(* maybe use and_list *)
 val bind_parser = 
   P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name))
 
@@ -54,8 +53,8 @@
 
 (* datatype parser *)
 val dt_parser =
-  ((P.type_args -- P.binding -- P.opt_infix) >> P.triple1) -- 
-    (P.$$$ "=" |-- P.enum1 "|" ((constr_parser -- bind_parser -- P.opt_mixfix) >> P.triple_swap))
+  (P.type_args -- P.binding -- P.opt_infix >> P.triple1) -- 
+    (P.$$$ "=" |-- P.enum1 "|" (constr_parser -- bind_parser -- P.opt_mixfix >> P.triple_swap)) >> tuple
 
 (* function equation parser *)
 val fun_parser = 
@@ -63,7 +62,7 @@
 
 (* main parser *)
 val main_parser =
-  (P.and_list1 dt_parser) -- fun_parser
+  (P.and_list1 dt_parser) -- fun_parser >> P.triple2
 
 end
 *}
@@ -141,20 +140,22 @@
   val dt_names' = add_raws dt_names
   val dt_full_names = map (Sign.full_bname thy) dt_names 
   val dt_full_names' = map (Sign.full_bname thy) dt_names' 
+  val dt_env = dt_full_names ~~ dt_full_names'
   
   val ctrs_names = map (Sign.full_bname thy) (get_constr_strs dts)
   val ctrs_names' = map (fn (x, y) => (Sign.full_bname_path thy (add_raw x) (add_raw y))) 
     (get_typed_constrs dts)
+  val ctrs_env = ctrs_names ~~ ctrs_names'
 
   val bn_fun_strs = get_bn_fun_strs bn_funs
   val bn_fun_strs' = add_raws bn_fun_strs
+  val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
   
   val bn_funs' = map (fn (bn, opt_ty, mx) => 
     (raw_bind bn, Option.map (replace_typ (dt_full_names ~~ dt_full_names')) opt_ty, mx)) bn_funs
   
   val bn_eqs' = map (fn trm => 
-    (Attrib.empty_binding, 
-      (replace_term ((ctrs_names ~~ ctrs_names') @ (bn_fun_strs ~~ bn_fun_strs')) (dt_full_names ~~ dt_full_names') trm))) bn_eqs
+    (Attrib.empty_binding, replace_term (ctrs_env @ bn_fun_env) dt_env trm)) bn_eqs
 in
   if null bn_eqs 
   then (([], []), lthy)
@@ -174,12 +175,12 @@
 *}
 
 ML {*
-(* makes a full named type out of a binding with tvars applied to it *)
-fun mk_type thy bind tvrs =
-  Type (Sign.full_name thy bind, map (fn s => TVar ((s, 0), [])) tvrs)
-
 fun get_constrs2 thy dts =
 let
+  (* makes a full named type out of a binding with tvars applied to it *)
+  fun mk_type thy bind tvrs =
+    Type (Sign.full_name thy bind, map (fn s => TVar ((s, 0), [])) tvrs)
+
   val dts' = map (fn (tvrs, tname, _, constrs) => (mk_type thy tname tvrs, constrs)) dts
 in
   flat (map (fn (ty, constrs) => map (fn (bn, tys, mx) =>  (bn, tys ---> ty, mx)) constrs) dts')
@@ -187,11 +188,11 @@
 *}
 
 ML {*
-fun nominal_datatype2_cmd (dt_strs, (bn_fun_strs, bn_eq_strs)) lthy =
+fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy =
 let
   val thy = ProofContext.theory_of lthy
 
-  fun prep_typ ((tvs, tname, mx), _) = (tname, length tvs, mx);
+  fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx);
 
   (* adding the types for parsing datatypes *)
   val lthy_tmp = lthy
@@ -200,7 +201,7 @@
   fun prep_cnstr lthy (((cname, atys), mx), binders) =
     (cname, map (Syntax.read_typ lthy o snd) atys, mx)
   
-  fun prep_dt lthy ((tvs, tname, mx), cnstrs) = 
+  fun prep_dt lthy (tvs, tname, mx, cnstrs) = 
     (tvs, tname, mx, map (prep_cnstr lthy) cnstrs)
 
   (* parsing the datatypes *)

--- a/Nominal/Test.thy	Thu Feb 25 12:30:50 2010 +0100
+++ b/Nominal/Test.thy	Thu Feb 25 12:32:15 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