{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

module Constrained.Examples.Fold where

import Constrained.API
import Constrained.Examples.List (Numbery)
import Constrained.GenT (GE (..), catMessages, genFromGenT, inspect)
import Constrained.SumList
import Data.String (fromString)
import Prettyprinter (fillSep, punctuate, space)
import System.Random (Random)
import Test.QuickCheck hiding (forAll, total)

-- ========================================================
-- Specifications we use in the examples and in the tests

oddSpec :: Specification Int
oddSpec :: Specification Int
oddSpec = [String] -> Specification Int -> Specification Int
forall deps a.
[String] -> SpecificationD deps a -> SpecificationD deps a
ExplainSpec [String
"odd via (y+y+1)"] (Specification Int -> Specification Int)
-> Specification Int -> Specification Int
forall a b. (a -> b) -> a -> b
$
  (Term Int -> Pred) -> Specification Int
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Int -> Pred) -> Specification Int)
-> (Term Int -> Pred) -> Specification Int
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var|oddx|] ->
    ((forall b. Term b -> b) -> GE Int) -> (Term Int -> [Pred]) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists
      (\forall b. Term b -> b
eval -> Int -> GE Int
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Int -> Int
forall a. Integral a => a -> a -> a
div (Term Int -> Int
forall b. Term b -> b
eval Term Int
oddx Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
2))
      (\ Term Int
[var|y|] -> [Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
oddx Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
y Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
y Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
1])

evenSpec ::
  forall n.
  (TypeSpec n ~ NumSpec n, Integral n, HasSpec n, MaybeBounded n) =>
  Specification n
evenSpec :: forall n.
(TypeSpec n ~ NumSpec n, Integral n, HasSpec n, MaybeBounded n) =>
Specification n
evenSpec = [String] -> SpecificationD Deps n -> SpecificationD Deps n
forall deps a.
[String] -> SpecificationD deps a -> SpecificationD deps a
ExplainSpec [String
"even via (x+x)"] (SpecificationD Deps n -> SpecificationD Deps n)
-> SpecificationD Deps n -> SpecificationD Deps n
forall a b. (a -> b) -> a -> b
$
  (Term n -> Pred) -> SpecificationD Deps n
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term n -> Pred) -> SpecificationD Deps n)
-> (Term n -> Pred) -> SpecificationD Deps n
forall a b. (a -> b) -> a -> b
$ \ Term n
[var|evenx|] ->
    ((forall b. Term b -> b) -> GE n) -> (Term n -> [Pred]) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists
      (\forall b. Term b -> b
eval -> n -> GE n
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (n -> n -> n
forall a. Integral a => a -> a -> a
div (Term n -> n
forall b. Term b -> b
eval Term n
evenx) n
2))
      (\ Term n
[var|somey|] -> [Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term n
evenx Term n -> Term n -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term n
somey Term n -> Term n -> Term n
forall a. Num a => a -> a -> a
+ Term n
somey])

sum3WithLength :: Integer -> Specification ([Int], Int, Int, Int)
sum3WithLength :: Integer -> Specification ([Int], Int, Int, Int)
sum3WithLength Integer
n =
  (Term ([Int], Int, Int, Int) -> Pred)
-> Specification ([Int], Int, Int, Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term ([Int], Int, Int, Int) -> Pred)
 -> Specification ([Int], Int, Int, Int))
-> (Term ([Int], Int, Int, Int) -> Pred)
-> Specification ([Int], Int, Int, Int)
forall a b. (a -> b) -> a -> b
$ \ Term ([Int], Int, Int, Int)
[var|quad|] ->
    Term ([Int], Int, Int, Int)
