{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

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 = 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 (Set Int)
s Term (Set Int)
s' ->
  forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set Int)
s forall a b. (a -> b) -> a -> b
$ \Term Int
x ->
    forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set Int)
s' forall a b. (a -> b) -> a -> b
$ \Term Int
y ->
      Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
y

fixedSetSpec :: Specification (Set Int)
fixedSetSpec :: Specification (Set Int)
fixedSetSpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
s ->
  forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set Int)
s forall a b. (a -> b) -> a -> b
$ \Term Int
x ->
    [Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. 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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set (Int, Int))
ps ->
  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 (Set (Int, Int))
ps forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y ->
    Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
y

setSingletonSpec :: Specification (Set (Int, Int))
setSingletonSpec :: Specification (Set (Int, Int))
setSingletonSpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set (Int, Int))
ps ->
  forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Int, Int))
ps forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p ->
    forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (forall a. (Ord a, HasSpec a) => Term a -> Term (Set a)
singleton_ (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (Int, Int)
p)) forall a b. (a -> b) -> a -> b
$ \Term Int
x ->
      Term Int
x 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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set (Either Int Int))
ss ->
  forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Either Int Int))
ss forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
s ->
    (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (Either Int Int)
s)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
a -> Term Int
a forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
0)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
b -> Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
b)

forAllAnySpec :: Specification (Set Int)
forAllAnySpec :: Specification (Set Int)
forAllAnySpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
as ->
  forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set Int)
as forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> Bool
True

maybeJustSetSpec :: Specification (Set (Maybe Int))
maybeJustSetSpec :: Specification (Set (Maybe Int))
maybeJustSetSpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set (Maybe Int))
ms ->
  forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Maybe Int))
ms forall a b. (a -> b) -> a -> b
$ \Term (Maybe Int)
m ->
    (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (Maybe Int)
m)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Bool
False)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
y -> Term Int
0 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 = 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 (Set Int)
s Term (Set Int)
s' -> Term Bool -> Term Bool
not_ forall a b. (a -> b) -> a -> b
$ 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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set (Either Int Int))
s ->
  forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Either Int Int))
s forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
x ->
    (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (Either Int Int)
x)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
l -> forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term Int
l forall a. Monoid a => a
mempty)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
r -> forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term Int
r forall a. Monoid a => a
mempty)

emptyEitherSpec :: Specification (Set (Either Int Int))
emptyEitherSpec :: Specification (Set (Either Int Int))
emptyEitherSpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set (Either Int Int))
s ->
  forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Either Int Int))
s forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
x ->
    (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (Either Int Int)
x)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> Bool
False)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> Bool
False)

notSubset :: Specification (Set Int)
notSubset :: Specification (Set Int)
notSubset = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
s ->
  Term Bool -> Term Bool
