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

module Constrained.Examples.Fold where

import Constrained
import Constrained.Base (Pred (..), genListWithSize, predSpecPair)
import Constrained.Examples.List (Numbery)
import Constrained.SumList
import Data.List.NonEmpty (NonEmpty ((:|)))
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 BaseFn Int
oddSpec :: Specification BaseFn Int
oddSpec = forall (fn :: [*] -> * -> *) a.
[String] -> Specification fn a -> Specification fn a
ExplainSpec [String
"odd via (y+y+1)"] forall a b. (a -> b) -> a -> b
$
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term BaseFn Int
[var|oddx|] ->
    forall a p (fn :: [*] -> * -> *).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists
      (\forall b.
Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  b
-> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Integral a => a -> a -> a
div (forall b.
Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  b
-> b
eval Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
oddx forall a. Num a => a -> a -> a
- Int
1) Int
2))
      (\ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
[var|y|] -> [forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Pred fn
Assert forall a b. (a -> b) -> a -> b
$ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
oddx forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y forall a. Num a => a -> a -> a
+ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y forall a. Num a => a -> a -> a
+ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
1])

evenSpec ::
  forall n.
  (TypeSpec BaseFn n ~ NumSpec BaseFn n, Integral n, HasSpec BaseFn n, MaybeBounded n) =>
  Specification BaseFn n
evenSpec :: forall n.
(TypeSpec BaseFn n ~ NumSpec BaseFn n, Integral n,
 HasSpec BaseFn n, MaybeBounded n) =>
Specification BaseFn n
evenSpec = forall (fn :: [*] -> * -> *) a.
[String] -> Specification fn a -> Specification fn a
ExplainSpec [String
"even via (x+x)"] forall a b. (a -> b) -> a -> b
$
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term BaseFn n
[var|evenx|] ->
    forall a p (fn :: [*] -> * -> *).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists
      (\forall b.
Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  b
-> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Integral a => a -> a -> a
div (forall b.
Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  b
-> b
eval Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  n
evenx) n
2))
      (\ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  n
[var|somey|] -> [forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Pred fn
Assert forall a b. (a -> b) -> a -> b
$ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  n
evenx forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  n
somey forall a. Num a => a -> a -> a
+ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  n
somey])

sum3WithLength :: Integer -> Specification BaseFn ([Int], Int, Int, Int)
sum3WithLength :: Integer -> Specification BaseFn ([Int], Int, Int, Int)
sum3WithLength Integer
n =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term BaseFn ([Int], Int, Int, Int)
[var|quad|] ->
    forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  ([Int], Int, Int, Int)
quad forall a b. (a -> b) -> a -> b
$ \ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  [Int]
[var|l|] Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
[var|n1|] Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
[var|n2|] Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
[var|n3|] ->
      [ forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Pred fn
Assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  [Int]
l forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Integer
n
      , forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  [Int]
l forall a b. (a -> b) -> a -> b
$ \ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
[var|item|] -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
item forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Int
0
      , forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Pred fn
Assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
Foldy fn a =>
Term fn [a] -> Term fn a
sum_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  [Int]
l forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
n1 forall a. Num a => a -> a -> a
+ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
n2 forall a. Num a => a -> a -> a
+ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
n3
      , forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Pred fn
Assert forall a b. (a -> b) -> a -> b
$ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
n1 forall a. Num a => a -> a -> a
+ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
n2 forall a. Num a => a -> a -> a
+ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
n3 forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall a. Num a => Integer -> a
fromInteger Integer
n)
      ]

sum3 :: Specification BaseFn [Int]
sum3 :: Specification BaseFn [Int]
sum3 = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term BaseFn [Int]
[var|xs|] -> [forall (fn :: [*] -> * -> *) a.
Foldy fn a =>
Term fn [a] -> Term fn a
sum_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  [Int]
xs forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Int
6 forall a. Num a => a -> a -> a
+ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Int
9 forall a. Num a => a -> a -> a
+ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Int
5, forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  [Int]
xs forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Integer
5]

listSumPair :: Numbery a => Specification BaseFn [(a, Int)]
listSumPair :: forall a. Numbery a => Specification BaseFn [(a, Int)]
listSumPair = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn [(a, Int)]
xs ->
  [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a b.
(Foldy fn b, HasSpec fn a) =>
(Term fn a -> Term fn b) -> Term fn [a] -> Term fn b
foldMap_ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn a
fst_ Term BaseFn [(a, Int)]
xs forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  a
100
  , forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term BaseFn [(a, Int)]
xs forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  a
x Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y -> [Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  a
20 forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  a
x, Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  a
x forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  a
30, Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
100]
  ]

listSumForall :: Numbery a => Specification BaseFn [a]
listSumForall :: forall a. Numbery a => Specification BaseFn [a]
listSumForall = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn [a]
xs ->
  [ forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term BaseFn [a]
xs forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  a
x -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  a
1 forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  a
x
  , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
Foldy fn a =>
Term fn [a] -> Term fn a
sum_ Term BaseFn [a]
xs forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  a
20
  ]

-- | Complicated, because if 'a' is too large, the spec is unsatisfiable.
listSumComplex :: Numbery a => a -> Specification BaseFn [a]
listSumComplex :: forall a. Numbery a => a -> Specification BaseFn [a]
listSumComplex a
a = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn [a]
xs ->
  [ forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term BaseFn [a]
xs forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  a
x -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  a
1 forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  a
x
  , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
Foldy fn a =>
Term fn [a] -> Term fn a
sum_ Term BaseFn [a]
xs forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  a
20
  , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term BaseFn [a]
xs forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Integer
4
  , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term BaseFn [a]
xs forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Integer
6
  , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
HasSpec fn a =>
Term fn a -> Term fn [a] -> Term fn Bool
elem_ (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit a
a) Term BaseFn [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 BaseFn a, Random a, Integral a, TypeSpec BaseFn a ~ NumSpec BaseFn a) =>
  Specification BaseFn Integer ->
  Specification BaseFn a ->
  Specification BaseFn a ->
  Outcome ->
  Gen Property
testFoldSpec :: forall a.
(Foldy BaseFn a, Random a, Integral a,
 TypeSpec BaseFn a ~ NumSpec BaseFn a) =>
Specification BaseFn Integer
-> Specification BaseFn a
-> Specification BaseFn a
-> Outcome
-> Gen Property
testFoldSpec Specification BaseFn Integer
size Specification BaseFn a
elemSpec Specification BaseFn 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 (fn :: [*] -> * -> *) a (m :: * -> *).
(Foldy fn a, MonadGenError m, Random a, Integral a,
 TypeSpec fn a ~ NumSpec fn a) =>
Specification fn Integer
-> Specification fn a -> Specification fn a -> GenT m [a]
genListWithSize Specification BaseFn Integer
size Specification BaseFn a
elemSpec Specification BaseFn a
total
  let callString :: String
callString = [String] -> String
parensList [String
"GenListWithSize", forall a. Show a => a -> String
show Specification BaseFn Integer
size, forall a b. (a, b) -> a
fst (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> (String, a -> Bool)
predSpecPair Specification BaseFn a
elemSpec), forall a. Show a => a -> String
show Specification BaseFn 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 BaseFn t) =>
  t -> t -> Specification BaseFn t -> t -> Int -> Outcome -> Gen Property
sumProp :: forall t.
(Integral t, Random t, HasSpec BaseFn t) =>
t
-> t
-> Specification BaseFn t
-> t
-> Int
-> Outcome
-> Gen Property
sumProp t
smallest t
largest Specification BaseFn 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 (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> (String, a -> Bool)
predSpecPair Specification BaseFn 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
    )