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
, (*==*)
, (*/=*)
, (*<=*)
, (*<*)
, counterExamples
, counterExampleGen
, counterExampleGens
, generalizations
, generalizationsCE
, generalizationsCEC
, generalizationsCounts
, weakestCondition
, candidateConditions
, conditionalGeneralization
, matchList
, newMatches
, Testable (..)
, results
, areInstancesOf
, expressionsT
)
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 Test.Extrapolate.Exprs (fold, unfold)
import Data.Maybe (listToMaybe, fromJust, fromMaybe, isJust, listToMaybe, catMaybes)
import Data.Either (isRight)
import Data.List (insert)
import Data.Functor ((<$>))
import Test.Extrapolate.Exprs
import Test.LeanCheck.Error (errorToFalse)
import Test.Extrapolate.TypeBinding
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 _ = [ 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 = [ constant "Just" (Just ->: mx) ]
++ bgEqWith1 (maybeEq ->:> mx)
++ bgOrdWith1 (maybeOrd ->:> 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 = [ constant "Left" (Left ->: exy)
, constant "Right" (Right ->: exy) ]
++ bgEqWith2 (eitherEq ->>:> exy)
++ bgOrdWith2 (eitherOrd ->>:> 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
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
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
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 = [ constant "length" (length -:> xs) ]
++ [ constant "elem" (elemBy (*==*) ->:> xs) | hasEq $ head xs ]
++ bgEqWith1 (listEq ->:> xs)
++ bgOrdWith1 (listOrd ->:> 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
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
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]
backgroundOf :: Generalizable a => a -> [Expr]
backgroundOf x = getBackground $ instances x []
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
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] ++ [360]
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] ++ [5]
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 _ = []
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 => Int -> a -> [Expr] -> [(Expr,[Expr])]
generalizationsCEC n p es | maxConditionSize p <= 0 = []
generalizationsCEC n p es =
[ (wc'', gs'')
| gs <- generalizations is es
, gs' <- vassignments gs
, let wc = weakestCondition n 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
expressionsT :: [Expr] -> [[Expr]]
expressionsT ds = [ds] \/ productMaybeWith ($$) es es `addWeight` 1
where
es = expressionsT ds
expressionsTT :: [[Expr]] -> [[Expr]]
expressionsTT dss = dss \/ productMaybeWith ($$) ess ess `addWeight` 1
where
ess = expressionsTT dss
conditionalGeneralization :: Testable a => Int -> a -> [Expr] -> [Expr] -> Maybe ([Expr],[Expr])
conditionalGeneralization m p es0 es1 = listToMaybe
[ ([c],es1)
| isJust $ es0 `newMatches` es1
, c <- candidates
, typ c == boolTy
, any (`elem` vars [c]) [(t,x) | Var x t <- vs]
, isCounterExampleUnder m p c es1
]
where
Just esM = es0 `newMatches` es1
candidates = concat . take (maxConditionSize p) . expressionsT $ vs ++ esU
vs = reverse [Var x (typ e) | (x,e) <- esM]
esU = concat [es | Instance "Background" _ es <- tinstances p]
weakestCondition :: Testable a => Int -> a -> [Expr] -> Expr
weakestCondition m p es = head $
[ c | c <- candidateConditions p es
, isCounterExampleUnder m p c es
] ++ [expr False]
where
candidateConditions :: Testable a => a -> [Expr] -> [Expr]
candidateConditions p es = expr True :
[ c
| c <- candidateExpressions p es
, typ c == boolTy
, hasVar c
, not (isAssignment c)
, not (isAssignmentTest is (maxTests p) c)
]
where
is = tinstances p
candidateExpressions :: Testable a => a -> [Expr] -> [Expr]
candidateExpressions p es = concat . take (maxConditionSize p) . expressionsTT
. foldr (\/) [vs ++ esU]
$ [ eval (error msg :: [[Expr]]) ess
| Instance "Listable" _ [ess] <- is ]
where
vs = [Var n t | (t,n) <- vars es]
esU = concat [es | Instance "Background" _ es <- is]
msg = "canditateConditions: wrong type, not [[Expr]]"
is = tinstances p
isCounterExampleUnder :: Testable a => Int -> a -> Expr -> [Expr] -> Bool
isCounterExampleUnder m p c es = and'
[ not . errorToFalse $ p $-| es'
| (bs,es') <- take m $ groundsAndBinds (tinstances p) es
, errorToFalse $ eval False (c `assigning` bs)
]
where
and' ps = and ps && length ps > m `div` 12
isVar :: Expr -> Bool
isVar (Var _ _) = True
isVar _ = False
fromBackgroundOf :: (Generalizable a, Typeable b) => String -> a -> Maybe b
fromBackgroundOf nm = listToMaybe
. catMaybes
. map 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