# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271235011 -7200
# Node ID 41054d1eb6f0a49359e56b0e69bb0aa7b2d8dacf
# Parent  8db45a1065699b20ee243762eecf88662b65518a
Separate define_fv.

diff -r 8db45a106569 -r 41054d1eb6f0 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Wed Apr 14 10:39:03 2010 +0200
+++ b/Nominal/Fv.thy	Wed Apr 14 10:50:11 2010 +0200
@@ -416,6 +416,103 @@
 *}
 
 ML {*
+fun define_fv (dt_info : Datatype_Aux.info) bindsall bns lthy =
+let
+  val thy = ProofContext.theory_of lthy;
+  val {descr, sorts, ...} = dt_info;
+  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: We need a transitive closure, but instead we do this hack considering
+   all binding functions as recursive or not *)
+  val nr_bns =
+    if (non_rec_binds bindsall) = [] then []
+    else map (fn (bn, _, _) => bn) bns;
+  val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns;
+  val (bn_fv_bns, fv_bn_names_eqs) = fv_bns thy dt_info fv_frees rel_bns;
+  val fvbns = map snd bn_fv_bns;
+  val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs;
+
+  fun fv_constr ith_dtyp (cname, dts) bindcs =
+    let
+      val Ts = map (typ_of_dtyp descr sorts) dts;
+      val bindslen = length bindcs
+      val pi_strs_same = replicate bindslen "pi"
+      val pi_strs = Name.variant_list [] pi_strs_same;
+      val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs;
+      val bind_pis_gath = bindcs ~~ pis;
+      val bind_pis = un_gather_binds_cons bind_pis_gath;
+      val bindcs = map fst bind_pis;
+      val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts);
+      val args = map Free (names ~~ Ts);
+      val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
+      val fv_c = nth fv_frees ith_dtyp;
+      val arg_nos = 0 upto (length dts - 1)
+      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 goes the code for preiously defined nominal datatypes *)
+            @{term "{} :: atom set"}
+        | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i)
+      fun fv_binds_as_set args relevant = mk_union (map (setify o fv_bind args) relevant)
+      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
+          SOME f =>
+            (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of
+                SOME fv_bn => fv_bn $ x
+              | NONE => error "bn specified in a non-rec binding but not in bn list")
+        | NONE =>
+            let
+              val arg =
+                if is_rec_type dt then nth fv_frees (body_index dt) $ x else
+                if ((is_atom thy) o fastype_of) x then mk_single_atom x else
+                if ((is_atom_set thy) o fastype_of) x then mk_atom_set x else
+                if ((is_atom_fset thy) o fastype_of) x then mk_atom_fset x else
+                (* TODO goes the code for preiously defined nominal datatypes *)
+                @{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 sub = fv_binds_as_set args relevant
+            in
+              mk_diff arg sub
+            end;
+      val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq
+        (fv_c $ list_comb (c, args), mk_union (map fv_arg  (dts ~~ args ~~ arg_nos))))
+    in
+      fv_eq
+    end;
+  fun fv_eq (i, (_, _, constrs)) binds = map2i (fv_constr i) constrs binds;
+  val fveqs = map2i fv_eq descr (gather_binds bindsall)
+  val fv_eqs_perfv = fveqs
+  val rel_bns_nos = map (fn (_, i, _) => i) rel_bns;
+  fun filter_fun (_, b) = b mem rel_bns_nos;
+  val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1))
+  val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs)))
+  val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs)))
+  val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs);
+  val fv_names_all = fv_names_fst @ fv_bn_names;
+  val add_binds = map (fn x => (Attrib.empty_binding, x))
+(* Function_Fun.add_fun Function_Common.default_config ... true *)
+  val (fvs, lthy') = (Primrec.add_primrec
+    (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy)
+  val (fvs2, lthy'') =
+    if fv_eqs_snd = [] then (([], []), lthy') else
+   (Primrec.add_primrec
+    (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_snd) (add_binds fv_eqs_snd) lthy')
+  val ordered_fvs = fv_frees @ fvbns;
+  val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2)
+in
+  ((all_fvs, ordered_fvs), lthy'')
+end
+*}
+
+ML {*
 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy =
 let
   val thy = ProofContext.theory_of lthy;