-> FunTy
     (MapList Term (ProductAsList ([Int], Int, Int, Int))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term ([Int], Int, Int, Int)
quad (FunTy (MapList Term (ProductAsList ([Int], Int, Int, Int))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList ([Int], Int, Int, Int))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term [Int]
[var|l|] Term Int
[var|n1|] Term Int
[var|n2|] Term Int
[var|n3|] ->
      [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term [Int] -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [Int]
l Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
n
      , Term [Int] -> (Term Int -> Term Bool) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
l ((Term Int -> Term Bool) -> Pred)
-> (Term Int -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var|item|] -> Term Int
item Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
0
      , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term [Int] -> Term Int
forall a. Foldy a => Term [a] -> Term a
sum_ Term [Int]
l Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
n1 Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
n2 Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
n3
      , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
n1 Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
n2 Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
n3 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n)
      ]

sum3 :: Specification [Int]
sum3 :: Specification [Int]
sum3 = (Term [Int] -> [Term Bool]) -> Specification [Int]
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term [Int] -> [Term Bool]) -> Specification [Int])
-> (Term [Int] -> [Term Bool]) -> Specification [Int]
forall a b. (a -> b) -> a -> b
$ \ Term [Int]
[var|xs|] -> [Term [Int] -> Term Int
forall a. Foldy a => Term [a] -> Term a
sum_ Term [Int]
xs Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
6 Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
9 Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
5, Term [Int] -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [Int]
xs Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
5]

listSumPair :: Numbery a => Specification [(a, Int)]
listSumPair :: forall a. Numbery a => Specification [(a, Int)]
listSumPair = (Term [(a, Int)] -> [Pred]) -> Specification [(a, Int)]
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term [(a, Int)] -> [Pred]) -> Specification [(a, Int)])
-> (Term [(a, Int)] -> [Pred]) -> Specification [(a, Int)]
forall a b. (a -> b) -> a -> b
$ \Term [(a, Int)]
xs ->
  [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ (Term (a, Int) -> Term a) -> Term [(a, Int)] -> Term a
forall a b.
(Foldy b, HasSpec a) =>
(Term a -> Term b) -> Term [a] -> Term b
foldMap_ Term (a, Int) -> Term a
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term [(a, Int)]
xs Term a -> Term a -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term a
100
  , Term [(a, Int)]
-> FunTy (MapList Term (Args (SimpleRep (a, Int)))) [Term Bool]
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
 HasSpec (SimpleRep a), HasSimpleRep a,
 All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
 HasSpec a, GenericRequires a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term [(a, Int)]
xs (FunTy (MapList Term (Args (SimpleRep (a, Int)))) [Term Bool]
 -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (a, Int)))) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term a
x Term Int
y -> [Term a
20 Term a -> Term a -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
x, Term a
x Term a -> Term a -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
30, Term Int
y Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
100]
  ]

listSumForall :: Numbery a => Specification [a]
listSumForall :: forall a. Numbery a => Specification [a]
listSumForall = (Term [a] -> [Pred]) -> Specification [a]
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term [a] -> [Pred]) -> Specification [a])
-> (Term [a] -> [Pred]) -> Specification [a]
forall a b. (a -> b) -> a -> b
$ \Term [a]
xs ->
  [ Term [a] -> (Term a -> Term Bool) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [a]
xs ((Term a -> Term Bool) -> Pred) -> (Term a -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term a
x -> Term a
1 Term a -> Term a -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
x
  , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term [a] -> Term a
forall a. Foldy a => Term [a] -> Term a
sum_ Term [a]
xs Term a -> Term a -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term a
20
  ]

-- | Complicated, because if 'a' is too large, the spec is unsatisfiable.
listSumComplex :: Numbery a => a -> Specification [a]
listSumComplex :: forall a. Numbery a => a -> Specification [a]
listSumComplex a
a = (Term [a] -> [Pred]) -> Specification [a]
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term [a] -> [Pred]) -> Specification [a])
-> (Term [a] -> [Pred]) -> Specification [a]
forall a b. (a -> b) -> a -> b
$ \Term [a]
xs ->
  [ Term [a] -> (Term a -> Term Bool) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [a]
xs ((Term a -> Term Bool) -> Pred) -> (Term a -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term a
x -> Term a
1 Term a -> Term a -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
x
  , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term [a] -> Term a
forall a. Foldy a => Term [a] -> Term a
sum_ Term [a]
xs Term a -> Term a -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term a
20
  , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term [a] -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [a]
xs Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
4
  , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term [a] -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [a]
xs Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
6
  , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term a -> Term [a] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ (a -> Term a
forall a. HasSpec a => a -> Term a
lit a
a) Term [a]
xs
  ]

-- ==============================================================
-- Tools for building properties that have good counterexamples

data Outcome = Succeed | Fail

propYes :: String -> Solution t -> Property
propYes :: forall t. String -> Solution t -> Property
propYes String
_ (Yes NonEmpty [t]
_) = Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
propYes String
msg (No [String]
xs) = Property -> Property
forall prop. Testable prop => prop -> Property
property (String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines (String
msg String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
xs)) Bool
False)

