{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstrainedClassMethods #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

-- | Operations for generating random elements of Num like types, that sum to a particular total.
--   The class `Foldy` (defined in the TheKnot.hs) gives the operations necessary to do this.
--   In this module we define the helper functions necessary to define the methods of the Foldy class.
--   The helper functions do not need to know about the Foldy class, and are not dependent upon any of
--   the mutually recursive operations defined in TheKnot, except the operations defined in the Complete class.
--   That class is defined in this module, but the instance for that class is made in TheKnot.
module Constrained.SumList where

import Data.Either (partitionEithers)
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
import Data.Semigroup (sconcat)
import System.Random (Random (..))
import Test.QuickCheck (Arbitrary, Gen, choose, shuffle, vectorOf)

import Constrained.Base
import Constrained.Conformance (conformsToSpec)
import Constrained.Core (Value (..))
import Constrained.GenT (
  GE (..),
  GenT,
  MonadGenError (..),
  oneofT,
  pureGen,
  push,
  scaleT,
  sizeT,
  suchThatT,
  tryGenT,
 )
import Constrained.List (List (..), ListCtx (..))
import Constrained.NumSpec (
  IntW (..),
  MaybeBounded (..),
  NumSpec (..),
  Numeric,
  geqSpec,
  gtSpec,
  leqSpec,
  ltSpec,
  nubOrd,
 )
import Control.Applicative ((<|>))
import Control.Monad (guard)
import Data.List ((\\))
import Data.Maybe (fromMaybe, isNothing, listToMaybe)
import qualified Data.Set as Set
import GHC.Stack
import Prettyprinter hiding (cat)

-- ====================================================================
-- What we need to know, that can only be defined in TheKnot module, is
-- abstracted into this class, which will be a precondition on the `Foldy` class

class HasSpec a => Complete a where
  -- method standing for `simplifySpec`
  simplifyA :: Specification a -> Specification a

  -- method standing for `genFromSpecT`
  genFromSpecA :: forall m. (HasCallStack, HasSpec a, MonadGenError m) => Specification a -> GenT m a

  -- method standing for method `theAddFn` from the `Foldy` class
  theAddA :: Numeric a => IntW '[a, a] a
  theAddA = forall b. NumLike b => IntW '[b, b] b
AddW

-- ==========================================================
-- helpers

-- ===================================================================

noNegativeValues :: forall a. (Num a, Eq a, MaybeBounded a) => Bool
noNegativeValues :: forall a. (Num a, Eq a, MaybeBounded a) => Bool
noNegativeValues = forall a. MaybeBounded a => Maybe a
lowerBound @a forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just a
0

knownUpperBound ::
  (TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
  Specification a ->
  Maybe a
knownUpperBound :: forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound (ExplainSpec [String]
_ Specification a
s) = forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
s
knownUpperBound Specification a
TrueSpec = forall a. MaybeBounded a => Maybe a
upperBound
knownUpperBound (MemberSpec NonEmpty a
as) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum NonEmpty a
as
knownUpperBound ErrorSpec {} = forall a. Maybe a
Nothing
knownUpperBound SuspendedSpec {} = forall a. MaybeBounded a => Maybe a
upperBound
knownUpperBound (TypeSpec (NumSpecInterval Maybe a
lo Maybe a
hi) [a]
cant) = Maybe a -> Maybe a -> Maybe a
upper (Maybe a
lo forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. MaybeBounded a => Maybe a
lowerBound) (Maybe a
hi forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. MaybeBounded a => Maybe a
upperBound)
  where
    upper :: Maybe a -> Maybe a -> Maybe a
upper Maybe a
_ Maybe a
Nothing = forall a. Maybe a
Nothing
    upper Maybe a
Nothing (Just a
b) = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ [a
b, a
b forall a. Num a => a -> a -> a
- a
1 ..] forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
cant
    upper (Just a
a) (Just a
b)
      | a
a forall a. Eq a => a -> a -> Bool
== a
b = a
a forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard (a
a forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [a]
cant)
      | Bool
otherwise = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ [a
b, a
b forall a. Num a => a -> a -> a
- a
1 .. a
a] forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
cant

knownLowerBound ::
  (TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
  Specification a ->
  Maybe a
knownLowerBound :: forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound (ExplainSpec [String]
_ Specification a
s) = forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
s
knownLowerBound Specification a
TrueSpec = forall a. MaybeBounded a => Maybe a
lowerBound
knownLowerBound (MemberSpec NonEmpty a
as) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum NonEmpty a
as
knownLowerBound ErrorSpec {} = forall a. Maybe a
Nothing
knownLowerBound SuspendedSpec {} = forall a. MaybeBounded a => Maybe a
lowerBound
knownLowerBound (TypeSpec (NumSpecInterval Maybe a
lo Maybe a
hi) [a]
cant) =
  Maybe a -> Maybe a -> Maybe a
lower (Maybe a
lo forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. MaybeBounded a => Maybe a
lowerBound) (Maybe a
hi forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. MaybeBounded a => Maybe a
upperBound)
  where
    lower :: Maybe a -> Maybe a -> Maybe a
lower Maybe a
Nothing Maybe a
_ = forall a. Maybe a
Nothing
    lower (Just a
a) Maybe a
Nothing = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ [a
a, a
a forall a. Num a => a -> a -> a
+ a
1 ..] forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
cant
    lower (Just a
a) (Just a
b)
      | a
a forall a. Eq a => a -> a -> Bool
== a
b = a
a forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard (a
a forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [a]
cant)
      | Bool
otherwise = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ [a
a, a
a forall a. Num a => a -> a -> a
+ a
1 .. a
b] forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
cant

isEmptyNumSpec ::
  (TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) => Specification a -> Bool
isEmptyNumSpec :: forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Bool
isEmptyNumSpec = \case
  ExplainSpec [String]
_ Specification a
s -> forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Bool
isEmptyNumSpec Specification a
s
  ErrorSpec {} -> Bool
True
  Specification a
TrueSpec -> Bool
False
  MemberSpec NonEmpty a
_ -> Bool
False -- MemberSpec always has at least one element (NE.NonEmpty)
  SuspendedSpec {} -> Bool
False
  TypeSpec TypeSpec a
i [a]
cant -> forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ forall a. (Enum a, Num a, MaybeBounded a) => NumSpec a -> [a]
enumerateInterval TypeSpec a
i forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
cant

-- | Note: potentially infinite list
enumerateInterval :: (Enum a, Num a, MaybeBounded a) => NumSpec a -> [a]
enumerateInterval :: forall a. (Enum a, Num a, MaybeBounded a) => NumSpec a -> [a]
enumerateInterval (NumSpecInterval Maybe a
lo Maybe a
hi) =
  case (Maybe a
lo forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. MaybeBounded a => Maybe a
lowerBound, Maybe a
hi forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. MaybeBounded a => Maybe a
upperBound) of
    (Maybe a
Nothing, Maybe a
Nothing) -> forall {a}. [a] -> [a] -> [a]
interleave [a
0 ..] [-a
1, -a
2 ..]
    (Maybe a
Nothing, Just a
b) -> [a
b, a
b forall a. Num a => a -> a -> a
- a
1 ..]
    (Just a
a, Maybe a
Nothing) -> [a
a ..]
    (Just a
a, Just a
b) -> [a
a .. a
b]
  where
    interleave :: [a] -> [a] -> [a]
interleave [] [a]
ys = [a]
ys
    interleave (a
x : [a]
xs) [a]
ys = a
x forall a. a -> [a] -> [a]
: [a] -> [a] -> [a]
interleave [a]
ys [a]
xs

-- ========================================================================
-- Operations to complete the Foldy instances genNumList, genListWithSize

genNumList ::
  forall a m.
  ( MonadGenError m
  , Arbitrary a
  , Integral a
  , MaybeBounded a
  , TypeSpec a ~ NumSpec a
  , -- , Foldy a
    Random a
  , Complete a
  ) =>
  Specification a ->
  Specification a ->
  GenT m [a]
genNumList :: forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
 TypeSpec a ~ NumSpec a, Random a, Complete a) =>
Specification a -> Specification a -> GenT m [a]
genNumList Specification a
elemSIn Specification a
foldSIn = do
  let extraElemConstraints :: Specification a
extraElemConstraints
        | Just a
l <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemSIn
        , a
0 forall a. Ord a => a -> a -> Bool
<= a
l
        , Just a
u <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldSIn =
            forall a. OrdLike a => a -> Specification a
leqSpec a
u
        | Bool
otherwise = forall a. Specification a
TrueSpec
      elemSIn' :: Specification a
elemSIn' = Specification a
elemSIn forall a. Semigroup a => a -> a -> a
<> Specification a
extraElemConstraints
  Specification a
normElemS <- Specification a -> GenT m (Specification a)
normalize Specification a
elemSIn'
  Specification a
normFoldS <- Specification a -> GenT m (Specification a)
normalize Specification a
foldSIn
  let narrowedSpecs :: (Specification a, Specification a)
narrowedSpecs = forall a.
(TypeSpec a ~ NumSpec a, Arbitrary a, Integral a, Random a,
 MaybeBounded a, Complete a) =>
(Specification a, Specification a)
-> (Specification a, Specification a)
narrowFoldSpecs (Specification a
normElemS, Specification a
normFoldS)
  forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
    ( forall a. [a] -> NonEmpty a
NE.fromList
        [ String
"Can't generate list of ints with fold constraint"
        , String
"  elemSpec = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
elemSIn
        , String
"  normElemSpec = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
normElemS
        , String
"  foldSpec = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
foldSIn
        ]
    )
    forall a b. (a -> b) -> a -> b
$ forall (m' :: * -> *).
MonadGenError m' =>
(Specification a, Specification a) -> Int -> [a] -> GenT m' [a]
gen (Specification a, Specification a)
narrowedSpecs Int
50 [] forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Gen [a]
shuffle
  where
    normalize :: Specification a -> GenT m (Specification a)
normalize (ExplainSpec [String]
es Specification a
x) = forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Specification a -> GenT m (Specification a)
normalize Specification a
x
    normalize spec :: Specification a
spec@SuspendedSpec {} = do
      Int
sz <- forall (m :: * -> *). Monad m => GenT m Int
sizeT
      Specification a
spec' <- Int -> Int -> Set a -> Specification a -> GenT m (Specification a)
buildMemberSpec Int
sz (Int
100 :: Int) forall a. Monoid a => a
mempty Specification a
spec
      Specification a -> GenT m (Specification a)
normalize forall a b. (a -> b) -> a -> b
$ Specification a
spec'
    normalize Specification a
spec =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty forall a. OrdLike a => a -> Specification a
geqSpec forall a. MaybeBounded a => Maybe a
lowerBound
          forall a. Semigroup a => a -> a -> a
<> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty forall a. OrdLike a => a -> Specification a
leqSpec forall a. MaybeBounded a => Maybe a
upperBound
          forall a. Semigroup a => a -> a -> a
<> Specification a
spec

    buildMemberSpec :: Int -> Int -> Set a -> Specification a -> GenT m (Specification a)
buildMemberSpec Int
_ Int
0 Set a
es Specification a
_ =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
            (forall a. Set a -> [a]
Set.toList Set a
es)
            (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"In genNumList, in buildMemberSpec 'es' is the empty list, can't make a MemberSpec from that")
        )
    buildMemberSpec Int
sz Int
fuel Set a
es Specification a
spec = do
      Maybe a
me <- forall (m :: * -> *) a. (Int -> Int) -> GenT m a -> GenT m a
scaleT (forall a b. a -> b -> a
const Int
sz) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadGenError m =>
GenT GE a -> GenT m (Maybe a)
tryGenT (forall a (m :: * -> *).
(Complete a, HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecA @a Specification a
spec)
      let sz' :: Int
sz'
            | Int
sz forall a. Ord a => a -> a -> Bool
> Int
100 = Int
sz
            | forall a. Maybe a -> Bool
isNothing Maybe a
me = Int
2 forall a. Num a => a -> a -> a
* Int
sz forall a. Num a => a -> a -> a
+ Int
1
            | Just a
e <- Maybe a
me, forall a. Ord a => a -> Set a -> Bool
Set.member a
e Set a
es = Int
2 forall a. Num a => a -> a -> a
* Int
sz forall a. Num a => a -> a -> a
+ Int
1
            | Bool
otherwise = Int
sz
      Int -> Int -> Set a -> Specification a -> GenT m (Specification a)
buildMemberSpec
        Int
sz'
        (Int
fuel forall a. Num a => a -> a -> a
- Int
1)
        (forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set a
es (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Ord a => a -> Set a -> Set a
Set.insert Set a
es) Maybe a
me)
        Specification a
spec

    gen ::
      forall m'. MonadGenError m' => (Specification a, Specification a) -> Int -> [a] -> GenT m' [a]
    gen :: forall (m' :: * -> *).
MonadGenError m' =>
(Specification a, Specification a) -> Int -> [a] -> GenT m' [a]
gen (Specification a
elemS, Specification a
foldS) Int
fuel [a]
lst
      | Int
fuel forall a. Ord a => a -> a -> Bool
<= Int
0
      , Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ a
0 forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldS =
          forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
genErrorNE forall a b. (a -> b) -> a -> b
$
            forall a. [a] -> NonEmpty a
NE.fromList
              [ String
"Ran out of fuel in genNumList"
              , String
"  elemSpec =" forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
elemSIn
              , String
"  foldSpec = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
foldSIn
              , String
"  lst = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. [a] -> [a]
reverse [a]
lst)
              ]
      | ErrorSpec NonEmpty String
err <- Specification a
foldS = forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
genErrorNE NonEmpty String
err
      | ErrorSpec {} <- Specification a
elemS = forall (f :: * -> *) a. Applicative f => a -> f a
pure [a]
lst -- At this point we know that foldS admits 0 (also this should be redundant)
      | a
0 forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldS = forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
[GenT GE a] -> GenT m a
oneofT [forall (f :: * -> *) a. Applicative f => a -> f a
pure [a]
lst, forall (m'' :: * -> *). MonadGenError m'' => GenT m'' [a]
nonemptyList @GE] -- TODO: distribution
      | Bool
otherwise = forall (m'' :: * -> *). MonadGenError m'' => GenT m'' [a]
nonemptyList
      where
        isUnsat :: (Specification a, Specification a) -> Bool
isUnsat (Specification a
elemSpec, Specification a
foldSpec) = forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Bool
isEmptyNumSpec Specification a
foldSpec Bool -> Bool -> Bool
|| Bool -> Bool
not (a
0 forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldSpec) Bool -> Bool -> Bool
&& forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Bool
isEmptyNumSpec Specification a
elemSpec
        nonemptyList :: forall m''. MonadGenError m'' => GenT m'' [a]
        nonemptyList :: forall (m'' :: * -> *). MonadGenError m'' => GenT m'' [a]
nonemptyList = do
          (a
x, (Specification a, Specification a)
specs') <-
            forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
              ( forall a. [a] -> NonEmpty a
NE.fromList
                  [ String
"Generating an element:"
                  , String
"  elemS = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
elemS
                  , String
"  foldS = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
foldS
                  , String
"  fuel  = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
fuel
                  , String
"  lst   = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. [a] -> [a]
reverse [a]
lst)
                  ]
              )
              forall a b. (a -> b) -> a -> b
$ do
                Int
sz <- forall (m :: * -> *). Monad m => GenT m Int
sizeT
                a
x <- forall a (m :: * -> *).
(Complete a, HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecA @a Specification a
elemS
                let foldS' :: Specification a
foldS' = forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate forall a. (Complete a, Numeric a) => IntW '[a, a] a
theAddA (forall {k} (a :: k). HOLE a a
HOLE forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:? forall a. Show a => a -> Value a
Value a
x forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil) Specification a
foldS
                    specs' :: (Specification a, Specification a)
specs' = forall a.
(TypeSpec a ~ NumSpec a, Arbitrary a, Integral a, Random a,
 MaybeBounded a, Complete a) =>
a
-> Int
-> (Specification a, Specification a)
-> (Specification a, Specification a)
narrowByFuelAndSize (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Int
fuel forall a. Num a => a -> a -> a
- Int
1) Int
sz (Specification a
elemS, Specification a
foldS')
                forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
x, (Specification a, Specification a)
specs')
                forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
GenT m a -> (a -> Bool) -> GenT m a
`suchThatT` Bool -> Bool
not
                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a} {a}.
(TypeSpec a ~ NumSpec a, TypeSpec a ~ NumSpec a, HasSpec a, Ord a,
 Ord a, Enum a, Enum a, Num a, Num a, MaybeBounded a,
 MaybeBounded a) =>
(Specification a, Specification a) -> Bool
isUnsat
                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd
          forall (m' :: * -> *).
MonadGenError m' =>
(Specification a, Specification a) -> Int -> [a] -> GenT m' [a]
gen (Specification a, Specification a)
specs' (Int
fuel forall a. Num a => a -> a -> a
- Int
1) (a
x forall a. a -> [a] -> [a]
: [a]
lst)

narrowFoldSpecs ::
  forall a.
  ( TypeSpec a ~ NumSpec a
  , Arbitrary a
  , Integral a
  , Random a
  , MaybeBounded a
  , Complete a
  ) =>
  (Specification a, Specification a) ->
  (Specification a, Specification a)
narrowFoldSpecs :: forall a.
(TypeSpec a ~ NumSpec a, Arbitrary a, Integral a, Random a,
 MaybeBounded a, Complete a) =>
(Specification a, Specification a)
-> (Specification a, Specification a)
narrowFoldSpecs (Specification a, Specification a)
specs = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Specification a, Specification a)
specs forall a.
(TypeSpec a ~ NumSpec a, Arbitrary a, Integral a, Random a,
 MaybeBounded a, Complete a) =>
(Specification a, Specification a)
-> (Specification a, Specification a)
narrowFoldSpecs ((Specification a, Specification a)
-> Maybe (Specification a, Specification a)
go (Specification a, Specification a)
specs)
  where
    -- Note: make sure there is some progress when returning Just or this will loop forever
    go :: (Specification a, Specification a) -> Maybe (Specification a, Specification a)
    go :: (Specification a, Specification a)
-> Maybe (Specification a, Specification a)
go (forall a. Complete a => Specification a -> Specification a
simplifyA -> Specification a
elemS, forall a. Complete a => Specification a -> Specification a
simplifyA -> Specification a
foldS) = case (Specification a
elemS, Specification a
foldS) of
      -- Empty foldSpec
      (Specification a
_, ErrorSpec {}) -> forall a. Maybe a
Nothing
      (Specification a, Specification a)
_ | forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Bool
isEmptyNumSpec Specification a
foldS -> forall a. a -> Maybe a
Just (Specification a
elemS, forall a. NonEmpty String -> Specification a
ErrorSpec (forall a. [a] -> NonEmpty a
NE.fromList [String
"Empty foldSpec:", forall a. Show a => a -> String
show Specification a
foldS]))
      -- Empty elemSpec
      (ErrorSpec {}, MemberSpec NonEmpty a
ys) | forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
ys forall a. Eq a => a -> a -> Bool
== [a
0] -> forall a. Maybe a
Nothing
      (ErrorSpec {}, Specification a
_)
        | a
0 forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldS -> forall a. a -> Maybe a
Just (Specification a
elemS, forall a. NonEmpty a -> Specification a
MemberSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
0))
        | Bool
otherwise ->
            forall a. a -> Maybe a
Just
              ( Specification a
elemS
              , forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$
                  forall a. [a] -> NonEmpty a
NE.fromList
                    [ String
"Empty elemSpec and non-zero foldSpec"
                    , forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall ann. Int -> Doc ann -> Doc ann
indent Int
2 forall a b. (a -> b) -> a -> b
$ Doc Any
"elemSpec =" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall a ann. Pretty a => a -> Doc ann
pretty Specification a
elemS
                    , forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall ann. Int -> Doc ann -> Doc ann
indent Int
2 forall a b. (a -> b) -> a -> b
$ Doc Any
"foldSpec =" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall a ann. Pretty a => a -> Doc ann
pretty Specification a
foldS
                    ]
              )
      -- We can reduce the size of the `elemS` interval when it is
      -- `[l, u]` or `[l, ∞)` given that `0 <= l` and we have
      -- an upper bound on the sum - we can't pick things bigger than the
      -- upper bound.
      (Specification a, Specification a)
_
        | Just a
lo <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS
        , a
0 forall a. Ord a => a -> a -> Bool
<= a
lo
        , Just a
hi <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldS
        , -- Check that we will actually be making the set smaller
          forall a. a -> Maybe a -> a
fromMaybe Bool
True ((a
hi forall a. Ord a => a -> a -> Bool
<) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS) ->
            forall a. a -> Maybe a
Just (Specification a
elemS forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (forall a. a -> Maybe a
Just a
lo) (forall a. a -> Maybe a
Just a
hi)), Specification a
foldS)
      -- We can reduce the size of the foldS set by bumping the lower bound when
      -- there is a positive lower bound on the elemS, we can't generate things smaller
      -- than the lower bound on `elemS`.
      (Specification a, Specification a)
_
        | Just a
lo <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS
        , a
0 forall a. Ord a => a -> a -> Bool
<= a
lo
        , Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ a
0 forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldS
        , -- Check that we will actually be making the set smaller
          forall a. a -> Maybe a -> a
fromMaybe Bool
True ((a
lo forall a. Ord a => a -> a -> Bool
>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
foldS) ->
            forall a. a -> Maybe a
Just (Specification a
elemS, Specification a
foldS forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (forall a. a -> Maybe a
Just a
lo) forall a. Maybe a
Nothing))
      -- NOTE: this is far from sufficient, but it's good enough of an approximation
      -- to avoid the worst failures.
      (Specification a, Specification a)
_
        | Just a
lo <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS
        , Just a
loS <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
foldS
        , Just a
hi <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS
        , Just a
hiS <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldS
        , a
hi forall a. Ord a => a -> a -> Bool
< a
loS
        , a
lo forall a. Ord a => a -> a -> Bool
> a
hiS forall a. Num a => a -> a -> a
- a
lo ->
            forall a. a -> Maybe a
Just
              ( forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall a. [a] -> NonEmpty a
NE.fromList [String
"Can't solve diophantine equation"]
              , forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall a. [a] -> NonEmpty a
NE.fromList [String
"Can't solve diophantine equation"]
              )
      (Specification a, Specification a)
_ -> forall a. Maybe a
Nothing

narrowByFuelAndSize ::
  forall a.
  ( TypeSpec a ~ NumSpec a
  , Arbitrary a
  , Integral a
  , Random a
  , MaybeBounded a
  , Complete a
  ) =>
  -- | Fuel
  a ->
  -- | Integer
  Int ->
  (Specification a, Specification a) ->
  (Specification a, Specification a)
narrowByFuelAndSize :: forall a.
(TypeSpec a ~ NumSpec a, Arbitrary a, Integral a, Random a,
 MaybeBounded a, Complete a) =>
a
-> Int
-> (Specification a, Specification a)
-> (Specification a, Specification a)
narrowByFuelAndSize a
fuel Int
size (Specification a, Specification a)
specpair =
  Int
-> (Specification a, Specification a)
-> (Specification a, Specification a)
loop (Int
100 :: Int) ((Specification a, Specification a)
-> (Specification a, Specification a)
onlyOnceTransformations forall a b. (a -> b) -> a -> b
$ (forall a.
(TypeSpec a ~ NumSpec a, Arbitrary a, Integral a, Random a,
 MaybeBounded a, Complete a) =>
(Specification a, Specification a)
-> (Specification a, Specification a)
narrowFoldSpecs (Specification a, Specification a)
specpair))
  where
    loop :: Int
-> (Specification a, Specification a)
-> (Specification a, Specification a)
loop Int
0 (Specification a, Specification a)
specs =
      forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
        [String] -> String
unlines
          [ String
"narrowByFuelAndSize loops:"
          , String
"  fuel = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
fuel
          , String
"  size = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
size
          , String
"  specs = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Specification a, Specification a)
specs
          , String
"  narrowFoldSpecs spec = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a.
(TypeSpec a ~ NumSpec a, Arbitrary a, Integral a, Random a,
 MaybeBounded a, Complete a) =>
(Specification a, Specification a)
-> (Specification a, Specification a)
narrowFoldSpecs (Specification a, Specification a)
specs)
          , String
"  go (narrowFoldSpecs specs) = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ((Specification a, Specification a)
-> Maybe (Specification a, Specification a)
go (forall a.
(TypeSpec a ~ NumSpec a, Arbitrary a, Integral a, Random a,
 MaybeBounded a, Complete a) =>
(Specification a, Specification a)
-> (Specification a, Specification a)
narrowFoldSpecs (Specification a, Specification a)
specs))
          ]
    loop Int
