(*  Title:      nominal_dt_rawfuns.ML

    Author:     Cezary Kaliszyk

    Author:     Christian Urban

*)

signature NOMINAL_DT_RAWFUNS =

sig

  (* info of raw datatypes *)

  type dt_info = string list * binding * mixfix * ((binding * typ list * mixfix) list) list

  (* info of raw binding functions *)

  type bn_info = term * int * (int * term option) 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

  (* FIXME: should be here - currently in Nominal2.thy

  val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list ->

    (Attrib.binding * term) list -> thm list -> thm list -> local_theory ->

    (term list * thm list * bn_info list * thm list * local_theory) 

  *)

  val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list -> 

    thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory

  val define_raw_bn_perms: typ list -> bn_info list -> cns_info list -> thm list -> thm list -> 

    local_theory -> (term 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

(* string list      - type variables of a datatype

   binding          - name of the datatype

   mixfix           - its mixfix

   (binding * typ list * mixfix) list  - datatype constructors of the type

*)  

type dt_info = string list * binding * mixfix * ((binding * typ list * mixfix) list) list

(* 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

datatype bmode = Lst | Res | Set

datatype bclause = BC of bmode * (term option * int) list * int list

fun lookup xs x = the (AList.lookup (op=) xs x)

(* 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

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

    val fset = @{term "fset :: atom fset => atom set"}

  in

    fset $ (Const (@{const_name map_fset}, fmap_ty) $ (atom_const atom_ty) $ t)

  end

  fun mk_atom_list t =

  let

    val ty = fastype_of t

    val atom_ty = dest_listT ty

    val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"}

  in

    Const (@{const_name map}, map_ty) $ (atom_const 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_list t

    else raise TERM ("listify", [t])

  end

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

fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, 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 binders = 

    let

      fun bind_set lthy args (NONE, i) = (setify lthy (nth args i), @{term "{}::atom set"})

        | bind_set _ args (SOME bn, i) = (bn $ (nth args i), 

            if  member (op=) bodies i then @{term "{}::atom set"}  

            else lookup fv_bn_map bn $ (nth args i))

      fun bind_lst lthy args (NONE, i) = (listify lthy (nth args i), @{term "[]::atom list"})

        | bind_lst _ args (SOME bn, i) = (bn $ (nth args i),

            if  member (op=) bodies i then @{term "[]::atom list"}  

            else lookup fv_bn_map bn $ (nth args i)) 

      val (combine_fn, bind_fn) =

        case bmode of

          Lst => (fold_append, bind_lst) 

        | Set => (fold_union, bind_set)

        | Res => (fold_union, bind_set)

    in

      binders

      |> map (bind_fn lthy args)

      |> split_list

      |> pairself combine_fn

    end  

    val t1 = map (mk_fv_body fv_map args) bodies

    val (t2, t3) = mk_fv_binder lthy fv_bn_map args binders

  in 

    mk_union (mk_diff (fold_union t1, to_set t2), to_set 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 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) => lookup fv_bn_map bn $ arg

    end  

  in

    case bclause of

      BC (_, [], bodies) => fold_union (map mk_fv_bn_body 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 = lookup 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 = lookup 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 simps_exp = map (Morphism.thm morphism) (the simps)

    val inducts_exp = map (Morphism.thm morphism) (the inducts)

    val (fvs', fv_bns') = chop (length fv_frees) fs

  in

    (fvs', fv_bns', simps_exp, inducts_exp, lthy'')

  end

(** definition of raw permute_bn functions **)

fun mk_perm_bn_eq_rhs p perm_bn_map bn_args (i, arg) = 

  case AList.lookup (op=) bn_args i of

    NONE => arg

  | SOME (NONE) => mk_perm p arg

  | SOME (SOME bn) => (lookup perm_bn_map bn) $ p $ arg   

fun mk_perm_bn_eq lthy bn_trm perm_bn_map bn_args (constr, _, arg_tys, _) =

  let

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

    val arg_names = Datatype_Prop.make_tnames arg_tys

    val args = map Free (arg_names ~~ arg_tys)

    val perm_bn = lookup perm_bn_map bn_trm

    val lhs = perm_bn $ p $ list_comb (constr, args)

    val rhs = list_comb (constr, map_index (mk_perm_bn_eq_rhs p perm_bn_map bn_args) args)

  in

    HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))

  end

fun mk_perm_bn_eqs lthy perm_bn_map cns_info (bn_trm, bn_n, bn_argss) = 

  let

    val nth_cns_info = nth cns_info bn_n

  in

    map2 (mk_perm_bn_eq lthy bn_trm perm_bn_map) bn_argss nth_cns_info

  end

fun define_raw_bn_perms raw_tys bn_info cns_info cns_thms size_thms lthy =

  if null bn_info

  then ([], [], lthy)

  else

    let

      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 perm_bn_names = map (prefix "permute_") bn_names

      val perm_bn_arg_tys = map (nth raw_tys) bn_tys

      val perm_bn_tys = map (fn ty => @{typ "perm"} --> ty --> ty) perm_bn_arg_tys

      val perm_bn_frees = map Free (perm_bn_names ~~ perm_bn_tys)

      val perm_bn_map = bns ~~ perm_bn_frees

      val perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map cns_info) bn_info

      val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) perm_bn_names

      val all_fun_eqs = map (pair Attrib.empty_binding) (flat perm_bn_eqs)

      val prod_simps = @{thms prod.inject HOL.simp_thms}

      val (_, lthy') = Function.add_function all_fun_names all_fun_eqs

        Function_Common.default_config (pat_completeness_simp (prod_simps @ cns_thms)) lthy

      val (info, lthy'') = prove_termination size_thms (Local_Theory.restore lthy')

      val {fs, simps, ...} = info;

      val morphism = ProofContext.export_morphism lthy'' lthy

      val simps_exp = map (Morphism.thm morphism) (the simps)

    in

      (fs, simps_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