propNo :: Show t => String -> Solution t -> Property
propNo :: forall t. Show t => String -> Solution t -> Property
propNo String
msg (Yes ([t]
x :| [[t]]
_)) = Property -> Property
forall prop. Testable prop => prop -> Property
property (String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines [String
msg, String
"Expected to fail, but succeeds with", [t] -> String
forall a. Show a => a -> String
show [t]
x]) Bool
False)
propNo String
_ (No [String]
_) = Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True

parensList :: [String] -> String
parensList :: [String] -> String
parensList [String]
xs = Doc Any -> String
forall a. Show a => a -> String
show ([Doc Any] -> Doc Any
forall ann. [Doc ann] -> Doc ann
fillSep ([Doc Any] -> Doc Any) -> [Doc Any] -> Doc Any
forall a b. (a -> b) -> a -> b
$ Doc Any -> [Doc Any] -> [Doc Any]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc Any
forall ann. Doc ann
space ([Doc Any] -> [Doc Any]) -> [Doc Any] -> [Doc Any]
forall a b. (a -> b) -> a -> b
$ (String -> Doc Any) -> [String] -> [Doc Any]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc Any
forall a. IsString a => String -> a
fromString [String]
xs)

-- ===============================================================
-- Functions for building properties about the functions defined
-- in module Constrained.SumList(logish,pickAll)

logishProp :: Gen Property
logishProp :: Gen Property
logishProp = do
  Int
n <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (-Int
17, Int
17 :: Int) -- Any bigger or smaller is out of the range of Int
  Int
i <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int -> (Int, Int)
forall a. Integral a => a -> (a, a)
logRange Int
n)
  Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Int
forall t. Integral t => t -> t
logish Int
i Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Int
n)

picktest :: (Ord a, Num a) => a -> a -> (a -> Bool) -> a -> Int -> [a] -> Bool
picktest :: forall a.
(Ord a, Num a) =>
a -> a -> (a -> Bool) -> a -> Int -> [a] -> Bool
picktest a
smallest a
largest a -> Bool
p a
total Int
count [a]
ans =
  a
smallest a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
largest
    Bool -> Bool -> Bool
&& a
total a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> a
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [a]
ans
    Bool -> Bool -> Bool
&& Int
count Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ans
    Bool -> Bool -> Bool
&& (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all a -> Bool
p [a]
ans

-- | generate a different category of test, each time.
pickProp :: Gen Property
pickProp :: Gen Property
pickProp = do
  Int
smallest <- [Int] -> Gen Int
forall a. HasCallStack => [a] -> Gen a
elements [-Int
4, Int
1 :: Int]
  Int
count <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
2, Int
4)
  Int
total <- (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
20) (Int -> Int) -> Gen Int -> Gen Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
smallest, Int
5477)
  let largest :: Int
largest = Int
total Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
10
  (String
nam, Int -> Bool
p) <-
    [(String, Int -> Bool)] -> Gen (String, Int -> Bool)