n (Specification a, Specification a)
specs = case (Specification a, Specification a)
-> Maybe (Specification a, Specification a)
go (Specification a, Specification a)
specs of
      Maybe (Specification a, Specification a)
Nothing -> (Specification a, Specification a)
specs
      Just (Specification a, Specification a)
specs' -> Int
-> (Specification a, Specification a)
-> (Specification a, Specification a)
loop (Int
n forall a. Num a => a -> a -> a
- Int
1) (forall a.
(TypeSpec a ~ NumSpec a, Arbitrary a, Integral a, Random a,
 MaybeBounded a, Complete a) =>
(Specification a, Specification a)
-> (Specification a, Specification a)
narrowFoldSpecs (Specification a, Specification a)
specs')

    -- Transformations only applied once. It's annoying to check if you're
    -- going to change the spec with these so easier to just make sure you only apply
    -- these once
    onlyOnceTransformations :: (Specification a, Specification a)
-> (Specification a, Specification a)
onlyOnceTransformations (Specification a
elemS, Specification a
foldS)
      | a
fuel forall a. Eq a => a -> a -> Bool
== a
1 = (Specification a
elemS forall a. Semigroup a => a -> a -> a
<> Specification a
foldS, Specification a
foldS)
      | Bool
otherwise = (Specification a
elemS, Specification a
foldS)

    canReach :: t -> t -> t -> Bool
canReach t
_ t
0 t
s = t
s forall a. Eq a => a -> a -> Bool
== t
0
    canReach t
e t
currentfuel t
s
      -- You can reach it in one step
      | t
s forall a. Ord a => a -> a -> Bool
<= t
e = t
0 forall a. Ord a => a -> a -> Bool
< t
currentfuel
      | Bool
otherwise = t -> t -> t -> Bool
canReach t
e (t
currentfuel forall a. Num a => a -> a -> a
- t
1) (t
s forall a. Num a => a -> a -> a
- t
e)

    -- Precondition:
    --   a is negative
    --   the type has more negative numbers than positive ones
    safeNegate :: a -> a
safeNegate a
a
      | Just a
u <- forall a. MaybeBounded a => Maybe a
upperBound
      , a
a forall a. Ord a => a -> a -> Bool
< forall a. Num a => a -> a
negate a
u =
          a
u
      | Bool
otherwise = forall a. Num a => a -> a
negate a
a

    divCeil :: a -> a -> a
divCeil a
a a
b
      | a
b forall a. Num a => a -> a -> a
* a
d forall a. Ord a => a -> a -> Bool
< a
a = a
d forall a. Num a => a -> a -> a
+ a
1
      | Bool
otherwise = a
d
      where
        d :: a
d = a
a forall a. Integral a => a -> a -> a
`div` a
b

    go :: (Specification a, Specification a) -> Maybe (Specification a, Specification a)
    go :: (Specification a, Specification a)
-> Maybe (Specification a, Specification a)
go (forall a. Complete a => Specification a -> Specification a
simplifyA -> Specification a
elemS, forall a. Complete a => Specification a -> Specification a
simplifyA -> Specification a
foldS)
      -- There is nothing we can do
      | a
fuel forall a. Eq a => a -> a -> Bool
== a
0 = forall a. Maybe a
Nothing
      | ErrorSpec {} <- Specification a
elemS = forall a. Maybe a
Nothing
      | ErrorSpec {} <- Specification a
foldS = forall a. Maybe a
Nothing
      -- Give up as early as possible
      | Just a
0 <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS
      , Just a
0 <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS
      , Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ a
0 forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldS =
          forall a. a -> Maybe a
Just (forall a. NonEmpty String -> Specification a
ErrorSpec (forall a. [a] -> NonEmpty a
NE.fromList [String
"only 0 left"]), Specification a
foldS)
      -- Make sure we try to generate the smallest possible list
      -- that gives you the right result - don't put a bunch of zeroes in
      -- a _small_ (size 0) list.
      | Int
size forall a. Eq a => a -> a -> Bool
== Int
0
      , a
0 forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
elemS =
          forall a. a -> Maybe a
Just (Specification a
elemS forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => a -> Specification a
notEqualSpec a
0, Specification a
foldS)
      -- Member specs with non-zero elements, TODO: explain
      | MemberSpec NonEmpty a
ys <- Specification a
elemS
      , let xs :: [a]
xs = forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
ys
      , Just a
u <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldS
      , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a
0 forall a. Ord a => a -> a -> Bool
<=) [a]
xs
      , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (a
0 forall a. Ord a => a -> a -> Bool
<) [a]
xs
      , let xMinP :: a
