207 |
207 |
208 val nitpick_mtd = ("nitpick", invoke_nitpick) |
208 val nitpick_mtd = ("nitpick", invoke_nitpick) |
209 |
209 |
210 (* filtering forbidden theorems and mutants *) |
210 (* filtering forbidden theorems and mutants *) |
211 |
211 |
212 val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}] |
212 val comms = [\<^const_name>\<open>HOL.eq\<close>, \<^const_name>\<open>HOL.disj\<close>, \<^const_name>\<open>HOL.conj\<close>] |
213 |
213 |
214 val forbidden = |
214 val forbidden = |
215 [(* (@{const_name "power"}, "'a"), *) |
215 [(* (@{const_name "power"}, "'a"), *) |
216 (*(@{const_name induct_equal}, "'a"), |
216 (*(@{const_name induct_equal}, "'a"), |
217 (@{const_name induct_implies}, "'a"), |
217 (@{const_name induct_implies}, "'a"), |
218 (@{const_name induct_conj}, "'a"),*) |
218 (@{const_name induct_conj}, "'a"),*) |
219 (@{const_name "undefined"}, "'a"), |
219 (\<^const_name>\<open>undefined\<close>, "'a"), |
220 (@{const_name "default"}, "'a"), |
220 (\<^const_name>\<open>default\<close>, "'a"), |
221 (@{const_name "Pure.dummy_pattern"}, "'a::{}"), |
221 (\<^const_name>\<open>Pure.dummy_pattern\<close>, "'a::{}"), |
222 (@{const_name "HOL.simp_implies"}, "prop => prop => prop"), |
222 (\<^const_name>\<open>HOL.simp_implies\<close>, "prop => prop => prop"), |
223 (@{const_name "bot_fun_inst.bot_fun"}, "'a"), |
223 (\<^const_name>\<open>bot_fun_inst.bot_fun\<close>, "'a"), |
224 (@{const_name "top_fun_inst.top_fun"}, "'a"), |
224 (\<^const_name>\<open>top_fun_inst.top_fun\<close>, "'a"), |
225 (@{const_name "Pure.term"}, "'a"), |
225 (\<^const_name>\<open>Pure.term\<close>, "'a"), |
226 (@{const_name "top_class.top"}, "'a"), |
226 (\<^const_name>\<open>top_class.top\<close>, "'a"), |
227 (@{const_name "Quotient.Quot_True"}, "'a")(*, |
227 (\<^const_name>\<open>Quotient.Quot_True\<close>, "'a")(*, |
228 (@{const_name "uminus"}, "'a"), |
228 (@{const_name "uminus"}, "'a"), |
229 (@{const_name "Nat.size"}, "'a"), |
229 (@{const_name "Nat.size"}, "'a"), |
230 (@{const_name "Groups.abs"}, "'a") *)] |
230 (@{const_name "Groups.abs"}, "'a") *)] |
231 |
231 |
232 val forbidden_thms = |
232 val forbidden_thms = |
233 ["finite_intvl_succ_class", |
233 ["finite_intvl_succ_class", |
234 "nibble"] |
234 "nibble"] |
235 |
235 |
236 val forbidden_consts = [@{const_name Pure.type}] |
236 val forbidden_consts = [\<^const_name>\<open>Pure.type\<close>] |
237 |
237 |
238 fun is_forbidden_theorem (s, th) = |
238 fun is_forbidden_theorem (s, th) = |
239 let val consts = Term.add_const_names (Thm.prop_of th) [] in |
239 let val consts = Term.add_const_names (Thm.prop_of th) [] in |
240 exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse |
240 exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse |
241 exists (member (op =) forbidden_consts) consts orelse |
241 exists (member (op =) forbidden_consts) consts orelse |
245 String.isSuffix "_raw" s orelse |
245 String.isSuffix "_raw" s orelse |
246 String.isPrefix "term_of" (List.last (Long_Name.explode s)) |
246 String.isPrefix "term_of" (List.last (Long_Name.explode s)) |
247 end |
247 end |
248 |
248 |
249 val forbidden_mutant_constnames = |
249 val forbidden_mutant_constnames = |
250 [@{const_name HOL.induct_equal}, |
250 [\<^const_name>\<open>HOL.induct_equal\<close>, |
251 @{const_name HOL.induct_implies}, |
251 \<^const_name>\<open>HOL.induct_implies\<close>, |
252 @{const_name HOL.induct_conj}, |
252 \<^const_name>\<open>HOL.induct_conj\<close>, |
253 @{const_name HOL.induct_forall}, |
253 \<^const_name>\<open>HOL.induct_forall\<close>, |
254 @{const_name undefined}, |
254 \<^const_name>\<open>undefined\<close>, |
255 @{const_name default}, |
255 \<^const_name>\<open>default\<close>, |
256 @{const_name Pure.dummy_pattern}, |
256 \<^const_name>\<open>Pure.dummy_pattern\<close>, |
257 @{const_name "HOL.simp_implies"}, |
257 \<^const_name>\<open>HOL.simp_implies\<close>, |
258 @{const_name "bot_fun_inst.bot_fun"}, |
258 \<^const_name>\<open>bot_fun_inst.bot_fun\<close>, |
259 @{const_name "top_fun_inst.top_fun"}, |
259 \<^const_name>\<open>top_fun_inst.top_fun\<close>, |
260 @{const_name "Pure.term"}, |
260 \<^const_name>\<open>Pure.term\<close>, |
261 @{const_name "top_class.top"}, |
261 \<^const_name>\<open>top_class.top\<close>, |
262 (*@{const_name "HOL.equal"},*) |
262 (*@{const_name "HOL.equal"},*) |
263 @{const_name "Quotient.Quot_True"}, |
263 \<^const_name>\<open>Quotient.Quot_True\<close>, |
264 @{const_name "equal_fun_inst.equal_fun"}, |
264 \<^const_name>\<open>equal_fun_inst.equal_fun\<close>, |
265 @{const_name "equal_bool_inst.equal_bool"}, |
265 \<^const_name>\<open>equal_bool_inst.equal_bool\<close>, |
266 @{const_name "ord_fun_inst.less_eq_fun"}, |
266 \<^const_name>\<open>ord_fun_inst.less_eq_fun\<close>, |
267 @{const_name "ord_fun_inst.less_fun"}, |
267 \<^const_name>\<open>ord_fun_inst.less_fun\<close>, |
268 @{const_name Meson.skolem}, |
268 \<^const_name>\<open>Meson.skolem\<close>, |
269 @{const_name ATP.fequal}, |
269 \<^const_name>\<open>ATP.fequal\<close>, |
270 @{const_name ATP.fEx}, |
270 \<^const_name>\<open>ATP.fEx\<close>, |
271 @{const_name enum_prod_inst.enum_all_prod}, |
271 \<^const_name>\<open>enum_prod_inst.enum_all_prod\<close>, |
272 @{const_name enum_prod_inst.enum_ex_prod}, |
272 \<^const_name>\<open>enum_prod_inst.enum_ex_prod\<close>, |
273 @{const_name Quickcheck_Random.catch_match}, |
273 \<^const_name>\<open>Quickcheck_Random.catch_match\<close>, |
274 @{const_name Quickcheck_Exhaustive.unknown}, |
274 \<^const_name>\<open>Quickcheck_Exhaustive.unknown\<close>, |
275 @{const_name Num.Bit0}, @{const_name Num.Bit1} |
275 \<^const_name>\<open>Num.Bit0\<close>, \<^const_name>\<open>Num.Bit1\<close> |
276 (*@{const_name Pure.imp}, @{const_name Pure.eq}*)] |
276 (*@{const_name Pure.imp}, @{const_name Pure.eq}*)] |
277 |
277 |
278 val forbidden_mutant_consts = |
278 val forbidden_mutant_consts = |
279 [ |
279 [ |
280 (@{const_name "Groups.zero_class.zero"}, @{typ "prop => prop => prop"}), |
280 (\<^const_name>\<open>Groups.zero_class.zero\<close>, \<^typ>\<open>prop => prop => prop\<close>), |
281 (@{const_name "Groups.one_class.one"}, @{typ "prop => prop => prop"}), |
281 (\<^const_name>\<open>Groups.one_class.one\<close>, \<^typ>\<open>prop => prop => prop\<close>), |
282 (@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}), |
282 (\<^const_name>\<open>Groups.plus_class.plus\<close>, \<^typ>\<open>prop => prop => prop\<close>), |
283 (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}), |
283 (\<^const_name>\<open>Groups.minus_class.minus\<close>, \<^typ>\<open>prop => prop => prop\<close>), |
284 (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}), |
284 (\<^const_name>\<open>Groups.times_class.times\<close>, \<^typ>\<open>prop => prop => prop\<close>), |
285 (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}), |
285 (\<^const_name>\<open>Lattices.inf_class.inf\<close>, \<^typ>\<open>prop => prop => prop\<close>), |
286 (@{const_name "Lattices.sup_class.sup"}, @{typ "prop => prop => prop"}), |
286 (\<^const_name>\<open>Lattices.sup_class.sup\<close>, \<^typ>\<open>prop => prop => prop\<close>), |
287 (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}), |
287 (\<^const_name>\<open>Orderings.bot_class.bot\<close>, \<^typ>\<open>prop => prop => prop\<close>), |
288 (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}), |
288 (\<^const_name>\<open>Orderings.ord_class.min\<close>, \<^typ>\<open>prop => prop => prop\<close>), |
289 (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}), |
289 (\<^const_name>\<open>Orderings.ord_class.max\<close>, \<^typ>\<open>prop => prop => prop\<close>), |
290 (@{const_name "Rings.modulo"}, @{typ "prop => prop => prop"}), |
290 (\<^const_name>\<open>Rings.modulo\<close>, \<^typ>\<open>prop => prop => prop\<close>), |
291 (@{const_name Rings.divide}, @{typ "prop => prop => prop"}), |
291 (\<^const_name>\<open>Rings.divide\<close>, \<^typ>\<open>prop => prop => prop\<close>), |
292 (@{const_name "GCD.gcd_class.gcd"}, @{typ "prop => prop => prop"}), |
292 (\<^const_name>\<open>GCD.gcd_class.gcd\<close>, \<^typ>\<open>prop => prop => prop\<close>), |
293 (@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}), |
293 (\<^const_name>\<open>GCD.gcd_class.lcm\<close>, \<^typ>\<open>prop => prop => prop\<close>), |
294 (@{const_name "Orderings.bot_class.bot"}, @{typ "bool => prop"}), |
294 (\<^const_name>\<open>Orderings.bot_class.bot\<close>, \<^typ>\<open>bool => prop\<close>), |
295 (@{const_name "Groups.one_class.one"}, @{typ "bool => prop"}), |
295 (\<^const_name>\<open>Groups.one_class.one\<close>, \<^typ>\<open>bool => prop\<close>), |
296 (@{const_name "Groups.zero_class.zero"},@{typ "bool => prop"}), |
296 (\<^const_name>\<open>Groups.zero_class.zero\<close>,\<^typ>\<open>bool => prop\<close>), |
297 (@{const_name "equal_class.equal"},@{typ "bool => bool => bool"})] |
297 (\<^const_name>\<open>equal_class.equal\<close>,\<^typ>\<open>bool => bool => bool\<close>)] |
298 |
298 |
299 fun is_forbidden_mutant t = |
299 fun is_forbidden_mutant t = |
300 let |
300 let |
301 val const_names = Term.add_const_names t [] |
301 val const_names = Term.add_const_names t [] |
302 val consts = Term.add_consts t [] |
302 val consts = Term.add_consts t [] |