making max_mutants an option that can be changed in the Mutabelle-script

--- a/src/HOL/Mutabelle/MutabelleExtra.thy	Sat Feb 11 11:36:21 2012 +0100
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Sat Feb 11 11:36:23 2012 +0100
@@ -42,7 +42,7 @@
   MutabelleExtra.thms_of false thy
   |> MutabelleExtra.take_random 200
   |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
-         @{theory} mtds thms (log_directory ^ "/" ^ name)))
+         @{theory} 50 mtds thms (log_directory ^ "/" ^ name)))
 *}
   
 

--- a/src/HOL/Mutabelle/etc/settings	Sat Feb 11 11:36:21 2012 +0100
+++ b/src/HOL/Mutabelle/etc/settings	Sat Feb 11 11:36:23 2012 +0100
@@ -4,5 +4,6 @@
 
 MUTABELLE_LOGIC=HOL
 MUTABELLE_IMPORT_THEORY=Complex_Main
+MUTABELLE_NUMBER_OF_MUTANTS=4
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$MUTABELLE_HOME/lib/Tools"

--- 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 {*

--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Feb 11 11:36:21 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Feb 11 11:36:23 2012 +0100
@@ -38,7 +38,7 @@
 val string_for_report : report -> string
 val write_report : string -> report -> unit
 val mutate_theorems_and_write_report :
-  theory -> mtd list -> thm list -> string -> unit
+  theory -> int -> mtd list -> thm list -> string -> unit
 
 val random_seed : real Unsynchronized.ref
 end;
@@ -51,7 +51,6 @@
 
 
 (* mutation options *)
-val max_mutants = 4
 val num_mutations = 1
 (* soundness check: *)
 (*val max_mutants =  10
@@ -396,7 +395,7 @@
   end
 
 (* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
-fun mutate_theorem create_entry thy mtds thm =
+fun mutate_theorem create_entry thy max_mutants mtds thm =
   let
     val exec = is_executable_thm thy thm
     val _ = tracing (if exec then "EXEC" else "NOEXEC")
@@ -434,7 +433,7 @@
   end
 
 (* theory -> mtd list -> thm list -> report *)
-val mutate_theorems = map ooo mutate_theorem
+val mutate_theorems = map oooo mutate_theorem
 
 fun string_of_mutant_subentry thy thm_name (t, results) =
   "mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^
@@ -499,7 +498,7 @@
   File.write (Path.explode file_name) o string_for_report
 
 (* theory -> mtd list -> thm list -> string -> unit *)
-fun mutate_theorems_and_write_report thy mtds thms file_name =
+fun mutate_theorems_and_write_report thy max_mutants mtds thms file_name =
   let
     val _ = Output.urgent_message "Starting Mutabelle..."
     val ctxt = Proof_Context.init_global thy
@@ -522,7 +521,7 @@
       "size: " ^ string_of_int (Config.get ctxt Quickcheck.size) ^
       "; iterations: " ^ string_of_int (Config.get ctxt Quickcheck.iterations) ^ "\n" ^
     "Isabelle environment = ISABELLE_GHC: " ^ getenv "ISABELLE_GHC" ^ "\n");
-    map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy mtds) thms;
+    map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy max_mutants mtds) thms;
     ()
   end