{-# 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 = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String
"odd via (y+y+1)"] forall a b. (a -> b) -> a -> b
$
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term Int
[var|oddx|] ->
    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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Integral a => a -> a -> a
div (forall b. Term b -> b
eval Term Int
oddx forall a. Num a => a -> a -> a
- Int
1) Int
2))
      (\ Term Int
[var|y|] -> [Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ Term Int
oddx forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
y forall a. Num a => a -> a -> a
+ Term Int
y 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 = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String
"even via (x+x)"] forall a b. (a -> b) -> a -> b
$
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term n
[var|evenx|] ->
    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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Integral a => a -> a -> a
div (forall b. Term b -> b
eval Term n
evenx) n
2))
      (\ Term n
[var|somey|] -> [Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ Term n
evenx forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term n
somey 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 =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term ([Int], Int, Int, Int)
[var|quad|] ->
    forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term ([Int], Int, Int, Int)
quad 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
Assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [Int]
l forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit Integer
n
      , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
l forall a b. (a -> b) -> a -> b
$ \ Term Int
[var|item|] -> Term Int
item forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. forall a. HasSpec a => a -> Term a
lit Int
0
      , Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ forall a. Foldy a => Term [a] -> Term a
sum_ Term [Int]
l forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
n1 forall a. Num a => a -> a -> a
+ Term Int
n2 forall a. Num a => a -> a -> a
+ Term Int
n3
      , Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ Term Int
n1 forall a. Num a => a -> a -> a
+ Term Int
n2 forall a. Num a => a -> a -> a
+ Term Int
n3 forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. forall a. HasSpec a => a -> Term a
lit (forall a. Num a => Integer -> a
fromInteger Integer
n)
      ]

sum3 :: Specification [Int]
sum3 :: Specification [Int]
sum3 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term [Int]
[var|xs|] -> [forall a. Foldy a => Term [a] -> Term a
sum_ Term [Int]
xs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit Int
6 forall a. Num a => a -> a -> a
+ forall a. HasSpec a => a -> Term a
lit Int
9 forall a. Num a => a -> a -> a
+ forall a. HasSpec a => a -> Term a
lit Int
5, forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [Int]
xs 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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term [(a, Int)]
xs ->
  [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a b.
(Foldy b, HasSpec a) =>
(Term a -> Term b) -> Term [a] -> Term b
foldMap_ forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term [(a, Int)]
xs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term a
100
  , 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) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term [(a, Int)]
xs forall a b. (a -> b) -> a -> b
$ \Term a
x Term Int
y -> [Term a
20 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
x, Term a
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
30, Term Int
y 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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term [a]
xs ->
  [ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [a]
xs forall a b. (a -> b) -> a -> b
$ \Term a
x -> Term a
1 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
x
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. Foldy a => Term [a] -> Term a
sum_ Term [a]
xs 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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term [a]
xs ->
  [ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [a]
xs forall a b. (a -> b) -> a -> b
$ \Term a
x -> Term a
1 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
x
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. Foldy a => Term [a] -> Term a
sum_ Term [a]
xs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term a
20
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [a]
xs forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. forall a. HasSpec a => a -> Term a
lit Integer
4
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [a]
xs forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. forall a. HasSpec a => a -> Term a
lit Integer
6
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ (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]
_) = forall prop. Testable prop => prop -> Property
property Bool
True
propYes String
msg (No [String]
xs) = forall prop. Testable prop => prop -> Property
property (forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines (String
msg 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]]
_)) = forall prop. Testable prop => prop -> Property
property (forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines [String
msg, String
"Expected to fail, but succeeds with", forall a. Show a => a -> String
show [t]
x]) Bool
False)
propNo String
_ (No [String]
_) = forall prop. Testable prop => prop -> Property
property Bool
True

parensList :: [String] -> String
parensList :: [String] -> String
parensList [String]
xs = forall a. Show a => a -> String
show (forall ann. [Doc ann] -> Doc ann
fillSep forall a b. (a -> b) -> a -> b
$ forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate forall ann. Doc ann
space forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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 <- 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 <- forall a. Random a => (a, a) -> Gen a
choose (forall a. Integral a => a -> (a, a)
logRange Int
n)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall t. Integral t => t -> t
logish Int
i 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 forall a. Ord a => a -> a -> Bool
<= a
largest
    Bool -> Bool -> Bool
&& a
total forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [a]
ans
    Bool -> Bool -> Bool
&& Int
count forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ans
    Bool -> Bool -> 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 <- forall a. HasCallStack => [a] -> Gen a
elements [-Int
4, Int
1 :: Int]
  Int
count <- forall a. Random a => (a, a) -> Gen a
choose (Int
2, Int
4)
  Int
total <- (forall a. Num a => a -> a -> a
+ Int
20) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Int
smallest, Int
5477)
  let largest :: Int
largest = Int
total forall a. Num a => a -> a -> a
+ Int
10
  (String
nam, Int -> Bool
p) <-
    forall a. HasCallStack => [a] -> Gen a
elements
      ( forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ if forall a. Integral a => a -> Bool
even Int
total then [(String
"even", forall a. Integral a => a -> Bool
even)] else []
          , if forall a. Integral a => a -> Bool
odd Int
total Bool -> Bool -> Bool
&& forall a. Integral a => a -> Bool
odd Int
count then [(String
"odd", forall a. Integral a => a -> Bool
odd)] else []
          , [(String
"(>0)", (forall a. Ord a => a -> a -> Bool
> Int
0)), (String
"true", forall a b. a -> b -> a
const Bool
True)]
          ]
      )
  (Cost
_cost, Solution Int
ans) <- 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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample (String
"predicate " forall a. [a] -> [a] -> [a]
++ String
nam forall a. [a] -> [a] -> [a]
++ String
"\n" 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 <- forall a. GenT GE a -> Gen a
genFromGenT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) x.
MonadGenError m =>
GenT GE x -> GenT m (GE x)
inspect forall a b. (a -> b) -> a -> b
$ 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", forall a. Show a => a -> String
show Specification Integer
size, forall a b. (a, b) -> a
fst (forall a. HasSpec a => Specification a -> (String, a -> Bool)
predSpecPair Specification a
elemSpec), 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", 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) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property Bool
True
    (Result [a]
xs, Outcome
Fail) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample ([a] -> String
fails [a]
xs) Bool
False
    (FatalError NonEmpty (NonEmpty String)
_, Outcome
Fail) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property Bool
True
    (FatalError NonEmpty (NonEmpty String)
xs, Outcome
Succeed) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property Bool
True
    (GenError NonEmpty (NonEmpty String)
xs, Outcome
Succeed) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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 = forall t.
(Show t, Integral t, Random t) =>
t
-> t -> (String, t -> Bool) -> t -> Int -> Outcome -> Gen Property
sumProp2 t
smallest t
largest (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) <- 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", forall a. Show a => a -> String
show t
smallest, (forall a b. (a, b) -> a
fst (String, t -> Bool)
spec), forall a. Show a => a -> String
show t
total, 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 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Solution t
ans
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( case Outcome
outcome of
        Outcome
Succeed -> forall t. String -> Solution t -> Property
propYes (String
callString forall a. [a] -> [a] -> [a]
++ Outcome -> String
message Outcome
outcome) Solution t
ans
        Outcome
Fail -> forall t. Show t => String -> Solution t -> Property
propNo String
callString Solution t
ans
    )