{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# 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 where

import Constrained.Base
import Constrained.Conformance
import Constrained.Core
import Constrained.GenT
import Constrained.Generic (Prod (..))
import Constrained.List
import Constrained.NumSpec (cardinality, geqSpec, leqSpec, nubOrd)
import Constrained.Spec.Set
import Constrained.Spec.SumProd
import Constrained.Syntax
import Constrained.TheKnot
import Control.Monad
import Data.Foldable
import Data.Kind
import Data.List (nub)
import qualified Data.List.NonEmpty as NE
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import GHC.Generics
import Prettyprinter
import Test.QuickCheck hiding (Fun, Witness, forAll)

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

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 :: HasSpec (Map a b) =>
SizeSpec -> [Integer] -> Specification (Map a b)
liftSizeSpec SizeSpec
sz [Integer]
cant = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall k v. Ord k => MapSpec k v
defaultMapSpec {mapSpecSize :: Specification Integer
mapSpecSize = forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec SizeSpec
sz [Integer]
cant}
  liftMemberSpec :: HasSpec (Map a b) => [Integer] -> Specification (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 a. NonEmpty String -> Specification 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 a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall k v. Ord k => MapSpec k v
defaultMapSpec {mapSpecSize :: Specification Integer
mapSpecSize = forall a. NonEmpty a -> Specification a
MemberSpec NonEmpty Integer
ys}
  sizeOfTypeSpec :: HasSpec (Map a b) => TypeSpec (Map a b) -> Specification Integer
sizeOfTypeSpec (MapSpec Maybe Integer
_ Set a
mustk [b]
mustv Specification Integer
size Specification (a, b)
_ FoldSpec b
_) =
    forall a. OrdLike a => a -> Specification a
geqSpec (forall t. Sized t => t -> Integer
sizeOf Set a
mustk)
      forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
geqSpec (forall t. Sized t => t -> Integer
sizeOf [b]
mustv)
      forall a. Semigroup a => a -> a -> a
<> Specification Integer
size

data MapSpec k v = MapSpec
  { forall k v. MapSpec k v -> Maybe Integer
mapSpecHint :: Maybe Integer
  , forall k v. MapSpec k v -> Set k
mapSpecMustKeys :: Set k
  , forall k v. MapSpec k v -> [v]
mapSpecMustValues :: [v]
  , forall k v. MapSpec k v -> Specification Integer
mapSpecSize :: Specification Integer
  , forall k v. MapSpec k v -> Specification (k, v)
mapSpecElem :: Specification (k, v)
  , forall k v. MapSpec k v -> FoldSpec v
mapSpecFold :: FoldSpec v
  }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k v x. Rep (MapSpec k v) x -> MapSpec k v
forall k v x. MapSpec k v -> Rep (MapSpec k v) x
$cto :: forall k v x. Rep (MapSpec k v) x -> MapSpec k v
$cfrom :: forall k v x. MapSpec k v -> Rep (MapSpec k v) x
Generic)

-- | emptySpec without all the constraints
defaultMapSpec :: Ord k => MapSpec k v
defaultMapSpec :: forall k v. Ord k => MapSpec k v
defaultMapSpec = forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec forall a. Maybe a
Nothing forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Specification a
TrueSpec forall a. Specification a
TrueSpec forall a. FoldSpec a
NoFold

-- TODO: consider making this more interesting to get fewer discarded tests
-- in `prop_gen_sound`
instance
  ( Arbitrary k
  , Arbitrary v
  , Arbitrary (TypeSpec k)
  , Arbitrary (TypeSpec v)
  , Ord k
  , HasSpec k
  , Foldy v
  ) =>
  Arbitrary (MapSpec k v)
  where
  arbitrary :: Gen (MapSpec k v)
arbitrary =
    forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec 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 a. FoldSpec a
NoFold), (Int
1, forall a. Arbitrary a => Gen a
arbitrary)]
  shrink :: MapSpec k v -> [MapSpec k v]
shrink = forall a.
(Generic a, RecursivelyShrink (Rep a), GSubterms (Rep a) a) =>
a -> [a]
genericShrink

