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
bulwahn@41933
     1
module Narrowing_Engine where {
bulwahn@41905
     2
bulwahn@41905
     3
import Monad;
bulwahn@41905
     4
import Control.Exception;
bulwahn@41905
     5
import System.IO;
bulwahn@41905
     6
import System.Exit;
bulwahn@41905
     7
import Code;
bulwahn@41905
     8
bulwahn@41908
     9
type Pos = [Int];
bulwahn@41905
    10
bulwahn@41905
    11
-- Term refinement
bulwahn@41905
    12
bulwahn@41933
    13
new :: Pos -> [[Type]] -> [Terma];
bulwahn@41905
    14
new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
bulwahn@41905
    15
           | (c, ts) <- zip [0..] ps ];
bulwahn@41905
    16
bulwahn@41933
    17
refine :: Terma -> Pos -> [Terma];
bulwahn@41905
    18
refine (Var p (SumOfProd ss)) [] = new p ss;
bulwahn@41905
    19
refine (Ctr c xs) p = map (Ctr c) (refineList xs p);
bulwahn@41905
    20
bulwahn@41933
    21
refineList :: [Terma] -> Pos -> [[Terma]];
bulwahn@41908
    22
refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is];
bulwahn@41905
    23
bulwahn@41905
    24
-- Find total instantiations of a partial value
bulwahn@41905
    25
bulwahn@41933
    26
total :: Terma -> [Terma];
bulwahn@41905
    27
total (Ctr c xs) = [Ctr c ys | ys <- mapM total xs];
bulwahn@41905
    28
total (Var p (SumOfProd ss)) = [y | x <- new p ss, y <- total x];
bulwahn@41905
    29
bulwahn@41905
    30
-- Answers
bulwahn@41905
    31
bulwahn@41905
    32
answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
bulwahn@41905
    33
answer a known unknown =
bulwahn@41905
    34
  try (evaluate a) >>= (\res ->
bulwahn@41905
    35
     case res of
bulwahn@41905
    36
       Right b -> known b
bulwahn@41908
    37
       Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
bulwahn@41905
    38
       Left e -> throw e);
bulwahn@41905
    39
bulwahn@41905
    40
-- Refute
bulwahn@41905
    41
bulwahn@41905
    42
str_of_list [] = "[]";
bulwahn@41905
    43
str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
bulwahn@41905
    44
bulwahn@41933
    45
report :: Result -> [Terma] -> IO Int;
bulwahn@41905
    46
report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) $ head [ys | ys <- mapM total xs]) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
bulwahn@41905
    47
bulwahn@41905
    48
eval :: Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
bulwahn@41905
    49
eval p k u = answer p (\p -> answer p k u) u;
bulwahn@41905
    50
bulwahn@41933
    51
ref :: Result -> [Terma] -> IO Int;
bulwahn@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));
bulwahn@41905
    53
          
bulwahn@41908
    54
refute :: Result -> IO Int;
bulwahn@41905
    55
refute r = ref r (args r);
bulwahn@41905
    56
bulwahn@41908
    57
sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
bulwahn@41905
    58
sumMapM f n [] = return n;
bulwahn@41905
    59
sumMapM f n (a:as) = seq n (do m <- f a ; sumMapM f (n+m) as);
bulwahn@41905
    60
bulwahn@41905
    61
-- Testable
bulwahn@41905
    62
bulwahn@41905
    63
instance Show Typerep where {
bulwahn@41908
    64
  show (Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
bulwahn@41905
    65
};
bulwahn@41905
    66
bulwahn@41933
    67
instance Show Term where {
bulwahn@41905
    68
  show (Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
bulwahn@41905
    69
  show (App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
bulwahn@41905
    70
  show (Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";  
bulwahn@41905
    71
};
bulwahn@41905
    72
bulwahn@41905
    73
data Result =
bulwahn@41933
    74
  Result { args     :: [Terma]
bulwahn@41933
    75
         , showArgs :: [Terma -> String]
bulwahn@41933
    76
         , apply_fun    :: [Terma] -> Bool
bulwahn@41905
    77
         };
bulwahn@41905
    78
bulwahn@41908
    79
data P = P (Int -> Int -> Result);
bulwahn@41905
    80
bulwahn@41933
    81
run :: Testable a => ([Terma] -> a) -> Int -> Int -> Result;
bulwahn@41905
    82
run a = let P f = property a in f;
bulwahn@41905
    83
bulwahn@41905
    84
class Testable a where {
bulwahn@41933
    85
  property :: ([Terma] -> a) -> P;
bulwahn@41905
    86
};
bulwahn@41905
    87
bulwahn@41905
    88
instance Testable Bool where {
bulwahn@41905
    89
  property app = P $ \n d -> Result [] [] (app . reverse);
bulwahn@41905
    90
};
bulwahn@41905
    91
bulwahn@41905
    92
instance (Term_of a, Serial a, Testable b) => Testable (a -> b) where {
bulwahn@41905
    93
  property f = P $ \n d ->
bulwahn@41905
    94
    let C t c = series d
bulwahn@41905
    95
        c' = conv c
bulwahn@41905
    96
        r = run (\(x:xs) -> f xs (c' x)) (n+1) d
bulwahn@41905
    97
    in  r { args = Var [n] t : args r, showArgs = (show . term_of . c') : showArgs r };
bulwahn@41905
    98
};
bulwahn@41905
    99
bulwahn@41905
   100
-- Top-level interface
bulwahn@41905
   101
bulwahn@41908
   102
depthCheck :: Testable a => Int -> a -> IO ();
bulwahn@41905
   103
depthCheck d p =
bulwahn@41905
   104
  (refute $ run (const p) 0 d) >>= (\n -> putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d);
bulwahn@41905
   105
bulwahn@41908
   106
smallCheck :: Testable a => Int -> a -> IO ();
bulwahn@41905
   107
smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE");
bulwahn@41905
   108
bulwahn@41905
   109
}
bulwahn@41905
   110