(*  Title:      nominal_dt_rawfuns.ML
    Author:     Cezary Kaliszyk
    Author:     Christian Urban

  Definitions of the raw fv and fv_bn functions
*)

signature NOMINAL_DT_RAWFUNS =
sig
  (* info of binding functions *)
  type bn_info = (term * int * (int * term option) list list) list

  (* binding modes and binding clauses *)
  datatype bmode = Lst | Res | Set
  datatype bclause = BC of bmode * (term option * int) list * int list

  val is_atom: Proof.context -> typ -> bool
  val is_atom_set: Proof.context -> typ -> bool
  val is_atom_fset: Proof.context -> typ -> bool
  val is_atom_list: Proof.context -> typ -> bool
  val mk_atom_set: term -> term
  val mk_atom_fset: term -> term

  val setify: Proof.context -> term -> term
  val listify: Proof.context -> term -> term

  val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> 
    thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory
 
  val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list
end


structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
struct

(* term              - is constant of the bn-function 
   int               - is datatype number over which the bn-function is defined
   int * term option - is number of the corresponding argument with possibly
                       recursive call with bn-function term 
*)  
type bn_info = (term * int * (int * term option) list list) list

datatype bmode = Lst | Res | Set
datatype bclause = BC of bmode * (term option * int) list * int list

(* testing for concrete atom types *)
fun is_atom ctxt ty =
  Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})

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

fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
  | is_atom_fset _ _ = false;

fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
  | is_atom_list _ _ = false


(* functions for producing sets, fsets and lists of general atom type
   out from concrete atom types *)
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 dest_fsetT (Type (@{type_name fset}, [T])) = T
  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);

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 => atom set"}
in
  fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
end

fun mk_atom_list t =
let
  val ty = fastype_of t;
  val atom_ty = dest_listT ty --> @{typ atom};
  val map_ty = atom_ty --> ty --> @{typ "atom list"};
in
  Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t
end

(* functions that coerces singletons, sets and fsets of concrete atoms
   into sets of general atoms *)
fun setify ctxt t =
let
  val ty = fastype_of t;
in
  if is_atom ctxt ty
    then  HOLogic.mk_set @{typ atom} [mk_atom t]
  else if is_atom_set ctxt ty
    then mk_atom_set t
  else if is_atom_fset ctxt ty
    then mk_atom_fset t
  else raise TERM ("setify", [t])
end

(* functions that coerces singletons and lists of concrete atoms
   into lists of general atoms  *)
fun listify ctxt t =
let
  val ty = fastype_of t;
in
  if is_atom ctxt ty
    then HOLogic.mk_list @{typ atom} [mk_atom t]
  else if is_atom_list ctxt ty
    then mk_atom_set t
  else raise TERM ("listify", [t])
end

(* coerces a list into a set *)
fun to_set t =
  if fastype_of t = @{typ "atom list"}
  then @{term "set::atom list => atom set"} $ t
  else t


(** functions that construct the equations for fv and fv_bn **)

fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
let
  fun mk_fv_body fv_map args i = 
  let
    val arg = nth args i
    val ty = fastype_of arg
  in
    case AList.lookup (op=) fv_map ty of
      NONE => mk_supp arg
    | SOME fv => fv $ arg
  end  

  fun mk_fv_binder lthy fv_bn_map args (bn_option, i) = 
  let
    val arg = nth args i
  in
    case bn_option of
      NONE => (setify lthy arg, @{term "{}::atom set"})
    | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg)
  end  

  val t1 = map (mk_fv_body fv_map args) bodies
  val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders)
in 
  fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
end

(* in case of fv_bn we have to treat the case special, where an
   "empty" binding clause is given *)
fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =
let
  fun mk_fv_bn_body fv_map fv_bn_map bn_args args i = 
  let
    val arg = nth args i
    val ty = fastype_of arg
  in
    case AList.lookup (op=) bn_args i of
      NONE => (case (AList.lookup (op=) fv_map ty) of
                 NONE => mk_supp arg
               | SOME fv => fv $ arg)
    | SOME (NONE) => @{term "{}::atom set"}
    | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg
  end  
in
  case bclause of
    BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies)
  | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause
end

fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses = 
let
  val arg_names = Datatype_Prop.make_tnames arg_tys
  val args = map Free (arg_names ~~ arg_tys)
  val fv = the (AList.lookup (op=) fv_map ty)
  val lhs = fv $ list_comb (constr, args)
  val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses
  val rhs = fold_union rhs_trms
in
  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
end

fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses =
let
  val arg_names = Datatype_Prop.make_tnames arg_tys
  val args = map Free (arg_names ~~ arg_tys)
  val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm)
  val lhs = fv_bn $ list_comb (constr, args)
  val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses
  val rhs = fold_union rhs_trms
in
  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
end

fun mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = 
let
  val nth_constrs_info = nth constrs_info bn_n
  val nth_bclausess = nth bclausesss bn_n
in
  map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
end

fun define_raw_fvs raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms size_simps lthy =
let
  val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names
  val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys
  val fv_frees = map Free (fv_names ~~ fv_tys);
  val fv_map = raw_tys ~~ fv_frees

  val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
  val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
  val fv_bn_names = map (prefix "fv_") bn_names
  val fv_bn_arg_tys = map (nth raw_tys) bn_tys
  val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys
  val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys)
  val fv_bn_map = bns ~~ fv_bn_frees

  val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) cns_info bclausesss 
  val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map cns_info bclausesss) bn_info
  
  val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
  val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)

  val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
    Function_Common.default_config (pat_completeness_simp constr_thms) lthy
  
  val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy')
 
  val {fs, simps, inducts, ...} = info;

  val morphism = ProofContext.export_morphism lthy'' lthy
  val fs_exp = map (Morphism.term morphism) fs
  val simps_exp = map (Morphism.thm morphism) (the simps)
  val inducts_exp = map (Morphism.thm morphism) (the inducts)
  val (fvs_exp, fv_bns_exp) = chop (length fv_frees) fs_exp
in
  (fvs_exp, fv_bns_exp, simps_exp, inducts_exp, lthy'')
end


(** equivarance proofs **)

val eqvt_apply_sym = @{thm eqvt_apply[symmetric]}

fun subproof_tac const_names simps = 
  SUBPROOF (fn {prems, context, ...} => 
    HEADGOAL 
      (simp_tac (HOL_basic_ss addsimps simps)
       THEN' Nominal_Permeq.eqvt_tac context [] const_names
       THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym]))))

fun prove_eqvt_tac insts ind_thms const_names simps ctxt = 
  HEADGOAL
    (Object_Logic.full_atomize_tac
     THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms))  
     THEN_ALL_NEW  subproof_tac const_names simps ctxt)

fun mk_eqvt_goal pi const arg =
let
  val lhs = mk_perm pi (const $ arg)
  val rhs = const $ (mk_perm pi arg)  
in
  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
end

fun raw_prove_eqvt consts ind_thms simps ctxt =
  if null consts then []
  else
    let 
      val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
      val p = Free (p, @{typ perm})
      val arg_tys = 
        consts
        |> map fastype_of
        |> map domain_type 
      val (arg_names, ctxt'') = 
        Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt'
      val args = map Free (arg_names ~~ arg_tys)
      val goals = map2 (mk_eqvt_goal p) consts args
      val insts = map (single o SOME) arg_names
      val const_names = map (fst o dest_Const) consts      
    in
      Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => 
        prove_eqvt_tac insts ind_thms const_names simps context)
      |> ProofContext.export ctxt'' ctxt
    end

end (* structure *)