module Test.Extrapolate.Core
( module Test.LeanCheck
, module Test.LeanCheck.Utils.TypeBinding
, module Test.Extrapolate.Exprs
, Generalizable (..)
, this
, backgroundWith
, (+++)
, backgroundOf
, bgEq
, bgOrd
, bgEqWith1
, bgEqWith2
, Option (..)
, WithOption (..)
, maxTests
, extraInstances
, maxConditionSize
, hasEq
, (*==*)
, (*/=*)
, (*<=*)
, (*<*)
, tBackground
, counterExamples
, counterExampleGen
, counterExampleGens
, generalizations
, generalizationsCE
, generalizationsCEC
, generalizationsCounts
, atoms
, theoryAndReprExprs
, theoryAndReprConds
, candidateConditions
, validConditions
, weakestCondition
, getBackground
, fullInstances
, matchList
, newMatches
, Testable (..)
, results
, areInstancesOf
)
where
import Test.Extrapolate.Utils
import Test.LeanCheck.Utils
import Test.LeanCheck.Utils.TypeBinding
import Data.Typeable
import Data.Dynamic
import Test.LeanCheck hiding
( Testable (..)
, results
, counterExamples
, counterExample
, productWith
, check
, checkFor
, checkResult
, checkResultFor
)
import Data.Maybe
import Data.Either (isRight)
import Data.List (insert, nub, sort)
import Data.Functor ((<$>))
import Test.Extrapolate.Exprs
import Test.LeanCheck.Error (errorToFalse)
import Data.Ratio (Ratio, numerator, denominator)
import Test.Extrapolate.TypeBinding
import Test.Speculate.Reason (Thy)
import Test.Speculate.Engine (theoryAndRepresentativesFromAtoms, classesFromSchemasAndVariables)
import Data.Monoid ((<>))
class (Listable a, Typeable a, Show a) => Generalizable a where
expr :: a -> Expr
name :: a -> String
name _ = "x"
background :: a -> [Expr]
background _ = []
instances :: a -> Instances -> Instances
instance Generalizable () where
expr = showConstant
name _ = "u"
instances u = this u id
instance Generalizable Bool where
expr = showConstant
name _ = "p"
background p = bgEq p
++ [ constant "not" not ]
instances p = this p id
instance Generalizable Int where
expr = showConstant
name _ = "x"
background x = bgOrd x
instances x = this x id
instance Generalizable Integer where
expr = showConstant
name _ = "x"
background x = bgOrd x
instances x = this x id
instance Generalizable Char where
expr = showConstant
name _ = "c"
background c = bgOrd c
instances c = this c id
instance (Generalizable a) => Generalizable (Maybe a) where
expr mx@Nothing = constant "Nothing" (Nothing -: mx)
expr mx@(Just x) = constant "Just" (Just ->: mx) :$ expr x
name mx = "m" ++ name (fromJust mx)
background mx = bgEqWith1 (maybeEq ->:> mx)
++ bgOrdWith1 (maybeOrd ->:> mx)
++ [ constant "Just" (Just ->: mx) ]
instances mx = this mx $ instances (fromJust mx)
instance (Generalizable a, Generalizable b) => Generalizable (Either a b) where
expr lx@(Left x) = constant "Left" (Left ->: lx) :$ expr x
expr ry@(Right y) = constant "Right" (Right ->: ry) :$ expr y
name exy = "e" ++ name (fromLeft exy) ++ name (fromRight exy)
background exy = bgEqWith2 (eitherEq ->>:> exy)
++ bgOrdWith2 (eitherOrd ->>:> exy)
++ [ constant "Left" (Left ->: exy)
, constant "Right" (Right ->: exy) ]
instances exy = this exy $ instances (fromLeft exy)
. instances (fromRight exy)
instance (Generalizable a, Generalizable b) => Generalizable (a,b) where
name xy = name (fst xy) ++ name (snd xy)
expr (x,y) = constant "," ((,) ->>: (x,y))
:$ expr x :$ expr y
background xy = bgEqWith2 (pairEq ->>:> xy)
++ bgOrdWith2 (pairOrd ->>:> xy)
instances xy = this xy $ instances (fst xy)
. instances (snd xy)
instance (Generalizable a, Generalizable b, Generalizable c)
=> Generalizable (a,b,c) where
name xyz = name x ++ name y ++ name z
where (x,y,z) = xyz
expr (x,y,z) = constant ",," ((,,) ->>>: (x,y,z))
:$ expr x :$ expr y :$ expr z
background xyz = bgEqWith3 (tripleEq ->>>:> xyz)
++ bgOrdWith3 (tripleOrd ->>>:> xyz)
instances xyz = this xyz $ instances x . instances y . instances z
where (x,y,z) = xyz
instance (Generalizable a, Generalizable b, Generalizable c, Generalizable d)
=> Generalizable (a,b,c,d) where
name xyzw = name x ++ name y ++ name z ++ name w
where (x,y,z,w) = xyzw
expr (x,y,z,w) = constant ",,," ((,,,) ->>>>: (x,y,z,w))
:$ expr x :$ expr y :$ expr z :$ expr w
background xyzw = bgEqWith4 (quadrupleEq ->>>>:> xyzw)
++ bgOrdWith4 (quadrupleOrd ->>>>:> xyzw)
instances xyzw = this xyzw $ instances x
. instances y
. instances z
. instances w
where (x,y,z,w) = xyzw
instance Generalizable a => Generalizable [a] where
name xs = name (head xs) ++ "s"
expr (xs@[]) = showConstant ([] -: xs)
expr (xs@(y:ys)) = constant ":" ((:) ->>: xs) :$ expr y :$ expr ys
background xs = bgEqWith1 (listEq ->:> xs)
++ bgOrdWith1 (listOrd ->:> xs)
++ [ constant "length" (length -:> xs) ]
++ [ constant "elem" (elemBy (*==*) ->:> xs) | hasEq $ head xs ]
instances xs = this xs $ instances (head xs)
instance Generalizable Ordering where
name o = "o"
expr o = showConstant o
background o = bgOrd o
instances o = this o id
bgEq :: (Eq a, Generalizable a) => a -> [Expr]
bgEq x = [ constant "==" ((==) -:> x)
, constant "/=" ((/=) -:> x) ]
bgOrd :: (Ord a, Generalizable a) => a -> [Expr]
bgOrd x = [ constant "==" ((==) -:> x)
, constant "/=" ((/=) -:> x)
, constant "<" ((<) -:> x)
, constant "<=" ((<=) -:> x) ]
bgEqWith1 :: (Generalizable a, Generalizable b)
=> ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]
bgEqWith1 makeEq = takeWhile (\_ -> hasEq x)
[ constant "==" ( makeEq (*==*))
, constant "/=" (not .: makeEq (*==*)) ]
where
x = argTy1of2 $ argTy1of2 makeEq
bgEqWith2 :: (Generalizable a, Generalizable b, Generalizable c)
=> ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]
bgEqWith2 makeEq = takeWhile (\_ -> hasEq x && hasEq y)
[ constant "==" ( makeEq (*==*) (*==*))
, constant "/=" (not .: makeEq (*==*) (*==*)) ]
where
x = argTy1of2 $ argTy1of2 makeEq
y = argTy1of2 . argTy1of2 $ argTy2of2 makeEq
bgEqWith3 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d)
=> ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> a -> a -> Bool)
-> [Expr]
bgEqWith3 makeEq = takeWhile (\_ -> hasEq x && hasEq y && hasEq z)
[ constant "==" (makeEq (*==*) (*==*) (*==*))
, constant "/=" (not .: makeEq (*==*) (*==*) (*==*)) ]
where
x = argTy1of2 $ argTy1of2 makeEq
y = argTy1of2 . argTy1of2 $ argTy2of2 makeEq
z = argTy1of2 . argTy1of2 . argTy2of2 $ argTy2of2 makeEq
bgEqWith4 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d, Generalizable e)
=> ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> (e->e->Bool) -> a -> a -> Bool)
-> [Expr]
bgEqWith4 makeEq = takeWhile (\_ -> hasEq x && hasEq y && hasEq z && hasEq w)
[ constant "==" (makeEq (*==*) (*==*) (*==*) (*==*))
, constant "/=" (not .: makeEq (*==*) (*==*) (*==*) (*==*)) ]
where
x = argTy1of2 $ argTy1of2 makeEq
y = argTy1of2 . argTy1of2 $ argTy2of2 makeEq
z = argTy1of2 . argTy1of2 . argTy2of2 $ argTy2of2 makeEq
w = argTy1of2 . argTy1of2 . argTy2of2 . argTy2of2 $ argTy2of2 makeEq
bgOrdWith1 :: (Generalizable a, Generalizable b)
=> ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]
bgOrdWith1 makeOrd = takeWhile (\_ -> hasOrd x)
[ constant "<=" ( makeOrd (*<=*))
, constant "<" (not .: flip (makeOrd (*<=*))) ]
where
x = argTy1of2 $ argTy1of2 makeOrd
bgOrdWith2 :: (Generalizable a, Generalizable b, Generalizable c)
=> ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]
bgOrdWith2 makeOrd = takeWhile (\_ -> hasOrd x && hasOrd y)
[ constant "<=" ( makeOrd (*<=*) (*<=*))
, constant "<" (not .: flip (makeOrd (*<=*) (*<=*))) ]
where
x = argTy1of2 $ argTy1of2 makeOrd
y = argTy1of2 . argTy1of2 $ argTy2of2 makeOrd
bgOrdWith3 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d)
=> ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> a -> a -> Bool)
-> [Expr]
bgOrdWith3 makeOrd = takeWhile (\_ -> hasOrd x && hasOrd y && hasOrd z)
[ constant "<=" (makeOrd (*<=*) (*<=*) (*<=*))
, constant "<" (not .: flip (makeOrd (*<=*) (*<=*) (*<=*))) ]
where
x = argTy1of2 $ argTy1of2 makeOrd
y = argTy1of2 . argTy1of2 $ argTy2of2 makeOrd
z = argTy1of2 . argTy1of2 . argTy2of2 $ argTy2of2 makeOrd
bgOrdWith4 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d, Generalizable e)
=> ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> (e->e->Bool) -> a -> a -> Bool)
-> [Expr]
bgOrdWith4 makeOrd = takeWhile (\_ -> hasOrd x && hasOrd y && hasOrd z && hasOrd w)
[ constant "<=" (makeOrd (*<=*) (*<=*) (*<=*) (*<=*))
, constant "<" (not .: flip (makeOrd (*<=*) (*<=*) (*<=*) (*<=*))) ]
where
x = argTy1of2 $ argTy1of2 makeOrd
y = argTy1of2 . argTy1of2 $ argTy2of2 makeOrd
z = argTy1of2 . argTy1of2 . argTy2of2 $ argTy2of2 makeOrd
w = argTy1of2 . argTy1of2 . argTy2of2 . argTy2of2 $ argTy2of2 makeOrd
ins :: Generalizable a => a -> Instances
ins x = listable x ++ nameWith (name x) x ++ backgroundWith (background x) x
this :: Generalizable a
=> a -> (Instances -> Instances) -> Instances -> Instances
this x f is =
if isListable is (typeOf x)
then is
else f (ins x ++ is)
backgroundWith :: Typeable a => [Expr] -> a -> Instances
backgroundWith es x = [ Instance "Background" (typeOf x) es ]
getBackground :: Instances -> [Expr]
getBackground is = concat [es | Instance "Background" _ es <- is]
getEqInstancesFromBackground :: Instances -> Instances
getEqInstancesFromBackground is =
[Instance "Eq" (argumentTy $ typ eq) [eq, iq] | eq <- eqs, iq <- iqs, typ eq == typ iq]
where
eqs = [Constant "==" e | Constant "==" e <- bg]
iqs = [Constant "/=" e | Constant "/=" e <- bg]
bg = getBackground is
backgroundOf :: Generalizable a => a -> [Expr]
backgroundOf x = getBackground $ instances x []
tBackground :: Testable a => a -> [Expr]
tBackground = getBackground . tinstances
generalizations1 :: Instances -> Expr -> [Expr]
generalizations1 is (Var _ _) = []
generalizations1 is (Constant _ dx) =
[holeOfTy t | let t = dynTypeRep dx, isListable is t]
generalizations1 is (e1 :$ e2) =
[holeOfTy t | isRight (etyp (e1 :$ e2))
, let t = typ (e1 :$ e2)
, isListable is t]
++ productWith (:$) (generalizations1 is e1) (generalizations1 is e2)
++ map (:$ e2) (generalizations1 is e1)
++ map (e1 :$) (generalizations1 is e2)
generalizations :: Instances -> [Expr] -> [ [Expr] ]
generalizations is = map unfold . generalizations1 is . fold
productWith :: (a -> b -> c) -> [a] -> [b] -> [c]
productWith f xs ys = [f x y | x <- xs, y <- ys]
data Option = MaxTests Int
| ExtraInstances Instances
| MaxConditionSize Int
| MinFailures (Ratio Int)
| MaxSpeculateSize (Maybe Int)
| ConditionBound (Maybe Int)
| ConstantBound (Maybe Int)
| DepthBound (Maybe Int)
deriving (Show, Typeable)
data WithOption a = With
{ property :: a
, option :: Option }
type Options = [Option]
maxTests :: Testable a => a -> Int
maxTests p = head $ [m | MaxTests m <- options p] ++ [500]
extraInstances :: Testable a => a -> Instances
extraInstances p = concat [is | ExtraInstances is <- options p]
maxConditionSize :: Testable a => a -> Int
maxConditionSize p = head $ [m | MaxConditionSize m <- options p] ++ [4]
computeMinFailures :: Testable a => a -> Int
computeMinFailures p = max 2 $ m * numerator r `div` denominator r
where
r = head $ [r | MinFailures r <- options p] ++ [0]
m = maxTests p
computeMaxSpeculateSize :: Testable a => a -> Maybe Int
computeMaxSpeculateSize p = head $ [b | MaxSpeculateSize b <- options p] ++ [Just 4]
computeConditionBound :: Testable a => a -> Maybe Int
computeConditionBound p = head $ [b | ConditionBound b <- options p] ++ [Nothing]
computeConstantBound :: Testable a => a -> Maybe Int
computeConstantBound p = head $ [b | ConstantBound b <- options p] ++ [Nothing]
computeDepthBound :: Testable a => a -> Maybe Int
computeDepthBound p = head $ [b | DepthBound b <- options p] ++ [Nothing]
class Testable a where
resultiers :: a -> [[([Expr],Bool)]]
($-|) :: a -> [Expr] -> Bool
tinstances :: a -> Instances
options :: a -> Options
options _ = []
instance Testable a => Testable (WithOption a) where
resultiers (p `With` o) = resultiers p
(p `With` o) $-| es = p $-| es
tinstances (p `With` o) = tinstances p ++ extraInstances (p `With` o)
options (p `With` o) = o : options p
instance Testable Bool where
resultiers p = [[([],p)]]
p $-| [] = p
p $-| _ = error "($-|): too many arguments"
tinstances _ = instances bool . instances int $ []
instance (Testable b, Generalizable a, Listable a) => Testable (a->b) where
resultiers p = concatMapT resultiersFor tiers
where resultiersFor x = mapFst (expr x:) `mapT` resultiers (p x)
mapFst f (x,y) = (f x, y)
p $-| [] = error "($-|): too few arguments"
p $-| (e:es) = p (eval (error "($-|): wrong type") e) $-| es
tinstances p = instances (undefarg p) $ tinstances (p undefined)
where
undefarg :: (a -> b) -> a
undefarg _ = undefined
results :: Testable a => a -> [([Expr],Bool)]
results = concat . resultiers
counterExamples :: Testable a => Int -> a -> [[Expr]]
counterExamples n p = [as | (as,False) <- take n (results p)]
counterExample :: Testable a => Int -> a -> Maybe [Expr]
counterExample n = listToMaybe . counterExamples n
counterExampleGens :: Testable a => Int -> a -> Maybe ([Expr],[[Expr]])
counterExampleGens n p = case counterExample n p of
Nothing -> Nothing
Just es -> Just (es,generalizationsCE n p es)
generalizationsCE :: Testable a => Int -> a -> [Expr] -> [[Expr]]
generalizationsCE n p es =
[ canonicalizeWith is gs'
| gs <- generalizations is es
, gs' <- vassignments gs
, isCounterExample n p gs'
]
where
is = tinstances p
generalizationsCEC :: Testable a => a -> [Expr] -> [(Expr,[Expr])]
generalizationsCEC p es | maxConditionSize p <= 0 = []
generalizationsCEC p es =
[ (wc'', gs'')
| gs <- generalizations is es
, gs' <- vassignments gs
, let thycs = theoryAndReprConds p
, let wc = weakestCondition thycs p gs'
, wc /= constant "False" False
, wc /= constant "True" True
, let (wc'':gs'') = canonicalizeWith is (wc:gs')
]
where
is = tinstances p
isCounterExample :: Testable a => Int -> a -> [Expr] -> Bool
isCounterExample m p = all (not . errorToFalse . (p $-|))
. take m
. grounds (tinstances p)
generalizationsCounts :: Testable a => Int -> a -> [Expr] -> [([Expr],Int)]
generalizationsCounts n p es =
[ (canonicalizeWith is gs', countPasses n p gs')
| gs <- generalizations is es
, gs' <- vassignments gs
]
where
is = tinstances p
countPasses :: Testable a => Int -> a -> [Expr] -> Int
countPasses m p = length . filter (p $-|) . take m . grounds (tinstances p)
counterExampleGen :: Testable a => Int -> a -> Maybe ([Expr],Maybe [Expr])
counterExampleGen n p = case counterExampleGens n p of
Nothing -> Nothing
Just (es,[]) -> Just (es,Nothing)
Just (es,(gs:_)) -> Just (es,Just gs)
areInstancesOf :: [Expr] -> [Expr] -> Bool
es1 `areInstancesOf` es2 = length es1 == length es2
&& and [e1 `isInstanceOf` e2 | (e1,e2) <- zip es1 es2]
matchList :: [Expr] -> [Expr] -> Maybe Binds
matchList = m []
where
m bs [] [] = Just bs
m bs (e1:es1) (e2:es2) =
case matchWith bs e1 e2 of
Nothing -> Nothing
Just bs -> m bs es1 es2
newMatches :: [Expr] -> [Expr] -> Maybe Binds
e1 `newMatches` e2 = filter (not . isVar . snd) <$> e1 `matchList` e2
expressionsTT :: [[Expr]] -> [[Expr]]
expressionsTT dss = dss \/ productMaybeWith ($$) ess ess `addWeight` 1
where
ess = expressionsTT dss
theoryAndReprsFromPropAndAtoms :: Testable a => a -> [[Expr]] -> (Thy,[[Expr]])
theoryAndReprsFromPropAndAtoms p ess =
theoryAndRepresentativesFromAtoms
(maxConditionSize p) compareExpr (const True) (===) ess
where
e1 === e2 = keep e1 && keep e2 && equal is m e1 e2
keep e = maybe True (\b -> length (consts e) <= b) constBound
&& maybe True (\b -> depthE e <= b) depthBound
&& maybe True (\b -> lengthE e <= b) (computeMaxSpeculateSize p)
constBound = computeConstantBound p
depthBound = computeDepthBound p
is = fullInstances p
m = maxTests p
compareExpr :: Expr -> Expr -> Ordering
compareExpr = compareComplexityThen (lexicompareBy cmp)
e1 `cmp` e2 | arity e1 == 0 && arity e2 /= 0 = LT
e1 `cmp` e2 | arity e1 /= 0 && arity e2 == 0 = GT
e1 `cmp` e2 = compareIndex (concat ess) e1 e2 <> e1 `compare` e2
fullInstances :: Testable a => a -> Instances
fullInstances p = is ++ getEqInstancesFromBackground is
where
is = tinstances p
atoms :: Testable a => a -> [[Expr]]
atoms p = ([vs] \/)
. foldr (\/) [esU]
$ [ eval (error msg :: [[Expr]]) ess
| Instance "Listable" _ [ess] <- is ]
where
vs = sort . map holeOfTy . filter (isListable is) . nubMergeMap (typesIn . typ) $ esU
esU = getBackground is
msg = "canditateConditions: wrong type, not [[Expr]]"
is = tinstances p
theoryAndReprExprs :: Testable a => a -> (Thy,[Expr])
theoryAndReprExprs p =
(\(thy,ess) -> (thy, concat $ take (maxConditionSize p) ess))
. theoryAndReprsFromPropAndAtoms p
$ atoms p
theoryAndReprConds :: Testable a => a -> (Thy, [Expr])
theoryAndReprConds p = (thy, filter (\c -> typ c == boolTy) es)
where
(thy,es) = theoryAndReprExprs p
candidateConditions :: Testable a => (Thy,[Expr]) -> a -> [Expr] -> [Expr]
candidateConditions (thy,cs) p es = expr True :
[ c | (c,_) <- classesFromSchemasAndVariables thy (uncurry (flip Var) <$> vars es) cs
, hasVar c
, not (isAssignment c)
, not (isAssignmentTest is (maxTests p) c)
]
where
is = tinstances p
validConditions :: Testable a => (Thy,[Expr]) -> a -> [Expr] -> [(Expr,Int)]
validConditions thyes p es =
[ (c,n) | c <- candidateConditions thyes p es
, let (is,n) = isCounterExampleUnder p c es
, is
] ++ [(expr False,0)]
weakestCondition :: Testable a => (Thy,[Expr]) -> a -> [Expr] -> Expr
weakestCondition thyes p es = fst
. maximumOn snd
. takeBound (computeConditionBound p)
$ validConditions thyes p es
isCounterExampleUnder :: Testable a => a -> Expr -> [Expr] -> (Bool, Int)
isCounterExampleUnder p c es = and'
[ not . errorToFalse $ p $-| es'
| (bs,es') <- take (maxTests p) $ groundsAndBinds (tinstances p) es
, errorToFalse $ eval False (c `assigning` bs)
]
where
and' ps = let len = length ps
in (and ps && len > computeMinFailures p && len > 0, len)
isVar :: Expr -> Bool
isVar (Var _ _) = True
isVar _ = False
fromBackgroundOf :: (Generalizable a, Typeable b) => String -> a -> Maybe b
fromBackgroundOf nm = listToMaybe
. mapMaybe evaluate
. filter (`isConstantNamed` nm)
. background
hasEq :: Generalizable a => a -> Bool
hasEq x = isJust $ "==" `fromBackgroundOf` x -: mayb (x >- x >- bool)
hasOrd :: Generalizable a => a -> Bool
hasOrd x = isJust $ "<=" `fromBackgroundOf` x -: mayb (x >- x >- bool)
(*==*) :: Generalizable a => a -> a -> Bool
x *==* y = x == y
where
(==) = fromMaybe (error "(*==*): no (==) operator in background")
$ "==" `fromBackgroundOf` x
(*/=*) :: Generalizable a => a -> a -> Bool
x */=* y = x /= y
where
(/=) = fromMaybe (error "(*/=*): no (/=) operator in background")
$ "/=" `fromBackgroundOf` x
(*<=*) :: Generalizable a => a -> a -> Bool
x *<=* y = x <= y
where
(<=) = fromMaybe (error "(*<=*): no (<=) operator in background")
$ "<=" `fromBackgroundOf` x
(*<*) :: Generalizable a => a -> a -> Bool
x *<* y = x < y
where
(<) = fromMaybe (error "(*<*): no (<) operator in background")
$ "<" `fromBackgroundOf` x