
diff -r 9911824a5396 -r ed89a26b7074 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Sat Mar 27 06:51:13 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 27 08:11:11 2010 +0100
@@ -140,6 +140,19 @@
 *}
 
 ML {*
+fun atyp_const AlphaGen = @{const_name alpha_gen}
+  | atyp_const AlphaRes = @{const_name alpha_res}
+  | atyp_const AlphaLst = @{const_name alpha_lst}
+*}
+
+(* TODO: make sure that parser checks that bindings are compatible *)
+ML {*
+fun alpha_const_for_binds [] = atyp_const AlphaGen
+  | alpha_const_for_binds ((NONE, _, _, at) :: t) = atyp_const at
+  | alpha_const_for_binds ((SOME (_, _), _, _, at) :: _) = atyp_const at
+*}
+
+ML {*
 fun is_atom thy typ =
   Sign.of_sort thy (typ, @{sort at})
 
@@ -167,11 +180,11 @@
 let
   fun gather_binds_cons binds =
     let
-      val common = map (fn (f, bi, _) => (f, bi)) binds
+      val common = map (fn (f, bi, _, aty) => (f, bi, aty)) binds
       val nodups = distinct (op =) common
-      fun find_bodys (sf, sbi) =
-        filter (fn (f, bi, _) => f = sf andalso bi = sbi) binds
-      val bodys = map ((map (fn (_, _, bo) => bo)) o find_bodys) nodups
+      fun find_bodys (sf, sbi, sty) =
+        filter (fn (f, bi, _, aty) => f = sf andalso bi = sbi andalso aty = sty) binds
+      val bodys = map ((map (fn (_, _, bo, _) => bo)) o find_bodys) nodups
     in
       nodups ~~ bodys
     end
@@ -182,11 +195,13 @@
 
 ML {*
 fun un_gather_binds_cons binds =
-  flat (map (fn (((f, bi), bos), pi) => map (fn bo => ((f, bi, bo), pi)) bos) binds)
+  flat (map (fn (((f, bi, aty), bos), pi) => map (fn bo => ((f, bi, bo, aty), pi)) bos) binds)
 *}
 
 ML {*
   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
+*}
+ML {*
   (* TODO: It is the same as one in 'nominal_atoms' *)
   fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom});
   val noatoms = @{term "{} :: atom set"};
@@ -263,7 +278,7 @@
 ML {*
 fun non_rec_binds l =
 let
-  fun is_non_rec (SOME (f, false), _, _) = SOME f
+  fun is_non_rec (SOME (f, false), _, _, _) = SOME f
     | is_non_rec _ = NONE
 in
   distinct (op =) (map_filter is_non_rec (flat (flat l)))
@@ -311,6 +326,7 @@
 end
 *}
 
+ML {* print_depth 100 *}
 ML {*
 fun fv_bns thy dt_info fv_frees rel_bns =
 let
@@ -390,7 +406,7 @@
 (* Checks that a list of bindings contains only compatible ones *)
 ML {*
 fun bns_same l =
-  length (distinct (op =) (map (fn ((b, _, _), _) => b) l)) = 1
+  length (distinct (op =) (map (fn ((b, _, _, atyp), _) => (b, atyp)) l)) = 1
 *}
 
 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
@@ -441,16 +457,16 @@
       val fv_c = nth fv_frees ith_dtyp;
       val alpha = nth alpha_frees ith_dtyp;
       val arg_nos = 0 upto (length dts - 1)
-      fun fv_bind args (NONE, i, _) =
+      fun fv_bind args (NONE, i, _, _) =
             if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
             if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else
             if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atom_set (nth args i) else
             if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (nth args i) else
             (* TODO we do not know what to do with non-atomizable things *)
             @{term "{} :: atom set"}
-        | fv_bind args (SOME (f, _), i, _) = f $ (nth args i);
+        | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i);
       fun fv_binds args relevant = mk_union (map (fv_bind args) relevant)
-      fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE
+      fun find_nonrec_binder j (SOME (f, false), i, _, _) = if i = j then SOME f else NONE
         | find_nonrec_binder _ _ = NONE
       fun fv_arg ((dt, x), arg_no) =
         case get_first (find_nonrec_binder arg_no) bindcs of
@@ -468,7 +484,7 @@
                 (* TODO we do not know what to do with non-atomizable things *)
                 @{term "{} :: atom set"};
               (* If i = j then we generate it only once *)
-              val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs;
+              val relevant = filter (fn (_, i, j, _) => ((i = arg_no) orelse (j = arg_no))) bindcs;
               val sub = fv_binds args relevant
             in
               mk_diff arg sub
@@ -479,13 +495,13 @@
         HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)));
       fun alpha_arg ((dt, arg_no), (arg, arg2)) =
         let
-          val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis;
-          val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis;
-          val rel_has_binds = filter (fn ((NONE, _, j), _) => j = arg_no
-                                       | ((SOME (_, false), _, j), _) => j = arg_no
+          val rel_in_simp_binds = filter (fn ((NONE, i, _, _), _) => i = arg_no | _ => false) bind_pis;
+          val rel_in_comp_binds = filter (fn ((SOME _, i, _, _), _) => i = arg_no | _ => false) bind_pis;
+          val rel_has_binds = filter (fn ((NONE, _, j, _), _) => j = arg_no
+                                       | ((SOME (_, false), _, j, _), _) => j = arg_no
                                        | _ => false) bind_pis;
-          val rel_has_rec_binds = filter 
-            (fn ((SOME (_, true), _, j), _) => j = arg_no | _ => false) bind_pis;
+          val rel_has_rec_binds = filter
+            (fn ((SOME (_, true), _, j, _), _) => j = arg_no | _ => false) bind_pis;
         in
           case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds, rel_has_rec_binds) of
             ([], [], [], []) =>
@@ -493,12 +509,12 @@
               else (HOLogic.mk_eq (arg, arg2))
           | (_, [], [], []) => @{term True}
           | ([], [], [], _) => @{term True}
-          | ([], ((((SOME (bn, is_rec)), _, _), _) :: _), [], []) =>
+          | ([], ((((SOME (bn, is_rec)), _, _, atyp), _) :: _), [], []) =>
             if not (bns_same rel_in_comp_binds) then error "incompatible bindings for an argument" else
             if is_rec then
               let
                 val (rbinds, rpis) = split_list rel_in_comp_binds
-                val bound_in_nos = map (fn (_, _, i) => i) rbinds
+                val bound_in_nos = map (fn (_, _, i, _) => i) rbinds
                 val bound_in_ty_nos = map (fn i => body_index (nth dts i)) bound_in_nos;
                 val bound_args = arg :: map (nth args) bound_in_nos;
                 val bound_args2 = arg2 :: map (nth args2) bound_in_nos;
@@ -513,7 +529,7 @@
                 val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos);
                 val alpha = mk_compound_alpha alphas;
                 val pi = foldr1 add_perm (distinct (op =) rpis);
-                val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
+                val alpha_gen_pre = Const (atyp_const atyp, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
                 val alpha_gen = Syntax.check_term lthy alpha_gen_pre
               in
                 alpha_gen
@@ -535,7 +551,8 @@
               val alpha = nth alpha_frees (body_index dt);
               val fv = nth fv_frees (body_index dt);
               val pi = foldr1 add_perm (distinct (op =) rpis);
-              val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
+              val alpha_const = alpha_const_for_binds rbinds;
+              val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
               val alpha_gen = Syntax.check_term lthy alpha_gen_pre
             in
               alpha_gen




