inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
authorbulwahn
Mon Dec 05 12:36:05 2011 +0100 (2011-12-05)
changeset 457603b5a735897c3
parent 45759 f8cc1f6528fb
child 45761 90028fd2f1fa
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
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	Mon Dec 05 12:36:03 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon Dec 05 12:36:05 2011 +0100
     1.3 @@ -38,9 +38,9 @@
     1.4         Left e -> throw e);
     1.5  
     1.6  answer :: Bool -> Bool -> (Bool -> Bool -> IO b) -> (Pos -> IO b) -> IO b;
     1.7 -answer potential a known unknown =
     1.8 +answer genuine_only a known unknown =
     1.9    Control.Exception.catch (answeri a known unknown) 
    1.10 -    (\ (PatternMatchFail _) -> known False (not potential));
    1.11 +    (\ (PatternMatchFail _) -> known False genuine_only);
    1.12  
    1.13  -- Refute
    1.14  
    1.15 @@ -52,14 +52,14 @@
    1.16    ", " ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
    1.17  
    1.18  eval :: Bool -> Bool -> (Bool -> Bool -> IO a) -> (Pos -> IO a) -> IO a;
    1.19 -eval potential p k u = answer potential p k u;
    1.20 +eval genuine_only p k u = answer genuine_only p k u;
    1.21  
    1.22  ref :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int;
    1.23 -ref potential r xs = eval potential (apply_fun r xs) (\genuine res -> if res then return 1 else report genuine r xs)
    1.24 -  (\p -> sumMapM (ref potential r) 1 (refineList xs p));
    1.25 +ref genuine_only r xs = eval genuine_only (apply_fun r xs) (\genuine res -> if res then return 1 else report genuine r xs)
    1.26 +  (\p -> sumMapM (ref genuine_only r) 1 (refineList xs p));
    1.27  
    1.28  refute :: Bool -> Result -> IO Int;
    1.29 -refute potential r = ref potential r (args r);
    1.30 +refute genuine_only r = ref genuine_only r (args r);
    1.31  
    1.32  sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
    1.33  sumMapM f n [] = return n;
    1.34 @@ -109,10 +109,10 @@
    1.35  -- Top-level interface
    1.36  
    1.37  depthCheck :: Testable a => Bool -> Int -> a -> IO ();
    1.38 -depthCheck potential d p =
    1.39 -  (refute potential $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
    1.40 +depthCheck genuine_only d p =
    1.41 +  (refute genuine_only $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
    1.42  
    1.43  smallCheck :: Testable a => Bool -> Int -> a -> IO ();
    1.44 -smallCheck potential d p = mapM_ (\d -> depthCheck potential d p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
    1.45 +smallCheck genuine_only d p = mapM_ (\d -> depthCheck genuine_only d p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
    1.46  
    1.47  }
     2.1 --- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Mon Dec 05 12:36:03 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Mon Dec 05 12:36:05 2011 +0100
     2.3 @@ -57,9 +57,9 @@
     2.4         Left e -> throw e
     2.5  
     2.6  answer :: Bool -> Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
     2.7 -answer potential a known unknown =
     2.8 +answer genuine_only a known unknown =
     2.9    Control.Exception.catch (answeri a known unknown) 
    2.10 -    (\ (PatternMatchFail _) -> known (not potential))
    2.11 +    (\ (PatternMatchFail _) -> known genuine_only)
    2.12  
    2.13  --  Proofs and Refutation
    2.14  
    2.15 @@ -154,19 +154,19 @@
    2.16  -- refute
    2.17  
    2.18  refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Bool -> Int -> QuantTree -> IO QuantTree
    2.19 -refute exec potential d t = ref t
    2.20 +refute exec genuine_only d t = ref t
    2.21    where
    2.22      ref t =
    2.23        let path = find t in
    2.24          do
    2.25 -          t' <- answer potential (exec (termListOf [] path)) (\b -> return (updateNode path (Eval b) t))
    2.26 +          t' <- answer genuine_only (exec (termListOf [] path)) (\b -> return (updateNode path (Eval b) t))
    2.27              (\p -> return (if length p < d then refineTree path p t else updateNode path unknown t));
    2.28            case evalOf t' of
    2.29              UnknownValue True -> ref t'
    2.30              _ -> return t'
    2.31  
    2.32  depthCheck :: Bool -> Int -> Generated_Code.Property -> IO ()
    2.33 -depthCheck potential d p = refute (checkOf p) potential d (treeOf 0 p) >>= (\t -> 
    2.34 +depthCheck genuine_only d p = refute (checkOf p) genuine_only d (treeOf 0 p) >>= (\t -> 
    2.35    case evalOf t of
    2.36     Eval False -> putStrLn ("SOME (" ++ show (counterexampleOf (reifysOf p) (exampleOf 0 t)) ++ ")")  
    2.37     _ -> putStrLn ("NONE"))
     3.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Dec 05 12:36:03 2011 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Dec 05 12:36:05 2011 +0100
     3.3 @@ -269,7 +269,7 @@
     3.4                val _ = current_size := k
     3.5                val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
     3.6                  (fn () => Isabelle_System.bash_output
     3.7 -                  (executable ^ " " ^ haskell_string_of_bool (not genuine_only) ^ " " ^ string_of_int k))
     3.8 +                  (executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ string_of_int k))
     3.9                val _ = Quickcheck.add_timing timing current_result
    3.10              in
    3.11                if response = "NONE\n" then