(*  Title:      nominal_permeq.ML

    Author:     Christian Urban

    Author:     Brian Huffman

*)

signature NOMINAL_PERMEQ =

sig

  val eqvt_rule: Proof.context -> thm list -> string list -> thm -> thm

  val eqvt_strict_rule: Proof.context -> thm list -> string list -> thm -> thm

  val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic

  val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic

  val perm_simp_meth: thm list * string list -> Proof.context -> Method.method

  val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method

  val args_parser: (thm list * string list) context_parser

  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  

*)

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

fun eqvt_apply_conv ctrm =

  case (term_of ctrm) of

    Const (@{const_name "permute"}, _) $ _ $ (_ $ _) =>

      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

        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 is_excluded excluded (Const (a, _)) = member (op=) excluded a 

  | is_excluded _ _ = false 

fun progress_info_conv ctxt strict_flag excluded ctrm =

  let

    fun msg trm =

      if is_excluded excluded trm then () else 

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

fun main_eqvt_conv ctxt strict_flag user_thms excluded 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

      [ Conv.rewrs_conv pre_thms,

        eqvt_apply_conv,

        eqvt_lambda_conv,

        Conv.rewrs_conv post_thms,

        progress_info_conv ctxt strict_flag excluded

      ] ctrm

  end

(* the eqvt-tactics first eta-normalise goals in 

   order to avoid problems with inductions in the

   equivariance command. *)

(* raises an error if some permutations cannot be eliminated *)

fun eqvt_strict_conv ctxt user_thms excluded = 

  Conv.top_conv 

    (fn ctxt => Thm.eta_conversion then_conv (main_eqvt_conv ctxt true user_thms excluded)) ctxt

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

fun eqvt_conv ctxt user_thms excluded = 

  Conv.top_conv 

    (fn ctxt => Thm.eta_conversion then_conv (main_eqvt_conv ctxt false user_thms excluded)) ctxt

(* thms rewriters *)

fun eqvt_strict_rule ctxt user_thms excluded = 

  Conv.fconv_rule (eqvt_strict_conv ctxt user_thms excluded)

fun eqvt_rule ctxt user_thms excluded = 

  Conv.fconv_rule (eqvt_conv ctxt user_thms excluded)

(* tactics *)

fun eqvt_strict_tac ctxt user_thms excluded = 

  CONVERSION (eqvt_strict_conv ctxt user_thms excluded)

fun eqvt_tac ctxt user_thms excluded = 

  CONVERSION (eqvt_conv ctxt user_thms excluded)

(* setup of the configuration value *)

val setup =

  trace_eqvt_setup

(** methods **)

fun unless_more_args scan = Scan.unless (Scan.lift ((Args.$$$ "exclude") -- Args.colon)) scan

val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- 

   Scan.repeat (unless_more_args Attrib.multi_thm) >> flat) [];

val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- 

  (Scan.repeat (Args.const true))) []

val args_parser =  add_thms_parser -- exclude_consts_parser 

fun perm_simp_meth (thms, consts) ctxt = 

  SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts))

fun perm_strict_simp_meth (thms, consts) ctxt = 

  SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts))

end; (* structure *)