{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} module Constrained.Examples.Set where import GHC.Generics import Data.Set (Set) import Data.Set qualified as Set import Constrained import Constrained.Examples.Basic setPairSpec :: Specification BaseFn (Set Int, Set Int) setPairSpec :: Specification BaseFn (Set Int, Set Int) setPairSpec = forall a (fn :: [*] -> * -> *) p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec fn a, IsPred p fn) => FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Specification fn a constrained' forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set Int) s Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set Int) s' -> forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set Int) s forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int x -> forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set Int) s' forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int y -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int x forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int y fixedSetSpec :: Specification BaseFn (Set Int) fixedSetSpec :: Specification BaseFn (Set Int) fixedSetSpec = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set Int) s -> forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term BaseFn (Set Int) s forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int x -> [Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int x forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit (Int i :: Int) | Int i <- [Int 1 .. Int 3]] setOfPairLetSpec :: Specification BaseFn (Set (Int, Int)) setOfPairLetSpec :: Specification BaseFn (Set (Int, Int)) setOfPairLetSpec = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set (Int, Int)) ps -> forall (fn :: [*] -> * -> *) t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t, HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn, IsProd (SimpleRep a), HasSpec fn a) => Term fn t -> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn forAll' Term BaseFn (Set (Int, Int)) ps forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int x Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int y -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int x forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int y setSingletonSpec :: Specification BaseFn (Set (Int, Int)) setSingletonSpec :: Specification BaseFn (Set (Int, Int)) setSingletonSpec = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set (Int, Int)) ps -> forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term BaseFn (Set (Int, Int)) ps forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Int, Int) p -> forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll (forall (fn :: [*] -> * -> *) a. (HasSpec fn a, Ord a) => Term fn a -> Term fn (Set a) singleton_ (forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn (a, b) -> Term fn a fst_ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Int, Int) p)) forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int x -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int x forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int 10 eitherSimpleSetSpec :: Specification BaseFn (Set (Either Int Int)) eitherSimpleSetSpec :: Specification BaseFn (Set (Either Int Int)) eitherSimpleSetSpec = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set (Either Int Int)) ss -> forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term BaseFn (Set (Either Int Int)) ss forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Either Int Int) s -> (forall (fn :: [*] -> * -> *) a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) => Term fn a -> FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) caseOn Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Either Int Int) s) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int a -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int a forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int 0) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int b -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int 0 forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int b) forAllAnySpec :: Specification BaseFn (Set Int) forAllAnySpec :: Specification BaseFn (Set Int) forAllAnySpec = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set Int) as -> forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term BaseFn (Set Int) as forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int _ -> Bool True maybeJustSetSpec :: Specification BaseFn (Set (Maybe Int)) maybeJustSetSpec :: Specification BaseFn (Set (Maybe Int)) maybeJustSetSpec = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set (Maybe Int)) ms -> forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term BaseFn (Set (Maybe Int)) ms forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Maybe Int) m -> (forall (fn :: [*] -> * -> *) a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) => Term fn a -> FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) caseOn Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Maybe Int) m) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) () _ -> Bool False) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int y -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int 0 forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int y) notSubsetSpec :: Specification BaseFn (Set Int, Set Int) notSubsetSpec :: Specification BaseFn (Set Int, Set Int) notSubsetSpec = forall a (fn :: [*] -> * -> *) p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec fn a, IsPred p fn) => FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Specification fn a constrained' forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set Int) s Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set Int) s' -> forall (fn :: [*] -> * -> *). BaseUniverse fn => Term fn Bool -> Term fn Bool not_ forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) a. (HasSpec fn a, Ord a) => Term fn (Set a) -> Term fn (Set a) -> Term fn Bool subset_ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set Int) s Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set Int) s' emptyEitherMemberSpec :: Specification BaseFn (Set (Either Int Int)) emptyEitherMemberSpec :: Specification BaseFn (Set (Either Int Int)) emptyEitherMemberSpec = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set (Either Int Int)) s -> forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term BaseFn (Set (Either Int Int)) s forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Either Int Int) x -> (forall (fn :: [*] -> * -> *) a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) => Term fn a -> FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) caseOn Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Either Int Int) x) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int l -> forall a (fn :: [*] -> * -> *). (HasSpec fn a, Ord a) => Term fn a -> Term fn (Set a) -> Term fn Bool member_ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int l forall a. Monoid a => a mempty) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int r -> forall a (fn :: [*] -> * -> *). (HasSpec fn a, Ord a) => Term fn a -> Term fn (Set a) -> Term fn Bool member_ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int r forall a. Monoid a => a mempty) emptyEitherSpec :: Specification BaseFn (Set (Either Int Int)) emptyEitherSpec :: Specification BaseFn (Set (Either Int Int)) emptyEitherSpec = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set (Either Int Int)) s -> forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term BaseFn (Set (Either Int Int)) s forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Either Int Int) x -> (forall (fn :: [*] -> * -> *) a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) => Term fn a -> FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) caseOn Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Either Int Int) x) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int _ -> Bool False) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int _ -> Bool False) notSubset :: Specification BaseFn (Set Int) notSubset :: Specification BaseFn (Set Int) notSubset = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set Int) s -> forall (fn :: [*] -> * -> *). BaseUniverse fn => Term fn Bool -> Term fn Bool not_ forall a b. (a -> b) -> a -> b $ Term BaseFn (Set Int) s forall (fn :: [*] -> * -> *) a. (HasSpec fn a, Ord a) => Term fn (Set a) -> Term fn (Set a) -> Term fn Bool `subset_` forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit (forall a. Ord a => [a] -> Set a Set.fromList [Int 1, Int 2, Int 3]) unionSized :: Specification BaseFn (Set Int) unionSized :: Specification BaseFn (Set Int) unionSized = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set Int) s -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Integer 10 forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Term fn a -> Term fn Bool ==. forall a (fn :: [*] -> * -> *). (HasSpec fn (Set a), Ord a) => Term fn (Set a) -> Term fn Integer size_ (Term BaseFn (Set Int) s forall a. Semigroup a => a -> a -> a <> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit (forall a. Ord a => [a] -> Set a Set.fromList [Int 1 .. Int 8])) maybeSpec :: Specification BaseFn (Set (Maybe Int)) maybeSpec :: Specification BaseFn (Set (Maybe Int)) maybeSpec = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set (Maybe Int)) ms -> forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term BaseFn (Set (Maybe Int)) ms forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Maybe Int) m -> (forall (fn :: [*] -> * -> *) a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) => Term fn a -> FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) caseOn Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Maybe Int) m) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) () _ -> Bool False) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int y -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int 0 forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int y) eitherSetSpec :: Specification BaseFn (Set (Either Int Int), Set (Either Int Int), Set (Either Int Int)) eitherSetSpec :: Specification BaseFn (Set (Either Int Int), Set (Either Int Int), Set (Either Int Int)) eitherSetSpec = forall a (fn :: [*] -> * -> *) p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec fn a, IsPred p fn) => FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Specification fn a constrained' forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set (Either Int Int)) es Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set (Either Int Int)) as Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set (Either Int Int)) bs -> [ forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set (Either Int Int)) es forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Term fn a -> Term fn Bool ==. (Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set (Either Int Int)) as forall a. Semigroup a => a -> a -> a <> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set (Either Int Int)) bs) , forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set (Either Int Int)) as forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Either Int Int) a -> (forall (fn :: [*] -> * -> *) a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) => Term fn a -> FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) caseOn Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Either Int Int) a) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int a' -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int a' forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int 0) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int b' -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int 1 forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int b') , forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set (Either Int Int)) bs forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Either Int Int) b -> (forall (fn :: [*] -> * -> *) a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) => Term fn a -> FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) caseOn Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Either Int Int) b) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int _ -> Bool False) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int b' -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int 1 forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int b') ] weirdSetPairSpec :: Specification BaseFn ([Int], Set (Either Int Int)) weirdSetPairSpec :: Specification BaseFn ([Int], Set (Either Int Int)) weirdSetPairSpec = forall a (fn :: [*] -> * -> *) p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec fn a, IsPred p fn) => FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Specification fn a constrained' forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) [Int] as Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set (Either Int Int)) as' -> [ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set (Either Int Int)) as' forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn a -> Term fn b -> Pred fn `dependsOn` Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) [Int] as , forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) [Int] as forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int a -> forall a (fn :: [*] -> * -> *). (HasSpec fn a, Ord a) => Term fn a -> Term fn (Set a) -> Term fn Bool member_ (forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b, IsNormalType a, IsNormalType b) => Term fn a -> Term fn (Either a b) left_ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int a) Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set (Either Int Int)) as' , forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set (Either Int Int)) as' forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Either Int Int) a' -> (forall (fn :: [*] -> * -> *) a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) => Term fn a -> FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) caseOn Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Either Int Int) a') (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int x -> forall a (fn :: [*] -> * -> *). HasSpec fn a => Term fn a -> Term fn [a] -> Term fn Bool elem_ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int x Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) [Int] as) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int _ -> Bool False) ] setPair :: Specification BaseFn (Set (Int, Int)) setPair :: Specification BaseFn (Set (Int, Int)) setPair = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set (Int, Int)) s -> [ forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term BaseFn (Set (Int, Int)) s forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Int, Int) p -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Int, Int) p forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn `satisfies` Specification BaseFn (Int, Int) leqPair , forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit (Int 0, Int 1) forall a (fn :: [*] -> * -> *). (HasSpec fn a, Ord a) => Term fn a -> Term fn (Set a) -> Term fn Bool `member_` Term BaseFn (Set (Int, Int)) s ] setSpec :: Specification BaseFn (Set Int) setSpec :: Specification BaseFn (Set Int) setSpec = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set Int) ss -> forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term BaseFn (Set Int) ss forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int s -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int s forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int 10 compositionalSpec :: Specification BaseFn (Set Int) compositionalSpec :: Specification BaseFn (Set Int) compositionalSpec = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set Int) x -> [ forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn satisfies Term BaseFn (Set Int) x Specification BaseFn (Set Int) setSpec , forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int 0 forall a (fn :: [*] -> * -> *). (HasSpec fn a, Ord a) => Term fn a -> Term fn (Set a) -> Term fn Bool `member_` Term BaseFn (Set Int) x ] emptySetSpec :: Specification BaseFn (Set Int) emptySetSpec :: Specification BaseFn (Set Int) emptySetSpec = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set Int) s -> forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term BaseFn (Set Int) s forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int x -> forall a (fn :: [*] -> * -> *). (HasSpec fn a, Ord a) => Term fn a -> Term fn (Set a) -> Term fn Bool member_ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int x forall a. Monoid a => a mempty setSubSize :: Specification BaseFn (Set Int) setSubSize :: Specification BaseFn (Set Int) setSubSize = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set Int) s -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Integer 2 forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Term fn a -> Term fn Bool ==. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Integer 12 forall a. Num a => a -> a -> a - (forall a (fn :: [*] -> * -> *). (HasSpec fn a, Sized a) => Term fn a -> Term fn Integer sizeOf_ Term BaseFn (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 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 fn a) => HasSpec fn (NotASet a) instance Ord a => Forallable (NotASet a) a emptyListSpec :: Specification BaseFn ([Int], NotASet (Either Int Int, Int)) emptyListSpec :: Specification BaseFn ([Int], NotASet (Either Int Int, Int)) emptyListSpec = forall a (fn :: [*] -> * -> *) p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec fn a, IsPred p fn) => FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Specification fn a constrained' forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) [Int] is Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (NotASet (Either Int Int, Int)) ls -> [ forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) [Int] is forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int i -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int i forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int 0 , forall (fn :: [*] -> * -> *) t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t, HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn, IsProd (SimpleRep a), HasSpec fn a) => Term fn t -> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn forAll' Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (NotASet (Either Int Int, Int)) ls forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Either Int Int) l Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int _ -> forall (fn :: [*] -> * -> *) a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) => Term fn a -> FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) caseOn Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Either Int Int) l (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int _ -> Bool False) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int _ -> Bool False) ] foldSingleCase :: Specification BaseFn Int foldSingleCase :: Specification BaseFn Int foldSingleCase = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn Int x -> [ forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *). BaseUniverse fn => Term fn Bool -> Term fn Bool not_ forall a b. (a -> b) -> a -> b $ forall a (fn :: [*] -> * -> *). (HasSpec fn a, Ord a) => Term fn a -> Term fn (Set a) -> Term fn Bool member_ Term BaseFn Int x (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit (forall a. Ord a => [a] -> Set a Set.fromList [Int 10])) , forall (fn :: [*] -> * -> *) a p. (HasSpec fn a, IsPred p fn) => Term fn a -> (Term fn a -> p) -> Pred fn letBind (forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn a -> Term fn b -> Term fn (a, b) pair_ Term BaseFn Int x forall a b. (a -> b) -> a -> b $ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit [(Int 10, Int 20) :: (Int, Int)]) forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Int, [(Int, Int)]) p -> forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, IsProductType fn a, IsPred p fn) => Term fn a -> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn match Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Int, [(Int, Int)]) p forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int _ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) [(Int, Int)] p1 -> forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) [(Int, Int)] p1 forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Int, Int) p2 -> forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert (Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int 0 forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn (a, b) -> Term fn b snd_ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Int, Int) p2) ] complexUnion :: Specification BaseFn (Set Int, Set Int) complexUnion :: Specification BaseFn (Set Int, Set Int) complexUnion = forall a (fn :: [*] -> * -> *) p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec fn a, IsPred p fn) => FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Specification fn a constrained' forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set Int) ys Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set Int) zs -> [ forall a (fn :: [*] -> * -> *). (HasSpec fn a, Sized a) => Term fn a -> Term fn Integer sizeOf_ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set Int) ys forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Integer 10 , Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Integer 0 forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <. forall a (fn :: [*] -> * -> *). (HasSpec fn a, Sized a) => Term fn a -> Term fn Integer sizeOf_ (Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set Int) ys forall a. Semigroup a => a -> a -> a <> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set Int) zs) ] unionBounded :: Specification BaseFn (Set Int) unionBounded :: Specification BaseFn (Set Int) unionBounded = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set Int) xs -> [ forall a (fn :: [*] -> * -> *). (HasSpec fn a, Sized a) => Term fn a -> Term fn Integer sizeOf_ (Term BaseFn (Set Int) xs forall a. Semigroup a => a -> a -> a <> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit (forall a. Ord a => [a] -> Set a Set.fromList [Int 1, Int 2, Int 3])) forall a (fn :: [*] -> * -> *). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Integer 3 ] -- Only possible value is {4} powersetPickOne :: Specification BaseFn (Set Int) powersetPickOne :: Specification BaseFn (Set Int) powersetPickOne = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Set Int) xs -> [ Term BaseFn (Set Int) xs forall (fn :: [*] -> * -> *) a. (HasSpec fn a, Ord a) => Term fn (Set a) -> Term fn (Set a) -> Term fn Bool `subset_` forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit (forall a. Ord a => [a] -> Set a Set.fromList [Int 3, Int 4]) , forall (fn :: [*] -> * -> *). BaseUniverse fn => Term fn Bool -> Term fn Bool not_ forall a b. (a -> b) -> a -> b $ Term BaseFn (Set Int) xs forall a (fn :: [*] -> * -> *). HasSpec fn a => Term fn a -> Term fn [a] -> Term fn Bool `elem_` forall a (fn :: [*] -> * -> *). Show a => a -> Term fn 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]] ]