quickcheck narrowing also shows potential counterexamples
authorbulwahn
Wed Nov 30 09:21:11 2011 +0100 (2011-11-30)
changeset 45685e2e928af750b
parent 45684 3d6ee9c7d7ef
child 45686 cf22004ad55d
quickcheck narrowing also shows potential counterexamples
src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     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  
     2.1 --- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Wed Nov 30 09:21:09 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Wed Nov 30 09:21:11 2011 +0100
     2.3 @@ -56,10 +56,10 @@
     2.4         Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
     2.5         Left e -> throw e
     2.6  
     2.7 -answer :: Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
     2.8 -answer a known unknown =
     2.9 +answer :: Bool -> Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
    2.10 +answer potential a known unknown =
    2.11    Control.Exception.catch (answeri a known unknown) 
    2.12 -    (\ (PatternMatchFail _) -> known True)
    2.13 +    (\ (PatternMatchFail _) -> known (not potential))
    2.14  
    2.15  --  Proofs and Refutation
    2.16  
    2.17 @@ -153,20 +153,20 @@
    2.18  
    2.19  -- refute
    2.20  
    2.21 -refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Int -> QuantTree -> IO QuantTree
    2.22 -refute exec d t = ref t
    2.23 +refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Bool -> Int -> QuantTree -> IO QuantTree
    2.24 +refute exec potential d t = ref t
    2.25    where
    2.26      ref t =
    2.27        let path = find t in
    2.28          do
    2.29 -          t' <- answer (exec (termListOf [] path)) (\b -> return (updateNode path (Eval b) t))
    2.30 +          t' <- answer potential (exec (termListOf [] path)) (\b -> return (updateNode path (Eval b) t))
    2.31              (\p -> return (if length p < d then refineTree path p t else updateNode path unknown t));
    2.32            case evalOf t' of
    2.33              UnknownValue True -> ref t'
    2.34              _ -> return t'
    2.35  
    2.36 -depthCheck :: Int -> Generated_Code.Property -> IO ()
    2.37 -depthCheck d p = refute (checkOf p) d (treeOf 0 p) >>= (\t -> 
    2.38 +depthCheck :: Bool -> Int -> Generated_Code.Property -> IO ()
    2.39 +depthCheck potential d p = refute (checkOf p) potential d (treeOf 0 p) >>= (\t -> 
    2.40    case evalOf t of
    2.41     Eval False -> putStrLn ("SOME (" ++ show (counterexampleOf (reifysOf p) (exampleOf 0 t)) ++ ")")  
    2.42     _ -> putStrLn ("NONE"))
     3.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Nov 30 09:21:09 2011 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Nov 30 09:21:11 2011 +0100
     3.3 @@ -222,7 +222,7 @@
     3.4    let val ({elapsed, ...}, result) = Timing.timing e ()
     3.5    in (result, (description, Time.toMilliseconds elapsed)) end
     3.6    
     3.7 -fun value (contains_existentials, (quiet, size)) ctxt cookie (code, value_name) =
     3.8 +fun value (contains_existentials, ((potential, quiet), size)) ctxt cookie (code, value_name) =
     3.9    let
    3.10      val (get, put, put_ml) = cookie
    3.11      fun message s = if quiet then () else Output.urgent_message s
    3.12 @@ -242,7 +242,8 @@
    3.13            "import System;\n" ^
    3.14            "import Narrowing_Engine;\n" ^
    3.15            "import Generated_Code;\n\n" ^
    3.16 -          "main = getArgs >>= \\[size] -> Narrowing_Engine.depthCheck (read size) (Generated_Code.value ())\n\n" ^
    3.17 +          "main = getArgs >>= \\[potential, size] -> " ^
    3.18 +          "Narrowing_Engine.depthCheck (read potential) (read size) (Generated_Code.value ())\n\n" ^
    3.19            "}\n"
    3.20          val code' = prefix "module Generated_Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
    3.21            (unprefix "module Generated_Code where {" code)
    3.22 @@ -257,6 +258,7 @@
    3.23          val (result, compilation_time) =
    3.24            elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) 
    3.25          val _ = Quickcheck.add_timing compilation_time current_result
    3.26 +        fun haskell_string_of_bool v = if v then "True" else "False"
    3.27          val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
    3.28          fun with_size k =
    3.29            if k > size then
    3.30 @@ -266,7 +268,8 @@
    3.31                val _ = message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k)
    3.32                val _ = current_size := k
    3.33                val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
    3.34 -                (fn () => Isabelle_System.bash_output (executable ^ " " ^ string_of_int k))
    3.35 +                (fn () => Isabelle_System.bash_output
    3.36 +                  (executable ^ " " ^ haskell_string_of_bool potential  ^ " " ^ string_of_int k))
    3.37                val _ = Quickcheck.add_timing timing current_result
    3.38              in
    3.39                if response = "NONE\n" then
    3.40 @@ -415,7 +418,8 @@
    3.41    let
    3.42      fun dest_result (Quickcheck.Result r) = r 
    3.43      val opts =
    3.44 -      (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.size)
    3.45 +      ((Config.get ctxt Quickcheck.potential, Config.get ctxt Quickcheck.quiet),
    3.46 +        Config.get ctxt Quickcheck.size)
    3.47      val thy = Proof_Context.theory_of ctxt
    3.48      val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
    3.49      val pnf_t = make_pnf_term thy t'