theory Fv

imports "Nominal2_Atoms" "Abs" "Perm" "Rsp" "Nominal2_FSet"

begin

(* The bindings data structure:

  Bindings are a list of lists of lists of triples.

   The first list represents the datatypes defined.

   The second list represents the constructors.

   The internal list is a list of all the bndings that

   concern the constructor.

   Every triple consists of a function, the binding and

   the body.

  Eg:

nominal_datatype

   C1

 | C2 x y z bind x in z

 | C3 x y z bind f x in z bind g y in z

yields:

[

 [],

 [(NONE, 0, 2)],

 [(SOME (Const f), 0, 2), (Some (Const g), 1, 2)]]

A SOME binding has to have a function which takes an appropriate

argument and returns an atom set. A NONE binding has to be on an

argument that is an atom or an atom set.

*)

(*

An overview of the generation of free variables:

1) fv_bn functions are generated only for the non-recursive binds.

   An fv_bn for a constructor is a union of values for the arguments:

   For an argument x that is in the bn function

   - if it is a recursive argument bn' we return: fv_bn' x

   - otherwise empty

   For an argument x that is not in the bn function

   - for atom we return: {atom x}

   - for atom set we return: atom ` x

   - for a recursive call to type ty' we return: fv_ty' x

     with fv of the appropriate type

   - otherwise empty

2) fv_ty functions generated for all types being defined:

   fv_ty for a constructor is a union of values for the arguments.

   For an argument that is bound in a shallow binding we return empty.

   For an argument x that bound in a non-recursive deep binding

   we return: fv_bn x.

   Otherwise we return the free variables of the argument minus the

   bound variables of the argument.

   The free variables for an argument x are:

   - for an atom: {atom x}

   - for atom set: atom ` x

   - for recursive call to type ty' return: fv_ty' x

   - for nominal datatype ty' return: fv_ty' x

   The bound variables are a union of results of all bindings that

   involve the given argument. For a paricular binding:

   - for a binding function bn: bn x

   - for a recursive argument of type ty': fv_fy' x

   - for nominal datatype ty' return: fv_ty' x

*)

(*

An overview of the generation of alpha-equivalence:

1) alpha_bn relations are generated for binding functions.

   An alpha_bn for a constructor is true if a conjunction of

   propositions for each argument holds.

   For an argument a proposition is build as follows from

   th:

   - for a recursive argument in the bn function, we return: alpha_bn argl argr

   - for a recursive argument for type ty not in bn, we return: alpha_ty argl argr

   - for other arguments in the bn function we return: True

   - for other arguments not in the bn function we return: argl = argr

2) alpha_ty relations are generated for all the types being defined:

   For each constructor we gather all the arguments that are bound,

   and for each of those we add a permutation. We associate those

   permutations with the bindings. Note that two bindings can have

   the same permutation if the arguments being bound are the same.

   An alpha_ty for a constructor is true if there exist permutations

   as above such that a conjunction of propositions for all arguments holds.

   For an argument we allow bindings where only one of the following

   holds:

   - Argument is bound in some shallow bindings: We return true

   - Argument of type ty is bound recursively in some other

     arguments [i1, .. in] with one binding function bn.

     We return:

     (bn argl, (argl, argl_i1, ..., argl_in)) \<approx>gen

     \<lambda>(argl,argl1,..,argln) (argr,argr1,..,argrn). 

         (alpha_ty argl argr) \<and> (alpha_i1 argl1 argr1) \<and> .. \<and> (alpha_in argln argrn)

     \<lambda>(arg,arg1,..,argn). (fv_ty arg) \<union> (fv_i1 arg1) \<union> .. \<union> (fv_in argn)

     pi

     (bn argr, (argr, argr_i1, ..., argr_in))

   - Argument is bound in some deep non-recursive bindings.

     We return: alpha_bn argl argr

   - Argument of type ty has some shallow bindings [b1..bn] and/or

     non-recursive bindings [f1 a1, .., fm am], where the bindings

     have the permutations p1..pl. We return:

     (b1l \<union>..\<union> bnl \<union> f1 a1l \<union>..\<union> fn anl, argl) \<approx>gen

     alpha_ty fv_ty (p1 +..+ pl)

     (b1r \<union>..\<union> bnr \<union> f1 a1r \<union>..\<union> fn anr, argr)

   - Argument has some recursive bindings. The bindings were

     already treated in 2nd case so we return: True

   - Argument has no bindings and is not bound.

     If it is recursive for type ty, we return: alpha_ty argl argr

     Otherwise we return: argl = argr

*)

ML {*

fun is_atom thy typ =

  Sign.of_sort thy (typ, @{sort at})

fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t

  | is_atom_set thy _ = false;

fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t

  | is_atom_fset thy _ = false;

val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"}

*}

