--- a/Quot/Nominal/Test.thy	Wed Feb 24 09:56:32 2010 +0100
+++ b/Quot/Nominal/Test.thy	Wed Feb 24 17:32:22 2010 +0100
@@ -83,28 +83,23 @@
 (* adds "_raw" to the end of constants and types *)
 ML {*
 fun add_raw s = s ^ "_raw"
+fun add_raws ss = map add_raw ss
 fun raw_bind bn = Binding.suffix_name "_raw" bn
 
-fun raw_str [] s = s
-  | raw_str (s'::ss) s = 
-      if (Long_Name.base_name s) = s' 
-      then add_raw s
-      else raw_str ss s
-
-fun raw_typ ty_strs (Type (a, Ts)) = Type (raw_str ty_strs a, map (raw_typ ty_strs) Ts)
-  | raw_typ ty_strs T = T  
+fun replace_str ss s = 
+  case (AList.lookup (op=) ss s) of 
+     SOME s' => s'
+   | NONE => s
 
-fun raw_aterm trm_strs (Const (a, T)) = Const (raw_str trm_strs a, T)
-  | raw_aterm trm_strs (Free (a, T)) = Free (raw_str trm_strs a, T)
-  | raw_aterm trm_strs trm = trm
- 
-fun raw_term trm_strs ty_strs trm =
-  trm |> Term.map_aterms (raw_aterm trm_strs) |> map_types (raw_typ ty_strs) 
+fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts)
+  | replace_typ ty_ss T = T  
 
-fun raw_dts ty_strs dts =
+fun raw_dts ty_ss dts =
 let
+  val ty_ss' = ty_ss ~~ (add_raws ty_ss)
+
   fun raw_dts_aux1 (bind, tys, mx) =
-    (raw_bind bind, map (raw_typ ty_strs) tys, mx)
+    (raw_bind bind, map (replace_typ ty_ss') tys, mx)
 
   fun raw_dts_aux2 (ty_args, bind, mx, constrs) =
     (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs)
@@ -112,16 +107,25 @@
   map raw_dts_aux2 dts
 end
 
+fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T)
+  | replace_aterm trm_ss (Free (a, T)) = Free (replace_str trm_ss a, T)
+  | replace_aterm trm_ss trm = trm
+
+fun replace_term trm_ss ty_ss trm =
+  trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss) 
+*}
+
+ML {*
 fun get_constrs dts =
-  flat (map (fn (_, _, _, constrs) => map (fn (bn, tys, mx) => (bn, tys, mx)) constrs) dts)
+  flat (map (fn (_, _, _, constrs) => constrs) dts)
+
+fun get_typed_constrs dts =
+  flat (map (fn (_, bn, _, constrs) => 
+   (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts)
 
 fun get_constr_strs dts =
   map (fn (bn, _, _) => Binding.name_of bn) (get_constrs dts)
 
-fun get_constrs2 dts =
-  flat (map (fn (tvrs, tname, _, constrs) => 
-    map (fn (bn, tys, mx) => (bn, tys ---> Type ("Test." ^ Binding.name_of tname, map (fn s => TVar ((s,0),[])) tvrs), mx)) constrs) dts)
-
 fun get_bn_fun_strs bn_funs =
   map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs
 *}
@@ -129,26 +133,44 @@
 ML {*
 fun raw_dts_decl dt_names dts lthy =
 let
+  val thy = ProofContext.theory_of lthy
   val conf = Datatype.default_config
 
-  val dt_names' = map add_raw dt_names
-  val dts' = raw_dts dt_names dts
+  val dt_names' = add_raws dt_names
+  val dt_full_names = map (Sign.full_bname thy) dt_names 
+  val dts' = raw_dts dt_full_names dts
 in
-  Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts') lthy
+  lthy
+  |> Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts')
 end 
 *}
 
 ML {*
-fun raw_bn_fun_decl dt_names cnstr_names bn_funs bn_eqs lthy =
+fun raw_bn_fun_decl dt_names dts bn_funs bn_eqs lthy =
 let
+  val thy = ProofContext.theory_of lthy
+
+  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 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 bn_fun_strs = get_bn_fun_strs bn_funs
+  val bn_fun_strs' = add_raws bn_fun_strs
   
   val bn_funs' = map (fn (bn, opt_ty, mx) => 
-    (raw_bind bn, Option.map (raw_typ dt_names) opt_ty, mx)) bn_funs
+    (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, raw_term (cnstr_names @ bn_fun_strs) dt_names trm)) bn_eqs
+    (Attrib.empty_binding, 
+      (replace_term ((ctrs_names ~~ ctrs_names') @ (bn_fun_strs ~~ bn_fun_strs')) (dt_full_names ~~ dt_full_names') trm))) bn_eqs
 in
-  Primrec.add_primrec bn_funs' bn_eqs' lthy
+  if null bn_eqs 
+  then (([], []), lthy)
+  else Primrec.add_primrec bn_funs' bn_eqs' lthy 
 end 
 *}
 
@@ -156,22 +178,36 @@
 fun nominal_datatype2 dts bn_funs bn_eqs lthy =
 let
   val dts_names = map (fn (_, s, _, _) => Binding.name_of s) dts
-  val ctrs_names = get_constr_strs dts
 in
   lthy
-  |> raw_dts_decl dts_names dts 
-  ||>> raw_bn_fun_decl dts_names ctrs_names bn_funs bn_eqs
+  |> raw_dts_decl dts_names dts
+  ||>> raw_bn_fun_decl dts_names dts bn_funs bn_eqs
 end
 *}
 
+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
+  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')
+end
+*}
 
 ML {*
 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);
+
+  (* adding the types for parsing datatypes *)
   val lthy_tmp = lthy
-    |> Local_Theory.theory
-        (Sign.add_types (map (fn ((tvs, tname, mx), _) =>
-          (tname, length tvs, mx)) dt_strs))
+    |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs))
 
   fun prep_cnstr lthy (((cname, atys), mx), binders) =
     (cname, map (Syntax.read_typ lthy o snd) atys, mx)
