41905
|
1 |
module LazySmallCheck where {
|
|
2 |
|
|
3 |
import Monad;
|
|
4 |
import Control.Exception;
|
|
5 |
import System.IO;
|
|
6 |
import System.Exit;
|
|
7 |
import Code;
|
|
8 |
|
|
9 |
type Pos = [Integer];
|
|
10 |
|
|
11 |
-- Term refinement
|
|
12 |
|
|
13 |
new :: Pos -> [[Type]] -> [Term];
|
|
14 |
new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
|
|
15 |
| (c, ts) <- zip [0..] ps ];
|
|
16 |
|
|
17 |
refine :: Term -> Pos -> [Term];
|
|
18 |
refine (Var p (SumOfProd ss)) [] = new p ss;
|
|
19 |
refine (Ctr c xs) p = map (Ctr c) (refineList xs p);
|
|
20 |
|
|
21 |
refineList :: [Term] -> Pos -> [[Term]];
|
|
22 |
refineList xs (i:is) = let (ls, x:rs) = splitAt (fromInteger i) xs in [ls ++ y:rs | y <- refine x is];
|
|
23 |
|
|
24 |
-- Find total instantiations of a partial value
|
|
25 |
|
|
26 |
total :: Term -> [Term];
|
|
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
|
|
37 |
Left (ErrorCall ('\0':p)) -> unknown (map (toInteger . fromEnum) p)
|
|
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 |
|
|
45 |
report :: Result -> [Term] -> IO Integer;
|
|
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 |
|
|
51 |
ref :: Result -> [Term] -> IO Integer;
|
|
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 |
|
|
54 |
refute :: Result -> IO Integer;
|
|
55 |
refute r = ref r (args r);
|
|
56 |
|
|
57 |
sumMapM :: (a -> IO Integer) -> Integer -> [a] -> IO Integer;
|
|
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 {
|
|
64 |
show (Typerepa c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
|
|
65 |
};
|
|
66 |
|
|
67 |
instance Show Terma where {
|
|
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 =
|
|
74 |
Result { args :: [Term]
|
|
75 |
, showArgs :: [Term -> String]
|
|
76 |
, apply_fun :: [Term] -> Bool
|
|
77 |
};
|
|
78 |
|
|
79 |
data P = P (Integer -> Integer -> Result);
|
|
80 |
|
|
81 |
run :: Testable a => ([Term] -> a) -> Integer -> Integer -> Result;
|
|
82 |
run a = let P f = property a in f;
|
|
83 |
|
|
84 |
class Testable a where {
|
|
85 |
property :: ([Term] -> a) -> P;
|
|
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 |
|
|
102 |
depthCheck :: Testable a => Integer -> a -> IO ();
|
|
103 |
depthCheck d p =
|
|
104 |
(refute $ run (const p) 0 d) >>= (\n -> putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d);
|
|
105 |
|
|
106 |
smallCheck :: Testable a => Integer -> a -> IO ();
|
|
107 |
smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE");
|
|
108 |
|
|
109 |
}
|
|
110 |
|