{-# 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 #-}

-- The pattern completeness checker is much weaker before ghc-9.0. Rather than introducing redundant
-- cases and turning off the overlap check in newer ghc versions we disable the check for old
-- versions.
#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)

------------------------------------------------------------------------
-- HasSpec
------------------------------------------------------------------------

instance Ord a => Sized fn (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 :: HasSpec fn (Map a b) =>
SizeSpec fn -> OrdSet Integer -> Specification fn (Map a b)
liftSizeSpec SizeSpec fn
sz OrdSet 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 OrdSet Integer
cant}
  liftMemberSpec :: HasSpec fn (Map a b) =>
OrdSet Integer -> Specification fn (Map a b)
liftMemberSpec OrdSet Integer
xs = case forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty (forall a. Ord a => [a] -> [a]
nubOrd OrdSet 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 :: 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 (fn :: [*] -> * -> *) t. Sized fn 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 (fn :: [*] -> * -> *) t. Sized fn 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)

-- | emptySpec without all the constraints
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

-- TODO: consider making this more interesting to get fewer discarded tests
-- in `prop_gen_sound`
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
            -- This is min because that allows more compositionality - if a spec specifies a
            -- low upper bound because some part of the spec will be slow it doesn't make sense
            -- to increase it somewhere else because that part isn't slow.
            (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 (fn :: [*] -> * -> *) t. Sized fn 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.
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 (fn :: [*] -> * -> *) t. Sized fn 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 ->
          -- TODO, we should make sure size' is greater than or equal to 0
          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 (fn :: [*] -> * -> *) t. Sized fn 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.
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 fn 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}

------------------------------------------------------------------------
-- Functions
------------------------------------------------------------------------

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 ->
      -- No TypeAbstractions in ghc-8.10
      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 (fn :: [*] -> * -> *) t. Sized fn 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 ->
      -- No TypeAbstractions in ghc-8.10
      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
                -- NOTE: you'd think `MemberSpec [r]` was a safe and easy case. However, that requires not only that the elements
                -- of the map are fixed to what is in `r`, but they appear in the order that they are in `r`. That's
                -- very difficult to achieve!
                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
$
                              -- TODO: What you want to write is `cJust_ v `satisfies` spec` but we can't
                              -- do that because we don't have access to `IsNormalType v` here. When
                              -- we refactor the `IsNormalType` machinery we will be able to make
                              -- this nicer.
                              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])
                     ]

  -- NOTE: this function over-approximates and returns a liberal spec.
  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
    -- TODO: consider checking against singleton member-specs in the other component
    -- interacting with cant
    MapFn fn '[a] b
Dom ->
      -- No TypeAbstractions in ghc-8.10
      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 ->
      -- No TypeAbstractions in ghc-8.10
      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

------------------------------------------------------------------------
-- Syntax
------------------------------------------------------------------------

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