# HG changeset patch # User Christian Urban # Date 1270974969 -7200 # Node ID 6d2a39db3862e1b45e94293978f46ec490c59d24 # Parent 78fdc6b36a1c64af69cfb970753915ce34c41996 added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed diff -r 78fdc6b36a1c -r 6d2a39db3862 Nominal-General/Nominal2_Eqvt.thy --- a/Nominal-General/Nominal2_Eqvt.thy Fri Apr 09 21:51:01 2010 +0200 +++ b/Nominal-General/Nominal2_Eqvt.thy Sun Apr 11 10:36:09 2010 +0200 @@ -282,15 +282,19 @@ shows "p \ unpermute p x \ x" unfolding unpermute_def by simp -ML {* @{const Trueprop} *} - use "nominal_permeq.ML" setup Nominal_Permeq.setup method_setup perm_simp = - {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms))) *} + {* Attrib.thms >> + (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms ["The"]))) *} {* pushes permutations inside *} +method_setup perm_strict_simp = + {* Attrib.thms >> + (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_strict_tac ctxt thms ["The"]))) *} + {* pushes permutations inside, raises an error if it cannot solve all permutations *} + declare [[trace_eqvt = true]] lemma @@ -352,13 +356,6 @@ oops lemma - fixes p q r::"perm" - and x::"'a::pt" - shows "p \ (q \ r \ x) = foo" -apply(perm_simp) -oops - -lemma fixes C D::"bool" shows "B (p \ (C = D))" apply(perm_simp) @@ -369,6 +366,7 @@ text {* Problem: there is no raw eqvt-rule for The *} lemma "p \ (THE x. P x) = foo" apply(perm_simp) +(* apply(perm_strict_simp) *) oops diff -r 78fdc6b36a1c -r 6d2a39db3862 Nominal-General/nominal_permeq.ML --- a/Nominal-General/nominal_permeq.ML Fri Apr 09 21:51:01 2010 +0200 +++ b/Nominal-General/nominal_permeq.ML Sun Apr 11 10:36:09 2010 +0200 @@ -1,59 +1,90 @@ -(* Title: nominal_thmdecls.ML - Author: Brian Huffman, Christian Urban +(* Title: nominal_permeq.ML + Author: Christian Urban + Author: Brian Huffman *) signature NOMINAL_PERMEQ = sig - val eqvt_tac: Proof.context -> thm list -> int -> tactic + 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; -(* TODO: +(* + +- 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 - - provide a method interface with the usual add and del options +- setting [[trace_eqvt = true]] switches on tracing + information + - - print a warning if for a constant no eqvt lemma is stored +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 -fun is_head_Trueprop trm = - case (head_of trm) of - @{const "Trueprop"} => true - | _ => false +open Nominal_ThmDecls; -(* debugging infrastructure *) +(* 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_conv ctxt conv ct = +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 + tracing (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 result = conv ct - val _ = - if trace_enabled ctxt andalso not (Thm.is_reflexive result) - then + val trm = term_of ctrm + val _ = case (head_of trm) of + @{const "Trueprop"} => () + | _ => tracing ("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 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 (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; @@ -61,42 +92,65 @@ 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} + 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 ct + | _ => Conv.no_conv ctrm (* 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 +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 *) -fun eqvt_conv ctxt thms ctrm = +fun eqvt_conv ctxt strict_flag thms bad_hds 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 + 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 = thms @ @{thms eqvt_bound} @ (get_eqvts_raw_thms ctxt) + val post_thms = @{thms permute_pure[THEN eq_reflection]} 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 + 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 thms bad_hds = + CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt true thms bad_hds) ctxt) -fun eqvt_tac ctxt thms = - CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt thms) ctxt) +(* prints a warning message if some permutations cannot be eliminated *) +fun eqvt_tac ctxt thms bad_hds = + CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt false thms bad_hds) ctxt) +(* setup of the configuration value *) val setup = trace_eqvt_setup