xMinP = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (a
0 forall a. Ord a => a -> a -> Bool
<) [a]
xs
            possible :: a -> Bool
possible a
x = a
x forall a. Eq a => a -> a -> Bool
== a
u Bool -> Bool -> Bool
|| a
xMinP forall a. Ord a => a -> a -> Bool
<= a
u forall a. Num a => a -> a -> a
- a
x
            xs' :: [a]
xs' = forall a. (a -> Bool) -> [a] -> [a]
filter a -> Bool
possible [a]
xs
      , [a]
xs' forall a. Eq a => a -> a -> Bool
/= [a]
xs =
          forall a. a -> Maybe a
Just (forall a. [a] -> NonEmpty String -> Specification a
memberSpecList (forall a. Ord a => [a] -> [a]
nubOrd [a]
xs') (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"None of " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [a]
xs forall {a}. [a] -> [a] -> [a]
++ String
" are possible")), Specification a
foldS)
      -- The lower bound on the number of elements is too low
      | Just a
e <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS
      , a
e forall a. Ord a => a -> a -> Bool
> a
0
      , Just a
s <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
foldS
      , a
s forall a. Ord a => a -> a -> Bool
> a
0
      , let c :: a
c = forall a. Integral a => a -> a -> a
divCeil a
s a
fuel
      , a
