# HG changeset patch
# User bulwahn
# Date 1307601139 -7200
# Node ID a9090cabca143883150b93821d9d6c329ce1c758
# Parent  d3c34987863b6766143415d4c52fbf8938248a58
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def

diff -r d3c34987863b -r a9090cabca14 src/HOL/Quickcheck_Narrowing.thy
--- 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
diff -r d3c34987863b -r a9090cabca14 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- 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 *)
 
diff -r d3c34987863b -r a9090cabca14 src/Tools/quickcheck.ML
--- 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 *)