# HG changeset patch
# User bulwahn
# Date 1316441914 -7200
# Node ID 7591039fb6b4b07443a8daef29de88458949ea71
# Parent  df36896aae0f04676925d26910f5fc9194a0ee66
catch PatternMatchFail exceptions in narrowing-based quickcheck

diff -r df36896aae0f -r 7591039fb6b4 src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon Sep 19 16:18:33 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon Sep 19 16:18:34 2011 +0200
@@ -29,14 +29,19 @@
 
 -- Answers
 
-answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
-answer a known unknown =
+answeri :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
+answeri a known unknown =
   try (evaluate a) >>= (\res ->
      case res of
        Right b -> known b
        Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
        Left e -> throw e);
 
+answer :: Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
+answer a known unknown =
+  Control.Exception.catch (answeri a known unknown) 
+    (\ (PatternMatchFail _) -> known True);
+
 -- Refute
 
 str_of_list [] = "[]";
diff -r df36896aae0f -r 7591039fb6b4 src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs
--- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Mon Sep 19 16:18:33 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Mon Sep 19 16:18:34 2011 +0200
@@ -48,14 +48,19 @@
 
 data Answer = Known Bool | Unknown Pos deriving Show;
 
-answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b
-answer a known unknown =
+answeri :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
+answeri a known unknown =
   do res <- try (evaluate a)
      case res of
        Right b -> known b
        Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
        Left e -> throw e
 
+answer :: Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
+answer a known unknown =
+  Control.Exception.catch (answeri a known unknown) 
+    (\ (PatternMatchFail _) -> known True)
+
 --  Proofs and Refutation
 
 data Quantifier = ExistentialQ | UniversalQ