e forall a. Ord a => a -> a -> Bool
< a
c =
          forall a. a -> Maybe a
Just (Specification a
elemS forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
geqSpec a
c, Specification a
foldS)
      -- The upper bound on the number of elements is too high
      | Just a
e <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS
      , a
e forall a. Ord a => a -> a -> Bool
< a
0
      , Just a
s <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldS
      , a
s forall a. Ord a => a -> a -> Bool
< a
0
      , let c :: a
c = forall a. Integral a => a -> a -> a
divCeil (forall {a}. (MaybeBounded a, Ord a, Num a) => a -> a
safeNegate a
s) a
fuel
      , forall a. Num a => a -> a
negate a
c forall a. Ord a => a -> a -> Bool
< a
e
      , forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (a
c forall a. Ord a => a -> a -> Bool
<) (forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS) =
          forall a. a -> Maybe a
Just (Specification a
elemS forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
leqSpec a
c, Specification a
foldS)
      -- It's time to stop generating negative numbers
      | Just a
s <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
foldS
      , a
s forall a. Ord a => a -> a -> Bool
> a
0
      , Just a
e <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS
      , a
e forall a. Ord a => a -> a -> Bool
> a
0
      , Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall {t} {t}. (Num t, Num t, Ord t, Ord t) => t -> t -> t -> Bool
canReach a
e (a
fuel forall a. Integral a => a -> a -> a
`div` a
2 forall a. Num a => a -> a -> a
+ a
1) a
s
      , forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (forall a. Ord a => a -> a -> Bool
<= a
0) (forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS) =
          forall a. a -> Maybe a
Just (Specification a
elemS forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
gtSpec a
0, Specification a
foldS)
      -- It's time to stop generating positive numbers
      | Just a
s <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldS
      , a
s forall a. Ord a => a -> a -> Bool
< a
0
      , Just a
e <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS
      , a
e forall a. Ord a => a -> a -> Bool
< a
0
      , Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall {t} {t}. (Num t, Num t, Ord t, Ord t) => t -> t -> t -> Bool
canReach (forall {a}. (MaybeBounded a, Ord a, Num a) => a -> a
safeNegate a
e) (a
fuel forall a. Integral a => a -> a -> a
`div` a
2 forall a. Num a => a -> a -> a
+ a
1) (forall {a}. (MaybeBounded a, Ord a, Num a) => a -> a
safeNegate a
s)
      , forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (a
0 forall a. Ord a => a -> a -> Bool
<=) (forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS) =
          forall a. a -> Maybe a
Just (Specification a
elemS forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
ltSpec a
0, Specification a
foldS)
      -- There is nothing we need to do
      | Bool
otherwise = forall a. Maybe a
Nothing

-- =====================================================================================
-- Like genList, but generate a list whose size conforms to s SizeSpec
-- =====================================================================================

-- | Generate a list with 'sizeSpec' elements, that add up to a total that conforms
--   to 'foldSpec'. Every element in the list should conform to 'elemSpec'
genListWithSize ::
  forall a m.
  ( Complete a
  , TypeSpec a ~ NumSpec a
  , MonadGenError m
  , Random a
  , Integral a
  , Arbitrary a
  , MaybeBounded a
  , Complete Integer
  , TypeSpec Integer ~ NumSpec Integer
  ) =>
  Specification Integer ->
  Specification a ->
  Specification a ->
  GenT m [a]
genListWithSize :: forall a (m :: * -> *).
(Complete a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
 Integral a, Arbitrary a, MaybeBounded a, Complete Integer,
 TypeSpec Integer ~ NumSpec Integer) =>
Specification Integer
-> Specification a -> Specification a -> GenT m [a]
genListWithSize Specification Integer
sizeSpec Specification a
elemSpec Specification a
foldSpec
  | Specification Integer
TrueSpec <- Specification Integer
sizeSpec = forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
 TypeSpec a ~ NumSpec a, Random a, Complete a) =>
Specification a -> Specification a -> GenT m [a]
genNumList Specification a
elemSpec Specification a
foldSpec
  | ErrorSpec NonEmpty String
_ <- Specification Integer
sizeSpec forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
geqSpec Integer
0 =
      forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE
        ( forall a. [a] -> NonEmpty a
NE.fromList
            [ String
"genListWithSize called with possible negative size"
            , String
"  sizeSpec = " forall {a}. [a] -> [a] -> [a]
++ forall a. HasSpec a => Specification a -> String
specName Specification Integer
sizeSpec
            , String
"  elemSpec = " forall {a}. [a] -> [a] -> [a]
++ forall a. HasSpec a => Specification a -> String
specName Specification a
elemSpec
            , String
"  foldSpec = " forall {a}. [a] -> [a] -> [a]
++ forall a. HasSpec a => Specification a -> String
specName Specification a
foldSpec
            ]
        )
  | Bool
otherwise = do
      a
