--- a/Nominal-General/nominal_permeq.ML	Fri Apr 09 09:02:54 2010 -0700
+++ b/Nominal-General/nominal_permeq.ML	Fri Apr 09 21:51:01 2010 +0200
@@ -4,8 +4,9 @@
 
 signature NOMINAL_PERMEQ =
 sig
-  val eqvt_tac: Proof.context -> int -> tactic 
-
+  val eqvt_tac: Proof.context -> thm list -> int -> tactic 
+  val trace_eqvt: bool Config.T
+  val setup: theory -> theory
 end;
 
 (* TODO:
@@ -14,20 +15,40 @@
 
  - print a warning if for a constant no eqvt lemma is stored
 
- - there seems to be too much simplified in case of multiple 
-   permutations, like
-
-      p o q o r o x 
-
-   we usually only want the outermost permutation to "float" in
 *)
 
 
 structure Nominal_Permeq: NOMINAL_PERMEQ =
 struct
 
-local
+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"}, _) $ _ $ (_ $ _)) =>
@@ -38,34 +59,45 @@
         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]
+        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
-
-fun eqvt_conv ctxt ct =
-  Conv.first_conv
-    [ Conv.rewr_conv @{thm eqvt_bound},
-      eqvt_apply_conv ctxt
-        then_conv Conv.comb_conv (eqvt_conv ctxt),
-      eqvt_lambda_conv ctxt
-        then_conv Conv.abs_conv (fn (v, ctxt) => eqvt_conv ctxt) ctxt,
+  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
-    ] ct
-
-fun eqvt_tac ctxt = 
-  CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt)
-
+    ]) 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 *)
\ No newline at end of file