{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ViewPatterns #-}

module Constrained.Examples.List where

import Constrained.API
import Constrained.Examples.Basic
import Data.Word

type Numbery a =
  ( Foldy a
  , OrdLike a
  , NumLike a
  , Ord a
  , Enum a
  )

listSum :: Numbery a => Specification [a]
listSum :: forall a. Numbery a => Specification [a]
listSum = (Term [a] -> Term Bool) -> Specification [a]
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term [a] -> Term Bool) -> Specification [a])
-> (Term [a] -> Term Bool) -> Specification [a]
forall a b. (a -> b) -> a -> b
$ \Term [a]
as ->
  Term a
10 Term a -> Term a -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term [a] -> Term a
forall a. Foldy a => Term [a] -> Term a
sum_ Term [a]
as

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
  ]

listSumRange :: Numbery a => Specification [a]
listSumRange :: forall a. Numbery a => Specification [a]
listSumRange = (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 ->
  let n :: Term a
n = Term [a] -> Term a
forall a. Foldy a => Term [a] -> Term a
sum_ Term [a]
xs
   in [ 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
n Term a -> Term a -> Term Bool
forall a. OrdLike 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
10 Term a -> Term a -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
n
      ]

listSumRangeUpper :: Numbery a => Specification [a]
listSumRangeUpper :: forall a. Numbery a => Specification [a]
listSumRangeUpper = (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 ->
  let n :: Term a
n = Term [a] -> Term a
forall a. Foldy a => Term [a] -> Term a
sum_ Term [a]
xs
   in -- All it takes is one big negative number,
      -- then we can't get enough small ones to exceed 10
      -- in the number of tries allowed.
      -- So we make x relatively large ( <. 12), If its is
      -- relatively small ( <. 5), we can get unlucky.
      [ 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
x Term a -> Term a -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
12]
      , 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
n Term a -> Term a -> Term Bool
forall a. OrdLike 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
10 Term a -> Term a -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
n
      ]

listSumRangeRange :: Numbery a => Specification [a]
listSumRangeRange :: forall a. Numbery a => Specification [a]
listSumRangeRange = (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 ->
  let n :: Term a
n = Term [a] -> Term a
forall a. Foldy a => Term [a] -> Term a
sum_ Term [a]
xs
   in [ 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 a
x Term a -> Term a -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
5]
      , 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
n Term a -> Term a -> Term Bool
forall a. OrdLike 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
10 Term a -> Term a -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
n
      ]

listSumElemRange :: Numbery a => Specification [a]
listSumElemRange :: forall a. Numbery a => Specification [a]
listSumElemRange = (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 ->
  let n :: Term a
n = Term [a] -> Term a
forall a. Foldy a => Term [a] -> Term a
sum_ Term [a]
xs
   in [ 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 a
x Term a -> Term a -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
5]
      , 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
n 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
10, a
12 .. a
20]
      ]

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),
 IsProductType a, HasSpec a, GenericRequires a,
 ProdAsListComputes 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]
  ]

listEmpty :: Specification [Int]
listEmpty :: Specification [Int]
listEmpty = (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]
xs ->
  [ Term [Int] -> (Term Int -> Bool) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
xs ((Term Int -> Bool) -> Pred) -> (Term Int -> Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> Bool
False
  , 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 => Term [a] -> Term Integer
length_ Term [Int]
xs Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
10
  ]

pairListError :: Specification [(Int, Int)]
pairListError :: Specification [(Int, Int)]
pairListError = (Term [(Int, Int)] -> [Pred]) -> Specification [(Int, Int)]
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term [(Int, Int)] -> [Pred]) -> Specification [(Int, Int)])
-> (Term [(Int, Int)] -> [Pred]) -> Specification [(Int, Int)]
forall a b. (a -> b) -> a -> b
$ \Term [(Int, Int)]
ps ->
  [ 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, Int)] -> Term Integer
forall a. HasSpec a => Term [a] -> Term Integer
length_ Term [(Int, Int)]
ps Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
10
  , Term [(Int, Int)]
