{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-} module Constrained.Examples.Map where import Data.Map (Map) import Data.Map qualified as Map import Data.Set (Set) import Data.Set qualified as Set import Data.Word import Constrained import Constrained.Examples.Basic mapElemSpec :: Specification BaseFn (Map Int (Bool, Int)) mapElemSpec :: Specification BaseFn (Map Int (Bool, Int)) mapElemSpec = forall a (fn :: Univ) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Map Int (Bool, Int)) m -> [ forall (fn :: Univ) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ Term BaseFn (Map Int (Bool, Int)) m forall (fn :: Univ) a. HasSpec fn a => Term fn a -> Term fn a -> Term fn Bool /=. forall a (fn :: Univ). Show a => a -> Term fn a lit forall a. Monoid a => a mempty , forall (fn :: Univ) 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' (forall (fn :: Univ) k v. (HasSpec fn k, HasSpec fn v, Ord k) => Term fn (Map k v) -> Term fn [v] rng_ Term BaseFn (Map Int (Bool, Int)) m) 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 _ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int b -> [Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int 0 forall a (fn :: Univ). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int b, Term (Fix (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 a (fn :: Univ). (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] ] mapPairSpec :: Specification BaseFn (Map Int Int, Set Int) mapPairSpec :: Specification BaseFn (Map Int Int, Set Int) mapPairSpec = forall a (fn :: Univ) 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))))) (Map Int Int) m Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set Int) s -> forall (fn :: Univ) a. (HasSpec fn a, Ord a) => Term fn (Set a) -> Term fn (Set a) -> Term fn Bool subset_ (forall (fn :: Univ) k v. (HasSpec fn (Map k v), HasSpec fn k, Ord k) => Term fn (Map k v) -> Term fn (Set k) dom_ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Map Int Int) m) Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set Int) s mapEmptyDomainSpec :: Specification BaseFn (Map Int Int) mapEmptyDomainSpec :: Specification BaseFn (Map Int Int) mapEmptyDomainSpec = forall a (fn :: Univ) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Map Int Int) m -> forall (fn :: Univ) a. (HasSpec fn a, Ord a) => Term fn (Set a) -> Term fn (Set a) -> Term fn Bool subset_ (forall (fn :: Univ) k v. (HasSpec fn (Map k v), HasSpec fn k, Ord k) => Term fn (Map k v) -> Term fn (Set k) dom_ Term BaseFn (Map Int Int) m) forall a. Monoid a => a mempty -- mempty in the Monoid instance (Term fn (Set a)) mapSubSize :: Specification BaseFn (Map Int Int) mapSubSize :: Specification BaseFn (Map Int Int) mapSubSize = forall a (fn :: Univ) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Map Int 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 :: Univ) 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 :: Univ). (HasSpec fn a, Sized a) => Term fn a -> Term fn Integer sizeOf_ Term BaseFn (Map Int Int) s) knownDomainMap :: Specification BaseFn (Map Int Int) knownDomainMap :: Specification BaseFn (Map Int Int) knownDomainMap = forall a (fn :: Univ) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Map Int Int) m -> [ forall (fn :: Univ) k v. (HasSpec fn (Map k v), HasSpec fn k, Ord k) => Term fn (Map k v) -> Term fn (Set k) dom_ Term BaseFn (Map Int Int) m forall (fn :: Univ) a. HasSpec fn a => Term fn a -> Term fn a -> Term fn Bool ==. forall a (fn :: Univ). Show a => a -> Term fn a lit (forall a. Ord a => [a] -> Set a Set.fromList [Int 1, Int 2]) , forall (fn :: Univ). BaseUniverse fn => Term fn Bool -> Term fn Bool not_ 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 :: Univ). HasSpec fn a => Term fn a -> Term fn [a] -> Term fn Bool `elem_` forall (fn :: Univ) k v. (HasSpec fn k, HasSpec fn v, Ord k) => Term fn (Map k v) -> Term fn [v] rng_ Term BaseFn (Map Int Int) m ] mapSizeConstrained :: Specification BaseFn (Map Three Int) mapSizeConstrained :: Specification BaseFn (Map Three Int) mapSizeConstrained = forall a (fn :: Univ) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Map Three Int) m -> forall a (fn :: Univ). (HasSpec fn (Set a), Ord a) => Term fn (Set a) -> Term fn Integer size_ (forall (fn :: Univ) k v. (HasSpec fn (Map k v), HasSpec fn k, Ord k) => Term fn (Map k v) -> Term fn (Set k) dom_ Term BaseFn (Map Three Int) m) forall a (fn :: Univ). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Integer 3 sumRange :: Specification BaseFn (Map Word64 Word64) sumRange :: Specification BaseFn (Map Word64 Word64) sumRange = forall a (fn :: Univ) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Map Word64 Word64) m -> forall (fn :: Univ) a. (BaseUniverse fn, Member (FunFn fn) fn, Foldy fn a) => Term fn [a] -> Term fn a sum_ (forall (fn :: Univ) k v. (HasSpec fn k, HasSpec fn v, Ord k) => Term fn (Map k v) -> Term fn [v] rng_ Term BaseFn (Map Word64 Word64) m) forall (fn :: Univ) a. HasSpec fn a => Term fn a -> Term fn a -> Term fn Bool ==. forall a (fn :: Univ). Show a => a -> Term fn a lit Word64 10 fixedRange :: Specification BaseFn (Map Int Int) fixedRange :: Specification BaseFn (Map Int Int) fixedRange = forall a (fn :: Univ) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Map Int Int) m -> [ forall t a (fn :: Univ) 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 :: Univ) k v. (HasSpec fn k, HasSpec fn v, Ord k) => Term fn (Map k v) -> Term fn [v] rng_ Term BaseFn (Map Int Int) m) (\Term (Fix (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 :: Univ) 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 5) , forall (fn :: Univ) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ (forall a (fn :: Univ). (HasSpec fn a, Sized a) => Term fn a -> Term fn Integer sizeOf_ Term BaseFn (Map Int Int) m) forall (fn :: Univ) 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 1 ] rangeHint :: Specification BaseFn (Map Int Int) rangeHint :: Specification BaseFn (Map Int Int) rangeHint = forall a (fn :: Univ) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Map Int Int) m -> forall (fn :: Univ) t. HasGenHint fn t => Hint t -> Term fn t -> Pred fn genHint Integer 10 (forall (fn :: Univ) k v. (HasSpec fn k, HasSpec fn v, Ord k) => Term fn (Map k v) -> Term fn [v] rng_ Term BaseFn (Map Int Int) m) rangeSumSize :: Specification BaseFn (Map Int Int) rangeSumSize :: Specification BaseFn (Map Int Int) rangeSumSize = forall a (fn :: Univ) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Map Int Int) m -> [ forall (fn :: Univ) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ forall a (fn :: Univ). (HasSpec fn a, Sized a) => Term fn a -> Term fn Integer sizeOf_ Term BaseFn (Map Int Int) m forall a (fn :: Univ). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Integer 0 , forall (fn :: Univ) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ forall (fn :: Univ) a. (BaseUniverse fn, Member (FunFn fn) fn, Foldy fn a) => Term fn [a] -> Term fn a sum_ (forall (fn :: Univ) k v. (HasSpec fn k, HasSpec fn v, Ord k) => Term fn (Map k v) -> Term fn [v] rng_ Term BaseFn (Map Int Int) m) forall a (fn :: Univ). (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 :: Univ) 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 1) forall a (fn :: Univ). (Ord a, OrdLike fn a) => Term fn a -> Term fn a -> Term fn Bool <=. forall (fn :: Univ) a. (BaseUniverse fn, Member (FunFn fn) fn, Foldy fn a) => Term fn [a] -> Term fn a sum_ (forall (fn :: Univ) k v. (HasSpec fn k, HasSpec fn v, Ord k) => Term fn (Map k v) -> Term fn [v] rng_ Term BaseFn (Map Int Int) m) , forall (fn :: Univ) t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t, HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn, IsProd (SimpleRep a), HasSpec fn a) => Term fn t -> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn forAll' Term BaseFn (Map Int Int) m 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 k Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int v -> [ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int k forall (fn :: Univ) 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 v forall (fn :: Univ) 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 ] ] elemSpec :: Specification BaseFn (Int, Int, Map Int Int) elemSpec :: Specification BaseFn (Int, Int, Map Int Int) elemSpec = forall a (fn :: Univ) 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 k Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int v Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Map Int Int) m -> [ forall (fn :: Univ) 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 k forall a (fn :: Univ). (HasSpec fn a, Ord a) => Term fn a -> Term fn (Set a) -> Term fn Bool `member_` forall (fn :: Univ) k v. (HasSpec fn (Map k v), HasSpec fn k, Ord k) => Term fn (Map k v) -> Term fn (Set k) dom_ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Map Int Int) m , forall (fn :: Univ) 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))))) (Map Int Int) m 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 k' Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int v' -> forall (fn :: Univ) p. (BaseUniverse fn, IsPred p fn) => Term fn Bool -> p -> Pred fn whenTrue (Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int k' forall (fn :: Univ) 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 k) (Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int v' forall (fn :: Univ) 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 v) , Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Map Int Int) m forall (fn :: Univ) 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 k ] lookupSpecific :: Specification BaseFn (Int, Int, Map Int Int) lookupSpecific :: Specification BaseFn (Int, Int, Map Int Int) lookupSpecific = forall a (fn :: Univ) 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 k Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int v Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Map Int Int) m -> [ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Map Int Int) m forall (fn :: Univ) 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 k , forall (fn :: Univ) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ forall (fn :: Univ) k v. (HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) => Term fn k -> Term fn (Map k v) -> Term fn (Maybe v) lookup_ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int k Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Map Int Int) m forall (fn :: Univ) a. HasSpec fn a => Term fn a -> Term fn a -> Term fn Bool ==. forall (fn :: Univ) a. (HasSpec fn a, IsNormalType a) => Term fn a -> Term fn (Maybe a) cJust_ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int v ] mapRestrictedValues :: Specification BaseFn (Map (Either Int ()) Int) mapRestrictedValues :: Specification BaseFn (Map (Either Int ()) Int) mapRestrictedValues = forall a (fn :: Univ) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Map (Either Int ()) Int) m -> [ forall (fn :: Univ) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ forall a (fn :: Univ). (HasSpec fn a, Sized a) => Term fn a -> Term fn Integer sizeOf_ (forall (fn :: Univ) k v. (HasSpec fn (Map k v), HasSpec fn k, Ord k) => Term fn (Map k v) -> Term fn (Set k) dom_ Term BaseFn (Map (Either Int ()) Int) m) forall (fn :: Univ) 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 6 , forall (fn :: Univ) t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t, HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn, IsProd (SimpleRep a), HasSpec fn a) => Term fn t -> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn forAll' Term BaseFn (Map (Either Int ()) Int) m forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Either Int ()) k Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int v -> [ forall (fn :: Univ) a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) => Term fn a -> FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) caseOn Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Either Int ()) k (forall (fn :: Univ) 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 _ -> Term (Fix (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 :: Univ). (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 v) (forall (fn :: Univ) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) () _ -> Bool True) , Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int v forall (fn :: Univ) 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))))) (Either Int ()) k ] ] -- NOTE: this fails if you pick the values of the map first - you're unlikely to generate -- three values such that two of them are <= -100 and >= 100 respectively even though -- you take satisfiability of the whole elem constraint into account. This can't be fixed -- with a `dependsOn v k` because the issue is that we've generated a bunch of values -- before we ever go to generate the keys. mapRestrictedValuesThree :: Specification BaseFn (Map Three Int) mapRestrictedValuesThree :: Specification BaseFn (Map Three Int) mapRestrictedValuesThree = forall a (fn :: Univ) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Map Three Int) m -> [ forall (fn :: Univ) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ forall a (fn :: Univ). (HasSpec fn a, Sized a) => Term fn a -> Term fn Integer sizeOf_ (forall (fn :: Univ) k v. (HasSpec fn (Map k v), HasSpec fn k, Ord k) => Term fn (Map k v) -> Term fn (Set k) dom_ Term BaseFn (Map Three Int) m) forall (fn :: Univ) 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 3 , forall (fn :: Univ) t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t, HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn, IsProd (SimpleRep a), HasSpec fn a) => Term fn t -> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn forAll' Term BaseFn (Map Three Int) m 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))))) Three k Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int v -> [ forall (fn :: Univ) a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) => Term fn a -> FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) caseOn Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Three k (forall (fn :: Univ) 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))))) () _ -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int v forall a (fn :: Univ). (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 100)) (forall (fn :: Univ) 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))))) () _ -> Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int 100 forall a (fn :: Univ). (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 v) (forall (fn :: Univ) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch forall a b. (a -> b) -> a -> b $ \Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) () _ -> Bool True) , -- This is important to demonstrate the point that keys sometimes need to be solved before -- values Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int v forall (fn :: Univ) 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))))) Three k ] ] mapRestrictedValuesBool :: Specification BaseFn (Map Bool Int) mapRestrictedValuesBool :: Specification BaseFn (Map Bool Int) mapRestrictedValuesBool = forall a (fn :: Univ) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Map Bool Int) m -> [ forall (fn :: Univ) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ forall a (fn :: Univ). (HasSpec fn a, Sized a) => Term fn a -> Term fn Integer sizeOf_ (forall (fn :: Univ) k v. (HasSpec fn (Map k v), HasSpec fn k, Ord k) => Term fn (Map k v) -> Term fn (Set k) dom_ Term BaseFn (Map Bool Int) m) forall (fn :: Univ) 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 (fn :: Univ) t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t, HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn, IsProd (SimpleRep a), HasSpec fn a) => Term fn t -> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn forAll' Term BaseFn (Map Bool Int) m 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 k Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int v -> [Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int v forall (fn :: Univ) 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))))) Bool k, forall (fn :: Univ) p. (BaseUniverse fn, IsPred p fn) => Term fn Bool -> p -> Pred fn whenTrue Term (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 k (Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) Int 100 forall a (fn :: Univ). (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 v)] ] mapSetSmall :: Specification BaseFn (Map (Set Int) Int) mapSetSmall :: Specification BaseFn (Map (Set Int) Int) mapSetSmall = forall a (fn :: Univ) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term BaseFn (Map (Set Int) Int) x -> forall t a (fn :: Univ) 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 :: Univ) k v. (HasSpec fn (Map k v), HasSpec fn k, Ord k) => Term fn (Map k v) -> Term fn (Set k) dom_ Term BaseFn (Map (Set Int) 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))))) (Set Int) d -> forall (fn :: Univ) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ forall (fn :: Univ) a. (HasSpec fn a, Ord a) => Term fn (Set a) -> Term fn (Set a) -> Term fn Bool subset_ Term (Fix (Oneof (Oneof (Oneof MapFn (Oneof PairFn ListFn)) (Oneof FunFn (Oneof SetFn OrdFn))) (Oneof (Oneof SumFn (Oneof BoolFn GenericsFn)) (Oneof SizeFn (Oneof EqFn IntFn))))) (Set Int) d forall a b. (a -> b) -> a -> b $ forall a (fn :: Univ). Show a => a -> Term fn a lit (forall a. Ord a => [a] -> Set a Set.fromList [Int 3 .. Int 4]) mapIsJust :: Specification BaseFn (Int, Int) mapIsJust :: Specification BaseFn (Int, Int) mapIsJust = forall a (fn :: Univ) 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 [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 |] -> forall (fn :: Univ) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ forall (fn :: Univ) a. (HasSpec fn a, IsNormalType a) => Term fn a -> Term fn (Maybe a) cJust_ Term (Fix (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 :: Univ) a. HasSpec fn a => Term fn a -> Term fn a -> Term fn Bool ==. forall (fn :: Univ) k v. (HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) => Term fn k -> Term fn (Map k v) -> Term fn (Maybe v) lookup_ Term (Fix (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 :: Univ). Show a => a -> Term fn a lit forall a b. (a -> b) -> a -> b $ forall k a. Ord k => [(k, a)] -> Map k a Map.fromList [(Int z, Int z) | Int z <- [Int 100 .. Int 102]])