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