# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264609110 -3600
# Node ID c16135580a45043c0b4b8c75a5e081a71d6a598d
# Parent  cc5d18c784464f6194373163d284636b4e39054b
Some processing of variables in constructors to get free variables.

diff -r cc5d18c78446 -r c16135580a45 Quot/Nominal/Test.thy
--- a/Quot/Nominal/Test.thy	Wed Jan 27 16:40:16 2010 +0100
+++ b/Quot/Nominal/Test.thy	Wed Jan 27 17:18:30 2010 +0100
@@ -103,18 +103,29 @@
 
 (* TODO: replace with proper thing *)
 ML {*
-fun is_atom ty = Binding.name_of ty = "name"
+fun is_atom ty = ty = "name"
 *}
 
+ML {* @{term "A \<union> B"} *}
+
+(* TODO: After variant_frees, check that the new names correspond to the ones given by user *)
 ML {*
-fun fv_constr lthy prefix (((name, anno_tys), bds), syn) =
+fun fv_constr lthy prefix dt_names (((name, anno_tys), bds), syn) =
 let
   fun prepare_name (NONE, ty) = ("", ty)
     | prepare_name (SOME n, ty) = (n, ty);
   val vars = map Free (Variable.variant_frees lthy [] (map prepare_name anno_tys));
   val var_strs = map (Syntax.string_of_term lthy) vars;
+  fun fv_var (t as Free (s, (ty as Type (tyS, _)))) =
+    if is_atom tyS then HOLogic.mk_set ty [t] else
+    if tyS mem dt_names then Free ("fv_" ^ tyS, dummyT) $ t else
+    @{term "{}"}
+  val fv_eq = 
+    if null vars then HOLogic.mk_set @{typ atom} []
+    else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars)
+  val fv_eq_str = Syntax.string_of_term lthy fv_eq
 in
-  prefix ^ " (" ^ (Binding.name_of name) ^ " " ^ (implode (separate " " var_strs)) ^ ") = "
+  prefix ^ " (" ^ (Binding.name_of name) ^ " " ^ (implode (separate " " var_strs)) ^ ") = " ^ fv_eq_str
 end
 *}
 
@@ -130,8 +141,8 @@
 *}
 
 ML {*
-fun fv_dt lthy (((s2, s3), syn), constrs) =
-    map (fv_constr lthy ("fv_" ^ Binding.name_of s3)) constrs
+fun fv_dt lthy dt_names (((s2, s3), syn), constrs) =
+    map (fv_constr lthy ("fv_" ^ Binding.name_of s3) dt_names) constrs
  |> separate "\n"
  |> implode
 *}
@@ -149,12 +160,16 @@
 *}
 
 ML {*
+fun dt_name (((s2, s3), syn), constrs) = Binding.name_of s3
+*}
+
+ML {*
 fun print_dts (dts, (funs, feqs)) lthy =
 let
   val _ = warning (implode (separate "\n" (map (single_dt lthy) dts)));
   val _ = warning (implode (separate "\n" (map single_fun_fix funs)));
   val _ = warning (implode (separate "\n" (map (single_fun_eq lthy) feqs)));
-  val _ = warning (implode (separate "\n" (map (fv_dt lthy) dts)));
+  val _ = warning (implode (separate "\n" (map (fv_dt lthy (map dt_name dts)) dts)));
 in
   lthy
 end