{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-} module Constrained.Examples.Basic where import GHC.Generics import Test.QuickCheck qualified as QC import Constrained leqPair :: Specification BaseFn (Int, Int) leqPair :: Specification BaseFn (Int, Int) leqPair = 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, Int) [var| 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) 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 [var| 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 [var| 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 simplePairSpec :: Specification BaseFn (Int, Int) simplePairSpec :: Specification BaseFn (Int, Int) simplePairSpec = 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 $ \(forall (fn :: [*] -> * -> *) a. String -> Term fn a -> Term fn a name String "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 :: [*] -> * -> *) 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) p forall a b. (a -> b) -> a -> b $ \(forall (fn :: [*] -> * -> *) a. String -> Term fn a -> Term fn a name String "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) 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 -> [ 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 x 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))))) Int 0 , forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) a. String -> Term fn a -> Term fn a name String "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 y 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))))) Int 0 , -- You can use `monitor` to add QuickCheck property modifiers for -- monitoring distribution, like classify, label, and cover, to your -- specification forall (fn :: [*] -> * -> *). ((forall a. Term fn a -> a) -> Property -> Property) -> Pred fn monitor forall a b. (a -> b) -> a -> b $ \forall 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))))) a -> a eval -> forall prop. Testable prop => Bool -> String -> prop -> Property QC.classify (forall 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))))) a -> a eval 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 forall a. Ord a => a -> a -> Bool > Int 0) String "positive y" forall b c a. (b -> c) -> (a -> b) -> a -> c . forall prop. Testable prop => Bool -> String -> prop -> Property QC.classify (forall 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))))) a -> a eval 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. Ord a => a -> a -> Bool > Int 0) String "positive x" ] sizeAddOrSub1 :: Specification BaseFn Integer sizeAddOrSub1 :: Specification BaseFn Integer sizeAddOrSub1 = 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 Integer 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 4 forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Term fn a -> Term fn Bool ==. Term BaseFn Integer s forall a. Num 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))))) Integer 2 sizeAddOrSub2 :: Specification BaseFn Integer sizeAddOrSub2 :: Specification BaseFn Integer sizeAddOrSub2 = 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 Integer 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 4 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 2 forall a. Num a => a -> a -> a + Term BaseFn Integer s sizeAddOrSub3 :: Specification BaseFn Integer sizeAddOrSub3 :: Specification BaseFn Integer sizeAddOrSub3 = 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 Integer 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 4 forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Term fn a -> Term fn Bool ==. Term BaseFn Integer s forall a. Num 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))))) Integer 2 -- | We expect a negative Integer, so ltSpec tests for that. sizeAddOrSub4 :: Specification BaseFn Integer sizeAddOrSub4 :: Specification BaseFn Integer sizeAddOrSub4 = forall (fn :: [*] -> * -> *) a. OrdLike fn a => a -> Specification fn a ltSpec Integer 0 forall a. Semigroup a => a -> a -> a <> (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 (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 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 4 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 2 forall a. Num 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))))) Integer s) sizeAddOrSub5 :: Specification BaseFn Integer sizeAddOrSub5 :: Specification BaseFn Integer sizeAddOrSub5 = 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 Integer 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 - Term BaseFn Integer s listSubSize :: Specification BaseFn [Int] listSubSize :: Specification BaseFn [Int] listSubSize = 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] 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 [Int] s) orPair :: Specification BaseFn (Int, Int) orPair :: Specification BaseFn (Int, Int) orPair = 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 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 5 forall (fn :: [*] -> * -> *). BaseUniverse fn => Term fn Bool -> Term fn Bool -> 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 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 5 trickyCompositional :: Specification BaseFn (Int, Int) trickyCompositional :: Specification BaseFn (Int, Int) trickyCompositional = 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, Int) p -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn satisfies Term BaseFn (Int, Int) p Specification BaseFn (Int, Int) simplePairSpec forall a. Semigroup a => a -> a -> a <> forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert (forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn (a, b) -> Term fn a fst_ Term BaseFn (Int, Int) p 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))))) Int 1000) data Foo = Foo Int | Bar Int Int deriving (Int -> Foo -> ShowS [Foo] -> ShowS Foo -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Foo] -> ShowS $cshowList :: [Foo] -> ShowS show :: Foo -> String $cshow :: Foo -> String showsPrec :: Int -> Foo -> ShowS $cshowsPrec :: Int -> Foo -> ShowS Show, Foo -> Foo -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Foo -> Foo -> Bool $c/= :: Foo -> Foo -> Bool == :: Foo -> Foo -> Bool $c== :: Foo -> Foo -> Bool Eq, Eq Foo Foo -> Foo -> Bool Foo -> Foo -> Ordering Foo -> Foo -> Foo forall a. Eq a -> (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: Foo -> Foo -> Foo $cmin :: Foo -> Foo -> Foo max :: Foo -> Foo -> Foo $cmax :: Foo -> Foo -> Foo >= :: Foo -> Foo -> Bool $c>= :: Foo -> Foo -> Bool > :: Foo -> Foo -> Bool $c> :: Foo -> Foo -> Bool <= :: Foo -> Foo -> Bool $c<= :: Foo -> Foo -> Bool < :: Foo -> Foo -> Bool $c< :: Foo -> Foo -> Bool compare :: Foo -> Foo -> Ordering $ccompare :: Foo -> Foo -> Ordering Ord, forall x. Rep Foo x -> Foo forall x. Foo -> Rep Foo x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a $cto :: forall x. Rep Foo x -> Foo $cfrom :: forall x. Foo -> Rep Foo x Generic) instance HasSimpleRep Foo instance BaseUniverse fn => HasSpec fn Foo fooSpec :: Specification BaseFn Foo fooSpec :: Specification BaseFn Foo fooSpec = 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 Foo foo -> (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 BaseFn Foo foo) ( 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 i -> [ 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 :: [*] -> * -> *). (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 i , forall (fn :: [*] -> * -> *). ((forall a. Term fn a -> a) -> Property -> Property) -> Pred fn monitor forall a b. (a -> b) -> a -> b $ \forall 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))))) a -> a _ -> forall prop. Testable prop => Double -> Bool -> String -> prop -> Property QC.cover Double 40 Bool True String "Foo" ] ) ( 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 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 j -> [ 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 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 j , forall (fn :: [*] -> * -> *). ((forall a. Term fn a -> a) -> Property -> Property) -> Pred fn monitor forall a b. (a -> b) -> a -> b $ \forall 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))))) a -> a _ -> forall prop. Testable prop => Double -> Bool -> String -> prop -> Property QC.cover Double 40 Bool True String "Bar" ] ) intSpec :: Specification BaseFn (Int, Int) intSpec :: Specification BaseFn (Int, Int) intSpec = 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 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 b -> forall (fn :: [*] -> * -> *) a b p. (HasSpec fn a, HasSpec fn b, IsPred p fn) => Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn reify 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. Integral a => a -> a -> a `mod` Int 10) 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 b 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))))) Int a' mapElemKeySpec :: Specification BaseFn Int mapElemKeySpec :: Specification BaseFn Int mapElemKeySpec = 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 n -> 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 n forall a b. (a -> b) -> a -> b $ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit (Bool False, Int 4)) forall a b. (a -> b) -> a -> b $ \(Term BaseFn (Int, (Bool, Int)) p :: Term BaseFn (Int, (Bool, Int))) -> 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, b) -> Term fn b snd_ (forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn (a, b) -> Term fn b snd_ Term BaseFn (Int, (Bool, 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, 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 x, forall (fn :: [*] -> * -> *). BaseUniverse fn => Term fn Bool -> Term fn Bool not_ forall a b. (a -> b) -> a -> b $ forall a (fn :: [*] -> * -> *). HasSpec fn a => Term fn a -> Term fn [a] -> Term fn Bool elem_ Term BaseFn Int n forall a b. (a -> b) -> a -> b $ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit []] intRangeSpec :: Int -> Specification BaseFn Int intRangeSpec :: Int -> Specification BaseFn Int intRangeSpec Int a = 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 n -> Term BaseFn Int n 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 a testRewriteSpec :: Specification BaseFn ((Int, Int), (Int, Int)) testRewriteSpec :: Specification BaseFn ((Int, Int), (Int, Int)) testRewriteSpec = 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, 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, 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, Int) x forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Term fn a -> Term fn Bool ==. forall a (fn :: [*] -> * -> *). (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) => Term fn (SimpleRep a) -> Term fn a fromGeneric_ (forall a (fn :: [*] -> * -> *). (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) => Term fn a -> Term fn (SimpleRep a) toGeneric_ 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) y) pairSingletonSpec :: Specification BaseFn (Int, Int) pairSingletonSpec :: Specification BaseFn (Int, Int) pairSingletonSpec = 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, Int) q -> 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_ Term BaseFn (Int, Int) q) 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 (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, 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 -> 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, 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) 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 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 parallelLet :: Specification BaseFn (Int, Int) parallelLet :: Specification BaseFn (Int, Int) parallelLet = 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, Int) p -> [ 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, b) -> Term fn a fst_ Term BaseFn (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 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 x , 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, b) -> Term fn b snd_ Term BaseFn (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 0 ] letExists :: Specification BaseFn (Int, Int) letExists :: Specification BaseFn (Int, Int) letExists = 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, Int) p -> [ 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, b) -> Term fn a fst_ Term BaseFn (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 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 x , forall a p (fn :: [*] -> * -> *). (HasSpec fn a, IsPred p fn) => ((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn exists (\forall 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))))) a -> a eval -> forall (f :: * -> *) a. Applicative f => a -> f a pure forall a b. (a -> b) -> a -> b $ forall a b. (a, b) -> b snd (forall 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))))) a -> a eval Term BaseFn (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 0 , forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn (a, b) -> Term fn b snd_ Term BaseFn (Int, Int) p 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))))) Int x ] ] letExistsLet :: Specification BaseFn (Int, Int) letExistsLet :: Specification BaseFn (Int, Int) letExistsLet = 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, Int) p -> [ 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, b) -> Term fn a fst_ Term BaseFn (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 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 x , forall a p (fn :: [*] -> * -> *). (HasSpec fn a, IsPred p fn) => ((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn exists (\forall 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))))) a -> a eval -> forall (f :: * -> *) a. Applicative f => a -> f a pure forall a b. (a -> b) -> a -> b $ forall a b. (a, b) -> b snd (forall 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))))) a -> a eval Term BaseFn (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 -> [ 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 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 0 , 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, b) -> Term fn b snd_ Term BaseFn (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 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 (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))))) 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 y 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 1 ] ] ] dependencyWeirdness :: Specification BaseFn (Int, Int, Int) dependencyWeirdness :: Specification BaseFn (Int, Int, Int) dependencyWeirdness = 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 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 z -> forall (fn :: [*] -> * -> *) a b p. (HasSpec fn a, HasSpec fn b, IsPred p fn) => Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn reify (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. Num 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))))) Int y) forall a. a -> a id 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 zv -> 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 z 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))))) Int zv parallelLetPair :: Specification BaseFn (Int, Int) parallelLetPair :: Specification BaseFn (Int, Int) parallelLetPair = 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, 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 BaseFn (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 y -> [ 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 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 , 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 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 x ] , 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 BaseFn (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 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 y 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 x ] existsUnfree :: Specification BaseFn Int existsUnfree :: Specification BaseFn Int existsUnfree = 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 _ -> forall a p (fn :: [*] -> * -> *). (HasSpec fn a, IsPred p fn) => ((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn exists (\forall 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))))) a -> a _ -> forall (f :: * -> *) a. Applicative f => a -> f a pure Int 1) 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 y 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 [Int 1, Int 2 :: Int] reifyYucky :: Specification BaseFn (Int, Int, Int) reifyYucky :: Specification BaseFn (Int, Int, Int) reifyYucky = 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 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 z -> [ forall (fn :: [*] -> * -> *) a b p. (HasSpec fn a, HasSpec fn b, IsPred p fn) => Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn reify 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. a -> a id 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 w -> [ 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 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))))) Int w , 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 z 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))))) Int w ] , 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 z 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 y ] basicSpec :: Specification BaseFn Int basicSpec :: Specification BaseFn Int basicSpec = 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 a p (fn :: [*] -> * -> *). (HasSpec fn a, IsPred p fn) => ((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn exists (\forall 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))))) a -> a eval -> forall (f :: * -> *) a. Applicative f => a -> f a pure forall a b. (a -> b) -> a -> b $ forall 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))))) a -> a eval Term BaseFn Int x) 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 -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn satisfies Term BaseFn Int x forall a b. (a -> b) -> a -> b $ 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 (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 1 forall a. Num 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))))) Int y canFollowLike :: Specification BaseFn ((Int, Int), (Int, Int)) canFollowLike :: Specification BaseFn ((Int, Int), (Int, Int)) canFollowLike = 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, 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) q -> 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) 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 ma 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 mi -> 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) q 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 ma' 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 mi' -> [ forall (fn :: [*] -> * -> *) p q. (BaseUniverse fn, IsPred p fn, IsPred q fn) => Term fn Bool -> p -> q -> Pred fn ifElse (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 ma' 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))))) Int ma) (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 mi' 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))))) Int mi forall a. Num 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))))) Int 1) (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 mi' 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))))) Int 0) , 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 ma' 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 ma forall a. Num 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))))) Int 1 , 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 ma 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 ma' , 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 ma' 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 ma ] ifElseBackwards :: Specification BaseFn (Int, Int) ifElseBackwards :: Specification BaseFn (Int, Int) ifElseBackwards = 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 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 q -> [ forall (fn :: [*] -> * -> *) p q. (BaseUniverse fn, IsPred p fn, IsPred q fn) => Term fn Bool -> p -> q -> Pred fn ifElse (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 p 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))))) Int 1) (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 q 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) (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 q) , 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 p 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 q ] assertReal :: Specification BaseFn Int assertReal :: Specification BaseFn Int assertReal = 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 $ Term BaseFn 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 , forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> (a -> Bool) -> Pred fn assertReified Term BaseFn Int x (forall a. Ord a => a -> a -> Bool <= Int 10) ] assertRealMultiple :: Specification BaseFn (Int, Int) assertRealMultiple :: Specification BaseFn (Int, Int) assertRealMultiple = 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 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 -> [ 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 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 , 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 11 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 , forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> (a -> Bool) -> Pred fn assertReified (forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn a -> Term fn b -> Term fn (a, b) pair_ 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) forall a b. (a -> b) -> a -> b $ forall a b c. (a -> b -> c) -> (a, b) -> c uncurry forall a. Eq a => a -> a -> Bool (/=) ] reifiesMultiple :: Specification BaseFn (Int, Int, Int) reifiesMultiple :: Specification BaseFn (Int, Int, Int) reifiesMultiple = 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 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 z -> [ forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn b -> Term fn a -> (a -> b) -> Pred fn reifies (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. Num 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))))) 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 z forall a. a -> a id , 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 (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 y ] data Three = One | Two | Three deriving (Eq Three Three -> Three -> Bool Three -> Three -> Ordering Three -> Three -> Three forall a. Eq a -> (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: Three -> Three -> Three $cmin :: Three -> Three -> Three max :: Three -> Three -> Three $cmax :: Three -> Three -> Three >= :: Three -> Three -> Bool $c>= :: Three -> Three -> Bool > :: Three -> Three -> Bool $c> :: Three -> Three -> Bool <= :: Three -> Three -> Bool $c<= :: Three -> Three -> Bool < :: Three -> Three -> Bool $c< :: Three -> Three -> Bool compare :: Three -> Three -> Ordering $ccompare :: Three -> Three -> Ordering Ord, Three -> Three -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Three -> Three -> Bool $c/= :: Three -> Three -> Bool == :: Three -> Three -> Bool $c== :: Three -> Three -> Bool Eq, Int -> Three -> ShowS [Three] -> ShowS Three -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Three] -> ShowS $cshowList :: [Three] -> ShowS show :: Three -> String $cshow :: Three -> String showsPrec :: Int -> Three -> ShowS $cshowsPrec :: Int -> Three -> ShowS Show, forall x. Rep Three x -> Three forall x. Three -> Rep Three x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a $cto :: forall x. Rep Three x -> Three $cfrom :: forall x. Three -> Rep Three x Generic) instance HasSimpleRep Three instance BaseUniverse fn => HasSpec fn Three trueSpecUniform :: Specification BaseFn Three trueSpecUniform :: Specification BaseFn Three trueSpecUniform = 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 Three o -> forall (fn :: [*] -> * -> *). ((forall a. Term fn a -> a) -> Property -> Property) -> Pred fn monitor forall a b. (a -> b) -> a -> b $ \forall 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))))) a -> a eval -> forall prop. Testable prop => Double -> Bool -> String -> prop -> Property QC.cover Double 30 Bool True (forall a. Show a => a -> String show forall a b. (a -> b) -> a -> b $ forall 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))))) a -> a eval Term BaseFn Three o) three :: Specification BaseFn Three three :: Specification BaseFn Three three = 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 Three o -> [ 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 BaseFn Three o (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => Int -> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branchW Int 1 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 True) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => Int -> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branchW Int 1 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 True) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => Int -> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branchW Int 1 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 True) , forall (fn :: [*] -> * -> *). ((forall a. Term fn a -> a) -> Property -> Property) -> Pred fn monitor forall a b. (a -> b) -> a -> b $ \forall 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))))) a -> a eval -> forall prop. Testable prop => Double -> Bool -> String -> prop -> Property QC.cover Double 30 Bool True (forall a. Show a => a -> String show forall a b. (a -> b) -> a -> b $ forall 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))))) a -> a eval Term BaseFn Three o) ] three' :: Specification BaseFn Three three' :: Specification BaseFn Three three' = Specification BaseFn Three three forall a. Semigroup a => a -> a -> a <> Specification BaseFn Three three threeSpecific :: Specification BaseFn Three threeSpecific :: Specification BaseFn Three threeSpecific = 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 Three o -> [ 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 BaseFn Three o (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => Int -> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branchW Int 1 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 True) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => Int -> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branchW Int 1 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 True) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => Int -> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branchW Int 2 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 True) , forall (fn :: [*] -> * -> *). ((forall a. Term fn a -> a) -> Property -> Property) -> Pred fn monitor forall a b. (a -> b) -> a -> b $ \forall 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))))) a -> a eval -> forall prop. Testable prop => String -> [(String, Double)] -> prop -> Property QC.coverTable String "TheValue" [(String "One", Double 22), (String "Two", Double 22), (String "Three", Double 47)] forall b c a. (b -> c) -> (a -> b) -> a -> c . forall prop. Testable prop => String -> [String] -> prop -> Property QC.tabulate String "TheValue" [forall a. Show a => a -> String show forall a b. (a -> b) -> a -> b $ forall 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))))) a -> a eval Term BaseFn Three o] ] threeSpecific' :: Specification BaseFn Three threeSpecific' :: Specification BaseFn Three threeSpecific' = Specification BaseFn Three threeSpecific forall a. Semigroup a => a -> a -> a <> Specification BaseFn Three threeSpecific posNegDistr :: Specification BaseFn Int posNegDistr :: Specification BaseFn Int posNegDistr = 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 :: [*] -> * -> *). ((forall a. Term fn a -> a) -> Property -> Property) -> Pred fn monitor forall a b. (a -> b) -> a -> b $ \forall 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))))) a -> a eval -> forall prop. Testable prop => Double -> Bool -> String -> prop -> Property QC.cover Double 60 (Int 0 forall a. Ord a => a -> a -> Bool < forall 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))))) a -> a eval Term BaseFn Int x) String "x positive" , Term BaseFn Int x forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn `satisfies` forall (fn :: [*] -> * -> *) a. HasSpec fn a => (Int, Specification fn a) -> (Int, Specification fn a) -> Specification fn a chooseSpec (Int 1, forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained (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)) (Int 2, forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained (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 <.)) ] ifElseMany :: Specification BaseFn (Bool, Int, Int) ifElseMany :: Specification BaseFn (Bool, Int, Int) ifElseMany = 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))))) Bool 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 -> forall (fn :: [*] -> * -> *) p q. (BaseUniverse fn, IsPred p fn, IsPred q fn) => Term fn Bool -> p -> q -> Pred fn ifElse 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 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 :: [*] -> * -> *). (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 , 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 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 ] [ 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 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 10 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 ] propBack :: Specification BaseFn (Int, Int) propBack :: Specification BaseFn (Int, Int) propBack = 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 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 (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))))) Int y forall a. Num 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))))) Int 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))))) 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 20 , 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 8 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 ] propBack' :: Specification BaseFn (Int, Int) propBack' :: Specification BaseFn (Int, Int) propBack' = 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 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 y 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))))) Int x forall a. Num 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))))) Int 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))))) Int 20 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 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 8 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 , 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 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 x forall a. Num 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))))) Int 20 ] propBack'' :: Specification BaseFn (Int, Int) propBack'' :: Specification BaseFn (Int, Int) propBack'' = 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 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 -> [ 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 y forall a. Num 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))))) Int 10 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))))) 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 (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 y , 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 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 20 , 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 8 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 ] chooseBackwards :: Specification BaseFn (Int, [Int]) chooseBackwards :: Specification BaseFn (Int, [Int]) chooseBackwards = 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, [Int]) xy -> [ forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ Term BaseFn (Int, [Int]) xy 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 [(Int 1, [Int 1001 .. Int 1005]), (Int 2, [Int 1006 .. Int 1010])] , 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 BaseFn (Int, [Int]) xy 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] ys -> 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] ys 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 ] chooseBackwards' :: Specification BaseFn ([(Int, [Int])], (Int, [Int])) chooseBackwards' :: Specification BaseFn ([(Int, [Int])], (Int, [Int])) chooseBackwards' = 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, [Int])] [var| xys |] 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]) [var| xy |] -> [ 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))))) [(Int, [Int])] xys 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] [var| ys |] -> 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] ys 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 [var| 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 1000 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 , 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))))) 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] => Term fn [a] -> Term fn Integer length_ 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])] xys , 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, [Int]) xy 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, [Int])] xys , 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]) xy 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] [var| ys |] -> 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] ys 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 [var| 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 ] whenTrueExists :: Specification BaseFn Int whenTrueExists :: Specification BaseFn Int whenTrueExists = 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) => Term fn Bool -> p -> Pred fn whenTrue ([var| x |] 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))))) Int 0) forall a b. (a -> b) -> a -> b $ forall a p (fn :: [*] -> * -> *). (HasSpec fn a, IsPred p fn) => ((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn exists (\forall 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))))) a -> a _ -> forall (f :: * -> *) a. Applicative f => a -> f a pure Bool False) 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 b -> [ forall (fn :: [*] -> * -> *). BaseUniverse fn => Term fn Bool -> Term fn Bool not_ [var| b |] , forall (fn :: [*] -> * -> *). BaseUniverse fn => Term fn Bool -> Term fn Bool not_ (forall (fn :: [*] -> * -> *). BaseUniverse fn => Term fn Bool -> Term fn Bool not_ 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 b) ]