author | bulwahn |
Fri, 11 Mar 2011 15:21:13 +0100 | |
changeset 41933 | 10f254a4e5b9 |
parent 41925 | 4b9fdfd23752 |
child 41962 | 27a61a3266d8 |
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; |
|
7 |
import Code; |
|
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 |
||
41933
10f254a4e5b9
adapting Main file generation for Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
13 |
new :: Pos -> [[Type]] -> [Terma]; |
41905 | 14 |
new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts) |
15 |
| (c, ts) <- zip [0..] ps ]; |
|
16 |
||
41933
10f254a4e5b9
adapting Main file generation for Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
17 |
refine :: Terma -> Pos -> [Terma]; |
41905 | 18 |
refine (Var p (SumOfProd ss)) [] = new p ss; |
19 |
refine (Ctr c xs) p = map (Ctr c) (refineList xs p); |
|
20 |
||
41933
10f254a4e5b9
adapting Main file generation for Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
21 |
refineList :: [Terma] -> Pos -> [[Terma]]; |
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 |
||
41933
10f254a4e5b9
adapting Main file generation for Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
26 |
total :: Terma -> [Terma]; |
41905 | 27 |
total (Ctr c xs) = [Ctr c ys | ys <- mapM total xs]; |
28 |
total (Var p (SumOfProd ss)) = [y | x <- new p ss, y <- total x]; |
|
29 |
||
30 |
-- Answers |
|
31 |
||
32 |
answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b; |
|
33 |
answer a known unknown = |
|
34 |
try (evaluate a) >>= (\res -> |
|
35 |
case res of |
|
36 |
Right b -> known 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 |
||
40 |
-- Refute |
|
41 |
||
42 |
str_of_list [] = "[]"; |
|
43 |
str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")"; |
|
44 |
||
41933
10f254a4e5b9
adapting Main file generation for Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
45 |
report :: Result -> [Terma] -> IO Int; |
41905 | 46 |
report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) $ head [ys | ys <- mapM total xs]) ++ ")") >> hFlush stdout >> exitWith ExitSuccess; |
47 |
||
48 |
eval :: Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a; |
|
49 |
eval p k u = answer p (\p -> answer p k u) u; |
|
50 |
||
41933
10f254a4e5b9
adapting Main file generation for Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
51 |
ref :: Result -> [Terma] -> IO Int; |
41905 | 52 |
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)); |
53 |
||
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
|
54 |
refute :: Result -> IO Int; |
41905 | 55 |
refute r = ref r (args r); |
56 |
||
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
|
57 |
sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int; |
41905 | 58 |
sumMapM f n [] = return n; |
59 |
sumMapM f n (a:as) = seq n (do m <- f a ; sumMapM f (n+m) as); |
|
60 |
||
61 |
-- Testable |
|
62 |
||
63 |
instance Show Typerep where { |
|
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 |
show (Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")"; |
41905 | 65 |
}; |
66 |
||
41933
10f254a4e5b9
adapting Main file generation for Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
67 |
instance Show Term where { |
41905 | 68 |
show (Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")"; |
69 |
show (App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")"; |
|
70 |
show (Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")"; |
|
71 |
}; |
|
72 |
||
73 |
data Result = |
|
41933
10f254a4e5b9
adapting Main file generation for Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
74 |
Result { args :: [Terma] |
10f254a4e5b9
adapting Main file generation for Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
75 |
, showArgs :: [Terma -> String] |
10f254a4e5b9
adapting Main file generation for Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
76 |
, apply_fun :: [Terma] -> Bool |
41905 | 77 |
}; |
78 |
||
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
|
79 |
data P = P (Int -> Int -> Result); |
41905 | 80 |
|
41933
10f254a4e5b9
adapting Main file generation for Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
81 |
run :: Testable a => ([Terma] -> a) -> Int -> Int -> Result; |
41905 | 82 |
run a = let P f = property a in f; |
83 |
||
84 |
class Testable a where { |
|
41933
10f254a4e5b9
adapting Main file generation for Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
85 |
property :: ([Terma] -> a) -> P; |
41905 | 86 |
}; |
87 |
||
88 |
instance Testable Bool where { |
|
89 |
property app = P $ \n d -> Result [] [] (app . reverse); |
|
90 |
}; |
|
91 |
||
92 |
instance (Term_of a, Serial a, Testable b) => Testable (a -> b) where { |
|
93 |
property f = P $ \n d -> |
|
94 |
let C t c = series d |
|
95 |
c' = conv c |
|
96 |
r = run (\(x:xs) -> f xs (c' x)) (n+1) d |
|
97 |
in r { args = Var [n] t : args r, showArgs = (show . term_of . c') : showArgs r }; |
|
98 |
}; |
|
99 |
||
100 |
-- Top-level interface |
|
101 |
||
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
|
102 |
depthCheck :: Testable a => Int -> a -> IO (); |
41905 | 103 |
depthCheck d p = |
104 |
(refute $ run (const p) 0 d) >>= (\n -> putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d); |
|
105 |
||
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
|
106 |
smallCheck :: Testable a => Int -> a -> IO (); |
41905 | 107 |
smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE"); |
108 |
||
109 |
} |
|
110 |