-- |
-- Module      : Test.Speculate.Expr.Ground
-- Copyright   : (c) 2016-2019 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part of Speculate.
--
-- Generate and evaluate ground values of expressions.
module Test.Speculate.Expr.Ground
  ( grounds
  , groundBinds
  , equal
  , lessOrEqual
  , less
  , inequal
  , isTrue
  , isFalse
  , condEqual
  , condEqualM
  , trueRatio
  )
where

import Test.Speculate.Expr.Core
import Test.Speculate.Expr.Instance
import Test.Speculate.Expr.Equate
import Test.LeanCheck
import Test.LeanCheck.Error (errorToFalse)
import Data.Ratio
import Data.Functor ((<$>)) -- for GHC < 7.10

-- | List all possible valuations of an expression (potentially infinite).
--   In pseudo-Haskell:
--
-- > take 3 $ grounds (lookupTiers preludeInstances) ((x + x) + y)
-- >   == [(0 + 0) + 0, (0 + 0) + 1, (1 + 1) + 0]
--
-- Note this function will return an empty list when a 'Listable' instance is
-- not found in the 'Instances' list.
grounds :: (Expr -> [[Expr]]) -> Expr -> [Expr]
grounds :: (Expr -> [[Expr]]) -> Expr -> [Expr]
grounds Expr -> [[Expr]]
tiersFor Expr
e = (Expr
e Expr -> [(Expr, Expr)] -> Expr
//-) ([(Expr, Expr)] -> Expr) -> [[(Expr, Expr)]] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> [[Expr]]) -> Expr -> [[(Expr, Expr)]]
groundBinds Expr -> [[Expr]]
tiersFor Expr
e

-- | List all possible variable bindings to an expression
--
-- > take 3 $ groundBinds (lookupTiers preludeInstances) ((x + x) + y)
-- >   == [ [("x",0),("y",0)]
-- >      , [("x",0),("y",1)]
-- >      , [("x",1),("y",0)] ]
groundBinds :: (Expr -> [[Expr]]) -> Expr -> [Binds]
groundBinds :: (Expr -> [[Expr]]) -> Expr -> [[(Expr, Expr)]]
groundBinds Expr -> [[Expr]]
tiersFor Expr
e =
  [[[(Expr, Expr)]]] -> [[(Expr, Expr)]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[[(Expr, Expr)]]] -> [[(Expr, Expr)]])
-> [[[(Expr, Expr)]]] -> [[(Expr, Expr)]]
forall a b. (a -> b) -> a -> b
$ [[[(Expr, Expr)]]] -> [[[(Expr, Expr)]]]
forall a. [[[a]]] -> [[[a]]]
products [(Expr -> (Expr, Expr)) -> [[Expr]] -> [[(Expr, Expr)]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT ((,) Expr
v) (Expr -> [[Expr]]
tiersFor Expr
v) | Expr
v <- Expr -> [Expr]
nubVars Expr
e]

-- | Are two expressions equal for a given number of tests?
equal :: Instances -> Int -> Expr -> Expr -> Bool
-- equal ti _ e1 e2 | e1 == e2 = isComparable ti e1 -- optional optimization
equal :: [Expr] -> Int -> Expr -> Expr -> Bool
equal [Expr]
ti Int
n = (Expr -> [Expr]) -> (Expr -> Expr -> Expr) -> Expr -> Expr -> Bool
isTrueComparison (Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
n ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> [[Expr]]) -> Expr -> [Expr]
grounds ([Expr] -> Expr -> [[Expr]]
lookupTiers [Expr]
ti)) ([Expr] -> Expr -> Expr -> Expr
mkEquation [Expr]
ti)

-- | Are two expressions equal
--   under a given condition
--   for a given number of tests?
condEqual :: Instances -> Int -> Expr -> Expr -> Expr -> Bool
condEqual :: [Expr] -> Int -> Expr -> Expr -> Expr -> Bool
condEqual [Expr]
ti Int
n Expr
pre Expr
e1 Expr
e2 = (Expr -> [Expr]) -> Expr -> Bool
isTrue (Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
n ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> [[Expr]]) -> Expr -> [Expr]
grounds ([Expr] -> Expr -> [[Expr]]
lookupTiers [Expr]
ti)) ([Expr] -> Expr -> Expr -> Expr -> Expr
mkConditionalEquation [Expr]
ti Expr
pre Expr
e1 Expr
e2)

-- | Are two expressions equal
--   under a given condition
--   for a given number of tests
--   and a minimum amount of tests
condEqualM :: Instances -> Int -> Int -> Expr -> Expr -> Expr -> Bool
condEqualM :: [Expr] -> Int -> Int -> Expr -> Expr -> Expr -> Bool
condEqualM [Expr]
ti Int
n Int
n0 Expr
pre Expr
e1 Expr
e2 = [Expr] -> Int -> Expr -> Expr -> Expr -> Bool
condEqual [Expr]
ti Int
n Expr
pre Expr
e1 Expr
e2 Bool -> Bool -> Bool
&& [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
cs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n0
  where
  cs :: [Expr]
cs = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter Expr -> Bool
evalBool ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
condition ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
n ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> [[Expr]]) -> Expr -> [Expr]
grounds ([Expr] -> Expr -> [[Expr]]
lookupTiers [Expr]
ti)
     (Expr -> [Expr]) -> Expr -> [Expr]
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr -> Expr -> Expr -> Expr
mkConditionalEquation [Expr]
ti Expr
pre Expr
e1 Expr
e2
  condition :: Expr -> Expr
