# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266413706 -3600
# Node ID 9cb99a28b40ee5db8aab06e9108dfe8078bc4de0
# Parent  9a609fefcf24c74b46e3159f7c3124d35a74ac5f
Some optimizations and fixes.

diff -r 9a609fefcf24 -r 9cb99a28b40e Quot/Nominal/Fv.thy
--- a/Quot/Nominal/Fv.thy	Wed Feb 17 14:17:02 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Wed Feb 17 14:35:06 2010 +0100
@@ -36,45 +36,58 @@
 [
  [],
  [[], [], [(NONE, 0)]],
- [[], [], [(SOME (Const f), 0), (Some (Const g), 1, 2)]]]
+ [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]]
 *)
 
+ML foldr1
+ML fold
 ML {*
   val {descr, ...} = Datatype.the_info @{theory} "Fv.rlam";
   val sorts = [];
-  val binds = [[], [[], []], [[], [(NONE, 0)]]];
+  val noatoms = @{term "{} :: atom set"}
+  val binds = [[[]], [[], []], [[], [(NONE, 0)]]];
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
     "fv_" ^ name_of_typ (nth_dtyp i)) descr);
   val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr;
   val fv_frees = map Free (fv_names ~~ fv_types);
-  (* TODO: should be optimized to avoid {}+{}+{} *)
-  fun mk_union sets = foldr1 (HOLogic.mk_binop @{const_name union}) sets;
-
-  fun fv_eq_constr i (cname, dts) bind =
+  fun mk_union sets =
+    fold (fn a => fn b =>
+      if a = noatoms then b else
+      if b = noatoms then a else
+      HOLogic.mk_binop @{const_name union} (a, b)) sets noatoms;
+  fun mk_diff a b =
+    if b = noatoms then a else
+    HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (a, b);
+  fun fv_eq_constr i (cname, dts) bindcs =
     let
       val Ts = map (typ_of_dtyp descr sorts) dts;
       val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
       val args = map Free (names ~~ Ts);
       val c = Const (cname, Ts ---> (nth_dtyp i));
       val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"});
-      fun fv_arg (dt, x) =
+      fun fv_bind (_, i) = @{term "{} :: atom set"}
+      fun fv_arg ((dt, x), bindxs) =
         let
           val arg =
             if is_rec_type dt then nth fv_frees (body_index dt) $ x
             (* TODO: we just assume everything is a 'name' *)
             else HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x]
+          val sub = mk_union (map fv_bind bindxs)
         in
-          arg
-        end
-     in
+          mk_diff arg sub
+        end;
+      val _ = tracing (string_of_int (length dts));
+      val _ = tracing (string_of_int (length bindcs));
+    in
       (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
-        (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args)))))
+        (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs)))))
     end;
   fun fv_eq (i, (_, _, constrs)) = map2 (fv_eq_constr i) constrs binds;
   val fv_eqs = maps fv_eq descr
 *}
 
+
 local_setup {*
 snd o (Primrec.add_primrec
   (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs)