74 | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm) |
67 | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm) |
75 in |
68 in |
76 Conv.no_conv ctrm |
69 Conv.no_conv ctrm |
77 end |
70 end |
78 |
71 |
79 (* conversion for applications: |
72 (* conversion for applications *) |
80 only applies the conversion, if the head of the |
73 fun eqvt_apply_conv ctrm = |
81 application is not a "bad head" *) |
|
82 fun has_bad_head bad_hds trm = |
|
83 case (head_of trm) of |
|
84 Const (s, _) => member (op=) bad_hds s |
|
85 | _ => false |
|
86 |
|
87 fun eqvt_apply_conv bad_hds ctrm = |
|
88 case (term_of ctrm) of |
74 case (term_of ctrm) of |
89 Const (@{const_name "permute"}, _) $ _ $ (trm $ _) => |
75 Const (@{const_name "permute"}, _) $ _ $ (_ $ _) => |
90 let |
76 let |
91 val (perm, t) = Thm.dest_comb ctrm |
77 val (perm, t) = Thm.dest_comb ctrm |
92 val (_, p) = Thm.dest_comb perm |
78 val (_, p) = Thm.dest_comb perm |
93 val (f, x) = Thm.dest_comb t |
79 val (f, x) = Thm.dest_comb t |
94 val a = ctyp_of_term x; |
80 val a = ctyp_of_term x; |
95 val b = ctyp_of_term t; |
81 val b = ctyp_of_term t; |
96 val ty_insts = map SOME [b, a] |
82 val ty_insts = map SOME [b, a] |
97 val term_insts = map SOME [p, f, x] |
83 val term_insts = map SOME [p, f, x] |
98 in |
84 in |
99 if has_bad_head bad_hds trm |
85 Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} |
100 then Conv.all_conv ctrm |
|
101 else Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} |
|
102 end |
86 end |
103 | _ => Conv.no_conv ctrm |
87 | _ => Conv.no_conv ctrm |
104 |
88 |
105 (* conversion for lambdas *) |
89 (* conversion for lambdas *) |
106 fun eqvt_lambda_conv ctrm = |
90 fun eqvt_lambda_conv ctrm = |
107 case (term_of ctrm) of |
91 case (term_of ctrm) of |
108 Const (@{const_name "permute"}, _) $ _ $ (Abs _) => |
92 Const (@{const_name "permute"}, _) $ _ $ (Abs _) => |
109 Conv.rewr_conv @{thm eqvt_lambda} ctrm |
93 Conv.rewr_conv @{thm eqvt_lambda} ctrm |
110 | _ => Conv.no_conv ctrm |
94 | _ => Conv.no_conv ctrm |
111 |
95 |
|
96 |
112 (* conversion that raises an error or prints a warning message, |
97 (* conversion that raises an error or prints a warning message, |
113 if a permutation on a constant or application cannot be analysed *) |
98 if a permutation on a constant or application cannot be analysed *) |
114 fun progress_info_conv ctxt strict_flag bad_hds ctrm = |
99 |
|
100 fun is_excluded excluded (Const (a, _)) = member (op=) excluded a |
|
101 | is_excluded _ _ = false |
|
102 |
|
103 fun progress_info_conv ctxt strict_flag excluded ctrm = |
115 let |
104 let |
116 fun msg trm = |
105 fun msg trm = |
117 let |
106 if is_excluded excluded trm then () else |
118 val hd = head_of trm |
107 (if strict_flag then error else warning) |
119 in |
108 ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) |
120 if is_Const hd andalso member (op =) bad_hds (fst (dest_Const hd)) then () |
|
121 else (if strict_flag then error else warning) |
|
122 ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) |
|
123 end |
|
124 |
109 |
125 val _ = case (term_of ctrm) of |
110 val _ = case (term_of ctrm) of |
126 Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm |
111 Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm |
127 | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm |
112 | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm |
128 | _ => () |
113 | _ => () |
129 in |
114 in |
130 Conv.all_conv ctrm |
115 Conv.all_conv ctrm |
131 end |
116 end |
132 |
117 |
133 (* main conversion *) |
118 (* main conversion *) |
134 fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm = |
119 fun eqvt_conv ctxt strict_flag user_thms excluded ctrm = |
135 let |
120 let |
136 val first_conv_wrapper = |
121 val first_conv_wrapper = |
137 if trace_enabled ctxt |
122 if trace_enabled ctxt |
138 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)) |
139 else Conv.first_conv |
124 else Conv.first_conv |
141 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 |
142 val post_thms = map safe_mk_equiv @{thms permute_pure} |
127 val post_thms = map safe_mk_equiv @{thms permute_pure} |
143 in |
128 in |
144 first_conv_wrapper |
129 first_conv_wrapper |
145 [ More_Conv.rewrs_conv pre_thms, |
130 [ More_Conv.rewrs_conv pre_thms, |
146 eqvt_apply_conv bad_hds, |
131 eqvt_apply_conv, |
147 eqvt_lambda_conv, |
132 eqvt_lambda_conv, |
148 More_Conv.rewrs_conv post_thms, |
133 More_Conv.rewrs_conv post_thms, |
149 progress_info_conv ctxt strict_flag bad_hds |
134 progress_info_conv ctxt strict_flag excluded |
150 ] ctrm |
135 ] ctrm |
151 end |
136 end |
152 |
137 |
153 (* the eqvt-tactics first eta-normalise goals in |
138 (* the eqvt-tactics first eta-normalise goals in |
154 order to avoid problems with inductions in the |
139 order to avoid problems with inductions in the |
155 equivaraince command. *) |
140 equivaraince command. *) |
156 |
141 |
157 (* raises an error if some permutations cannot be eliminated *) |
142 (* raises an error if some permutations cannot be eliminated *) |
158 fun eqvt_strict_tac ctxt user_thms bad_hds = |
143 fun eqvt_strict_tac ctxt user_thms excluded = |
159 CONVERSION (More_Conv.top_conv |
144 CONVERSION (More_Conv.top_conv |
160 (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms bad_hds)) ctxt) |
145 (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms excluded)) ctxt) |
161 |
146 |
162 (* prints a warning message if some permutations cannot be eliminated *) |
147 (* prints a warning message if some permutations cannot be eliminated *) |
163 fun eqvt_tac ctxt user_thms bad_hds = |
148 fun eqvt_tac ctxt user_thms excluded = |
164 CONVERSION (More_Conv.top_conv |
149 CONVERSION (More_Conv.top_conv |
165 (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms bad_hds)) ctxt) |
150 (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms excluded)) ctxt) |
166 |
151 |
167 (* setup of the configuration value *) |
152 (* setup of the configuration value *) |
168 val setup = |
153 val setup = |
169 trace_eqvt_setup |
154 trace_eqvt_setup |
170 |
155 |