total <- forall a (m :: * -> *).
(Complete a, HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecA @a Specification a
foldSpec
      -- The compatible sizes for the list, for a given choice of total
      let sizeAdjusted :: Specification Integer
sizeAdjusted =
            if a
total forall a. Eq a => a -> a -> Bool
/= a
0
              then Specification Integer
sizeSpec forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
gtSpec Integer
0 -- if total is not zero, we better not pick a 0 size
              else
                if forall a. MaybeBounded a => Maybe a
lowerBound @a forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just a
0 -- Type `a` has no negative numbers (Natural, Word8, Word16, Word 32, Word64)
                  then Specification Integer
sizeSpec forall a. Semigroup a => a -> a -> a
<> forall a. a -> Specification a
equalSpec Integer
0 -- if it is zero, and negative numbers not allowed, then only possible size is 0
                  else Specification Integer
sizeSpec forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
gtSpec Integer
0
          message :: [String]
message =
            [ String
"\nGenSizedList fails"
            , String
"sizespec = " forall {a}. [a] -> [a] -> [a]
++ forall a. HasSpec a => Specification a -> String
specName Specification Integer
sizeSpec
            , String
"elemSpec = " forall {a}. [a] -> [a] -> [a]
++ forall a. HasSpec a => Specification a -> String
specName Specification a
elemSpec
            , String
"foldSpec = " forall {a}. [a] -> [a] -> [a]
++ forall a. HasSpec a => Specification a -> String
specName Specification a
foldSpec
            , String
"total choosen from foldSpec = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
total
            , String
"size adjusted for total = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification Integer
sizeAdjusted
            ]
      forall (m :: * -> *) a. MonadGenError m => [String] -> m a -> m a
push [String]
message forall a b. (a -> b) -> a -> b
$ do
        Integer
count <- forall a (m :: * -> *).
(Complete a, HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecA @Integer Specification Integer
sizeAdjusted
        case forall a. Ord a => a -> a -> Ordering
compare a
total a
0 of
          Ordering
EQ ->
            if Integer
count forall a. Eq a => a -> a -> Bool
== Integer
0
              then forall (f :: * -> *) a. Applicative f => a -> f a
pure []
              else forall t (m :: * -> *).
(Integral t, Random t, MonadGenError m, TypeSpec t ~ NumSpec t,
 Complete t) =>
Specification t -> t -> Integer -> GenT m [t]
pickPositive Specification a
elemSpec a
total Integer
count
          Ordering
GT -> forall t (m :: * -> *).
(Integral t, Random t, MonadGenError m, TypeSpec t ~ NumSpec t,
 Complete t) =>
Specification t -> t -> Integer -> GenT m [t]
pickPositive Specification a
elemSpec a
total Integer
count
          Ordering
LT -> forall t (m :: * -> *).
(Integral t, Complete t, Random t, MonadGenError m,
 TypeSpec t ~ NumSpec t) =>
Specification t -> t -> Integer -> GenT m [t]
pickNegative Specification a
elemSpec a
total Integer
count

pickPositive ::
  forall t m.
  (Integral t, Random t, MonadGenError m, TypeSpec t ~ NumSpec t, Complete t) =>
  Specification t ->
  t ->
  Integer ->
  GenT m [t]
pickPositive :: forall t (m :: * -> *).
(Integral t, Random t, MonadGenError m, TypeSpec t ~ NumSpec t,
 Complete t) =>
Specification t -> t -> Integer -> GenT m [t]
pickPositive Specification t
elemspec t
total Integer
count = do
  (Cost, Solution t)
sol <-
    forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen forall a b. (a -> b) -> a -> b
$
      forall t.
(Show t, Integral t, Random t) =>
t
-> t
-> (String, t -> Bool)
-> t
-> Int
-> Cost
-> Gen (Cost, Solution t)
pickAll
        (forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
minFromSpec t
0 Specification t
elemspec) -- Search from [0..total] unless elemspec says otherwise
        (forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
maxFromSpec t
total Specification t
elemspec)
        (forall a. HasSpec a => Specification a -> (String, a -> Bool)
predSpecPair Specification t
elemspec)
        t
total
        (forall a. Num a => Integer -> a
fromInteger Integer
count)
        (Int -> Cost
Cost Int
0)
  case forall a b. (a, b) -> b
snd (Cost, Solution t)
sol of
    No [String]
msgs -> forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE (forall a. [a] -> NonEmpty a
NE.fromList [String]
msgs)
    Yes ([t]
x :| [[t]]
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [t]
x

pickNegative ::
  forall t m.
  (Integral t, Complete t, Random t, MonadGenError m, TypeSpec t ~ NumSpec t) =>
  Specification t ->
  t ->
  Integer ->
  GenT m [t]

-- | total can be either negative, or 0. If it is 0, we want `count` numbers that add to `zero`
pickNegative :: forall t (m :: * -> *).
(Integral t, Complete t, Random t, MonadGenError m,
 TypeSpec t ~ NumSpec t) =>
Specification t -> t -> Integer -> GenT m [t]
pickNegative Specification t
elemspec t
total Integer
count = do
  (Cost, Solution t)
sol <-
    forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen forall a b. (a -> b) -> a -> b
$
      forall t.
(Show t, Integral t, Random t) =>
t
-> t
-> (String, t -> Bool)
-> t
-> Int
-> Cost
-> Gen (Cost, Solution t)
pickAll
        -- Recall 'total' is negative here.
        -- Here is a graphic of the range we search in (smallest .. largest)
        -- [(total+n) .. total .. 0 .. (0-n)],  where n = (total `div` 4) which is negative.
        (forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
minFromSpec (t
total forall a. Num a => a -> a -> a
+ (t
total forall a. Integral a => a -> a -> a
`div` t
4)) Specification t
elemspec)
        (forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
maxFromSpec (t
0 forall a. Num a => a -> a -> a
- (t
total forall a. Integral a => a -> a -> a
`div` t
4)) Specification t
elemspec)
        (forall a. HasSpec a => Specification a -> (String, a -> Bool)
predSpecPair Specification t
elemspec)
        t
total
        (forall a. Num a => Integer -> a
fromInteger Integer
count)
        (Int -> Cost
Cost Int
0)
  case forall a b. (a, b) -> b
snd (Cost, Solution t)
sol of
    No [String]
msgs -> forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE (forall a. [a] -> NonEmpty a
NE.fromList [String]
msgs)
    Yes ([t]
x :| [[t]]
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [t]
x

specName :: forall a. HasSpec a => Specification a -> String
specName :: forall a. HasSpec a => Specification a -> String
specName (ExplainSpec [String
x] Specification a
_) = String
x
specName Specification a
x = forall a. Show a => a -> String
show Specification a
x

predSpecPair :: forall a. HasSpec a => Specification a -> (String, a -> Bool)
predSpecPair :: forall a. HasSpec a => Specification a -> (String, a -> Bool)
predSpecPair Specification a
spec = (forall a. HasSpec a => Specification a -> String
specName Specification a
spec, (forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
spec))

-- | The smallest number admitted by the spec, if we can find one.
--   if not return the defaultValue 'dv'
minFromSpec ::
  forall n.
  (Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
  n ->
  Specification n ->
  n
minFromSpec :: forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
minFromSpec n
dv (ExplainSpec [String]
_ Specification n
spec) = forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
minFromSpec @n n
dv Specification n
spec
minFromSpec n
dv Specification n
TrueSpec = n
dv
minFromSpec n
dv s :: Specification n
s@(SuspendedSpec Var n
_ Pred
_) =
  case forall a. Complete a => Specification a -> Specification a
simplifyA Specification n
s of
    SuspendedSpec {} -> n
dv
    Specification n
x -> forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
minFromSpec @n n
dv Specification n
x
minFromSpec n
dv (ErrorSpec NonEmpty String
_) = n
dv
minFromSpec n
_ (MemberSpec NonEmpty n
xs) = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum NonEmpty n
xs
minFromSpec n
dv (TypeSpec (NumSpecInterval Maybe n
lo Maybe n
_) [n]
_) = forall b a. b -> (a -> b) -> Maybe a -> b
maybe n
dv forall a. a -> a
id Maybe n
lo

-- | The largest number admitted by the spec, if we can find one.
--   if not return the defaultValue 'dv'
maxFromSpec ::
  forall n.
  (Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
  n ->
  Specification n ->
  n
maxFromSpec :: forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
maxFromSpec n
dv (ExplainSpec [String]
_ Specification n
spec) = forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
maxFromSpec @n n
dv Specification n
spec
maxFromSpec n
dv Specification n
TrueSpec = n
dv
maxFromSpec n
dv s :: Specification n
s@(SuspendedSpec Var n
_ Pred
_) =
  case forall a. Complete a => Specification a -> Specification a
simplifyA Specification n
s of
    SuspendedSpec {} -> n
dv
    Specification n
x -> forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
maxFromSpec @n n
dv Specification n
x
maxFromSpec n
dv (ErrorSpec NonEmpty String
_) = n
dv
maxFromSpec n
_ (MemberSpec NonEmpty n
xs) = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum NonEmpty n
xs
maxFromSpec n
dv (TypeSpec (NumSpecInterval Maybe n
_ Maybe n
hi) [n]
_) = forall b a. b -> (a -> b) -> Maybe a -> b
maybe n
dv forall a. a -> a
id Maybe n
hi

-- =======================================================
-- Helper functions for genSizedList

data Solution t = Yes (NonEmpty [t]) | No [String]
  deriving (Solution t -> Solution t -> Bool
forall t. Eq t => Solution t -> Solution t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Solution t -> Solution t -> Bool
$c/= :: forall t. Eq t => Solution t -> Solution t -> Bool
== :: Solution t -> Solution t -> Bool
$c== :: forall t. Eq t => Solution t -> Solution t -> Bool
Eq)

instance Show t => Show (Solution t) where
  show :: Solution t -> String
show (No [String]
xs) = String
"No" forall {a}. [a] -> [a] -> [a]
++ String
"\n" forall {a}. [a] -> [a] -> [a]
++ [String] -> String
unlines [String]
xs
  show (Yes NonEmpty [t]
xs) = String
"Yes " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show NonEmpty [t]
xs

-- | The basic idea is to concat all the Yes's and skip over the No's.
--   The one wrinkle is if everything is No, then in that case return an arbitrary one of the No's.
--   This can be done in linear time in the length of the list. Call that length n.
--   Check for all No. This takes time proportional to n. If it is true return one of them.
--   If it is not all No, then concat all the Yes, and skip all the No.
--   We find the first No (if it exist), and all the Yes by partitioning the list
--   This is similar in spirit to Constrained.GenT.catGEs, but doesn't require a
--   a Monad to escape on the first No.
concatSolution :: Show t => t -> t -> String -> t -> Int -> [Solution t] -> Solution t
concatSolution :: forall t.
Show t =>
t -> t -> String -> t -> Int -> [Solution t] -> Solution t
concatSolution t
smallest t
largest String
pName t
total Int
count [Solution t]
sols =
  case forall a b. [Either a b] -> ([a], [b])
partitionEithers (forall a b. (a -> b) -> [a] -> [b]
map (\case Yes NonEmpty [t]
x -> forall a b. a -> Either a b
Left NonEmpty [t]
x; No [String]
x -> forall a b. b -> Either a b
Right [String]
x) [Solution t]
sols) of
    ([], [String]
n : [[String]]
_) -> forall t. [String] -> Solution t
No [String]
n -- All No, arbitrarily return the first.
    (NonEmpty [t]
y : [NonEmpty [t]]
ys, [[String]]
_) -> forall t. NonEmpty [t] -> Solution t
Yes forall a b. (a -> b) -> a -> b
$ forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty [t]
y forall a. a -> [a] -> NonEmpty a
:| [NonEmpty [t]]
ys) -- At least one Yes, and all No's skipped ('ys')
    ([], []) ->
      forall t. [String] -> Solution t
No -- The list is empty
        [ String
"\nThe sample in pickAll was empty"
        , String
"  smallest = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
smallest
        , String
"  largest = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
largest
        , String
"  pred = " forall {a}. [a] -> [a] -> [a]
++ String
pName
        , String
"  total = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
total
        , String
"  count = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
count
        ]

newtype Cost = Cost Int deriving (Cost -> Cost -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Cost -> Cost -> Bool
$c/= :: Cost -> Cost -> Bool
== :: Cost -> Cost -> Bool
$c== :: Cost -> Cost -> Bool
Eq, Int -> Cost -> ShowS
[Cost] -> ShowS
Cost -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Cost] -> ShowS
$cshowList :: [Cost] -> ShowS
show :: Cost -> String
$cshow :: Cost -> String
showsPrec :: Int -> Cost -> ShowS
$cshowsPrec :: Int -> Cost -> ShowS
Show, Integer -> Cost
Cost -> Cost
Cost -> Cost -> Cost
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> Cost
$cfromInteger :: Integer -> Cost
signum :: Cost -> Cost
$csignum :: Cost -> Cost
abs :: Cost -> Cost
$cabs :: Cost -> Cost
negate :: Cost -> Cost
$cnegate :: Cost -> Cost
* :: Cost -> Cost -> Cost
$c* :: Cost -> Cost -> Cost
- :: Cost -> Cost -> Cost
$c- :: Cost -> Cost -> Cost
+ :: Cost -> Cost -> Cost
$c+ :: Cost -> Cost -> Cost
Num, Eq Cost
Cost -> Cost -> Bool
Cost -> Cost -> Ordering
Cost -> Cost -> Cost
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Cost -> Cost -> Cost
$cmin :: Cost -> Cost -> Cost
max :: Cost -> Cost -> Cost
$cmax :: Cost -> Cost -> Cost
>= :: Cost -> Cost -> Bool
$c>= :: Cost -> Cost -> Bool
> :: Cost -> Cost -> Bool
$c> :: Cost -> Cost -> Bool
<= :: Cost -> Cost -> Bool
$c<= :: Cost -> Cost -> Bool
< :: Cost -> Cost -> Bool
$c< :: Cost -> Cost -> Bool
compare :: Cost -> Cost -> Ordering
$ccompare :: Cost -> Cost -> Ordering
Ord)

firstYesG ::
  Monad m => Solution t -> (x -> Cost -> m (Cost, Solution t)) -> [x] -> Cost -> m (Cost, Solution t)
firstYesG :: forall (m :: * -> *) t x.
Monad m =>
Solution t
-> (x -> Cost -> m (Cost, Solution t))
-> [x]
-> Cost
-> m (Cost, Solution t)
firstYesG Solution t
nullSolution x -> Cost -> m (Cost, Solution t)
f [x]
xs Cost
c = [x] -> Cost -> m (Cost, Solution t)
go [x]
xs Cost
c
  where
    go :: [x] -> Cost -> m (Cost, Solution t)
go [] Cost
cost = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cost
cost, Solution t
nullSolution)
    go [x
x] Cost
cost = x -> Cost -> m (Cost, Solution t)
f x
x (Cost
cost forall a. Num a => a -> a -> a
+ Cost
1)
    go (x
x : [x]
more) Cost
cost = do
      (Cost, Solution t)
ans <- x -> Cost -> m (Cost, Solution t)
f x
x (Cost
cost forall a. Num a => a -> a -> a
+ Cost
1)
      case (Cost, Solution t)
ans of
        (Cost
cost1, No [String]
_) -> [x] -> Cost -> m (Cost, Solution t)
go [x]
more Cost
cost1
        (Cost
_, Yes NonEmpty [t]
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cost, Solution t)
ans

noChoices :: Show t => Cost -> String -> t -> t -> t -> Int -> [(t, t)] -> Solution t
noChoices :: forall t.
Show t =>
Cost -> String -> t -> t -> t -> Int -> [(t, t)] -> Solution t
noChoices Cost
cost String
p t
smallest t
largest t
total Int
count [(t, t)]
samp =
  forall t. [String] -> Solution t
No
    [ String
"\nNo legal choice can be found, where for each sample (x,y)"
    , String
"x+y = total && predicate x && predicate y"
    , String
"  predicate = " forall {a}. [a] -> [a] -> [a]
++ String
p
    , String
"  smallest = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
smallest
    , String
"  largest = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
largest
    , String
"  total = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
total
    , String
"  count = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
count
    , String
"  cost = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Cost
cost
    , String
"Small sample of what was explored"
    , forall a. Show a => a -> String
show [(t, t)]
samp
    ]

-- =====================================================

-- | Given 'count', return a list of pairs, that add to 'count'
--   splitsOf 6 --> [(1,5),(2,4),(3,3)].
--   Note we don't return reflections like (5,1) and (4,2),
--   as they have the same information as (1,5) and (2,4).
splitsOf :: Integral b => b -> [(b, b)]
splitsOf :: forall b. Integral b => b -> [(b, b)]
splitsOf b
count = [(b
i, b
j) | b
i <- [b
1 .. forall a. Integral a => a -> a -> a
div b
count b
2], let j :: b
j = b
count forall a. Num a => a -> a -> a
- b
i]
{-# SPECIALIZE splitsOf :: Int -> [(Int, Int)] #-}

-- | Given a Path, find a representative solution, 'ans', for that path, such that
--   1) (length ans) == 'count',
--   2) (sum ans) == 'total'
--   3) (all p ans) is True
--   What is a path?
--   Suppose i==5, then we recursively explore every way to split 5 into
--   split pairs that add to 5. I.e. (1,4) (2,3), then we split each of those.
--   Here is a picture of the graph of all paths for i==5. A path goes from the root '5'
--   to one of the leaves. Note all leaves are count == '1 (where the solution is '[total]').
--   To solve for 5, we could solve either of the sub problems rooted at 5: [1,4] or [2,3].
--   5
--   |
--   [1,4]
--   |  |
--   |  [1,3]
--   |  |  |
--   |  |  [1,2]
--   |  |     |
--   |  |     [1,1]
--   |  |
--   |  [2,2]
--   |   | |
--   |   | [1,1]
--   |   |
--   |   [1,1]
--   |
--   [2,3]
--    | |
--    | [1,2]
--    |    |
--    |    [1,1]
--    [1,1]
--  In 'pickAll' will explore a path for every split of 'count'
--  so if it returns (No _), we can be somewhat confidant that no solution exists.
--  Note that count of 1 and 2, are base cases.
--  When 'count' is greater than 1, we need to sample from [smallest..total],
--  so 'smallest' better be less that or equal to 'total'
pickAll ::
  forall t.
  (Show t, Integral t, Random t) =>
  t ->
  t ->
  (String, t -> Bool) ->
  t ->
  Int ->
  Cost ->
  Gen (Cost, Solution t)
pickAll :: forall t.
(Show t, Integral t, Random t) =>
t
-> t
-> (String, t -> Bool)
-> t
-> Int
-> Cost
-> Gen (Cost, Solution t)
pickAll t
smallest t
largest (String
pName, t -> Bool
_) t
total Int
count Cost
cost
  | Cost
cost forall a. Ord a => a -> a -> Bool
> Cost
1000 =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        ( Cost
cost
        , forall t. [String] -> Solution t
No
            [ String
"\nPickAll exceeds cost limit " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Cost
cost
            , String
"  predicate = " forall {a}. [a] -> [a] -> [a]
++ String
pName
            , String
"  smallest = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
smallest
            , String
"  largest = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
largest
            , String
"  total = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
total
            , String
"  count = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
count
            ]
        )
pickAll t
smallest t
largest (String
pName, t -> Bool
p) t
total Int
0 Cost
cost =
  if t
total forall a. Eq a => a -> a -> Bool
== t
0 Bool -> Bool -> Bool
&& t -> Bool
p t
total
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cost
cost, forall t. NonEmpty [t] -> Solution t
Yes forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure [])
    else
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( Cost
cost
        , forall t. [String] -> Solution t
No
            [ String
"We are trying to find list of length 0."
            , String
"  Whose sum is " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
total forall {a}. [a] -> [a] -> [a]
++ String
"."
            , String
"  That is only possible if the sum == 0."
            , String
"  All elements have to satisfy " forall {a}. [a] -> [a] -> [a]
++ String
pName
            , String
"  smallest = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
smallest
            , String
"  largest = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
largest
            ]
        )
