{-# LANGUAGE DeriveDataTypeable #-}
module Test.Extrapolate.Testable
( Testable (..)
, results
, limitedResults
, counterExample
, counterExamples
, Option (..)
, WithOption (..)
, testableMaxTests
, testableMaxConditionSize
, testableExtraInstances
, testableGrounds
, testableNames
, testableBackground
, testableMkEquation
, testableAtoms
)
where
import Data.List
import Data.Maybe
import Data.Ratio (Ratio)
import Test.Extrapolate.Utils
import Test.LeanCheck hiding (Testable, results, counterExample, counterExamples)
import Test.LeanCheck.Utils (bool, int)
import Test.Extrapolate.Generalizable
class Typeable a => Testable a where
resultiers :: a -> [[(Expr,Bool)]]
tinstances :: a -> Instances
options :: a -> Options
options a
_ = []
instance Testable a => Testable (WithOption a) where
resultiers :: WithOption a -> [[(Expr, Bool)]]
resultiers (a
p `With` Option
o) = a -> [[(Expr, Bool)]]
forall a. Testable a => a -> [[(Expr, Bool)]]
resultiers a
p
tinstances :: WithOption a -> Instances
tinstances (a
p `With` Option
o) = a -> Instances
forall a. Testable a => a -> Instances
tinstances a
p Instances -> Instances -> Instances
forall a. [a] -> [a] -> [a]
++ WithOption a -> Instances
forall a. Testable a => a -> Instances
testableExtraInstances (a
p a -> Option -> WithOption a
forall a. a -> Option -> WithOption a
`With` Option
o)
options :: WithOption a -> Options
options (a
p `With` Option
o) = Option
o Option -> Options -> Options
forall a. a -> [a] -> [a]
: a -> Options
forall a. Testable a => a -> Options
options a
p
instance Testable Bool where
resultiers :: Bool -> [[(Expr, Bool)]]
resultiers Bool
p = [[(String -> Bool -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"prop" Bool
p, Bool
p)]]
tinstances :: Bool -> Instances
tinstances Bool
_ = Bool -> Instances -> Instances
forall a. Generalizable a => a -> Instances -> Instances
instances Bool
bool (Instances -> Instances)
-> (Instances -> Instances) -> Instances -> Instances
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Instances -> Instances
forall a. Generalizable a => a -> Instances -> Instances
instances Int
int (Instances -> Instances) -> Instances -> Instances
forall a b. (a -> b) -> a -> b
$ []
instance (Testable b, Generalizable a, Listable a) => Testable (a->b) where
resultiers :: (a -> b) -> [[(Expr, Bool)]]
resultiers a -> b
p = (a -> [[(Expr, Bool)]]) -> [[a]] -> [[(Expr, Bool)]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT a -> [[(Expr, Bool)]]
resultiersFor [[a]]
forall a. Listable a => [[a]]
tiers
where resultiersFor :: a -> [[(Expr, Bool)]]
resultiersFor a
x = (Expr -> Expr) -> (Expr, Bool) -> (Expr, Bool)
forall t a b. (t -> a) -> (t, b) -> (a, b)
mapFst (Expr -> Expr -> Expr
replaceFun (String -> (a -> b) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"prop" a -> b
p Expr -> Expr -> Expr
:$ a -> Expr
forall a. Express a => a -> Expr
expr a
x)) ((Expr, Bool) -> (Expr, Bool))
-> [[(Expr, Bool)]] -> [[(Expr, Bool)]]
forall a b. (a -> b) -> [[a]] -> [[b]]
`mapT` b -> [[(Expr, Bool)]]
forall a. Testable a => a -> [[(Expr, Bool)]]
resultiers (a -> b
p a
x)
mapFst :: (t -> a) -> (t, b) -> (a, b)
mapFst t -> a
f (t
x,b
y) = (t -> a
f t
x, b
y)
tinstances :: (a -> b) -> Instances
tinstances a -> b
p = a -> Instances -> Instances
forall a. Generalizable a => a -> Instances -> Instances
instances ((a -> b) -> a
forall a b. (a -> b) -> a
undefarg a -> b
p) (Instances -> Instances) -> Instances -> Instances
forall a b. (a -> b) -> a -> b
$ b -> Instances
forall a. Testable a => a -> Instances
tinstances (a -> b
p a
forall a. HasCallStack => a
undefined)
where
undefarg :: (a -> b) -> a
undefarg :: (a -> b) -> a
undefarg a -> b
_ = a
forall a. HasCallStack => a
undefined
results :: Testable a => a -> [(Expr,Bool)]
results :: a -> [(Expr, Bool)]
results = [[(Expr, Bool)]] -> [(Expr, Bool)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Expr, Bool)]] -> [(Expr, Bool)])
-> (a -> [[(Expr, Bool)]]) -> a -> [(Expr, Bool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [[(Expr, Bool)]]
forall a. Testable a => a -> [[(Expr, Bool)]]
resultiers
limitedResults :: Testable a => a -> [(Expr,Bool)]
limitedResults :: a -> [(Expr, Bool)]
limitedResults a
p = Int -> [(Expr, Bool)] -> [(Expr, Bool)]
forall a. Int -> [a] -> [a]
take (a -> Int
forall a. Testable a => a -> Int
testableMaxTests a
p) (a -> [(Expr, Bool)]
forall a. Testable a => a -> [(Expr, Bool)]
results a
p)
counterExample :: Testable a => a -> Maybe Expr
counterExample :: a -> Maybe Expr
counterExample = Instances -> Maybe Expr
forall a. [a] -> Maybe a
listToMaybe (Instances -> Maybe Expr) -> (a -> Instances) -> a -> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Instances
forall a. Testable a => a -> Instances
counterExamples
counterExamples :: Testable a => a -> [Expr]
counterExamples :: a -> Instances
counterExamples a
p = [Expr
as | (Expr
as,Bool
False) <- a -> [(Expr, Bool)]
forall a. Testable a => a -> [(Expr, Bool)]
limitedResults a
p]
data Option = MaxTests Int
| Instances
| MaxConditionSize Int
deriving Typeable
data WithOption a = With
{ WithOption a -> a
property :: a
, WithOption a -> Option
option :: Option }
deriving Typeable
type Options = [Option]
testableMaxTests :: Testable a => a -> Int
testableMaxTests :: a -> Int
testableMaxTests a
p = [Int] -> Int
forall a. [a] -> a
head ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ [Int
m | MaxTests Int
m <- a -> Options
forall a. Testable a => a -> Options
options a
p] [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
500]
testableMaxConditionSize :: Testable a => a -> Int
testableMaxConditionSize :: a -> Int
testableMaxConditionSize a
p = [Int] -> Int
forall a. [a] -> a
head ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ [Int
m | MaxConditionSize Int
m <- a -> Options
forall a. Testable a => a -> Options
options a
p] [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
4]
testableExtraInstances :: Testable a => a -> Instances
a
p = [Instances] -> Instances
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Instances
is | ExtraInstances Instances
is <- a -> Options
forall a. Testable a => a -> Options
options a
p]
testableGrounds :: Testable a => a -> Expr -> [Expr]
testableGrounds :: a -> Expr -> Instances
testableGrounds a
p = Int -> Instances -> Instances
forall a. Int -> [a] -> [a]
take (a -> Int
forall a. Testable a => a -> Int
testableMaxTests a
p) (Instances -> Instances)
-> (Expr -> Instances) -> Expr -> Instances
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> [Instances]) -> Expr -> Instances
grounds (Instances -> Expr -> [Instances]
lookupTiers (Instances -> Expr -> [Instances])
-> Instances -> Expr -> [Instances]
forall a b. (a -> b) -> a -> b
$ a -> Instances
forall a. Testable a => a -> Instances
tinstances a
p)
testableMkEquation :: Testable a => a -> Expr -> Expr -> Expr
testableMkEquation :: a -> Expr -> Expr -> Expr
testableMkEquation a
p = Instances -> Expr -> Expr -> Expr
mkEquation (Instances -> Instances
getEqInstancesFromBackground Instances
is)
where
is :: Instances
is = a -> Instances
forall a. Testable a => a -> Instances
tinstances a
p
getEqInstancesFromBackground :: Instances -> Instances
getEqInstancesFromBackground Instances
is = Instances
eqs Instances -> Instances -> Instances
forall a. [a] -> [a] -> [a]
++ Instances
iqs
where
eqs :: Instances
eqs = [Expr
e | e :: Expr
e@(Value "==" _) <- Instances
bg]
iqs :: Instances
iqs = [Expr
e | e :: Expr
e@(Value "/=" _) <- Instances
bg]
bg :: Instances
bg = [Instances] -> Instances
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Expr -> Instances
forall a. Typeable a => Expr -> a
evl Expr
e | e :: Expr
e@(Value String
"background" Dynamic
_) <- Instances
is]
testableNames :: Testable a => a -> Expr -> [String]
testableNames :: a -> Expr -> [String]
testableNames = Instances -> Expr -> [String]
lookupNames (Instances -> Expr -> [String])
-> (a -> Instances) -> a -> Expr -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Instances
forall a. Testable a => a -> Instances
tinstances
testableBackground :: Testable a => a -> [Expr]
testableBackground :: a -> Instances
testableBackground a
p = [Instances] -> Instances
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Instances -> Expr -> Instances
forall a. Typeable a => a -> Expr -> a
eval Instances
forall a. a
err Expr
e | e :: Expr
e@(Value String
"background" Dynamic
_) <- a -> Instances
forall a. Testable a => a -> Instances
tinstances a
p]
where
err :: a
err = String -> a
forall a. HasCallStack => String -> a
error String
"Cannot evaluate background"
testableAtoms :: Testable a => a -> [[Expr]]
testableAtoms :: a -> [Instances]
testableAtoms = Instances -> [Instances]
atoms (Instances -> [Instances]) -> (a -> Instances) -> a -> [Instances]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Instances
forall a. Testable a => a -> Instances
tinstances
where
atoms :: Instances -> [[Expr]]
atoms :: Instances -> [Instances]
atoms Instances
is = ([Instances
vs] [Instances] -> [Instances] -> [Instances]
forall a. [[a]] -> [[a]] -> [[a]]
\/)
([Instances] -> [Instances])
-> ([[Instances]] -> [Instances]) -> [[Instances]] -> [Instances]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Instances] -> [Instances] -> [Instances])
-> [Instances] -> [[Instances]] -> [Instances]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [Instances] -> [Instances] -> [Instances]
forall a. [[a]] -> [[a]] -> [[a]]
(\/) [Instances
esU]
([[Instances]] -> [Instances]) -> [[Instances]] -> [Instances]
forall a b. (a -> b) -> a -> b
$ [ [Instances] -> Expr -> [Instances]
forall a. Typeable a => a -> Expr -> a
eval (String -> [Instances]
forall a. HasCallStack => String -> a
error String
msg :: [[Expr]]) Expr
tiersE
| tiersE :: Expr
tiersE@(Value String
"tiers" Dynamic
_) <- Instances
is ]
where
vs :: Instances
vs = Instances -> Instances
forall a. Ord a => [a] -> [a]
sort (Instances -> Instances)
-> (Instances -> Instances) -> Instances -> Instances
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeRep -> Maybe Expr) -> [TypeRep] -> Instances
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Instances -> TypeRep -> Maybe Expr
maybeHoleOfTy Instances
is) ([TypeRep] -> Instances)
-> (Instances -> [TypeRep]) -> Instances -> Instances
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TypeRep] -> [TypeRep]
typesInList ([TypeRep] -> [TypeRep])
-> (Instances -> [TypeRep]) -> Instances -> [TypeRep]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> TypeRep) -> Instances -> [TypeRep]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> TypeRep
typ (Instances -> Instances) -> Instances -> Instances
forall a b. (a -> b) -> a -> b
$ Instances
esU
esU :: Instances
esU = [Instances] -> Instances
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Expr -> Instances
forall a. Typeable a => Expr -> a
evl Expr
e | e :: Expr
e@(Value String
"background" Dynamic
_) <- Instances
is]
msg :: String
msg = String
"canditateConditions: wrong type, not [[Expr]]"