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

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"} => ()

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

(* main conversion *)

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 post_thms = @{thms permute_pure[THEN eq_reflection]}

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

(* prints a warning message if some permutations cannot be eliminated *)

(* setup of the configuration value *)

val setup =

  trace_eqvt_setup

end; (* structure *)