instance Arbitrary (FoldSpec (Map k v)) where
  arbitrary :: Gen (FoldSpec (Map k v))
arbitrary = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. FoldSpec a
NoFold

instance
  ( HasSpec (k, v)
  , HasSpec k
  , HasSpec v
  , HasSpec [v]
  ) =>
  Pretty (WithPrec (MapSpec k v))
  where
  pretty :: forall ann. WithPrec (MapSpec k v) -> Doc ann
pretty (WithPrec Int
d MapSpec 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 k v. MapSpec k v -> Maybe Integer
mapSpecHint MapSpec k v
s)
          , Doc ann
"mustKeys   =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow (forall k v. MapSpec k v -> Set k
mapSpecMustKeys MapSpec k v
s)
          , Doc ann
"mustValues =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow (forall k v. MapSpec k v -> [v]
mapSpecMustValues MapSpec k v
s)
          , Doc ann
"size       =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall k v. MapSpec k v -> Specification Integer
mapSpecSize MapSpec k v
s)
          , Doc ann
"elem       =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall k v. MapSpec k v -> Specification (k, v)
mapSpecElem MapSpec k v
s)
          , Doc ann
"fold       =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall k v. MapSpec k v -> FoldSpec v
mapSpecFold MapSpec k v
s)
          ]

instance
  ( HasSpec (k, v)
  , HasSpec k
  , HasSpec v
  , HasSpec [v]
  ) =>
  Show (MapSpec k v)
  where
  showsPrec :: Int -> MapSpec 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 :: (HasSpec (Map k v), HasSpec (k, v)) =>
Specification (k, v) -> Specification (Map k v)
fromForAllSpec Specification (k, v)
kvs = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall k v. Ord k => MapSpec k v
defaultMapSpec {mapSpecElem :: Specification (k, v)
mapSpecElem = Specification (k, v)
kvs}
  forAllToList :: Map k v -> [(k, v)]
forAllToList = forall k a. Map k a -> [(k, a)]
Map.toList

-- ============================================================
-- We will need to take projections on (Specification (a,b))

fstSpec :: forall k v. (HasSpec k, HasSpec v) => Specification (k, v) -> Specification k
fstSpec :: forall k v.
(HasSpec k, HasSpec v) =>
Specification (k, v) -> Specification k
fstSpec Specification (k, v)
s = forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec forall b b1. (HasSpec b, HasSpec b1) => ProdW '[Prod b b1] b
ProdFstW (forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec forall a. GenericRequires a => BaseW '[a] (SimpleRep a)
ToGenericW Specification (k, v)
s)

sndSpec :: forall k v. (HasSpec k, HasSpec v) => Specification (k, v) -> Specification v
sndSpec :: forall k v.
(HasSpec k, HasSpec v) =>
Specification (k, v) -> Specification v
sndSpec Specification (k, v)
s = forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec forall a1 b. (HasSpec a1, HasSpec b) => ProdW '[Prod a1 b] b
ProdSndW (forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec forall a. GenericRequires a => BaseW '[a] (SimpleRep a)
ToGenericW Specification (k, v)
s)

-- ======================================================================
-- The HasSpec instance for Maps

instance
  (Ord k, HasSpec (Prod k v), HasSpec k, HasSpec v, HasSpec [v], IsNormalType k, IsNormalType v) =>
  HasSpec (Map k v)
  where
  type TypeSpec (Map k v) = MapSpec k v
  type Prerequisites (Map k v) = (HasSpec k, HasSpec v)

  emptySpec :: TypeSpec (Map k v)
emptySpec = forall k v. Ord k => MapSpec k v
defaultMapSpec

  combineSpec :: TypeSpec (Map k v) -> TypeSpec (Map k v) -> Specification (Map k v)
combineSpec
    (MapSpec Maybe Integer
mHint Set k
mustKeys [v]
mustVals Specification Integer
size Specification (k, v)
kvs FoldSpec v
foldSpec)
    (MapSpec Maybe Integer
mHint' Set k
mustKeys' [v]
mustVals' Specification Integer
size' Specification (k, v)
kvs' FoldSpec v
foldSpec') = case forall a. FoldSpec a -> FoldSpec a -> Either [String] (FoldSpec a)
combineFoldSpec FoldSpec v
foldSpec FoldSpec v
foldSpec' of
      Left [String]
msgs ->
        forall a. NonEmpty String -> Specification 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 v
foldSpec
            , String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show FoldSpec v
foldSpec'
            ]
              forall a. [a] -> [a] -> [a]
