diff --git a/LICENSE.md b/LICENSE.md new file mode 100644 --- /dev/null +++ b/LICENSE.md @@ -0,0 +1,30 @@ +Copyright (c)2012, Lee Pike + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Lee Pike nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/examples/Div0.hs b/examples/Div0.hs new file mode 100644 --- /dev/null +++ b/examples/Div0.hs @@ -0,0 +1,95 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} + +-- | Divide by 0 example in a simple arithmetic language. + +module Div0 where + +import Test.QuickCheck +import Test.SmartCheck +import Control.Monad + +import GHC.Generics +import Data.Typeable + +----------------------------------------------------------------- + +data Exp = C Int + | Add Exp Exp + | Div Exp Exp + deriving (Read, Show, Typeable, Generic) + +instance SubTypes Exp + +eval :: Exp -> Maybe Int +eval (C i) = Just i +eval (Add e0 e1) = + liftM2 (+) (eval e0) (eval e1) +eval (Div e0 e1) = + let e = eval e1 in + if e == Just 0 then Nothing + else liftM2 div (eval e0) e + +instance Arbitrary Exp where + arbitrary = sized mkM + where + mkM 0 = liftM C arbitrary + mkM n = oneof [ liftM2 Add mkM' mkM' + , liftM2 Div mkM' mkM' ] + where mkM' = mkM =<< choose (0,n-1) + + -- shrink (C i) = map C (shrink i) + -- shrink (Add e0 e1) = [e0, e1] + -- shrink (Div e0 e1) = [e0, e1] + +-- property: so long as 0 isn't in the divisor, we won't try to divide by 0. +-- It's false: something might evaluate to 0 still. +prop_div :: Exp -> ScProperty +prop_div e = divSubTerms e --> eval e /= Nothing +-- prop_div e = property $ case x of +-- Nothing -> True +-- Just True -> True +-- _ -> False +-- where x = fmap (< 1) (eval e) + + -- precondition: no dividand in a subterm can be 0. +divSubTerms :: Exp -> Bool +divSubTerms (C _) = True +divSubTerms (Div _ (C 0)) = False +divSubTerms (Add e0 e1) = divSubTerms e0 && divSubTerms e1 +divSubTerms (Div e0 e1) = divSubTerms e0 && divSubTerms e1 + +-- div0 (A _ _) = property False +-- div0 _ = property True + +-- prop_test m = case eval m of +-- Nothing -> True +-- Just i -> i < 5 + +divTest :: IO () +divTest = smartCheck args prop_div + where + args = scStdArgs { qcArgs = stdArgs + -- { maxSuccess = 1000 + -- , maxSize = 20 } + , format = PrintString + , runForall = True + } + +-- Get the minimal offending sub-value. +findVal :: Exp -> (Exp,Exp) +findVal (Div e0 e1) + | eval e1 == Just 0 = (e0,e1) + | eval e1 == Nothing = findVal e1 + | otherwise = findVal e0 +findVal a@(Add e0 e1) + | eval e0 == Nothing = findVal e0 + | eval e1 == Nothing = findVal e1 + | eval a == Just 0 = (a,a) +findVal _ = error "not possible" + +divSubValue :: Exp +divSubValue = + Add (Div (C 5) (C (-12))) (Add (Add (C 2) (C 4)) (Add (C 7) (Div (C 3) (Add (C (-5)) (C 5))))) + +-------------------------------------------------------------------------------- diff --git a/examples/Heap_Program.hs b/examples/Heap_Program.hs new file mode 100644 --- /dev/null +++ b/examples/Heap_Program.hs @@ -0,0 +1,227 @@ +{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, DeriveDataTypeable, StandaloneDeriving #-} +{-# LANGUAGE DeriveGeneric #-} + +{-# OPTIONS_GHC -fno-warn-missing-signatures #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- Copied from QuickCheck2's examples. + +module Heap_Program where + +-------------------------------------------------------------------------- +-- imports + +import Test.QuickCheck +import Test.QuickCheck.Poly + +import Data.List + ( sort + , (\\) + ) +import Data.Typeable + +import GHC.Generics + +import qualified Test.SmartCheck as SC + +-------------------------------------------------------------------------- +-- SmartCheck Testing. Comment out shrink instance if you want to be more +-- impressed. :) +-------------------------------------------------------------------------- + +instance Read OrdA where + readsPrec _ i = [ (OrdA j, str) | (j, str) <- reads i ] + +deriving instance Typeable OrdA +deriving instance Generic OrdA + +heapProgramTest :: IO () +heapProgramTest = SC.smartCheck SC.scStdArgs (\h -> (prop_ToSortedList h)) + +instance SC.SubTypes OrdA +instance (SC.SubTypes a, Ord a, Arbitrary a, Generic a) + => SC.SubTypes (Heap a) +instance (SC.SubTypes a, Arbitrary a, Generic a) + => SC.SubTypes (HeapP a) +instance (SC.SubTypes a, Ord a, Arbitrary a, Generic a) + => SC.SubTypes (HeapPP a) + +instance (Ord a, Arbitrary a) => Arbitrary (Heap a) where + arbitrary = do p <- arbitrary :: Gen (HeapP a) + return $ heap p + +-------------------------------------------------------------------------- +-- skew heaps +-- Smallest values on top. + +data Heap a + = Node a (Heap a) (Heap a) + | Nil + deriving ( Eq, Ord, Show, Read, Typeable, Generic ) + +empty :: Heap a +empty = Nil + +isEmpty :: Heap a -> Bool +isEmpty Nil = True +isEmpty _ = False + +unit :: a -> Heap a +unit x = Node x empty empty + +size :: Heap a -> Int +size Nil = 0 +size (Node _ h1 h2) = 1 + size h1 + size h2 + +insert :: Ord a => a -> Heap a -> Heap a +insert x h = unit x `merge` h + +removeMin :: Ord a => Heap a -> Maybe (a, Heap a) +removeMin Nil = Nothing +removeMin (Node x h1 h2) = Just (x, h1 `merge` h2) + +merge :: Ord a => Heap a -> Heap a -> Heap a +h1 `merge` Nil = h1 +Nil `merge` h2 = h2 +h1@(Node x h11 h12) `merge` h2@(Node y h21 h22) + | x <= y = Node x (h12 `merge` h2) h11 + | otherwise = Node y (h22 `merge` h1) h21 + +fromList :: Ord a => [a] -> Heap a +fromList xs = merging [ unit x | x <- xs ] + where + merging [] = empty + merging [h] = h + merging hs = merging (sweep hs) + + sweep [] = [] + sweep [h] = [h] + sweep (h1:h2:hs) = (h1 `merge` h2) : sweep hs + +toList :: Heap a -> [a] +toList h = toList' [h] + where + toList' [] = [] + toList' (Nil : hs) = toList' hs + toList' (Node x h1 h2 : hs) = x : toList' (h1:h2:hs) + +toSortedList :: Ord a => Heap a -> [a] +toSortedList Nil = [] +toSortedList (Node x h1 h2) = x : toList (h1 `merge` h2) + +-------------------------------------------------------------------------- +-- heap programs + +data HeapP a + = Empty + | Unit a + | Insert a (HeapP a) + | SafeRemoveMin (HeapP a) + | Merge (HeapP a) (HeapP a) + | FromList [a] + deriving ( Show, Read, Typeable, Generic ) + +heap :: Ord a => HeapP a -> Heap a +heap Empty = empty +heap (Unit x) = unit x +heap (Insert x p) = insert x (heap p) +heap (SafeRemoveMin p) = case removeMin (heap p) of + Nothing -> empty -- arbitrary choice + Just (_,h) -> h +heap (Merge p q) = heap p `merge` heap q +heap (FromList xs) = fromList xs + +instance Arbitrary a => Arbitrary (HeapP a) where + arbitrary = sized arbHeapP + where + arbHeapP s = + frequency + [ (1, do return Empty) + , (1, do x <- arbitrary + return (Unit x)) + , (s, do x <- arbitrary + p <- arbHeapP s1 + return (Insert x p)) + , (s, do p <- arbHeapP s1 + return (SafeRemoveMin p)) + , (s, do p <- arbHeapP s2 + q <- arbHeapP s2 + return (Merge p q)) + , (1, do xs <- arbitrary + return (FromList xs)) + ] + where + s1 = s-1 + s2 = s`div`2 + + + -- shrink (Unit x) = [ Unit x' | x' <- shrink x ] + -- shrink (FromList xs) = [ Unit x | x <- xs ] + -- ++ [ FromList xs' | xs' <- shrink xs ] + -- shrink (Insert x p) = [ p ] + -- ++ [ Insert x p' | p' <- shrink p ] + -- ++ [ Insert x' p | x' <- shrink x ] + -- shrink (SafeRemoveMin p) = [ p ] + -- ++ [ SafeRemoveMin p' | p' <- shrink p ] + -- shrink (Merge p q) = [ p, q ] + -- ++ [ Merge p' q | p' <- shrink p ] + -- ++ [ Merge p q' | q' <- shrink q ] + -- shrink _ = [] + +data HeapPP a = HeapPP (HeapP a) (Heap a) + deriving ( Show, Read, Typeable, Generic ) + +instance (Ord a, Arbitrary a) => Arbitrary (HeapPP a) where + arbitrary = + do p <- arbitrary + return (HeapPP p (heap p)) + + -- shrink (HeapPP p _) = + -- [ HeapPP p' (heap p') | p' <- shrink p ] + +-------------------------------------------------------------------------- +-- properties + +(==?) :: Heap OrdA -> [OrdA] -> Bool +h ==? xs = sort (toList h) == sort xs + +prop_Empty = + empty ==? [] + +prop_IsEmpty (HeapPP _ h) = + isEmpty h == null (toList h) + +prop_Unit x = + unit x ==? [x] + +prop_Size (HeapPP _ h) = + size h == length (toList h) + +prop_Insert x (HeapPP _ h) = + insert x h ==? (x : toList h) + +prop_RemoveMin (HeapPP _ h) = + cover (size h > 1) 80 "non-trivial" $ + case removeMin h of + Nothing -> h ==? [] + Just (x,h') -> x == minimum (toList h) && h' ==? (toList h \\ [x]) + +prop_Merge (HeapPP _ h1) (HeapPP _ h2) = + (h1 `merge` h2) ==? (toList h1 ++ toList h2) + +prop_FromList xs = + fromList xs ==? xs + +prop_ToSortedList :: HeapPP OrdA -> Bool +prop_ToSortedList (HeapPP _ h) = + h ==? xs && xs == sort xs + where + xs = toSortedList h + +-------------------------------------------------------------------------- +-- main + +-- main = $(quickCheckAll) + +-------------------------------------------------------------------------- +-- the end. diff --git a/examples/LambdaCalc.hs b/examples/LambdaCalc.hs new file mode 100644 --- /dev/null +++ b/examples/LambdaCalc.hs @@ -0,0 +1,141 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} + +-- Copied from + +module LambdaCalc where + +import Data.List +import Data.Typeable + +import Control.Monad +import GHC.Generics + +import Test.QuickCheck + +import Test.SmartCheck + +type Sym = String + +data Expr + = Var Sym + | App Expr Expr + | Lam Sym Expr + deriving (Eq, Read, Show, Typeable, Generic) + +freeVars :: Expr -> [Sym] +freeVars (Var v) = [v] +freeVars (App f a) = freeVars f `union` freeVars a +freeVars (Lam i e) = freeVars e \\ [i] + +subst :: Sym -> Expr -> Expr -> Expr +subst v x b = sub b + where sub e@(Var i) = if i == v then x else e + sub (App f a) = App (sub f) (sub a) + sub (Lam i e) = + if v == i then + Lam i e + else if i `elem` fvx then + let i' = cloneSym e i + e' = substVar i i' e + in Lam i' (sub e') + else + Lam i (sub e) + fvx = freeVars x + cloneSym e i = loop i + where loop i' = if i' `elem` vs then loop (i ++ "'") else i' + vs = fvx ++ freeVars e + +substVar :: Sym -> Sym -> Expr -> Expr +substVar v v' e = subst v (Var v') e + +alphaEq :: Expr -> Expr -> Bool +alphaEq (Var v) (Var v') = v == v' +alphaEq (App f a) (App f' a') = alphaEq f f' && alphaEq a a' +alphaEq (Lam v e) (Lam v' e') = alphaEq e (substVar v' v e') +alphaEq _ _ = False + +nf :: Expr -> Expr +nf ee = spine ee [] + where spine (App f a) as = spine f (a:as) + spine (Lam v e) [] = Lam v (nf e) + spine (Lam v e) (a:as) = spine (subst v a e) as + spine f as = app f as + app f as = foldl App f (map nf as) + +betaEq :: Expr -> Expr -> Bool +betaEq e1 e2 = alphaEq (nf e1) (nf e2) + +z,s,m,n :: Expr +[z,s,m,n] = map (Var . (:[])) "zsmn" +app2 :: Expr -> Expr -> Expr -> Expr +app2 f x y = App (App f x) y +zero, one, two, three, plus :: Expr +zero = Lam "s" $ Lam "z" z +one = Lam "s" $ Lam "z" $ App s z +two = Lam "s" $ Lam "z" $ App s $ App s z +three = Lam "s" $ Lam "z" $ App s $ App s $ App s z +plus = Lam "m" $ Lam "n" $ Lam "s" $ Lam "z" $ app2 m s (app2 n s z) + +test0 :: Bool +test0 = betaEq (app2 plus one two) three + +--------------------------------------------------------------------------------- + +instance SubTypes Expr +instance SubTypes Pr + +--------------------------------------------------------------------------------- + +data Pr = Pr Expr Expr + deriving (Read, Show, Typeable, Generic) + +instance Arbitrary Expr where + arbitrary = sized mkE + where + mkE 0 = liftM Var vars + mkE x = oneof [ liftM2 App (liftM2 Lam vars mkE') mkE' + , liftM2 Lam vars mkE' + ] + where + mkE' = mkE =<< choose (0, x-1) + +vars :: Gen [Char] +vars = oneof $ map return ["x", "y", "z"] + +instance Arbitrary Pr where + arbitrary = do expr <- arbitrary + return $ Pr expr expr + +--------------------------------------------------------------------------------- + +-- prop0 :: Pr -> Property +-- prop0 (Pr (e0, e1)) = alphaEq e0 e1 ==> betaEq e0 e1 + +-- if you do a beta reduction to nf +-- prop1 :: Pr -> ScProperty +-- prop1 (Pr e0 e1) = -- Timeout due to possible non-termination +-- within 1000 $ alphaEq e0 e1 --> betaEq e0 (substVar "x" "y" e1) + +-- lambdaTest :: IO () +-- lambdaTest = smartCheck args prop1 +-- where args = scStdArgs { qcArgs = stdArgs { maxSuccess = 100 +-- , maxSize = 100 +-- } +-- } + +--------------------------------------------------------------------------------- +-- Cruft + +{- +nonDet = App x x + where + x = Lam "x" (App (Var "x") (Var "x")) + + +xx = (App (Lam "`" (App (Lam "\SI" (Var "f")) + (App (Lam "" (Var "O\172")) + (Var "3UC"))))) + +aa (Pr a b) = alphaEq a b +-} diff --git a/examples/MutualRecData.hs b/examples/MutualRecData.hs new file mode 100644 --- /dev/null +++ b/examples/MutualRecData.hs @@ -0,0 +1,60 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} + +module MutualRecData where + +import Test.SmartCheck +import Test.QuickCheck hiding (Result) + +import Data.Tree +import Control.Monad.State +import Data.Typeable + +import GHC.Generics + +-------------------------------------------------------------------------------- + +data M = M N N Int | P + deriving (Typeable, Show, Eq, Read, Generic) + +instance SubTypes M + +data N = N M Int String + deriving (Typeable, Show, Eq, Read, Generic) + +instance SubTypes N + +-------------------------------------------------------------------------------- + +instance Arbitrary M where + arbitrary = + sized $ \n -> if n == 0 then return P + else oneof [ return P + , liftM3 M (resize (n-1) arbitrary) + (resize (n-1) arbitrary) + arbitrary + ] + +instance Arbitrary N where + arbitrary = liftM3 N arbitrary arbitrary arbitrary + +-------------------------------------------------------------------------------- + +prop0 :: M -> Bool +prop0 (M _ _ a) = a < 100 +prop0 _ = True + +mutRecTest :: IO () +mutRecTest = smartCheck args prop0 + where + args = scStdArgs { qcArgs = stdArgs {maxSuccess = 1000} } + +-------------------------------------------------------------------------------- + +xx :: M +xx = M (N (M (N P 1 "goo") (N P 7 "foo") 8) 3 "hi") (N P 4 "bye") 6 +yy :: Forest Int +yy = [Node 0 [Node 1 [], Node 2 []], Node 3 [Node 4 [], Node 5 [Node 6 []]]] + +-------------------------------------------------------------------------------- diff --git a/examples/Tests.hs b/examples/Tests.hs new file mode 100644 --- /dev/null +++ b/examples/Tests.hs @@ -0,0 +1,15 @@ +module Main where + +import Div0 +import MutualRecData +import Heap_Program +--import LambdaCalc +--import Protocol + +main :: IO () +main = do + divTest + mutRecTest + heapProgramTest +-- lambdaTest +-- protocolTest diff --git a/smartcheck.cabal b/smartcheck.cabal new file mode 100644 --- /dev/null +++ b/smartcheck.cabal @@ -0,0 +1,68 @@ +Name: smartcheck +Version: 0.1 +Synopsis: A smarter QuickCheck. +Homepage: https://github.com/leepike/SmartCheck +Description: See the README.md. +License: BSD3 +License-file: LICENSE.md +Author: Lee Pike +Maintainer: leepike@gmail.com +Copyright: copyright, Lee Pike 2012. +Category: Testing +Build-type: Simple +Extra-source-files: + +Cabal-version: >=1.10 + +source-repository head + type: git + location: https://github.com/leepike/SmartCheck.git + +Library + Exposed-modules: Test.SmartCheck, + Test.SmartCheck.Args, + Test.SmartCheck.ConstructorGen, + Test.SmartCheck.DataToTree, + Test.SmartCheck.Extrapolate, + Test.SmartCheck.Matches, + Test.SmartCheck.Reduce, + Test.SmartCheck.Render, + Test.SmartCheck.SmartGen, + Test.SmartCheck.Types + + Build-depends: base >= 4.0 && < 5, + QuickCheck >= 2.6, + mtl, + random >= 1.0.1.1, + containers >= 0.4, + generic-deriving >= 1.2.1, + ghc-prim + + default-language: Haskell2010 + + hs-source-dirs: src + + ghc-options: + -Wall + -fwarn-tabs + -auto-all + -caf-all + -fno-warn-orphans + +executable sc-regression + Main-is: Tests.hs + Other-modules: Div0, + MutualRecData, + Heap_Program, + LambdaCalc + Hs-source-dirs: examples + Build-depends: base >= 4.0 && < 5, + smartcheck, + QuickCheck >= 2.4.2, + mtl, + random >= 1.0.1.1, + containers >= 0.4, + generic-deriving >= 1.2.1, + ghc-prim + Default-language: Haskell2010 + Ghc-options: -Wall diff --git a/src/Test/SmartCheck.hs b/src/Test/SmartCheck.hs new file mode 100644 --- /dev/null +++ b/src/Test/SmartCheck.hs @@ -0,0 +1,248 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE FlexibleInstances #-} + +-- | Interface module. + +module Test.SmartCheck + ( -- ** Main interface function. + smartCheck + + -- ** Type of SmartCheck properties. + , ScProperty() + -- ** Implication for SmartCheck properties. + , (-->) + + -- ** Run QuickCheck and get a result. + , runQCInit + + -- ** Arguments + , module Test.SmartCheck.Args + + -- ** Main type class based on Generics. + , SubTypes(..) + + -- ** For constructing new instances of `SubTypes` + , gst + , grc + , gtc + , gsf + , gsz + ) where + +import Test.SmartCheck.Args +import Test.SmartCheck.Types +import Test.SmartCheck.Matches +import Test.SmartCheck.Reduce +import Test.SmartCheck.Extrapolate +import Test.SmartCheck.Render +import Test.SmartCheck.ConstructorGen + +import qualified Test.QuickCheck as Q + +import Generics.Deriving + +-------------------------------------------------------------------------------- + +-- | Main interface function. +smartCheck :: forall a prop. + ( Read a, Q.Arbitrary a, SubTypes a + , Generic a, ConNames (Rep a) + , ScProp prop, Q.Testable prop + ) => ScArgs -> (a -> prop) -> IO () +smartCheck args scProp = do + -- Run standard QuickCheck or read in value. + (mcex, prop) <- + if qc args then runQCInit (qcArgs args) scProp + else do smartPrtLn "Input value to SmartCheck:" + mcex <- fmap Just (readLn :: IO a) + return (mcex, propify scProp) + + smartPrtLn $ + "(If any stage takes too long, try modifying the standard " + ++ "arguments (see Args.hs).)" + runSmartCheck prop mcex + + where + runSmartCheck :: (a -> Q.Property) -> Maybe a -> IO () + runSmartCheck origProp = smartCheck' [] origProp + where + smartCheck' :: [(a, Replace Idx)] + -> (a -> Q.Property) + -> Maybe a + -> IO () + smartCheck' ds prop mcex = do + maybe (maybeDoneMsg >> return ()) go mcex + where + go cex = do + -- Run the smart reduction algorithm. + d <- smartRun args cex prop + -- If we asked to extrapolate values, do so. + valIdxs <- forallExtrap args d origProp + -- If we asked to extrapolate constructors, do so, again with the + -- original property. + csIdxs <- existsExtrap args d valIdxs origProp + + let replIdxs = Replace valIdxs csIdxs + -- If either kind of extrapolation pass yielded fruit, prettyprint it. + showExtrapOutput args valIdxs csIdxs replIdxs d + + -- Ask the user if she wants to try again. + runAgainMsg + s <- getLine + + if s == "" + -- If so, then loop, with the new prop. + then do let oldVals = (d,replIdxs):ds + let matchesProp a = + not (matchesShapes a oldVals) + Q.==> prop a + mcex' <- runQC (qcArgs args) matchesProp + smartCheck' oldVals matchesProp mcex' + else smartPrtLn "Done." + + maybeDoneMsg = smartPrtLn "No value to smart-shrink; done." + +-------------------------------------------------------------------------------- + +existsExtrap :: (Generic a, SubTypes a, ConNames (Rep a)) + => ScArgs -> a -> [Idx] -> (a -> Q.Property) -> IO [Idx] +existsExtrap args d valIdxs origProp = + if runExists args + then constrsGen args d origProp valIdxs + else return [] + +-------------------------------------------------------------------------------- + +forallExtrap :: SubTypes a => ScArgs -> a -> (a -> Q.Property) -> IO [Idx] +forallExtrap args d origProp = + if runForall args + then -- Extrapolate with the original property to see if we + -- get a previously-visited value back. + extrapolate args d origProp + else return [] + +-------------------------------------------------------------------------------- + +showExtrapOutput :: SubTypes a1 + => ScArgs -> [a] -> [a] -> Replace Idx -> a1 -> IO () +showExtrapOutput args valIdxs csIdxs replIdxs d = + if (runForall args || runExists args) && (not $ null (valIdxs ++ csIdxs)) + then output + else smartPrtLn "Could not extrapolate a new value." + where + output = do + putStrLn "" + smartPrtLn "Extrapolated value:" + renderWithVars (format args) d replIdxs + +-------------------------------------------------------------------------------- + +runAgainMsg :: IO () +runAgainMsg = putStrLn $ + "\nAttempt to find a new counterexample?\n" + ++ " ('Enter' to continue;" + ++ " any character then 'Enter' to quit.)" + +-------------------------------------------------------------------------------- + +-- XXX I have to parse a string from QC to get the counterexamples. + +-- | Run QuickCheck initially, to get counterexamples for each argument, +-- includding the one we want to focus on for SmartCheck, plus a `Property`. +runQCInit :: (Show a, Read a, Q.Arbitrary a, ScProp prop, Q.Testable prop) + => Q.Args -> (a -> prop) -> IO (Maybe a, a -> Q.Property) +runQCInit args scProp = do + res <- Q.quickCheckWithResult args (genProp $ propify scProp) + return $ maybe + -- 2nd arg should never be evaluated if the first arg is Nothing. + (Nothing, errorMsg "Bug in runQCInit") + ((\(cex, p) -> (Just cex, p)) . parse) + (getOut res) + where + parse outs = (read $ head cexs, prop') + where cexs = lenChk ((< 2) . length) outs + prop' = propifyWithArgs (tail cexs) scProp + +-- | Run QuickCheck only analyzing the SmartCheck value, holding the other +-- values constant. +runQC :: (Show a, Read a, Q.Arbitrary a) + => Q.Args -> (a -> Q.Property) -> IO (Maybe a) +runQC args prop = do + res <- Q.quickCheckWithResult args (genProp prop) + return $ fmap parse (getOut res) + where + parse outs = read $ head cexs + where cexs = lenChk ((/= 2) . length) outs + +lenChk :: ([String] -> Bool) -> [String] -> [String] +lenChk chk ls = if chk ls then errorMsg "No value to SmartCheck!" + else tail ls + +getOut :: Q.Result -> Maybe [String] +getOut res = + case res of + Q.Failure _ _ _ _ _ _ _ out -> Just $ lines out + _ -> Nothing + +genProp :: (Show a, Q.Testable prop, Q.Arbitrary a) + => (a -> prop) -> Q.Property +genProp prop = Q.forAllShrink Q.arbitrary Q.shrink prop + +-------------------------------------------------------------------------------- + +-- | Type for SmartCheck properties. Moral equivalent of QuickCheck's +-- `Property` type. +data ScProperty = Implies (Bool, Bool) + | Simple Bool + deriving (Show, Read, Eq) + +instance Q.Testable ScProperty where + property (Simple prop) = Q.property prop + property (Implies prop) = Q.property (toQCImp prop) + exhaustive (Simple prop) = Q.exhaustive prop + exhaustive (Implies prop) = Q.exhaustive (toQCImp prop) + +-- same as ==> +infixr 0 --> +-- | Moral equivalent of QuickCheck's `==>` operator. +(-->) :: Bool -> Bool -> ScProperty +pre --> post = Implies (pre, post) + +-- Helper function. +toQCImp :: (Bool, Bool) -> Q.Property +toQCImp (pre, post) = pre Q.==> post + +-- | Turn a function that returns a `Bool` into a QuickCheck `Property`. +class ScProp prop where + scProperty :: [String] -> prop -> Q.Property + qcProperty :: prop -> Q.Property + +-- | Instance without preconditions. +instance ScProp Bool where + scProperty _ res = Q.property res + qcProperty = Q.property + +-- | Wrapped properties. +instance ScProp ScProperty where + scProperty _ (Simple res) = Q.property res + scProperty _ (Implies prop) = Q.property $ toQCImp prop + + qcProperty (Simple res) = Q.property res + qcProperty (Implies prop) = Q.property $ toQCImp prop + +-- | Beta-reduction. +instance (Q.Arbitrary a, Q.Testable prop, Show a, Read a, ScProp prop) + => ScProp (a -> prop) where + scProperty (str:strs) f = Q.property $ scProperty strs (f (read str)) + scProperty _ _ = errorMsg "Insufficient values applied to property!" + qcProperty = Q.property + +propifyWithArgs :: (Read a, ScProp prop) + => [String] -> (a -> prop) -> (a -> Q.Property) +propifyWithArgs strs prop = \a -> scProperty strs (prop a) + +propify :: ScProp prop => (a -> prop) -> (a -> Q.Property) +propify prop = \a -> qcProperty (prop a) + +-------------------------------------------------------------------------------- diff --git a/src/Test/SmartCheck/Args.hs b/src/Test/SmartCheck/Args.hs new file mode 100644 --- /dev/null +++ b/src/Test/SmartCheck/Args.hs @@ -0,0 +1,81 @@ +-- | SmartCheck arguments. + +module Test.SmartCheck.Args + ( ScArgs(..) + , scStdArgs + , Format(..) + ) where + +import qualified Test.QuickCheck as Q + +------------------------------------------------------------------------------- + +data Format = PrintTree | PrintString + deriving (Eq, Read, Show) + +data ScArgs = + ScArgs { format :: Format -- ^ How to show extrapolated formula + -------------- + , qcArgs :: Q.Args -- ^ QuickCheck arguments + -------------- + , qc :: Bool -- ^ Should we run QuickCheck? (If not, + -- you are expected to pass in data to + -- analyze.) + -------------- + , scMaxSize :: Int -- ^ Maximum size of data to generate, in + -- terms of the size parameter of + -- QuickCheck's Arbitrary instance for + -- your data. + -------------- + , scMaxDepth :: Maybe Int -- ^ How many levels into the structure of + -- the failed value should we descend + -- when reducing or generalizing? + -- Nothing means we go down to base + -- types. + -------------- + -- Reduction + , scMaxReduce :: Int -- ^ How hard (number of rounds) to look + -- for failure in the reduction stage. + -------------- + -- Extrapolation + , runForall :: Bool -- ^ Should we extrapolate? + -------------- + , scMaxForall :: Int -- ^ How hard (number of rounds) to look + -- for failures during the extrapolation + -- stage. + -------------- + , scMinForall :: Int -- ^ Minimum number of times a property's + -- precondition must be passed to + -- generalize it. + -------------- + -- Constructor generalization + , runExists :: Bool -- ^ Should we try to generalize + -- constructors? + -------------- + , scMaxExists :: Int -- ^ How hard (number of rounds) to look + -- for failing values with each + -- constructor. For "wide" sum types, this + -- value should be increased. + -------------- + } deriving (Show, Read) + +-------------------------------------------------------------------------------- + +scStdArgs :: ScArgs +scStdArgs = ScArgs { format = PrintTree + , qcArgs = Q.stdArgs + , qc = True + , scMaxSize = 10 + , scMaxDepth = Nothing + --------------------- + , scMaxReduce = 100 + --------------------- + , runForall = True + , scMaxForall = 20 + , scMinForall = 10 + --------------------- + , runExists = True + , scMaxExists = 20 + } + +-------------------------------------------------------------------------------- diff --git a/src/Test/SmartCheck/ConstructorGen.hs b/src/Test/SmartCheck/ConstructorGen.hs new file mode 100644 --- /dev/null +++ b/src/Test/SmartCheck/ConstructorGen.hs @@ -0,0 +1,107 @@ +{-# LANGUAGE FlexibleContexts #-} + +module Test.SmartCheck.ConstructorGen + ( constrsGen + ) where + +import Test.SmartCheck.Args +import Test.SmartCheck.Types +import Test.SmartCheck.DataToTree +import Test.SmartCheck.SmartGen +import Test.SmartCheck.Render + +import Prelude hiding (max) +import Generics.Deriving +import qualified Data.Set as S +import Data.List +import Control.Monad (liftM) + +import qualified Test.QuickCheck as Q + +-------------------------------------------------------------------------------- + +-- | Entry point to generalize constructors. We pass in a list of indexes from +-- value generalizations so we don't try to generalize those constructors (or +-- anything below). +constrsGen :: (SubTypes a, Generic a, ConNames (Rep a)) + => ScArgs -> a -> (a -> Q.Property) -> [Idx] -> IO [Idx] +constrsGen args d prop vs = do + putStrLn "" + smartPrtLn "Extrapolating Constructors ..." + (_, idxs) <- iter' forest (Idx 0 0) [] + return idxs + + where + forest = let forest' = mkSubstForest d True in + -- This ensures we don't try to replace anything below the indexs + -- from vs. It does NOT ensure we don't replace equal indexes. + foldl' (\f idx -> forestReplaceChildren f idx False) forest' vs + + iter' = iter d test next prop (scMaxDepth args) + + -- Check if this has been generalized already during extrapolating values. + test x idx = do res <- extrapolateConstrs args x idx prop + return $ idx `notElem` vs && res + + -- Control-flow. + next _ res forest' idx idxs = + iter' (if res then forestReplaceChildren forest' idx False else forest') + idx { column = column idx + 1 } idxs' + + where + idxs' = if res then idx : idxs else idxs + +-------------------------------------------------------------------------------- + +-- | Return True if we can generalize; False otherwise. +extrapolateConstrs :: (SubTypes a, Generic a, ConNames (Rep a)) + => ScArgs -> a -> Idx -> (a -> Q.Property) -> IO Bool +extrapolateConstrs args a idx prop = + recConstrs (S.singleton $ subConstr a idx (scMaxDepth args)) + where + notProp = Q.expectFailure . prop + allConstrs = S.fromList (conNames a) + + recConstrs :: S.Set String -> IO Bool + recConstrs constrs = + let newConstr x = subConstr x idx (scMaxDepth args) `S.insert` constrs in + -- Check if every possible constructor is an element of constrs passed in. + if allConstrs `S.isSubsetOf` constrs + then return True + else do v <- arbSubset args a idx notProp constrs + case v of + Result x -> recConstrs (newConstr x) + FailedPreCond -> return False + FailedProp -> return False + +-------------------------------------------------------------------------------- + +-- | For a value a (used just for typing), and a list of representations of +-- constructors cs, arbSubset generages a new value b, if possible, such that b +-- has the same type as a, and b's constructor is not found in cs. +-- +-- Assumes there is some new constructor to test with. +arbSubset :: (SubTypes a, Generic a, ConNames (Rep a)) + => ScArgs -> a -> Idx -> (a -> Q.Property) + -> S.Set String -> IO (Result a) +arbSubset args a idx prop constrs = + liftM snd $ iterateArbIdx a (idx, scMaxDepth args) + (scMaxExists args) (scMaxSize args) prop' + where + prop' b = newConstr b Q.==> prop b + -- Make sure b's constructor is a new one. + newConstr b = not $ subConstr b idx (scMaxDepth args) `S.member` constrs + +-------------------------------------------------------------------------------- + +-- | Get the constructor at an index in x. +subConstr :: SubTypes a => a -> Idx -> Maybe Int -> String +subConstr x idx max = + case getAtIdx x idx max of + Nothing -> errorMsg "constrs'" + Just x' -> subTconstr x' + + where + subTconstr (SubT v) = toConstr v + +-------------------------------------------------------------------------------- diff --git a/src/Test/SmartCheck/DataToTree.hs b/src/Test/SmartCheck/DataToTree.hs new file mode 100644 --- /dev/null +++ b/src/Test/SmartCheck/DataToTree.hs @@ -0,0 +1,192 @@ +{-# LANGUAGE ScopedTypeVariables #-} + +module Test.SmartCheck.DataToTree + ( forestReplaceChildren + , getAtIdx + , replaceAtIdx + , getIdxForest + , breadthLevels + , mkSubstForest + , depth + , tooDeep + ) where + +import Test.SmartCheck.Types + +import Data.Tree +import Data.List +import Data.Maybe +import Data.Typeable + +-------------------------------------------------------------------------------- +-- Operations on Trees and Forests. +-------------------------------------------------------------------------------- + +-- | Return the list of values at each level in a Forest Not like levels in +-- Data.Tree (but what I imagined it should have done!). +breadthLevels :: Forest a -> [[a]] +breadthLevels forest = + takeWhile (not . null) go + where + go = map (getLevel forest) [0..] + +-------------------------------------------------------------------------------- + +-- | Return the elements at level i from a forest. 0-based indexing. +getLevel :: Forest a -> Int -> [a] +getLevel fs 0 = map rootLabel fs +getLevel fs n = concatMap (\fs' -> getLevel (subForest fs') (n-1)) fs + +-------------------------------------------------------------------------------- + +-- | Get the depth of a Forest. 0-based (an empty Forest has depth 0). +depth :: Forest a -> Int +depth forest = if null ls then 0 else maximum ls + where + ls = map depth' forest + depth' (Node _ []) = 1 + depth' (Node _ forest') = 1 + depth forest' + +-------------------------------------------------------------------------------- + +-- | How many members are at level i in the Tree? +levelLength :: Int -> Tree a -> Int +levelLength 0 t = length (subForest t) +levelLength n t = sum $ map (levelLength (n-1)) (subForest t) + +-------------------------------------------------------------------------------- + +-- | Get the tree at idx in a forest. Nothing if the index is out-of-bounds. +getIdxForest :: Forest a -> Idx -> Maybe (Tree a) +getIdxForest forest (Idx (0 :: Int) n) = + if length forest > n then Just (forest !! n) + else Nothing +getIdxForest forest idx = + -- Should be a single Just x in the list, holding the value. + listToMaybe . catMaybes . snd $ acc + + where + acc = mapAccumL findTree (column idx) (map Just forest) + + l = level idx - 1 + -- Invariant: not at the right level yet. + findTree :: Int -> Maybe (Tree a) -> (Int, Maybe (Tree a)) + findTree n Nothing = (n, Nothing) + findTree n (Just t) = + let len = levelLength l t in + if n < 0 -- Already found index + then (n, Nothing) + else if n < len -- Big enough to index, so we climb down this one. + then let t' = getIdxForest (subForest t) (Idx l n) in + (n-len, t') + else (n-len, Nothing) + +-------------------------------------------------------------------------------- + +-- Morally, we should be using generic zippers and a nice, recursive breadth-first search function, e.g. + +{- + +data Tree = N Int Tree Tree + | E + +index :: Int -> Tree -> Tree +index = index' [] + where + index' :: [Tree] -> Int -> Tree -> Tree + index' _ 0 t = t + index' [] idx (N i t0 t1) = index' [t1] (idx-1) t0 + index' (k:ks) idx E = index' ks (idx-1) k + index' (k:ks) idx (N i t0 t1) = index' (ks ++ [t0, t1]) (idx-1) k + +-} + +-- | Returns the value at index idx. Returns nothing if the index is out of +-- bounds. +getAtIdx :: SubTypes a + => a -- ^ Value + -> Idx -- ^ Index of hole + -> Maybe Int -- ^ Maximum depth we want to extract + -> Maybe SubT +getAtIdx d Idx { level = l, column = c } maxDepth + | tooDeep l maxDepth = Nothing + | length lev > c = Just (lev !! c) + | otherwise = Nothing + where + lev = getLevel (subTypes d) l + +-------------------------------------------------------------------------------- + +tooDeep :: Int -> Maybe Int -> Bool +tooDeep l = maybe False (l >) + +-------------------------------------------------------------------------------- + +data SubStrat = Parent -- ^ Replace everything in the path from the root to + -- here. Used as breadcrumbs to the value. Chop the + -- subforest. + | Children -- ^ Replace a value and all of its subchildren. + deriving (Show, Read, Eq) + +-------------------------------------------------------------------------------- + +forestReplaceParent, forestReplaceChildren :: Forest a -> Idx -> a -> Forest a +forestReplaceParent = sub Parent +forestReplaceChildren = sub Children + +-------------------------------------------------------------------------------- + +sub :: SubStrat -> Forest a -> Idx -> a -> Forest a +-- on right level, and we'll assume correct subtree. +sub strat forest (Idx (0 :: Int) n) a = + snd $ mapAccumL f 0 forest + where + f i node | i == n = ( i+1, news ) + | otherwise = ( i+1, node ) + + where + news = case strat of + Parent -> Node a [] + Children -> fmap (const a) (forest !! n) + +sub strat forest idx a = + snd $ mapAccumL findTree (column idx) forest + where + l = level idx - 1 + -- Invariant: not at the right level yet. + findTree n t + -- Already found index + | n < 0 = (n, t) + -- Big enough to index, so we climb down this one. + | n < len = (n-len, newTree) + | otherwise = (n-len, t) + where + len = levelLength l t + newTree = Node newRootLabel (sub strat (subForest t) (Idx l n) a) + newRootLabel = case strat of + Parent -> a + Children -> rootLabel t + +-------------------------------------------------------------------------------- +-- Operations on SubTypes. +-------------------------------------------------------------------------------- + +-- | Make a substitution Forest (all proper children). Initially we don't +-- replace anything. +mkSubstForest :: SubTypes a => a -> b -> Forest b +mkSubstForest a b = map tMap (subTypes a) + where tMap = fmap (const b) + +-------------------------------------------------------------------------------- + +-- | Replace a value at index idx generically in a Tree/Forest generically. +replaceAtIdx :: (SubTypes a, Typeable b) + => a -- ^ Parent value + -> Idx -- ^ Index of hole to replace + -> b -- ^ Value to replace with + -> Maybe a +replaceAtIdx m idx = replaceChild m (forestReplaceParent subF idx Subst) + where + subF = mkSubstForest m Keep + +-------------------------------------------------------------------------------- diff --git a/src/Test/SmartCheck/Extrapolate.hs b/src/Test/SmartCheck/Extrapolate.hs new file mode 100644 --- /dev/null +++ b/src/Test/SmartCheck/Extrapolate.hs @@ -0,0 +1,60 @@ +{-# LANGUAGE ScopedTypeVariables #-} + +module Test.SmartCheck.Extrapolate + ( extrapolate + ) where + +import Test.SmartCheck.Args +import Test.SmartCheck.Types +import Test.SmartCheck.DataToTree +import Test.SmartCheck.SmartGen +import Test.SmartCheck.Render + +import qualified Test.QuickCheck as Q + +-------------------------------------------------------------------------------- + +-- | Test d with arbitrary values replacing its children. For anything we get +-- 100% failure for, we claim we can generalize it---any term in that hole +-- fails. +-- +-- We extrapolate if there exists at least one test that satisfies the +-- precondition, and for all tests that satisfy the precondition, they fail. + +-- We extrapolate w.r.t. the original property since extrapolation throws away +-- any values that fail the precondition of the property (i.e., before the +-- Q.==>). +extrapolate :: SubTypes a + => ScArgs -- ^ Arguments + -> a -- ^ Current failed value + -> (a -> Q.Property) -- ^ Original property + -> IO ([Idx]) +extrapolate args d origProp = do + putStrLn "" + smartPrtLn "Extrapolating values ..." + (_, idxs) <- iter' forest (Idx 0 0) [] + return idxs + + where + forest = mkSubstForest d True + iter' = iter d test next origProp (scMaxDepth args) + + -- In this call to iterateArb, we want to claim we can extrapolate iff at + -- least one test passes a precondition, and for every test in which the + -- precondition is passed, it fails. We test values of all possible sizes, up + -- to Q.maxSize. + test _ idx = iterateArbIdx d (idx, scMaxDepth args) (scMaxForall args) + (scMaxSize args) origProp + + -- Control-flow. + + -- None of the tries satisfy prop (but something passed the precondition). + -- Prevent recurring down this tree, since we can generalize. + next _ (i, FailedProp) forest' idx idxs + | scMinForall args < i = + nextIter (forestReplaceChildren forest' idx False) idx (idx : idxs) + next _ _ forest' idx idxs = nextIter forest' idx idxs + + nextIter f idx = iter' f idx { column = column idx + 1 } + +-------------------------------------------------------------------------------- diff --git a/src/Test/SmartCheck/Matches.hs b/src/Test/SmartCheck/Matches.hs new file mode 100644 --- /dev/null +++ b/src/Test/SmartCheck/Matches.hs @@ -0,0 +1,52 @@ +{-# LANGUAGE ScopedTypeVariables #-} + +module Test.SmartCheck.Matches + ( matchesShapes + ) where + +import Test.SmartCheck.DataToTree +import Test.SmartCheck.Types +import Test.SmartCheck.SmartGen + +import Data.List +import Data.Tree + +-------------------------------------------------------------------------------- + +-- | True if d matches any ds. Assume all ds are unequal to each other. +matchesShapes :: SubTypes a => a -> [(a,Replace Idx)] -> Bool +matchesShapes d = any (matchesShape d) + +-------------------------------------------------------------------------------- + +-- | At each index that we generalize (either value generalization or +-- constructor generalization), we replace that value from b into a. At this +-- point, we check for constructor equality between the two values, decending +-- their structures. +matchesShape :: forall a . SubTypes a => a -> (a, Replace Idx) -> Bool +matchesShape a (b, Replace idxVals idxConstrs) + | toConstr a /= toConstr b = False + | Just a' <- aRepl = let x = subTypes a' in + let y = subTypes b in + all foldEqConstrs (zip x y) + | otherwise = False + + where + foldEqConstrs :: (Tree SubT, Tree SubT) -> Bool + foldEqConstrs (Node (SubT l0) sts0, Node (SubT l1) sts1) + -- Don't need a baseType test, since they don't ever appear in subTypes. + | toConstr l0 == toConstr l1 = next + | otherwise = False + where next = all foldEqConstrs (zip sts0 sts1) + + bSub :: Idx -> Maybe SubT + bSub idx = getAtIdx b idx Nothing + + updateA :: Idx -> a -> Maybe a + updateA idx d = maybe Nothing (replace d idx) (bSub idx) + + aRepl :: Maybe a + aRepl = foldl' go (Just a) (idxVals ++ idxConstrs) + where go ma idx = maybe Nothing (updateA idx) ma + +-------------------------------------------------------------------------------- diff --git a/src/Test/SmartCheck/Reduce.hs b/src/Test/SmartCheck/Reduce.hs new file mode 100644 --- /dev/null +++ b/src/Test/SmartCheck/Reduce.hs @@ -0,0 +1,126 @@ +{-# LANGUAGE ScopedTypeVariables #-} + +module Test.SmartCheck.Reduce + (smartRun + ) where + +import Test.SmartCheck.Args +import Test.SmartCheck.Types +import Test.SmartCheck.SmartGen +import Test.SmartCheck.DataToTree +import Test.SmartCheck.Render + +import qualified Test.QuickCheck as Q + +import Data.Typeable +import Data.Tree +import Data.Maybe + +import Control.Monad (liftM) + +-------------------------------------------------------------------------------- + +-- Smarter than shrinks. Does substitution. m is a value that failed QC that's +-- been shrunk. We substitute successive children with strictly smaller (and +-- increasingly larger) randomly-generated values until we find a failure, and +-- return that result. (We call smartShrink recursively.) +smartRun :: SubTypes a => ScArgs -> a -> (a -> Q.Property) -> IO a +smartRun args res prop = do + putStrLn "" + smartPrtLn "Smart Shrinking ..." + new <- smartShrink args res prop + smartPrtLn "Smart-shrunk value:" + print new + return new + +-------------------------------------------------------------------------------- + +-- | Breadth-first traversal of d, trying to shrink it with *strictly* smaller +-- children. We replace d whenever a successful shrink is found and try again. +smartShrink :: forall a. SubTypes a => ScArgs -> a -> (a -> Q.Property) -> IO a +smartShrink args d prop = + liftM fst $ iter' d (mkForest d) (Idx 0 0) + where + mkForest x = mkSubstForest x True + notProp = Q.expectFailure . prop + + iter' x forest_ idx' = + iter x test next notProp (scMaxDepth args) forest_ idx' + (errorMsg "next-idxs") + + -------------------------------------- + + -- next tells the iter what to do after running a test. + next :: a -> Maybe a -> Forest Bool -> Idx -> [Idx] -> IO (a, [Idx]) + next x res forest idx _ = + case res of + -- Found a try that fails prop. We'll now test try, and start trying to + -- reduce from the top! + Just y -> iter' y (mkForest y) (Idx 0 0) + -- Either couldn't satisfy the precondition or nothing satisfied the + -- property. Either way, we can't shrink it. + Nothing -> iter' x forest idx { column = column idx + 1 } + + -------------------------------------- + + -- Our test function. First, we'll see if we can just return the hole at idx, + -- assuming it's (1) well-typed and (2), fails the test. Otherwise, we'll + -- test x by replacing values at idx against (Q.expectFailure . prop). Make + -- sure that values generated are strictly smaller than the value at + -- idx. + test :: a -> Idx -> IO (Maybe a) + test x idx = do + let vm = getAtIdx x idx (scMaxDepth args) + case vm of + Nothing -> errorMsg "smartShrink0" + Just v -> do + hole <- testHole v + if isJust hole then return hole + else do (_, r) <- iterateArb x v idx (scMaxReduce args) + -- Maximum size of values to generate; the minimum + -- of the value at the current index and the + -- maxSize parameter. + (min (subValSize x idx) (scMaxSize args)) + notProp + return $ resultToMaybe r + + where + testHole :: SubT -> IO (Maybe a) + testHole SubT { unSubT = v } = + maybe (return Nothing) extractAndTest (cast v :: Maybe a) + where + extractAndTest :: a -> IO (Maybe a) + extractAndTest y = do + res <- resultify notProp y + return $ resultToMaybe res + +resultToMaybe :: Result a -> Maybe a +resultToMaybe res = + case res of + FailedPreCond -> Nothing + FailedProp -> Nothing + Result n -> Just n + +-------------------------------------------------------------------------------- + +-- | Get the maximum depth of d's subforest at idx. Intuitively, it's the +-- maximum number of constructors you have *below* the constructor at idx. So +-- for a unary constructor C, the value [C, C, C] + +-- (:) C +-- (:) C +-- (:) C [] + +-- At (Idx 0 0) in v, we're at C, so subValSize v (Idx 0 0) == 0. +-- At (Idx 0 1) in v, we're at (C : C : []), so subValSize v (Idx 0 1) == 2, since +-- we have the constructors :, C (or :, []) in the longest path underneath. +-- Base-types have subValSize 0. So subValSize [1,2,3] idx == 0 for any idx. +-- Note that if we have subValSize d idx == 0, then it is impossible to construct a +-- *structurally* smaller value at hole idx. +subValSize :: SubTypes a => a -> Idx -> Int +subValSize d idx = maybe 0 depth forestIdx + where + forestIdx :: Maybe [Tree Bool] + forestIdx = fmap subForest $ getIdxForest (mkSubstForest d True) idx + +-------------------------------------------------------------------------------- diff --git a/src/Test/SmartCheck/Render.hs b/src/Test/SmartCheck/Render.hs new file mode 100644 --- /dev/null +++ b/src/Test/SmartCheck/Render.hs @@ -0,0 +1,120 @@ +-- | Rendering arbitrary data, and filling in holes in the data with variables. + +module Test.SmartCheck.Render + ( renderWithVars + , smartPrtLn + ) where + +import Test.SmartCheck.Types +import Test.SmartCheck.Args hiding (format) +import Test.SmartCheck.DataToTree + +import Data.Maybe +import Data.Tree +import Data.List +import Data.Char +import Control.Monad + +-------------------------------------------------------------------------------- + +smartPrefix :: String +smartPrefix = "*** " + +smartPrtLn :: String -> IO () +smartPrtLn = putStrLn . (smartPrefix ++) + +-------------------------------------------------------------------------------- + +-- only print if variable list is non-empty. +renderWithVars :: SubTypes a => Format -> a -> Replace Idx -> IO () +renderWithVars format d idxs = do + prtVars "values" valsLen valVars + prtVars "constructors" constrsLen constrVars + constrArgs + putStrLn "" + putStrLn $ replaceWithVars format d idxs' (Replace valVars constrVars) + putStrLn "" + + where + idxs' = let cs = unConstrs idxs \\ unVals idxs in + idxs { unConstrs = cs } + + constrArgs = + unless (constrsLen == 0) $ putStrLn " there exist arguments x̅ s.t." + + prtVars kind len vs = + when (len > 0) + ( putStrLn $ "forall " ++ kind ++ " " + ++ unwords (take len vs) ++ ":") + + vars str = map (\(x,i) -> x ++ show i) (zip (repeat str) [0::Integer ..]) + valVars = vars "x" + constrVars = vars "C" + + valsLen = length (unVals idxs') + constrsLen = length (unConstrs idxs') + +-------------------------------------------------------------------------------- + +type VarRepl = Either String String + +-- | At each index into d from idxs, replace the whole with a fresh value. +replaceWithVars :: SubTypes a + => Format -> a -> Replace Idx -> Replace String -> String +replaceWithVars format d idxs vars = + case format of + PrintTree -> drawTree strTree + -- We have to be careful here. We can't just show d and then find the + -- matching substrings to replace, since the same substring may show up in + -- multiple places. Rather, we have to recursively descend down the tree of + -- substrings, finding matches, til we hit our variable. + PrintString -> stitchTree strTree + + where + strTree :: Tree String + strTree = remSubVars (foldl' f t zipRepl) + + where + -- Now we'll remove everything after the initial Rights, which are below + -- variables. + remSubVars (Node (Left s ) sf) = Node s (map remSubVars sf) + remSubVars (Node (Right s) _ ) = Node s [] + + f :: Tree VarRepl -> (String, Idx) -> Tree VarRepl + f tree (var, idx) = Node (rootLabel tree) $ + case getIdxForest sf idx of + Nothing -> errorMsg "replaceWithVars" + Just (Node (Right _) _) -> sf -- Don't replace anything + Just (Node (Left _) _) -> forestReplaceChildren sf idx (Right var) + + where + sf = subForest tree + + -- A tree representation of the data turned into a tree of Strings showing the + -- data. showForest is one of our generic methods. + t :: Tree VarRepl + t = let forest = showForest d in + if null forest then errorMsg "replaceWithVars" + else fmap Left (head forest) -- Should be a singleton + + -- Note: we put value idxs before constrs, since they take precedence. + zipRepl :: [(String, Idx)] + zipRepl = zip (unVals vars) (unVals idxs) + ++ zip (unConstrs vars) (unConstrs idxs) + +-------------------------------------------------------------------------------- + +-- | Make a string out a Tree of Strings. Put parentheses around complex +-- subterms, where "complex" means we have two or more items (i.e., there's a +-- space). +stitchTree :: Tree String -> String +stitchTree = stitch + where + stitch (Node str forest) = str ++ " " ++ unwords (map stitchTree' forest) + + stitchTree' (Node str []) = if isJust $ find isSpace str + then '(' : str ++ ")" + else str + stitchTree' node = '(' : stitch node ++ ")" + +-------------------------------------------------------------------------------- diff --git a/src/Test/SmartCheck/SmartGen.hs b/src/Test/SmartCheck/SmartGen.hs new file mode 100644 --- /dev/null +++ b/src/Test/SmartCheck/SmartGen.hs @@ -0,0 +1,177 @@ +{-# LANGUAGE ScopedTypeVariables #-} + +module Test.SmartCheck.SmartGen + ( iterateArbIdx + , iterateArb + , resultify + , replace + , iter + ) where + +import Test.SmartCheck.Types +import Test.SmartCheck.DataToTree + +import qualified Test.QuickCheck.Gen as Q +import qualified Test.QuickCheck as Q hiding (Result) +import qualified Test.QuickCheck.Property as P + +import Prelude hiding (max) +import System.Random +import Data.Tree hiding (levels) + +-------------------------------------------------------------------------------- + +-- | Driver for iterateArb. +iterateArbIdx :: SubTypes a + => a -> (Idx, Maybe Int) -> Int -> Int + -> (a -> Q.Property) -> IO (Int, Result a) +iterateArbIdx d (idx, max) tries sz prop = + maybe (errorMsg "iterateArb 0") + (\ext -> iterateArb d ext idx tries sz prop) + (getAtIdx d idx max) + +-- | Replace the hole in d indexed by idx with a bunch of random values, and +-- test the new d against the property. Returns the first new d (the full d but +-- with the hole replaced) that succeeds. "Succeeds" is determined by the call +-- to resultify---if we're expecting failure, then we succeed by getting a value +-- that passes the precondition but fails the property; otherwise we succeed by +-- getting a value that passes the precondition and satisfies the property. If +-- no value ever satisfies the precondition, then we return FailedPreCond. +-- (Thus, there's an implied linear order on the Result type: FailedPreCond < +-- FailedProp < Result a.) +iterateArb :: forall a. SubTypes a + => a -- ^ Counterexample. + -> SubT -- ^ Sub-value in the counterexample. + -> Idx -- ^ Index of sub-value. + -> Int -- ^ Maximum number of iterations. + -> Int -- ^ Maximum size of value to generate. + -> (a -> Q.Property) -- ^ Property. + -> IO (Int, Result a) -- ^ Number of times precondition is passed and returned + -- result. +iterateArb d ext idx tries max prop = do + g <- newStdGen + iterateArb' (0, FailedPreCond) g 0 0 + where + newMax SubT { unSubT = v } = valDepth v + + -- Main loop. We break out if we ever satisfy the property. Otherwise, we + -- return the latest value. + iterateArb' :: (Int, Result a) -> StdGen -> Int -> Int -> IO (Int, Result a) + iterateArb' (i, res) g try currMax + -- We've exhausted the number of iterations. + | try >= tries = return (i, res) + -- The generated random value is too big. Start again sampling again with + -- size at 0. + | newMax s >= max = iterateArb' (i, res) g0 (try + 1) 0 + | otherwise = + case replace d idx s of + Nothing -> errorMsg "iterateArb 1" + Just d' -> do + res' <- resultify prop d' + case res' of + FailedPreCond -> rec (i, FailedPreCond) + FailedProp -> rec (i+1, FailedProp) + Result x -> return (i+1, Result x) + where + (size, g0) = randomR (0, currMax) g + s = sample ext g size + sample SubT { unSubT = v } = newVal v + rec res' = + iterateArb' res' g0 (try + 1) + -- XXX what ratio is right to increase size of values? This gives us + -- exponentail growth, but remember we're randomly chosing within the + -- range of [0, max], so many values are significantly smaller than the + -- max. Plus we reset the size whenever we get a value that's too big. + -- Note the need for (+ 1), since we seed with 0. + ((currMax + 1) * 2) + +-------------------------------------------------------------------------------- + +-- | Make a new random value given a generator and a max size. Based on the +-- value's type's arbitrary instance. +newVal :: forall a. (SubTypes a, Q.Arbitrary a) + => a -> StdGen -> Int -> SubT +newVal _ g size = + let Q.MkGen m = Q.resize size (Q.arbitrary :: Q.Gen a) in + let v = m g size in + subT v + +-------------------------------------------------------------------------------- + +-- | Put a value v into a another value d at a hole idx, if v is well-typed. +-- Return Nothing if dynamic typing fails. +replace :: SubTypes a => a -> Idx -> SubT -> Maybe a +replace d idx SubT { unSubT = v } = replaceAtIdx d idx v + +-------------------------------------------------------------------------------- + +-- | Make a QuickCheck Result by applying a property function to a value and +-- then get out the Result using our result type. +resultify :: (a -> Q.Property) -> a -> IO (Result a) +resultify prop a = do + P.MkRose r _ <- res fs + return $ maybe FailedPreCond -- Failed precondition (discard) + -- If failed because of an exception, just say we failed. + (\b -> if notExceptionFail r then get b r else FailedProp) + (P.ok r) -- result of test case (True ==> passed) + where + get b r + | b && P.expect r = Result a -- expected to pass and we did + | not b && not (P.expect r) = Result a -- expected failure and got it + | otherwise = FailedProp -- We'll just discard it. + + Q.MkGen { Q.unGen = f } = prop a :: Q.Gen P.Prop + fs = P.unProp $ f err err :: P.Rose P.Result + res = P.protectRose . P.reduceRose + + -- XXX A hack! Means we failed the property because it failed, not because of + -- an exception (i.e., with partial function tests). + notExceptionFail r = let e = P.reason r in + e == "Falsifiable" || e == "" + + err = errorMsg "resultify: should not evaluate." + +-------------------------------------------------------------------------------- + +type Test a b = a -> Idx -> IO b +type Next a b = a -> b -> Forest Bool -> Idx -> [Idx] -> IO (a, [Idx]) + +-- Do a breadth-first traversal of the data. First, we find the next valid +-- index we can use. Then we apply our test function, passing the result to our +-- next function. +iter :: SubTypes a + => a -- ^ Failed value + -> Test a b -- ^ Test to use + -> Next a b -- ^ What to do after the test + -> (a -> Q.Property) -- ^ Property + -> Maybe Int -- ^ Max depth to analyze + -> Forest Bool -- ^ Only evaluate at True indexes. + -> Idx -- ^ Starting index to extrapolate + -> [Idx] -- ^ List of generalized indices + -> IO (a, [Idx]) +iter d test nxt prop maxLevel forest idx idxs + | done = return (d, idxs) + | nextLevel = iter' + | atFalse = iter' -- Must be last check or !! index below may be out of + -- bounds! + | otherwise = do tries <- test d idx + nxt d tries forest idx idxs + where + -- Location is w.r.t. the forest, not the original data value. + l = level idx + levels = breadthLevels forest + done = length levels <= l || tooDeep l maxLevel + nextLevel = length (levels !! l) <= column idx + atFalse = not $ (levels !! l) !! column idx + iter' = iter d test nxt prop maxLevel forest + idx { level = l + 1, column = 0 } idxs + +-------------------------------------------------------------------------------- + +-- | Get the maximum depth of a value, where depth is measured in the maximum +-- depth of the tree representation, not counting base types (defined in +-- Types.hs). +valDepth :: SubTypes a => a -> Int +valDepth d = depth (mkSubstForest d True) + +-------------------------------------------------------------------------------- diff --git a/src/Test/SmartCheck/Types.hs b/src/Test/SmartCheck/Types.hs new file mode 100644 --- /dev/null +++ b/src/Test/SmartCheck/Types.hs @@ -0,0 +1,421 @@ +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE OverlappingInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Test.SmartCheck.Types + ( SubT(..) + , subT + , Result(..) + , SubTypes(..) + , Idx(..) + , Subst(..) + , Replace(..) + , errorMsg + -- ** For constructing new instances of `SubTypes` + , gst + , grc + , gtc + , gsf + , gsz + ) where + +import GHC.Generics +import Data.Tree +import Data.Typeable + +-- For instances +import Data.Word +import Data.Int +import Data.Ratio +import Data.Complex + +import qualified Test.QuickCheck as Q + +------------------------------------------------------------------------------- + +-- | Nominally, a list for value generalization indexes and existential +-- generalization. +data Replace a = Replace { unVals :: [a], unConstrs :: [a] } + deriving (Show, Read, Eq) + +-------------------------------------------------------------------------------- +-- Result type +-------------------------------------------------------------------------------- + +-- | Possible results of iterateArb. +data Result a = FailedPreCond -- ^ Couldn't satisfy the precondition of a + -- QuickCheck property + | FailedProp -- ^ Failed the property---either we expect + -- failure and it passes or we expect to pass it + -- and we fail. + | Result a -- ^ Satisfied it, with the satisfying value. + deriving (Show, Read, Eq) + +instance Functor Result where + fmap _ FailedPreCond = FailedPreCond + fmap _ FailedProp = FailedProp + fmap f (Result a) = Result (f a) + +instance Monad Result where + return a = Result a + FailedPreCond >>= _ = FailedPreCond + FailedProp >>= _ = FailedProp + Result a >>= f = f a + +------------------------------------------------------------------------------- +-- Indexing +------------------------------------------------------------------------------- + +-- | Index into a Tree/Forest, where level is the depth from the root and column +-- is the distance d is the dth value on the same level. Thus, all left-most +-- nodes are in column 0. This is a "matrix view" of tree-structured data. +data Idx = Idx { level :: Int, column :: Int } + deriving Eq + +instance Show Idx where + show (Idx l c) = foldr1 (++) ["Idx ", show l, " ", show c] + +-- | Keep or substitue a value in the tree. +data Subst = Keep | Subst + deriving (Show, Eq, Read) + +-- | Sort in order of depth first then left to right. +instance Ord Idx where + compare (Idx l0 c0) (Idx l1 c1) | l0 < l1 = LT + | l0 > l1 = GT + | c0 < c1 = LT + | c0 > c1 = GT + | True = EQ + +------------------------------------------------------------------------------- +-- User-defined subtypes of data +------------------------------------------------------------------------------- + +data SubT = forall a. (Q.Arbitrary a, SubTypes a) + => SubT { unSubT :: a } + +subT :: (Q.Arbitrary a, SubTypes a) => a -> SubT +subT = SubT + +-- Would require SubT to derive Eq. +-- instance Eq SubT where +-- SubT a == SubT b = cast a == Just b + +instance Show SubT where + show (SubT t) = show t + +-- | This class covers algebraic datatypes that can be transformed into Trees. +-- subTypes is the main method, placing values into trees. For types that can't +-- be put into a *structural* order (e.g., Int), we don't want SmartCheck to +-- touch them, so that aren't placed in the tree (the baseType method tells +-- subTypes which types have this property). +-- +-- for a datatype with constructors A and C, +-- +-- > subTypes (A (C 0) 1) +-- > [Node {rootLabel = C 0, subForest = []}] +-- +class (Q.Arbitrary a, Show a, Typeable a) => SubTypes a where + ----------------------------------------------------------- + subTypes :: a -> Forest SubT + default subTypes :: (Generic a, GST (Rep a)) + => a -> Forest SubT + subTypes = gst . from + ----------------------------------------------------------- + baseType :: a -> Bool + baseType _ = False + ----------------------------------------------------------- + -- | Generically replace child i in m with value s. A total function: returns + -- Nothing if you try to replace a child with an ill-typed child s. (Returns + -- Just (the original data) if your index is out of bounds). + replaceChild :: Typeable b => a -> Forest Subst -> b -> Maybe a + default replaceChild :: (Generic a, GST (Rep a), Typeable b) + => a -> Forest Subst -> b -> Maybe a + replaceChild a forest b = fmap to $ grc (from a) forest b + ----------------------------------------------------------- + -- Grab the top contructor. + toConstr :: a -> String + default toConstr :: (Generic a, GST (Rep a)) => a -> String + toConstr = gtc . from + ----------------------------------------------------------- + -- | showForest generically shows a value while preserving its structure (in a + -- Tree). You should always end up with either a singleton list containing + -- the tree or an empty list for baseTypes. Also, it must be the case that + -- for a value v, + -- + -- null (subTypes v) iff null (showForest v) + -- and + -- if not . null (subTypes v), then subForest . head (showForest v) + -- has the same structure as subTypes v. + -- + -- We can't just return a Tree String or Maybe (Tree String). The reason is + -- that in generically constructing the value, we have to deal with product + -- types. There is no sane way to join them other than list-like + -- concatenation (i.e., gsf (a :*: b) = gsf a ++ gsf b). + showForest :: a -> Forest String + default showForest :: (Generic a, GST (Rep a)) + => a -> Forest String + showForest = gsf . from + ----------------------------------------------------------- + + +------------------------------------------------------------------------------- +-- Generic representation +------------------------------------------------------------------------------- + +class GST f where + -- Names are abbreviations of the corresponding method names above. + gst :: f a -> Forest SubT + grc :: Typeable b => f a -> Forest Subst -> b -> Maybe (f a) + gtc :: f a -> String + gsf :: f a -> Forest String + gsz :: f a -> Int + +instance GST U1 where + gst U1 = [] + grc _ _ _ = Nothing + gtc U1 = "" + gsf U1 = [] + gsz U1 = 0 + +instance (GST a, GST b) => GST (a :*: b) where + gst (a :*: b) = gst a ++ gst b + + grc (a :*: b) forest c = + case forest of + [] -> Just (a :*: b) + ls -> do let (x,y) = splitAt (gsz a) ls + left <- grc a x c + right <- grc b y c + return $ left :*: right + + gtc (a :*: b) = gtc a ++ gtc b + gsf (a :*: b) = gsf a ++ gsf b + gsz (a :*: b) = gsz a + gsz b + +instance (GST a, GST b) => GST (a :+: b) where + gst (L1 a) = gst a + gst (R1 b) = gst b + + grc (L1 a) forest c = grc a forest c >>= return . L1 + grc (R1 a) forest c = grc a forest c >>= return . R1 + + gtc (L1 a) = gtc a + gtc (R1 a) = gtc a + + gsf (L1 a) = gsf a + gsf (R1 a) = gsf a + + gsz (L1 a) = gsz a + gsz (R1 a) = gsz a + +-- Constructor meta-information +instance (Constructor c, GST a) => GST (M1 C c a) where + gst (M1 a) = gst a + grc (M1 a) forest c = grc a forest c >>= return . M1 + gtc = conName + + gsf m@(M1 a) = [ tree ] + where + -- When a tree has reached a constructor with a baseType value (e.g., A 3 + -- for some constructor A), we want to show the constructor and the value, + -- but not have a subForest. So we check if the rest is a baseType (gst a + -- tells us that), and if so, we show the conName, and extract (rootLabel + -- . head) (gsf a), which is basically just showing the rest (look at gsf + -- (K1 a) below). Otherwise, we just want the constructor. + tree | null (gst a) = Node root [] + | otherwise = Node (conName m) (gsf a) + root | null (gsf a) = conName m + | otherwise = conName m ++ " " ++ (rootLabel . head) (gsf a) + + gsz (M1 a) = gsz a + +-- All the other meta-information (selector, module, etc.) +instance GST a => GST (M1 i k a) where + gst (M1 a) = gst a + grc (M1 a) forest c = grc a forest c >>= return . M1 + gtc (M1 a) = gtc a + gsf (M1 a) = gsf a + gsz (M1 a) = gsz a + +instance (Show a, Q.Arbitrary a, SubTypes a, Typeable a) => GST (K1 i a) where + gst (K1 a) = if baseType a then [] else [ Node (subT a) (subTypes a) ] + + grc (K1 a) forest c = + case forest of + [] -> Just (K1 a) + (Node Keep _ : _) -> Just (K1 a) + (Node Subst [] : _) -> fmap K1 (cast c) + (Node Subst ls : _) -> replaceChild a ls c >>= return . K1 + + gtc _ = "" + + -- Yes, this is right. For a baseType value v, showForest v will just yield + -- [] using showForest'. But to make the tree using generics, when we get + -- down to baseTypes, we need to actually show them, returing a Forest. We + -- extract the value in the rootLabel above. + gsf (K1 a) = if baseType a then [Node (show a) []] else showForest a + + gsz (K1 a) = if baseType a then 0 else 1 + +------------------------------------------------------------------------------- +-- We try to cover the instances supported by QuickCheck: http://hackage.haskell.org/packages/archive/QuickCheck/2.4.2/doc/html/Test-QuickCheck-Arbitrary.html + +instance SubTypes Bool where baseType _ = True +instance SubTypes Char where baseType _ = True +instance SubTypes Double where baseType _ = True +instance SubTypes Float where baseType _ = True +instance SubTypes Int where baseType _ = True +instance SubTypes Integer where + subTypes _ = [] + baseType _ = True + replaceChild = replaceChild' + toConstr = toConstr' + showForest = showForest' +instance SubTypes Int8 where + subTypes _ = [] + baseType _ = True + replaceChild = replaceChild' + toConstr = toConstr' + showForest = showForest' +instance SubTypes Int16 where + subTypes _ = [] + baseType _ = True + replaceChild = replaceChild' + toConstr = toConstr' + showForest = showForest' +instance SubTypes Int32 where + subTypes _ = [] + baseType _ = True + replaceChild = replaceChild' + toConstr = toConstr' + showForest = showForest' +instance SubTypes Int64 where + subTypes _ = [] + baseType _ = True + replaceChild = replaceChild' + toConstr = toConstr' + showForest = showForest' +instance SubTypes Word where + subTypes _ = [] + baseType _ = True + replaceChild = replaceChild' + toConstr = toConstr' + showForest = showForest' +instance SubTypes Word8 where + subTypes _ = [] + baseType _ = True + replaceChild = replaceChild' + toConstr = toConstr' + showForest = showForest' +instance SubTypes Word16 where + subTypes _ = [] + baseType _ = True + replaceChild = replaceChild' + toConstr = toConstr' + showForest = showForest' +instance SubTypes Word32 where + subTypes _ = [] + baseType _ = True + replaceChild = replaceChild' + toConstr = toConstr' + showForest = showForest' +instance SubTypes Word64 where + subTypes _ = [] + baseType _ = True + replaceChild = replaceChild' + toConstr = toConstr' + showForest = showForest' +instance SubTypes () where baseType _ = True + +--instance (Q.Arbitrary a, SubTypes a, Typeable a) => SubTypes [a] +-- subTypes = concatMap subTypes +-- baseType _ = True +-- replaceChild = replaceChild' +-- toConstr = toConstr' +-- -- toConstrAndBase = toConstrAndBase' +-- showForest = showForest' + +-- For container types like list, if it's over a baseType, we don't want to +-- evaluate the container either. The intuition is that, e.g., for [Int], it'll +-- be shrunk enough by QuickCheck and doesn't really have "interesting +-- structure". + +-- For example, this makes String a baseType automatically. +instance (Q.Arbitrary a, SubTypes a, Typeable a) => SubTypes [a] where + subTypes = if baseType (undefined :: a) then \_ -> [] + else gst . from + baseType _ = baseType (undefined :: a) + replaceChild x forest y = if baseType (undefined :: a) + then replaceChild' x forest y + else fmap to $ grc (from x) forest y + toConstr = if baseType (undefined :: a) then toConstr' + else gtc . from + showForest = if baseType (undefined :: a) then showForest' + else gsf . from + +instance (Integral a, Q.Arbitrary a, SubTypes a, Typeable a) + => SubTypes (Ratio a) where + subTypes _ = [] + baseType _ = True + replaceChild = replaceChild' + toConstr = toConstr' + showForest = showForest' +instance (RealFloat a, Q.Arbitrary a, SubTypes a, Typeable a) + => SubTypes (Complex a) where + subTypes _ = [] + baseType _ = True + replaceChild = replaceChild' + toConstr = toConstr' + showForest = showForest' +instance (Q.Arbitrary a, SubTypes a, Typeable a) => SubTypes (Maybe a) +instance ( Q.Arbitrary a, SubTypes a, Typeable a + , Q.Arbitrary b, SubTypes b, Typeable b) + => SubTypes (Either a b) +instance ( Q.Arbitrary a, SubTypes a, Typeable a + , Q.Arbitrary b, SubTypes b, Typeable b) + => SubTypes (a, b) +instance ( Q.Arbitrary a, SubTypes a, Typeable a + , Q.Arbitrary b, SubTypes b, Typeable b + , Q.Arbitrary c, SubTypes c, Typeable c) + => SubTypes (a, b, c) +instance ( Q.Arbitrary a, SubTypes a, Typeable a + , Q.Arbitrary b, SubTypes b, Typeable b + , Q.Arbitrary c, SubTypes c, Typeable c + , Q.Arbitrary d, SubTypes d, Typeable d) + => SubTypes (a, b, c, d) +instance ( Q.Arbitrary a, SubTypes a, Typeable a + , Q.Arbitrary b, SubTypes b, Typeable b + , Q.Arbitrary c, SubTypes c, Typeable c + , Q.Arbitrary d, SubTypes d, Typeable d + , Q.Arbitrary e, SubTypes e, Typeable e) + => SubTypes (a, b, c, d, e) + +------------------------------------------------------------------------------- +-- Helpers + +-- These should never be directly called. We provide compatible instances anyway. +toConstr' :: Show a => a -> String +toConstr' = show + +replaceChild' :: (Typeable a, Typeable b) + => a -> Forest Subst -> b -> Maybe a +replaceChild' a [] _ = Just a +replaceChild' a (Node Keep _ : _) _ = Just a +replaceChild' _ (Node Subst _ : _) b = cast b + +showForest' :: Show a => a -> Forest String +showForest' _ = [] + +------------------------------------------------------------------------------- + +errorMsg :: String -> a +errorMsg loc = error $ "SmartCheck error: unexpected error in " ++ loc + ++ ". Please file a bug report at " + ++ "." + +-------------------------------------------------------------------------------