# HG changeset patch
# User nipkow
# Date 1307020643 -7200
# Node ID 9f368cdb4b09df91ffa28149083aea4b21767154
# Parent  9675d631df3dccb9f438943e7a570b905024e694# Parent  69bc4dafcc53fdedb1dbd87af47526a45d4ffcec
merged

diff -r 69bc4dafcc53 -r 9f368cdb4b09 src/HOL/Mutabelle/lib/Tools/mutabelle
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Thu Jun 02 10:10:23 2011 +0200
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Thu Jun 02 15:17:23 2011 +0200
@@ -77,7 +77,7 @@
 mkdir -p "$MUTABELLE_OUTPUT_PATH"
 
 echo "theory Mutabelle_Test
-imports $MUTABELLE_IMPORTS
+imports \"~~/src/HOL/Library/Quickcheck_Narrowing\" $MUTABELLE_IMPORTS
 uses     
   \"$MUTABELLE_HOME/mutabelle.ML\"
   \"$MUTABELLE_HOME/mutabelle_extra.ML\"
@@ -87,7 +87,11 @@
 val mtds = [
   MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"random\") \"random\",
   MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\") \"exhaustive\",
-  MutabelleExtra.nitpick_mtd
+  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\" #> Config.put Quickcheck.finite_types false) \"exhaustive_nft\",
+  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"narrowing\" #> Config.put Quickcheck.finite_types false) \"narrowing\",
+  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"narrowing\" #> Config.put Quickcheck.finite_types false
+    #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ int}])))) \"narrowing_nat\"  
+(*  MutabelleExtra.nitpick_mtd *)
 ]
 *}
 
@@ -120,13 +124,16 @@
   cat "$MUTABELLE_OUTPUT_PATH/log" | grep "$1: $2" | wc -l
 }
 
-echo "random      : C: $(count "quickcheck_random" "GenuineCex") N: $(count "quickcheck_random" "NoCex") \
-T: $(count "quickcheck_random" "Timeout") E: $(count "quickcheck_random" "Error")"
-echo "exhaustive  : C: $(count "quickcheck_exhaustive" "GenuineCex") N: $(count "quickcheck_exhaustive" "NoCex") \
-T: $(count "quickcheck_exhaustive" "Timeout") E: $(count "quickcheck_exhaustive" "Error")"
-echo "nitpick     : C: $(count "nitpick" "GenuineCex") N: $(count "nitpick" "NoCex") \
-T: $(count "nitpick" "Timeout") E: $(count "nitpick" "Error")"
+function mk_stat() {
+  echo "$1 : C: $(count $1 "GenuineCex") N: $(count $1 "NoCex") T: $(count $1 "Timeout") E: $(count $1 "Error")"
+}
 
+mk_stat "quickcheck_random"
+mk_stat "quickcheck_exhaustive"
+mk_stat "quickcheck_exhaustive_nft"
+mk_stat "quickcheck_narrowing"
+mk_stat "quickcheck_narrowing_nat"
+mk_stat "nitpick"
 
 ## cleanup
 
diff -r 69bc4dafcc53 -r 9f368cdb4b09 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Thu Jun 02 10:10:23 2011 +0200
+++ b/src/Tools/quickcheck.ML	Thu Jun 02 15:17:23 2011 +0200
@@ -457,18 +457,21 @@
         collect_results f ts (result :: results)
     end  
 
-fun test_goal_terms lthy (limit_time, is_interactive) insts goals =
+fun test_goal_terms ctxt (limit_time, is_interactive) insts goals =
   let
     fun test_term' goal =
       case goal of
-        [(NONE, t)] => test_term lthy (limit_time, is_interactive) t
-      | ts => test_term_with_increasing_cardinality lthy (limit_time, is_interactive) (map snd ts)
-    val correct_inst_goals = instantiate_goals lthy insts goals
+        [(NONE, t)] => test_term ctxt (limit_time, is_interactive) t
+      | ts => test_term_with_increasing_cardinality ctxt (limit_time, is_interactive) (map snd ts)
+    val correct_inst_goals = instantiate_goals ctxt insts goals
   in
-    if Config.get lthy finite_types then
-      collect_results test_term' correct_inst_goals []
-    else
-      collect_results (test_term lthy (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
+    case lookup_tester ctxt (Config.get ctxt tester) of
+      SOME test_goal_terms => test_goal_terms ctxt (limit_time, is_interactive) insts goals
+    | NONE =>
+        if Config.get ctxt finite_types then
+          collect_results test_term' correct_inst_goals []
+        else
+          collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
   end;
 
 fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state =
@@ -492,9 +495,8 @@
       | SOME locale =>
         map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
           (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
-    val test_goals = the_default test_goal_terms (lookup_tester lthy (Config.get lthy tester))
   in
-    test_goals lthy (time_limit, is_interactive) insts goals
+    test_goal_terms lthy (time_limit, is_interactive) insts goals
   end
 
 (* pretty printing *)