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

module Constrained.Examples.List where

import Data.Word

import Constrained.API
import Constrained.Examples.Basic

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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term [a]
as ->
  Term a
10 forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. 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 = 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
  ]

listSumRange :: Numbery a => Specification [a]
listSumRange :: forall a. Numbery a => Specification [a]
listSumRange = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term [a]
xs ->
  let n :: Term a
n = forall a. Foldy a => Term [a] -> Term a
sum_ Term [a]
xs
   in [ 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
$ Term a
n forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
20
      , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term a
10 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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term [a]
xs ->
  let n :: Term a
n = 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.
      [ 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
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
12]
      , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term a
n forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
20
      , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term a
10 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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term [a]
xs ->
  let n :: Term a
n = forall a. Foldy a => Term [a] -> Term a
sum_ Term [a]
xs
   in [ 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, Term a
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
5]
      , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term a
n forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
20
      , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term a
10 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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term [a]
xs ->
  let n :: Term a
n = forall a. Foldy a => Term [a] -> Term a
sum_ Term [a]
xs
   in [ 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, Term a
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term a
5]
      , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term a
n forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` 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 = 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]
  ]

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

pairListError :: Specification [(Int, Int)]
pairListError :: Specification [(Int, Int)]
pairListError = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term [(Int, Int)]
ps ->
  [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Term [a] -> Term Integer
length_ Term [(Int, Int)]
ps forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
10
  , 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 [(Int, Int)]
ps forall a b. (a -> b) -> a -> b
$ \Term Int
a Term Int
b ->
      [ Term Int
a forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall a. HasSpec a => a -> Term a
lit [Int
1 .. Int
8]
      , Term Int
a forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
9
      , Term Int
b forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
a
      ]
  ]

listMustSizeIssue :: Specification [Int]
listMustSizeIssue :: Specification [Int]
listMustSizeIssue = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term [Int]
xs ->
  [ Term Int
1 forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` Term [Int]
xs
  , forall a. HasSpec a => Term [a] -> Term Integer
length_ Term [Int]
xs 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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term [Word64]
xs ->
  [ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Word64]
xs forall a b. (a -> b) -> a -> b
$ \Term Word64
x -> forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists forall a b. (a -> b) -> a -> b
$ \Term Word64
y -> Term Word64
y forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Word64
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 [Word64]
xs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit Word64
10
  ]

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

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

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

appendSingleton :: Specification Int
appendSingleton :: Specification Int
appendSingleton = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term Int
[var| x |] ->
  Term Int
10 forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall a. (Sized [a], HasSpec a) => Term a -> Term [a]
singletonList_ Term Int
x forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. forall a. HasSpec a => a -> Term a
lit [Int
1, Int
2, Int
3]

singletonSubset :: Specification Int
singletonSubset :: Specification Int
singletonSubset = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term Int
[var| x |] ->
  forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
fromList_ (forall a. (Sized [a], HasSpec a) => Term a -> Term [a]
singletonList_ Term Int
x) forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
fromList_ (forall a. HasSpec a => a -> Term a
lit [Int
1, Int
2, Int
3])

appendSuffix :: Specification ([Int], [Int])
appendSuffix :: Specification ([Int], [Int])
appendSuffix = 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, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$
  \ Term [Int]
[var|x|] Term [Int]
[var|y|] -> forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term [Int]
x forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term [Int]
y forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. forall a. HasSpec a => a -> Term a
lit [Int
4, Int
5, Int
6]

appendForAll :: Specification ([Int], [Int])
appendForAll :: Specification ([Int], [Int])
appendForAll = 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, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \ Term [Int]
[var| xs |] Term [Int]
[var| ys |] ->
  [ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
xs forall a b. (a -> b) -> a -> b
$ \Term Int
x -> Term Int
x forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall a. HasSpec a => a -> Term a
lit [Int
2, Int
4 .. Int
10]
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term [Int]
xs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term [Int]
ys forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. 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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term Int
[var| x |] ->
  forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
fromList_ (forall a. HasSpec a => a -> Term a
lit [Int
1, Int
2, Int
3]) forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
fromList_ (forall a. (Sized [a], HasSpec a) => Term a -> Term [a]
singletonList_ Term Int
x)

singletonErrorTooLong :: Specification Int
singletonErrorTooLong :: Specification Int
singletonErrorTooLong = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term Int
[var| x |] ->
  Term Integer
2 forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. forall a. HasSpec a => Term [a] -> Term Integer
length_ (forall a. (Sized [a], HasSpec a) => Term a -> Term [a]
singletonList_ Term Int
x)

appendTooLong :: Specification [Int]
appendTooLong :: Specification [Int]
appendTooLong = 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. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (forall a. HasSpec a => a -> Term a
lit [Int
1, Int
2, Int
3, Int
4] forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. Term [Int]
xs) 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 = 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, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$
  \ Term [Int]
[var|x|] Term [Int]
[var|y|] ->
    [ forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term [Int]
y Term [Int]
x
    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term [Int]
x forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit [Int
1, Int
2, Int
3] forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. Term [Int]
y
    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term [Int]
y forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit [Int
4, Int
5, Int
6]
    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term [Int]
x forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. 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 = 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, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \ Term [Int]
[var| xs |] Term [Int]
[var| ys |] Term [Int]
[var| zs |] ->
  [ Term [Int]
xs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit [Int
1, Int
2, Int
3] forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. Term [Int]
ys
  , Term [Int]
xs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit [Int
3, Int
4, Int
5] forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. Term [Int]
zs
  ]

overconstrainedSuffixes :: Specification ([Int], [Int], [Int])
overconstrainedSuffixes :: Specification ([Int], [Int], [Int])
overconstrainedSuffixes = 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, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \ Term [Int]
[var| xs |] Term [Int]
[var| ys |] Term [Int]
[var| zs |] ->
  [ Term [Int]
xs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term [Int]
ys forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. forall a. HasSpec a => a -> Term a
lit [Int
1, Int
2, Int
3]
  , Term [Int]
xs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term [Int]
zs forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. forall a. HasSpec a => a -> Term a
lit [Int
3, Int
4, Int
5]
  ]

appendForAllBad :: Specification ([Int], [Int])
appendForAllBad :: Specification ([Int], [Int])
appendForAllBad = 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, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \ Term [Int]
[var| xs |] Term [Int]
[var| ys |] ->
  [ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
xs forall a b. (a -> b) -> a -> b
$ \Term Int
x -> Term Int
x forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall a. HasSpec a => a -> Term a
lit [Int
1 .. Int
10]
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term [Int]
xs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term [Int]
ys forall a. HasSpec a => Term [a] -> Term [a] -> Term [a]
++. forall a. HasSpec a => a -> Term a
lit [Int
2, Int
4, Int
11]
  ]