++ [String]
msgs
      Right FoldSpec v
foldSpec'' ->
        forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$
          forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec 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 Integer
size forall a. Semigroup a => a -> a -> a
<> Specification Integer
size')
            (Specification (k, v)
kvs forall a. Semigroup a => a -> a -> a
<> Specification (k, v)
kvs')
            FoldSpec v
foldSpec''

  conformsTo :: HasCallStack => Map k v -> TypeSpec (Map k v) -> Bool
conformsTo Map k v
m (MapSpec Maybe Integer
_ Set k
mustKeys [v]
mustVals Specification Integer
size Specification (k, v)
kvs FoldSpec 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 a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification Integer
size
      , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification (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 a. [a] -> FoldSpec a -> Bool
`conformsToFoldSpec` FoldSpec v
foldSpec
      ]

  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec (Map k v) -> GenT m (Map k v)
genFromTypeSpec (MapSpec Maybe Integer
mHint Set k
mustKeys [v]
mustVals Specification Integer
size (forall a. HasSpec a => Specification a -> Specification a
simplifySpec -> Specification (k, v)
kvs) FoldSpec 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 Integer
size' =
              forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
                [ forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Specification a
TrueSpec (forall a. OrdLike a => a -> Specification 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 Integer
size
                , Specification Integer -> Specification Integer
maxSpec (forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality (forall k v.
(HasSpec k, HasSpec v) =>
Specification (k, v) -> Specification k
fstSpec Specification (k, v)
kvs)) -- (mapSpec FstW  (mapSpec ToGenericW kvs)))
                , Specification Integer -> Specification Integer
maxSpec (forall a. HasSpec a => Specification Integer
cardinalTrueSpec @k)
                , forall a. OrdLike a => a -> Specification a
geqSpec Integer
0
                ]
        Integer
n <- forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification Integer
size'
        let go :: Integer -> Specification (k, v) -> Map k v -> GenT m (Map k v)
go Integer
0 Specification (k, v)
_ Map k v
m = forall (f :: * -> *) a. Applicative f => a -> f a
pure Map k v
m
            go Integer
n' Specification (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 a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification (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 a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification Integer
size -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Map k v
m
                Just (k
k, v
v) ->
                  Integer -> Specification (k, v) -> Map k v -> GenT m (Map k v)
go
                    (Integer
n' forall a. Num a => a -> a -> a
- Integer
1)
                    (Specification (k, v)
kvs' forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall a b. Specification a -> Specification b -> PairSpec a b
Cartesian (forall a. HasSpec a => a -> Specification 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
genErrorNE
                    ( 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 (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 a. HasSpec a => Specification a -> Specification a
simplifySpec Specification (k, v)
kvs')
                        ]
                    )
        forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain (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 (k, v) -> Map k v -> GenT m (Map k v)
go Integer
n Specification (k, v)
kvs forall a. Monoid a => a
mempty
  genFromTypeSpec (MapSpec Maybe Integer
mHint Set k
mustKeys [v]
mustVals Specification Integer
size (forall a. HasSpec a => Specification a -> Specification a
simplifySpec -> Specification (k, v)
kvs) FoldSpec v
foldSpec) = do
    ![(k, v)]
mustMap <- forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain 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 v
vSpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term v
v -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ (forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit k
k) Term v
v) Specification (k, v)
kvs
      v
v <- forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain (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 v
vSpec) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification v
vSpec
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (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 Integer
size' = forall a. HasSpec a => Specification a -> Specification a
simplifySpec forall a b. (a -> b) -> a -> b
$ forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Integer
sz ->
          -- TODO, we should make sure size' is greater than or equal to 0
          forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
            (Term Integer
sz forall a. Num a => a -> a -> a
+ forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit (forall t. Sized t => t -> Integer
sizeOf [(k, v)]
mustMap))
            ( forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Specification a
TrueSpec (forall a. OrdLike a => a -> Specification 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 Integer
size
                forall a. Semigroup a => a -> a -> a
<> Specification Integer -> Specification Integer
maxSpec (forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality (forall k v.
(HasSpec k, HasSpec v) =>
Specification (k, v) -> Specification k
fstSpec Specification (k, v)
kvs)) -- (mapSpec FstW $ mapSpec ToGenericW kvs))
                forall a. Semigroup a => a -> a -> a
<> Specification Integer -> Specification Integer
maxSpec (forall a. HasSpec a => Specification Integer
cardinalTrueSpec @k)
            )
        !foldSpec' :: FoldSpec v
foldSpec' = case FoldSpec v
foldSpec of
          FoldSpec v
NoFold -> forall a. FoldSpec a
NoFold
          FoldSpec fn :: Fun '[v] b
fn@(Fun t '[v] b
symbol) Specification b
sumSpec -> forall b a.
(HasSpec a, HasSpec b, Foldy b) =>
Fun '[a] b -> Specification b -> FoldSpec a
FoldSpec Fun '[v] b
fn forall a b. (a -> b) -> a -> b
$ forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate forall a. Foldy a => IntW '[a, a] a
theAddFn (forall {k} (a :: k). 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 b
sumSpec
            where
              mustSum :: b
mustSum = forall a. Foldy a => [a] -> a
adds (forall a b. (a -> b) -> [a] -> [b]
map (forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t '[v] b
symbol) [v]
haveVals)
    let !valsSpec :: ListSpec v
valsSpec =
          forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec
            forall a. Maybe a
Nothing
            [v]
mustVals'
            Specification Integer
size'
            (forall a. HasSpec a => Specification a -> Specification a
simplifySpec forall a b. (a -> b) -> a -> b
$ forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term v
v -> forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists forall a b. (a -> b) -> a -> b
$ \Term k
k -> forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term k
k Term v
v forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (k, v)
kvs)
            FoldSpec v
foldSpec'

    ![v]
restVals <-
      forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
        ( 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 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 Integer
size'
            ]
        )
        forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(HasSpec a, HasCallStack, MonadGenError m) =>
TypeSpec a -> GenT m a
genFromTypeSpec
        forall a b. (a -> b) -> a -> b
$ ListSpec 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 k
keySpec = forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification 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 p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained (\Term k
k -> forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term k
k (forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit v
v) forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (k, v)
kvs)
          k
k <-
            forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
              ( 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 k
keySpec
                  ]
              )
              forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification 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 (Map k v) -> Specification Integer
cardinalTypeSpec TypeSpec (Map k v)
_ = forall a. Specification a
TrueSpec

  shrinkWithTypeSpec :: TypeSpec (Map k v) -> Map k v -> [Map k v]
shrinkWithTypeSpec (MapSpec Maybe Integer
_ Set k
_ [v]
_ Specification Integer
_ Specification (k, v)
kvs FoldSpec 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 a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification (k, v)
kvs) (forall k a. Map k a -> [(k, a)]
Map.toList Map k v
m)

  toPreds :: Term (Map k v) -> TypeSpec (Map k v) -> Pred
toPreds Term (Map k v)
m (MapSpec Maybe Integer
mHint Set k
mustKeys [v]
mustVals Specification Integer
size Specification (k, v)
kvs FoldSpec v
foldSpec) =
    forall p. IsPred p => p -> Pred
toPred forall a b. (a -> b) -> a -> b
$
      [ Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Set k
mustKeys forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map k v)
m
      , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit [v]
mustVals) forall a b. (a -> b) -> a -> b
$ \Term v
val ->
          Term v
val forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map k v)
m
      , forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map k v)
m) forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification Integer
size
      , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map k v)
