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

module Constrained.Examples.Set where

import Constrained.API
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
  ]

-- Only possible value is {4}
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]]
    ]