--- a/src/HOL/Mutabelle/lib/Tools/mutabelle Sat Feb 11 11:36:21 2012 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Sat Feb 11 11:36:23 2012 +0100
@@ -17,6 +17,7 @@
echo " -T THEORY parent theory to use (default $MUTABELLE_IMPORT_THEORY)"
echo " -O DIR output directory for test data (default $MUTABELLE_OUTPUT_PATH)"
echo " -N NUMBER number of lemmas to choose randomly, if not given all lemmas are chosen"
+ echo " -M NUMBER number of mutants for each lemma (default $MUTABELLE_NUMBER_OF_MUTANTS)"
echo
echo " THEORY is the name of the theory of which all theorems should be"
echo " mutated and tested."
@@ -31,7 +32,7 @@
MUTABELLE_IMPORTS=""
-while getopts "L:T:O:N:" OPT
+while getopts "L:T:O:N:M:" OPT
do
case "$OPT" in
L)
@@ -46,6 +47,9 @@
N)
NUMBER_OF_LEMMAS="$OPTARG"
;;
+ M)
+ MUTABELLE_NUMBER_OF_MUTANTS="$OPTARG"
+ ;;
\?)
usage
;;
@@ -95,13 +99,13 @@
ML {*
val mtds = [
MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"])) \"random\",
+ MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"]) #> Config.put Quickcheck.finite_types false) \"random_int\",
MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"])) \"exhaustive\",
- MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_no_finite_types\",
+ MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_int\",
MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types true) \"narrowing\",
- MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_no_finite_types\",
+ MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_int\",
MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false
#> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\"
-
(*, MutabelleExtra.refute_mtd, *)
, MutabelleExtra.nitpick_mtd
@@ -113,7 +117,7 @@
(MutabelleExtra.random_seed := 1.0;
MutabelleExtra.thms_of false thy $MUTABELLE_FILTER
|> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
- @{theory} mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\")))
+ @{theory} $MUTABELLE_NUMBER_OF_MUTANTS mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\")))
*}
ML {*