# HG changeset patch
# User bulwahn
# Date 1322774075 -3600
# Node ID 2987b29518aadf944c35841d4afe09d1d34e60c2
# Parent  1f5fc44254d73c8d4efed8edfc313f19f04a1880
the narrowing also indicates if counterexample is potentially spurious

diff -r 1f5fc44254d7 -r 2987b29518aa src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Thu Dec 01 22:14:35 2011 +0100
@@ -29,32 +29,33 @@
 
 -- Answers
 
-answeri :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
+answeri :: a -> (Bool -> a -> IO b) -> (Pos -> IO b) -> IO b;
 answeri a known unknown =
   try (evaluate a) >>= (\res ->
      case res of
-       Right b -> known b
+       Right b -> known True b
        Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
        Left e -> throw e);
 
-answer :: Bool -> Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
+answer :: Bool -> Bool -> (Bool -> Bool -> IO b) -> (Pos -> IO b) -> IO b;
 answer potential a known unknown =
   Control.Exception.catch (answeri a known unknown) 
-    (\ (PatternMatchFail _) -> known (not potential));
+    (\ (PatternMatchFail _) -> known False (not potential));
 
 -- Refute
 
 str_of_list [] = "[]";
 str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
 
-report :: Result -> [Generated_Code.Narrowing_term] -> IO Int;
-report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
+report :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int;
+report genuine r xs = putStrLn ("SOME (" ++ (if genuine then "true" else "false") ++
+  ", " ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
 
-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;
+eval :: Bool -> Bool -> (Bool -> Bool -> IO a) -> (Pos -> IO a) -> IO a;
+eval potential p k u = answer potential p (\genuine p -> answer potential p k u) u;
 
 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)
+ref potential r xs = eval potential (apply_fun r xs) (\genuine res -> if res then return 1 else report genuine r xs)
   (\p -> sumMapM (ref potential r) 1 (refineList xs p));
           
 refute :: Bool -> Result -> IO Int;
@@ -115,4 +116,3 @@
 smallCheck potential d p = mapM_ (\d -> depthCheck potential d p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
 
 }
-
diff -r 1f5fc44254d7 -r 2987b29518aa src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Dec 01 22:14:35 2011 +0100
@@ -14,7 +14,7 @@
   datatype counterexample = Universal_Counterexample of (term * counterexample)
     | Existential_Counterexample of (term * counterexample) list
     | Empty_Assignment
-  val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
+  val put_counterexample: (unit -> (bool * term list) option) -> Proof.context -> Proof.context
   val put_existential_counterexample : (unit -> counterexample option) -> Proof.context -> Proof.context
   val setup: theory -> theory
 end;
@@ -302,7 +302,7 @@
   
 structure Counterexample = Proof_Data
 (
-  type T = unit -> term list option
+  type T = unit -> (bool * term list) option
   fun init _ () = error "Counterexample"
 )
 
@@ -450,11 +450,11 @@
           Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
         val (counterexample, result) = dynamic_value_strict (false, opts)
           (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
-          thy (apfst o Option.map o map) (ensure_testable (finitize t'))
+          thy (apfst o Option.map o apsnd o map) (ensure_testable (finitize t'))
       in
         Quickcheck.Result
          {counterexample =
-           Option.map (((curry (op ~~)) (Term.add_free_names t [])) o map post_process) counterexample,
+           Option.map (((curry (op ~~)) (Term.add_free_names t [])) o map post_process o snd) counterexample,
           evaluation_terms = Option.map (K []) counterexample,
           timings = #timings (dest_result result), reports = #reports (dest_result result)}
       end