# HG changeset patch
# User bulwahn
# Date 1322641271 -3600
# Node ID e2e928af750b6fd2afee66f2110a9afa55854304
# Parent  3d6ee9c7d7ef89e4fec0c3868f68490798c2e378
quickcheck narrowing also shows potential counterexamples

diff -r 3d6ee9c7d7ef -r e2e928af750b src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Wed Nov 30 09:21:09 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Wed Nov 30 09:21:11 2011 +0100
@@ -37,10 +37,10 @@
        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 =
+answer :: Bool -> Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
+answer potential a known unknown =
   Control.Exception.catch (answeri a known unknown) 
-    (\ (PatternMatchFail _) -> known True);
+    (\ (PatternMatchFail _) -> known (not potential));
 
 -- Refute
 
@@ -50,14 +50,15 @@
 report :: Result -> [Generated_Code.Narrowing_term] -> IO Int;
 report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
 
-eval :: Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
-eval p k u = answer p (\p -> answer p k u) u;
+eval :: Bool -> Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
+eval potential p k u = answer potential p (\p -> answer potential p k u) u;
 
-ref :: Result -> [Generated_Code.Narrowing_term] -> IO Int;
-ref r xs = eval (apply_fun r xs) (\res -> if res then return 1 else report r xs) (\p -> sumMapM (ref r) 1 (refineList xs p));
+ref :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int;
+ref potential r xs = eval potential (apply_fun r xs) (\res -> if res then return 1 else report r xs)
+  (\p -> sumMapM (ref potential r) 1 (refineList xs p));
           
-refute :: Result -> IO Int;
-refute r = ref r (args r);
+refute :: Bool -> Result -> IO Int;
+refute potential r = ref potential r (args r);
 
 sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
 sumMapM f n [] = return n;
@@ -106,12 +107,12 @@
 
 -- Top-level interface
 
-depthCheck :: Testable a => Int -> a -> IO ();
-depthCheck d p =
-  (refute $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
+depthCheck :: Testable a => Bool -> Int -> a -> IO ();
+depthCheck potential d p =
+  (refute potential $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
 
-smallCheck :: Testable a => Int -> a -> IO ();
-smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
+smallCheck :: Testable a => Bool -> Int -> a -> IO ();
+smallCheck potential d p = mapM_ (\d -> depthCheck potential d p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
 
 }
 
diff -r 3d6ee9c7d7ef -r e2e928af750b src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs
--- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Wed Nov 30 09:21:09 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Wed Nov 30 09:21:11 2011 +0100
@@ -56,10 +56,10 @@
        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 =
+answer :: Bool -> Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
+answer potential a known unknown =
   Control.Exception.catch (answeri a known unknown) 
-    (\ (PatternMatchFail _) -> known True)
+    (\ (PatternMatchFail _) -> known (not potential))
 
 --  Proofs and Refutation
 
@@ -153,20 +153,20 @@
 
 -- refute
 
-refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Int -> QuantTree -> IO QuantTree
-refute exec d t = ref t
+refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Bool -> Int -> QuantTree -> IO QuantTree
+refute exec potential d t = ref t
   where
     ref t =
       let path = find t in
         do
-          t' <- answer (exec (termListOf [] path)) (\b -> return (updateNode path (Eval b) t))
+          t' <- answer potential (exec (termListOf [] path)) (\b -> return (updateNode path (Eval b) t))
             (\p -> return (if length p < d then refineTree path p t else updateNode path unknown t));
           case evalOf t' of
             UnknownValue True -> ref t'
             _ -> return t'
 
-depthCheck :: Int -> Generated_Code.Property -> IO ()
-depthCheck d p = refute (checkOf p) d (treeOf 0 p) >>= (\t -> 
+depthCheck :: Bool -> Int -> Generated_Code.Property -> IO ()
+depthCheck potential d p = refute (checkOf p) potential d (treeOf 0 p) >>= (\t -> 
   case evalOf t of
    Eval False -> putStrLn ("SOME (" ++ show (counterexampleOf (reifysOf p) (exampleOf 0 t)) ++ ")")  
    _ -> putStrLn ("NONE"))
diff -r 3d6ee9c7d7ef -r e2e928af750b src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Nov 30 09:21:09 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Nov 30 09:21:11 2011 +0100
@@ -222,7 +222,7 @@
   let val ({elapsed, ...}, result) = Timing.timing e ()
   in (result, (description, Time.toMilliseconds elapsed)) end
   
-fun value (contains_existentials, (quiet, size)) ctxt cookie (code, value_name) =
+fun value (contains_existentials, ((potential, quiet), size)) ctxt cookie (code, value_name) =
   let
     val (get, put, put_ml) = cookie
     fun message s = if quiet then () else Output.urgent_message s
@@ -242,7 +242,8 @@
           "import System;\n" ^
           "import Narrowing_Engine;\n" ^
           "import Generated_Code;\n\n" ^
-          "main = getArgs >>= \\[size] -> Narrowing_Engine.depthCheck (read size) (Generated_Code.value ())\n\n" ^
+          "main = getArgs >>= \\[potential, size] -> " ^
+          "Narrowing_Engine.depthCheck (read potential) (read size) (Generated_Code.value ())\n\n" ^
           "}\n"
         val code' = prefix "module Generated_Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
           (unprefix "module Generated_Code where {" code)
@@ -257,6 +258,7 @@
         val (result, compilation_time) =
           elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) 
         val _ = Quickcheck.add_timing compilation_time current_result
+        fun haskell_string_of_bool v = if v then "True" else "False"
         val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
         fun with_size k =
           if k > size then
@@ -266,7 +268,8 @@
               val _ = message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k)
               val _ = current_size := k
               val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
-                (fn () => Isabelle_System.bash_output (executable ^ " " ^ string_of_int k))
+                (fn () => Isabelle_System.bash_output
+                  (executable ^ " " ^ haskell_string_of_bool potential  ^ " " ^ string_of_int k))
               val _ = Quickcheck.add_timing timing current_result
             in
               if response = "NONE\n" then
@@ -415,7 +418,8 @@
   let
     fun dest_result (Quickcheck.Result r) = r 
     val opts =
-      (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.size)
+      ((Config.get ctxt Quickcheck.potential, Config.get ctxt Quickcheck.quiet),
+        Config.get ctxt Quickcheck.size)
     val thy = Proof_Context.theory_of ctxt
     val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
     val pnf_t = make_pnf_term thy t'