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