src/HOL/Mutabelle/lib/Tools/mutabelle

--- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Fri Jan 20 09:28:54 2012 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Mon Jan 23 11:59:00 2012 +0100
@@ -16,6 +16,7 @@
   echo "    -L LOGIC     parent logic to use (default $MUTABELLE_LOGIC)"
   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
   echo "  THEORY is the name of the theory of which all theorems should be"
   echo "  mutated and tested."
@@ -30,7 +31,7 @@
 
 MUTABELLE_IMPORTS=""
 
-while getopts "L:T:O:" OPT
+while getopts "L:T:O:N:" OPT
 do
   case "$OPT" in
     L)
@@ -42,6 +43,9 @@
     O)      
       MUTABELLE_OUTPUT_PATH="$OPTARG"
       ;;
+    N)
+      NUMBER_OF_LEMMAS="$OPTARG"
+      ;;
     \?)
       usage
       ;;
@@ -66,6 +70,9 @@
 
 export MUTABELLE_OUTPUT_PATH
 
+if [ "$NUMBER_OF_LEMMAS" != "" ]; then
+  MUTABELLE_FILTER="|> MutabelleExtra.take_random $NUMBER_OF_LEMMAS"
+fi
 
 ## main
 
@@ -104,7 +111,7 @@
 ML {*
 fun mutation_testing_of thy =
   (MutabelleExtra.random_seed := 1.0;
-  MutabelleExtra.thms_of false thy
+  MutabelleExtra.thms_of false thy $MUTABELLE_FILTER 
   |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
          @{theory} mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\")))
 *}