-- editorconfig-checker-disable-file
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications  #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

module Evaluation.Builtins.Costing where

import PlutusCore
import PlutusCore.Evaluation.Machine.CostStream
import PlutusCore.Evaluation.Machine.ExBudget
import PlutusCore.Evaluation.Machine.ExBudgetStream
import PlutusCore.Evaluation.Machine.ExMemory
import PlutusCore.Evaluation.Machine.ExMemoryUsage
import PlutusCore.Generators.QuickCheck.Builtin (magnitudesPositive)
import PlutusCore.Generators.QuickCheck.Utils

import Data.Bifunctor
import Data.Int
import Data.List
import Data.Maybe
import Data.SatInt
import Test.QuickCheck.Gen
import Test.Tasty
import Test.Tasty.QuickCheck

deriving newtype instance Foldable NonEmptyList  -- QuickCheck...

-- | Direct equality of two 'CostStream's. Same as @deriving stock Eq@. We don't want to do the
-- latter, because the semantics of a 'CostStream' are those of the sum of its elements and the
-- derived 'Eq' instance would conflict with that.
eqCostStream :: CostStream -> CostStream -> Bool
eqCostStream :: CostStream -> CostStream -> Bool
eqCostStream (CostLast SatInt
cost1) (CostLast SatInt
cost2) = SatInt
cost1 SatInt -> SatInt -> Bool
forall a. Eq a => a -> a -> Bool
== SatInt
cost2
eqCostStream (CostCons SatInt
cost1 CostStream
costs1) (CostCons SatInt
cost2 CostStream
costs2) =
    SatInt
cost1 SatInt -> SatInt -> Bool
forall a. Eq a => a -> a -> Bool
== SatInt
cost2 Bool -> Bool -> Bool
&& CostStream -> CostStream -> Bool
eqCostStream CostStream
costs1 CostStream
costs2
eqCostStream CostStream
_ CostStream
_ = Bool
False

fromCostList :: NonEmptyList CostingInteger -> CostStream
fromCostList :: NonEmptyList SatInt -> CostStream
fromCostList (NonEmpty [])               = [Char] -> CostStream
forall a. HasCallStack => [Char] -> a
error [Char]
"Panic: an empty non-empty list"
fromCostList (NonEmpty (SatInt
cost0 : [SatInt]
costs0)) = SatInt -> [SatInt] -> CostStream
go SatInt
cost0 [SatInt]
costs0 where
    go :: SatInt -> [SatInt] -> CostStream
go SatInt
cost []              = SatInt -> CostStream
CostLast SatInt
cost
    go SatInt
cost (SatInt
cost' : [SatInt]
costs) = SatInt -> CostStream -> CostStream
CostCons SatInt
cost (CostStream -> CostStream) -> CostStream -> CostStream
forall a b. (a -> b) -> a -> b
$ SatInt -> [SatInt] -> CostStream
go SatInt
cost' [SatInt]
costs

toCostList :: CostStream -> NonEmptyList CostingInteger
toCostList :: CostStream -> NonEmptyList SatInt
toCostList = [SatInt] -> NonEmptyList SatInt
forall a. [a] -> NonEmptyList a
NonEmpty ([SatInt] -> NonEmptyList SatInt)
-> (CostStream -> [SatInt]) -> CostStream -> NonEmptyList SatInt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CostStream -> [SatInt]
go where
    go :: CostStream -> [SatInt]
go (CostLast SatInt
cost)       = [SatInt
cost]
    go (CostCons SatInt
cost CostStream
costs) = SatInt
cost SatInt -> [SatInt] -> [SatInt]
forall a. a -> [a] -> [a]
: CostStream -> [SatInt]
go CostStream
costs

toExBudgetList :: ExBudgetStream -> NonEmptyList ExBudget
toExBudgetList :: ExBudgetStream -> NonEmptyList ExBudget
toExBudgetList = [ExBudget] -> NonEmptyList ExBudget
forall a. [a] -> NonEmptyList a
NonEmpty ([ExBudget] -> NonEmptyList ExBudget)
-> (ExBudgetStream -> [ExBudget])
-> ExBudgetStream
-> NonEmptyList ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExBudgetStream -> [ExBudget]
go where
    go :: ExBudgetStream -> [ExBudget]
go (ExBudgetLast ExBudget
budget)         = [ExBudget
budget]
    go (ExBudgetCons ExBudget
budget ExBudgetStream
budgets) = ExBudget
budget ExBudget -> [ExBudget] -> [ExBudget]
forall a. a -> [a] -> [a]
: ExBudgetStream -> [ExBudget]
go ExBudgetStream
budgets

-- | A list of ranges: @(0, 0), (1, 10) : (11, 100) : (101, 1000) : ... : [(10^18, maxBound)]@.
magnitudes :: [(SatInt, SatInt)]
magnitudes :: [(SatInt, SatInt)]
magnitudes
    = ((Integer, Integer) -> (SatInt, SatInt))
-> [(Integer, Integer)] -> [(SatInt, SatInt)]
forall a b. (a -> b) -> [a] -> [b]
map ((Integer -> SatInt)
-> (Integer -> SatInt) -> (Integer, Integer) -> (SatInt, SatInt)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Integer -> SatInt
forall a. Num a => Integer -> a
fromInteger Integer -> SatInt
forall a. Num a => Integer -> a
fromInteger)
    ([(Integer, Integer)] -> [(SatInt, SatInt)])
-> (Integer -> [(Integer, Integer)])
-> Integer
-> [(SatInt, SatInt)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Integer
0, Integer
0) (Integer, Integer) -> [(Integer, Integer)] -> [(Integer, Integer)]
forall a. a -> [a] -> [a]
:)
    ([(Integer, Integer)] -> [(Integer, Integer)])
-> (Integer -> [(Integer, Integer)])
-> Integer
-> [(Integer, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Integer) -> Integer -> [(Integer, Integer)]
magnitudesPositive (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
10)
    (Integer -> [(SatInt, SatInt)]) -> Integer -> [(SatInt, SatInt)]
forall a b. (a -> b) -> a -> b
$ SatInt -> Integer
forall a. Num a => SatInt -> a
fromSatInt (SatInt
forall a. Bounded a => a
maxBound :: SatInt)

-- | Return the range (in the sense of 'magnitudes') in which the given 'SatInt' belongs. E.g.
--
-- >>> toRange 42
-- (11,100)
-- >>> toRange 1234
-- (1001,10000)
toRange :: SatInt -> (SatInt, SatInt)
toRange :: SatInt -> (SatInt, SatInt)
toRange SatInt
cost = (SatInt, SatInt) -> Maybe (SatInt, SatInt) -> (SatInt, SatInt)
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> (SatInt, SatInt)
forall a. HasCallStack => [Char] -> a
error ([Char] -> (SatInt, SatInt)) -> [Char] -> (SatInt, SatInt)
forall a b. (a -> b) -> a -> b
$ [Char]
"Panic: an unexpected cost: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SatInt -> [Char]
forall a. Show a => a -> [Char]
show SatInt
cost) (Maybe (SatInt, SatInt) -> (SatInt, SatInt))
-> Maybe (SatInt, SatInt) -> (SatInt, SatInt)
forall a b. (a -> b) -> a -> b
$
    ((SatInt, SatInt) -> Bool)
-> [(SatInt, SatInt)] -> Maybe (SatInt, SatInt)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((SatInt -> SatInt -> Bool
forall a. Ord a => a -> a -> Bool
>= SatInt
cost) (SatInt -> Bool)
-> ((SatInt, SatInt) -> SatInt) -> (SatInt, SatInt) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SatInt, SatInt) -> SatInt
forall a b. (a, b) -> b
snd) [(SatInt, SatInt)]
magnitudes

-- | Generate a 'SatInt' in the given range.
chooseSatInt :: (SatInt, SatInt) -> Gen SatInt
chooseSatInt :: (SatInt, SatInt) -> Gen SatInt
chooseSatInt = (Int -> SatInt) -> Gen Int -> Gen SatInt
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> SatInt
unsafeToSatInt (Gen Int -> Gen SatInt)
-> ((SatInt, SatInt) -> Gen Int) -> (SatInt, SatInt) -> Gen SatInt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Int) -> Gen Int
chooseInt ((Int, Int) -> Gen Int)
-> ((SatInt, SatInt) -> (Int, Int)) -> (SatInt, SatInt) -> Gen Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SatInt -> Int)
-> (SatInt -> Int) -> (SatInt, SatInt) -> (Int, Int)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap SatInt -> Int
unSatInt SatInt -> Int
unSatInt

