equal
deleted
inserted
replaced
104 Conv.rewr_conv @{thm eqvt_lambda} ctrm |
104 Conv.rewr_conv @{thm eqvt_lambda} ctrm |
105 | _ => Conv.no_conv ctrm |
105 | _ => Conv.no_conv ctrm |
106 |
106 |
107 (* conversion that raises an error or prints a warning message, |
107 (* conversion that raises an error or prints a warning message, |
108 if a permutation on a constant or application cannot be analysed *) |
108 if a permutation on a constant or application cannot be analysed *) |
109 fun progress_info_conv ctxt strict_flag ctrm = |
109 fun progress_info_conv ctxt strict_flag bad_hds ctrm = |
110 let |
110 let |
111 fun msg trm = |
111 fun msg trm = |
112 (if strict_flag then error else warning) |
112 let |
113 ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) |
113 val hd = head_of trm |
|
114 in |
|
115 if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then () |
|
116 else (if strict_flag then error else warning) |
|
117 ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) |
|
118 end |
114 |
119 |
115 val _ = case (term_of ctrm) of |
120 val _ = case (term_of ctrm) of |
116 Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm |
121 Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm |
117 | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm |
122 | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm |
118 | _ => () |
123 | _ => () |
134 first_conv_wrapper |
139 first_conv_wrapper |
135 [ More_Conv.rewrs_conv pre_thms, |
140 [ More_Conv.rewrs_conv pre_thms, |
136 eqvt_apply_conv bad_hds, |
141 eqvt_apply_conv bad_hds, |
137 eqvt_lambda_conv, |
142 eqvt_lambda_conv, |
138 More_Conv.rewrs_conv post_thms, |
143 More_Conv.rewrs_conv post_thms, |
139 progress_info_conv ctxt strict_flag |
144 progress_info_conv ctxt strict_flag bad_hds |
140 ] ctrm |
145 ] ctrm |
141 end |
146 end |
142 |
147 |
143 (* raises an error if some permutations cannot be eliminated *) |
148 (* raises an error if some permutations cannot be eliminated *) |
144 fun eqvt_strict_tac ctxt user_thms bad_hds = |
149 fun eqvt_strict_tac ctxt user_thms bad_hds = |