(* Like map2, only if the second list is empty passes empty lists insted of error *)

ML {*

fun map2i _ [] [] = []

  | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys

  | map2i f (x :: xs) [] = f x [] :: map2i f xs []

  | map2i _ _ _ = raise UnequalLengths;

*}

(* Finds bindings with the same function and binding, and gathers all

   bodys for such pairs

 *)

ML {*

fun gather_binds binds =

let

  fun gather_binds_cons binds =

    let

      val common = map (fn (f, bi, _) => (f, bi)) 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

    in

      nodups ~~ bodys

    end

in

  map (map gather_binds_cons) binds

end

*}

ML {*

fun un_gather_binds_cons binds =

  flat (map (fn (((f, bi), bos), pi) => map (fn bo => ((f, bi, bo), pi)) bos) binds)

*}

ML {*

  open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);

  (* 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"};

  fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x];

  fun mk_union sets =

    fold (fn a => fn b =>

      if a = noatoms then b else

      if b = noatoms then a else

      if a = b then a else

      HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;

  val mk_inter = foldr1 (HOLogic.mk_binop @{const_name inf})

  fun mk_conjl props =

    fold (fn a => fn b =>

      if a = @{term True} then b else

      if b = @{term True} then a else

      HOLogic.mk_conj (a, b)) (rev props) @{term True};

  fun mk_diff a b =

    if b = noatoms then a else

    if b = a then noatoms else

    HOLogic.mk_binop @{const_name minus} (a, b);

  fun mk_atom_set t =

    let

      val ty = fastype_of t;

      val atom_ty = HOLogic.dest_setT ty --> @{typ atom};

      val img_ty = atom_ty --> ty --> @{typ "atom set"};

    in

      (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t)

    end;

  fun mk_atom_fset t =

    let

      val ty = fastype_of t;

      val atom_ty = dest_fsetT ty --> @{typ atom};

      val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};

    in

      fset_to_set $ ((Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t))

    end;

  (* Similar to one in USyntax *)

  fun mk_pair (fst, snd) =

    let val ty1 = fastype_of fst

      val ty2 = fastype_of snd

      val c = HOLogic.pair_const ty1 ty2

    in c $ fst $ snd

    end;

*}

(* Given [fv1, fv2, fv3] creates %(x, y, z). fv1 x u fv2 y u fv3 z *)

ML {*

fun mk_compound_fv fvs =

let

  val nos = (length fvs - 1) downto 0;

  val fvs_applied = map (fn (fv, no) => fv $ Bound no) (fvs ~~ nos);

  val fvs_union = mk_union fvs_applied;

  val (tyh :: tys) = rev (map (domain_type o fastype_of) fvs);

  fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))

in

  fold fold_fun tys (Abs ("", tyh, fvs_union))

end;

*}

ML {* @{term "\<lambda>(x, y, z). \<lambda>(x', y', z'). R x x' \<and> R2 y y' \<and> R3 z z'"} *}

(* Given [R1, R2, R3] creates %(x,x'). %(y,y'). %(z,z'). R x x' \<and> R y y' \<and> R z z' *)

ML {*

fun mk_compound_alpha Rs =

let

  val nos = (length Rs - 1) downto 0;

  val nos2 = (2 * length Rs - 1) downto length Rs;

  val Rs_applied = map (fn (R, (no2, no)) => R $ Bound no2 $ Bound no) (Rs ~~ (nos2 ~~ nos));

  val Rs_conj = mk_conjl Rs_applied;

  val (tyh :: tys) = rev (map (domain_type o fastype_of) Rs);

  fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))

  val abs_rhs = fold fold_fun tys (Abs ("", tyh, Rs_conj))

in

  fold fold_fun tys (Abs ("", tyh, abs_rhs))

end;

*}

ML {* cterm_of @{theory} (mk_compound_alpha [@{term "R :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}, @{term "R2 :: 'b \<Rightarrow> 'b \<Rightarrow> bool"}, @{term "R3 :: 'b \<Rightarrow> 'b \<Rightarrow> bool"}]) *}

ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *}

ML {*

fun non_rec_binds l =

let

  fun is_non_rec (SOME (f, false), _, _) = SOME f

    | is_non_rec _ = NONE

in

  distinct (op =) (map_filter is_non_rec (flat (flat l)))

end

*}

(* We assume no bindings in the type on which bn is defined *)

(* TODO: currently works only with current fv_bn function *)

ML {*

fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bns) =

let

  val {descr, sorts, ...} = dt_info;

  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);

  val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));

  val fvbn = Free (fvbn_name, fastype_of (nth fv_frees ith_dtyp));

  fun fv_bn_constr (cname, dts) args_in_bn =

  let

    val Ts = map (typ_of_dtyp descr sorts) dts;

    val names = Datatype_Prop.make_tnames Ts;

    val args = map Free (names ~~ Ts);

    val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));

    fun fv_arg ((dt, x), arg_no) =

      let

        val ty = fastype_of x

      in

        if arg_no mem args_in_bn then 

          (if is_rec_type dt then

            (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: recursive argument, but wrong datatype.")

          else @{term "{} :: atom set"}) else

        if is_atom thy ty then mk_single_atom x else

        if is_atom_set thy ty then mk_atom_set x else

        if is_atom_fset thy ty then mk_atom_fset x else

        if is_rec_type dt then nth fv_frees (body_index dt) $ x else

        @{term "{} :: atom set"}

      end;

    val arg_nos = 0 upto (length dts - 1)

  in

    HOLogic.mk_Trueprop (HOLogic.mk_eq

      (fvbn $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos))))

  end;

  val (_, (_, _, constrs)) = nth descr ith_dtyp;

  val eqs = map2i fv_bn_constr constrs args_in_bns