-- | Generate asymptotically bigger 'SatInt's with exponentially lower chance. This is in order to
-- make the generator of 'CostStream' produce streams whose sums are more or less evenly distributed
-- across 'magnitudes'.
instance Arbitrary SatInt where
    arbitrary :: Gen SatInt
arbitrary = [(Int, Gen SatInt)] -> Gen SatInt
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency ([(Int, Gen SatInt)] -> Gen SatInt)
-> ([Gen SatInt] -> [(Int, Gen SatInt)])
-> [Gen SatInt]
-> Gen SatInt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> [Gen SatInt] -> [(Int, Gen SatInt)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
freqs ([Gen SatInt] -> [(Int, Gen SatInt)])
-> ([Gen SatInt] -> [Gen SatInt])
-> [Gen SatInt]
-> [(Int, Gen SatInt)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Gen SatInt] -> [Gen SatInt]
forall a. [a] -> [a]
reverse ([Gen SatInt] -> Gen SatInt) -> [Gen SatInt] -> Gen SatInt
forall a b. (a -> b) -> a -> b
$ ((SatInt, SatInt) -> Gen SatInt)
-> [(SatInt, SatInt)] -> [Gen SatInt]
forall a b. (a -> b) -> [a] -> [b]
map (SatInt, SatInt) -> Gen SatInt
chooseSatInt [(SatInt, SatInt)]
magnitudes where
        freqs :: [Int]
freqs = (Double -> Int) -> [Double] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Double -> Int
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor ([Double] -> [Int]) -> [Double] -> [Int]
forall a b. (a -> b) -> a -> b
$ (Double -> Double) -> Double -> [Double]
forall a. (a -> a) -> a -> [a]
iterate (Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
1.3) (Double
2 :: Double)

    -- See Note [QuickCheck and integral types].
    shrink :: SatInt -> [SatInt]
shrink = (Int64 -> SatInt) -> [Int64] -> [SatInt]
forall a b. (a -> b) -> [a] -> [b]
map Int64 -> SatInt
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([Int64] -> [SatInt]) -> (SatInt -> [Int64]) -> SatInt -> [SatInt]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Arbitrary a => a -> [a]
shrink @Int64 (Int64 -> [Int64]) -> (SatInt -> Int64) -> SatInt -> [Int64]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SatInt -> Int64
forall a. Num a => SatInt -> a
fromSatInt

instance Arbitrary CostStream where
    arbitrary :: Gen CostStream
arbitrary = [(Int, Gen CostStream)] -> Gen CostStream
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
        [ -- Single-element streams an important enough corner-case to justify tilting the
          -- generator.
          (Int
1, SatInt -> CostStream
CostLast (SatInt -> CostStream) -> Gen SatInt -> Gen CostStream
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen SatInt
forall a. Arbitrary a => Gen a
arbitrary)
        , (Int
6, NonEmptyList SatInt -> CostStream
fromCostList (NonEmptyList SatInt -> CostStream)
-> Gen (NonEmptyList SatInt) -> Gen CostStream
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (NonEmptyList SatInt)
forall a. Arbitrary a => Gen a
arbitrary)
        ]

    shrink :: CostStream -> [CostStream]
shrink (CostLast SatInt
cost)       = (SatInt -> CostStream) -> [SatInt] -> [CostStream]
forall a b. (a -> b) -> [a] -> [b]
map SatInt -> CostStream
CostLast ([SatInt] -> [CostStream]) -> [SatInt] -> [CostStream]
forall a b. (a -> b) -> a -> b
$ SatInt -> [SatInt]
forall a. Arbitrary a => a -> [a]
shrink SatInt
cost
    shrink (CostCons SatInt
cost CostStream
costs) = SatInt -> CostStream
CostLast SatInt
cost CostStream -> [CostStream] -> [CostStream]
forall a. a -> [a] -> [a]
: CostStream
costs CostStream -> [CostStream] -> [CostStream]
forall a. a -> [a] -> [a]
: do
        -- Shrinking the recursive part first.
        (CostStream
costs', SatInt
cost') <- (CostStream, SatInt) -> [(CostStream, SatInt)]
forall a. Arbitrary a => a -> [a]
shrink (CostStream
costs, SatInt
cost)
        CostStream -> [CostStream]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CostStream -> [CostStream]) -> CostStream -> [CostStream]
forall a b. (a -> b) -> a -> b
$ SatInt -> CostStream -> CostStream
CostCons SatInt
cost' CostStream
costs'

instance CoArbitrary SatInt where
    -- See Note [QuickCheck and integral types]. No idea what kind of coverages we get here though.
    coarbitrary :: forall b. SatInt -> Gen b -> Gen b
coarbitrary = Int64 -> Gen b -> Gen b
forall b. Int64 -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
coarbitrary (Int64 -> Gen b -> Gen b)
-> (SatInt -> Int64) -> SatInt -> Gen b -> Gen b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => SatInt -> a
fromSatInt @Int64

instance Function SatInt where
    -- See Note [QuickCheck and integral types]. No idea what kind of coverages we get here though.
    function :: forall b. (SatInt -> b) -> SatInt :-> b
function = (SatInt -> Int64)
-> (Int64 -> SatInt) -> (SatInt -> b) -> SatInt :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
functionMap SatInt -> Int64
forall a. Num a => SatInt -> a
fromSatInt ((Int64 -> SatInt) -> (SatInt -> b) -> SatInt :-> b)
-> (Int64 -> SatInt) -> (SatInt -> b) -> SatInt :-> b
forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int64

-- | Same as '(===)' except accepts a custom equality checking function.
checkEqualsVia :: Show a => (a -> a -> Bool) -> a -> a -> Property
checkEqualsVia :: forall a. Show a => (a -> a -> Bool) -> a -> a -> Property
checkEqualsVia a -> a -> Bool
eq a
x a
y =
    [Char] -> Bool -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample (a -> [Char]
forall a. Show a => a -> [Char]
show a
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Bool -> [Char]
interpret Bool
res [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
y) Bool
res
  where
    res :: Bool
res = a -> a -> Bool
eq a
x a
y
    interpret :: Bool -> [Char]
interpret Bool
True  = [Char]
" === "
    interpret Bool
False = [Char]
" =/= "

-- | A value to use in tests to make sure what's not supposed to be forced isn't forced.
bottom :: a
bottom :: forall a. a
bottom = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"this value wasn't supposed to be forced"

-- | Test that 'magnitudes' has the correct bounds.
test_magnitudes :: TestTree
test_magnitudes :: TestTree
test_magnitudes =
    [Char] -> Bool -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"magnitudes" (Bool -> TestTree) -> Bool -> TestTree
forall a b. (a -> b) -> a -> b
$
        let check :: (a, a) -> (a, a) -> Bool
check (a
0, a
0)   (a
1,   a
10)  = Bool
True
            check (a
_, a
hi1) (a
lo2, a
hi2) = a
hi1 a -> a -> a
forall a. Num a => a -> a -> a
+ a
1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
lo2 Bool -> Bool -> Bool
&& a
hi1 a -> a -> a
forall a. Num a => a -> a -> a
* a
10 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
hi2
        in [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
           [ (SatInt, SatInt) -> SatInt
forall a b. (a, b) -> a
fst ([(SatInt, SatInt)] -> (SatInt, SatInt)
forall a. HasCallStack => [a] -> a
head [(SatInt, SatInt)]
magnitudes) SatInt -> SatInt -> Bool
forall a. Eq a => a -> a -> Bool
== SatInt
0
           , (SatInt, SatInt) -> SatInt
forall a b. (a, b) -> b
snd ([(SatInt, SatInt)] -> (SatInt, SatInt)
forall a. HasCallStack => [a] -> a
last [(SatInt, SatInt)]
magnitudes) SatInt -> SatInt -> Bool
forall a. Eq a => a -> a -> Bool
== SatInt
forall a. Bounded a => a
maxBound
           , [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool)
-> ([(SatInt, SatInt)] -> [Bool]) -> [(SatInt, SatInt)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SatInt, SatInt) -> (SatInt, SatInt) -> Bool)
-> [(SatInt, SatInt)] -> [(SatInt, SatInt)] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (SatInt, SatInt) -> (SatInt, SatInt) -> Bool
forall {a} {a}.
(Eq a, Eq a, Num a, Num a) =>
(a, a) -> (a, a) -> Bool
check [(SatInt, SatInt)]
magnitudes ([(SatInt, SatInt)] -> Bool) -> [(SatInt, SatInt)] -> Bool
forall a b. (a -> b) -> a -> b
$ [(SatInt, SatInt)] -> [(SatInt, SatInt)]
forall a. HasCallStack => [a] -> [a]
tail [(SatInt, SatInt)]
magnitudes
           ]

-- | Show the distribution of generated 'CostStream's as a diagnostic.
test_CostStreamDistribution :: TestTree
test_CostStreamDistribution :: TestTree
test_CostStreamDistribution =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"distribution of the generated CostStream values" (Property -> TestTree)
-> ((CostStream -> Property) -> Property)
-> (CostStream -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (CostStream -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
10000 ((CostStream -> Property) -> TestTree)
-> (CostStream -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
        \CostStream
costs ->
            let costsSum :: SatInt
costsSum = CostStream -> SatInt
sumCostStream CostStream
costs
                (SatInt
low, SatInt
high) = SatInt -> (SatInt, SatInt)
toRange SatInt
costsSum
            in [Char] -> Bool -> Property
forall prop. Testable prop => [Char] -> prop -> Property
label (SatInt -> [Char]
forall a. Show a => a -> [Char]
show SatInt
low [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" - " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SatInt -> [Char]
forall a. Show a => a -> [Char]
show SatInt
high) Bool
True

-- | Test that @fromCostList . toCostList@ is identity.
test_toCostListRoundtrip :: TestTree
test_toCostListRoundtrip :: TestTree
test_toCostListRoundtrip =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"fromCostList cancels toCostList" (Property -> TestTree)
-> ((CostStream -> Property) -> Property)
-> (CostStream -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (CostStream -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5000 ((CostStream -> Property) -> TestTree)
-> (CostStream -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \CostStream
costs ->
        (CostStream -> CostStream -> Bool)
-> CostStream -> CostStream -> Property
forall a. Show a => (a -> a -> Bool) -> a -> a -> Property
checkEqualsVia CostStream -> CostStream -> Bool
eqCostStream
            (NonEmptyList SatInt -> CostStream
fromCostList (NonEmptyList SatInt -> CostStream)
-> NonEmptyList SatInt -> CostStream
forall a b. (a -> b) -> a -> b
$ CostStream -> NonEmptyList SatInt
toCostList CostStream
costs)
            CostStream
costs

-- | Test that @toCostList . fromCostList@ is identity.
test_fromCostListRoundtrip :: TestTree
test_fromCostListRoundtrip :: TestTree
test_fromCostListRoundtrip =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"toCostList cancels fromCostList" (Property -> TestTree)
-> ((NonEmptyList SatInt -> Property) -> Property)
-> (NonEmptyList SatInt -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (NonEmptyList SatInt -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5000 ((NonEmptyList SatInt -> Property) -> TestTree)
-> (NonEmptyList SatInt -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \NonEmptyList SatInt
costs ->
        CostStream -> NonEmptyList SatInt
toCostList (NonEmptyList SatInt -> CostStream
fromCostList NonEmptyList SatInt
costs) NonEmptyList SatInt -> NonEmptyList SatInt -> Property
forall a. (Eq a, Show a) => a -> a -> Property
===
            NonEmptyList SatInt
costs

-- | Test that @uncurry reconsCost . unconsCost@ is identity.
test_unconsCostRoundtrip :: TestTree
test_unconsCostRoundtrip :: TestTree
test_unconsCostRoundtrip =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"reconsCost cancels unconsCost" (Property -> TestTree)
-> ((CostStream -> Property) -> Property)
-> (CostStream -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (CostStream -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5000 ((CostStream -> Property) -> TestTree)
-> (CostStream -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \CostStream
costs ->
        (CostStream -> CostStream -> Bool)
-> CostStream -> CostStream -> Property
forall a. Show a => (a -> a -> Bool) -> a -> a -> Property
checkEqualsVia CostStream -> CostStream -> Bool
eqCostStream
            ((SatInt -> Maybe CostStream -> CostStream)
-> (SatInt, Maybe CostStream) -> CostStream
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SatInt -> Maybe CostStream -> CostStream
reconsCost ((SatInt, Maybe CostStream) -> CostStream)
-> (SatInt, Maybe CostStream) -> CostStream
forall a b. (a -> b) -> a -> b
$ CostStream -> (SatInt, Maybe CostStream)
unconsCost CostStream
costs)
            CostStream
costs

-- | Test that 'sumCostStream' returns the sum of the elements of a 'CostStream'.
test_sumCostStreamIsSum :: TestTree
test_sumCostStreamIsSum :: TestTree
test_sumCostStreamIsSum =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"sumCostStream is sum" (Property -> TestTree)
-> ((CostStream -> Property) -> Property)
-> (CostStream -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (CostStream -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5000 ((CostStream -> Property) -> TestTree)
-> (CostStream -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \CostStream
costs ->
        CostStream -> SatInt
sumCostStream CostStream
costs SatInt -> SatInt -> Property
forall a. (Eq a, Show a) => a -> a -> Property
===
            NonEmptyList SatInt -> SatInt
forall a. Num a => NonEmptyList a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (CostStream -> NonEmptyList SatInt
toCostList CostStream
costs)

-- | Test that 'mapCostStream' applies a function to each element of a 'CostStream'.
test_mapCostStreamIsMap :: TestTree
test_mapCostStreamIsMap :: TestTree
test_mapCostStreamIsMap =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"mapCostStream is map" (Property -> TestTree)
-> ((Fun SatInt SatInt -> NonEmptyList SatInt -> Property)
    -> Property)
-> (Fun SatInt SatInt -> NonEmptyList SatInt -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int
-> (Fun SatInt SatInt -> NonEmptyList SatInt -> Property)
-> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
500 ((Fun SatInt SatInt -> NonEmptyList SatInt -> Property)
 -> TestTree)
-> (Fun SatInt SatInt -> NonEmptyList SatInt -> Property)
-> TestTree
forall a b. (a -> b) -> a -> b
$ \(Fun (SatInt :-> SatInt, SatInt, Shrunk)
_ SatInt -> SatInt
f) NonEmptyList SatInt
costs ->
        (CostStream -> CostStream -> Bool)
-> CostStream -> CostStream -> Property
forall a. Show a => (a -> a -> Bool) -> a -> a -> Property
checkEqualsVia CostStream -> CostStream -> Bool
eqCostStream
            ((SatInt -> SatInt) -> CostStream -> CostStream
mapCostStream SatInt -> SatInt
f (CostStream -> CostStream) -> CostStream -> CostStream
forall a b. (a -> b) -> a -> b
$ NonEmptyList SatInt -> CostStream
fromCostList NonEmptyList SatInt
costs)
            (NonEmptyList SatInt -> CostStream
fromCostList (NonEmptyList SatInt -> CostStream)
-> NonEmptyList SatInt -> CostStream
forall a b. (a -> b) -> a -> b
$ (SatInt -> SatInt) -> NonEmptyList SatInt -> NonEmptyList SatInt
forall a b. (a -> b) -> NonEmptyList a -> NonEmptyList b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SatInt -> SatInt
f NonEmptyList SatInt
costs)

-- | Test that the sum of a stream returned by 'addCostStream' equals the sum of the sums of its two
-- arguments.
test_addCostStreamIsAdd :: TestTree
test_addCostStreamIsAdd :: TestTree
test_addCostStreamIsAdd =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"addCostStream is add" (Property -> TestTree)
-> ((CostStream -> CostStream -> Property) -> Property)
-> (CostStream -> CostStream -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (CostStream -> CostStream -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5000 ((CostStream -> CostStream -> Property) -> TestTree)
-> (CostStream -> CostStream -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \CostStream
costs1 CostStream
costs2 ->
        CostStream -> SatInt
sumCostStream (CostStream -> CostStream -> CostStream
addCostStream CostStream
costs1 CostStream
costs2) SatInt -> SatInt -> Property
forall a. (Eq a, Show a) => a -> a -> Property
===
            CostStream -> SatInt
sumCostStream CostStream
costs1 SatInt -> SatInt -> SatInt
forall a. Num a => a -> a -> a
+ CostStream -> SatInt
sumCostStream CostStream
costs2

-- | Test that the sum of a stream returned by 'minCostStream' equals the minimum of the sums of its
-- two arguments.
test_minCostStreamIsMin :: TestTree
test_minCostStreamIsMin :: TestTree
test_minCostStreamIsMin =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"minCostStream is min" (Property -> TestTree)
-> ((CostStream -> CostStream -> Property) -> Property)
-> (CostStream -> CostStream -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (CostStream -> CostStream -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5000 ((CostStream -> CostStream -> Property) -> TestTree)
-> (CostStream -> CostStream -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \CostStream
costs1 CostStream
costs2 ->
        CostStream -> SatInt
sumCostStream (CostStream -> CostStream -> CostStream
minCostStream CostStream
costs1 CostStream
costs2) SatInt -> SatInt -> Property
forall a. (Eq a, Show a) => a -> a -> Property
===
            SatInt -> SatInt -> SatInt
forall a. Ord a => a -> a -> a
min (CostStream -> SatInt
sumCostStream CostStream
costs1) (CostStream -> SatInt
sumCostStream CostStream
costs2)

-- | Test that the sum of a stream returned by 'zipCostStream' equals an 'ExBudget' containing the
-- sums of its two arguments.
test_zipCostStreamIsZip :: TestTree
test_zipCostStreamIsZip :: TestTree
test_zipCostStreamIsZip =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"zipCostStream is zip" (Property -> TestTree)
-> ((CostStream -> CostStream -> Property) -> Property)
-> (CostStream -> CostStream -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (CostStream -> CostStream -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5000 ((CostStream -> CostStream -> Property) -> TestTree)
-> (CostStream -> CostStream -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \CostStream
costs1 CostStream
costs2 ->
        ExBudgetStream -> ExBudget
sumExBudgetStream (CostStream -> CostStream -> ExBudgetStream
zipCostStream CostStream
costs1 CostStream
costs2) ExBudget -> ExBudget -> Property
forall a. (Eq a, Show a) => a -> a -> Property
===
            ExCPU -> ExMemory -> ExBudget
ExBudget (SatInt -> ExCPU
ExCPU (SatInt -> ExCPU) -> SatInt -> ExCPU
forall a b. (a -> b) -> a -> b
$ CostStream -> SatInt
sumCostStream CostStream
costs1) (SatInt -> ExMemory
ExMemory (SatInt -> ExMemory) -> SatInt -> ExMemory
forall a b. (a -> b) -> a -> b
$ CostStream -> SatInt
sumCostStream CostStream
costs2)

-- | Test that 'mapCostStream' preserves the length of the stream.
test_mapCostStreamReasonableLength :: TestTree
test_mapCostStreamReasonableLength :: TestTree
test_mapCostStreamReasonableLength =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"mapCostStream: reasonable length" (Property -> TestTree)
-> ((Fun SatInt SatInt -> CostStream -> Property) -> Property)
-> (Fun SatInt SatInt -> CostStream -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (Fun SatInt SatInt -> CostStream -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
500 ((Fun SatInt SatInt -> CostStream -> Property) -> TestTree)
-> (Fun SatInt SatInt -> CostStream -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \(Fun (SatInt :-> SatInt, SatInt, Shrunk)
_ SatInt -> SatInt
f) CostStream
costs ->
        NonEmptyList SatInt -> Int
forall a. NonEmptyList a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (CostStream -> NonEmptyList SatInt
toCostList ((SatInt -> SatInt) -> CostStream -> CostStream
mapCostStream SatInt -> SatInt
f CostStream
costs)) Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
===
            NonEmptyList SatInt -> Int
forall a. NonEmptyList a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (CostStream -> NonEmptyList SatInt
toCostList CostStream
costs)

-- | Test that the length of the stream returned by 'addCostStream' equals the sum of the lengths of
-- its two arguments.
test_addCostStreamReasonableLength :: TestTree
test_addCostStreamReasonableLength :: TestTree
test_addCostStreamReasonableLength =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"addCostStream: reasonable length " (Property -> TestTree)
-> ((CostStream -> CostStream -> Property) -> Property)
-> (CostStream -> CostStream -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (CostStream -> CostStream -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5000 ((CostStream -> CostStream -> Property) -> TestTree)
-> (CostStream -> CostStream -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \CostStream
costs1 CostStream
costs2 ->
        Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
2 (NonEmptyList SatInt -> Int
forall a. NonEmptyList a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (CostStream -> NonEmptyList SatInt
toCostList (CostStream -> CostStream -> CostStream
addCostStream CostStream
costs1 CostStream
costs2))) Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
===
            NonEmptyList SatInt -> Int
forall a. NonEmptyList a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (CostStream -> NonEmptyList SatInt
toCostList CostStream
costs1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ NonEmptyList SatInt -> Int
forall a. NonEmptyList a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (CostStream -> NonEmptyList SatInt
toCostList CostStream
costs2)

-- | Test that the length of the stream returned by 'addCostStream' is
--
-- 1. greater than or equal to the minimum of the lengths of its two arguments
-- 2. smaller than or equal to the sum of the lengths of its two arguments.
test_minCostStreamReasonableLength :: TestTree
test_minCostStreamReasonableLength :: TestTree
test_minCostStreamReasonableLength =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"minCostStream: reasonable length " (Property -> TestTree)
-> ((CostStream -> CostStream -> Bool) -> Property)
-> (CostStream -> CostStream -> Bool)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (CostStream -> CostStream -> Bool) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5000 ((CostStream -> CostStream -> Bool) -> TestTree)
-> (CostStream -> CostStream -> Bool) -> TestTree
forall a b. (a -> b) -> a -> b
$ \CostStream
costs1 CostStream
costs2 ->
        let len1 :: Int
len1   = NonEmptyList SatInt -> Int
forall a. NonEmptyList a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (NonEmptyList SatInt -> Int) -> NonEmptyList SatInt -> Int
forall a b. (a -> b) -> a -> b
$ CostStream -> NonEmptyList SatInt
toCostList CostStream
costs1
            len2 :: Int
len2   = NonEmptyList SatInt -> Int
forall a. NonEmptyList a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (NonEmptyList SatInt -> Int) -> NonEmptyList SatInt -> Int
forall a b. (a -> b) -> a -> b
$ CostStream -> NonEmptyList SatInt
toCostList CostStream
costs2
            lenMin :: Int
lenMin = NonEmptyList SatInt -> Int
forall a. NonEmptyList a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (NonEmptyList SatInt -> Int)
-> (CostStream -> NonEmptyList SatInt) -> CostStream -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CostStream -> NonEmptyList SatInt
toCostList (CostStream -> Int) -> CostStream -> Int
forall a b. (a -> b) -> a -> b
$ CostStream -> CostStream -> CostStream
minCostStream CostStream
costs1 CostStream
costs2
        in Int
lenMin Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
len1 Int
len2 Bool -> Bool -> Bool
&& Int
lenMin Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
len1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
len2

-- | Test that the length of the stream returned by 'zipCostStream' equals the maximum of the
-- lengths of its two arguments.
test_zipCostStreamReasonableLength :: TestTree
test_zipCostStreamReasonableLength :: TestTree
test_zipCostStreamReasonableLength =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"zipCostStream: reasonable length " (Property -> TestTree)
-> ((CostStream -> CostStream -> Property) -> Property)
-> (CostStream -> CostStream -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (CostStream -> CostStream -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5000 ((CostStream -> CostStream -> Property) -> TestTree)
-> (CostStream -> CostStream -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \CostStream
costs1 CostStream
costs2 ->
        NonEmptyList ExBudget -> Int
forall a. NonEmptyList a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (ExBudgetStream -> NonEmptyList ExBudget
toExBudgetList (CostStream -> CostStream -> ExBudgetStream
zipCostStream CostStream
costs1 CostStream
costs2)) Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
===
            Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (NonEmptyList SatInt -> Int
forall a. NonEmptyList a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (CostStream -> NonEmptyList SatInt
toCostList CostStream
costs1)) (NonEmptyList SatInt -> Int
forall a. NonEmptyList a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (CostStream -> NonEmptyList SatInt
toCostList CostStream
costs2))

-- | Test that 'mapCostStream' preserves the laziness of its argument.
test_mapCostStreamHandlesBottom :: TestTree
test_mapCostStreamHandlesBottom :: TestTree
test_mapCostStreamHandlesBottom =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"mapCostStream handles bottom suffixes" (Property -> TestTree)
-> ((Fun SatInt SatInt -> [SatInt] -> Property) -> Property)
-> (Fun SatInt SatInt -> [SatInt] -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (Fun SatInt SatInt -> [SatInt] -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
500 ((Fun SatInt SatInt -> [SatInt] -> Property) -> TestTree)
-> (Fun SatInt SatInt -> [SatInt] -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \(Fun (SatInt :-> SatInt, SatInt, Shrunk)
_ SatInt -> SatInt
f) [SatInt]
xs ->
        let n :: Int
n = [SatInt] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SatInt]
xs
            -- 'fromCostList' forces an additional element, so we account for that here.
            suff :: [SatInt]
suff = SatInt
0 SatInt -> [SatInt] -> [SatInt]
forall a. a -> [a] -> [a]
: [SatInt]
forall a. a
bottom
            costs :: CostStream
costs = NonEmptyList SatInt -> CostStream
fromCostList (NonEmptyList SatInt -> CostStream)
-> ([SatInt] -> NonEmptyList SatInt) -> [SatInt] -> CostStream
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SatInt] -> NonEmptyList SatInt
forall a. [a] -> NonEmptyList a
NonEmpty ([SatInt] -> CostStream) -> [SatInt] -> CostStream
forall a b. (a -> b) -> a -> b
$ [SatInt]
xs [SatInt] -> [SatInt] -> [SatInt]
forall a. [a] -> [a] -> [a]
++ [SatInt]
suff
        in [SatInt] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Int -> [SatInt] -> [SatInt]
forall a. Int -> [a] -> [a]
take Int
n ([SatInt] -> [SatInt])
-> (CostStream -> [SatInt]) -> CostStream -> [SatInt]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyList SatInt -> [SatInt]
forall a. NonEmptyList a -> [a]
getNonEmpty (NonEmptyList SatInt -> [SatInt])
-> (CostStream -> NonEmptyList SatInt) -> CostStream -> [SatInt]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CostStream -> NonEmptyList SatInt
toCostList (CostStream -> [SatInt]) -> CostStream -> [SatInt]
forall a b. (a -> b) -> a -> b
$ (SatInt -> SatInt) -> CostStream -> CostStream
mapCostStream SatInt -> SatInt
f CostStream
costs) Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Int
n

-- | Test that 'mapCostStream' preserves the laziness of its two arguments.
test_addCostStreamHandlesBottom :: TestTree
test_addCostStreamHandlesBottom :: TestTree
test_addCostStreamHandlesBottom =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"addCostStream handles bottom suffixes" (Property -> TestTree)
-> ((Positive Int -> Property) -> Property)
-> (Positive Int -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (Positive Int -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5000 ((Positive Int -> Property) -> TestTree)
-> (Positive Int -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \(Positive Int
n) ->
        let interleave :: [a] -> [a] -> [a]
interleave [a]
xs [a]
ys = [[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[a]] -> [a]) -> [[a]] -> [a]
forall a b. (a -> b) -> a -> b
$ [[a]] -> [[a]]
forall a. [[a]] -> [[a]]
transpose [[a]
xs, [a]
ys]
            zeroToN :: [SatInt]
zeroToN = (Int -> SatInt) -> [Int] -> [SatInt]
forall a b. (a -> b) -> [a] -> [b]
map Int -> SatInt
unsafeToSatInt [Int
0 .. Int
n] [SatInt] -> [SatInt] -> [SatInt]
forall a. [a] -> [a] -> [a]
++ [SatInt]
forall a. a
bottom
            nPlus1To2NPlus1 :: [SatInt]
nPlus1To2NPlus1 = (Int -> SatInt) -> [Int] -> [SatInt]
forall a b. (a -> b) -> [a] -> [b]
map Int -> SatInt
unsafeToSatInt [Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1] [SatInt] -> [SatInt] -> [SatInt]
forall a. [a] -> [a] -> [a]
++ [SatInt]
forall a. a
bottom
            taken :: [SatInt]
taken = Int -> [SatInt] -> [SatInt]
forall a. Int -> [a] -> [a]
take Int
n ([SatInt] -> [SatInt])
-> (CostStream -> [SatInt]) -> CostStream -> [SatInt]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyList SatInt -> [SatInt]
forall a. NonEmptyList a -> [a]
getNonEmpty (NonEmptyList SatInt -> [SatInt])
-> (CostStream -> NonEmptyList SatInt) -> CostStream -> [SatInt]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CostStream -> NonEmptyList SatInt
toCostList (CostStream -> [SatInt]) -> CostStream -> [SatInt]
forall a b. (a -> b) -> a -> b
$ CostStream -> CostStream -> CostStream
addCostStream
                (NonEmptyList SatInt -> CostStream
fromCostList (NonEmptyList SatInt -> CostStream)
-> NonEmptyList SatInt -> CostStream
forall a b. (a -> b) -> a -> b
$ [SatInt] -> NonEmptyList SatInt
forall a. [a] -> NonEmptyList a
NonEmpty [SatInt]
zeroToN)
                (NonEmptyList SatInt -> CostStream
fromCostList (NonEmptyList SatInt -> CostStream)
-> NonEmptyList SatInt -> CostStream
forall a b. (a -> b) -> a -> b
$ [SatInt] -> NonEmptyList SatInt
forall a. [a] -> NonEmptyList a
NonEmpty [SatInt]
nPlus1To2NPlus1)
        in  -- Every element in the resulting stream comes from one of the generated lists.
            (SatInt -> Bool) -> [SatInt] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\SatInt
cost -> SatInt
cost SatInt -> [SatInt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SatInt] -> [SatInt] -> [SatInt]
forall a. [a] -> [a] -> [a]
interleave [SatInt]
zeroToN [SatInt]
nPlus1To2NPlus1) [SatInt]
taken Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&.
            -- No element is duplicated.
            [SatInt] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (([SatInt] -> SatInt) -> [[SatInt]] -> [SatInt]
forall a b. (a -> b) -> [a] -> [b]
map [SatInt] -> SatInt
forall a. HasCallStack => [a] -> a
head ([[SatInt]] -> [SatInt])
-> ([SatInt] -> [[SatInt]]) -> [SatInt] -> [SatInt]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SatInt] -> [[SatInt]]
forall a. Eq a => [a] -> [[a]]
group ([SatInt] -> [SatInt]) -> [SatInt] -> [SatInt]
forall a b. (a -> b) -> a -> b
$ [SatInt] -> [SatInt]
forall a. Ord a => [a] -> [a]
sort [SatInt]
taken) Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== [SatInt] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SatInt]
taken

-- | Test that 'minCostStream' preserves the laziness of its two arguments.
test_minCostStreamHandlesBottom :: TestTree
test_minCostStreamHandlesBottom :: TestTree
test_minCostStreamHandlesBottom =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"minCostStream handles bottom suffixes" (Property -> TestTree)
-> (([SatInt] -> [SatInt] -> Bool) -> Property)
-> ([SatInt] -> [SatInt] -> Bool)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ([SatInt] -> [SatInt] -> Bool) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5000 (([SatInt] -> [SatInt] -> Bool) -> TestTree)
-> ([SatInt] -> [SatInt] -> Bool) -> TestTree
forall a b. (a -> b) -> a -> b
$ \[SatInt]
xs [SatInt]
ys ->
        let m :: SatInt
m = SatInt -> SatInt -> SatInt
forall a. Ord a => a -> a -> a
min ([SatInt] -> SatInt
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [SatInt]
xs) ([SatInt] -> SatInt
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [SatInt]
ys)
            -- 'minCostStream' can force only a single extra element of the stream.
            suff :: [SatInt]
suff = SatInt
0 SatInt -> [SatInt] -> [SatInt]
forall a. a -> [a] -> [a]
: [SatInt]
forall a. a
bottom
            xsYsMin :: CostStream
xsYsMin = CostStream -> CostStream -> CostStream
minCostStream
                (NonEmptyList SatInt -> CostStream
fromCostList (NonEmptyList SatInt -> CostStream)
-> ([SatInt] -> NonEmptyList SatInt) -> [SatInt] -> CostStream
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SatInt] -> NonEmptyList SatInt
forall a. [a] -> NonEmptyList a
NonEmpty ([SatInt] -> CostStream) -> [SatInt] -> CostStream
forall a b. (a -> b) -> a -> b
$ [SatInt]
xs [SatInt] -> [SatInt] -> [SatInt]
forall a. [a] -> [a] -> [a]
++ [SatInt]
suff)
                (NonEmptyList SatInt -> CostStream
fromCostList (NonEmptyList SatInt -> CostStream)
-> ([SatInt] -> NonEmptyList SatInt) -> [SatInt] -> CostStream
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SatInt] -> NonEmptyList SatInt
forall a. [a] -> NonEmptyList a
NonEmpty ([SatInt] -> CostStream) -> [SatInt] -> CostStream
forall a b. (a -> b) -> a -> b
$ [SatInt]
ys [SatInt] -> [SatInt] -> [SatInt]
forall a. [a] -> [a] -> [a]
++ [SatInt]
suff)
        in -- Rolling '(+)' over a list representing the minimum of two streams eventually
           -- gives us the sum of the minimum stream before triggering any of the bottoms.
           SatInt -> [SatInt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem SatInt
m ([SatInt] -> Bool)
-> (NonEmptyList SatInt -> [SatInt]) -> NonEmptyList SatInt -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SatInt -> SatInt -> SatInt) -> SatInt -> [SatInt] -> [SatInt]
forall b a. (b -> a -> b) -> b -> [a] -> [b]
scanl' SatInt -> SatInt -> SatInt
forall a. Num a => a -> a -> a
(+) SatInt
0 ([SatInt] -> [SatInt])
-> (NonEmptyList SatInt -> [SatInt])
-> NonEmptyList SatInt
-> [SatInt]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyList SatInt -> [SatInt]
forall a. NonEmptyList a -> [a]
getNonEmpty (NonEmptyList SatInt -> Bool) -> NonEmptyList SatInt -> Bool
forall a b. (a -> b) -> a -> b
$ CostStream -> NonEmptyList SatInt
toCostList CostStream
xsYsMin

-- | Pad the shortest of the given lists by appending the given element to it until the length of
-- the result matches the length of the other list.
--
-- >>> postAlignWith 'a' "bcd" "e"
-- ("bcd","eaa")
-- >>> postAlignWith 'a' "b" "cdef"
-- ("baaa","cdef")
postAlignWith :: a -> [a] -> [a] -> ([a], [a])
postAlignWith :: forall a. a -> [a] -> [a] -> ([a], [a])
postAlignWith a
z [a]
xs [a]
ys = ([a] -> [a]
align [a]
xs, [a] -> [a]
align [a]
ys) where
    align :: [a] -> [a]
align [a]
zs = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs Int -> Int -> Int
forall a. Ord a => a -> a -> a
`max` [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ys) ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ [a]
zs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ a -> [a]
forall a. a -> [a]
repeat a
z

-- | Test that 'zipCostStream' preserves the laziness of its two arguments.
test_zipCostStreamHandlesBottom :: TestTree
test_zipCostStreamHandlesBottom :: TestTree
test_zipCostStreamHandlesBottom =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"zipCostStream handles bottom suffixes" (Property -> TestTree)
-> (([SatInt] -> [SatInt] -> Bool) -> Property)
-> ([SatInt] -> [SatInt] -> Bool)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ([SatInt] -> [SatInt] -> Bool) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5000 (([SatInt] -> [SatInt] -> Bool) -> TestTree)
-> ([SatInt] -> [SatInt] -> Bool) -> TestTree
forall a b. (a -> b) -> a -> b
$ \[SatInt]
xs [SatInt]
ys ->
        let z :: ExBudget
z = ExCPU -> ExMemory -> ExBudget
ExBudget (SatInt -> ExCPU
ExCPU (SatInt -> ExCPU) -> SatInt -> ExCPU
forall a b. (a -> b) -> a -> b
$ [SatInt] -> SatInt
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [SatInt]
xs) (SatInt -> ExMemory
ExMemory (SatInt -> ExMemory) -> SatInt -> ExMemory
forall a b. (a -> b) -> a -> b
$ [SatInt] -> SatInt
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [SatInt]
ys)
            ([SatInt]
xsA, [SatInt]
ysA) = SatInt -> [SatInt] -> [SatInt] -> ([SatInt], [SatInt])
forall a. a -> [a] -> [a] -> ([a], [a])
postAlignWith SatInt
0 [SatInt]
xs [SatInt]
ys
            -- 'fromCostList' forces an additional element, so we account for that here.
            suff :: [SatInt]
suff = SatInt
0 SatInt -> [SatInt] -> [SatInt]
forall a. a -> [a] -> [a]
: [SatInt]
forall a. a
bottom
            xys :: ExBudgetStream
xys = CostStream -> CostStream -> ExBudgetStream
zipCostStream
                (NonEmptyList SatInt -> CostStream
fromCostList (NonEmptyList SatInt -> CostStream)
-> ([SatInt] -> NonEmptyList SatInt) -> [SatInt] -> CostStream
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SatInt] -> NonEmptyList SatInt
forall a. [a] -> NonEmptyList a
NonEmpty ([SatInt] -> CostStream) -> [SatInt] -> CostStream
forall a b. (a -> b) -> a -> b
$ [SatInt]
xsA [SatInt] -> [SatInt] -> [SatInt]
forall a. [a] -> [a] -> [a]
++ [SatInt]
suff)
                (NonEmptyList SatInt -> CostStream
fromCostList (NonEmptyList SatInt -> CostStream)
-> ([SatInt] -> NonEmptyList SatInt) -> [SatInt] -> CostStream
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SatInt] -> NonEmptyList SatInt
forall a. [a] -> NonEmptyList a
NonEmpty ([SatInt] -> CostStream) -> [SatInt] -> CostStream
forall a b. (a -> b) -> a -> b
$ [SatInt]
ysA [SatInt] -> [SatInt] -> [SatInt]
forall a. [a] -> [a] -> [a]
++ [SatInt]
suff)
        in  -- Rolling '(<>)' over a list representing the zipped cost streams eventually
            -- gives us an 'ExBudget' containing the sums of the streams computed separately.
            ExBudget -> [ExBudget] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ExBudget
z ([ExBudget] -> Bool)
-> (NonEmptyList ExBudget -> [ExBudget])
-> NonEmptyList ExBudget
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ExBudget -> ExBudget -> ExBudget)
-> ExBudget -> [ExBudget] -> [ExBudget]
forall b a. (b -> a -> b) -> b -> [a] -> [b]
scanl' ExBudget -> ExBudget -> ExBudget
forall a. Semigroup a => a -> a -> a
(<>) ExBudget
forall a. Monoid a => a
mempty ([ExBudget] -> [ExBudget])
-> (NonEmptyList ExBudget -> [ExBudget])
-> NonEmptyList ExBudget
-> [ExBudget]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyList ExBudget -> [ExBudget]
forall a. NonEmptyList a -> [a]
getNonEmpty (NonEmptyList ExBudget -> Bool) -> NonEmptyList ExBudget -> Bool
forall a b. (a -> b) -> a -> b
$ ExBudgetStream -> NonEmptyList ExBudget
toExBudgetList ExBudgetStream
xys

-- | The size 'sierpinskiRose' of the given depth.
sierpinskiSize :: Int -> Int
sierpinskiSize :: Int -> Int
sierpinskiSize Int
n
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1    = Int
1
    | Bool
otherwise = Int -> Int
sierpinskiSize (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
3 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1

-- | Return a finite balanced tree with each node (apart from the leaves) having exactly 3 children.
-- The parameter is the depth of the tree.
-- Named after https://en.wikipedia.org/wiki/Sierpi%C5%84ski_triangle
sierpinskiRose :: Int -> CostRose
sierpinskiRose :: Int -> CostRose
sierpinskiRose Int
n0
    | Int
n0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1   = SatInt -> CostRose
singletonRose SatInt
1
    | Bool
otherwise = SatInt -> [CostRose] -> CostRose
CostRose (Int -> SatInt
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n0) ([CostRose] -> CostRose) -> (Int -> [CostRose]) -> Int -> CostRose
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> CostRose) -> [Int] -> [CostRose]
forall a b. (a -> b) -> [a] -> [b]
map Int -> CostRose
sierpinskiRose ([Int] -> [CostRose]) -> (Int -> [Int]) -> Int -> [CostRose]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> [Int]
forall a. Int -> a -> [a]
replicate Int
3 (Int -> CostRose) -> Int -> CostRose
forall a b. (a -> b) -> a -> b
$ Int
n0 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

-- | Traverse a 'sierpinskiRose' of the given depth and display the total amount of elements
-- processed. See 'test_flattenCostRoseIsLinear' for why we do this.
test_flattenCostRoseIsLinearForSierpinskiRose :: Int -> TestTree
test_flattenCostRoseIsLinearForSierpinskiRose :: Int -> TestTree
test_flattenCostRoseIsLinearForSierpinskiRose Int
depth =
    let size :: Int
size = Int -> Int
sierpinskiSize Int
depth
    in [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty ([Char]
"sierpinski rose: taking " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
size [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" elements") (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
1 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
            NonEmptyList SatInt -> Int
forall a. NonEmptyList a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (CostStream -> NonEmptyList SatInt
toCostList (CostStream -> NonEmptyList SatInt)
-> (CostRose -> CostStream) -> CostRose -> NonEmptyList SatInt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CostRose -> CostStream
flattenCostRose (CostRose -> NonEmptyList SatInt)
-> CostRose -> NonEmptyList SatInt
forall a b. (a -> b) -> a -> b
$ Int -> CostRose
sierpinskiRose Int
depth) Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
===
                Int
size

-- | Test that traversing a larger 'CostRose' takes _linearly_ more time. The actual test can only
-- be done with eyes unfortunately, because the tests are way too noisy for evaluation times to be
-- reported even remotely accurately.
test_flattenCostRoseIsLinear :: TestTree
test_flattenCostRoseIsLinear :: TestTree
test_flattenCostRoseIsLinear = [Char] -> [TestTree] -> TestTree
testGroup [Char]
"flattenCostRose is linear"
    [ Int -> TestTree
test_flattenCostRoseIsLinearForSierpinskiRose Int
12
    , Int -> TestTree
test_flattenCostRoseIsLinearForSierpinskiRose Int
13
    , Int -> TestTree
test_flattenCostRoseIsLinearForSierpinskiRose Int
14
    ]

{- Note [Generating a CostRose]
We use an overly pedantic approach for generating 'CostRose's. The idea is simple: generate a list
of costs, chop it into chunks and turn each of those into its own 'CostRose' recursively, then
assemble them together to get the resulting 'CostRose'. We do it this way, because that makes it
trivial to ensure that the generator is not exponential as each generated 'CostRose' only has those
(and only those) elements in it that came from the generated list and the generator for lists isn't
exponential. It also makes it easy to control the distribution of the shapes of generated
'CostRose's. Do we want long forests? Do we want to cover all possible trees up to a certain depth?
All of that is easy to tweak, although the actual logic can get complicated pretty quickly. But at
least all this complicated logic is fairly local unlike with the usual approach when generation is
size-driven and minor tweaks in size handling at any step can result in major changes in the overall
generation strategy such as exponential growth of the generated objects.
-}

-- See Note [Generating a CostRose].
-- | Generate a 'CostRose' from the given list by splitting the list into sublists and generating
-- a 'CostRose' for each of them recursively.
genCostRose :: NonEmptyList SatInt -> Gen CostRose
genCostRose :: NonEmptyList SatInt -> Gen CostRose
genCostRose (NonEmpty [])             = [Char] -> Gen CostRose
forall a. HasCallStack => [Char] -> a
error [Char]
"Panic: an empty non-empty list"
genCostRose (NonEmpty (SatInt
cost : [SatInt]
costs)) =
    SatInt -> [CostRose] -> CostRose
CostRose SatInt
cost ([CostRose] -> CostRose) -> Gen [CostRose] -> Gen CostRose
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((NonEmptyList SatInt -> Gen CostRose)
-> [NonEmptyList SatInt] -> Gen [CostRose]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse NonEmptyList SatInt -> Gen CostRose
genCostRose ([NonEmptyList SatInt] -> Gen [CostRose])
-> Gen [NonEmptyList SatInt] -> Gen [CostRose]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [SatInt] -> Gen [NonEmptyList SatInt]
forall a. [a] -> Gen [NonEmptyList a]
multiSplit1 [SatInt]
costs)

fromCostRose :: CostRose -> NonEmptyList SatInt
fromCostRose :: CostRose -> NonEmptyList SatInt
fromCostRose (CostRose SatInt
cost [CostRose]
costs) =
    [SatInt] -> NonEmptyList SatInt
forall a. [a] -> NonEmptyList a
NonEmpty ([SatInt] -> NonEmptyList SatInt)
-> [SatInt] -> NonEmptyList SatInt
forall a b. (a -> b) -> a -> b
$ SatInt
cost SatInt -> [SatInt] -> [SatInt]
forall a. a -> [a] -> [a]
: (CostRose -> [SatInt]) -> [CostRose] -> [SatInt]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (NonEmptyList SatInt -> [SatInt]
forall a. NonEmptyList a -> [a]
getNonEmpty (NonEmptyList SatInt -> [SatInt])
-> (CostRose -> NonEmptyList SatInt) -> CostRose -> [SatInt]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CostRose -> NonEmptyList SatInt
fromCostRose) [CostRose]
costs

instance Arbitrary CostRose where
    -- By default the lengt of generated lists is capped at 100, which would give us too small of
    -- 'CostRose's, so we scale the size parameter.
    arbitrary :: Gen CostRose
arbitrary = (Int -> Int)
-> Gen (NonEmptyList SatInt) -> Gen (NonEmptyList SatInt)
forall a. (Int -> Int) -> Gen a -> Gen a
scale (Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
10) Gen (NonEmptyList SatInt)
forall a. Arbitrary a => Gen a
arbitrary Gen (NonEmptyList SatInt)
-> (NonEmptyList SatInt -> Gen CostRose) -> Gen CostRose
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= NonEmptyList SatInt -> Gen CostRose
genCostRose

    shrink :: CostRose -> [CostRose]
shrink (CostRose SatInt
cost [CostRose]
costs) = do
        -- Shrinking the recursive part first.
        ([CostRose]
costs', SatInt
cost') <- ([CostRose], SatInt) -> [([CostRose], SatInt)]
forall a. Arbitrary a => a -> [a]
shrink ([CostRose]
costs, SatInt
cost)
        CostRose -> [CostRose]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CostRose -> [CostRose]) -> CostRose -> [CostRose]
forall a b. (a -> b) -> a -> b
$ SatInt -> [CostRose] -> CostRose
CostRose SatInt
cost' [CostRose]
costs'

-- | Return the lengths of all the forests in a 'CostRose'.
collectListLengths :: CostRose -> [Int]
collectListLengths :: CostRose -> [Int]
collectListLengths (CostRose SatInt
_ [CostRose]
costs) = [CostRose] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CostRose]
costs Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: (CostRose -> [Int]) -> [CostRose] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CostRose -> [Int]
collectListLengths [CostRose]
costs

-- | Show the distribution of forest lengths in generated 'CostRose' values as a diagnostic.
test_CostRoseListLengthsDistribution :: TestTree
test_CostRoseListLengthsDistribution :: TestTree
test_CostRoseListLengthsDistribution =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"distribution of list lengths in CostRose values" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        Int -> (CostRose -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
1000 ((CostRose -> Property) -> Property)
-> (CostRose -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \CostRose
rose ->
            let render :: a -> [Char]
render a
n
                    | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
10   = a -> [Char]
forall a. Show a => a -> [Char]
show a
n
                    | Bool
otherwise = a -> [Char]
forall a. Show a => a -> [Char]
show a
m [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" < n <= " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show (a
m a -> a -> a
forall a. Num a => a -> a -> a
+ a
10)
                    where m :: a
m = [a] -> a
forall a. HasCallStack => [a] -> a
head ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$ (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
n) [a
10, a
20..]
            in [Char] -> [[Char]] -> Bool -> Property
forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"n" ((Int -> [Char]) -> [Int] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Int -> [Char]
forall {a}. (Show a, Ord a, Num a, Enum a) => a -> [Char]
render ([Int] -> [[Char]]) -> ([Int] -> [Int]) -> [Int] -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0) ([Int] -> [[Char]]) -> [Int] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ CostRose -> [Int]
collectListLengths CostRose
rose) Bool
True

-- | Test that 'genCostRose' only takes costs from its argument when generating a 'CostRose'.
test_genCostRoseSound :: TestTree
test_genCostRoseSound :: TestTree
test_genCostRoseSound =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"genCostRose puts 100% of its input and nothing else into the output" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        Int -> (NonEmptyList SatInt -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
1000 ((NonEmptyList SatInt -> Property) -> Property)
-> (NonEmptyList SatInt -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \NonEmptyList SatInt
costs ->
            Gen CostRose -> (CostRose -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (NonEmptyList SatInt -> Gen CostRose
genCostRose NonEmptyList SatInt
costs) ((CostRose -> Property) -> Property)
-> (CostRose -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \CostRose
rose ->
                CostRose -> NonEmptyList SatInt
fromCostRose CostRose
rose NonEmptyList SatInt -> NonEmptyList SatInt -> Property
forall a. (Eq a, Show a) => a -> a -> Property
===
                    NonEmptyList SatInt
costs

-- | Test that 'flattenCostRose' returns the elements of its argument.
test_flattenCostRoseSound :: TestTree
test_flattenCostRoseSound :: TestTree
test_flattenCostRoseSound =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"flattenCostRose puts 100% of its input and nothing else into the output" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        Int -> (CostRose -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
1000 ((CostRose -> Property) -> Property)
-> (CostRose -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \CostRose
rose ->
            -- This assumes that 'flattenCostRose' is left-biased, which isn't really necessary, but
            -- it doesn't seem like we're giving up on the assumption any time soon anyway, so why
            -- not keep it simple instead of sorting the results.
            (CostStream -> CostStream -> Bool)
-> CostStream -> CostStream -> Property
forall a. Show a => (a -> a -> Bool) -> a -> a -> Property
checkEqualsVia CostStream -> CostStream -> Bool
eqCostStream
                (CostRose -> CostStream
flattenCostRose CostRose
rose)
                (NonEmptyList SatInt -> CostStream
fromCostList (NonEmptyList SatInt -> CostStream)
-> NonEmptyList SatInt -> CostStream
forall a b. (a -> b) -> a -> b
$ CostRose -> NonEmptyList SatInt
fromCostRose CostRose
rose)

-- | Test that 'flattenCostRose' is lazy.
test_flattenCostRoseHandlesBottom :: TestTree
test_flattenCostRoseHandlesBottom :: TestTree
test_flattenCostRoseHandlesBottom =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"flattenCostRose handles bottom subtrees" (Property -> TestTree)
-> (([SatInt] -> [SatInt] -> Property) -> Property)
-> ([SatInt] -> [SatInt] -> Property)
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ([SatInt] -> [SatInt] -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5000 (([SatInt] -> [SatInt] -> Property) -> TestTree)
-> ([SatInt] -> [SatInt] -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \[SatInt]
xs [SatInt]
ys ->
        -- Create a 'CostRose' with a negative cost somewhere in it, then replace the subtree after
        -- that cost with 'bottom' and check that we can get to the negative cost without forcing
        -- the bottom. We could've implemented generation of 'CostRose's with bottoms in them, but
        -- 'genCostRose' is already complicated enough, so it's easier to put a magical number into
        -- its input and postprocess the generated rose.
        Gen CostRose -> (CostRose -> Bool) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (NonEmptyList SatInt -> Gen CostRose
genCostRose (NonEmptyList SatInt -> Gen CostRose)
-> ([SatInt] -> NonEmptyList SatInt) -> [SatInt] -> Gen CostRose
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SatInt] -> NonEmptyList SatInt
forall a. [a] -> NonEmptyList a
NonEmpty ([SatInt] -> Gen CostRose) -> [SatInt] -> Gen CostRose
forall a b. (a -> b) -> a -> b
$ [SatInt]
xs [SatInt] -> [SatInt] -> [SatInt]
forall a. [a] -> [a] -> [a]
++ (-SatInt
1) SatInt -> [SatInt] -> [SatInt]
forall a. a -> [a] -> [a]
: [SatInt]
ys) ((CostRose -> Bool) -> Property) -> (CostRose -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \CostRose
rose ->
            let spoilCostRose :: CostRose -> CostRose
spoilCostRose (CostRose SatInt
cost [CostRose]
forest) =
                    SatInt -> [CostRose] -> CostRose
CostRose SatInt
cost ([CostRose] -> CostRose) -> [CostRose] -> CostRose
forall a b. (a -> b) -> a -> b
$ if SatInt
cost SatInt -> SatInt -> Bool
forall a. Eq a => a -> a -> Bool
== -SatInt
1
                        -- 'flattenCostRose' forces an additional constructor, which is why 'bottom'
                        -- is put into a list.
                        then [CostRose
forall a. a
bottom]
                        else (CostRose -> CostRose) -> [CostRose] -> [CostRose]
forall a b. (a -> b) -> [a] -> [b]
map CostRose -> CostRose
spoilCostRose [CostRose]
forest
            in SatInt -> NonEmptyList SatInt -> Bool
forall a. Eq a => a -> NonEmptyList a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (-SatInt
1) (NonEmptyList SatInt -> Bool)
-> (CostRose -> NonEmptyList SatInt) -> CostRose -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CostStream -> NonEmptyList SatInt
toCostList (CostStream -> NonEmptyList SatInt)
-> (CostRose -> CostStream) -> CostRose -> NonEmptyList SatInt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CostRose -> CostStream
flattenCostRose (CostRose -> Bool) -> CostRose -> Bool
forall a b. (a -> b) -> a -> b
$ CostRose -> CostRose
spoilCostRose CostRose
rose

-- | Test that 'memoryUsage' called over a value of a built-in type never returns a stream
-- containing a negative cost.
test_costsAreNeverNegative :: TestTree
test_costsAreNeverNegative :: TestTree
test_costsAreNeverNegative =
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"costs coming from 'memoryUsage' are never negative" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        Int -> (Some (ValueOf DefaultUni) -> Bool) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
1000 ((Some (ValueOf DefaultUni) -> Bool) -> Property)
-> (Some (ValueOf DefaultUni) -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(Some (ValueOf DefaultUni)
val :: Some (ValueOf DefaultUni)) ->
            (SatInt -> Bool) -> NonEmptyList SatInt -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SatInt -> SatInt -> Bool
forall a. Ord a => a -> a -> Bool
>= SatInt
0) (NonEmptyList SatInt -> Bool)
-> (CostRose -> NonEmptyList SatInt) -> CostRose -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CostStream -> NonEmptyList SatInt
toCostList (CostStream -> NonEmptyList SatInt)
-> (CostRose -> CostStream) -> CostRose -> NonEmptyList SatInt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CostRose -> CostStream
flattenCostRose (CostRose -> Bool) -> CostRose -> Bool
forall a b. (a -> b) -> a -> b
$ Some (ValueOf DefaultUni) -> CostRose
forall a. ExMemoryUsage a => a -> CostRose
memoryUsage Some (ValueOf DefaultUni)
val

test_costing :: TestTree
test_costing :: TestTree
test_costing = [Char] -> [TestTree] -> TestTree
testGroup [Char]
"costing"
    [ TestTree
test_magnitudes
    , TestTree
test_CostStreamDistribution
    , TestTree
test_toCostListRoundtrip
    , TestTree
test_fromCostListRoundtrip
    , TestTree
test_unconsCostRoundtrip
    , TestTree
test_sumCostStreamIsSum
    , TestTree
test_mapCostStreamIsMap
    , TestTree
test_addCostStreamIsAdd
    , TestTree
test_minCostStreamIsMin
    , TestTree
test_zipCostStreamIsZip
    , TestTree
test_mapCostStreamReasonableLength
    , TestTree
test_addCostStreamReasonableLength
    , TestTree
test_minCostStreamReasonableLength
    , TestTree
test_zipCostStreamReasonableLength
    , TestTree
test_mapCostStreamHandlesBottom
    , TestTree
test_addCostStreamHandlesBottom
    , TestTree
test_minCostStreamHandlesBottom
    , TestTree
test_zipCostStreamHandlesBottom
    , TestTree
test_flattenCostRoseIsLinear
    , TestTree
test_CostRoseListLengthsDistribution
    , TestTree
test_genCostRoseSound
    , TestTree
test_flattenCostRoseSound
    , TestTree
test_flattenCostRoseHandlesBottom
    , TestTree
test_costsAreNeverNegative
    ]