m forall a b. (a -> b) -> a -> b
$ \Term (k, v)
kv -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (k, v)
kv Specification (k, v)
kvs
      , forall a. HasSpec a => Term [a] -> FoldSpec a -> Pred
toPredsFoldSpec (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map k v)
m) FoldSpec v
foldSpec
      , forall b a. b -> (a -> b) -> Maybe a -> b
maybe Pred
TruePred (forall t. HasGenHint t => Hint t -> Term t -> Pred
`genHint` Term (Map k v)
m) Maybe Integer
mHint
      ]

instance
  (Ord k, HasSpec k, HasSpec v, HasSpec [v], IsNormalType k, IsNormalType v) =>
  HasGenHint (Map k v)
  where
  type Hint (Map k v) = Integer
  giveHint :: Hint (Map k v) -> Specification (Map k v)
giveHint Hint (Map k v)
h = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall k v. Ord k => MapSpec k v
defaultMapSpec {mapSpecHint :: Maybe Integer
mapSpecHint = forall a. a -> Maybe a
Just Hint (Map k v)
h}

------------------------------------------------------------------------
-- Logic instances for
------------------------------------------------------------------------

data MapW (dom :: [Type]) (rng :: Type) where
  DomW :: (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) => MapW '[Map k v] (Set k)
  RngW :: (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) => MapW '[Map k v] [v]
  LookupW ::
    (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) => MapW '[k, Map k v] (Maybe v)

