{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

module Constrained.Examples.Map where

import Constrained
import Constrained.Examples.Basic
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Word

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 (Set a), Ord a, Show a, Typeable 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 (Set a), Ord a, Show a, Typeable 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 fn 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. 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 fn 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 fn 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. 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. 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 fn 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 fn 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 fn 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 (Set a), Ord a, Show a, Typeable 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])

-- | this tests the function saturatePred
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) 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]])