equal
deleted
inserted
replaced
45 fun trace_msg ctxt result = |
45 fun trace_msg ctxt result = |
46 let |
46 let |
47 val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) |
47 val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) |
48 val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result)) |
48 val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result)) |
49 in |
49 in |
50 tracing (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) |
50 warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) |
51 end |
51 end |
52 |
52 |
53 fun trace_conv ctxt conv ctrm = |
53 fun trace_conv ctxt conv ctrm = |
54 let |
54 let |
55 val result = conv ctrm |
55 val result = conv ctrm |
64 fun trace_info_conv ctxt ctrm = |
64 fun trace_info_conv ctxt ctrm = |
65 let |
65 let |
66 val trm = term_of ctrm |
66 val trm = term_of ctrm |
67 val _ = case (head_of trm) of |
67 val _ = case (head_of trm) of |
68 @{const "Trueprop"} => () |
68 @{const "Trueprop"} => () |
69 | _ => tracing ("Analysing term " ^ Syntax.string_of_term ctxt trm) |
69 | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm) |
70 in |
70 in |
71 Conv.no_conv ctrm |
71 Conv.no_conv ctrm |
72 end |
72 end |
73 |
73 |
74 |
74 |
119 | _ => () |
119 | _ => () |
120 in |
120 in |
121 Conv.all_conv ctrm |
121 Conv.all_conv ctrm |
122 end |
122 end |
123 |
123 |
|
124 fun mk_equiv r = r RS @{thm eq_reflection}; |
|
125 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
124 |
126 |
125 (* main conversion *) |
127 (* main conversion *) |
126 fun eqvt_conv ctxt strict_flag thms bad_hds ctrm = |
128 fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm = |
127 let |
129 let |
128 val first_conv_wrapper = |
130 val first_conv_wrapper = |
129 if trace_enabled ctxt |
131 if trace_enabled ctxt |
130 then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) |
132 then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) |
131 else Conv.first_conv |
133 else Conv.first_conv |
132 |
134 |
133 val pre_thms = thms @ @{thms eqvt_bound} @ (get_eqvts_raw_thms ctxt) |
135 val pre_thms = (map safe_mk_equiv user_thms) @ @{thms eqvt_bound} @ (get_eqvts_raw_thms ctxt) |
134 val post_thms = @{thms permute_pure[THEN eq_reflection]} |
136 val post_thms = @{thms permute_pure[THEN eq_reflection]} |
135 in |
137 in |
136 first_conv_wrapper |
138 first_conv_wrapper |
137 [ More_Conv.rewrs_conv pre_thms, |
139 [ More_Conv.rewrs_conv pre_thms, |
138 eqvt_apply_conv bad_hds, |
140 eqvt_apply_conv bad_hds, |
141 progress_info_conv ctxt strict_flag |
143 progress_info_conv ctxt strict_flag |
142 ] ctrm |
144 ] ctrm |
143 end |
145 end |
144 |
146 |
145 (* raises an error if some permutations cannot be eliminated *) |
147 (* raises an error if some permutations cannot be eliminated *) |
146 fun eqvt_strict_tac ctxt thms bad_hds = |
148 fun eqvt_strict_tac ctxt user_thms bad_hds = |
147 CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt true thms bad_hds) ctxt) |
149 CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt true user_thms bad_hds) ctxt) |
148 |
150 |
149 (* prints a warning message if some permutations cannot be eliminated *) |
151 (* prints a warning message if some permutations cannot be eliminated *) |
150 fun eqvt_tac ctxt thms bad_hds = |
152 fun eqvt_tac ctxt user_thms bad_hds = |
151 CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt false thms bad_hds) ctxt) |
153 CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt false user_thms bad_hds) ctxt) |
152 |
154 |
153 (* setup of the configuration value *) |
155 (* setup of the configuration value *) |
154 val setup = |
156 val setup = |
155 trace_eqvt_setup |
157 trace_eqvt_setup |
156 |
158 |