condition Expr
ceq = let (Expr
ce,Expr
_,Expr
_) = Expr -> (Expr, Expr, Expr)
unConditionalEquation Expr
ceq in Expr
ce

-- | Are two expressions less-than-or-equal for a given number of tests?
lessOrEqual :: Instances -> Int -> Expr -> Expr -> Bool
lessOrEqual :: [Expr] -> Int -> Expr -> Expr -> Bool
lessOrEqual [Expr]
ti Int
n = (Expr -> [Expr]) -> (Expr -> Expr -> Expr) -> Expr -> Expr -> Bool
isTrueComparison (Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
n ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> [[Expr]]) -> Expr -> [Expr]
grounds ([Expr] -> Expr -> [[Expr]]
lookupTiers [Expr]
ti)) ([Expr] -> Expr -> Expr -> Expr
mkComparisonLE [Expr]
ti)

-- | Are two expressions less-than for a given number of tests?
less :: Instances -> Int -> Expr -> Expr -> Bool
less :: [Expr] -> Int -> Expr -> Expr -> Bool
less [Expr]
ti Int
n = (Expr -> [Expr]) -> (Expr -> Expr -> Expr) -> Expr -> Expr -> Bool
isTrueComparison (Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
n ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> [[Expr]]) -> Expr -> [Expr]
grounds ([Expr] -> Expr -> [[Expr]]
lookupTiers [Expr]
ti)) ([Expr] -> Expr -> Expr -> Expr
mkComparisonLT [Expr]
ti)

-- | Are two expressions inequal for *all* variable assignments?
--   Note this is different than @not . equal@.
inequal :: Instances -> Int -> Expr -> Expr -> Bool
inequal :: [Expr] -> Int -> Expr -> Expr -> Bool
inequal [Expr]
ti Int
n Expr
e1 Expr
e2 = (Expr -> [Expr]) -> Expr -> Bool
isFalse (Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
n ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> [[Expr]]) -> Expr -> [Expr]
grounds ([Expr] -> Expr -> [[Expr]]
lookupTiers [Expr]
ti)) ([Expr] -> Expr -> Expr -> Expr
mkEquation [Expr]
ti Expr
e1 Expr
e2)

-- | Under a maximum number of tests,
--   returns the ratio for which an expression holds true.
trueRatio :: Instances -> Int -> Expr -> Ratio Int
trueRatio :: [Expr] -> Int -> Expr -> Ratio Int
trueRatio [Expr]
is Int
n Expr
e = [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
trueBinds Int -> Int -> Ratio Int
forall a. Integral a => a -> a -> Ratio a
% [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
gs
  where
  gs :: [Expr]
gs = Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
n ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ (Expr -> [[Expr]]) -> Expr -> [Expr]
grounds ([Expr] -> Expr -> [[Expr]]
lookupTiers [Expr]
is) Expr
e
  trueBinds :: [Expr]
trueBinds = [Expr
e | Expr
e <- [Expr]
gs , Bool -> Expr -> Bool
forall a. Typeable a => a -> Expr -> a
eval Bool
False Expr
e]

isTrueComparison :: (Expr -> [Expr]) -> (Expr -> Expr -> Expr) -> Expr -> Expr -> Bool
isTrueComparison :: (Expr -> [Expr]) -> (Expr -> Expr -> Expr) -> Expr -> Expr -> Bool
isTrueComparison Expr -> [Expr]
grounds Expr -> Expr -> Expr
mkComparison Expr
e1 Expr
e2  =  (Expr -> [Expr]) -> Expr -> Bool
isTrue Expr -> [Expr]
grounds (Expr -> Expr -> Expr
mkComparison Expr
e1 Expr
e2)

-- | Is a boolean expression true for all variable assignments?
isTrue :: (Expr -> [Expr]) -> Expr -> Bool
isTrue :: (Expr -> [Expr]) -> Expr -> Bool
isTrue Expr -> [Expr]
grounds  =  (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
evalBool ([Expr] -> Bool) -> (Expr -> [Expr]) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
grounds

-- | Is an expression ALWAYS false?
-- This is *NOT* the same as not true.
isFalse :: (Expr -> [Expr]) -> Expr -> Bool
isFalse :: (Expr -> [Expr]) -> Expr -> Bool
isFalse Expr -> [Expr]
grounds  =  (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Bool
evalBool) ([Expr] -> Bool) -> (Expr -> [Expr]) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
grounds

evalBool :: Expr -> Bool
evalBool :: Expr -> Bool
evalBool  =  Bool -> Bool
errorToFalse (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Expr -> Bool
forall a. Typeable a => a -> Expr -> a
eval Bool
False