pickAll t
smallest t
largest (String
pName, t -> Bool
p) t
total Int
1 Cost
cost =
  if t -> Bool
p t
total
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cost
cost, forall t. NonEmpty [t] -> Solution t
Yes forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure [t
total])
    else forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cost
cost, forall t.
Show t =>
Cost -> String -> t -> t -> t -> Int -> [(t, t)] -> Solution t
noChoices Cost
cost String
pName t
smallest t
largest t
total Int
1 [(t
total, t
0)])
pickAll t
smallest t
largest (String
pName, t -> Bool
_) t
total Int
count Cost
cost
  | t
smallest forall a. Ord a => a -> a -> Bool
> t
largest =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        ( Cost
cost
        , forall t. [String] -> Solution t
No
            [ String
"\nThe feasible range to pickAll ["
                forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
smallest
                forall {a}. [a] -> [a] -> [a]
++ String
" .. "
                forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Integral a => a -> a -> a
div t
total t
2)
                forall {a}. [a] -> [a] -> [a]
++ String
"] was empty"
            , String
"  predicate = " forall {a}. [a] -> [a] -> [a]
++ String
pName
            , String
"  smallest = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
smallest
            , String
"  largest = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
largest
            , String
"  total = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
total
            , String
"  count = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
count
            , String
"  cost = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Cost
cost
            ]
        )