@@ -179,21 +215,22 @@
   fun prep_dt lthy ((tvs, tname, mx), cnstrs) = 
     (tvs, tname, mx, map (prep_cnstr lthy) cnstrs)
 
+  (* parsing the datatypes *)
   val dts_prep = map (prep_dt lthy_tmp) dt_strs
 
+  (* adding constructors for parsing functions *)
   val lthy_tmp2 = lthy_tmp
-    |> Local_Theory.theory (Sign.add_consts_i (get_constrs2 dts_prep))
+    |> Local_Theory.theory (Sign.add_consts_i (get_constrs2 thy dts_prep))
+
+  val (bn_fun_aux, bn_eq_aux) = fst (Specification.read_spec bn_fun_strs bn_eq_strs lthy_tmp2)
 
   fun prep_bn_fun ((bn, T), mx) = (bn, SOME T, mx) 
 
   fun prep_bn_eq (attr, t) = t
 
-  val (bn_fun_aux, bn_eq_aux) = fst (Specification.read_spec bn_fun_strs bn_eq_strs lthy_tmp2)
-  
   val bn_fun_prep = map prep_bn_fun bn_fun_aux
   val bn_eq_prep = map prep_bn_eq bn_eq_aux 
 
-  val _ = tracing (cat_lines (map (Syntax.string_of_term lthy_tmp2) bn_eq_prep))
 in
   nominal_datatype2 dts_prep bn_fun_prep bn_eq_prep lthy |> snd
 end
@@ -210,6 +247,7 @@
 *}
 
 text {* example 1 *}
+
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"
@@ -223,7 +261,8 @@
 
 typ lam_raw
 term VAR_raw
-term BP_raw
+term Test.BP_raw
+thm bi_raw.simps
 
 print_theorems
 
@@ -236,29 +275,33 @@
 and pat =
   PN
 | PS "name"
-| PD "name \<times> name"
+| PD "name" "name"
 binder
   f::"pat \<Rightarrow> name set"
 where 
   "f PN = {}"
 | "f (PS x) = {x}"
-| "f (PD (x,y)) = {x,y}"
+| "f (PD x y) = {x,y}"
+
+thm f_raw.simps
 
-nominal_datatype trm2 =
-  Var2 "name"
-| App2 "trm2" "trm2"
-| Lam2 x::"name" t::"trm2"          bind x in t 
-| Let2 p::"pat2" "trm2" t::"trm2"   bind "f2 p" in t
-and pat2 =
-  PN2
-| PS2 "name"
-| PD2 "pat2 \<times> pat2"
+nominal_datatype trm0 =
+  Var0 "name"
+| App0 "trm0" "trm0"
+| Lam0 x::"name" t::"trm0"          bind x in t 
+| Let0 p::"pat0" "trm0" t::"trm0"   bind "f0 p" in t
+and pat0 =
+  PN0
+| PS0 "name"
+| PD0 "pat0" "pat0"
 binder