deriving instance Eq (MapW dom rng)

mapSem :: MapW d r -> FunTy d r
mapSem :: forall (d :: [*]) r. MapW d r -> FunTy d r
mapSem MapW d r
DomW = forall k a. Map k a -> Set k
Map.keysSet
mapSem MapW d r
RngW = forall k a. Map k a -> [a]
Map.elems
mapSem MapW d r
LookupW = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup

instance Semantics MapW where
  semantics :: forall (d :: [*]) r. MapW d r -> FunTy d r
semantics = forall (d :: [*]) r. MapW d r -> FunTy d r
mapSem

instance Syntax MapW

instance Show (MapW d r) where
  show :: MapW d r -> String
show MapW d r
DomW = String
"dom_"
  show MapW d r
RngW = String
"rng_"
  show MapW d r
LookupW = String
"lookup_"

-- ============ DomW

instance Logic MapW where
  propagate :: forall (as :: [*]) b a.
(AppRequires MapW as b, HasSpec a) =>
MapW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate MapW as b
f ListCtx Value as (HOLE a)
ctxt (ExplainSpec [String]
es Specification b
s) = forall a. [String] -> Specification a -> Specification a
explainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate MapW as b
f ListCtx Value as (HOLE a)
ctxt Specification b
s
  propagate MapW as b
_ ListCtx Value as (HOLE a)
_ Specification b
TrueSpec = forall a. Specification a
TrueSpec
  propagate MapW as b
_ ListCtx Value as (HOLE a)
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate MapW as b
f ListCtx Value as (HOLE a)
ctx (SuspendedSpec Var b
v Pred
ps) = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term a
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App MapW as b
f (forall (as :: [*]) a.
All HasSpec as =>
ListCtx Value as (HOLE a) -> Term a -> List Term as
fromListCtx ListCtx Value as (HOLE a)
ctx Term a
v')) (Var b
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate MapW as b
DomW (Unary HOLE a (Map k v)
HOLE) Specification b
spec =
    case Specification b
spec of
      MemberSpec (b
s :| []) ->
        forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$
          forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec forall a. Maybe a
Nothing b
s [] (forall a. a -> Specification a
equalSpec forall a b. (a -> b) -> a -> b
$ forall t. Sized t => t -> Integer
sizeOf b
s) forall a. Specification a
TrueSpec forall a. FoldSpec a
NoFold
      TypeSpec (SetSpec Set k
must Specification k
elemspec Specification Integer
size) [] ->
        forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$
          forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec
            forall a. Maybe a
Nothing
            Set k
must
            []
            Specification Integer
size
            (forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (k, v)
kv -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (k, v)
kv) Specification k
elemspec)
            forall a. FoldSpec a
NoFold
      Specification b
_ -> forall a. NonEmpty String -> Specification a
ErrorSpec (forall a. [a] -> NonEmpty a
NE.fromList [String
"Dom on bad map spec", forall a. Show a => a -> String
show Specification b
spec])
  propagate MapW as b
