author | wenzelm |
Wed, 28 Dec 2011 13:08:18 +0100 | |
changeset 46004 | 484ef66bc3a1 |
parent 45760 | 3b5a735897c3 |
child 46335 | 0fd9ab902b5a |
permissions | -rw-r--r-- |
41933
10f254a4e5b9
adapting Main file generation for Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
1 |
module Narrowing_Engine where { |
41905 | 2 |
|
3 |
import Monad; |
|
4 |
import Control.Exception; |
|
5 |
import System.IO; |
|
6 |
import System.Exit; |
|
45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
7 |
import qualified Generated_Code; |
41905 | 8 |
|
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
9 |
type Pos = [Int]; |
41905 | 10 |
|
11 |
-- Term refinement |
|
12 |
||
45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
13 |
new :: Pos -> [[Generated_Code.Narrowing_type]] -> [Generated_Code.Narrowing_term]; |
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
14 |
new p ps = [ Generated_Code.Ctr c (zipWith (\i t -> Generated_Code.Var (p++[i]) t) [0..] ts) |
41905 | 15 |
| (c, ts) <- zip [0..] ps ]; |
16 |
||
45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
17 |
refine :: Generated_Code.Narrowing_term -> Pos -> [Generated_Code.Narrowing_term]; |
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
18 |
refine (Generated_Code.Var p (Generated_Code.SumOfProd ss)) [] = new p ss; |
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
19 |
refine (Generated_Code.Ctr c xs) p = map (Generated_Code.Ctr c) (refineList xs p); |
41905 | 20 |
|
45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
21 |
refineList :: [Generated_Code.Narrowing_term] -> Pos -> [[Generated_Code.Narrowing_term]]; |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
22 |
refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is]; |
41905 | 23 |
|
24 |
-- Find total instantiations of a partial value |
|
25 |
||
45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
26 |
total :: Generated_Code.Narrowing_term -> [Generated_Code.Narrowing_term]; |
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
27 |
total (Generated_Code.Ctr c xs) = [Generated_Code.Ctr c ys | ys <- mapM total xs]; |
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
28 |
total (Generated_Code.Var p (Generated_Code.SumOfProd ss)) = [y | x <- new p ss, y <- total x]; |
41905 | 29 |
|
30 |
-- Answers |
|
31 |
||
45725
2987b29518aa
the narrowing also indicates if counterexample is potentially spurious
bulwahn
parents:
45685
diff
changeset
|
32 |
answeri :: a -> (Bool -> a -> IO b) -> (Pos -> IO b) -> IO b; |
45003
7591039fb6b4
catch PatternMatchFail exceptions in narrowing-based quickcheck
bulwahn
parents:
44751
diff
changeset
|
33 |
answeri a known unknown = |
41905 | 34 |
try (evaluate a) >>= (\res -> |
35 |
case res of |
|
45725
2987b29518aa
the narrowing also indicates if counterexample is potentially spurious
bulwahn
parents:
45685
diff
changeset
|
36 |
Right b -> known True b |
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
37 |
Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p) |
41905 | 38 |
Left e -> throw e); |
39 |
||
45725
2987b29518aa
the narrowing also indicates if counterexample is potentially spurious
bulwahn
parents:
45685
diff
changeset
|
40 |
answer :: Bool -> Bool -> (Bool -> Bool -> IO b) -> (Pos -> IO b) -> IO b; |
45760
3b5a735897c3
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
bulwahn
parents:
45756
diff
changeset
|
41 |
answer genuine_only a known unknown = |
45003
7591039fb6b4
catch PatternMatchFail exceptions in narrowing-based quickcheck
bulwahn
parents:
44751
diff
changeset
|
42 |
Control.Exception.catch (answeri a known unknown) |
45760
3b5a735897c3
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
bulwahn
parents:
45756
diff
changeset
|
43 |
(\ (PatternMatchFail _) -> known False genuine_only); |
45003
7591039fb6b4
catch PatternMatchFail exceptions in narrowing-based quickcheck
bulwahn
parents:
44751
diff
changeset
|
44 |
|
41905 | 45 |
-- Refute |
46 |
||
47 |
str_of_list [] = "[]"; |
|
48 |
str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")"; |
|
49 |
||
45725
2987b29518aa
the narrowing also indicates if counterexample is potentially spurious
bulwahn
parents:
45685
diff
changeset
|
50 |
report :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int; |
2987b29518aa
the narrowing also indicates if counterexample is potentially spurious
bulwahn
parents:
45685
diff
changeset
|
51 |
report genuine r xs = putStrLn ("SOME (" ++ (if genuine then "true" else "false") ++ |
2987b29518aa
the narrowing also indicates if counterexample is potentially spurious
bulwahn
parents:
45685
diff
changeset
|
52 |
", " ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess; |
41905 | 53 |
|
45725
2987b29518aa
the narrowing also indicates if counterexample is potentially spurious
bulwahn
parents:
45685
diff
changeset
|
54 |
eval :: Bool -> Bool -> (Bool -> Bool -> IO a) -> (Pos -> IO a) -> IO a; |
45760
3b5a735897c3
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
bulwahn
parents:
45756
diff
changeset
|
55 |
eval genuine_only p k u = answer genuine_only p k u; |
41905 | 56 |
|
45685
e2e928af750b
quickcheck narrowing also shows potential counterexamples
bulwahn
parents:
45081
diff
changeset
|
57 |
ref :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int; |
45760
3b5a735897c3
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
bulwahn
parents:
45756
diff
changeset
|
58 |
ref genuine_only r xs = eval genuine_only (apply_fun r xs) (\genuine res -> if res then return 1 else report genuine r xs) |
3b5a735897c3
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
bulwahn
parents:
45756
diff
changeset
|
59 |
(\p -> sumMapM (ref genuine_only r) 1 (refineList xs p)); |
45756
295658b28d3b
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn
parents:
45725
diff
changeset
|
60 |
|
45685
e2e928af750b
quickcheck narrowing also shows potential counterexamples
bulwahn
parents:
45081
diff
changeset
|
61 |
refute :: Bool -> Result -> IO Int; |
45760
3b5a735897c3
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
bulwahn
parents:
45756
diff
changeset
|
62 |
refute genuine_only r = ref genuine_only r (args r); |
41905 | 63 |
|
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
64 |
sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int; |
41905 | 65 |
sumMapM f n [] = return n; |
66 |
sumMapM f n (a:as) = seq n (do m <- f a ; sumMapM f (n+m) as); |
|
67 |
||
68 |
-- Testable |
|
69 |
||
45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
70 |
instance Show Generated_Code.Typerep where { |
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
71 |
show (Generated_Code.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")"; |
41905 | 72 |
}; |
73 |
||
45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
74 |
instance Show Generated_Code.Term where { |
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
75 |
show (Generated_Code.Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")"; |
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
76 |
show (Generated_Code.App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")"; |
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
77 |
show (Generated_Code.Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")"; |
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
78 |
show (Generated_Code.Free s ty) = "Free (\"" ++ s ++ "\", " ++ show ty ++ ")"; |
41905 | 79 |
}; |
80 |
||
81 |
data Result = |
|
45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
82 |
Result { args :: [Generated_Code.Narrowing_term] |
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
83 |
, showArgs :: [Generated_Code.Narrowing_term -> String] |
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
84 |
, apply_fun :: [Generated_Code.Narrowing_term] -> Bool |
41905 | 85 |
}; |
86 |
||
41908
3bd9a21366d2
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
bulwahn
parents:
41905
diff
changeset
|
87 |
data P = P (Int -> Int -> Result); |
41905 | 88 |
|
45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
89 |
run :: Testable a => ([Generated_Code.Narrowing_term] -> a) -> Int -> Int -> Result; |
41905 | 90 |
run a = let P f = property a in f; |
91 |
||
92 |
class Testable a where { |
|
45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
93 |
property :: ([Generated_Code.Narrowing_term] -> a) -> P; |
41905 | 94 |
}; |
95 |
||
96 |
instance Testable Bool where { |
|
97 |
property app = P $ \n d -> Result [] [] (app . reverse); |
|
98 |
}; |
|
99 |
||
45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
100 |
instance (Generated_Code.Partial_term_of a, Generated_Code.Narrowing a, Testable b) => Testable (a -> b) where { |
41905 | 101 |
property f = P $ \n d -> |
45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
102 |
let Generated_Code.C t c = Generated_Code.narrowing d |
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
103 |
c' = Generated_Code.conv c |
41905 | 104 |
r = run (\(x:xs) -> f xs (c' x)) (n+1) d |
45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
105 |
in r { args = Generated_Code.Var [n] t : args r, |
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
bulwahn
parents:
45003
diff
changeset
|
106 |
showArgs = (show . Generated_Code.partial_term_of (Generated_Code.Type :: Generated_Code.Itself a)) : showArgs r }; |
41905 | 107 |
}; |
108 |
||
109 |
-- Top-level interface |
|
110 |
||
45685
e2e928af750b
quickcheck narrowing also shows potential counterexamples
bulwahn
parents:
45081
diff
changeset
|
111 |
depthCheck :: Testable a => Bool -> Int -> a -> IO (); |
45760
3b5a735897c3
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
bulwahn
parents:
45756
diff
changeset
|
112 |
depthCheck genuine_only d p = |
3b5a735897c3
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
bulwahn
parents:
45756
diff
changeset
|
113 |
(refute genuine_only $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout; |
41905 | 114 |
|
45685
e2e928af750b
quickcheck narrowing also shows potential counterexamples
bulwahn
parents:
45081
diff
changeset
|
115 |
smallCheck :: Testable a => Bool -> Int -> a -> IO (); |
45760
3b5a735897c3
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
bulwahn
parents:
45756
diff
changeset
|
116 |
smallCheck genuine_only d p = mapM_ (\d -> depthCheck genuine_only d p) [0..d] >> putStrLn ("NONE") >> hFlush stdout; |
41905 | 117 |
|
118 |
} |