src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
changeset 41925 4b9fdfd23752
parent 41908 3bd9a21366d2
child 41933 10f254a4e5b9
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Fri Mar 11 15:21:13 2011 +0100
     1.3 @@ -0,0 +1,110 @@
     1.4 +module LazySmallCheck where {
     1.5 +
     1.6 +import Monad;
     1.7 +import Control.Exception;
     1.8 +import System.IO;
     1.9 +import System.Exit;
    1.10 +import Code;
    1.11 +
    1.12 +type Pos = [Int];
    1.13 +
    1.14 +-- Term refinement
    1.15 +
    1.16 +new :: Pos -> [[Type]] -> [Term];
    1.17 +new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
    1.18 +           | (c, ts) <- zip [0..] ps ];
    1.19 +
    1.20 +refine :: Term -> Pos -> [Term];
    1.21 +refine (Var p (SumOfProd ss)) [] = new p ss;
    1.22 +refine (Ctr c xs) p = map (Ctr c) (refineList xs p);
    1.23 +
    1.24 +refineList :: [Term] -> Pos -> [[Term]];
    1.25 +refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is];
    1.26 +
    1.27 +-- Find total instantiations of a partial value
    1.28 +
    1.29 +total :: Term -> [Term];
    1.30 +total (Ctr c xs) = [Ctr c ys | ys <- mapM total xs];
    1.31 +total (Var p (SumOfProd ss)) = [y | x <- new p ss, y <- total x];
    1.32 +
    1.33 +-- Answers
    1.34 +
    1.35 +answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
    1.36 +answer a known unknown =
    1.37 +  try (evaluate a) >>= (\res ->
    1.38 +     case res of
    1.39 +       Right b -> known b
    1.40 +       Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
    1.41 +       Left e -> throw e);
    1.42 +
    1.43 +-- Refute
    1.44 +
    1.45 +str_of_list [] = "[]";
    1.46 +str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
    1.47 +
    1.48 +report :: Result -> [Term] -> IO Int;
    1.49 +report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) $ head [ys | ys <- mapM total xs]) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
    1.50 +
    1.51 +eval :: Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
    1.52 +eval p k u = answer p (\p -> answer p k u) u;
    1.53 +
    1.54 +ref :: Result -> [Term] -> IO Int;
    1.55 +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.56 +          
    1.57 +refute :: Result -> IO Int;
    1.58 +refute r = ref r (args r);
    1.59 +
    1.60 +sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
    1.61 +sumMapM f n [] = return n;
    1.62 +sumMapM f n (a:as) = seq n (do m <- f a ; sumMapM f (n+m) as);
    1.63 +
    1.64 +-- Testable
    1.65 +
    1.66 +instance Show Typerep where {
    1.67 +  show (Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
    1.68 +};
    1.69 +
    1.70 +instance Show Terma where {
    1.71 +  show (Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
    1.72 +  show (App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
    1.73 +  show (Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";  
    1.74 +};
    1.75 +
    1.76 +data Result =
    1.77 +  Result { args     :: [Term]
    1.78 +         , showArgs :: [Term -> String]
    1.79 +         , apply_fun    :: [Term] -> Bool
    1.80 +         };
    1.81 +
    1.82 +data P = P (Int -> Int -> Result);
    1.83 +
    1.84 +run :: Testable a => ([Term] -> a) -> Int -> Int -> Result;
    1.85 +run a = let P f = property a in f;
    1.86 +
    1.87 +class Testable a where {
    1.88 +  property :: ([Term] -> a) -> P;
    1.89 +};
    1.90 +
    1.91 +instance Testable Bool where {
    1.92 +  property app = P $ \n d -> Result [] [] (app . reverse);
    1.93 +};
    1.94 +
    1.95 +instance (Term_of a, Serial a, Testable b) => Testable (a -> b) where {
    1.96 +  property f = P $ \n d ->
    1.97 +    let C t c = series d
    1.98 +        c' = conv c
    1.99 +        r = run (\(x:xs) -> f xs (c' x)) (n+1) d
   1.100 +    in  r { args = Var [n] t : args r, showArgs = (show . term_of . c') : showArgs r };
   1.101 +};
   1.102 +
   1.103 +-- Top-level interface
   1.104 +
   1.105 +depthCheck :: Testable a => Int -> a -> IO ();
   1.106 +depthCheck d p =
   1.107 +  (refute $ run (const p) 0 d) >>= (\n -> putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d);
   1.108 +
   1.109 +smallCheck :: Testable a => Int -> a -> IO ();
   1.110 +smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE");
   1.111 +
   1.112 +}
   1.113 +