pickAll t
smallest t
largest (String
pName, t -> Bool
p) t
total Int
2 Cost
cost = do
  -- for large things, use a fair sample.
  [(t, t)]
choices <- forall t.
(Random t, Integral t) =>
t -> t -> t -> t -> Int -> Gen [(t, t)]
smallSample t
smallest t
largest t
total t
1000 Int
100
  case forall a. (a -> Bool) -> [a] -> [a]
filter (\(t
x, t
y) -> t -> Bool
p t
x Bool -> Bool -> Bool
&& t -> Bool
p t
y) [(t, t)]
choices of
    [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (Cost
cost forall a. Num a => a -> a -> a
+ Cost
1, forall t.
Show t =>
Cost -> String -> t -> t -> t -> Int -> [(t, t)] -> Solution t
noChoices Cost
cost String
pName t
smallest t
largest t
total Int
2 (forall a. Int -> [a] -> [a]
take Int
10 [(t, t)]
choices))
    [(t, t)]
zs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (Cost
cost forall a. Num a => a -> a -> a
+ Cost
1, forall t. NonEmpty [t] -> Solution t
Yes forall a b. (a -> b) -> a -> b
$ forall a. [a] -> NonEmpty a
NE.fromList (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(t
x, t
y) -> [t
x, t
y]) [(t, t)]
zs))
pickAll t
smallest t
largest (String
pName, t -> Bool
p) t
total Int
count Cost
cost = do
  -- Compute a representative sample of the choices between smallest and total.
  -- E.g. when smallest = -2, and total = 5, the complete set of values is:
  -- [(-2,7),(-1,6),(0,5),(1,4),(2,3),(3,2),(4,1),(5,0)]  Note they all add to 5
  -- We could explore the whole set of values, but that can be millions of choices.
  -- so we choose to explore a representative subset. See the function 'fairSample', for details.
  -- Remember this is just 1 step on one path. So if this step fails, there are many more
  -- paths to explore. In fact there are usually many many solutions. We need to find just 1.
  [(t, t)]
choices <- forall t.
(Random t, Integral t) =>
t -> t -> t -> t -> Int -> Gen [(t, t)]
smallSample t
smallest t
largest t
total t
1000 Int
20
  -- The choice of splits is crucial. If total >> count, we want the larger splits first
  -- if count >> total , we want smaller splits first
  [(Int, Int)]
splits <-
    if Int
count forall a. Ord a => a -> a -> Bool
>= Int
20
      then forall a. [a] -> Gen [a]
shuffle forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
10 (forall b. Integral b => b -> [(b, b)]
splitsOf Int
count)
      else
        if t
total forall a. Ord a => a -> a -> Bool
> forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
count
          then forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. [a] -> [a]
reverse (forall b. Integral b => b -> [(b, b)]
splitsOf Int
count))
          else forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall b. Integral b => b -> [(b, b)]
splitsOf Int
count)

  forall (m :: * -> *) t x.
Monad m =>
Solution t
-> (x -> Cost -> m (Cost, Solution t))
-> [x]
-> Cost
-> m (Cost, Solution t)
firstYesG
    (forall t. [String] -> Solution t
No [String
"\nNo split has a solution", String
"cost = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Cost
cost])
    (forall t.
(Random t, Show t, Integral t) =>
t
-> t
-> (String, t -> Bool)
-> t
-> [(t, t)]
-> (Int, Int)
-> Cost
-> Gen (Cost, Solution t)
doSplit t
smallest t
largest (String
pName, t -> Bool
p) t
total [(t, t)]
choices)
    [(Int, Int)]
splits
    Cost
cost

-- TODO run some tests to see if this is a better solution than firstYesG
-- concatSolution smallest pName total count
--  <$> mapM  (doSplit smallest largest total (pName, p) choices (pickAll (depth +1) smallest)) splits

-- {-# SPECIALIZE pickAll::Int -> (String, Int -> Bool) -> Int -> Int -> Cost -> Gen (Cost, Solution Int) #-}

doSplit ::
  (Random t, Show t, Integral t) =>
  t ->
  t ->
  (String, t -> Bool) ->
  t ->
  [(t, t)] ->
  -- (t -> (String, t -> Bool) -> t -> Int -> Cost -> Gen (Cost, Solution t)) ->
  (Int, Int) ->
  Cost ->
  Gen (Cost, Solution t)
doSplit :: forall t.
(Random t, Show t, Integral t) =>
t
-> t
-> (String, t -> Bool)
-> t
-> [(t, t)]
-> (Int, Int)
-> Cost
-> Gen (Cost, Solution t)
doSplit t
smallest t
largest (String
pName, t -> Bool
p) t
total [(t, t)]
sample (Int
i, Int
j) Cost
c = [(t, t)] -> Cost -> Gen (Cost, Solution t)
go [(t, t)]
sample Cost
c
  where
    -- The 'sample' is a list of pairs (x,y), where we know (x+y) == total.
    -- We will search for the first good solution in the given sample
    -- to build a representative value for this path, with split (i,j).
    go :: [(t, t)] -> Cost -> Gen (Cost, Solution t)
go ((t
x, t
y) : [(t, t)]
more) Cost
cost0 = do
      -- Note (i+j) = current length of the ans we are looking for
      --      (x+y) = total
      -- pick 'ans1' such that (sum ans1 == x) and (length ans1 == i)
      (Cost
cost1, Solution t
ans1) <- forall t.
(Show t, Integral t, Random t) =>
t
-> t
-> (String, t -> Bool)
-> t
-> Int
-> Cost
-> Gen (Cost, Solution t)
pickAll t
smallest t
largest (String
pName, t -> Bool
p) t
x Int
i Cost
cost0
      -- pick 'ans2' such that (sum ans2 == y) and (length ans2 == j)
      (Cost
cost2, Solution t
ans2) <- forall t.
(Show t, Integral t, Random t) =>
t
-> t
-> (String, t -> Bool)
-> t
-> Int
-> Cost
-> Gen (Cost, Solution t)
pickAll t
smallest t
largest (String
pName, t -> Bool
p) t
y Int
j Cost
cost1
      case (Solution t
ans1, Solution t
ans2) of
        (Yes NonEmpty [t]
ys, Yes NonEmpty [t]
zs) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (Cost
cost2, forall t. NonEmpty [t] -> Solution t
Yes (forall a. [a] -> NonEmpty a
NE.fromList [[t]
a forall a. Semigroup a => a -> a -> a
<> [t]
b | [t]
a <- forall a. NonEmpty a -> [a]
NE.toList NonEmpty [t]
ys, [t]
b <- forall a. NonEmpty a -> [a]
NE.toList NonEmpty [t]
zs]))
        (Solution t, Solution t)
_ -> [(t, t)] -> Cost -> Gen (Cost, Solution t)
go [(t, t)]
more Cost
cost2
    go [] Cost
cost =
      case [(t, t)]
sample of
        [] ->
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
            ( Cost
cost
            , forall t. [String] -> Solution t
No
                [ String
"\nThe sample passed to doSplit [" forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
smallest forall {a}. [a] -> [a] -> [a]
++ String
" .. " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Integral a => a -> a -> a
div t
total t
2) forall {a}. [a] -> [a] -> [a]
++ String
"] was empty"
                , String
"  predicate = " forall {a}. [a] -> [a] -> [a]
++ String
pName
                , String
"  smallest = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
smallest
                , String
"  largest = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
largest
                , String
"  total " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
total
                , String
"  count = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Int
i forall a. Num a => a -> a -> a
+ Int
j)
                , String
"  split of count = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Int
i, Int
j)
                ]
            )
        ((t
left, t
right) : [(t, t)]
_) ->
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
            ( Cost
cost
            , forall t. [String] -> Solution t
No
                [ String
"\nAll choices in (genSizedList " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Int
i forall a. Num a => a -> a -> a
+ Int
j) forall {a}. [a] -> [a] -> [a]
++ String
" 'p' " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
total forall {a}. [a] -> [a] -> [a]
++ String
") have failed."
                , String
"Here is 1 example failure."
                , String
"  smallest = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
smallest
                , String
"  largest = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
largest
                , String
"  total " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
total forall {a}. [a] -> [a] -> [a]
++ String
" = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
left forall {a}. [a] -> [a] -> [a]
++ String
" + " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
right
                , String
"  count = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Int
i forall a. Num a => a -> a -> a
+ Int
j) forall {a}. [a] -> [a] -> [a]
++ String
", split of count = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Int
i, Int
j)
                , String