in

  ((bn, fvbn), (fvbn_name, eqs))

end

*}

ML {*

fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees ((bn, ith_dtyp, args_in_bns), is_rec) =

let

  val {descr, sorts, ...} = dt_info;

  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);

  val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));

  val alpha_bn_type = 

    (*if is_rec then @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} else*)

    nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool};

  val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type);

  val pi = Free("pi", @{typ perm})

  fun alpha_bn_constr (cname, dts) args_in_bn =

  let

    val Ts = map (typ_of_dtyp descr sorts) dts;

    val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);

    val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);

    val args = map Free (names ~~ Ts);

    val args2 = map Free (names2 ~~ Ts);

    val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));

    val rhs = HOLogic.mk_Trueprop

      (alpha_bn_free $ (list_comb (c, args)) $ (list_comb (c, args2)));

    fun lhs_arg ((dt, arg_no), (arg, arg2)) =

      let

        val argty = fastype_of arg;

        val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty);

      in

      if is_rec_type dt then

        if arg_no mem args_in_bn then alpha_bn_free $ arg $ arg2

        else (nth alpha_frees (body_index dt)) $ arg $ arg2

      else

        if arg_no mem args_in_bn then @{term True}

        else HOLogic.mk_eq (arg, arg2)

      end

    val arg_nos = 0 upto (length dts - 1)

    val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2)))

    val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs)

  in

    eq

  end

  val (_, (_, _, constrs)) = nth descr ith_dtyp;

  val eqs = map2i alpha_bn_constr constrs args_in_bns

in

  ((bn, alpha_bn_free), (alpha_bn_name, eqs))

end

*}

(* Checks that a list of bindings contains only compatible ones *)

ML {*

fun bns_same l =

  length (distinct (op =) (map (fn ((b, _, _), _) => b) l)) = 1

*}

(* TODO: Notice datatypes without bindings and replace alpha with equality *)

ML {*

fun define_fv_alpha (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);

  val nr_bns = non_rec_binds bindsall;

  val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns;

  val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns);

  val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs;

  val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>

    "alpha_" ^ name_of_typ (nth_dtyp i)) descr);

  val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;

  val alpha_frees = map Free (alpha_names ~~ alpha_types);

  (* We assume that a bn is either recursive or not *)

  val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns;

  val (bn_alpha_bns, alpha_bn_names_eqs) = split_list (map (alpha_bn thy dt_info alpha_frees) (bns ~~ bns_rec))

  val (alpha_bn_names, alpha_bn_eqs) = split_list alpha_bn_names_eqs;

  val alpha_bn_frees = map snd bn_alpha_bns;

  val alpha_bn_types = map fastype_of alpha_bn_frees;

  fun fv_alpha_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 names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts);

      val args2 = map Free (names2 ~~ Ts);

      val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));

      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, _) =

            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);

      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

        | 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 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 sub = fv_binds 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))))

      val alpha_rhs =

        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

                                       | _ => 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

            ([], [], [], []) =>

              if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)

              else (HOLogic.mk_eq (arg, arg2))

          | (_, [], [], []) => @{term True}

          | ([], [], [], _) => @{term True}

          | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), [], []) =>

            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_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;

                fun bound_in args (_, _, i) = nth args i;

                val lhs_binds = fv_binds args rbinds

                val lhs_arg = foldr1 HOLogic.mk_prod bound_args

                val lhs = mk_pair (lhs_binds, lhs_arg);

                val rhs_binds = fv_binds args2 rbinds;

                val rhs_arg = foldr1 HOLogic.mk_prod bound_args2;

                val rhs = mk_pair (rhs_binds, rhs_arg);

                val fvs = map (nth fv_frees) ((body_index dt) :: bound_in_ty_nos);

                val fv = mk_compound_fv fvs;