99 |
99 |
100 fun trace_enabled ctxt = Config.get ctxt trace_eqvt |
100 fun trace_enabled ctxt = Config.get ctxt trace_eqvt |
101 |
101 |
102 fun trace_msg ctxt result = |
102 fun trace_msg ctxt result = |
103 let |
103 let |
104 val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) |
104 val lhs_str = Syntax.string_of_term ctxt (Thm.term_of (Thm.lhs_of result)) |
105 val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result)) |
105 val rhs_str = Syntax.string_of_term ctxt (Thm.term_of (Thm.rhs_of result)) |
106 in |
106 in |
107 warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) |
107 warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) |
108 end |
108 end |
109 |
109 |
110 fun trace_conv ctxt conv ctrm = |
110 fun trace_conv ctxt conv ctrm = |
118 |
118 |
119 (* this conversion always fails, but prints |
119 (* this conversion always fails, but prints |
120 out the analysed term *) |
120 out the analysed term *) |
121 fun trace_info_conv ctxt ctrm = |
121 fun trace_info_conv ctxt ctrm = |
122 let |
122 let |
123 val trm = term_of ctrm |
123 val trm = Thm.term_of ctrm |
124 val _ = case (head_of trm) of |
124 val _ = case (head_of trm) of |
125 @{const "Trueprop"} => () |
125 @{const "Trueprop"} => () |
126 | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm) |
126 | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm) |
127 in |
127 in |
128 Conv.no_conv ctrm |
128 Conv.no_conv ctrm |
129 end |
129 end |
130 |
130 |
131 (* conversion for applications *) |
131 (* conversion for applications *) |
132 fun eqvt_apply_conv ctrm = |
132 fun eqvt_apply_conv ctrm = |
133 case (term_of ctrm) of |
133 case Thm.term_of ctrm of |
134 Const (@{const_name "permute"}, _) $ _ $ (_ $ _) => |
134 Const (@{const_name "permute"}, _) $ _ $ (_ $ _) => |
135 let |
135 let |
136 val (perm, t) = Thm.dest_comb ctrm |
136 val (perm, t) = Thm.dest_comb ctrm |
137 val (_, p) = Thm.dest_comb perm |
137 val (_, p) = Thm.dest_comb perm |
138 val (f, x) = Thm.dest_comb t |
138 val (f, x) = Thm.dest_comb t |
139 val a = ctyp_of_term x; |
139 val a = Thm.ctyp_of_cterm x; |
140 val b = ctyp_of_term t; |
140 val b = Thm.ctyp_of_cterm t; |
141 val ty_insts = map SOME [b, a] |
141 val ty_insts = map SOME [b, a] |
142 val term_insts = map SOME [p, f, x] |
142 val term_insts = map SOME [p, f, x] |
143 in |
143 in |
144 Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} |
144 Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} |
145 end |
145 end |
146 | _ => Conv.no_conv ctrm |
146 | _ => Conv.no_conv ctrm |
147 |
147 |
148 (* conversion for lambdas *) |
148 (* conversion for lambdas *) |
149 fun eqvt_lambda_conv ctrm = |
149 fun eqvt_lambda_conv ctrm = |
150 case (term_of ctrm) of |
150 case Thm.term_of ctrm of |
151 Const (@{const_name "permute"}, _) $ _ $ (Abs _) => |
151 Const (@{const_name "permute"}, _) $ _ $ (Abs _) => |
152 Conv.rewr_conv @{thm eqvt_lambda} ctrm |
152 Conv.rewr_conv @{thm eqvt_lambda} ctrm |
153 | _ => Conv.no_conv ctrm |
153 | _ => Conv.no_conv ctrm |
154 |
154 |
155 |
155 |
164 fun msg trm = |
164 fun msg trm = |
165 if is_excluded excluded trm then () else |
165 if is_excluded excluded trm then () else |
166 (if strict_flag then error else warning) |
166 (if strict_flag then error else warning) |
167 ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) |
167 ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) |
168 |
168 |
169 val _ = case (term_of ctrm) of |
169 val _ = |
|
170 case Thm.term_of ctrm of |
170 Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm |
171 Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm |
171 | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm |
172 | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm |
172 | _ => () |
173 | _ => () |
173 in |
174 in |
174 Conv.all_conv ctrm |
175 Conv.all_conv ctrm |