--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs Mon Dec 05 12:36:03 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs Mon Dec 05 12:36:05 2011 +0100
@@ -38,9 +38,9 @@
Left e -> throw e);
answer :: Bool -> Bool -> (Bool -> Bool -> IO b) -> (Pos -> IO b) -> IO b;
-answer potential a known unknown =
+answer genuine_only a known unknown =
Control.Exception.catch (answeri a known unknown)
- (\ (PatternMatchFail _) -> known False (not potential));
+ (\ (PatternMatchFail _) -> known False genuine_only);
-- Refute
@@ -52,14 +52,14 @@
", " ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
eval :: Bool -> Bool -> (Bool -> Bool -> IO a) -> (Pos -> IO a) -> IO a;
-eval potential p k u = answer potential p k u;
+eval genuine_only p k u = answer genuine_only p k u;
ref :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int;
-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));
+ref genuine_only r xs = eval genuine_only (apply_fun r xs) (\genuine res -> if res then return 1 else report genuine r xs)
+ (\p -> sumMapM (ref genuine_only r) 1 (refineList xs p));
refute :: Bool -> Result -> IO Int;
-refute potential r = ref potential r (args r);
+refute genuine_only r = ref genuine_only r (args r);
sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
sumMapM f n [] = return n;
@@ -109,10 +109,10 @@
-- Top-level interface
depthCheck :: Testable a => Bool -> Int -> a -> IO ();
-depthCheck potential d p =
- (refute potential $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
+depthCheck genuine_only d p =
+ (refute genuine_only $ run (const 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;
+smallCheck genuine_only d p = mapM_ (\d -> depthCheck genuine_only d p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
}
--- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs Mon Dec 05 12:36:03 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs Mon Dec 05 12:36:05 2011 +0100
@@ -57,9 +57,9 @@
Left e -> throw e
answer :: Bool -> Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
-answer potential a known unknown =
+answer genuine_only a known unknown =
Control.Exception.catch (answeri a known unknown)
- (\ (PatternMatchFail _) -> known (not potential))
+ (\ (PatternMatchFail _) -> known genuine_only)
-- Proofs and Refutation
@@ -154,19 +154,19 @@
-- refute
refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Bool -> Int -> QuantTree -> IO QuantTree
-refute exec potential d t = ref t
+refute exec genuine_only d t = ref t
where
ref t =
let path = find t in
do
- t' <- answer potential (exec (termListOf [] path)) (\b -> return (updateNode path (Eval b) t))
+ t' <- answer genuine_only (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 :: Bool -> Int -> Generated_Code.Property -> IO ()
-depthCheck potential d p = refute (checkOf p) potential d (treeOf 0 p) >>= (\t ->
+depthCheck genuine_only d p = refute (checkOf p) genuine_only d (treeOf 0 p) >>= (\t ->
case evalOf t of
Eval False -> putStrLn ("SOME (" ++ show (counterexampleOf (reifysOf p) (exampleOf 0 t)) ++ ")")
_ -> putStrLn ("NONE"))
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Dec 05 12:36:03 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Dec 05 12:36:05 2011 +0100
@@ -269,7 +269,7 @@
val _ = current_size := k
val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
(fn () => Isabelle_System.bash_output
- (executable ^ " " ^ haskell_string_of_bool (not genuine_only) ^ " " ^ string_of_int k))
+ (executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ string_of_int k))
val _ = Quickcheck.add_timing timing current_result
in
if response = "NONE\n" then