39 val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false); |
39 val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false); |
40 |
40 |
41 fun trace_enabled ctxt = Config.get ctxt trace_eqvt |
41 fun trace_enabled ctxt = Config.get ctxt trace_eqvt |
42 |
42 |
43 fun trace_msg ctxt result = |
43 fun trace_msg ctxt result = |
44 let |
44 let |
45 val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) |
45 val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) |
46 val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result)) |
46 val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result)) |
47 in |
47 in |
48 warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) |
48 warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) |
49 end |
49 end |
50 |
50 |
51 fun trace_conv ctxt conv ctrm = |
51 fun trace_conv ctxt conv ctrm = |
52 let |
52 let |
53 val result = conv ctrm |
53 val result = conv ctrm |
54 in |
54 in |
55 if Thm.is_reflexive result |
55 if Thm.is_reflexive result |
56 then result |
56 then result |
57 else (trace_msg ctxt result; result) |
57 else (trace_msg ctxt result; result) |
58 end |
58 end |
59 |
59 |
60 (* this conversion always fails, but prints |
60 (* this conversion always fails, but prints |
61 out the analysed term *) |
61 out the analysed term *) |
62 fun trace_info_conv ctxt ctrm = |
62 fun trace_info_conv ctxt ctrm = |
63 let |
63 let |
64 val trm = term_of ctrm |
64 val trm = term_of ctrm |
65 val _ = case (head_of trm) of |
65 val _ = case (head_of trm) of |
66 @{const "Trueprop"} => () |
66 @{const "Trueprop"} => () |
67 | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm) |
67 | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm) |
68 in |
68 in |
69 Conv.no_conv ctrm |
69 Conv.no_conv ctrm |
70 end |
70 end |
71 |
71 |
72 (* conversion for applications *) |
72 (* conversion for applications *) |
73 fun eqvt_apply_conv ctrm = |
73 fun eqvt_apply_conv ctrm = |
74 case (term_of ctrm) of |
74 case (term_of ctrm) of |
75 Const (@{const_name "permute"}, _) $ _ $ (_ $ _) => |
75 Const (@{const_name "permute"}, _) $ _ $ (_ $ _) => |
99 |
99 |
100 fun is_excluded excluded (Const (a, _)) = member (op=) excluded a |
100 fun is_excluded excluded (Const (a, _)) = member (op=) excluded a |
101 | is_excluded _ _ = false |
101 | is_excluded _ _ = false |
102 |
102 |
103 fun progress_info_conv ctxt strict_flag excluded ctrm = |
103 fun progress_info_conv ctxt strict_flag excluded ctrm = |
104 let |
104 let |
105 fun msg trm = |
105 fun msg trm = |
106 if is_excluded excluded trm then () else |
106 if is_excluded excluded trm then () else |
107 (if strict_flag then error else warning) |
107 (if strict_flag then error else warning) |
108 ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) |
108 ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) |
109 |
109 |
110 val _ = case (term_of ctrm) of |
110 val _ = case (term_of ctrm) of |
111 Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm |
111 Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm |
112 | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm |
112 | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm |
113 | _ => () |
113 | _ => () |
114 in |
114 in |
115 Conv.all_conv ctrm |
115 Conv.all_conv ctrm |
116 end |
116 end |
117 |
117 |
118 (* main conversion *) |
118 (* main conversion *) |
119 fun eqvt_conv ctxt strict_flag user_thms excluded ctrm = |
119 fun eqvt_conv ctxt strict_flag user_thms excluded ctrm = |
120 let |
120 let |
121 val first_conv_wrapper = |
121 val first_conv_wrapper = |
122 if trace_enabled ctxt |
122 if trace_enabled ctxt |
123 then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) |
123 then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) |
124 else Conv.first_conv |
124 else Conv.first_conv |
125 |
125 |
126 val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt |
126 val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt |
127 val post_thms = map safe_mk_equiv @{thms permute_pure} |
127 val post_thms = map safe_mk_equiv @{thms permute_pure} |
128 in |
128 in |
129 first_conv_wrapper |
129 first_conv_wrapper |
130 [ Conv.rewrs_conv pre_thms, |
130 [ Conv.rewrs_conv pre_thms, |
131 eqvt_apply_conv, |
131 eqvt_apply_conv, |
132 eqvt_lambda_conv, |
132 eqvt_lambda_conv, |
133 Conv.rewrs_conv post_thms, |
133 Conv.rewrs_conv post_thms, |
134 progress_info_conv ctxt strict_flag excluded |
134 progress_info_conv ctxt strict_flag excluded |
135 ] ctrm |
135 ] ctrm |
136 end |
136 end |
137 |
137 |
138 (* the eqvt-tactics first eta-normalise goals in |
138 (* the eqvt-tactics first eta-normalise goals in |
139 order to avoid problems with inductions in the |
139 order to avoid problems with inductions in the |
140 equivaraince command. *) |
140 equivaraince command. *) |
141 |
141 |