{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
module Constrained.Examples.Set where
import Constrained.API
import Constrained.Base (Forallable)
import Constrained.Examples.Basic
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Typeable
import GHC.Generics
setPairSpec :: Specification (Set Int, Set Int)
setPairSpec :: Specification (Set Int, Set Int)
setPairSpec = FunTy (MapList Term (Args (SimpleRep (Set Int, Set Int)))) Pred
-> Specification (Set Int, Set 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 (Set Int, Set Int)))) Pred
-> Specification (Set Int, Set Int))
-> FunTy (MapList Term (Args (SimpleRep (Set Int, Set Int)))) Pred
-> Specification (Set Int, Set Int)
forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
s Term (Set Int)
s' ->
Term (Set Int) -> (Term Int -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set Int)
s ((Term Int -> Pred) -> Pred) -> (Term Int -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
x ->
Term (Set Int) -> (Term Int -> Term Bool) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set Int)
s' ((Term Int -> Term Bool) -> Pred)
-> (Term Int -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
y ->
Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
y
fixedSetSpec :: Specification (Set Int)
fixedSetSpec :: Specification (Set Int)
fixedSetSpec = (Term (Set Int) -> Pred) -> Specification (Set Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set Int) -> Pred) -> Specification (Set Int))
-> (Term (Set Int) -> Pred) -> Specification (Set Int)
forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
s ->
Term (Set Int) -> (Term Int -> [Term Bool]) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set Int)
s ((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. OrdLike a => Term a -> Term a -> Term Bool
<=. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit (Int
i :: Int) | Int
i <- [Int
1 .. Int
3]]
setOfPairLetSpec :: Specification (Set (Int, Int))
setOfPairLetSpec :: Specification (Set (Int, Int))
setOfPairLetSpec = (Term (Set (Int, Int)) -> Pred) -> Specification (Set (Int, Int))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set (Int, Int)) -> Pred) -> Specification (Set (Int, Int)))
-> (Term (Set (Int, Int)) -> Pred)
-> Specification (Set (Int, Int))
forall a b. (a -> b) -> a -> b
$ \Term (Set (Int, Int))
ps ->
Term (Set (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 (Set (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
x Term Int
y ->
Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
y
setSingletonSpec :: Specification (Set (Int, Int))
setSingletonSpec :: Specification (Set (Int, Int))
setSingletonSpec = (Term (Set (Int, Int)) -> Pred) -> Specification (Set (Int, Int))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set (Int, Int)) -> Pred) -> Specification (Set (Int, Int)))
-> (Term (Set (Int, Int)) -> Pred)
-> Specification (Set (Int, Int))
forall a b. (a -> b) -> a -> b
$ \Term (Set (Int, Int))
ps ->
Term (Set (Int, Int)) -> (Term (Int, Int) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Int, Int))
ps ((Term (Int, Int) -> Pred) -> Pred)
-> (Term (Int, Int) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p ->
Term (Set Int) -> (Term Int -> Term Bool) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term Int -> Term (Set Int)
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a)
singleton_ (Term (Int, Int) -> Term Int
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (Int, Int)
p)) ((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. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
10
eitherSimpleSetSpec :: Specification (Set (Either Int Int))
eitherSimpleSetSpec :: Specification (Set (Either Int Int))
eitherSimpleSetSpec = (Term (Set (Either Int Int)) -> Pred)
-> Specification (Set (Either Int Int))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set (Either Int Int)) -> Pred)
-> Specification (Set (Either Int Int)))
-> (Term (Set (Either Int Int)) -> Pred)
-> Specification (Set (Either Int Int))
forall a b. (a -> b) -> a -> b
$ \Term (Set (Either Int Int))
ss ->
Term (Set (Either Int Int))
-> (Term (Either Int Int) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Either Int Int))
ss ((Term (Either Int Int) -> Pred) -> Pred)
-> (Term (Either Int Int) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
s ->
(Term (Either Int Int)
-> FunTy
(MapList
(Weighted (BinderD Deps)) (Cases (SimpleRep (Either Int Int))))
Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
(MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (Either Int Int)
s)
(FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
a -> Term Int
a Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
0)
(FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
b -> Term Int
0 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
b)
forAllAnySpec :: Specification (Set Int)
forAllAnySpec :: Specification (Set Int)
forAllAnySpec = (Term (Set Int) -> Pred) -> Specification (Set Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set Int) -> Pred) -> Specification (Set Int))
-> (Term (Set Int) -> Pred) -> Specification (Set Int)
forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
as ->
Term (Set Int) -> (Term Int -> Bool) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set Int)
as ((Term Int -> Bool) -> Pred) -> (Term Int -> Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> Bool
True
maybeJustSetSpec :: Specification (Set (Maybe Int))
maybeJustSetSpec :: Specification (Set (Maybe Int))
maybeJustSetSpec = (Term (Set (Maybe Int)) -> Pred) -> Specification (Set (Maybe Int))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set (Maybe Int)) -> Pred)
-> Specification (Set (Maybe Int)))
-> (Term (Set (Maybe Int)) -> Pred)
-> Specification (Set (Maybe Int))
forall a b. (a -> b) -> a -> b
$ \Term (Set (Maybe Int))
ms ->
Term (Set (Maybe Int)) -> (Term (Maybe Int) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Maybe Int))
ms ((Term (Maybe Int) -> Pred) -> Pred)
-> (Term (Maybe Int) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Maybe Int)
m ->
(Term (Maybe Int)
-> FunTy
(MapList (Weighted (BinderD Deps)) (Cases (SimpleRep (Maybe Int))))
Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
(MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (Maybe Int)
m)
(FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
False)
(FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
y -> Term Int
0 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
y)
notSubsetSpec :: Specification (Set Int, Set Int)
notSubsetSpec :: Specification (Set Int, Set Int)
notSubsetSpec = FunTy
(MapList Term (Args (SimpleRep (Set Int, Set Int)))) (Term Bool)
-> Specification (Set Int, Set 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 (Set Int, Set Int)))) (Term Bool)
-> Specification (Set Int, Set Int))
-> FunTy
(MapList Term (Args (SimpleRep (Set Int, Set Int)))) (Term Bool)
-> Specification (Set Int, Set Int)
forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
s Term (Set Int)
s' -> Term Bool -> Term Bool
not_ (Term Bool -> Term Bool) -> Term Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term (Set Int) -> Term (Set Int) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ Term (Set Int)
s Term (Set Int)
s'
emptyEitherMemberSpec :: Specification (Set (Either Int Int))
emptyEitherMemberSpec :: Specification (Set (Either Int Int))
emptyEitherMemberSpec = (Term (Set (Either Int Int)) -> Pred)
-> Specification (Set (Either Int Int))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set (Either Int Int)) -> Pred)
-> Specification (Set (Either Int Int)))
-> (Term (Set (Either Int Int)) -> Pred)
-> Specification (Set (Either Int Int))
forall a b. (a -> b) -> a -> b
$ \Term (Set (Either Int Int))
s ->
Term (Set (Either Int Int))
-> (Term (Either Int Int) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Either Int Int))
s ((Term (Either Int Int) -> Pred) -> Pred)
-> (Term (Either Int Int) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
x ->
(Term (Either Int Int)
-> FunTy
(MapList
(Weighted (BinderD Deps)) (Cases (SimpleRep (Either Int Int))))
Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
(MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (Either Int Int)
x)
(FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
l -> Term Int -> Term (Set Int) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term Int
l Term (Set Int)
forall a. Monoid a => a
mempty)
(FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
r -> Term Int -> Term (Set Int) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term Int
r Term (Set Int)
forall a. Monoid a => a
mempty)
emptyEitherSpec :: Specification (Set (Either Int Int))
emptyEitherSpec :: Specification (Set (Either Int Int))
emptyEitherSpec = (Term (Set (Either Int Int)) -> Pred)
-> Specification (Set (Either Int Int))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set (Either Int Int)) -> Pred)
-> Specification (Set (Either Int Int)))
-> (Term (Set (Either Int Int)) -> Pred)
-> Specification (Set (Either Int Int))
forall a b. (a -> b) -> a -> b
$ \Term (Set (Either Int Int))
s ->
Term (Set (Either Int Int))
-> (Term (Either Int Int) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Either Int Int))
s ((Term (Either Int Int) -> Pred) -> Pred)
-> (Term (Either Int Int) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
x ->
(Term (Either Int Int)
-> FunTy
(MapList
(Weighted (BinderD Deps)) (Cases (SimpleRep (Either Int Int))))
Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
(MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (Either Int Int)
x)
(FunTy (MapList Term (Args Int)) Bool -> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) Bool
-> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) Bool
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> Bool
False)
(FunTy (MapList Term (Args Int)) Bool -> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) Bool
-> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) Bool
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> Bool
False)
notSubset :: Specification (Set Int)
notSubset :: Specification (Set Int)
notSubset = (Term (Set Int) -> Term Bool) -> Specification (Set Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set Int) -> Term Bool) -> Specification (Set Int))
-> (Term (Set Int) -> Term Bool) -> Specification (Set Int)
forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
s ->
Term Bool -> Term Bool
not_ (Term Bool -> Term Bool) -> Term Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term (Set Int)
s Term (Set Int) -> Term (Set Int) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Set Int -> Term (Set Int)
forall a. HasSpec a => a -> Term a
lit ([Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList [Int
1, Int
2, Int
3])
unionSized :: Specification (Set Int)
unionSized :: Specification (Set Int)
unionSized = (Term (Set Int) -> Term Bool) -> Specification (Set Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set Int) -> Term Bool) -> Specification (Set Int))
-> (Term (Set Int) -> Term Bool) -> Specification (Set Int)
forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
s ->
Term Integer
10 Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (Set Int) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Set Int)
s Term (Set Int) -> Term (Set Int) -> Term (Set Int)
forall a. Semigroup a => a -> a -> a
<> Set Int -> Term (Set Int)
forall a. HasSpec a => a -> Term a
lit ([Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList [Int
1 .. Int
8]))
maybeSpec :: Specification (Set (Maybe Int))
maybeSpec :: Specification (Set (Maybe Int))
maybeSpec = (Term (Set (Maybe Int)) -> Pred) -> Specification (Set (Maybe Int))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set (Maybe Int)) -> Pred)
-> Specification (Set (Maybe Int)))
-> (Term (Set (Maybe Int)) -> Pred)
-> Specification (Set (Maybe Int))
forall a b. (a -> b) -> a -> b
$ \Term (Set (Maybe Int))
ms ->
Term (Set (Maybe Int)) -> (Term (Maybe Int) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Maybe Int))
ms ((Term (Maybe Int) -> Pred) -> Pred)
-> (Term (Maybe Int) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Maybe Int)
m ->
(Term (Maybe Int)
-> FunTy
(MapList (Weighted (BinderD Deps)) (Cases (SimpleRep (Maybe Int))))
Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
(MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (Maybe Int)
m)
(FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
False)
(FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
y -> Term Int
0 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
y)
eitherSetSpec ::
Specification (Set (Either Int Int), Set (Either Int Int), Set (Either Int Int))
eitherSetSpec :: Specification
(Set (Either Int Int), Set (Either Int Int), Set (Either Int Int))
eitherSetSpec = FunTy
(MapList
Term
(Args
(SimpleRep
(Set (Either Int Int), Set (Either Int Int),
Set (Either Int Int)))))
[Pred]
-> Specification
(Set (Either Int Int), Set (Either Int Int), Set (Either 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
(Set (Either Int Int), Set (Either Int Int),
Set (Either Int Int)))))
[Pred]
-> Specification
(Set (Either Int Int), Set (Either Int Int), Set (Either Int Int)))
-> FunTy
(MapList
Term
(Args
(SimpleRep
(Set (Either Int Int), Set (Either Int Int),
Set (Either Int Int)))))
[Pred]
-> Specification
(Set (Either Int Int), Set (Either Int Int), Set (Either Int Int))
forall a b. (a -> b) -> a -> b
$ \Term (Set (Either Int Int))
es Term (Set (Either Int Int))
as Term (Set (Either Int Int))
bs ->
[ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Either Int Int))
es Term (Set (Either Int Int))
-> Term (Set (Either Int Int)) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (Term (Set (Either Int Int))
as Term (Set (Either Int Int))
-> Term (Set (Either Int Int)) -> Term (Set (Either Int Int))
forall a. Semigroup a => a -> a -> a
<> Term (Set (Either Int Int))
bs)
, Term (Set (Either Int Int))
-> (Term (Either Int Int) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Either Int Int))
as ((Term (Either Int Int) -> Pred) -> Pred)
-> (Term (Either Int Int) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
a ->
(Term (Either Int Int)
-> FunTy
(MapList
(Weighted (BinderD Deps)) (Cases (SimpleRep (Either Int Int))))
Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
(MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (Either Int Int)
a)
(FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
a' -> Term Int
a' Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
0)
(FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
b' -> Term Int
1 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
b')
, Term (Set (Either Int Int))
-> (Term (Either Int Int) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Either Int Int))
bs ((Term (Either Int Int) -> Pred) -> Pred)
-> (Term (Either Int Int) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
b ->
(Term (Either Int Int)
-> FunTy
(MapList
(Weighted (BinderD Deps)) (Cases (SimpleRep (Either Int Int))))
Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
(MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (Either Int Int)
b)
(FunTy (MapList Term (Args Int)) Bool -> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) Bool
-> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) Bool
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> Bool
False)
(FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
b' -> Term Int
1 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
b')
]
weirdSetPairSpec :: Specification ([Int], Set (Either Int Int))
weirdSetPairSpec :: Specification ([Int], Set (Either Int Int))
weirdSetPairSpec = FunTy
(MapList Term (Args (SimpleRep ([Int], Set (Either Int Int)))))
[Pred]
-> Specification ([Int], Set (Either 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], Set (Either Int Int)))))
[Pred]
-> Specification ([Int], Set (Either Int Int)))
-> FunTy
(MapList Term (Args (SimpleRep ([Int], Set (Either Int Int)))))
[Pred]
-> Specification ([Int], Set (Either Int Int))
forall a b. (a -> b) -> a -> b
$ \Term [Int]
as Term (Set (Either Int Int))
as' ->
[ Term (Set (Either Int Int))
as' Term (Set (Either Int Int)) -> Term [Int] -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term [Int]
as
, Term [Int] -> (Term Int -> Term Bool) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
as ((Term Int -> Term Bool) -> Pred)
-> (Term Int -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
a ->
Term (Either Int Int) -> Term (Set (Either Int Int)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ (Term Int -> Term (Either Int Int)
forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term (Either a b)
left_ Term Int
a) Term (Set (Either Int Int))
as'
, Term (Set (Either Int Int))
-> (Term (Either Int Int) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Either Int Int))
as' ((Term (Either Int Int) -> Pred) -> Pred)
-> (Term (Either Int Int) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
a' ->
(Term (Either Int Int)
-> FunTy
(MapList
(Weighted (BinderD Deps)) (Cases (SimpleRep (Either Int Int))))
Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
(MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (Either Int Int)
a')
(FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
x -> Term Int -> Term [Int] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ Term Int
x Term [Int]
as)
(FunTy (MapList Term (Args Int)) Bool -> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) Bool
-> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) Bool
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> Bool
False)
]
setPair :: Specification (Set (Int, Int))
setPair :: Specification (Set (Int, Int))
setPair = (Term (Set (Int, Int)) -> [Pred]) -> Specification (Set (Int, Int))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set (Int, Int)) -> [Pred])
-> Specification (Set (Int, Int)))
-> (Term (Set (Int, Int)) -> [Pred])
-> Specification (Set (Int, Int))
forall a b. (a -> b) -> a -> b
$ \Term (Set (Int, Int))
s ->
[ Term (Set (Int, Int)) -> (Term (Int, Int) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Int, Int))
s ((Term (Int, Int) -> Pred) -> Pred)
-> (Term (Int, Int) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p ->
Term (Int, Int)
p Term (Int, Int) -> Specification (Int, Int) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (Int, Int)
leqPair
, Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> Term (Int, Int)
forall a. HasSpec a => a -> Term a
lit (Int
0, Int
1) Term (Int, Int) -> Term (Set (Int, Int)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` Term (Set (Int, Int))
s
]
setSpec :: Specification (Set Int)
setSpec :: Specification (Set Int)
setSpec = (Term (Set Int) -> Pred) -> Specification (Set Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set Int) -> Pred) -> Specification (Set Int))
-> (Term (Set Int) -> Pred) -> Specification (Set Int)
forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
ss ->
Term (Set Int) -> (Term Int -> Term Bool) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set Int)
ss ((Term Int -> Term Bool) -> Pred)
-> (Term Int -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
s ->
Term Int
s Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
10
compositionalSpec :: Specification (Set Int)
compositionalSpec :: Specification (Set Int)
compositionalSpec = (Term (Set Int) -> [Pred]) -> Specification (Set Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set Int) -> [Pred]) -> Specification (Set Int))
-> (Term (Set Int) -> [Pred]) -> Specification (Set Int)
forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
x ->
[ Term (Set Int) -> Specification (Set Int) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Set Int)
x Specification (Set Int)
setSpec
, 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
0 Term Int -> Term (Set Int) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` Term (Set Int)
x
]
emptySetSpec :: Specification (Set Int)
emptySetSpec :: Specification (Set Int)
emptySetSpec = (Term (Set Int) -> Pred) -> Specification (Set Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set Int) -> Pred) -> Specification (Set Int))
-> (Term (Set Int) -> Pred) -> Specification (Set Int)
forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
s ->
Term (Set Int) -> (Term Int -> Term Bool) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set Int)
s ((Term Int -> Term Bool) -> Pred)
-> (Term Int -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
x -> Term Int -> Term (Set Int) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term Int
x Term (Set Int)
forall a. Monoid a => a
mempty
setSubSize :: Specification (Set Int)
setSubSize :: Specification (Set Int)
setSubSize = (Term (Set Int) -> Term Bool) -> Specification (Set Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set Int) -> Term Bool) -> Specification (Set Int))
-> (Term (Set Int) -> Term Bool) -> Specification (Set Int)
forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
s ->
Term Integer
2 Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
12 Term Integer -> Term Integer -> Term Integer
forall a. Num a => a -> a -> a
- (Term (Set Int) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Set Int)
s)
newtype NotASet a = NotASet (Set a)
deriving ((forall x. NotASet a -> Rep (NotASet a) x)
-> (forall x. Rep (NotASet a) x -> NotASet a)
-> Generic (NotASet a)
forall x. Rep (NotASet a) x -> NotASet a
forall x. NotASet a -> Rep (NotASet a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (NotASet a) x -> NotASet a
forall a x. NotASet a -> Rep (NotASet a) x
$cfrom :: forall a x. NotASet a -> Rep (NotASet a) x
from :: forall x. NotASet a -> Rep (NotASet a) x
$cto :: forall a x. Rep (NotASet a) x -> NotASet a
to :: forall x. Rep (NotASet a) x -> NotASet a
Generic, Int -> NotASet a -> ShowS
[NotASet a] -> ShowS
NotASet a -> String
(Int -> NotASet a -> ShowS)
-> (NotASet a -> String)
-> ([NotASet a] -> ShowS)
-> Show (NotASet a)
forall a. Show a => Int -> NotASet a -> ShowS
forall a. Show a => [NotASet a] -> ShowS
forall a. Show a => NotASet a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> NotASet a -> ShowS
showsPrec :: Int -> NotASet a -> ShowS
$cshow :: forall a. Show a => NotASet a -> String
show :: NotASet a -> String
$cshowList :: forall a. Show a => [NotASet a] -> ShowS
showList :: [NotASet a] -> ShowS
Show, NotASet a -> NotASet a -> Bool
(NotASet a -> NotASet a -> Bool)
-> (NotASet a -> NotASet a -> Bool) -> Eq (NotASet a)
forall a. Eq a => NotASet a -> NotASet a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => NotASet a -> NotASet a -> Bool
== :: NotASet a -> NotASet a -> Bool
$c/= :: forall a. Eq a => NotASet a -> NotASet a -> Bool
/= :: NotASet a -> NotASet a -> Bool
Eq)
instance (Typeable a, Ord a) => HasSimpleRep (NotASet a) where
type SimpleRep (NotASet a) = [a]
fromSimpleRep :: SimpleRep (NotASet a) -> NotASet a
fromSimpleRep = Set a -> NotASet a
forall a. Set a -> NotASet a
NotASet (Set a -> NotASet a) -> ([a] -> Set a) -> [a] -> NotASet a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList
toSimpleRep :: NotASet a -> SimpleRep (NotASet a)
toSimpleRep (NotASet Set a
s) = Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
s
instance (Ord a, HasSpec a) => HasSpec (NotASet a)
instance (Typeable a, Ord a) => Forallable (NotASet a) a
emptyListSpec :: Specification ([Int], NotASet (Either Int Int, Int))
emptyListSpec :: Specification ([Int], NotASet (Either Int Int, Int))
emptyListSpec = FunTy
(MapList
Term (Args (SimpleRep ([Int], NotASet (Either Int Int, Int)))))
[Pred]
-> Specification ([Int], NotASet (Either 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], NotASet (Either Int Int, Int)))))
[Pred]
-> Specification ([Int], NotASet (Either Int Int, Int)))
-> FunTy
(MapList
Term (Args (SimpleRep ([Int], NotASet (Either Int Int, Int)))))
[Pred]
-> Specification ([Int], NotASet (Either Int Int, Int))
forall a b. (a -> b) -> a -> b
$ \Term [Int]
is Term (NotASet (Either Int Int, Int))
ls ->
[ Term [Int] -> (Term Int -> Term Bool) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
is ((Term Int -> Term Bool) -> Pred)
-> (Term Int -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
i -> Term Int
i Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
0
, Term (NotASet (Either Int Int, Int))
-> FunTy
(MapList Term (Args (SimpleRep (Either Int Int, Int)))) Pred
-> 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 (NotASet (Either Int Int, Int))
ls (FunTy (MapList Term (Args (SimpleRep (Either Int Int, Int)))) Pred
-> Pred)
-> FunTy
(MapList Term (Args (SimpleRep (Either Int Int, Int)))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
l Term Int
_ ->
Term (Either Int Int)
-> FunTy
(MapList
(Weighted (BinderD Deps)) (Cases (SimpleRep (Either Int Int))))
Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
(MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (Either Int Int)
l (FunTy (MapList Term (Args Int)) Bool -> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) Bool
-> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) Bool
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> Bool
False) (FunTy (MapList Term (Args Int)) Bool -> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) Bool
-> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) Bool
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> Bool
False)
]
foldSingleCase :: Specification Int
foldSingleCase :: Specification Int
foldSingleCase = (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
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 Bool -> Term Bool
not_ (Term Bool -> Term Bool) -> Term Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term Int -> Term (Set Int) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term Int
x (Set Int -> Term (Set Int)
forall a. HasSpec a => a -> Term a
lit ([Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList [Int
10]))
, Term (Int, [(Int, Int)])
-> (Term (Int, [(Int, Int)]) -> Pred) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (Term Int -> Term [(Int, Int)] -> Term (Int, [(Int, Int)])
forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term Int
x (Term [(Int, Int)] -> Term (Int, [(Int, Int)]))
-> Term [(Int, Int)] -> Term (Int, [(Int, Int)])
forall a b. (a -> b) -> a -> b
$ [(Int, Int)] -> Term [(Int, Int)]
forall a. HasSpec a => a -> Term a
lit [(Int
10, Int
20) :: (Int, Int)]) ((Term (Int, [(Int, Int)]) -> Pred) -> Pred)
-> (Term (Int, [(Int, Int)]) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Int, [(Int, Int)])
p ->
Term (Int, [(Int, Int)])
-> FunTy (MapList Term (ProductAsList (Int, [(Int, Int)]))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, [(Int, Int)])
p (FunTy (MapList Term (ProductAsList (Int, [(Int, Int)]))) Pred
-> Pred)
-> FunTy (MapList Term (ProductAsList (Int, [(Int, Int)]))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
_ Term [(Int, Int)]
p1 -> Term [(Int, Int)] -> (Term (Int, Int) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [(Int, Int)]
p1 ((Term (Int, Int) -> Pred) -> Pred)
-> (Term (Int, Int) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p2 ->
Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Int
0 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term (Int, Int) -> Term Int
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (Int, Int)
p2)
]
complexUnion :: Specification (Set Int, Set Int)
complexUnion :: Specification (Set Int, Set Int)
complexUnion = FunTy
(MapList Term (Args (SimpleRep (Set Int, Set Int)))) [Term Bool]
-> Specification (Set Int, Set 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 (Set Int, Set Int)))) [Term Bool]
-> Specification (Set Int, Set Int))
-> FunTy
(MapList Term (Args (SimpleRep (Set Int, Set Int)))) [Term Bool]
-> Specification (Set Int, Set Int)
forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
ys Term (Set Int)
zs ->
[ Term (Set Int) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Set Int)
ys Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
10
, Term Integer
0 Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term (Set Int) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Set Int)
ys Term (Set Int) -> Term (Set Int) -> Term (Set Int)
forall a. Semigroup a => a -> a -> a
<> Term (Set Int)
zs)
]
unionBounded :: Specification (Set Int)
unionBounded :: Specification (Set Int)
unionBounded = (Term (Set Int) -> [Term Bool]) -> Specification (Set Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set Int) -> [Term Bool]) -> Specification (Set Int))
-> (Term (Set Int) -> [Term Bool]) -> Specification (Set Int)
forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
xs ->
[ Term (Set Int) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Set Int)
xs Term (Set Int) -> Term (Set Int) -> Term (Set Int)
forall a. Semigroup a => a -> a -> a
<> Set Int -> Term (Set Int)
forall a. HasSpec a => a -> Term a
lit ([Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList [Int
1, Int
2, Int
3])) Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
3
]
powersetPickOne :: Specification (Set Int)
powersetPickOne :: Specification (Set Int)
powersetPickOne =
(Term (Set Int) -> [Term Bool]) -> Specification (Set Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set Int) -> [Term Bool]) -> Specification (Set Int))
-> (Term (Set Int) -> [Term Bool]) -> Specification (Set Int)
forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
xs ->
[ Term (Set Int)
xs Term (Set Int) -> Term (Set Int) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Set Int -> Term (Set Int)
forall a. HasSpec a => a -> Term a
lit ([Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList [Int
3, Int
4])
, Term Bool -> Term Bool
not_ (Term Bool -> Term Bool) -> Term Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term (Set Int)
xs Term (Set Int) -> Term [Set Int] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` [Set Int] -> Term [Set Int]
forall a. HasSpec a => a -> Term a
lit [Set Int
forall a. Monoid a => a
mempty, [Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList [Int
3], [Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList [Int
3, Int
4]]
]