-  f2::"pat2 \<Rightarrow> name set"
+  f0::"pat0 \<Rightarrow> name set"
 where 
-  "f2 PN2 = {}"
-| "f2 (PS2 x) = {x}"
-| "f2 (PD2 (p1, p2)) = (f2 p1) \<union> (f2 p2)"
+  "f0 PN0 = {}"
+| "f0 (PS0 x) = {x}"
+| "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
+
+thm f0_raw.simps
 
 text {* example type schemes *}
 datatype ty = 
@@ -270,54 +313,132 @@
 
 
 
+(* example 1 from Terms.thy *)
+
+nominal_datatype trm1 =
+  Vr1 "name"
+| Ap1 "trm1" "trm1"
+| Lm1 x::"name" t::"trm1"      bind x in t 
+| Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t 
+and bp1 =
+  BUnit1
+| BV1 "name"
+| BP1 "bp1" "bp1"
+binder
+  bv1
+where
+  "bv1 (BUnit1) = {}"
+| "bv1 (BV1 x) = {atom x}"
+| "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
+
+thm bv1_raw.simps
+
+(* example 2 from Terms.thy *)
+
+nominal_datatype trm2 =
+  Vr2 "name"
+| Ap2 "trm2" "trm2"
+| Lm2 x::"name" t::"trm2"       bind x in t
+| Lt2 r::"rassign" t::"trm2"    bind "bv2 r" in t
+and rassign = 
+  As "name" "trm2"
+binder
+  bv2
+where
+  "bv2 (As x t) = {atom x}"
+
+(* example 3 from Terms.thy *)
+
+nominal_datatype trm3 =
+  Vr3 "name"
+| Ap3 "trm3" "trm3"
+| Lm3 x::"name" t::"trm3"        bind x in t
+| Lt3 r::"rassigns3" t::"trm3"   bind "bv3 r" in t
+and rassigns3 =
+  ANil
+| ACons "name" "trm3" "rassigns3"
+binder
+  bv3
+where
+  "bv3 ANil = {}"
+| "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
+
+(* example 4 from Terms.thy *)
+
+nominal_datatype trm4 =
+  Vr4 "name"
+| Ap4 "trm4" "trm4 list"
+| Lm4 x::"name" t::"trm4"  bind x in t
+
+(* example 5 from Terms.thy *)
+
+nominal_datatype trm5 =
+  Vr5 "name"
+| Ap5 "trm5" "trm5"
+| Lt5 l::"lts" t::"trm5"  bind "bv5 l" in t
+and lts =
+  Lnil
+| Lcons "name" "trm5" "lts"
+binder
+  bv5
+where
+  "bv5 Lnil = {}"
+| "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
+
+(* example 6 from Terms.thy *)
+
+nominal_datatype trm6 =
+  Vr6 "name"
+| Lm6 x::"name" t::"trm6"         bind x in t
+| Lt6 left::"trm6" right::"trm6"  bind "bv6 left" in right
+binder
+  bv6
+where
+  "bv6 (Vr6 n) = {}"
+| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
+| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
+
+(* example 7 from Terms.thy *)
+
+nominal_datatype trm7 =
+  Vr7 "name"
+| Lm7 l::"name" r::"trm7"   bind l in r
+| Lt7 l::"trm7" r::"trm7"   bind "bv7 l" in r
+binder 
+  bv7 
+where
+  "bv7 (Vr7 n) = {atom n}"
+| "bv7 (Lm7 n t) = bv7 t - {atom n}"
+| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
+
+(* example 8 from Terms.thy *)
+
+nominal_datatype foo8 =
+  Foo0 "name"
+| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in foo
+and bar8 =
+  Bar0 "name"
+| Bar1 "name" s::"name" b::"bar8" bind s in b
+binder 
+  bv8
+where
+  "bv8 (Bar0 x) = {}"
+| "bv8 (Bar1 v x b) = {atom v}"
+
+(* example 9 from Terms.thy *)
+
+nominal_datatype lam9 =
+  Var9 "name"
+| Lam9 n::"name" l::"lam9" bind n in l
+and bla9 =
+  Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
+binder
+  bv9
+where
+  "bv9 (Var9 x) = {}"
+| "bv9 (Lam9 x b) = {atom x}"
 
 end
 
 
-(* 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
-*}
-