src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
changeset 45760 3b5a735897c3
parent 45756 295658b28d3b
child 46335 0fd9ab902b5a
--- 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;
 
 }