{-# 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 #-}
#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)
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)
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
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
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)
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
(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))
, 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 ->
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))
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}
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_"
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
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
$
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)
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