--- a/src/HOL/Quickcheck_Narrowing.thy Thu Jun 09 08:32:18 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Thu Jun 09 08:32:19 2011 +0200
@@ -533,5 +533,6 @@
hide_type (open) code_int narrowing_type narrowing_term cons
hide_const (open) int_of of_int nth error toEnum map_index split_At empty
C cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable all exists
+hide_fact empty_def
end
\ No newline at end of file
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jun 09 08:32:18 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jun 09 08:32:19 2011 +0200
@@ -415,14 +415,16 @@
end;
fun test_goals ctxt (limit_time, is_interactive) insts goals =
- let
- val correct_inst_goals = Quickcheck.instantiate_goals ctxt insts goals
- in
- if Config.get ctxt Quickcheck.finite_types then
- error "Quickcheck-Narrowing does not support finite_types"
- else
+ if (not (getenv "ISABELLE_GHC" = "")) then
+ let
+ val correct_inst_goals = Quickcheck.instantiate_goals ctxt insts goals
+ in
Quickcheck.collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
- end
+ end
+ else
+ (if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message
+ ("Environment variable ISABELLE_GHC is not set. To use narrowing-based quickcheck, please set "
+ ^ "this variable to your GHC Haskell compiler in your settings file."); [Quickcheck.empty_result])
(* setup *)
--- a/src/Tools/quickcheck.ML Thu Jun 09 08:32:18 2011 +0200
+++ b/src/Tools/quickcheck.ML Thu Jun 09 08:32:19 2011 +0200
@@ -38,6 +38,7 @@
evaluation_terms : (term * term) list option,
timings : (string * int) list,
reports : (int * report) list}
+ val empty_result : result
val counterexample_of : result -> (string * term) list option
val timings_of : result -> (string * int) list
(* registering generators *)