RngW (Unary HOLE a (Map k v)
HOLE) Specification b
spec =
    case Specification b
spec of
      TypeSpec (ListSpec Maybe Integer
listHint [v]
must Specification Integer
size Specification v
elemspec FoldSpec v
foldspec) [] ->
        forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$
          forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec
            Maybe Integer
listHint
            forall a. Set a
Set.empty
            [v]
must
            Specification Integer
size
            (forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (k, v)
kv -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (k, v)
kv) Specification v
elemspec)
            FoldSpec 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 b
_ -> forall a. NonEmpty String -> Specification a
ErrorSpec (forall a. [a] -> NonEmpty a
NE.fromList [String
"Rng on bad map spec", forall a. Show a => a -> String
show Specification b
spec])
  propagate MapW as b
LookupW (Value a
k :! Unary HOLE a (Map k v)
HOLE) Specification b
spec =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term a
m ->
      [Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
k forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term a
m | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification b
spec]
        forall a. [a] -> [a] -> [a]
++ [ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term a
m forall a b. (a -> b) -> a -> b
$ \Term (a, v)
kv ->
              forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (a, v)
kv) forall a b. (a -> b) -> a -> b
$ \Term a
k' ->
                forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (a, v)
kv) forall a b. (a -> b) -> a -> b
$ \Term v
v ->
                  forall p. IsPred p => Term Bool -> p -> Pred
whenTrue (forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
k forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term 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 b
spec of
                      MemberSpec NonEmpty b
as -> Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ Term v
v forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit [v
a | Just v
a <- forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
as]
                      TypeSpec (SumSpec Maybe (Int, Int)
_ Specification ()
_ Specification v
vspec) [b]
cant ->
                        Term v
v forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` (Specification v
vspec forall a. Semigroup a => a -> a -> a
<> forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec [v
a | Just v
a <- [b]
cant])
           ]
  propagate MapW as b
LookupW (HOLE a a
HOLE :? Value a
m :> List Value as1
Nil) Specification b
spec =
    if forall a. Maybe a
Nothing forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification b
spec
      then forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec [a
k | (a
k, v
v) <- forall k a. Map k a -> [(k, a)]
Map.toList a
m, Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just v
v forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification b
spec]
      else
        forall a. [a] -> NonEmpty String -> Specification 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 a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification b
spec) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just) a
m)
          ( forall a. [a] -> NonEmpty a
NE.fromList
              [ String
"propagate (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 b
spec
              ]
          )

  mapTypeSpec :: forall a b.
(HasSpec a, HasSpec b) =>
MapW '[a] b -> TypeSpec a -> Specification b
mapTypeSpec MapW '[a] b
DomW (MapSpec Maybe Integer
_ Set k
mustSet [v]
_ Specification Integer
sz Specification (k, v)
kvSpec FoldSpec v
_) = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec Set k
mustSet (forall k v.
(HasSpec k, HasSpec v) =>
Specification (k, v) -> Specification k
fstSpec Specification (k, v)
kvSpec) Specification Integer
sz
  mapTypeSpec MapW '[a] b
RngW (MapSpec Maybe Integer
_ Set k
_ [v]
mustList Specification Integer
sz Specification (k, v)
kvSpec FoldSpec v
foldSpec) = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ (forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec forall a. Maybe a
Nothing [v]
mustList Specification Integer
sz (forall k v.
(HasSpec k, HasSpec v) =>
Specification (k, v) -> Specification v
sndSpec Specification (k, v)
kvSpec) FoldSpec v
foldSpec)

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

dom_ ::
  (HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k, IsNormalType v) =>
  Term (Map k v) ->
  Term (Set k)
dom_ :: forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ = forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall k v.
(HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) =>
MapW '[Map k v] (Set k)
DomW

rng_ ::
  (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
  Term (Map k v) ->
  Term [v]
rng_ :: forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ = forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall k v.
(HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) =>
MapW '[Map k v] [v]
RngW

lookup_ ::
  (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
  Term k ->
  Term (Map k v) ->
  Term (Maybe v)
lookup_ :: forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ = forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall k v.
(HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) =>
MapW '[k, Map k v] (Maybe v)
LookupW