(*  Title:      nominal_dt_rawperm.ML

    Author:     Cezary Kaliszyk

    Author:     Christian Urban

  Definitions of the raw bn, fv and fv_bn

  functions

*)

signature NOMINAL_DT_RAWFUNS =

sig

  datatype bmode = Lst | Res | Set

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

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

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

end

structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =

struct

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

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

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

fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =

let

  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 =

  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

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

let

  val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;

  val fv_frees = map Free (fv_names ~~ fv_tys);

  val fv_map = fv_arg_tys ~~ fv_frees

  fun pat_completeness_auto lthy =

    Pat_Completeness.pat_completeness_tac lthy 1

      THEN auto_tac (clasimpset_of lthy)

  fun prove_termination lthy =

    Function.prove_termination NONE

      (Lexicographic_Order.lexicographic_order_tac true lthy) lthy

    Function_Common.default_config pat_completeness_auto lthy

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

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

  val morphism = ProofContext.export_morphism lthy'' lthy

  val fs_exp = map (Morphism.term morphism) fs

  val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp

  val simps_exp = Morphism.fact morphism (the simps)

in

  (fv_frees_exp, fv_bns_exp, simps_exp, lthy'')

end

end (* structure *)