forall a. HasCallStack => [a] -> Gen a
elements
      ( [[(String, Int -> Bool)]] -> [(String, Int -> Bool)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ if Int -> Bool
forall a. Integral a => a -> Bool
even Int
total then [(String
"even", Int -> Bool
forall a. Integral a => a -> Bool
even)] else []
          , if Int -> Bool
forall a. Integral a => a -> Bool
odd Int
total Bool -> Bool -> Bool
&& Int -> Bool
forall a. Integral a => a -> Bool
odd Int
count then [(String
"odd", Int -> Bool
forall a. Integral a => a -> Bool
odd)] else []
          , [(String
"(>0)", (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0)), (String
"true", Bool -> Int -> Bool
forall a b. a -> b -> a
const Bool
True)]
          ]
      )
  (Cost
_cost, Solution Int
ans) <- Int
-> Int
-> (String, Int -> Bool)
-> Int
-> Int
-> Cost
-> Gen (Cost, Solution Int)
forall t.
(Show t, Integral t, Random t) =>
t
-> t
-> (String, t -> Bool)
-> t
-> Int
-> Cost
-> Gen (Cost, Solution t)
pickAll Int
smallest Int
largest (String
nam, Int -> Bool
p) Int
total Int
count (Int -> Cost
Cost Int
0)
  case Solution Int
ans of
    Yes NonEmpty [Int]
result -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ ([Int] -> Bool) -> NonEmpty [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> Int -> (Int -> Bool) -> Int -> Int -> [Int] -> Bool
forall a.
(Ord a, Num a) =>
a -> a -> (a -> Bool) -> a -> Int -> [a] -> Bool
picktest Int
smallest Int
largest Int -> Bool
p Int
total Int
count) NonEmpty [Int]
result
    No [String]
msgs -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"predicate " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nam String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines [String]
msgs) Bool
False

-- | Build properties about calls to 'genListWithSize'
testFoldSpec ::
  forall a.
  (Foldy a, Random a, Integral a, TypeSpec a ~ NumSpec a, Arbitrary a, MaybeBounded a) =>
  Specification Integer ->
  Specification a ->
  Specification a ->
  Outcome ->
  Gen Property
testFoldSpec :: forall a.
(Foldy a, Random a, Integral a, TypeSpec a ~ NumSpec a,
 Arbitrary a, MaybeBounded a) =>
Specification Integer
-> Specification a -> Specification a -> Outcome -> Gen Property
testFoldSpec Specification Integer
size Specification a
elemSpec Specification a
total Outcome
outcome = do
  GE [a]
ans <- GenT GE (GE [a]) -> Gen (GE [a])
forall a. GenT GE a -> Gen a
genFromGenT (GenT GE (GE [a]) -> Gen (GE [a]))
-> GenT GE (GE [a]) -> Gen (GE [a])
forall a b. (a -> b) -> a -> b
$ GenT GE [a] -> GenT GE (GE [a])
forall (m :: * -> *) x.
MonadGenError m =>
GenT GE x -> GenT m (GE x)
inspect (GenT GE [a] -> GenT GE (GE [a]))
-> GenT GE [a] -> GenT GE (GE [a])
forall a b. (a -> b) -> a -> b
$ Specification Integer
-> Specification a -> Specification a -> GenT GE [a]
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
size Specification a
elemSpec Specification a
total
  let callString :: String
callString = [String] -> String
parensList [String
"GenListWithSize", Specification Integer -> String
forall a. Show a => a -> String
show Specification Integer
size, (String, a -> Bool) -> String
forall a b. (a, b) -> a
fst (Specification a -> (String, a -> Bool)
forall a. HasSpec a => Specification a -> (String, a -> Bool)
predSpecPair Specification a
elemSpec), Specification a -> String
forall a. Show a => a -> String
show Specification a
total]
      fails :: [a] -> String
fails [a]
xs = [String] -> String
unlines [String
callString, String
"Should fail, but it succeeds with", [a] -> String
forall a. Show a => a -> String
show [a]
xs]
      succeeds :: NonEmpty (NonEmpty String) -> String
