# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266412622 -3600
# Node ID 9a609fefcf24c74b46e3159f7c3124d35a74ac5f
# Parent  62632eec979c6fae723eb5b70f1d6a1f8091a3a5
Simplified format of bindings.

diff -r 62632eec979c -r 9a609fefcf24 Quot/Nominal/Fv.thy
--- a/Quot/Nominal/Fv.thy	Wed Feb 17 13:56:31 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Wed Feb 17 14:17:02 2010 +0100
@@ -17,26 +17,32 @@
 ML {* dest_Type @{typ rlam} *}
 
 (* Bindings are given as a list which has a length being equal
-   to the length of the number of constructors. Each element
-   is a specification of all the bindings n this constructor.
-   The bindings are given as triples: function, bound argument,
-   and the argument in which it is bound.
+   to the length of the number of constructors.
+
+   Each element is a list whose length is equal to the number
+   of arguents.
+
+   Every element specifies bindings of this argument given as
+   a tuple: function, bound argument.
 
   Eg:
 nominal_datatype
 
    C1
  | C2 x y z bind x in z
- | C3 x y z bind f x in y bind g y in z
+ | C3 x y z bind f x in z bind g y in z
 
 yields:
-[[], [(NONE, 0, 2)], [(SOME (Const f), 0, 1), (Some (Const g), 1, 2)]]
+[
+ [],
+ [[], [], [(NONE, 0)]],
+ [[], [], [(SOME (Const f), 0), (Some (Const g), 1, 2)]]]
 *)
 
 ML {*
   val {descr, ...} = Datatype.the_info @{theory} "Fv.rlam";
   val sorts = [];
-
+  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);
@@ -45,7 +51,7 @@
   (* 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) =
+  fun fv_eq_constr i (cname, dts) bind =
     let
       val Ts = map (typ_of_dtyp descr sorts) dts;
       val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
@@ -53,15 +59,19 @@
       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) =
-        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]
+        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]
+        in
+          arg
+        end
      in
       (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
         (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args)))))
     end;
-  fun fv_eq (i, (_, _, constrs)) = map (fv_eq_constr i) constrs;
+  fun fv_eq (i, (_, _, constrs)) = map2 (fv_eq_constr i) constrs binds;
   val fv_eqs = maps fv_eq descr
 *}