-> FunTy (MapList Term (Args (SimpleRep (Int, 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),
 IsProductType a, HasSpec a, GenericRequires a,
 ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term [(Int, Int)]
ps (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
 -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
a Term Int
b ->
      [ Term Int
a Term Int -> Term [Int] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` [Int] -> Term [Int]
forall a. HasSpec a => a -> Term a
lit [Int
1 .. Int
8]
      , Term Int
a Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
9
      , Term Int
b Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
a
      ]
  ]

listMustSizeIssue :: Specification [Int]
listMustSizeIssue :: Specification [Int]
listMustSizeIssue = (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]
xs ->
  [ Term Int
1 Term Int -> Term [Int] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` Term [Int]
xs
  , Term [Int] -> Term Integer
forall a. HasSpec a => Term [a] -> Term Integer
length_ Term [Int]
xs Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
1
  ]

-- FIX ME, generates but the unsafeExists means it is unsound
sumListBad :: Specification [Word64]
sumListBad :: Specification [Word64]
sumListBad = (Term [Word64] -> [Pred]) -> Specification [Word64]
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term [Word64] -> [Pred]) -> Specification [Word64])
-> (Term [Word64] -> [Pred]) -> Specification [Word64]
forall a b. (a -> b) -> a -> b
$ \Term [Word64]
xs ->
  [ Term [Word64] -> (Term Word64 -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Word64]
xs ((Term Word64 -> Pred) -> Pred) -> (Term Word64 -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Word64
x -> (Term Word64 -> Term Bool) -> Pred
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists ((Term Word64 -> Term Bool) -> Pred)
-> (Term Word64 -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Word64
y -> Term Word64
y Term Word64 -> Term Word64 -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Word64
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 [Word64] -> Term Word64
forall a. Foldy a => Term [a] -> Term a
sum_ Term [Word64]
xs Term Word64 -> Term Word64 -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Word64 -> Term Word64
forall a. HasSpec a => a -> Term a
lit Word64
10
  ]

listExistsUnfree :: Specification [Int]
listExistsUnfree :: Specification [Int]
listExistsUnfree = (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]
xs ->
  [ Term [Int] -> (Term Int -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
xs ((Term Int -> Pred) -> Pred) -> (Term Int -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
x -> Term Int
x Term Int -> Specification Int -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification Int
existsUnfree
  , 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]
xs Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
3
  ]

listSumShort :: Specification [Int]
listSumShort :: Specification [Int]
listSumShort = (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| 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 [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. OrdLike a => Term a -> Term a -> Term Bool
<=. Term 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 [Int] -> Term Int
forall a. Foldy a => Term [a] -> Term a
sum_ Term [Int]
xs Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
100000
  , Term [Int] -> (Term Int -> [Pred]) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
xs ((Term Int -> [Pred]) -> Pred) -> (Term Int -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var| x |] ->
      [ ((forall b. Term b -> b) -> GE Bool) -> (Term Bool -> Pred) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (GE Bool -> (forall b. Term b -> b) -> GE Bool
forall a b. a -> b -> a
const (GE Bool -> (forall b. Term b -> b) -> GE Bool)
-> GE Bool -> (forall b. Term b -> b) -> GE Bool
forall a b. (a -> b) -> a -> b
$ Bool -> GE Bool
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) ((Term Bool -> Pred) -> Pred) -> (Term Bool -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Bool
b ->
          Term Bool -> Term Bool -> Pred
forall p. IsPred p => Term Bool -> p -> Pred
whenTrue Term Bool
b (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
10000000
      ]
  ]

appendSize :: Specification ([Int], [Int])
appendSize :: Specification ([Int], [Int])
appendSize = FunTy (MapList Term (Args (SimpleRep ([Int], [Int])))) [Pred]
-> Specification ([Int], [Int])
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy (MapList Term (Args (SimpleRep ([Int], [Int])))) [Pred]
 -> Specification ([Int], [Int]))
-> FunTy (MapList Term (Args (SimpleRep ([Int], [Int])))) [Pred]
-> Specification ([Int], [Int])
forall a b. (a -> b) -> a -> b
$ \ Term [Int]
[var| xs |] Term [Int]
[var| ys |] ->
  [ 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]
xs Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
10
  , 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]
ys Term [Int] -> Term [Int] -> Term [Int]
forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. Term [Int]
xs) Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
15
  ]

appendSingleton :: Specification Int
appendSingleton :: Specification Int
appendSingleton = (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| x |] ->
  Term Int
10 Term Int -> Term [Int] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` Term Int -> Term [Int]
forall a. (Sized [a], HasSpec a) => Term a -> Term [a]
singletonList_ Term Int
x Term [Int] -> Term [Int] -> Term [Int]
forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. [Int] -> Term [Int]
forall a. HasSpec a => a -> Term a
lit [Int
1, Int
2, Int
3]

singletonSubset :: Specification Int
singletonSubset :: Specification Int
singletonSubset = (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| x |] ->
  Term [Int] -> Term (Set Int)
forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
fromList_ (Term Int -> Term [Int]
forall a. (Sized [a], HasSpec a) => Term a -> Term [a]
singletonList_ Term Int
x) Term (Set Int) -> Term (Set Int) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Term [Int] -> Term (Set Int)
forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
fromList_ ([Int] -> Term [Int]
forall a. HasSpec a => a -> Term a
lit [Int
1, Int
2, Int
3])

appendSuffix :: Specification ([Int], [Int])
appendSuffix :: Specification ([Int], [Int])
appendSuffix = FunTy (MapList Term (Args (SimpleRep ([Int], [Int])))) Pred
-> Specification ([Int], [Int])
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy (MapList Term (Args (SimpleRep ([Int], [Int])))) Pred
 -> Specification ([Int], [Int]))
-> FunTy (MapList Term (Args (SimpleRep ([Int], [Int])))) Pred
-> Specification ([Int], [Int])
forall a b. (a -> b) -> a -> b
$
  \ Term [Int]
[var|x|] 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]
x 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. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. [Int] -> Term [Int]
forall a. HasSpec a => a -> Term a
lit [Int
4, Int
5, Int
6]

appendForAll :: Specification ([Int], [Int])
appendForAll :: Specification ([Int], [Int])
appendForAll = FunTy (MapList Term (Args (SimpleRep ([Int], [Int])))) [Pred]
-> Specification ([Int], [Int])
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy (MapList Term (Args (SimpleRep ([Int], [Int])))) [Pred]
 -> Specification ([Int], [Int]))
-> FunTy (MapList Term (Args (SimpleRep ([Int], [Int])))) [Pred]
-> Specification ([Int], [Int])
forall a b. (a -> b) -> a -> b
$ \ Term [Int]
[var| xs |] Term [Int]
[var| ys |] ->
  [ 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]
xs ((Term Int -> Term Bool) -> Pred)
-> (Term Int -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
x -> Term Int
x Term Int -> Term [Int] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` [Int] -> Term [Int]
forall a. HasSpec a => a -> Term a
lit [Int
2, Int
4 .. Int
10]
  , 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]
xs Term [Int] -> Term [Int] -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term [Int]
ys Term [Int] -> Term [Int] -> Term [Int]
forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. [Int] -> Term [Int]
forall a. HasSpec a => a -> Term a
lit [Int
2, Int
4, Int
6]
  ]

-- Some notable error cases that shouldn't succeed

singletonErrorTooMany :: Specification Int
singletonErrorTooMany :: Specification Int
singletonErrorTooMany = (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| x |] ->
  Term [Int] -> Term (Set Int)
forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
fromList_ ([Int] -> Term [Int]
forall a. HasSpec a => a -> Term a
lit [Int
1, Int
2, Int
3]) Term (Set Int) -> Term (Set Int) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Term [Int] -> Term (Set Int)
forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
fromList_ (Term Int -> Term [Int]
forall a. (Sized [a], HasSpec a) => Term a -> Term [a]
singletonList_ Term Int
x)

singletonErrorTooLong :: Specification Int
singletonErrorTooLong :: Specification Int
singletonErrorTooLong = (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| x |] ->
  Term Integer
2 Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term [Int] -> Term Integer
forall a. HasSpec a => Term [a] -> Term Integer
length_ (Term Int -> Term [Int]
forall a. (Sized [a], HasSpec a) => Term a -> Term [a]
singletonList_ Term Int
x)

appendTooLong :: Specification [Int]
appendTooLong :: Specification [Int]
appendTooLong = (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 Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ ([Int] -> Term [Int]
forall a. HasSpec a => a -> Term a
lit [Int
1, Int
2, Int
3, Int
4] Term [Int] -> Term [Int] -> Term [Int]
forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. Term [Int]
xs) Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
3

-- | Fails because the cant set is over constrained
overconstrainedAppend :: Specification ([Int], [Int])
overconstrainedAppend :: Specification ([Int], [Int])
overconstrainedAppend = FunTy (MapList Term (Args (SimpleRep ([Int], [Int])))) [Pred]
-> Specification ([Int], [Int])
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy (MapList Term (Args (SimpleRep ([Int], [Int])))) [Pred]
 -> Specification ([Int], [Int]))
-> FunTy (MapList Term (Args (SimpleRep ([Int], [Int])))) [Pred]
-> Specification ([Int], [Int])
forall a b. (a -> b) -> a -> b
$
  \ Term [Int]
[var|x|] Term [Int]
[var|y|] ->
    [ Term [Int] -> Term [Int] -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term [Int]
y Term [Int]
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 [Int]
x 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
1, Int
2, Int
3] Term [Int] -> Term [Int] -> Term [Int]
forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. Term [Int]
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]
y 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
4, Int
5, Int
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 [Int]
x 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
1, Int
2, Int
3, Int
4, Int
5, Int
6]
    ]

