# HG changeset patch
# User bulwahn
# Date 1328958788 -3600
# Node ID d72ab6bf6e6dc69fa74fb7b2292115312f0cad5f
# Parent  9e83b7c24b05bb7923d3b9713a06e611158ec6fc
making num_mutations a configuration that can be changed with the mutabelle bash command

diff -r 9e83b7c24b05 -r d72ab6bf6e6d src/HOL/Mutabelle/MutabelleExtra.thy
--- a/src/HOL/Mutabelle/MutabelleExtra.thy	Sat Feb 11 11:36:23 2012 +0100
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Sat Feb 11 12:13:08 2012 +0100
@@ -42,7 +42,7 @@
   MutabelleExtra.thms_of false thy
   |> MutabelleExtra.take_random 200
   |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
-         @{theory} 50 mtds thms (log_directory ^ "/" ^ name)))
+         @{theory} (1, 50) mtds thms (log_directory ^ "/" ^ name)))
 *}
   
 
diff -r 9e83b7c24b05 -r d72ab6bf6e6d src/HOL/Mutabelle/etc/settings
--- a/src/HOL/Mutabelle/etc/settings	Sat Feb 11 11:36:23 2012 +0100
+++ b/src/HOL/Mutabelle/etc/settings	Sat Feb 11 12:13:08 2012 +0100
@@ -5,5 +5,6 @@
 MUTABELLE_LOGIC=HOL
 MUTABELLE_IMPORT_THEORY=Complex_Main
 MUTABELLE_NUMBER_OF_MUTANTS=4
+MUTABELLE_NUMBER_OF_MUTATIONS=1
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$MUTABELLE_HOME/lib/Tools"
diff -r 9e83b7c24b05 -r d72ab6bf6e6d src/HOL/Mutabelle/lib/Tools/mutabelle
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Sat Feb 11 11:36:23 2012 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Sat Feb 11 12:13:08 2012 +0100
@@ -18,6 +18,7 @@
   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 "    -X NUMBER    number of mutations in a mutant  (default $MUTABELLE_NUMBER_OF_MUTATIONS)"
   echo
   echo "  THEORY is the name of the theory of which all theorems should be"
   echo "  mutated and tested."
@@ -32,7 +33,7 @@
 
 MUTABELLE_IMPORTS=""
 
-while getopts "L:T:O:N:M:" OPT
+while getopts "L:T:O:N:M:X:" OPT
 do
   case "$OPT" in
     L)
@@ -50,6 +51,9 @@
     M)
       MUTABELLE_NUMBER_OF_MUTANTS="$OPTARG"
       ;;
+    X)
+      MUTABELLE_NUMBER_OF_MUTATIONS="$OPTARG"
+      ;;
     \?)
       usage
       ;;
@@ -117,7 +121,7 @@
   (MutabelleExtra.random_seed := 1.0;
   MutabelleExtra.thms_of false thy $MUTABELLE_FILTER 
   |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
-         @{theory} $MUTABELLE_NUMBER_OF_MUTANTS mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\")))
+         @{theory} ($MUTABELLE_NUMBER_OF_MUTATIONS, $MUTABELLE_NUMBER_OF_MUTANTS) mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\")))
 *}
 
 ML {*
diff -r 9e83b7c24b05 -r d72ab6bf6e6d src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Feb 11 11:36:23 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Feb 11 12:13:08 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 -> int -> mtd list -> thm list -> string -> unit
+  theory -> int * int -> mtd list -> thm list -> string -> unit
 
 val random_seed : real Unsynchronized.ref
 end;
@@ -49,16 +49,6 @@
 (* Own seed; can't rely on the Isabelle one to stay the same *)
 val random_seed = Unsynchronized.ref 1.0;
 
-
-(* mutation options *)
-val num_mutations = 1
-(* soundness check: *)
-(*val max_mutants =  10
-val num_mutations = 1*)
-
-(* quickcheck options *)
-(*val quickcheck_generator = "SML"*)
-
 (* Another Random engine *)
 
 exception RANDOM;
@@ -395,7 +385,7 @@
   end
 
 (* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
-fun mutate_theorem create_entry thy max_mutants mtds thm =
+fun mutate_theorem create_entry thy (num_mutations, max_mutants) mtds thm =
   let
     val exec = is_executable_thm thy thm
     val _ = tracing (if exec then "EXEC" else "NOEXEC")
@@ -498,7 +488,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 max_mutants mtds thms file_name =
+fun mutate_theorems_and_write_report thy (num_mutations, max_mutants) mtds thms file_name =
   let
     val _ = Output.urgent_message "Starting Mutabelle..."
     val ctxt = Proof_Context.init_global thy
@@ -521,7 +511,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 max_mutants mtds) thms;
+    map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy (num_mutations, max_mutants) mtds) thms;
     ()
   end