changing Quickcheck_Narrowing's main function to enumerate the depth instead upto the depth
authorbulwahn
Wed Mar 23 08:50:39 2011 +0100 (2011-03-23)
changeset 42090ef566ce50170
parent 42089 904897d0c5bd
child 42091 6fe4abb9437b
changing Quickcheck_Narrowing's main function to enumerate the depth instead upto the depth
src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Wed Mar 23 08:50:32 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Wed Mar 23 08:50:39 2011 +0100
     1.3 @@ -101,10 +101,10 @@
     1.4  
     1.5  depthCheck :: Testable a => Int -> a -> IO ();
     1.6  depthCheck d p =
     1.7 -  (refute $ run (const p) 0 d) >>= (\n -> putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d);
     1.8 +  (refute $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
     1.9  
    1.10  smallCheck :: Testable a => Int -> a -> IO ();
    1.11 -smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE");
    1.12 +smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
    1.13  
    1.14  }
    1.15  
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Mar 23 08:50:32 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Mar 23 08:50:39 2011 +0100
     2.3 @@ -136,7 +136,7 @@
     2.4          val main = "module Main where {\n\n" ^
     2.5            "import Narrowing_Engine;\n" ^
     2.6            "import Code;\n\n" ^
     2.7 -          "main = Narrowing_Engine.smallCheck " ^ string_of_int size ^ " (Code.value ())\n\n" ^
     2.8 +          "main = Narrowing_Engine.depthCheck " ^ string_of_int size ^ " (Code.value ())\n\n" ^
     2.9            "}\n"
    2.10          val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
    2.11            (unprefix "module Code where {" code)