overconstrainedPrefixes :: Specification ([Int], [Int], [Int])
overconstrainedPrefixes :: Specification ([Int], [Int], [Int])
overconstrainedPrefixes = FunTy
  (MapList Term (Args (SimpleRep ([Int], [Int], [Int])))) [Term Bool]
-> Specification ([Int], [Int], [Int])
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep ([Int], [Int], [Int])))) [Term Bool]
 -> Specification ([Int], [Int], [Int]))
-> FunTy
     (MapList Term (Args (SimpleRep ([Int], [Int], [Int])))) [Term Bool]
-> Specification ([Int], [Int], [Int])
forall a b. (a -> b) -> a -> b
$ \ Term [Int]
[var| xs |] Term [Int]
[var| ys |] Term [Int]
[var| zs |] ->
  [ 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
1, Int
2, Int
3] Term [Int] -> Term [Int] -> Term [Int]
forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. Term [Int]
ys
  , 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
3, Int
4, Int
5] Term [Int] -> Term [Int] -> Term [Int]
forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. Term [Int]
zs
  ]

overconstrainedSuffixes :: Specification ([Int], [Int], [Int])
overconstrainedSuffixes :: Specification ([Int], [Int], [Int])
overconstrainedSuffixes = FunTy
  (MapList Term (Args (SimpleRep ([Int], [Int], [Int])))) [Term Bool]
