theory NewFv
imports "../Nominal-General/Nominal2_Atoms" 
        "Abs" "Perm" "Rsp" "Nominal2_FSet"
begin

ML {*
datatype bmodes =
   BEmy of int
|  BLst of ((term option * int) list) * (int list)
|  BSet of ((term option * int) list) * (int list)
|  BRes of ((term option * int) list) * (int list)
*}

ML {*
fun mk_singleton_atom x = HOLogic.mk_set @{typ atom} [mk_atom x];

val noatoms = @{term "{} :: atom set"};

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

ML {*
fun is_atom thy ty =
  Sign.of_sort thy (ty, @{sort at})

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

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

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) $ mk_atom_ty 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"};
  val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"}
in
  fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ mk_atom_ty atom_ty t)
end;

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

ML {*
fun atoms thy t =
let
  val ty = fastype_of t;
in
  if is_atom thy ty 
    then mk_singleton_atom t 
  else if is_atom_set thy ty 
    then mk_atom_set t 
  else if is_atom_fset thy ty 
    then mk_atom_fset t 
  else noatoms
end
*}

ML {*
fun setify x =
  if fastype_of x = @{typ "atom list"} 
    then @{term "set::atom list \<Rightarrow> atom set"} $ x 
    else x
*}

ML {*
fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =
let
  fun fv_body i =
    let
      val x = nth args i;
      val dt = nth dts i;
    in
      if Datatype_Aux.is_rec_type dt 
      then nth fv_frees (Datatype_Aux.body_index dt) $ x 
      else atoms thy x
    end
  val fv_bodys = mk_union (map fv_body bodys)
  val bound_vars =
    case binds of
      [(SOME bn, i)] => setify (bn $ nth args i)
    | _ => mk_union (map fv_body (map snd binds));
  val non_rec_vars =
    case binds of
      [(SOME bn, i)] =>
        if i mem bodys
        then ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)
        else noatoms
    | _ => noatoms
in
  mk_union [mk_diff fv_bodys bound_vars, non_rec_vars]
end
*}

ML {*
fun fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn bm =
case bm of
  BEmy i =>
    let
      val x = nth args i;
      val dt = nth dts i;
    in
      case AList.lookup (op=) args_in_bn i of
        NONE => if Datatype_Aux.is_rec_type dt 
                then nth fv_frees (Datatype_Aux.body_index dt) $ x 
                else atoms thy x
      | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x
      | SOME NONE => noatoms
    end
| BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
| BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
| BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
*}

ML {*
fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees
  bn_fvbn bmll (fvbn, (_, ith_dtyp, args_in_bns)) =
let
  val {descr, sorts, ...} = dt_info;
  fun fv_bn_constr (cname, dts) (args_in_bn, bml) =
  let
    val Ts = map (Datatype_Aux.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 descr sorts ith_dtyp));
    val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn
  in
    HOLogic.mk_Trueprop (HOLogic.mk_eq
      (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bml)))
  end;
  val (_, (_, _, constrs)) = nth descr ith_dtyp;
in
  map2 fv_bn_constr constrs (args_in_bns ~~ bmll)
end
*}

ML {*
fun fv_bns thy dt_info fv_frees bn_funs bclauses =
let
  fun mk_fvbn_free (bn, ith, _) =
    let
      val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));
    in
      (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith)))
    end;
  val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs);
  val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees
  val bmlls = map (fn (_, i, _) => nth bclauses i) bn_funs;
  val eqs = map2 (fv_bn thy dt_info fv_frees bn_fvbn) bmlls (fvbn_frees ~~ bn_funs);
in
  (bn_fvbn, fvbn_names, eqs)
end
*}

ML {*
fun fv_bm thy dts args fv_frees bn_fvbn bm =
case bm of
  BEmy i =>
    let
      val x = nth args i;
      val dt = nth dts i;
    in
      if Datatype_Aux.is_rec_type dt 
      then nth fv_frees (Datatype_Aux.body_index dt) $ x 
      else atoms thy x
    end
| BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
| BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
| BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
*}

ML {*
fun fv thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn bmll (fv_free, ith_dtyp) =
let
  val {descr, sorts, ...} = dt_info;
  fun fv_constr (cname, dts) bml =
  let
    val Ts = map (Datatype_Aux.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 descr sorts ith_dtyp));
    val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn
  in
    HOLogic.mk_Trueprop (HOLogic.mk_eq
      (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bml)))
  end;
  val (_, (_, _, constrs)) = nth descr ith_dtyp;
in
  map2 fv_constr constrs bmll
end
*}

ML {*
val by_pat_completeness_auto =
  Proof.global_terminal_proof
    (Method.Basic Pat_Completeness.pat_completeness,
     SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))

fun termination_by method =
  Function.termination_proof NONE
  #> Proof.global_terminal_proof (Method.Basic method, NONE)
*}

ML {*
fun define_raw_fv dt_info bn_funs bclauses lthy =
let
  val thy = ProofContext.theory_of lthy;
  val {descr as dt_descr, sorts, ...} = dt_info;

  val fv_names = prefix_dt_names dt_descr sorts "fv_"
  val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) dt_descr;
  val fv_frees = map Free (fv_names ~~ fv_types);

  val (bn_fvbn, fv_bn_names, fv_bn_eqs) = 
    fv_bns thy dt_info fv_frees bn_funs bclauses;

  val fvbns = map snd bn_fvbn;
  val fv_nums = 0 upto (length fv_frees - 1)

  val fv_eqs = map2 (fv thy dt_info fv_frees bn_fvbn) bclauses (fv_frees ~~ fv_nums);
  val fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
  val fv_eqs_binds = map (fn x => (Attrib.empty_binding, x)) (flat fv_eqs @ flat fv_bn_eqs)

  val lthy' =
    lthy
    |> Function.add_function fv_names fv_eqs_binds Function_Common.default_config
    |> by_pat_completeness_auto
    |> Local_Theory.restore
    |> termination_by (Lexicographic_Order.lexicographic_order)
in
  (fv_frees @ fvbns, lthy')
end
*}

end