-- |
-- Module      : Test.Extrapolate.Testable
-- Copyright   : (c) 2017-2019 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part of Extrapolate,
-- a library for generalization of counter-examples.
--
-- This defines the 'Testable' typeclass
-- and utilities involving it.
--
-- You are probably better off importing "Test.Extrapolate".
{-# LANGUAGE DeriveDataTypeable #-} -- for GHC <= 7.8
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]


-- I don't love Option/WithOption.  It is clever but it is not __clear__.
-- Maybe remove from future versions of the tool?
data Option = MaxTests Int
            | ExtraInstances Instances
            | MaxConditionSize Int
  deriving Typeable -- for GHC <= 7.8

data WithOption a = With
                  { WithOption a -> a
property :: a
                  , WithOption a -> Option
option :: Option }
  deriving Typeable -- for GHC <= 7.8

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
testableExtraInstances :: a -> Instances
testableExtraInstances 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"

-- Given a property, returns the atoms to be passed to Speculate
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]]"