not_ forall a b. (a -> b) -> a -> b
$ Term (Set Int)
s forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` forall a. HasSpec a => a -> Term a
lit (forall a. Ord a => [a] -> Set a
Set.fromList [Int
1, Int
2, Int
3])

unionSized :: Specification (Set Int)
unionSized :: Specification (Set Int)
unionSized = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
s ->
  Term Integer
10 forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Set Int)
s forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => a -> Term a
lit (forall a. Ord a => [a] -> Set a
Set.fromList [Int
1 .. Int
8]))

maybeSpec :: Specification (Set (Maybe Int))
maybeSpec :: Specification (Set (Maybe Int))
maybeSpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set (Maybe Int))
ms ->
  forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Maybe Int))
ms forall a b. (a -> b) -> a -> b
$ \Term (Maybe Int)
m ->
    (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (Maybe Int)
m)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Bool
False)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
y -> Term Int
0 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 = 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 (Set (Either Int Int))
es Term (Set (Either Int Int))
as Term (Set (Either Int Int))
bs ->
  [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Set (Either Int Int))
es forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (Term (Set (Either Int Int))
as forall a. Semigroup a => a -> a -> a
<> Term (Set (Either Int Int))
bs)
  , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Either Int Int))
as forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
a ->
      (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (Either Int Int)
a)
        (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
a' -> Term Int
a' forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
0)
        (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
b' -> Term Int
1 forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
b')
  , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Either Int Int))
bs forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
b ->
      (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (Either Int Int)
b)
        (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> Bool
False)
        (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
b' -> Term Int
1 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 = 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]
as Term (Set (Either Int Int))
as' ->
  [ Term (Set (Either Int Int))
as' forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term [Int]
as
  , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
as forall a b. (a -> b) -> a -> b
$ \Term Int
a ->
      forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ (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'
  , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Either Int Int))
as' forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
a' ->
      (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (Either Int Int)
a')
        (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
x -> forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ Term Int
x Term [Int]
as)
        (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> Bool
False)
  ]

setPair :: Specification (Set (Int, Int))
setPair :: Specification (Set (Int, Int))
setPair = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set (Int, Int))
s ->
  [ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Int, Int))
s forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p ->
      Term (Int, Int)
p forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (Int, Int)
leqPair
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => a -> Term a
lit (Int
0, Int
1) 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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
ss ->
  forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set Int)
ss forall a b. (a -> b) -> a -> b
$ \Term Int
s ->
    Term Int
s forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
10

compositionalSpec :: Specification (Set Int)
compositionalSpec :: Specification (Set Int)
compositionalSpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
x ->
  [ forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Set Int)
x Specification (Set Int)
setSpec
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
0 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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
s ->
  forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set Int)
s forall a b. (a -> b) -> a -> b
$ \Term Int
x -> forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term Int
x forall a. Monoid a => a
mempty

setSubSize :: Specification (Set Int)
setSubSize :: Specification (Set Int)
setSubSize = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
s ->
  Term Integer
2 forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
12 forall a. Num a => a -> a -> a
- (forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Set Int)
s)

newtype NotASet a = NotASet (Set a)
  deriving (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
$cto :: forall a x. Rep (NotASet a) x -> NotASet a
$cfrom :: forall a x. NotASet a -> Rep (NotASet a) x
Generic, Int -> NotASet a -> ShowS
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
showList :: [NotASet a] -> ShowS
$cshowList :: forall a. Show a => [NotASet a] -> ShowS
show :: NotASet a -> String
$cshow :: forall a. Show a => NotASet a -> String
showsPrec :: Int -> NotASet a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> NotASet a -> ShowS
Show, NotASet a -> NotASet a -> Bool
forall a. Eq a => NotASet a -> NotASet a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NotASet a -> NotASet a -> Bool
$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
Eq)
instance (Typeable a, Ord a) => HasSimpleRep (NotASet a) where
  type SimpleRep (NotASet a) = [a]
  fromSimpleRep :: SimpleRep (NotASet a) -> NotASet a
fromSimpleRep = forall a. Set a -> NotASet a
NotASet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
Set.fromList
  toSimpleRep :: NotASet a -> SimpleRep (NotASet a)
toSimpleRep (NotASet Set a
s) = 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 = 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]
is Term (NotASet (Either Int Int, Int))
ls ->
  [ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
is forall a b. (a -> b) -> a -> b
$ \Term Int
i -> Term Int
i forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
0
  , 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 (NotASet (Either Int Int, Int))
ls forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
l Term Int
_ ->
      forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (Either Int Int)
l (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> Bool
False) (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> Bool
False)
  ]

foldSingleCase :: Specification Int
foldSingleCase :: Specification Int
foldSingleCase = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Int
x ->
  [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ forall a b. (a -> b) -> a -> b
$ forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term Int
x (forall a. HasSpec a => a -> Term a
lit (forall a. Ord a => [a] -> Set a
Set.fromList [Int
10]))
  , forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term Int
x forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => a -> Term a
lit [(Int
10, Int
20) :: (Int, Int)]) forall a b. (a -> b) -> a -> b
$ \Term (Int, [(Int, Int)])
p ->
      forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, [(Int, Int)])
p forall a b. (a -> b) -> a -> b
$ \Term Int
_ Term [(Int, Int)]
p1 -> forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [(Int, Int)]
p1 forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p2 ->
        forall p. IsPred p => p -> Pred
assert (Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. 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 = 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 (Set Int)
ys Term (Set Int)
zs ->
  [ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Set Int)
ys forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
10
  , Term Integer
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Set Int)
ys forall a. Semigroup a => a -> a -> a
<> Term (Set Int)
zs)
  ]

unionBounded :: Specification (Set Int)
unionBounded :: Specification (Set Int)
unionBounded = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
xs ->
  [ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Set Int)
xs forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => a -> Term a
lit (forall a. Ord a => [a] -> Set a
Set.fromList [Int
1, Int
2, Int
3])) forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
3
  ]

-- Only possible value is {4}
powersetPickOne :: Specification (Set Int)
powersetPickOne :: Specification (Set Int)
powersetPickOne =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
xs ->
    [ Term (Set Int)
xs forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` forall a. HasSpec a => a -> Term a
lit (forall a. Ord a => [a] -> Set a
Set.fromList [Int
3, Int
4])
    , Term Bool -> Term Bool
not_ forall a b. (a -> b) -> a -> b
$ Term (Set Int)
xs forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall a. HasSpec a => a -> Term a
lit [forall a. Monoid a => a
mempty, forall a. Ord a => [a] -> Set a
Set.fromList [Int
3], forall a. Ord a => [a] -> Set a
Set.fromList [Int
3, Int
4]]
    ]