"We are trying to solve sub-problems like:"
                , String
"  split " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
left forall {a}. [a] -> [a] -> [a]
++ String
" into " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall {a}. [a] -> [a] -> [a]
++ String
" parts, where all parts meet 'p'"
                , String
"  split " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
right forall {a}. [a] -> [a] -> [a]
++ String
" into " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
j forall {a}. [a] -> [a] -> [a]
++ String
" parts, where all parts meet 'p'"
                , String
"Predicate 'p' = " forall {a}. [a] -> [a] -> [a]
++ String
pName
                , String
"A small prefix of the sample, elements (x,y) where x+y = " forall {a}. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
total
                , [String] -> String
unlines (forall a b. (a -> b) -> [a] -> [b]
map ((String
"  " forall {a}. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) (forall a. Int -> [a] -> [a]
take Int
10 [(t, t)]
sample))
                ]
            )
{-# INLINE doSplit #-}

-- | If the sample is small enough, then enumerate all of it, otherwise take a fair sample.
smallSample :: (Random t, Integral t) => t -> t -> t -> t -> Int -> Gen [(t, t)]
smallSample :: forall t.
(Random t, Integral t) =>
t -> t -> t -> t -> Int -> Gen [(t, t)]
smallSample t
smallest t
largest t
total t
bound Int
size
  | t
largest forall a. Num a => a -> a -> a
- t
smallest forall a. Ord a => a -> a -> Bool
<= t
bound = do
      forall a. [a] -> Gen [a]
shuffle forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Ord a => a -> a -> Bool
(<=)) [(t
x, t
total forall a. Num a => a -> a -> a
- t
x) | t
x <- [t
smallest .. t
total]]
  | Bool
otherwise = do
      [t]
choices <- forall a.
(Random a, Integral a) =>
a -> a -> Int -> Int -> Bool -> Gen [a]
fair t
smallest t
largest Int
size Int
5 Bool
True
      forall a. [a] -> Gen [a]
shuffle [(t
x, t
total forall a. Num a => a -> a -> a
- t
x) | t
x <- [t]
choices]
{-# INLINE smallSample #-}

-- | Generates a fair sample of numbers between 'smallest' and 'largest'.
--   makes sure there are numbers of all sizes. Controls both the size of the sample
--   and the precision (how many powers of 10 are covered)
--   Here is how we generate one sample when we call (fair (-3455) (10234) 12 3 True)
--   raw = [(-9999,-1000),(-999,-100),(-99,-10),(-9,-1),(0,9),(10,99),(100,999),(1000,9999),(10000,99999)]
--   ranges = [(-3455,-1000),(-999,-100),(-99,-10),(-9,-1),(0,9),(10,99),(100,999),(1000,9999),(10000,10234)]
--   count = 4
--   largePrecision = [(10000,10234),(1000,9999),(100,999)]
--   smallPrecision = [(-3455,-1000),(-999,-100),(-99,-10)]
--   answer generated = [10128,10104,10027,10048,4911,7821,5585,2157,448,630,802,889]
--   isLarge==True   means be biased towards the large end of the range,
--   isLArge==False  means be biased towards the small end of the range,
fair :: (Random a, Integral a) => a -> a -> Int -> Int -> Bool -> Gen [a]
fair :: forall a.
(Random a, Integral a) =>
a -> a -> Int -> Int -> Bool -> Gen [a]
fair a
smallest a
largest Int
size Int
precision Bool
isLarge =
  forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (a, a) -> Gen [a]
oneRange (if Bool
isLarge then [(a, a)]
largePrecision else [(a, a)]
smallPrecision)
  where
    raw :: [(a, a)]
raw = forall a b. (a -> b) -> [a] -> [b]
map forall a. Integral a => a -> (a, a)
logRange [forall t. Integral t => t -> t
logish a
smallest .. forall t. Integral t => t -> t
logish a
largest]
    fixEnds :: (a, a) -> (a, a)
fixEnds (a
x, a
y) = (forall a. Ord a => a -> a -> a
max a
smallest a
x, forall a. Ord a => a -> a -> a
min a
largest a
y)
    ranges :: [(a, a)]
ranges = forall a b. (a -> b) -> [a] -> [b]
map (a, a) -> (a, a)
fixEnds [(a, a)]
raw
    count :: Int
count = forall a. Integral a => a -> a -> a
div Int
size Int
precision
    largePrecision :: [(a, a)]
largePrecision = forall a. Int -> [a] -> [a]
take Int
precision (forall a. [a] -> [a]
reverse [(a, a)]
ranges)
    smallPrecision :: [(a, a)]
smallPrecision = forall a. Int -> [a] -> [a]
take Int
precision [(a, a)]
ranges
    oneRange :: (a, a) -> Gen [a]
oneRange (a
x, a
y) = forall a. Int -> Gen a -> Gen [a]
vectorOf Int
count (forall a. Random a => (a, a) -> Gen a
choose (a
x, a
y))

logRange :: Integral a => a -> (a, a)
logRange :: forall a. Integral a => a -> (a, a)
logRange a
1 = (a
10, a
99)
logRange (-1) = (-a
9, -a
1)
logRange a
n = case forall a. Ord a => a -> a -> Ordering
compare a
n a
0 of
  Ordering
EQ -> (a
0, a
9)
  Ordering
LT -> (forall a. Num a => a -> a
negate (forall a. Integral a => a -> a -> a
div a
b a
10), forall a. Num a => a -> a
negate (forall a. Integral a => a -> a -> a
div a
a a
10))
  Ordering
GT -> (a
10 forall a b. (Num a, Integral b) => a -> b -> a
^ a
n, a
10 forall a b. (Num a, Integral b) => a -> b -> a
^ (a
n forall a. Num a => a -> a -> a
+ a
1) forall a. Num a => a -> a -> a
- a
1)
  where
    (a
a, a
b) = forall a. Integral a => a -> (a, a)
logRange (forall a. Num a => a -> a
negate a
n)

-- | like (logBase10 n), except negative answers mean negative numbers, rather than fractions less than 1.
logish :: Integral t => t -> t
logish :: forall t. Integral t => t -> t
logish t
n
  | t
0 forall a. Ord a => a -> a -> Bool
<= t
n Bool -> Bool -> Bool
&& t
n forall a. Ord a => a -> a -> Bool
<= t
9 = t
0
  | t
n forall a. Ord a => a -> a -> Bool
> t
9 = t
1 forall a. Num a => a -> a -> a
+ forall t. Integral t => t -> t
logish (t
n forall a. Integral a => a -> a -> a
`div` t
10)
  | (-t
9) forall a. Ord a => a -> a -> Bool
<= t
n Bool -> Bool -> Bool
&& t
n forall a. Ord a => a -> a -> Bool
<= (-t
1) = -t
1
  | Bool
True = forall a. Num a => a -> a
negate (t
1 forall a. Num a => a -> a -> a
+ forall t. Integral t => t -> t
logish (forall a. Num a => a -> a
negate t
n))

-- =====================================================================