src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
changeset 45725 2987b29518aa
parent 45685 e2e928af750b
child 45756 295658b28d3b
     1.1 --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Thu Dec 01 22:14:35 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Thu Dec 01 22:14:35 2011 +0100
     1.3 @@ -29,32 +29,33 @@
     1.4  
     1.5  -- Answers
     1.6  
     1.7 -answeri :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
     1.8 +answeri :: a -> (Bool -> a -> IO b) -> (Pos -> IO b) -> IO b;
     1.9  answeri a known unknown =
    1.10    try (evaluate a) >>= (\res ->
    1.11       case res of
    1.12 -       Right b -> known b
    1.13 +       Right b -> known True b
    1.14         Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
    1.15         Left e -> throw e);
    1.16  
    1.17 -answer :: Bool -> Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
    1.18 +answer :: Bool -> Bool -> (Bool -> Bool -> IO b) -> (Pos -> IO b) -> IO b;
    1.19  answer potential a known unknown =
    1.20    Control.Exception.catch (answeri a known unknown) 
    1.21 -    (\ (PatternMatchFail _) -> known (not potential));
    1.22 +    (\ (PatternMatchFail _) -> known False (not potential));
    1.23  
    1.24  -- Refute
    1.25  
    1.26  str_of_list [] = "[]";
    1.27  str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
    1.28  
    1.29 -report :: Result -> [Generated_Code.Narrowing_term] -> IO Int;
    1.30 -report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
    1.31 +report :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int;
    1.32 +report genuine r xs = putStrLn ("SOME (" ++ (if genuine then "true" else "false") ++
    1.33 +  ", " ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
    1.34  
    1.35 -eval :: Bool -> Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
    1.36 -eval potential p k u = answer potential p (\p -> answer potential p k u) u;
    1.37 +eval :: Bool -> Bool -> (Bool -> Bool -> IO a) -> (Pos -> IO a) -> IO a;
    1.38 +eval potential p k u = answer potential p (\genuine p -> answer potential p k u) u;
    1.39  
    1.40  ref :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int;
    1.41 -ref potential r xs = eval potential (apply_fun r xs) (\res -> if res then return 1 else report r xs)
    1.42 +ref potential r xs = eval potential (apply_fun r xs) (\genuine res -> if res then return 1 else report genuine r xs)
    1.43    (\p -> sumMapM (ref potential r) 1 (refineList xs p));
    1.44            
    1.45  refute :: Bool -> Result -> IO Int;
    1.46 @@ -115,4 +116,3 @@
    1.47  smallCheck potential d p = mapM_ (\d -> depthCheck potential d p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
    1.48  
    1.49  }
    1.50 -