{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}
#if __GLASGOW_HASKELL__ < 900
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
#endif
module Constrained.Spec.Map (MapSpec (..), defaultMapSpec, dom_, rng_, lookup_) where
import Constrained.Base
import Constrained.Core
import Constrained.GenT
import Constrained.Instances ()
import Constrained.List
import Constrained.Spec.Generics
import Constrained.Spec.Pairs
import Constrained.Univ
import Control.Monad
import Data.Foldable
import Data.List (nub)
import Data.List.NonEmpty (NonEmpty ((:|)))
import Data.List.NonEmpty qualified as NE
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
import GHC.Generics
import Prettyprinter
import Test.QuickCheck (Arbitrary (..), frequency, genericShrink, shrinkList)
instance Ord a => Sized (Map.Map a b) where
sizeOf :: Map a b -> Integer
sizeOf = forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> Int
Map.size
liftSizeSpec :: forall (fn :: [*] -> * -> *).
HasSpec fn (Map a b) =>
SizeSpec fn -> [Integer] -> Specification fn (Map a b)
liftSizeSpec SizeSpec fn
sz [Integer]
cant = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$ forall k (fn :: [*] -> * -> *) v. Ord k => MapSpec fn k v
defaultMapSpec {mapSpecSize :: Specification fn Integer
mapSpecSize = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> OrdSet a -> Specification fn a
TypeSpec SizeSpec fn
sz [Integer]
cant}
liftMemberSpec :: forall (fn :: [*] -> * -> *).
HasSpec fn (Map a b) =>
[Integer] -> Specification fn (Map a b)
liftMemberSpec [Integer]
xs = case forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty (forall a. Ord a => [a] -> [a]
nubOrd [Integer]
xs) of
Maybe (NonEmpty Integer)
Nothing -> forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"In liftMemberSpec for the (Sized Map) instance, xs is the empty list"))
Just NonEmpty Integer
ys -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$ forall k (fn :: [*] -> * -> *) v. Ord k => MapSpec fn k v
defaultMapSpec {mapSpecSize :: Specification fn Integer
mapSpecSize = forall a (fn :: [*] -> * -> *). NonEmpty a -> Specification fn a
MemberSpec NonEmpty Integer
ys}
sizeOfTypeSpec :: forall (fn :: [*] -> * -> *).
HasSpec fn (Map a b) =>
TypeSpec fn (Map a b) -> Specification fn Integer
sizeOfTypeSpec (MapSpec Maybe Integer
_ Set a
mustk [b]
mustv Specification fn Integer
size Specification fn (a, b)
_ FoldSpec fn b
_) =
forall (fn :: [*] -> * -> *) a.
OrdLike fn a =>
a -> Specification fn a
geqSpec (forall t. Sized t => t -> Integer
sizeOf Set a
mustk)
forall a. Semigroup a => a -> a -> a
<> forall (fn :: [*] -> * -> *) a.
OrdLike fn a =>
a -> Specification fn a
geqSpec (forall t. Sized t => t -> Integer
sizeOf [b]
mustv)
forall a. Semigroup a => a -> a -> a
<> Specification fn Integer
size
data MapSpec fn k v = MapSpec
{ forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> Maybe Integer
mapSpecHint :: Maybe Integer
, forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> Set k
mapSpecMustKeys :: Set k
, forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> [v]
mapSpecMustValues :: [v]
, forall (fn :: [*] -> * -> *) k v.
MapSpec fn k v -> Specification fn Integer
mapSpecSize :: Specification fn Integer
, forall (fn :: [*] -> * -> *) k v.
MapSpec fn k v -> Specification fn (k, v)
mapSpecElem :: Specification fn (k, v)
, forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> FoldSpec fn v
mapSpecFold :: FoldSpec fn v
}
deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (fn :: [*] -> * -> *) k v x.
Rep (MapSpec fn k v) x -> MapSpec fn k v
forall (fn :: [*] -> * -> *) k v x.
MapSpec fn k v -> Rep (MapSpec fn k v) x
$cto :: forall (fn :: [*] -> * -> *) k v x.
Rep (MapSpec fn k v) x -> MapSpec fn k v
$cfrom :: forall (fn :: [*] -> * -> *) k v x.
MapSpec fn k v -> Rep (MapSpec fn k v) x
Generic)
defaultMapSpec :: Ord k => MapSpec fn k v
defaultMapSpec :: forall k (fn :: [*] -> * -> *) v. Ord k => MapSpec fn k v
defaultMapSpec = forall (fn :: [*] -> * -> *) k v.
Maybe Integer
-> Set k
-> [v]
-> Specification fn Integer
-> Specification fn (k, v)
-> FoldSpec fn v
-> MapSpec fn k v
MapSpec forall a. Maybe a
Nothing forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec forall (fn :: [*] -> * -> *) a. FoldSpec fn a
NoFold
instance
( Arbitrary k
, Arbitrary v
, Arbitrary (TypeSpec fn k)
, Arbitrary (TypeSpec fn v)
, Ord k
, HasSpec fn k
, Foldy fn v
) =>
Arbitrary (MapSpec fn k v)
where
arbitrary :: Gen (MapSpec fn k v)
arbitrary =
forall (fn :: [*] -> * -> *) k v.
Maybe Integer
-> Set k
-> [v]
-> Specification fn Integer
-> Specification fn (k, v)
-> FoldSpec fn v
-> MapSpec fn k v
MapSpec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (fn :: [*] -> * -> *) a. FoldSpec fn a
NoFold), (Int
1, forall a. Arbitrary a => Gen a
arbitrary)]
shrink :: MapSpec fn k v -> [MapSpec fn k v]
shrink = forall a.
(Generic a, RecursivelyShrink (Rep a), GSubterms (Rep a) a) =>
a -> [a]
genericShrink
instance Arbitrary (FoldSpec fn (Map k v)) where
arbitrary :: Gen (FoldSpec fn (Map k v))
arbitrary = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (fn :: [*] -> * -> *) a. FoldSpec fn a
NoFold
instance
( HasSpec fn (k, v)
, HasSpec fn k
, HasSpec fn v
, HasSpec fn [v]
) =>
Pretty (WithPrec (MapSpec fn k v))
where
pretty :: forall ann. WithPrec (MapSpec fn k v) -> Doc ann
pretty (WithPrec Int
d MapSpec fn k v
s) =
forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$
Doc ann
"MapSpec"
forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [Doc ann] -> Doc ann
vsep
[ Doc ann
"hint =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow (forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> Maybe Integer
mapSpecHint MapSpec fn k v
s)
, Doc ann
"mustKeys =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow (forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> Set k
mapSpecMustKeys MapSpec fn k v
s)
, Doc ann
"mustValues =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow (forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> [v]
mapSpecMustValues MapSpec fn k v
s)
, Doc ann
"size =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall (fn :: [*] -> * -> *) k v.
MapSpec fn k v -> Specification fn Integer
mapSpecSize MapSpec fn k v
s)
, Doc ann
"elem =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall (fn :: [*] -> * -> *) k v.
MapSpec fn k v -> Specification fn (k, v)
mapSpecElem MapSpec fn k v
s)
, Doc ann
"fold =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> FoldSpec fn v
mapSpecFold MapSpec fn k v
s)
]
instance
( HasSpec fn (k, v)
, HasSpec fn k
, HasSpec fn v
, HasSpec fn [v]
) =>
Show (MapSpec fn k v)
where
showsPrec :: Int -> MapSpec fn k v -> ShowS
showsPrec Int
d = forall a. Show a => a -> ShowS
shows forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
d
instance Ord k => Forallable (Map k v) (k, v) where
fromForAllSpec :: forall (fn :: [*] -> * -> *).
(HasSpec fn (Map k v), HasSpec fn (k, v), BaseUniverse fn) =>
Specification fn (k, v) -> Specification fn (Map k v)
fromForAllSpec Specification fn (k, v)
kvs = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$ forall k (fn :: [*] -> * -> *) v. Ord k => MapSpec fn k v
defaultMapSpec {mapSpecElem :: Specification fn (k, v)
mapSpecElem = Specification fn (k, v)
kvs}
forAllToList :: Map k v -> [(k, v)]
forAllToList = forall k a. Map k a -> [(k, a)]
Map.toList
instance
(Ord k, HasSpec fn (Prod k v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) =>
HasSpec fn (Map k v)
where
type TypeSpec fn (Map k v) = MapSpec fn k v
type Prerequisites fn (Map k v) = (HasSpec fn k, HasSpec fn v)
emptySpec :: TypeSpec fn (Map k v)
emptySpec = forall k (fn :: [*] -> * -> *) v. Ord k => MapSpec fn k v
defaultMapSpec
combineSpec :: TypeSpec fn (Map k v)
-> TypeSpec fn (Map k v) -> Specification fn (Map k v)
combineSpec
(MapSpec Maybe Integer
mHint Set k
mustKeys [v]
mustVals Specification fn Integer
size Specification fn (k, v)
kvs FoldSpec fn v
foldSpec)
(MapSpec Maybe Integer
mHint' Set k
mustKeys' [v]
mustVals' Specification fn Integer
size' Specification fn (k, v)
kvs' FoldSpec fn v
foldSpec') = case forall (fn :: [*] -> * -> *) a.
FoldSpec fn a -> FoldSpec fn a -> Either [String] (FoldSpec fn a)
combineFoldSpec FoldSpec fn v
foldSpec FoldSpec fn v
foldSpec' of
Left [String]
msgs ->
forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec forall a b. (a -> b) -> a -> b
$
forall a. [a] -> NonEmpty a
NE.fromList forall a b. (a -> b) -> a -> b
$
[ String
"Error in combining FoldSpec in combineSpec for Map"
, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show FoldSpec fn v
foldSpec
, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show FoldSpec fn v
foldSpec'
]
forall a. [a] -> [a] -> [a]
++ [String]
msgs
Right FoldSpec fn v
foldSpec'' ->
forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$
forall (fn :: [*] -> * -> *) k v.
Maybe Integer
-> Set k
-> [v]
-> Specification fn Integer
-> Specification fn (k, v)
-> FoldSpec fn v
-> MapSpec fn k v
MapSpec
(forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe forall a. Ord a => a -> a -> a
min Maybe Integer
mHint Maybe Integer
mHint')
(Set k
mustKeys forall a. Semigroup a => a -> a -> a
<> Set k
mustKeys')
(forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ [v]
mustVals forall a. Semigroup a => a -> a -> a
<> [v]
mustVals')
(Specification fn Integer
size forall a. Semigroup a => a -> a -> a
<> Specification fn Integer
size')
(Specification fn (k, v)
kvs forall a. Semigroup a => a -> a -> a
<> Specification fn (k, v)
kvs')
FoldSpec fn v
foldSpec''
conformsTo :: HasCallStack => Map k v -> TypeSpec fn (Map k v) -> Bool
conformsTo Map k v
m (MapSpec Maybe Integer
_ Set k
mustKeys [v]
mustVals Specification fn Integer
size Specification fn (k, v)
kvs FoldSpec fn v
foldSpec) =
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
[ Set k
mustKeys forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` forall k a. Map k a -> Set k
Map.keysSet Map k v
m
, forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall k a. Map k a -> [a]
Map.elems Map k v
m) [v]
mustVals
, forall t. Sized t => t -> Integer
sizeOf Map k v
m forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn Integer
size
, forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn (k, v)
kvs) (forall k a. Map k a -> [(k, a)]
Map.toList Map k v
m)
, forall k a. Map k a -> [a]
Map.elems Map k v
m forall (fn :: [*] -> * -> *) a. [a] -> FoldSpec fn a -> Bool
`conformsToFoldSpec` FoldSpec fn v
foldSpec
]
genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec fn (Map k v) -> GenT m (Map k v)
genFromTypeSpec (MapSpec Maybe Integer
mHint Set k
mustKeys [v]
mustVals Specification fn Integer
size (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Specification fn a
simplifySpec -> Specification fn (k, v)
kvs) FoldSpec fn v
NoFold)
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set k
mustKeys
, forall (t :: * -> *) a. Foldable t => t a -> Bool
null [v]
mustVals = do
let size' :: Specification fn Integer
size' =
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
[ forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec (forall (fn :: [*] -> * -> *) a.
OrdLike fn a =>
a -> Specification fn a
leqSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => a -> a -> a
max Integer
0) Maybe Integer
mHint
, Specification fn Integer
size
, forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Specification fn Integer -> Specification fn Integer
maxSpec (forall (fn :: [*] -> * -> *) a.
(Eq a, BaseUniverse fn, HasSpec fn a) =>
Specification fn a -> Specification fn Integer
cardinality (forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
fn '[a] b -> Specification fn a -> Specification fn b
mapSpec forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] a
fstFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
fn '[a] b -> Specification fn a -> Specification fn b
mapSpec forall (fn :: [*] -> * -> *) a.
(HasSpec fn (SimpleRep a),
TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) =>
fn '[a] (SimpleRep a)
toGenericFn Specification fn (k, v)
kvs))
, forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Specification fn Integer -> Specification fn Integer
maxSpec (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn Integer
cardinalTrueSpec @fn @k)
, forall (fn :: [*] -> * -> *) a.
OrdLike fn a =>
a -> Specification fn a
geqSpec Integer
0
]
Integer
n <- forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT Specification fn Integer
size'
let go :: Integer -> Specification fn (k, v) -> Map k v -> GenT m (Map k v)
go Integer
0 Specification fn (k, v)
_ Map k v
m = forall (f :: * -> *) a. Applicative f => a -> f a
pure Map k v
m
go Integer
n' Specification fn (k, v)
kvs' Map k v
m = do
Maybe (k, v)
mkv <- forall (m :: * -> *) a.
MonadGenError m =>
GenT GE a -> GenT m (Maybe a)
tryGenT forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT Specification fn (k, v)
kvs'
case Maybe (k, v)
mkv of
Maybe (k, v)
Nothing
| forall t. Sized t => t -> Integer
sizeOf Map k v
m forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn Integer
size -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Map k v
m
Just (k
k, v
v) ->
Integer -> Specification fn (k, v) -> Map k v -> GenT m (Map k v)
go
(Integer
n' forall a. Num a => a -> a -> a
- Integer
1)
(Specification fn (k, v)
kvs' forall a. Semigroup a => a -> a -> a
<> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec (forall (fn :: [*] -> * -> *) a b.
Specification fn a -> Specification fn b -> PairSpec fn a b
Cartesian (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a
notEqualSpec k
k) forall a. Monoid a => a
mempty))
(forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
k v
v Map k v
m)
Maybe (k, v)
_ ->
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
genError
( forall a. [a] -> NonEmpty a
NE.fromList
[ String
"Failed to generate enough elements for the map:"
, String
" m = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Map k v
m
, String
" n' = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n'
, forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
" kvs' = " forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Specification fn (k, v)
kvs'
, forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
" simplifySpec kvs' = " forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Specification fn a
simplifySpec Specification fn (k, v)
kvs')
]
)
forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain1 (String
" n = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n) forall a b. (a -> b) -> a -> b
$ Integer -> Specification fn (k, v) -> Map k v -> GenT m (Map k v)
go Integer
n Specification fn (k, v)
kvs forall a. Monoid a => a
mempty
genFromTypeSpec (MapSpec Maybe Integer
mHint Set k
mustKeys [v]
mustVals Specification fn Integer
size (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Specification fn a
simplifySpec -> Specification fn (k, v)
kvs) FoldSpec fn v
foldSpec) = do
[(k, v)]
mustMap <- forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain1 String
"Make the mustMap" forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a. Set a -> [a]
Set.toList Set k
mustKeys) forall a b. (a -> b) -> a -> b
$ \k
k -> do
let vSpec :: Specification fn v
vSpec = 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 fn v
v -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies (forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Term fn (a, b)
pair_ (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit k
k) Term fn v
v) Specification fn (k, v)
kvs
v
v <- forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain1 (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"vSpec =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Specification fn v
vSpec) forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT Specification fn v
vSpec
forall (f :: * -> *) a. Applicative f => a -> f a
pure (k
k, v
v)
let haveVals :: [v]
haveVals = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(k, v)]
mustMap
mustVals' :: [v]
mustVals' = forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [v]
haveVals) [v]
mustVals
size' :: Specification fn Integer
size' = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Specification fn a
simplifySpec 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 fn Integer
sz ->
forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies
(Term fn Integer
sz forall a. Num a => a -> a -> a
+ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit (forall t. Sized t => t -> Integer
sizeOf [(k, v)]
mustMap))
( forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec (forall (fn :: [*] -> * -> *) a.
OrdLike fn a =>
a -> Specification fn a
leqSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => a -> a -> a
max Integer
0) Maybe Integer
mHint
forall a. Semigroup a => a -> a -> a
<> Specification fn Integer
size
forall a. Semigroup a => a -> a -> a
<> forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Specification fn Integer -> Specification fn Integer
maxSpec (forall (fn :: [*] -> * -> *) a.
(Eq a, BaseUniverse fn, HasSpec fn a) =>
Specification fn a -> Specification fn Integer
cardinality (forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
fn '[a] b -> Specification fn a -> Specification fn b
mapSpec forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] a
fstFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
fn '[a] b -> Specification fn a -> Specification fn b
mapSpec forall (fn :: [*] -> * -> *) a.
(HasSpec fn (SimpleRep a),
TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) =>
fn '[a] (SimpleRep a)
toGenericFn Specification fn (k, v)
kvs))
forall a. Semigroup a => a -> a -> a
<> forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Specification fn Integer -> Specification fn Integer
maxSpec (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn Integer
cardinalTrueSpec @fn @k)
)
foldSpec' :: FoldSpec fn v
foldSpec' = case FoldSpec fn v
foldSpec of
FoldSpec fn v
NoFold -> forall (fn :: [*] -> * -> *) a. FoldSpec fn a
NoFold
FoldSpec fn '[v] b
fn Specification fn b
sumSpec -> forall b (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn b, Foldy fn b, Member (ListFn fn) fn,
BaseUniverse fn) =>
fn '[a] b -> Specification fn b -> FoldSpec fn a
FoldSpec fn '[v] b
fn forall a b. (a -> b) -> a -> b
$ forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) a b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn a,
HasSpec fn b, All (HasSpec fn) as) =>
f as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun (forall (fn :: [*] -> * -> *) a. Foldy fn a => fn '[a, a] a
theAddFn @fn) (forall a. HOLE a a
HOLE forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:? forall a. Show a => a -> Value a
Value b
mustSum forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil) Specification fn b
sumSpec
where
mustSum :: b
mustSum = forall (fn :: [*] -> * -> *) a. Foldy fn a => [a] -> a
adds @fn (forall a b. (a -> b) -> [a] -> [b]
map (forall (fn :: [*] -> * -> *) (as :: [*]) b.
FunctionLike fn =>
fn as b -> FunTy as b
sem fn '[v] b
fn) [v]
haveVals)
let valsSpec :: ListSpec fn v
valsSpec =
forall (fn :: [*] -> * -> *) a.
Maybe Integer
-> [a]
-> Specification fn Integer
-> Specification fn a
-> FoldSpec fn a
-> ListSpec fn a
ListSpec
forall a. Maybe a
Nothing
[v]
mustVals'
Specification fn Integer
size'
(forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Specification fn a
simplifySpec 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 fn v
v -> forall a p (fn :: [*] -> * -> *).
(HasSpec fn a, IsPred p fn) =>
(Term fn a -> p) -> Pred fn
unsafeExists forall a b. (a -> b) -> a -> b
$ \Term fn k
k -> forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Term fn (a, b)
pair_ Term fn k
k Term fn v
v forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn (k, v)
kvs)
FoldSpec fn v
foldSpec'
[v]
restVals <-
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explain
( forall a. [a] -> NonEmpty a
NE.fromList
[ String
"Make the restVals"
, forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
" valsSpec =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty ListSpec fn v
valsSpec
, forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
" mustMap =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow [(k, v)]
mustMap
, forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
" size' =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Specification fn Integer
size'
]
)
forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasSpec fn a, HasCallStack, MonadGenError m) =>
TypeSpec fn a -> GenT m a
genFromTypeSpec
forall a b. (a -> b) -> a -> b
$ ListSpec fn v
valsSpec
let go :: Map k v -> [v] -> GenT m (Map k v)
go Map k v
m [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure Map k v
m
go Map k v
m (v
v : [v]
restVals') = do
let keySpec :: Specification fn k
keySpec = forall (fn :: [*] -> * -> *) a (f :: * -> *).
(HasSpec fn a, Foldable f) =>
f a -> Specification fn a
notMemberSpec (forall k a. Map k a -> Set k
Map.keysSet Map k v
m) 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 (\Term fn k
k -> forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Term fn (a, b)
pair_ Term fn k
k (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit v
v) forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn (k, v)
kvs)
k
k <-
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explain
( forall a. [a] -> NonEmpty a
NE.fromList
[ String
"Make a key"
, forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall ann. Int -> Doc ann -> Doc ann
indent Int
4 forall a b. (a -> b) -> a -> b
$ Doc Any
"keySpec =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Specification fn k
keySpec
]
)
forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT Specification fn k
keySpec
Map k v -> [v] -> GenT m (Map k v)
go (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
k v
v Map k v
m) [v]
restVals'
Map k v -> [v] -> GenT m (Map k v)
go (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(k, v)]
mustMap) [v]
restVals
cardinalTypeSpec :: TypeSpec fn (Map k v) -> Specification fn Integer
cardinalTypeSpec TypeSpec fn (Map k v)
_ = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
shrinkWithTypeSpec :: TypeSpec fn (Map k v) -> Map k v -> [Map k v]
shrinkWithTypeSpec (MapSpec Maybe Integer
_ Set k
_ [v]
_ Specification fn Integer
_ Specification fn (k, v)
kvs FoldSpec fn v
_) Map k v
m = forall a b. (a -> b) -> [a] -> [b]
map forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec Specification fn (k, v)
kvs) (forall k a. Map k a -> [(k, a)]
Map.toList Map k v
m)
toPreds :: Term fn (Map k v) -> TypeSpec fn (Map k v) -> Pred fn
toPreds Term fn (Map k v)
m (MapSpec Maybe Integer
mHint Set k
mustKeys [v]
mustVals Specification fn Integer
size Specification fn (k, v)
kvs FoldSpec fn v
foldSpec) =
forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, PredLike p, UnivConstr p fn) =>
p -> Pred fn
toPred forall a b. (a -> b) -> a -> b
$
[ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Set k
mustKeys forall (fn :: [*] -> * -> *) 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 :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map k v)
m
, 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 a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit [v]
mustVals) forall a b. (a -> b) -> a -> b
$ \Term fn v
val ->
Term fn v
val forall a (fn :: [*] -> * -> *).
HasSpec fn a =>
Term fn a -> Term fn [a] -> Term fn Bool
`elem_` forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map k v)
m
, forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map k v)
m) forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn Integer
size
, 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 fn (Map k v)
m forall a b. (a -> b) -> a -> b
$ \Term fn (k, v)
kv -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (k, v)
kv Specification fn (k, v)
kvs
, forall (fn :: [*] -> * -> *) a.
BaseUniverse fn =>
Term fn [a] -> FoldSpec fn a -> Pred fn
toPredsFoldSpec (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map k v)
m) FoldSpec fn v
foldSpec
, forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall (fn :: [*] -> * -> *). Pred fn
TruePred (forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
`genHint` Term fn (Map k v)
m) Maybe Integer
mHint
]
instance
(Ord k, HasSpec fn (Prod k v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) =>
HasGenHint fn (Map k v)
where
type Hint (Map k v) = Integer
giveHint :: Hint (Map k v) -> Specification fn (Map k v)
giveHint Hint (Map k v)
h = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$ forall k (fn :: [*] -> * -> *) v. Ord k => MapSpec fn k v
defaultMapSpec {mapSpecHint :: Maybe Integer
mapSpecHint = forall a. a -> Maybe a
Just Hint (Map k v)
h}
instance BaseUniverse fn => Functions (MapFn fn) fn where
propagateSpecFun :: forall (as :: [*]) a b.
(TypeList as, Typeable as, HasSpec fn a, HasSpec fn b,
All (HasSpec fn) as) =>
MapFn fn as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun MapFn fn as b
_ ListCtx Value as (HOLE a)
_ Specification fn b
TrueSpec = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
propagateSpecFun MapFn fn as b
fn ListCtx Value as (HOLE a)
ctx (ExplainSpec [] Specification fn b
s) = forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) a b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn a,
HasSpec fn b, All (HasSpec fn) as) =>
f as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun MapFn fn as b
fn ListCtx Value as (HOLE a)
ctx Specification fn b
s
propagateSpecFun MapFn fn as b
fn ListCtx Value as (HOLE a)
ctx (ExplainSpec [String]
es Specification fn b
s) = forall (fn :: [*] -> * -> *) a.
[String] -> Specification fn a -> Specification fn a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) a b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn a,
HasSpec fn b, All (HasSpec fn) as) =>
f as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun MapFn fn as b
fn ListCtx Value as (HOLE a)
ctx Specification fn b
s
propagateSpecFun MapFn fn as b
_ ListCtx Value as (HOLE a)
_ (ErrorSpec NonEmpty String
err) = forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec NonEmpty String
err
propagateSpecFun MapFn fn as b
fn ListCtx Value as (HOLE a)
ctx Specification fn b
spec = case MapFn fn as b
fn of
MapFn fn as b
_
| SuspendedSpec Var b
v Pred fn
ps <- Specification fn b
spec
, ListCtx List Value as
pre HOLE a a
HOLE List Value as'
suf <- ListCtx Value as (HOLE a)
ctx ->
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 fn a
v' ->
let args :: List (Term fn) (Append as (a : as'))
args = forall {a} (f :: a -> *) (as :: [a]) (bs :: [a]).
List f as -> List f bs -> List f (Append as bs)
appendList (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (\(Value a
a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit a
a) List Value as
pre) (Term fn a
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (\(Value a
a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit a
a) List Value as'
suf)
in forall (fn :: [*] -> * -> *) a. Term fn a -> Binder fn a -> Pred fn
Let (forall (as :: [*]) (fn :: [*] -> * -> *) a.
(Typeable as, TypeList as, All (HasSpec fn) as, HasSpec fn a,
BaseUniverse fn) =>
fn as a -> List (Term fn) as -> Term fn a
App (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn MapFn fn as b
fn) List (Term fn) (Append as (a : as'))
args) (Var b
v forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Pred fn -> Binder fn a
:-> Pred fn
ps)
MapFn fn as b
Dom ->
case MapFn fn as b
fn of
(MapFn fn '[Map k v] (Set k)
_ :: MapFn fn '[Map k v] (Set k))
| NilCtx HOLE a (Map k v)
HOLE <- ListCtx Value as (HOLE a)
ctx
, Evidence (Prerequisites fn (Map k v))
Evidence <- forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Evidence (Prerequisites fn a)
prerequisites @fn @(Map k v) -> case Specification fn b
spec of
MemberSpec (b
s :| []) ->
forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$
forall (fn :: [*] -> * -> *) k v.
Maybe Integer
-> Set k
-> [v]
-> Specification fn Integer
-> Specification fn (k, v)
-> FoldSpec fn v
-> MapSpec fn k v
MapSpec forall a. Maybe a
Nothing b
s [] (forall a (fn :: [*] -> * -> *). a -> Specification fn a
equalSpec forall a b. (a -> b) -> a -> b
$ forall t. Sized t => t -> Integer
sizeOf b
s) forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec forall (fn :: [*] -> * -> *) a. FoldSpec fn a
NoFold
TypeSpec (SetSpec Set k
must Specification fn k
elemspec Specification fn Integer
size) [] ->
forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$
forall (fn :: [*] -> * -> *) k v.
Maybe Integer
-> Set k
-> [v]
-> Specification fn Integer
-> Specification fn (k, v)
-> FoldSpec fn v
-> MapSpec fn k v
MapSpec
forall a. Maybe a
Nothing
Set k
must
[]
Specification fn Integer
size
(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 fn (k, v)
kv -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies (forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app (forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] a
fstFn @fn) (forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app (forall (fn :: [*] -> * -> *) a.
(HasSpec fn (SimpleRep a),
TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) =>
fn '[a] (SimpleRep a)
toGenericFn @fn) Term fn (k, v)
kv)) Specification fn k
elemspec)
forall (fn :: [*] -> * -> *) a. FoldSpec fn a
NoFold
Specification fn b
_ -> forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec (forall a. [a] -> NonEmpty a
NE.fromList [String
"Dom on bad map spec", forall a. Show a => a -> String
show Specification fn b
spec])
MapFn fn as b
Rng ->
case MapFn fn as b
fn of
(MapFn fn '[Map k v] [v]
_ :: MapFn fn '[Map k v] [v])
| NilCtx HOLE a (Map k v)
HOLE <- ListCtx Value as (HOLE a)
ctx
, Evidence (Prerequisites fn (Map k v))
Evidence <- forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Evidence (Prerequisites fn a)
prerequisites @fn @(Map k v) ->
case Specification fn b
spec of
TypeSpec (ListSpec Maybe Integer
listHint [v]
must Specification fn Integer
size Specification fn v
elemspec FoldSpec fn v
foldspec) [] ->
forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$
forall (fn :: [*] -> * -> *) k v.
Maybe Integer
-> Set k
-> [v]
-> Specification fn Integer
-> Specification fn (k, v)
-> FoldSpec fn v
-> MapSpec fn k v
MapSpec
Maybe Integer
listHint
forall a. Set a
Set.empty
[v]
must
Specification fn Integer
size
(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 fn (k, v)
kv -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies (forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app (forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] b
sndFn @fn) (forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app (forall (fn :: [*] -> * -> *) a.
(HasSpec fn (SimpleRep a),
TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) =>
fn '[a] (SimpleRep a)
toGenericFn @fn) Term fn (k, v)
kv)) Specification fn v
elemspec)
FoldSpec fn v
foldspec
Specification fn b
_ -> forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec (forall a. [a] -> NonEmpty a
NE.fromList [String
"Rng on bad map spec", forall a. Show a => a -> String
show Specification fn b
spec])
MapFn fn as b
Lookup ->
case MapFn fn as b
fn of
MapFn fn '[k, Map k v] (Maybe v)
Lookup :: MapFn fn '[k, Map k v] (Maybe v)
| HOLE a a
HOLE :? Value (Map k v
m :: Map k v) :> List Value as1
Nil <- ListCtx Value as (HOLE a)
ctx ->
if forall a. Maybe a
Nothing forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn b
spec
then forall (fn :: [*] -> * -> *) a (f :: * -> *).
(HasSpec fn a, Foldable f) =>
f a -> Specification fn a
notMemberSpec [k
k | (k
k, v
v) <- forall k a. Map k a -> [(k, a)]
Map.toList Map k v
m, Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just v
v forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn b
spec]
else
forall a (fn :: [*] -> * -> *).
[a] -> NonEmpty String -> Specification fn a
memberSpecList
(forall k a. Map k a -> [k]
Map.keys forall a b. (a -> b) -> a -> b
$ forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter ((forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn b
spec) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just) Map k v
m)
( forall a. [a] -> NonEmpty a
NE.fromList
[ String
"propagateSpecFun (lookup HOLE ms) on (MemberSpec ms)"
, String
"forall pairs (d,r) in ms, no 'd' conforms to spec"
, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification fn b
spec
]
)
| Value a
k :! NilCtx HOLE a (Map k v)
HOLE <- ListCtx Value as (HOLE a)
ctx
, Evidence (Prerequisites fn (Map k v))
Evidence <- forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Evidence (Prerequisites fn a)
prerequisites @fn @(Map k v) ->
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 fn a
m ->
[forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit a
k forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
`member_` forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn a
m | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn b
spec]
forall a. [a] -> [a] -> [a]
++ [ 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 fn a
m forall a b. (a -> b) -> a -> b
$ \Term fn (a, v)
kv ->
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 fn (a, v)
kv) forall a b. (a -> b) -> a -> b
$ \Term fn a
k' ->
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 fn (a, v)
kv) forall a b. (a -> b) -> a -> b
$ \Term fn v
v ->
forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
Term fn Bool -> p -> Pred fn
whenTrue (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit a
k forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn a
k') forall a b. (a -> b) -> a -> b
$
case Specification fn b
spec of
MemberSpec NonEmpty b
as -> forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn v
v 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 [v
a | Just v
a <- forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
as]
TypeSpec (SumSpec Maybe (Int, Int)
_ Specification fn ()
_ Specification fn v
vspec) [b]
cant ->
Term fn v
v forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` (Specification fn v
vspec forall a. Semigroup a => a -> a -> a
<> forall (fn :: [*] -> * -> *) a (f :: * -> *).
(HasSpec fn a, Foldable f) =>
f a -> Specification fn a
notMemberSpec [v
a | Just v
a <- [b]
cant])
]
mapTypeSpec :: forall a b.
(HasSpec fn a, HasSpec fn b) =>
MapFn fn '[a] b -> TypeSpec fn a -> Specification fn b
mapTypeSpec MapFn fn '[a] b
f TypeSpec fn a
ts = case MapFn fn '[a] b
f of
MapFn fn '[a] b
Dom ->
case MapFn fn '[a] b
f of
(MapFn fn '[Map k v] (Set k)
_ :: MapFn fn '[Map k v] (Set k))
| MapSpec Maybe Integer
_ Set k
mustSet [v]
_ Specification fn Integer
sz Specification fn (k, v)
kvSpec FoldSpec fn v
_ <- TypeSpec fn a
ts
, Evidence (Prerequisites fn (Map k v))
Evidence <- forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Evidence (Prerequisites fn a)
prerequisites @fn @(Map k v) ->
forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
Set a
-> Specification fn a -> Specification fn Integer -> SetSpec fn a
SetSpec Set k
mustSet (forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
fn '[a] b -> Specification fn a -> Specification fn b
mapSpec (forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] a
fstFn @fn) forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Specification fn a -> Specification fn (SimpleRep a)
toSimpleRepSpec Specification fn (k, v)
kvSpec) Specification fn Integer
sz
MapFn fn '[a] b
Rng ->
case MapFn fn '[a] b
f of
(MapFn fn '[Map k v] [v]
_ :: MapFn fn '[Map k v] [v])
| MapSpec Maybe Integer
_ Set k
_ [v]
mustList Specification fn Integer
sz Specification fn (k, v)
kvSpec FoldSpec fn v
foldSpec <- TypeSpec fn a
ts
, Evidence (Prerequisites fn (Map k v))
Evidence <- forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Evidence (Prerequisites fn a)
prerequisites @fn @(Map k v) ->
forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
Maybe Integer
-> [a]
-> Specification fn Integer
-> Specification fn a
-> FoldSpec fn a
-> ListSpec fn a
ListSpec forall a. Maybe a
Nothing [v]
mustList Specification fn Integer
sz (forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
fn '[a] b -> Specification fn a -> Specification fn b
mapSpec (forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] b
sndFn @fn) forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Specification fn a -> Specification fn (SimpleRep a)
toSimpleRepSpec Specification fn (k, v)
kvSpec) FoldSpec fn v
foldSpec
dom_ ::
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) ->
Term fn (Set k)
dom_ :: forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ = forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app forall (fn :: [*] -> * -> *) k v.
(Member (MapFn fn) fn, Ord k) =>
fn '[Map k v] (Set k)
domFn
rng_ ::
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) ->
Term fn [v]
rng_ :: forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ = forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app forall (fn :: [*] -> * -> *) k v.
Member (MapFn fn) fn =>
fn '[Map k v] [v]
rngFn
lookup_ ::
(HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) =>
Term fn k ->
Term fn (Map k v) ->
Term fn (Maybe v)
lookup_ :: forall (fn :: [*] -> * -> *) 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_ = forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app forall (fn :: [*] -> * -> *) k v.
(Member (MapFn fn) fn, Ord k) =>
fn '[k, Map k v] (Maybe v)
lookupFn