{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstrainedClassMethods #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
module Constrained.SumList where
import Constrained.AbstractSyntax
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 Constrained.PrettyUtils
import Control.Applicative ((<|>))
import Control.Monad (guard)
import Data.Either (partitionEithers)
import Data.List ((\\))
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
import Data.Maybe (fromMaybe, isNothing, listToMaybe)
import Data.Semigroup (sconcat)
import qualified Data.Set as Set
import GHC.Stack
import Prettyprinter hiding (cat)
import System.Random (Random (..))
import Test.QuickCheck (Arbitrary, Gen, choose, shuffle, vectorOf)
class HasSpec a => Complete a where
simplifyA :: Specification a -> Specification a
genFromSpecA :: forall m. (HasCallStack, HasSpec a, MonadGenError m) => Specification a -> GenT m a
theAddA :: Numeric a => IntW '[a, a] a
theAddA = IntW '[a, a] a
forall b. NumLike b => IntW '[b, b] b
AddW
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 Maybe a -> Maybe a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> Maybe a
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]
_ SpecificationD Deps a
s) = SpecificationD Deps a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound SpecificationD Deps a
s
knownUpperBound SpecificationD Deps a
TrueSpec = Maybe a
forall a. MaybeBounded a => Maybe a
upperBound
knownUpperBound (MemberSpec NonEmpty a
as) = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ NonEmpty a -> a
forall a. Ord a => NonEmpty a -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum NonEmpty a
as
knownUpperBound ErrorSpec {} = Maybe a
forall a. Maybe a
Nothing
knownUpperBound SuspendedSpec {} = Maybe a
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 Maybe a -> Maybe a -> Maybe a
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe a
forall a. MaybeBounded a => Maybe a
lowerBound) (Maybe a
hi Maybe a -> Maybe a -> Maybe a
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe a
forall a. MaybeBounded a => Maybe a
upperBound)
where
upper :: Maybe a -> Maybe a -> Maybe a
upper Maybe a
_ Maybe a
Nothing = Maybe a
forall a. Maybe a
Nothing
upper Maybe a
Nothing (Just a
b) = [a] -> Maybe a
forall a. [a] -> Maybe a
listToMaybe ([a] -> Maybe a) -> [a] -> Maybe a
forall a b. (a -> b) -> a -> b
$ [a
b, a
b a -> a -> a
forall a. Num a => a -> a -> a
- a
1 ..] [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
cant
upper (Just a
a) (Just a
b)
| a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b = a
a a -> Maybe () -> Maybe a
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (a
a a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [a]
cant)
| Bool
otherwise = [a] -> Maybe a
forall a. [a] -> Maybe a
listToMaybe ([a] -> Maybe a) -> [a] -> Maybe a
forall a b. (a -> b) -> a -> b
$ [a
b, a
b a -> a -> a
forall a. Num a => a -> a -> a
- a
1 .. a
a] [a] -> [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]
_ SpecificationD Deps a
s) = SpecificationD Deps a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound SpecificationD Deps a
s
knownLowerBound SpecificationD Deps a
TrueSpec = Maybe a
forall a. MaybeBounded a => Maybe a
lowerBound
knownLowerBound (MemberSpec NonEmpty a
as) = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ NonEmpty a -> a
forall a. Ord a => NonEmpty a -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum NonEmpty a
as
knownLowerBound ErrorSpec {} = Maybe a
forall a. Maybe a
Nothing
knownLowerBound SuspendedSpec {} = Maybe a
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 Maybe a -> Maybe a -> Maybe a
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe a
forall a. MaybeBounded a => Maybe a
lowerBound) (Maybe a
hi Maybe a -> Maybe a -> Maybe a
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe a
forall a. MaybeBounded a => Maybe a
upperBound)
where
lower :: Maybe a -> Maybe a -> Maybe a
lower Maybe a
Nothing Maybe a
_ = Maybe a
forall a. Maybe a
Nothing
lower (Just a
a) Maybe a
Nothing = [a] -> Maybe a
forall a. [a] -> Maybe a
listToMaybe ([a] -> Maybe a) -> [a] -> Maybe a
forall a b. (a -> b) -> a -> b
$ [a
a, a
a a -> a -> a
forall a. Num a => a -> a -> a
+ a
1 ..] [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
cant
lower (Just a
a) (Just a
b)
| a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b = a
a a -> Maybe () -> Maybe a
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (a
a a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [a]
cant)
| Bool
otherwise = [a] -> Maybe a
forall a. [a] -> Maybe a
listToMaybe ([a] -> Maybe a) -> [a] -> Maybe a
forall a b. (a -> b) -> a -> b
$ [a
a, a
a a -> a -> a
forall a. Num a => a -> a -> a
+ a
1 .. a
b] [a] -> [a] -> [a]
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 -> Specification a -> Bool
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
SuspendedSpec {} -> Bool
False
TypeSpec TypeSpec a
i [a]
cant -> [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([a] -> Bool) -> [a] -> Bool
forall a b. (a -> b) -> a -> b
$ NumSpec a -> [a]
forall a. (Enum a, Num a, MaybeBounded a) => NumSpec a -> [a]
enumerateInterval TypeSpec a
NumSpec a
i [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
cant
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 Maybe a -> Maybe a -> Maybe a
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe a
forall a. MaybeBounded a => Maybe a
lowerBound, Maybe a
hi Maybe a -> Maybe a -> Maybe a
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe a
forall a. MaybeBounded a => Maybe a
upperBound) of
(Maybe a
Nothing, Maybe a
Nothing) -> [a] -> [a] -> [a]
forall {a}. [a] -> [a] -> [a]
interleave [a
0 ..] [-a
1, -a
2 ..]
(Maybe a
Nothing, Just a
b) -> [a
b, a
b a -> a -> a
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 a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a] -> [a]
interleave [a]
ys [a]
xs
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 :: 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 <- Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemSIn
, a
0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
l
, Just a
u <- Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldSIn =
a -> Specification a
forall a. OrdLike a => a -> Specification a
leqSpec a
u
| Bool
otherwise = Specification a
forall deps a. SpecificationD deps a
TrueSpec
elemSIn' :: Specification a
elemSIn' = Specification a
elemSIn Specification a -> Specification a -> Specification a
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 = (Specification a, Specification a)
-> (Specification a, Specification a)
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)
NonEmpty String -> GenT m [a] -> GenT m [a]
forall a. HasCallStack => NonEmpty String -> GenT m a -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ String
"Can't generate list of ints with fold constraint"
, String
" elemSpec = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Specification a -> String
forall a. Show a => a -> String
show Specification a
elemSIn
, String
" normElemSpec = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Specification a -> String
forall a. Show a => a -> String
show Specification a
normElemS
, String
" foldSpec = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Specification a -> String
forall a. Show a => a -> String
show Specification a
foldSIn
]
)
(GenT m [a] -> GenT m [a]) -> GenT m [a] -> GenT m [a]
forall a b. (a -> b) -> a -> b
$ (Specification a, Specification a) -> Int -> [a] -> GenT m [a]
forall (m' :: * -> *).
MonadGenError m' =>
(Specification a, Specification a) -> Int -> [a] -> GenT m' [a]
gen (Specification a, Specification a)
narrowedSpecs Int
50 [] GenT m [a] -> ([a] -> GenT m [a]) -> GenT m [a]
forall a b. GenT m a -> (a -> GenT m b) -> GenT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Gen [a] -> GenT m [a]
forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen (Gen [a] -> GenT m [a]) -> ([a] -> Gen [a]) -> [a] -> GenT m [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Gen [a]
forall a. [a] -> Gen [a]
shuffle
where
normalize :: Specification a -> GenT m (Specification a)
normalize (ExplainSpec [String]
es Specification a
x) = [String] -> Specification a -> Specification a
forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es (Specification a -> Specification a)
-> GenT m (Specification a) -> GenT m (Specification a)
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 <- GenT m Int
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) Set a
forall a. Monoid a => a
mempty Specification a
spec
Specification a -> GenT m (Specification a)
normalize (Specification a -> GenT m (Specification a))
-> Specification a -> GenT m (Specification a)
forall a b. (a -> b) -> a -> b
$ Specification a
spec'
normalize Specification a
spec =
Specification a -> GenT m (Specification a)
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Specification a -> GenT m (Specification a))
-> Specification a -> GenT m (Specification a)
forall a b. (a -> b) -> a -> b
$
Specification a
-> (a -> Specification a) -> Maybe a -> Specification a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Specification a
forall a. Monoid a => a
mempty a -> Specification a
forall a. OrdLike a => a -> Specification a
geqSpec Maybe a
forall a. MaybeBounded a => Maybe a
lowerBound
Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> Specification a
-> (a -> Specification a) -> Maybe a -> Specification a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Specification a
forall a. Monoid a => a
mempty a -> Specification a
forall a. OrdLike a => a -> Specification a
leqSpec Maybe a
forall a. MaybeBounded a => Maybe a
upperBound
Specification a -> Specification a -> Specification a
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
_ =
Specification a -> GenT m (Specification a)
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( [a] -> NonEmpty String -> Specification a
forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
(Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
es)
(String -> NonEmpty String
forall a. a -> NonEmpty a
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 <- (Int -> Int) -> GenT m (Maybe a) -> GenT m (Maybe a)
forall (m :: * -> *) a. (Int -> Int) -> GenT m a -> GenT m a
scaleT (Int -> Int -> Int
forall a b. a -> b -> a
const Int
sz) (GenT m (Maybe a) -> GenT m (Maybe a))
-> GenT m (Maybe a) -> GenT m (Maybe a)
forall a b. (a -> b) -> a -> b
$ GenT GE a -> GenT m (Maybe a)
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
100 = Int
sz
| Maybe a -> Bool
forall a. Maybe a -> Bool
isNothing Maybe a
me = Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
sz Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
| Just a
e <- Maybe a
me, a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member a
e Set a
es = Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
sz Int -> Int -> Int
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
(Set a -> (a -> Set a) -> Maybe a -> Set a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set a
es ((a -> Set a -> Set a) -> Set a -> a -> Set a
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> Set a -> Set a
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0
, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a
0 a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldS =
NonEmpty String -> GenT m' [a]
forall a. HasCallStack => NonEmpty String -> GenT m' a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
genErrorNE (NonEmpty String -> GenT m' [a]) -> NonEmpty String -> GenT m' [a]
forall a b. (a -> b) -> a -> b
$
[String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ String
"Ran out of fuel in genNumList"
, String
" elemSpec =" String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Specification a -> String
forall a. Show a => a -> String
show Specification a
elemSIn
, String
" foldSpec = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Specification a -> String
forall a. Show a => a -> String
show Specification a
foldSIn
, String
" lst = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
lst)
]
| ErrorSpec NonEmpty String
err <- Specification a
foldS = NonEmpty String -> GenT m' [a]
forall a. HasCallStack => NonEmpty String -> GenT m' a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
genErrorNE NonEmpty String
err
| ErrorSpec {} <- Specification a
elemS = [a] -> GenT m' [a]
forall a. a -> GenT m' a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [a]
lst
| a
0 a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldS = [GenT GE [a]] -> GenT m' [a]
forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
[GenT GE a] -> GenT m a
oneofT [[a] -> GenT GE [a]
forall a. a -> GenT GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [a]
lst, forall (m'' :: * -> *). MonadGenError m'' => GenT m'' [a]
nonemptyList @GE]
| Bool
otherwise = GenT m' [a]
forall (m'' :: * -> *). MonadGenError m'' => GenT m'' [a]
nonemptyList
where
isUnsat :: (Specification a, Specification a) -> Bool
isUnsat (Specification a
elemSpec, Specification a
foldSpec) = Specification a -> Bool
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 a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldSpec) Bool -> Bool -> Bool
&& Specification a -> 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') <-
NonEmpty String
-> GenT m'' (a, (Specification a, Specification a))
-> GenT m'' (a, (Specification a, Specification a))
forall a.
HasCallStack =>
NonEmpty String -> GenT m'' a -> GenT m'' a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ String
"Generating an element:"
, String
" elemS = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Specification a -> String
forall a. Show a => a -> String
show Specification a
elemS
, String
" foldS = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Specification a -> String
forall a. Show a => a -> String
show Specification a
foldS
, String
" fuel = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
fuel
, String
" lst = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
lst)
]
)
(GenT m'' (a, (Specification a, Specification a))
-> GenT m'' (a, (Specification a, Specification a)))
-> GenT m'' (a, (Specification a, Specification a))
-> GenT m'' (a, (Specification a, Specification a))
forall a b. (a -> b) -> a -> b
$ do
Int
sz <- GenT m'' Int
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' = IntW '[a, a] a
-> ListCtx Value '[a, a] (HOLE a)
-> Specification a
-> Specification a
forall (as :: [*]) b a.
(AppRequires IntW as b, HasSpec a) =>
IntW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
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 IntW '[a, a] a
forall a. (Complete a, Numeric a) => IntW '[a, a] a
theAddA (HOLE a a
forall {k} (a :: k). HOLE a a
HOLE HOLE a a -> List Value '[a] -> ListCtx Value '[a, a] (HOLE a)
forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:? a -> Value a
forall a. Show a => a -> Value a
Value a
x Value a -> List Value '[] -> List Value '[a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Value '[]
forall {k} (f :: k -> *). List f '[]
Nil) Specification a
foldS
specs' :: (Specification a, Specification a)
specs' = a
-> Int
-> (Specification a, Specification a)
-> (Specification a, Specification a)
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 (Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> a) -> Int -> a
forall a b. (a -> b) -> a -> b
$ Int
fuel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
sz (Specification a
elemS, Specification a
foldS')
(a, (Specification a, Specification a))
-> GenT m'' (a, (Specification a, Specification a))
forall a. a -> GenT m'' a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
x, (Specification a, Specification a)
specs')
GenT m'' (a, (Specification a, Specification a))
-> ((a, (Specification a, Specification a)) -> Bool)
-> GenT m'' (a, (Specification a, Specification a))
forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
GenT m a -> (a -> Bool) -> GenT m a
`suchThatT` Bool -> Bool
not
(Bool -> Bool)
-> ((a, (Specification a, Specification a)) -> Bool)
-> (a, (Specification a, Specification a))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Specification a, Specification a) -> Bool
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
((Specification a, Specification a) -> Bool)
-> ((a, (Specification a, Specification a))
-> (Specification a, Specification a))
-> (a, (Specification a, Specification a))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, (Specification a, Specification a))
-> (Specification a, Specification a)
forall a b. (a, b) -> b
snd
(Specification a, Specification a) -> Int -> [a] -> GenT m'' [a]
forall (m' :: * -> *).
MonadGenError m' =>
(Specification a, Specification a) -> Int -> [a] -> GenT m' [a]
gen (Specification a, Specification a)
specs' (Int
fuel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (a
x a -> [a] -> [a]
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 = (Specification a, Specification a)
-> ((Specification a, Specification a)
-> (Specification a, Specification a))
-> Maybe (Specification a, Specification a)
-> (Specification a, Specification a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Specification a, Specification a)
specs (Specification a, Specification a)
-> (Specification a, Specification a)
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
go :: (Specification a, Specification a) -> Maybe (Specification a, Specification a)
go :: (Specification a, Specification a)
-> Maybe (Specification a, Specification a)
go (Specification a -> Specification a
forall a. Complete a => Specification a -> Specification a
simplifyA -> Specification a
elemS, Specification a -> Specification a
forall a. Complete a => Specification a -> Specification a
simplifyA -> Specification a
foldS) = case (Specification a
elemS, Specification a
foldS) of
(Specification a
_, ErrorSpec {}) -> Maybe (Specification a, Specification a)
forall a. Maybe a
Nothing
(Specification a, Specification a)
_ | Specification a -> Bool
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Bool
isEmptyNumSpec Specification a
foldS -> (Specification a, Specification a)
-> Maybe (Specification a, Specification a)
forall a. a -> Maybe a
Just (Specification a
elemS, NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec ([String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String
"Empty foldSpec:", Specification a -> String
forall a. Show a => a -> String
show Specification a
foldS]))
(ErrorSpec {}, MemberSpec NonEmpty a
ys) | NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
ys [a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
== [a
0] -> Maybe (Specification a, Specification a)
forall a. Maybe a
Nothing
(ErrorSpec {}, Specification a
_)
| a
0 a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldS -> (Specification a, Specification a)
-> Maybe (Specification a, Specification a)
forall a. a -> Maybe a
Just (Specification a
elemS, NonEmpty a -> Specification a
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec (a -> NonEmpty a
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
0))
| Bool
otherwise ->
(Specification a, Specification a)
-> Maybe (Specification a, Specification a)
forall a. a -> Maybe a
Just
( Specification a
elemS
, NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (NonEmpty String -> Specification a)
-> NonEmpty String -> Specification a
forall a b. (a -> b) -> a -> b
$
[String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ String
"Empty elemSpec and non-zero foldSpec"
, Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ Doc Any
"elemSpec =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
/> Specification a -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification a -> Doc ann
pretty Specification a
elemS
, Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ Doc Any
"foldSpec =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
/> Specification a -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification a -> Doc ann
pretty Specification a
foldS
]
)
(Specification a, Specification a)
_
| Just a
lo <- Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS
, a
0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
lo
, Just a
hi <- Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldS
,
Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
True ((a
hi a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<) (a -> Bool) -> Maybe a -> Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS) ->
(Specification a, Specification a)
-> Maybe (Specification a, Specification a)
forall a. a -> Maybe a
Just (Specification a
elemS Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Maybe a -> Maybe a -> NumSpec a
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (a -> Maybe a
forall a. a -> Maybe a
Just a
lo) (a -> Maybe a
forall a. a -> Maybe a
Just a
hi)), Specification a
foldS)
(Specification a, Specification a)
_
| Just a
lo <- Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS
, a
0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
lo
, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a
0 a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldS
,
Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
True ((a
lo a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>) (a -> Bool) -> Maybe a -> Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
foldS) ->
(Specification a, Specification a)
-> Maybe (Specification a, Specification a)
forall a. a -> Maybe a
Just (Specification a
elemS, Specification a
foldS Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Maybe a -> Maybe a -> NumSpec a
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (a -> Maybe a
forall a. a -> Maybe a
Just a
lo) Maybe a
forall a. Maybe a
Nothing))
(Specification a, Specification a)
_
| Just a
lo <- Specification a -> Maybe a
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 <- Specification a -> Maybe a
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 <- Specification a -> Maybe a
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 <- Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldS
, a
hi a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
loS
, a
lo a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
hiS a -> a -> a
forall a. Num a => a -> a -> a
- a
lo ->
(Specification a, Specification a)
-> Maybe (Specification a, Specification a)
forall a. a -> Maybe a
Just
( NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (NonEmpty String -> Specification a)
-> NonEmpty String -> Specification a
forall a b. (a -> b) -> a -> b
$ [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String
"Can't solve diophantine equation"]
, NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (NonEmpty String -> Specification a)
-> NonEmpty String -> Specification a
forall a b. (a -> b) -> a -> b
$ [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String
"Can't solve diophantine equation"]
)
(Specification a, Specification a)
_ -> Maybe (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
) =>
a ->
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 ((Specification a, Specification a)
-> (Specification a, Specification a))
-> (Specification a, Specification a)
-> (Specification a, Specification a)
forall a b. (a -> b) -> a -> b
$ ((Specification a, Specification a)
-> (Specification a, Specification a)
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 =
String -> (Specification a, Specification a)
forall a. HasCallStack => String -> a
error (String -> (Specification a, Specification a))
-> String -> (Specification a, Specification a)
forall a b. (a -> b) -> a -> b
$
[String] -> String
unlines
[ String
"narrowByFuelAndSize loops:"
, String
" fuel = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
fuel
, String
" size = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
size
, String
" specs = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ (Specification a, Specification a) -> String
forall a. Show a => a -> String
show (Specification a, Specification a)
specs
, String
" narrowFoldSpecs spec = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ (Specification a, Specification a) -> String
forall a. Show a => a -> String
show ((Specification a, Specification a)
-> (Specification a, Specification a)
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) = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Maybe (Specification a, Specification a) -> String
forall a. Show a => a -> String
show ((Specification a, Specification a)
-> Maybe (Specification a, Specification a)
go ((Specification a, Specification a)
-> (Specification a, Specification a)
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) ((Specification a, Specification a)
-> (Specification a, Specification a)
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')
onlyOnceTransformations :: (Specification a, Specification a)
-> (Specification a, Specification a)
onlyOnceTransformations (Specification a
elemS, Specification a
foldS)
| a
fuel a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
1 = (Specification a
elemS Specification a -> Specification a -> Specification a
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 t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0
canReach t
e t
currentfuel t
s
| t
s t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
e = t
0 t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
currentfuel
| Bool
otherwise = t -> t -> t -> Bool
canReach t
e (t
currentfuel t -> t -> t
forall a. Num a => a -> a -> a
- t
1) (t
s t -> t -> t
forall a. Num a => a -> a -> a
- t
e)
safeNegate :: a -> a
safeNegate a
a
| Just a
u <- Maybe a
forall a. MaybeBounded a => Maybe a
upperBound
, a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a -> a
forall a. Num a => a -> a
negate a
u =
a
u
| Bool
otherwise = a -> a
forall a. Num a => a -> a
negate a
a
divCeil :: a -> a -> a
divCeil a
a a
b
| a
b a -> a -> a
forall a. Num a => a -> a -> a
* a
d a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
a = a
d a -> a -> a
forall a. Num a => a -> a -> a
+ a
1
| Bool
otherwise = a
d
where
d :: a
d = a
a a -> 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 (Specification a -> Specification a
forall a. Complete a => Specification a -> Specification a
simplifyA -> Specification a
elemS, Specification a -> Specification a
forall a. Complete a => Specification a -> Specification a
simplifyA -> Specification a
foldS)
| a
fuel a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 = Maybe (Specification a, Specification a)
forall a. Maybe a
Nothing
| ErrorSpec {} <- Specification a
elemS = Maybe (Specification a, Specification a)
forall a. Maybe a
Nothing
| ErrorSpec {} <- Specification a
foldS = Maybe (Specification a, Specification a)
forall a. Maybe a
Nothing
| Just a
0 <- Specification a -> Maybe a
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 <- Specification a -> Maybe a
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 (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a
0 a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldS =
(Specification a, Specification a)
-> Maybe (Specification a, Specification a)
forall a. a -> Maybe a
Just (NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec ([String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String
"only 0 left"]), Specification a
foldS)
| Int
size Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
, a
0 a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
elemS =
(Specification a, Specification a)
-> Maybe (Specification a, Specification a)
forall a. a -> Maybe a
Just (Specification a
elemS Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> a -> Specification a
forall a. HasSpec a => a -> Specification a
notEqualSpec a
0, Specification a
foldS)
| MemberSpec NonEmpty a
ys <- Specification a
elemS
, let xs :: [a]
xs = NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
ys
, Just a
u <- Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldS
, (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a
0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<=) [a]
xs
, (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (a
0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<) [a]
xs
, let xMinP :: a
xMinP = [a] -> a
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$ (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (a
0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<) [a]
xs
possible :: a -> Bool
possible a
x = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
u Bool -> Bool -> Bool
|| a
xMinP a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
u a -> a -> a
forall a. Num a => a -> a -> a
- a
x
xs' :: [a]
xs' = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter a -> Bool
possible [a]
xs
, [a]
xs' [a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
/= [a]
xs =
(Specification a, Specification a)
-> Maybe (Specification a, Specification a)
forall a. a -> Maybe a
Just ([a] -> NonEmpty String -> Specification a
forall a. [a] -> NonEmpty String -> Specification a
memberSpecList ([a] -> [a]
forall a. Ord a => [a] -> [a]
nubOrd [a]
xs') (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"None of " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show [a]
xs String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
" are possible")), Specification a
foldS)
| Just a
e <- Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS
, a
e a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0
, Just a
s <- Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
foldS
, a
s a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0
, let c :: a
c = a -> a -> a
forall a. Integral a => a -> a -> a
divCeil a
s a
fuel
, a
e a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
c =
(Specification a, Specification a)
-> Maybe (Specification a, Specification a)
forall a. a -> Maybe a
Just (Specification a
elemS Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> a -> Specification a
forall a. OrdLike a => a -> Specification a
geqSpec a
c, Specification a
foldS)
| Just a
e <- Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS
, a
e a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0
, Just a
s <- Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldS
, a
s a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0
, let c :: a
c = a -> a -> a
forall a. Integral a => a -> a -> a
divCeil (a -> a
forall {a}. (MaybeBounded a, Ord a, Num a) => a -> a
safeNegate a
s) a
fuel
, a -> a
forall a. Num a => a -> a
negate a
c a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
e
, Bool -> (a -> Bool) -> Maybe a -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (a
c a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<) (Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS) =
(Specification a, Specification a)
-> Maybe (Specification a, Specification a)
forall a. a -> Maybe a
Just (Specification a
elemS Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> a -> Specification a
forall a. OrdLike a => a -> Specification a
leqSpec a
c, Specification a
foldS)
| Just a
s <- Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
foldS
, a
s a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0
, Just a
e <- Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS
, a
e a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0
, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> Bool
forall {t} {t}. (Num t, Num t, Ord t, Ord t) => t -> t -> t -> Bool
canReach a
e (a
fuel a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
2 a -> a -> a
forall a. Num a => a -> a -> a
+ a
1) a
s
, Bool -> (a -> Bool) -> Maybe a -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
0) (Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS) =
(Specification a, Specification a)
-> Maybe (Specification a, Specification a)
forall a. a -> Maybe a
Just (Specification a
elemS Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> a -> Specification a
forall a. OrdLike a => a -> Specification a
gtSpec a
0, Specification a
foldS)
| Just a
s <- Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldS
, a
s a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0
, Just a
e <- Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS
, a
e a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0
, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> Bool
forall {t} {t}. (Num t, Num t, Ord t, Ord t) => t -> t -> t -> Bool
canReach (a -> a
forall {a}. (MaybeBounded a, Ord a, Num a) => a -> a
safeNegate a
e) (a
fuel a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
2 a -> a -> a
forall a. Num a => a -> a -> a
+ a
1) (a -> a
forall {a}. (MaybeBounded a, Ord a, Num a) => a -> a
safeNegate a
s)
, Bool -> (a -> Bool) -> Maybe a -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (a
0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<=) (Specification a -> Maybe a
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS) =
(Specification a, Specification a)
-> Maybe (Specification a, Specification a)
forall a. a -> Maybe a
Just (Specification a
elemS Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> a -> Specification a
forall a. OrdLike a => a -> Specification a
ltSpec a
0, Specification a
foldS)
| Bool
otherwise = Maybe (Specification a, Specification a)
forall a. Maybe a
Nothing
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 = Specification a -> Specification a -> GenT m [a]
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 Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
geqSpec Integer
0 =
NonEmpty String -> GenT m [a]
forall a. HasCallStack => NonEmpty String -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE
( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ String
"genListWithSize called with possible negative size"
, String
" sizeSpec = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Specification Integer -> String
forall a. HasSpec a => Specification a -> String
specName Specification Integer
sizeSpec
, String
" elemSpec = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Specification a -> String
forall a. HasSpec a => Specification a -> String
specName Specification a
elemSpec
, String
" foldSpec = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Specification a -> String
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
let sizeAdjusted :: Specification Integer
sizeAdjusted =
if a
total a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0
then Specification Integer
sizeSpec Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
gtSpec Integer
0
else
if forall a. MaybeBounded a => Maybe a
lowerBound @a Maybe a -> Maybe a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> Maybe a
forall a. a -> Maybe a
Just a
0
then Specification Integer
sizeSpec Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Specification Integer
forall a. a -> Specification a
equalSpec Integer
0
else Specification Integer
sizeSpec Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
gtSpec Integer
0
message :: [String]
message =
[ String
"\nGenSizedList fails"
, String
"sizespec = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Specification Integer -> String
forall a. HasSpec a => Specification a -> String
specName Specification Integer
sizeSpec
, String
"elemSpec = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Specification a -> String
forall a. HasSpec a => Specification a -> String
specName Specification a
elemSpec
, String
"foldSpec = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Specification a -> String
forall a. HasSpec a => Specification a -> String
specName Specification a
foldSpec
, String
"total choosen from foldSpec = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
total
, String
"size adjusted for total = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Specification Integer -> String
forall a. Show a => a -> String
show Specification Integer
sizeAdjusted
]
[String] -> GenT m [a] -> GenT m [a]
forall (m :: * -> *) a. MonadGenError m => [String] -> m a -> m a
push [String]
message (GenT m [a] -> GenT m [a]) -> GenT m [a] -> GenT m [a]
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 a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
total a
0 of
Ordering
EQ ->
if Integer
count Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
then [a] -> GenT m [a]
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
else Specification a -> a -> Integer -> GenT m [a]
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 -> Specification a -> a -> Integer -> GenT m [a]
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 -> Specification a -> a -> Integer -> GenT m [a]
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 <-
Gen (Cost, Solution t) -> GenT m (Cost, Solution t)
forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen (Gen (Cost, Solution t) -> GenT m (Cost, Solution t))
-> Gen (Cost, Solution t) -> GenT m (Cost, Solution t)
forall a b. (a -> b) -> a -> b
$
t
-> t
-> (String, t -> Bool)
-> t
-> Int
-> Cost
-> Gen (Cost, Solution t)
forall t.
(Show t, Integral t, Random t) =>
t
-> t
-> (String, t -> Bool)
-> t
-> Int
-> Cost
-> Gen (Cost, Solution t)
pickAll
(t -> Specification t -> t
forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
minFromSpec t
0 Specification t
elemspec)
(t -> Specification t -> t
forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
maxFromSpec t
total Specification t
elemspec)
(Specification t -> (String, t -> Bool)
forall a. HasSpec a => Specification a -> (String, a -> Bool)
predSpecPair Specification t
elemspec)
t
total
(Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
count)
(Int -> Cost
Cost Int
0)
case (Cost, Solution t) -> Solution t
forall a b. (a, b) -> b
snd (Cost, Solution t)
sol of
No [String]
msgs -> NonEmpty String -> GenT m [t]
forall a. HasCallStack => NonEmpty String -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE ([String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String]
msgs)
Yes ([t]
x :| [[t]]
_) -> [t] -> GenT m [t]
forall a. a -> GenT m a
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]
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 <-
Gen (Cost, Solution t) -> GenT m (Cost, Solution t)
forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen (Gen (Cost, Solution t) -> GenT m (Cost, Solution t))
-> Gen (Cost, Solution t) -> GenT m (Cost, Solution t)
forall a b. (a -> b) -> a -> b
$
t
-> t
-> (String, t -> Bool)
-> t
-> Int
-> Cost
-> Gen (Cost, Solution t)
forall t.
(Show t, Integral t, Random t) =>
t
-> t
-> (String, t -> Bool)
-> t
-> Int
-> Cost
-> Gen (Cost, Solution t)
pickAll
(t -> Specification t -> t
forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
minFromSpec (t
total t -> t -> t
forall a. Num a => a -> a -> a
+ (t
total t -> t -> t
forall a. Integral a => a -> a -> a
`div` t
4)) Specification t
elemspec)
(t -> Specification t -> t
forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
maxFromSpec (t
0 t -> t -> t
forall a. Num a => a -> a -> a
- (t
total t -> t -> t
forall a. Integral a => a -> a -> a
`div` t
4)) Specification t
elemspec)
(Specification t -> (String, t -> Bool)
forall a. HasSpec a => Specification a -> (String, a -> Bool)
predSpecPair Specification t
elemspec)
t
total
(Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
count)
(Int -> Cost
Cost Int
0)
case (Cost, Solution t) -> Solution t
forall a b. (a, b) -> b
snd (Cost, Solution t)
sol of
No [String]
msgs -> NonEmpty String -> GenT m [t]
forall a. HasCallStack => NonEmpty String -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE ([String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String]
msgs)
Yes ([t]
x :| [[t]]
_) -> [t] -> GenT m [t]
forall a. a -> GenT m a
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 = Specification a -> String
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 = (Specification a -> String
forall a. HasSpec a => Specification a -> String
specName Specification a
spec, (a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
spec))
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]
_ SpecificationD Deps n
spec) = forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
minFromSpec @n n
dv SpecificationD Deps n
spec
minFromSpec n
dv SpecificationD Deps n
TrueSpec = n
dv
minFromSpec n
dv s :: SpecificationD Deps n
s@(SuspendedSpec Var n
_ PredD Deps
_) =
case SpecificationD Deps n -> SpecificationD Deps n
forall a. Complete a => Specification a -> Specification a
simplifyA SpecificationD Deps n
s of
SuspendedSpec {} -> n
dv
SpecificationD Deps n
x -> forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
minFromSpec @n n
dv SpecificationD Deps n
x
minFromSpec n
dv (ErrorSpec NonEmpty String
_) = n
dv
minFromSpec n
_ (MemberSpec NonEmpty n
xs) = NonEmpty n -> n
forall a. Ord a => NonEmpty a -> a
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]
_) = n -> (n -> n) -> Maybe n -> n
forall b a. b -> (a -> b) -> Maybe a -> b
maybe n
dv n -> n
forall a. a -> a
id Maybe n
lo
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]
_ SpecificationD Deps n
spec) = forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
maxFromSpec @n n
dv SpecificationD Deps n
spec
maxFromSpec n
dv SpecificationD Deps n
TrueSpec = n
dv
maxFromSpec n
dv s :: SpecificationD Deps n
s@(SuspendedSpec Var n
_ PredD Deps
_) =
case SpecificationD Deps n -> SpecificationD Deps n
forall a. Complete a => Specification a -> Specification a
simplifyA SpecificationD Deps n
s of
SuspendedSpec {} -> n
dv
SpecificationD Deps n
x -> forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
maxFromSpec @n n
dv SpecificationD Deps n
x
maxFromSpec n
dv (ErrorSpec NonEmpty String
_) = n
dv
maxFromSpec n
_ (MemberSpec NonEmpty n
xs) = NonEmpty n -> n
forall a. Ord a => NonEmpty a -> a
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]
_) = n -> (n -> n) -> Maybe n -> n
forall b a. b -> (a -> b) -> Maybe a -> b
maybe n
dv n -> n
forall a. a -> a
id Maybe n
hi
data Solution t = Yes (NonEmpty [t]) | No [String]
deriving (Solution t -> Solution t -> Bool
(Solution t -> Solution t -> Bool)
-> (Solution t -> Solution t -> Bool) -> Eq (Solution t)
forall t. Eq t => Solution t -> Solution t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: Solution t -> Solution t -> Bool
Eq)
instance Show t => Show (Solution t) where
show :: Solution t -> String
show (No [String]
xs) = String
"No" String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ [String] -> String
unlines [String]
xs
show (Yes NonEmpty [t]
xs) = String
"Yes " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ NonEmpty [t] -> String
forall a. Show a => a -> String
show NonEmpty [t]
xs
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 [Either (NonEmpty [t]) [String]] -> ([NonEmpty [t]], [[String]])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ((Solution t -> Either (NonEmpty [t]) [String])
-> [Solution t] -> [Either (NonEmpty [t]) [String]]
forall a b. (a -> b) -> [a] -> [b]
map (\case Yes NonEmpty [t]
x -> NonEmpty [t] -> Either (NonEmpty [t]) [String]
forall a b. a -> Either a b
Left NonEmpty [t]
x; No [String]
x -> [String] -> Either (NonEmpty [t]) [String]
forall a b. b -> Either a b
Right [String]
x) [Solution t]
sols) of
([], [String]
n : [[String]]
_) -> [String] -> Solution t
forall t. [String] -> Solution t
No [String]
n
(NonEmpty [t]
y : [NonEmpty [t]]
ys, [[String]]
_) -> NonEmpty [t] -> Solution t
forall t. NonEmpty [t] -> Solution t
Yes (NonEmpty [t] -> Solution t) -> NonEmpty [t] -> Solution t
forall a b. (a -> b) -> a -> b
$ NonEmpty (NonEmpty [t]) -> NonEmpty [t]
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty [t]
y NonEmpty [t] -> [NonEmpty [t]] -> NonEmpty (NonEmpty [t])
forall a. a -> [a] -> NonEmpty a
:| [NonEmpty [t]]
ys)
([], []) ->
[String] -> Solution t
forall t. [String] -> Solution t
No
[ String
"\nThe sample in pickAll was empty"
, String
" smallest = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
smallest
, String
" largest = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
largest
, String
" pred = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
pName
, String
" total = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
total
, String
" count = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
count
]
newtype Cost = Cost Int deriving (Cost -> Cost -> Bool
(Cost -> Cost -> Bool) -> (Cost -> Cost -> Bool) -> Eq Cost
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Cost -> Cost -> Bool
== :: Cost -> Cost -> Bool
$c/= :: Cost -> Cost -> Bool
/= :: Cost -> Cost -> Bool
Eq, Int -> Cost -> String -> String
[Cost] -> String -> String
Cost -> String
(Int -> Cost -> String -> String)
-> (Cost -> String) -> ([Cost] -> String -> String) -> Show Cost
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Cost -> String -> String
showsPrec :: Int -> Cost -> String -> String
$cshow :: Cost -> String
show :: Cost -> String
$cshowList :: [Cost] -> String -> String
showList :: [Cost] -> String -> String
Show, Integer -> Cost
Cost -> Cost
Cost -> Cost -> Cost
(Cost -> Cost -> Cost)
-> (Cost -> Cost -> Cost)
-> (Cost -> Cost -> Cost)
-> (Cost -> Cost)
-> (Cost -> Cost)
-> (Cost -> Cost)
-> (Integer -> Cost)
-> Num Cost
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: Cost -> Cost -> Cost
+ :: Cost -> Cost -> Cost
$c- :: Cost -> Cost -> Cost
- :: Cost -> Cost -> Cost
$c* :: Cost -> Cost -> Cost
* :: Cost -> Cost -> Cost
$cnegate :: Cost -> Cost
negate :: Cost -> Cost
$cabs :: Cost -> Cost
abs :: Cost -> Cost
$csignum :: Cost -> Cost
signum :: Cost -> Cost
$cfromInteger :: Integer -> Cost
fromInteger :: Integer -> Cost
Num, Eq Cost
Eq Cost =>
(Cost -> Cost -> Ordering)
-> (Cost -> Cost -> Bool)
-> (Cost -> Cost -> Bool)
-> (Cost -> Cost -> Bool)
-> (Cost -> Cost -> Bool)
-> (Cost -> Cost -> Cost)
-> (Cost -> Cost -> Cost)
-> Ord 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
$ccompare :: Cost -> Cost -> Ordering
compare :: Cost -> Cost -> Ordering
$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
>= :: Cost -> Cost -> Bool
$cmax :: Cost -> Cost -> Cost
max :: Cost -> Cost -> Cost
$cmin :: Cost -> Cost -> Cost
min :: Cost -> Cost -> Cost
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 = (Cost, Solution t) -> m (Cost, Solution t)
forall a. a -> m a
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 Cost -> 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 Cost -> 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]
_) -> (Cost, Solution t) -> m (Cost, Solution t)
forall a. a -> m a
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 =
[String] -> Solution t
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 = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
p
, String
" smallest = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
smallest
, String
" largest = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
largest
, String
" total = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
total
, String
" count = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
count
, String
" cost = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Cost -> String
forall a. Show a => a -> String
show Cost
cost
, String
"Small sample of what was explored"
, [(t, t)] -> String
forall a. Show a => a -> String
show [(t, t)]
samp
]
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 .. b -> b -> b
forall a. Integral a => a -> a -> a
div b
count b
2], let j :: b
j = b
count b -> b -> b
forall a. Num a => a -> a -> a
- b
i]
{-# SPECIALIZE splitsOf :: Int -> [(Int, Int)] #-}
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 Cost -> Cost -> Bool
forall a. Ord a => a -> a -> Bool
> Cost
1000 =
(Cost, Solution t) -> Gen (Cost, Solution t)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Cost, Solution t) -> Gen (Cost, Solution t))
-> (Cost, Solution t) -> Gen (Cost, Solution t)
forall a b. (a -> b) -> a -> b
$
( Cost
cost
, [String] -> Solution t
forall t. [String] -> Solution t
No
[ String
"\nPickAll exceeds cost limit " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Cost -> String
forall a. Show a => a -> String
show Cost
cost
, String
" predicate = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
pName
, String
" smallest = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
smallest
, String
" largest = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
largest
, String
" total = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
total
, String
" count = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Int -> String
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 t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0 Bool -> Bool -> Bool
&& t -> Bool
p t
total
then (Cost, Solution t) -> Gen (Cost, Solution t)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cost
cost, NonEmpty [t] -> Solution t
forall t. NonEmpty [t] -> Solution t
Yes (NonEmpty [t] -> Solution t) -> NonEmpty [t] -> Solution t
forall a b. (a -> b) -> a -> b
$ [t] -> NonEmpty [t]
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [])
else
(Cost, Solution t) -> Gen (Cost, Solution t)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( Cost
cost
, [String] -> Solution t
forall t. [String] -> Solution t
No
[ String
"We are trying to find list of length 0."
, String
" Whose sum is " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
total String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
"."
, String
" That is only possible if the sum == 0."
, String
" All elements have to satisfy " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
pName
, String
" smallest = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
smallest
, String
" largest = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
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 (Cost, Solution t) -> Gen (Cost, Solution t)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cost
cost, NonEmpty [t] -> Solution t
forall t. NonEmpty [t] -> Solution t
Yes (NonEmpty [t] -> Solution t) -> NonEmpty [t] -> Solution t
forall a b. (a -> b) -> a -> b
$ [t] -> NonEmpty [t]
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [t
total])
else (Cost, Solution t) -> Gen (Cost, Solution t)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cost
cost, Cost -> String -> t -> t -> t -> Int -> [(t, t)] -> Solution t
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 t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
largest =
(Cost, Solution t) -> Gen (Cost, Solution t)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Cost, Solution t) -> Gen (Cost, Solution t))
-> (Cost, Solution t) -> Gen (Cost, Solution t)
forall a b. (a -> b) -> a -> b
$
( Cost
cost
, [String] -> Solution t
forall t. [String] -> Solution t
No
[ String
"\nThe feasible range to pickAll ["
String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
smallest
String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
" .. "
String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show (t -> t -> t
forall a. Integral a => a -> a -> a
div t
total t
2)
String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
"] was empty"
, String
" predicate = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
pName
, String
" smallest = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
smallest
, String
" largest = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
largest
, String
" total = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
total
, String
" count = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
count
, String
" cost = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Cost -> String
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
[(t, t)]
choices <- t -> t -> t -> t -> Int -> Gen [(t, t)]
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 ((t, t) -> Bool) -> [(t, t)] -> [(t, t)]
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
[] -> (Cost, Solution t) -> Gen (Cost, Solution t)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Cost, Solution t) -> Gen (Cost, Solution t))
-> (Cost, Solution t) -> Gen (Cost, Solution t)
forall a b. (a -> b) -> a -> b
$ (Cost
cost Cost -> Cost -> Cost
forall a. Num a => a -> a -> a
+ Cost
1, Cost -> String -> t -> t -> t -> Int -> [(t, t)] -> Solution t
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 (Int -> [(t, t)] -> [(t, t)]
forall a. Int -> [a] -> [a]
take Int
10 [(t, t)]
choices))
[(t, t)]
zs -> (Cost, Solution t) -> Gen (Cost, Solution t)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Cost, Solution t) -> Gen (Cost, Solution t))
-> (Cost, Solution t) -> Gen (Cost, Solution t)
forall a b. (a -> b) -> a -> b
$ (Cost
cost Cost -> Cost -> Cost
forall a. Num a => a -> a -> a
+ Cost
1, NonEmpty [t] -> Solution t
forall t. NonEmpty [t] -> Solution t
Yes (NonEmpty [t] -> Solution t) -> NonEmpty [t] -> Solution t
forall a b. (a -> b) -> a -> b
$ [[t]] -> NonEmpty [t]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList (((t, t) -> [t]) -> [(t, t)] -> [[t]]
forall a b. (a -> b) -> [a] -> [b]
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
[(t, t)]
choices <- t -> t -> t -> t -> Int -> Gen [(t, t)]
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
[(Int, Int)]
splits <-
if Int
count Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
20
then [(Int, Int)] -> Gen [(Int, Int)]
forall a. [a] -> Gen [a]
shuffle ([(Int, Int)] -> Gen [(Int, Int)])
-> [(Int, Int)] -> Gen [(Int, Int)]
forall a b. (a -> b) -> a -> b
$ Int -> [(Int, Int)] -> [(Int, Int)]
forall a. Int -> [a] -> [a]
take Int
10 (Int -> [(Int, Int)]
forall b. Integral b => b -> [(b, b)]
splitsOf Int
count)
else
if t
total t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> t
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
count
then [(Int, Int)] -> Gen [(Int, Int)]
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Int, Int)] -> [(Int, Int)]
forall a. [a] -> [a]
reverse (Int -> [(Int, Int)]
forall b. Integral b => b -> [(b, b)]
splitsOf Int
count))
else [(Int, Int)] -> Gen [(Int, Int)]
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> [(Int, Int)]
forall b. Integral b => b -> [(b, b)]
splitsOf Int
count)
Solution t
-> ((Int, Int) -> Cost -> Gen (Cost, Solution t))
-> [(Int, Int)]
-> Cost
-> Gen (Cost, Solution t)
forall (m :: * -> *) t x.
Monad m =>
Solution t
-> (x -> Cost -> m (Cost, Solution t))
-> [x]
-> Cost
-> m (Cost, Solution t)
firstYesG
([String] -> Solution t
forall t. [String] -> Solution t
No [String
"\nNo split has a solution", String
"cost = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Cost -> String
forall a. Show a => a -> String
show Cost
cost])
(t
-> t
-> (String, t -> Bool)
-> t
-> [(t, t)]
-> (Int, Int)
-> Cost
-> Gen (Cost, Solution t)
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
doSplit ::
(Random t, Show t, Integral t) =>
t ->
t ->
(String, t -> Bool) ->
t ->
[(t, 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
go :: [(t, t)] -> Cost -> Gen (Cost, Solution t)
go ((t
x, t
y) : [(t, t)]
more) Cost
cost0 = do
(Cost
cost1, Solution t
ans1) <- t
-> t
-> (String, t -> Bool)
-> t
-> Int
-> Cost
-> Gen (Cost, Solution t)
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
(Cost
cost2, Solution t
ans2) <- t
-> t
-> (String, t -> Bool)
-> t
-> Int
-> Cost
-> Gen (Cost, Solution t)
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) -> (Cost, Solution t) -> Gen (Cost, Solution t)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Cost, Solution t) -> Gen (Cost, Solution t))
-> (Cost, Solution t) -> Gen (Cost, Solution t)
forall a b. (a -> b) -> a -> b
$ (Cost
cost2, NonEmpty [t] -> Solution t
forall t. NonEmpty [t] -> Solution t
Yes ([[t]] -> NonEmpty [t]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [[t]
a [t] -> [t] -> [t]
forall a. Semigroup a => a -> a -> a
<> [t]
b | [t]
a <- NonEmpty [t] -> [[t]]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty [t]
ys, [t]
b <- NonEmpty [t] -> [[t]]
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
[] ->
(Cost, Solution t) -> Gen (Cost, Solution t)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Cost, Solution t) -> Gen (Cost, Solution t))
-> (Cost, Solution t) -> Gen (Cost, Solution t)
forall a b. (a -> b) -> a -> b
$
( Cost
cost
, [String] -> Solution t
forall t. [String] -> Solution t
No
[ String
"\nThe sample passed to doSplit [" String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
smallest String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
" .. " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show (t -> t -> t
forall a. Integral a => a -> a -> a
div t
total t
2) String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
"] was empty"
, String
" predicate = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
pName
, String
" smallest = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
smallest
, String
" largest = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
largest
, String
" total " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
total
, String
" count = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j)
, String
" split of count = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Int
i, Int
j)
]
)
((t
left, t
right) : [(t, t)]
_) ->
(Cost, Solution t) -> Gen (Cost, Solution t)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Cost, Solution t) -> Gen (Cost, Solution t))
-> (Cost, Solution t) -> Gen (Cost, Solution t)
forall a b. (a -> b) -> a -> b
$
( Cost
cost
, [String] -> Solution t
forall t. [String] -> Solution t
No
[ String
"\nAll choices in (genSizedList " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j) String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
" 'p' " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
total String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
") have failed."
, String
"Here is 1 example failure."
, String
" smallest = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
smallest
, String
" largest = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
largest
, String
" total " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
total String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
left String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
" + " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
right
, String
" count = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j) String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
", split of count = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Int
i, Int
j)
, String
"We are trying to solve sub-problems like:"
, String
" split " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
left String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
" into " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
" parts, where all parts meet 'p'"
, String
" split " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
right String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
" into " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
j String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
" parts, where all parts meet 'p'"
, String
"Predicate 'p' = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ String
pName
, String
"A small prefix of the sample, elements (x,y) where x+y = " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
total
, [String] -> String
unlines (((t, t) -> String) -> [(t, t)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String
" " String -> String -> String
forall {a}. [a] -> [a] -> [a]
++) (String -> String) -> ((t, t) -> String) -> (t, t) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t, t) -> String
forall a. Show a => a -> String
show) (Int -> [(t, t)] -> [(t, t)]
forall a. Int -> [a] -> [a]
take Int
10 [(t, t)]
sample))
]
)
{-# INLINE doSplit #-}
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 t -> t -> t
forall a. Num a => a -> a -> a
- t
smallest t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
bound = do
[(t, t)] -> Gen [(t, t)]
forall a. [a] -> Gen [a]
shuffle ([(t, t)] -> Gen [(t, t)]) -> [(t, t)] -> Gen [(t, t)]
forall a b. (a -> b) -> a -> b
$ ((t, t) -> Bool) -> [(t, t)] -> [(t, t)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile ((t -> t -> Bool) -> (t, t) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry t -> t -> Bool
forall a. Ord a => a -> a -> Bool
(<=)) [(t
x, t
total t -> t -> t
forall a. Num a => a -> a -> a
- t
x) | t
x <- [t
smallest .. t
total]]
| Bool
otherwise = do
[t]
choices <- t -> t -> Int -> Int -> Bool -> Gen [t]
forall a.
(Random a, Integral a) =>
a -> a -> Int -> Int -> Bool -> Gen [a]
fair t
smallest t
largest Int
size Int
5 Bool
True
[(t, t)] -> Gen [(t, t)]
forall a. [a] -> Gen [a]
shuffle [(t
x, t
total t -> t -> t
forall a. Num a => a -> a -> a
- t
x) | t
x <- [t]
choices]
{-# INLINE smallSample #-}
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 =
[[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[a]] -> [a]) -> Gen [[a]] -> Gen [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((a, a) -> Gen [a]) -> [(a, a)] -> Gen [[a]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (a, a) -> Gen [a]
oneRange (if Bool
isLarge then [(a, a)]
largePrecision else [(a, a)]
smallPrecision)
where
raw :: [(a, a)]
raw = (a -> (a, a)) -> [a] -> [(a, a)]
forall a b. (a -> b) -> [a] -> [b]
map a -> (a, a)
forall a. Integral a => a -> (a, a)
logRange [a -> a
forall t. Integral t => t -> t
logish a
smallest .. a -> a
forall t. Integral t => t -> t
logish a
largest]
fixEnds :: (a, a) -> (a, a)
fixEnds (a
x, a
y) = (a -> a -> a
forall a. Ord a => a -> a -> a
max a
smallest a
x, a -> a -> a
forall a. Ord a => a -> a -> a
min a
largest a
y)
ranges :: [(a, a)]
ranges = ((a, a) -> (a, a)) -> [(a, a)] -> [(a, a)]
forall a b. (a -> b) -> [a] -> [b]
map (a, a) -> (a, a)
fixEnds [(a, a)]
raw
count :: Int
count = Int -> Int -> Int
forall a. Integral a => a -> a -> a
div Int
size Int
precision
largePrecision :: [(a, a)]
largePrecision = Int -> [(a, a)] -> [(a, a)]
forall a. Int -> [a] -> [a]
take Int
precision ([(a, a)] -> [(a, a)]
forall a. [a] -> [a]
reverse [(a, a)]
ranges)
smallPrecision :: [(a, a)]
smallPrecision = Int -> [(a, a)] -> [(a, a)]
forall a. Int -> [a] -> [a]
take Int
precision [(a, a)]
ranges
oneRange :: (a, a) -> Gen [a]
oneRange (a
x, a
y) = Int -> Gen a -> Gen [a]
forall a. Int -> Gen a -> Gen [a]
vectorOf Int
count ((a, a) -> Gen a
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 a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
n a
0 of
Ordering
EQ -> (a
0, a
9)
Ordering
LT -> (a -> a
forall a. Num a => a -> a
negate (a -> a -> a
forall a. Integral a => a -> a -> a
div a
b a
10), a -> a
forall a. Num a => a -> a
negate (a -> a -> a
forall a. Integral a => a -> a -> a
div a
a a
10))
Ordering
GT -> (a
10 a -> a -> a
forall a b. (Num a, Integral b) => a -> b -> a
^ a
n, a
10 a -> a -> a
forall a b. (Num a, Integral b) => a -> b -> a
^ (a
n a -> a -> a
forall a. Num a => a -> a -> a
+ a
1) a -> a -> a
forall a. Num a => a -> a -> a
- a
1)
where
(a
a, a
b) = a -> (a, a)
forall a. Integral a => a -> (a, a)
logRange (a -> a
forall a. Num a => a -> a
negate a
n)
logish :: Integral t => t -> t
logish :: forall t. Integral t => t -> t
logish t
n
| t
0 t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
n Bool -> Bool -> Bool
&& t
n t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
9 = t
0
| t
n t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
9 = t
1 t -> t -> t
forall a. Num a => a -> a -> a
+ t -> t
forall t. Integral t => t -> t
logish (t
n t -> t -> t
forall a. Integral a => a -> a -> a
`div` t
10)
| (-t
9) t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
n Bool -> Bool -> Bool
&& t
n t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= (-t
1) = -t
1
| Bool
True = t -> t
forall a. Num a => a -> a
negate (t
1 t -> t -> t
forall a. Num a => a -> a -> a
+ t -> t
forall t. Integral t => t -> t
logish (t -> t
forall a. Num a => a -> a
negate t
n))