1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1 |
(* Title: nominal_permeq.ML
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
2 |
Author: Christian Urban
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
3 |
Author: Brian Huffman
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
*)
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
signature NOMINAL_PERMEQ =
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
sig
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
8 |
val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
9 |
val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
10 |
val trace_eqvt: bool Config.T
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
11 |
val setup: theory -> theory
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
end;
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
14 |
(*
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
15 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
- eqvt_tac and eqvt_strict_tac take a list of theorems
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
17 |
which are first tried to simplify permutations
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
18 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
19 |
the string list contains constants that should not be
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
20 |
analysed (for example there is no raw eqvt-lemma for
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
21 |
the constant The; therefore it should not be analysed
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
23 |
- setting [[trace_eqvt = true]] switches on tracing
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
24 |
information
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
25 |
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
26 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
27 |
TODO:
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
28 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
29 |
- provide a proper parser for the method (see Nominal2_Eqvt)
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
30 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
31 |
- proably the list of bad constant should be a dataslot
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
32 |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
*)
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
34 |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
35 |
structure Nominal_Permeq: NOMINAL_PERMEQ =
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
struct
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
38 |
open Nominal_ThmDecls;
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
39 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
40 |
(* tracing infrastructure *)
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
41 |
val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false);
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
42 |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
43 |
fun trace_enabled ctxt = Config.get ctxt trace_eqvt
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
45 |
fun trace_msg ctxt result =
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
46 |
let
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
47 |
val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result))
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
48 |
val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result))
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
49 |
in
|
1803
ed46cf122016
used warning instead of tracing (does not seem to produce stable output)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
50 |
warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str]))
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
51 |
end
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
52 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
53 |
fun trace_conv ctxt conv ctrm =
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
54 |
let
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
55 |
val result = conv ctrm
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
56 |
in
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
57 |
if Thm.is_reflexive result
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
58 |
then result
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
59 |
else (trace_msg ctxt result; result)
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
60 |
end
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
61 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
62 |
(* this conversion always fails, but prints
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
63 |
out the analysed term *)
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
64 |
fun trace_info_conv ctxt ctrm =
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
65 |
let
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
66 |
val trm = term_of ctrm
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
67 |
val _ = case (head_of trm) of
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
68 |
@{const "Trueprop"} => ()
|
1803
ed46cf122016
used warning instead of tracing (does not seem to produce stable output)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
69 |
| _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm)
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
70 |
in
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
71 |
Conv.no_conv ctrm
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
72 |
end
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
73 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
74 |
(* conversion for applications:
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
75 |
only applies the conversion, if the head of the
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
76 |
application is not a "bad head" *)
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
77 |
fun has_bad_head bad_hds trm =
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
78 |
case (head_of trm) of
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
79 |
Const (s, _) => member (op=) bad_hds s
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
80 |
| _ => false
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
81 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
82 |
fun eqvt_apply_conv bad_hds ctrm =
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
83 |
case (term_of ctrm) of
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
84 |
Const (@{const_name "permute"}, _) $ _ $ (trm $ _) =>
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
85 |
let
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
86 |
val (perm, t) = Thm.dest_comb ctrm
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
87 |
val (_, p) = Thm.dest_comb perm
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
88 |
val (f, x) = Thm.dest_comb t
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
89 |
val a = ctyp_of_term x;
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
90 |
val b = ctyp_of_term t;
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
91 |
val ty_insts = map SOME [b, a]
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
92 |
val term_insts = map SOME [p, f, x]
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
93 |
in
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
94 |
if has_bad_head bad_hds trm
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
95 |
then Conv.no_conv ctrm
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
96 |
else Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
97 |
end
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
98 |
| _ => Conv.no_conv ctrm
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
99 |
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
100 |
(* conversion for lambdas *)
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
101 |
fun eqvt_lambda_conv ctrm =
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
102 |
case (term_of ctrm) of
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
103 |
Const (@{const_name "permute"}, _) $ _ $ (Abs _) =>
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
104 |
Conv.rewr_conv @{thm eqvt_lambda} ctrm
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
105 |
| _ => Conv.no_conv ctrm
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
106 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
107 |
(* conversion that raises an error or prints a warning message,
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
108 |
if a permutation on a constant or application cannot be analysed *)
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
109 |
fun progress_info_conv ctxt strict_flag ctrm =
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
110 |
let
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
111 |
fun msg trm =
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
112 |
(if strict_flag then error else warning)
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
113 |
("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
114 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
115 |
val _ = case (term_of ctrm) of
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
116 |
Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
117 |
| Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
118 |
| _ => ()
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
119 |
in
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
120 |
Conv.all_conv ctrm
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
121 |
end
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
122 |
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
123 |
(* main conversion *)
|
1803
ed46cf122016
used warning instead of tracing (does not seem to produce stable output)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
124 |
fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm =
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
125 |
let
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
126 |
val first_conv_wrapper =
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
127 |
if trace_enabled ctxt
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
128 |
then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt))
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
129 |
else Conv.first_conv
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
130 |
|
1810
894930834ca8
fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
131 |
val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt
|
894930834ca8
fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
132 |
val post_thms = map safe_mk_equiv @{thms permute_pure}
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
133 |
in
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
134 |
first_conv_wrapper
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
135 |
[ More_Conv.rewrs_conv pre_thms,
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
136 |
eqvt_apply_conv bad_hds,
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
137 |
eqvt_lambda_conv,
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
138 |
More_Conv.rewrs_conv post_thms,
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
139 |
progress_info_conv ctxt strict_flag
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
140 |
] ctrm
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
141 |
end
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
142 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
143 |
(* raises an error if some permutations cannot be eliminated *)
|
1803
ed46cf122016
used warning instead of tracing (does not seem to produce stable output)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
144 |
fun eqvt_strict_tac ctxt user_thms bad_hds =
|
ed46cf122016
used warning instead of tracing (does not seem to produce stable output)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
145 |
CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt true user_thms bad_hds) ctxt)
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
146 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
147 |
(* prints a warning message if some permutations cannot be eliminated *)
|
1803
ed46cf122016
used warning instead of tracing (does not seem to produce stable output)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
148 |
fun eqvt_tac ctxt user_thms bad_hds =
|
ed46cf122016
used warning instead of tracing (does not seem to produce stable output)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
149 |
CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt false user_thms bad_hds) ctxt)
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
150 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
151 |
(* setup of the configuration value *)
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
152 |
val setup =
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
153 |
trace_eqvt_setup
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
154 |
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
155 |
end; (* structure *) |