-> Specification ([Int], [Int], [Int])
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep ([Int], [Int], [Int])))) [Term Bool]
 -> Specification ([Int], [Int], [Int]))
-> FunTy
     (MapList Term (Args (SimpleRep ([Int], [Int], [Int])))) [Term Bool]
-> Specification ([Int], [Int], [Int])
forall a b. (a -> b) -> a -> b
$ \ Term [Int]
[var| xs |] Term [Int]
[var| ys |] Term [Int]
[var| zs |] ->
  [ Term [Int]
xs Term [Int] -> Term [Int] -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term [Int]
ys Term [Int] -> Term [Int] -> Term [Int]
forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. [Int] -> Term [Int]
forall a. HasSpec a => a -> Term a
lit [Int
1, Int
2, Int
3]
  , Term [Int]
xs Term [Int] -> Term [Int] -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term [Int]
zs Term [Int] -> Term [Int] -> Term [Int]
forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. [Int] -> Term [Int]
forall a. HasSpec a => a -> Term a
lit [Int
3, Int
4, Int
5]
  ]

appendForAllBad :: Specification ([Int], [Int])
appendForAllBad :: Specification ([Int], [Int])
appendForAllBad = FunTy (MapList Term (Args (SimpleRep ([Int], [Int])))) [Pred]
-> Specification ([Int], [Int])
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy (MapList Term (Args (SimpleRep ([Int], [Int])))) [Pred]
 -> Specification ([Int], [Int]))
-> FunTy (MapList Term (Args (SimpleRep ([Int], [Int])))) [Pred]
-> Specification ([Int], [Int])
forall a b. (a -> b) -> a -> b
$ \ Term [Int]
[var| xs |] Term [Int]
[var| ys |] ->
  [ 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]
xs ((Term Int -> Term Bool) -> Pred)
-> (Term Int -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
x -> Term Int
x Term Int -> Term [Int] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` [Int] -> Term [Int]
forall a. HasSpec a => a -> Term a
lit [Int
1 .. Int
10]
  , 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]
xs Term [Int] -> Term [Int] -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term [Int]
ys Term [Int] -> Term [Int] -> Term [Int]
forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. [Int] -> Term [Int]
forall a. HasSpec a => a -> Term a
lit [Int
2, Int
4, Int
11]
  ]