{-# 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
[ 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
]
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]
]
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
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]
]