src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
author bulwahn
Mon Dec 05 12:36:20 2011 +0100 (2011-12-05)
changeset 45763 3bb2bdf654f7
parent 45760 3b5a735897c3
child 46335 0fd9ab902b5a
permissions -rw-r--r--
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
     1 module Narrowing_Engine where {
     2 
     3 import Monad;
     4 import Control.Exception;
     5 import System.IO;
     6 import System.Exit;
     7 import qualified Generated_Code;
     8 
     9 type Pos = [Int];
    10 
    11 -- Term refinement
    12 
    13 new :: Pos -> [[Generated_Code.Narrowing_type]] -> [Generated_Code.Narrowing_term];
    14 new p ps = [ Generated_Code.Ctr c (zipWith (\i t -> Generated_Code.Var (p++[i]) t) [0..] ts)
    15            | (c, ts) <- zip [0..] ps ];
    16 
    17 refine :: Generated_Code.Narrowing_term -> Pos -> [Generated_Code.Narrowing_term];
    18 refine (Generated_Code.Var p (Generated_Code.SumOfProd ss)) [] = new p ss;
    19 refine (Generated_Code.Ctr c xs) p = map (Generated_Code.Ctr c) (refineList xs p);
    20 
    21 refineList :: [Generated_Code.Narrowing_term] -> Pos -> [[Generated_Code.Narrowing_term]];
    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 :: Generated_Code.Narrowing_term -> [Generated_Code.Narrowing_term];
    27 total (Generated_Code.Ctr c xs) = [Generated_Code.Ctr c ys | ys <- mapM total xs];
    28 total (Generated_Code.Var p (Generated_Code.SumOfProd ss)) = [y | x <- new p ss, y <- total x];
    29 
    30 -- Answers
    31 
    32 answeri :: a -> (Bool -> a -> IO b) -> (Pos -> IO b) -> IO b;
    33 answeri a known unknown =
    34   try (evaluate a) >>= (\res ->
    35      case res of
    36        Right b -> known True b
    37        Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
    38        Left e -> throw e);
    39 
    40 answer :: Bool -> Bool -> (Bool -> Bool -> IO b) -> (Pos -> IO b) -> IO b;
    41 answer genuine_only a known unknown =
    42   Control.Exception.catch (answeri a known unknown) 
    43     (\ (PatternMatchFail _) -> known False genuine_only);
    44 
    45 -- Refute
    46 
    47 str_of_list [] = "[]";
    48 str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
    49 
    50 report :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int;
    51 report genuine r xs = putStrLn ("SOME (" ++ (if genuine then "true" else "false") ++
    52   ", " ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
    53 
    54 eval :: Bool -> Bool -> (Bool -> Bool -> IO a) -> (Pos -> IO a) -> IO a;
    55 eval genuine_only p k u = answer genuine_only p k u;
    56 
    57 ref :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int;
    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)
    59   (\p -> sumMapM (ref genuine_only r) 1 (refineList xs p));
    60 
    61 refute :: Bool -> Result -> IO Int;
    62 refute genuine_only r = ref genuine_only r (args r);
    63 
    64 sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
    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 
    70 instance Show Generated_Code.Typerep where {
    71   show (Generated_Code.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
    72 };
    73 
    74 instance Show Generated_Code.Term where {
    75   show (Generated_Code.Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
    76   show (Generated_Code.App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
    77   show (Generated_Code.Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
    78   show (Generated_Code.Free s ty) = "Free (\"" ++ s ++  "\", " ++ show ty ++ ")";
    79 };
    80 
    81 data Result =
    82   Result { args     :: [Generated_Code.Narrowing_term]
    83          , showArgs :: [Generated_Code.Narrowing_term -> String]
    84          , apply_fun    :: [Generated_Code.Narrowing_term] -> Bool
    85          };
    86 
    87 data P = P (Int -> Int -> Result);
    88 
    89 run :: Testable a => ([Generated_Code.Narrowing_term] -> a) -> Int -> Int -> Result;
    90 run a = let P f = property a in f;
    91 
    92 class Testable a where {
    93   property :: ([Generated_Code.Narrowing_term] -> a) -> P;
    94 };
    95 
    96 instance Testable Bool where {
    97   property app = P $ \n d -> Result [] [] (app . reverse);
    98 };
    99 
   100 instance (Generated_Code.Partial_term_of a, Generated_Code.Narrowing a, Testable b) => Testable (a -> b) where {
   101   property f = P $ \n d ->
   102     let Generated_Code.C t c = Generated_Code.narrowing d
   103         c' = Generated_Code.conv c
   104         r = run (\(x:xs) -> f xs (c' x)) (n+1) d
   105     in  r { args = Generated_Code.Var [n] t : args r,
   106       showArgs = (show . Generated_Code.partial_term_of (Generated_Code.Type :: Generated_Code.Itself a)) : showArgs r };
   107 };
   108 
   109 -- Top-level interface
   110 
   111 depthCheck :: Testable a => Bool -> Int -> a -> IO ();
   112 depthCheck genuine_only d p =
   113   (refute genuine_only $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
   114 
   115 smallCheck :: Testable a => Bool -> Int -> a -> IO ();
   116 smallCheck genuine_only d p = mapM_ (\d -> depthCheck genuine_only d p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
   117 
   118 }