src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
changeset 45685 e2e928af750b
parent 45081 f00e52acbd42
child 45725 2987b29518aa
     1.1 --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Wed Nov 30 09:21:09 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Wed Nov 30 09:21:11 2011 +0100
     1.3 @@ -37,10 +37,10 @@
     1.4         Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
     1.5         Left e -> throw e);
     1.6  
     1.7 -answer :: Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
     1.8 -answer a known unknown =
     1.9 +answer :: Bool -> Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
    1.10 +answer potential a known unknown =
    1.11    Control.Exception.catch (answeri a known unknown) 
    1.12 -    (\ (PatternMatchFail _) -> known True);
    1.13 +    (\ (PatternMatchFail _) -> known (not potential));
    1.14  
    1.15  -- Refute
    1.16  
    1.17 @@ -50,14 +50,15 @@
    1.18  report :: Result -> [Generated_Code.Narrowing_term] -> IO Int;
    1.19  report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
    1.20  
    1.21 -eval :: Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
    1.22 -eval p k u = answer p (\p -> answer p k u) u;
    1.23 +eval :: Bool -> Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
    1.24 +eval potential p k u = answer potential p (\p -> answer potential p k u) u;
    1.25  
    1.26 -ref :: Result -> [Generated_Code.Narrowing_term] -> IO Int;
    1.27 -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));
    1.28 +ref :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int;
    1.29 +ref potential r xs = eval potential (apply_fun r xs) (\res -> if res then return 1 else report r xs)
    1.30 +  (\p -> sumMapM (ref potential r) 1 (refineList xs p));
    1.31            
    1.32 -refute :: Result -> IO Int;
    1.33 -refute r = ref r (args r);
    1.34 +refute :: Bool -> Result -> IO Int;
    1.35 +refute potential r = ref potential r (args r);
    1.36  
    1.37  sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
    1.38  sumMapM f n [] = return n;
    1.39 @@ -106,12 +107,12 @@
    1.40  
    1.41  -- Top-level interface
    1.42  
    1.43 -depthCheck :: Testable a => Int -> a -> IO ();
    1.44 -depthCheck d p =
    1.45 -  (refute $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
    1.46 +depthCheck :: Testable a => Bool -> Int -> a -> IO ();
    1.47 +depthCheck potential d p =
    1.48 +  (refute potential $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
    1.49  
    1.50 -smallCheck :: Testable a => Int -> a -> IO ();
    1.51 -smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
    1.52 +smallCheck :: Testable a => Bool -> Int -> a -> IO ();
    1.53 +smallCheck potential d p = mapM_ (\d -> depthCheck potential d p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
    1.54  
    1.55  }
    1.56