
diff -r 20f76fde8ef1 -r c179ad9d2446 Quot/Nominal/Test.thy
--- a/Quot/Nominal/Test.thy	Tue Feb 23 13:33:01 2010 +0100
+++ b/Quot/Nominal/Test.thy	Tue Feb 23 16:31:40 2010 +0100
@@ -75,7 +75,7 @@
 
 (* main parser *)
 val main_parser =
-  P.and_list1 dt_parser -- fun_parser
+  (P.and_list1 dt_parser) -- fun_parser
 
 end
 *}
@@ -120,154 +120,68 @@
 *}
 
 ML {*
-fun nominal_dt_decl dt_names dts bn_funs bn_eqs lthy =
+fun raw_dts_decl dt_names dts lthy =
 let
   val conf = Datatype.default_config
-  
+
   val dt_names' = map add_raw dt_names
   val dts' = raw_dts dt_names dts
-  val constr_strs = get_constr_strs dts
+in
+  Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts') lthy
+end 
+*}
+
+ML {*
+fun raw_bn_fun_decl dt_names cnstr_names bn_funs bn_eqs lthy =
+let
   val bn_fun_strs = get_bn_fun_strs bn_funs
   
   val bn_funs' = map (fn (bn, opt_ty, mx) => 
     (raw_bind bn, Option.map (raw_typ dt_names) opt_ty, mx)) bn_funs
   val bn_eqs' = map (fn trm => 
-    (Attrib.empty_binding, raw_term (constr_strs @ bn_fun_strs) dt_names trm)) bn_eqs
+    (Attrib.empty_binding, raw_term (cnstr_names @ bn_fun_strs) dt_names trm)) bn_eqs
 in
-  lthy
-  |> (Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts'))
-  ||>> Primrec.add_primrec bn_funs' bn_eqs'
+  (*Primrec.add_primrec bn_funs' bn_eqs' lthy*)
+  ((), lthy)
 end 
 *}
 
