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

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

(* 

- eqvt_tac and eqvt_strict_tac take a list of theorems
  which are first tried to simplify permutations

  the string list contains constants that should not be
  analysed (for example there is no raw eqvt-lemma for
  the constant The; therefore it should not be analysed 

- setting [[trace_eqvt = true]] switches on tracing 
  information  


TODO:

 - provide a proper parser for the method (see Nominal2_Eqvt)
   
 - proably the list of bad constant should be a dataslot

*)

structure Nominal_Permeq: NOMINAL_PERMEQ =
struct

open Nominal_ThmDecls;

(* tracing 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_msg ctxt result = 
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

fun trace_conv ctxt conv ctrm =
let
  val result = conv ctrm
in
  if Thm.is_reflexive result 
  then result
  else (trace_msg ctxt result; result)
end

(* this conversion always fails, but prints 
   out the analysed term  *)
fun trace_info_conv ctxt ctrm = 
let
  val trm = term_of ctrm
  val _ = case (head_of trm) of 
      @{const "Trueprop"} => ()
    | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm)
in
  Conv.no_conv ctrm
end

(* conversion for applications: 
   only applies the conversion, if the head of the
   application is not a "bad head" *)
fun has_bad_head bad_hds trm = 
  case (head_of trm) of 
    Const (s, _) => member (op=) bad_hds s 
  | _ => false 

fun eqvt_apply_conv bad_hds ctrm =
  case (term_of ctrm) of
    Const (@{const_name "permute"}, _) $ _ $ (trm $ _) =>
      let
        val (perm, t) = Thm.dest_comb ctrm
        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
        if has_bad_head bad_hds trm
        then Conv.no_conv ctrm
        else Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
      end
  | _ => Conv.no_conv ctrm

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

(* conversion that raises an error or prints a warning message, 
   if a permutation on a constant or application cannot be analysed *)
fun progress_info_conv ctxt strict_flag ctrm =
let
  fun msg trm = 
    (if strict_flag then error else warning) 
      ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))

  val _ = case (term_of ctrm) of
      Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm
    | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm
    | _ => () 
in
  Conv.all_conv ctrm 
end

fun mk_equiv r = r RS @{thm eq_reflection};
fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;

(* main conversion *)
fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm =
let
  val first_conv_wrapper = 
    if trace_enabled ctxt 
    then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt))
    else Conv.first_conv

  val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt
  val post_thms = map safe_mk_equiv @{thms permute_pure}
in
  first_conv_wrapper
    [ More_Conv.rewrs_conv pre_thms,
      eqvt_apply_conv bad_hds,
      eqvt_lambda_conv,
      More_Conv.rewrs_conv post_thms,
      progress_info_conv ctxt strict_flag
    ] ctrm
end

(* raises an error if some permutations cannot be eliminated *)
fun eqvt_strict_tac ctxt user_thms bad_hds = 
  CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt true user_thms bad_hds) ctxt)

(* prints a warning message if some permutations cannot be eliminated *)
fun eqvt_tac ctxt user_thms bad_hds = 
  CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt false user_thms bad_hds) ctxt)

(* setup of the configuration value *)
val setup =
  trace_eqvt_setup

end; (* structure *)