src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
author bulwahn
Fri Mar 11 15:21:13 2011 +0100 (2011-03-11)
changeset 41933 10f254a4e5b9
parent 41925 4b9fdfd23752
child 41962 27a61a3266d8
permissions -rw-r--r--
adapting Main file generation for Quickcheck_Narrowing
     1 module Narrowing_Engine where {
     2 
     3 import Monad;
     4 import Control.Exception;
     5 import System.IO;
     6 import System.Exit;
     7 import Code;
     8 
     9 type Pos = [Int];
    10 
    11 -- Term refinement
    12 
    13 new :: Pos -> [[Type]] -> [Terma];
    14 new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
    15            | (c, ts) <- zip [0..] ps ];
    16 
    17 refine :: Terma -> Pos -> [Terma];
    18 refine (Var p (SumOfProd ss)) [] = new p ss;
    19 refine (Ctr c xs) p = map (Ctr c) (refineList xs p);
    20 
    21 refineList :: [Terma] -> Pos -> [[Terma]];
    22 refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is];
    23 
    24 -- Find total instantiations of a partial value
    25 
    26 total :: Terma -> [Terma];
    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 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 -> [Terma] -> IO Int;
    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 -> [Terma] -> IO Int;
    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 Int;
    55 refute r = ref r (args r);
    56 
    57 sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
    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 (Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
    65 };
    66 
    67 instance Show Term 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     :: [Terma]
    75          , showArgs :: [Terma -> String]
    76          , apply_fun    :: [Terma] -> Bool
    77          };
    78 
    79 data P = P (Int -> Int -> Result);
    80 
    81 run :: Testable a => ([Terma] -> a) -> Int -> Int -> Result;
    82 run a = let P f = property a in f;
    83 
    84 class Testable a where {
    85   property :: ([Terma] -> 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 => Int -> 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 => Int -> a -> IO ();
   107 smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE");
   108 
   109 }
   110