-- |
-- Module      : Test.LeanCheck.Function.ListsOfPairs
-- Copyright   : (c) 2015-2020 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part of LeanCheck,
-- a simple enumerative property-based testing library.
--
-- This module exports means to enumerate functions via lists of pairs.
--
-- This module considers functions as a finite list of exceptional input-output
-- cases to a default value (list of pairs of arguments and results).
module Test.LeanCheck.Function.ListsOfPairs
  ( (-->>)
  , exceptionPairs
  )
where

import Test.LeanCheck
import Test.LeanCheck.Tiers

-- | Given tiers of argument and result values,
--   return tiers of functional values.
(-->>) :: Eq a => [[a]] -> [[b]] -> [[a->b]]
[[a]]
xss -->> :: [[a]] -> [[b]] -> [[a -> b]]
-->> [[b]]
yss
  | [[a]] -> Bool
forall a. [[a]] -> Bool
finite [[a]]
xss  =  ([b] -> a -> b) -> [[[b]]] -> [[a -> b]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT ((a -> b
forall a. HasCallStack => a
undefined (a -> b) -> [(a, b)] -> a -> b
forall a b. Eq a => (a -> b) -> [(a, b)] -> a -> b
`mutate`) ([(a, b)] -> a -> b) -> ([b] -> [(a, b)]) -> [b] -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[a]]
xss))
                        ([[[b]]] -> [[[b]]]
forall a. [[[a]]] -> [[[a]]]
products ([[[b]]] -> [[[b]]]) -> [[[b]]] -> [[[b]]]
forall a b. (a -> b) -> a -> b
$ Int -> [[b]] -> [[[b]]]
forall a. Int -> a -> [a]
replicate ([a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([a] -> Int) -> [a] -> Int
forall a b. (a -> b) -> a -> b
$ [[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[a]]
xss) [[b]]
yss)
  | Bool
otherwise   =  ((b, [[b]]) -> [[a -> b]]) -> [[(b, [[b]])]] -> [[a -> b]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT (\(b
r,[[b]]
yss) -> ([(a, b)] -> a -> b) -> [[[(a, b)]]] -> [[a -> b]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT (b -> a -> b
forall a b. a -> b -> a
const b
r (a -> b) -> [(a, b)] -> a -> b
forall a b. Eq a => (a -> b) -> [(a, b)] -> a -> b
`mutate`)
                                                ([[a]] -> [[b]] -> [[[(a, b)]]]
forall a b. [[a]] -> [[b]] -> [[[(a, b)]]]
exceptionPairs [[a]]
xss [[b]]
yss))
                              ([[b]] -> [[(b, [[b]])]]
forall a. [[a]] -> [[(a, [[a]])]]
choices [[b]]
yss)


mutate :: Eq a => (a -> b) -> [(a,b)] -> (a -> b)
mutate :: (a -> b) -> [(a, b)] -> a -> b
mutate a -> b
f [(a, b)]
ms  =  ((a, b) -> (a -> b) -> a -> b) -> (a -> b) -> [(a, b)] -> a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (a, b) -> (a -> b) -> a -> b
forall t p. Eq t => (t, p) -> (t -> p) -> t -> p
mut a -> b
f [(a, b)]
ms
  where
  mut :: (t, p) -> (t -> p) -> t -> p
mut (t
x',p
fx') t -> p
f t
x  =  if t
x t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
x' then p
fx' else t -> p
f t
x


-- | Given tiers of input values and tiers of output values,
-- return tiers with all possible lists of input-output pairs.
-- These represent functional relations.
-- In the implementation of '-->>',
-- they represent exceptions to a constant function,
-- hence the name 'exceptionPairs'.
exceptionPairs :: [[a]] -> [[b]] -> [[ [(a,b)] ]]
exceptionPairs :: [[a]] -> [[b]] -> [[[(a, b)]]]
exceptionPairs [[a]]
xss [[b]]
yss  =  ([a] -> [[[(a, b)]]]) -> [[[a]]] -> [[[(a, b)]]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT [a] -> [[[(a, b)]]]
forall b. [b] -> [[[(b, b)]]]
exceptionsFor ([[a]] -> [[[a]]]
forall a. [[a]] -> [[[a]]]
incompleteSetsOf [[a]]
xss)
  where
--exceptionsFor :: [a] -> [[ [(a,b)] ]]
  exceptionsFor :: [b] -> [[[(b, b)]]]
exceptionsFor [b]
xs  =  [b] -> [b] -> [(b, b)]
forall a b. [a] -> [b] -> [(a, b)]
zip [b]
xs ([b] -> [(b, b)]) -> [[[b]]] -> [[[(b, b)]]]
forall a b. (a -> b) -> [[a]] -> [[b]]
`mapT` [[[b]]] -> [[[b]]]
forall a. [[[a]]] -> [[[a]]]
products ([[b]] -> b -> [[b]]
forall a b. a -> b -> a
const [[b]]
yss (b -> [[b]]) -> [b] -> [[[b]]]
forall a b. (a -> b) -> [a] -> [b]
`map` [b]
xs)
-- incompleteSetsOf is needed, instead of setsOf, because mutating *all* values
-- of a constant function makes no sense (we would have already enumerated that
-- function anyway).  As of 2c23c1a, it makes no difference whether
-- incompleteSetsOf is used instead of setsOf for types with less than 12
-- values because of the finite guard on `-->>`.

-- | Returns tiers of sets excluding the universe set.
--
-- > incompleteSetsOf (tiers :: [[Bool]])  =  [[],[[False],[True]],[]]
-- > incompleteSetsOf (tiers :: [[()]])    =  [[]]
--
-- This is the same as 'setsOf' on types with infinite values:
--
-- > incompleteSetsOf (tiers :: [[Int]])  =  setsOf (tiers :: [[Int]])
incompleteSetsOf :: [[a]] -> [[ [a] ]]
incompleteSetsOf :: [[a]] -> [[[a]]]
incompleteSetsOf  =  [[[a]]] -> [[[a]]]
forall a. [a] -> [a]
init ([[[a]]] -> [[[a]]]) -> ([[a]] -> [[[a]]]) -> [[a]] -> [[[a]]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[a]] -> [[[a]]]
forall a. [[a]] -> [[[a]]]
setsOf
-- the above implementation works because, and depends on the fact that:
-- the last tier returned by setsOf contains only the complete set