succeeds NonEmpty (NonEmpty String)
xs =
        [String] -> String
unlines [String
callString, String
"Should succeed, but it fails with", NonEmpty (NonEmpty String) -> String
catMessages NonEmpty (NonEmpty String)
xs]
  case (GE [a]
ans, Outcome
outcome) of
    (Result [a]
_, Outcome
Succeed) -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
    (Result [a]
xs, Outcome
Fail) -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ([a] -> String
fails [a]
xs) Bool
False
    (FatalError NonEmpty (NonEmpty String)
_, Outcome
Fail) -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
    (FatalError NonEmpty (NonEmpty String)
xs, Outcome
Succeed) -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (NonEmpty (NonEmpty String) -> String
succeeds NonEmpty (NonEmpty String)
xs) Bool
False
    (GenError NonEmpty (NonEmpty String)
_, Outcome
Fail) -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
    (GenError NonEmpty (NonEmpty String)
xs, Outcome
Succeed) -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (NonEmpty (NonEmpty String) -> String
succeeds NonEmpty (NonEmpty String)
xs) Bool
False

-- | Generate a property from a call to 'pickAll'. We can test for success or failure using 'outcome'
sumProp ::
  (Integral t, Random t, HasSpec t) =>
  t ->
  t ->
  Specification t ->
  t ->
  Int ->
  Outcome ->
  Gen Property
sumProp :: forall t.
(Integral t, Random t, HasSpec t) =>
t -> t -> Specification t -> t -> Int -> Outcome -> Gen Property
sumProp t
smallest t
largest Specification t
spec t
total Int
count Outcome
outcome = t
-> t -> (String, t -> Bool) -> t -> Int -> Outcome -> Gen Property
forall t.
(Show t, Integral t, Random t) =>
t
-> t -> (String, t -> Bool) -> t -> Int -> Outcome -> Gen Property
sumProp2 t
smallest t
largest (Specification t -> (String, t -> Bool)
forall a. HasSpec a => Specification a -> (String, a -> Bool)
predSpecPair Specification t
spec) t
total Int
count Outcome
outcome

-- | Like SumProp, but instead of using a (Specification fn n) for the element predicate
--   It uses an explicit pair of a (String, n -> Bool). This means we can test things
--   using any Haskell function.
sumProp2 ::
  (Show t, Integral t, Random t) =>
  t ->
  t ->
  (String, t -> Bool) ->
  t ->
  Int ->
  Outcome ->
  Gen Property
sumProp2 :: forall t.
(Show t, Integral t, Random t) =>
t
-> t -> (String, t -> Bool) -> t -> Int -> Outcome -> Gen Property
sumProp2 t
smallest t
largest (String, t -> Bool)
spec t
total Int
count Outcome
outcome = do
  (Cost
_, Solution t
ans) <- 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, t -> Bool)
spec t
total Int
count (Int -> Cost
Cost Int
0)
  let callString :: String
callString = [String] -> String
parensList [String
"pickAll", t -> String
forall a. Show a => a -> String
show t
smallest, ((String, t -> Bool) -> String
forall a b. (a, b) -> a
fst (String, t -> Bool)
spec), t -> String
forall a. Show a => a -> String
show t
total, Int -> String
forall a. Show a => a -> String
show Int
count]
      message :: Outcome -> String
message Outcome
Succeed = String
"\nShould succeed, but it fails with"
      message Outcome
Fail = String
"\nShould fail, but it succeeds with " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Solution t -> String
forall a. Show a => a -> String
show Solution t
ans
  Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( case Outcome
outcome of
        Outcome
Succeed -> String -> Solution t -> Property
forall t. String -> Solution t -> Property
propYes (String
callString String -> String -> String
forall a. [a] -> [a] -> [a]
++ Outcome -> String
message Outcome
outcome) Solution t
ans
        Outcome
Fail -> String -> Solution t -> Property
forall t. Show t => String -> Solution t -> Property
propNo String
callString Solution t
ans
    )