-local_setup {*
+ML {* 
+fun nominal_datatype2 dts bn_funs bn_eqs lthy =
 let
-  val T0 = Type ("Test.foo", [])
-  val T1 = T0 --> @{typ "nat"}
+  val dts_names = map (fn (_, s, _, _) => Binding.name_of s) dts
+  val ctrs_names = get_constr_strs dts
 in
-nominal_dt_decl
-  ["foo"]
-  [([], @{binding "foo"}, NoSyn, 
-    [(@{binding "myzero"}, [], NoSyn),(@{binding "mysuc"}, [Type ("Test.foo", [])], NoSyn)])]
-  [(@{binding "Bar"}, SOME T1, NoSyn)]
-  [HOLogic.mk_Trueprop (HOLogic.mk_eq 
-        (Free ("Bar", T1) $ Const ("Test.foo_raw.myzero", T0), @{term "0::nat"})),
-   HOLogic.mk_Trueprop (HOLogic.mk_eq 
-        (Free ("Bar", T1) $ (Const ("Test.foo_raw.mysuc", T0 --> T0) $ Free ("n", T0)), @{term "0::nat"}))]
-  #> snd
-end
-*}
-
-typ foo_raw
-thm foo_raw.induct
-term myzero_raw
-term mysuc_raw
-thm Bar_raw.simps
-
-(* printing stuff *)
-
-ML {*
-fun print_str_option NONE = "NONE"
-  | print_str_option (SOME s) = (s:bstring)
-
-fun print_anno_typ lthy (NONE, ty) = Syntax.string_of_typ lthy ty
-  | print_anno_typ lthy (SOME x, ty) = x ^ ":" ^ Syntax.string_of_typ lthy ty
-
-fun print_bind (s1, s2) = "bind " ^ s1 ^ " in " ^ s2
-
-fun print_constr lthy (((name, anno_tys), bds), syn) =
-  (Binding.name_of name ^ " of " ^ (commas (map (print_anno_typ lthy) anno_tys)) ^ "   "
-   ^ (commas (map print_bind bds)) ^ "  "
-   ^ (Pretty.str_of (Syntax.pretty_mixfix syn)))
-
-fun print_single_dt lthy (((s2, s3), syn), constrs) =
-   ["constructor declaration"]
- @ ["type arguments: "] @ s2 
- @ ["datatype name: ", Binding.name_of s3] 
- @ ["typ mixfix: ", Pretty.string_of (Syntax.pretty_mixfix syn)]
- @ ["constructors: "] @ (map (print_constr lthy) constrs)
- |> separate "\n"
- |> implode
-
-fun print_single_fun_eq lthy (at, s) = 
-  ["function equations: ", (Syntax.string_of_term lthy s)] 
-  |> separate "\n"
-  |> implode
-
-fun print_single_fun_fix lthy (b, _, _) = 
-  ["functions: ", Binding.name_of b] 
-  |> separate "\n"
-  |> implode
-
-fun dt_name (((s2, s3), syn), constrs) = Binding.name_of s3
-
-fun print_dts (dts, (funs, feqs)) lthy =
-let
-  val _ = warning (implode (separate "\n" (map (print_single_dt lthy) dts)));
-  val _ = warning (implode (separate "\n" (map (print_single_fun_fix lthy) funs)));
-  val _ = warning (implode (separate "\n" (map (print_single_fun_eq lthy) feqs)));
-in
-  ()
+  lthy
+  |> raw_dts_decl dts_names dts 
+  ||>> raw_bn_fun_decl dts_names ctrs_names bn_funs bn_eqs
 end
 *}
 
 ML {*
-fun transp_ty_arg (anno, ty) = ty
-
-fun transp_constr (((constr_name, ty_args), bind), mx) = 
-  (constr_name, map transp_ty_arg ty_args, mx)
-
-fun transp_dt (((ty_args, ty_name), mx), constrs) = 
- (ty_args, ty_name, mx, map transp_constr constrs)
-*}
-
-ML {*
-fun dt_defn dts thy =
+fun nominal_datatype2_cmd (dt_strs, (bn_fun_strs, bn_eq_strs)) lthy =
 let
-  val names = map (fn (_, s, _, _) => Binding.name_of s) dts
-  val thy' = Datatype.datatype_cmd names dts thy
-in
-  thy'
-end
-*}
-
-ML {*
-fun fn_defn [] [] lthy = lthy
-  | fn_defn funs feqs lthy =
-      Function_Fun.add_fun Function_Common.default_config funs feqs false lthy
+  val lthy_tmp = lthy
+    |> (Local_Theory.theory
+        (Sign.add_types (map (fn ((tvs, tname, mx), _) =>
+          (tname, length tvs, mx)) dt_strs)))
 
-fun fn_defn_cmd [] [] lthy = lthy
-  | fn_defn_cmd funs feqs lthy =
-      Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy
-*}
-
-ML {*
-fun parse_fun lthy (b, NONE, m) = (b, NONE, m)
-  | parse_fun lthy (b, SOME ty, m) = (b, SOME (Syntax.read_typ lthy ty), m)
-
-fun parse_feq lthy (b, t) = (b, Syntax.read_prop lthy t);
-
-fun parse_anno_ty lthy (anno, ty) = (anno, Syntax.read_typ lthy ty);
-
-fun parse_constr lthy (((constr_name, ty_args), bind), mx) =
-  (((constr_name, map (parse_anno_ty lthy) ty_args), bind), mx);
+  fun prep_cnstr lthy (((cname, atys), mx), binders) =
+    (cname, map (Syntax.read_typ lthy o snd) atys, mx)
   
-fun parse_dt lthy (((ty_args, ty_name), mx), constrs) =
-   (((ty_args, ty_name), mx), map (parse_constr lthy) constrs);
-*}
+  fun prep_dt lthy ((tvs, tname, mx), cnstrs) = 
+    (tvs, tname, mx, map (prep_cnstr lthy) cnstrs)
+
+  fun prep_bn_fun lthy (bn, ty_str, mx) =
+    (bn, Option.map (Syntax.read_typ lthy) ty_str, mx) 
 
-ML {*
-fun nominal_datatype2_cmd (dt_strs, (fun_strs, feq_strs)) thy =
-let
-  val thy' = dt_defn (map transp_dt dt_strs) thy
-  val lthy = Theory_Target.init NONE thy'
-  val lthy' = fn_defn_cmd fun_strs feq_strs lthy
-  val funs = map (parse_fun lthy') fun_strs
-  val feqs = map (parse_feq lthy') feq_strs
-  val dts = map (parse_dt lthy') dt_strs
-  val _ = print_dts (dts, (funs, feqs)) lthy'
+  fun prep_bn_eq lthy (attr, trm_str) = Syntax.read_term lthy trm_str
+
+  val dts_prep = map (prep_dt lthy_tmp) dt_strs
+  val bn_fun_prep = map (prep_bn_fun lthy_tmp) bn_fun_strs
+  val bn_eq_prep = map (prep_bn_eq lthy_tmp) bn_eq_strs
 in
-  Local_Theory.exit_global lthy'
+  nominal_datatype2 dts_prep bn_fun_prep [] lthy |> snd
 end
 *}
 
@@ -276,8 +190,8 @@
 let
    val kind = OuterKeyword.thy_decl
 in
-   OuterSyntax.command "nominal_datatype" "test" kind 
-     (parser >> (Toplevel.theory o nominal_datatype2_cmd))
+   OuterSyntax.local_theory "nominal_datatype" "test" kind 
+     (main_parser >> nominal_datatype2_cmd)
 end
 *}
 
@@ -292,6 +206,11 @@
   bi::"bp \<Rightarrow> name set"
 where
   "bi (BP x t) = {x}"
+
+typ lam_raw
+term VAR_raw
+term BP_raw
+
 print_theorems
 
 text {* examples 2 *}
@@ -341,5 +260,50 @@
 end
 
 
-(* probably can be done with a clever morphism trick *)
+(* printing stuff *)
+
+ML {*
+fun print_str_option NONE = "NONE"
+  | print_str_option (SOME s) = (s:bstring)
+
+fun print_anno_typ lthy (NONE, ty) = Syntax.string_of_typ lthy ty
+  | print_anno_typ lthy (SOME x, ty) = x ^ ":" ^ Syntax.string_of_typ lthy ty
+
+fun print_bind (s1, s2) = "bind " ^ s1 ^ " in " ^ s2
+
+fun print_constr lthy (((name, anno_tys), bds), syn) =
+  (Binding.name_of name ^ " of " ^ (commas (map (print_anno_typ lthy) anno_tys)) ^ "   "
+   ^ (commas (map print_bind bds)) ^ "  "
+   ^ (Pretty.str_of (Syntax.pretty_mixfix syn)))
 
+fun print_single_dt lthy (((s2, s3), syn), constrs) =
+   ["constructor declaration"]
+ @ ["type arguments: "] @ s2 
+ @ ["datatype name: ", Binding.name_of s3] 
+ @ ["typ mixfix: ", Pretty.string_of (Syntax.pretty_mixfix syn)]
+ @ ["constructors: "] @ (map (print_constr lthy) constrs)
+ |> separate "\n"
+ |> implode
+
+fun print_single_fun_eq lthy (at, s) = 
+  ["function equations: ", (Syntax.string_of_term lthy s)] 
+  |> separate "\n"
+  |> implode
+
+fun print_single_fun_fix lthy (b, _, _) = 
+  ["functions: ", Binding.name_of b] 
+  |> separate "\n"
+  |> implode
+
+fun dt_name (((s2, s3), syn), constrs) = Binding.name_of s3
+
+fun print_dts (dts, (funs, feqs)) lthy =
+let
+  val _ = warning (implode (separate "\n" (map (print_single_dt lthy) dts)));
+  val _ = warning (implode (separate "\n" (map (print_single_fun_fix lthy) funs)));
+  val _ = warning (implode (separate "\n" (map (print_single_fun_eq lthy) feqs)));
+in
+  ()
+end
+*}
+




