(*  Title:      nominal_thmdecls.ML
    Author:     Brian Huffman, Christian Urban
*)

signature NOMINAL_PERMEQ =
sig
  val eqvt_tac: Proof.context -> thm list -> int -> tactic 
  val trace_eqvt: bool Config.T
  val setup: theory -> theory
end;

(* TODO:

 - provide a method interface with the usual add and del options

 - print a warning if for a constant no eqvt lemma is stored

*)


structure Nominal_Permeq: NOMINAL_PERMEQ =
struct

fun is_head_Trueprop trm = 
  case (head_of trm) of 
    @{const "Trueprop"} => true 
  | _ => false 

(* debugging infrastructure *)
val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false);

fun trace_enabled ctxt = Config.get ctxt trace_eqvt

fun trace_conv ctxt conv ct =
let
  val result = conv ct
  val _ = 
    if trace_enabled ctxt andalso not (Thm.is_reflexive result) 
    then  
      let
        val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result))
        val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result))
      in
        warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) 
      end
    else ()
in
  result
end;

(* conversion for applications *)
fun eqvt_apply_conv ctxt ct =
  case (term_of ct) of
    (Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) =>
      let
        val (perm, t) = Thm.dest_comb ct
        val (_, p) = Thm.dest_comb perm
        val (f, x) = Thm.dest_comb t
        val a = ctyp_of_term x;
        val b = ctyp_of_term t;
        val ty_insts = map SOME [b, a]
        val term_insts = map SOME [p, f, x]                        
      in
        Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
      end
  | _ => Conv.no_conv ct

(* conversion for lambdas *)
fun eqvt_lambda_conv ctxt ct =
  case (term_of ct) of
    (Const (@{const_name "permute"}, _) $ _ $ Abs _) =>
      Conv.rewr_conv @{thm eqvt_lambda} ct
  | _ => Conv.no_conv ct


(* main conversion *)
fun eqvt_conv ctxt thms ctrm =
let
  val trm = term_of ctrm 
  val _ = if trace_enabled ctxt andalso not (is_head_Trueprop trm)
    then warning ("analysing " ^ Syntax.string_of_term ctxt trm) 
    else ()
  val wrapper = if trace_enabled ctxt then trace_conv ctxt else I			
in
  Conv.first_conv (map wrapper
    [ More_Conv.rewrs_conv thms,
      Conv.rewr_conv @{thm eqvt_bound},
      More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvts_raw_thms ctxt),
      eqvt_apply_conv ctxt,
      eqvt_lambda_conv ctxt,
      More_Conv.rewrs_conv @{thms permute_pure[THEN eq_reflection]},
      Conv.all_conv
    ]) ctrm
end


fun eqvt_tac ctxt thms = 
  CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt thms) ctxt)

val setup =
  trace_eqvt_setup

end; (* structure *)