{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Constrained.Spec.Map where
import Constrained.AbstractSyntax
import Constrained.Base
import Constrained.Conformance
import Constrained.Core
import Constrained.FunctionSymbol
import Constrained.GenT
import Constrained.Generic (Prod (..))
import Constrained.List
import Constrained.NumSpec (cardinality, geqSpec, leqSpec, nubOrd)
import Constrained.PrettyUtils
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 = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> (Map a b -> Int) -> Map a b -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a b -> Int
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 = TypeSpec (Map a b) -> Specification (Map a b)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec (Map a b) -> Specification (Map a b))
-> TypeSpec (Map a b) -> Specification (Map a b)
forall a b. (a -> b) -> a -> b
$ MapSpec a b
forall k v. Ord k => MapSpec k v
defaultMapSpec {mapSpecSize = TypeSpec sz cant}
liftMemberSpec :: HasSpec (Map a b) => [Integer] -> Specification (Map a b)
liftMemberSpec [Integer]
xs = case [Integer] -> Maybe (NonEmpty Integer)
forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty ([Integer] -> [Integer]
forall a. Ord a => [a] -> [a]
nubOrd [Integer]
xs) of
Maybe (NonEmpty Integer)
Nothing -> NonEmpty String -> Specification (Map a b)
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (String -> NonEmpty String
forall a. a -> NonEmpty a
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 -> TypeSpec (Map a b) -> Specification (Map a b)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec (Map a b) -> Specification (Map a b))
-> TypeSpec (Map a b) -> Specification (Map a b)
forall a b. (a -> b) -> a -> b
$ MapSpec a b
forall k v. Ord k => MapSpec k v
defaultMapSpec {mapSpecSize = MemberSpec 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
_) =
Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
geqSpec (Set a -> Integer
forall t. Sized t => t -> Integer
sizeOf Set a
mustk)
Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
geqSpec ([b] -> Integer
forall t. Sized t => t -> Integer
sizeOf [b]
mustv)
Specification Integer
-> Specification Integer -> Specification Integer
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 x. MapSpec k v -> Rep (MapSpec k v) x)
-> (forall x. Rep (MapSpec k v) x -> MapSpec k v)
-> Generic (MapSpec k v)
forall x. Rep (MapSpec k v) x -> MapSpec k v
forall x. MapSpec k v -> Rep (MapSpec k v) x
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
$cfrom :: forall k v x. MapSpec k v -> Rep (MapSpec k v) x
from :: forall x. MapSpec k v -> Rep (MapSpec k v) x
$cto :: forall k v x. Rep (MapSpec k v) x -> MapSpec k v
to :: forall x. Rep (MapSpec k v) x -> MapSpec k v
Generic)
defaultMapSpec :: Ord k => MapSpec k v
defaultMapSpec :: forall k v. Ord k => MapSpec k v
defaultMapSpec = Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec Maybe Integer
forall a. Maybe a
Nothing Set k
forall a. Monoid a => a
mempty [v]
forall a. Monoid a => a
mempty Specification Integer
forall deps a. SpecificationD deps a
TrueSpec Specification (k, v)
forall deps a. SpecificationD deps a
TrueSpec FoldSpec v
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 =
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec
(Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v)
-> Gen (Maybe Integer)
-> Gen
(Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Maybe Integer)
forall a. Arbitrary a => Gen a
arbitrary
Gen
(Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v)
-> Gen (Set k)
-> Gen
([v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Set k)
forall a. Arbitrary a => Gen a
arbitrary
Gen
([v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v)
-> Gen [v]
-> Gen
(Specification Integer
-> Specification (k, v) -> FoldSpec v -> MapSpec k v)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen [v]
forall a. Arbitrary a => Gen a
arbitrary
Gen
(Specification Integer
-> Specification (k, v) -> FoldSpec v -> MapSpec k v)
-> Gen (Specification Integer)
-> Gen (Specification (k, v) -> FoldSpec v -> MapSpec k v)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Specification Integer)
forall a. Arbitrary a => Gen a
arbitrary
Gen (Specification (k, v) -> FoldSpec v -> MapSpec k v)
-> Gen (Specification (k, v)) -> Gen (FoldSpec v -> MapSpec k v)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Specification (k, v))
forall a. Arbitrary a => Gen a
arbitrary
Gen (FoldSpec v -> MapSpec k v)
-> Gen (FoldSpec v) -> Gen (MapSpec k v)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [(Int, Gen (FoldSpec v))] -> Gen (FoldSpec v)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
1, FoldSpec v -> Gen (FoldSpec v)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FoldSpec v
forall a. FoldSpec a
NoFold), (Int
1, Gen (FoldSpec v)
forall a. Arbitrary a => Gen a
arbitrary)]
shrink :: MapSpec k v -> [MapSpec k v]
shrink = MapSpec k v -> [MapSpec k v]
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 = FoldSpec (Map k v) -> Gen (FoldSpec (Map k v))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FoldSpec (Map k v)
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) =
Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
Doc ann
"MapSpec"
Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
/> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep
[ Doc ann
"hint =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Maybe Integer -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (MapSpec k v -> Maybe Integer
forall k v. MapSpec k v -> Maybe Integer
mapSpecHint MapSpec k v
s)
, Doc ann
"mustKeys =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Set k -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (MapSpec k v -> Set k
forall k v. MapSpec k v -> Set k
mapSpecMustKeys MapSpec k v
s)
, Doc ann
"mustValues =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [v] -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (MapSpec k v -> [v]
forall k v. MapSpec k v -> [v]
mapSpecMustValues MapSpec k v
s)
, Doc ann
"size =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification Integer -> Doc ann
pretty (MapSpec k v -> Specification Integer
forall k v. MapSpec k v -> Specification Integer
mapSpecSize MapSpec k v
s)
, Doc ann
"elem =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification (k, v) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification (k, v) -> Doc ann
pretty (MapSpec k v -> Specification (k, v)
forall k v. MapSpec k v -> Specification (k, v)
mapSpecElem MapSpec k v
s)
, Doc ann
"fold =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FoldSpec v -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. FoldSpec v -> Doc ann
pretty (MapSpec k v -> FoldSpec v
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 = Doc Any -> ShowS
forall a. Show a => a -> ShowS
shows (Doc Any -> ShowS)
-> (MapSpec k v -> Doc Any) -> MapSpec k v -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> MapSpec k v -> Doc Any
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 = TypeSpec (Map k v) -> Specification (Map k v)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec (Map k v) -> Specification (Map k v))
-> TypeSpec (Map k v) -> Specification (Map k v)
forall a b. (a -> b) -> a -> b
$ MapSpec k v
forall k v. Ord k => MapSpec k v
defaultMapSpec {mapSpecElem = kvs}
forAllToList :: Map k v -> [(k, v)]
forAllToList = Map k v -> [(k, v)]
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 = ProdW '[Prod k v] k -> Specification (Prod k v) -> Specification k
forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec ProdW '[Prod k v] k
forall b b1. (HasSpec b, HasSpec b1) => ProdW '[Prod b b1] b
ProdFstW (BaseW '[(k, v)] (Prod k v)
-> Specification (k, v) -> Specification (Prod k v)
forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec BaseW '[(k, v)] (SimpleRep (k, v))
BaseW '[(k, v)] (Prod k v)
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 = ProdW '[Prod k v] v -> Specification (Prod k v) -> Specification v
forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec ProdW '[Prod k v] v
forall a1 b. (HasSpec a1, HasSpec b) => ProdW '[Prod a1 b] b
ProdSndW (BaseW '[(k, v)] (Prod k v)
-> Specification (k, v) -> Specification (Prod k v)
forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec BaseW '[(k, v)] (SimpleRep (k, v))
BaseW '[(k, v)] (Prod k v)
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 = TypeSpec (Map k v)
MapSpec k v
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 FoldSpec v -> FoldSpec v -> Either [String] (FoldSpec v)
forall a. FoldSpec a -> FoldSpec a -> Either [String] (FoldSpec a)
combineFoldSpec FoldSpec v
foldSpec FoldSpec v
foldSpec' of
Left [String]
msgs ->
NonEmpty String -> Specification (Map k v)
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (NonEmpty String -> Specification (Map k v))
-> NonEmpty String -> Specification (Map k v)
forall a b. (a -> b) -> a -> b
$
[String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList ([String] -> NonEmpty String) -> [String] -> NonEmpty String
forall a b. (a -> b) -> a -> b
$
[ String
"Error in combining FoldSpec in combineSpec for Map"
, String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FoldSpec v -> String
forall a. Show a => a -> String
show FoldSpec v
foldSpec
, String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FoldSpec v -> String
forall a. Show a => a -> String
show FoldSpec v
foldSpec'
]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
msgs
Right FoldSpec v
foldSpec'' ->
TypeSpec (Map k v) -> Specification (Map k v)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec (Map k v) -> Specification (Map k v))
-> TypeSpec (Map k v) -> Specification (Map k v)
forall a b. (a -> b) -> a -> b
$
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec
((Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe Integer -> Maybe Integer
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Maybe Integer
mHint Maybe Integer
mHint')
(Set k
mustKeys Set k -> Set k -> Set k
forall a. Semigroup a => a -> a -> a
<> Set k
mustKeys')
([v] -> [v]
forall a. Eq a => [a] -> [a]
nub ([v] -> [v]) -> [v] -> [v]
forall a b. (a -> b) -> a -> b
$ [v]
mustVals [v] -> [v] -> [v]
forall a. Semigroup a => a -> a -> a
<> [v]
mustVals')
(Specification Integer
size Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Specification Integer
size')
(Specification (k, v)
kvs Specification (k, v)
-> Specification (k, v) -> Specification (k, v)
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) =
[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
[ Set k
mustKeys Set k -> Set k -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Map k v -> Set k
forall k a. Map k a -> Set k
Map.keysSet Map k v
m
, (v -> Bool) -> [v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (v -> [v] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map k v -> [v]
forall k a. Map k a -> [a]
Map.elems Map k v
m) [v]
mustVals
, Map k v -> Integer
forall t. Sized t => t -> Integer
sizeOf Map k v
m Integer -> Specification Integer -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification Integer
size
, ((k, v) -> Bool) -> [(k, v)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((k, v) -> Specification (k, v) -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification (k, v)
kvs) (Map k v -> [(k, v)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k v
m)
, Map k v -> [v]
forall k a. Map k a -> [a]
Map.elems Map k v
m [v] -> FoldSpec v -> Bool
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 (Specification (k, v) -> Specification (k, v)
forall a. HasSpec a => Specification a -> Specification a
simplifySpec -> Specification (k, v)
kvs) FoldSpec v
NoFold)
| Set k -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set k
mustKeys
, [v] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [v]
mustVals = do
let size' :: Specification Integer
size' =
[Specification Integer] -> Specification Integer
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
[ Specification Integer
-> (Integer -> Specification Integer)
-> Maybe Integer
-> Specification Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Specification Integer
forall deps a. SpecificationD deps a
TrueSpec (Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
leqSpec (Integer -> Specification Integer)
-> (Integer -> Integer) -> Integer -> Specification Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
0) Maybe Integer
mHint
, Specification Integer
size
, Specification Integer -> Specification Integer
maxSpec (Specification k -> Specification Integer
forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality (Specification (k, v) -> Specification k
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)
, Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
geqSpec Integer
0
]
Integer
n <- Specification Integer -> GenT m Integer
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 = Map k v -> GenT m (Map k v)
forall a. a -> GenT m a
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 <- GenT GE (k, v) -> GenT m (Maybe (k, v))
forall (m :: * -> *) a.
MonadGenError m =>
GenT GE a -> GenT m (Maybe a)
tryGenT (GenT GE (k, v) -> GenT m (Maybe (k, v)))
-> GenT GE (k, v) -> GenT m (Maybe (k, v))
forall a b. (a -> b) -> a -> b
$ Specification (k, v) -> GenT GE (k, v)
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
| Map k v -> Integer
forall t. Sized t => t -> Integer
sizeOf Map k v
m Integer -> Specification Integer -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification Integer
size -> Map k v -> GenT m (Map k v)
forall a. a -> GenT m a
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' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
(Specification (k, v)
kvs' Specification (k, v)
-> Specification (k, v) -> Specification (k, v)
forall a. Semigroup a => a -> a -> a
<> TypeSpec (k, v) -> Specification (k, v)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Specification k -> Specification v -> PairSpec k v
forall a b. Specification a -> Specification b -> PairSpec a b
Cartesian (k -> Specification k
forall a. HasSpec a => a -> Specification a
notEqualSpec k
k) Specification v
forall a. Monoid a => a
mempty))
(k -> v -> Map k v -> Map k v
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)
_ ->
NonEmpty String -> GenT m (Map k v)
forall a. HasCallStack => NonEmpty String -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
genErrorNE
( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ String
"Failed to generate enough elements for the map:"
, String
" m = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Map k v -> String
forall a. Show a => a -> String
show Map k v
m
, String
" n' = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n'
, Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
" kvs' = " Doc Any -> Doc Any -> Doc Any
forall a. Semigroup a => a -> a -> a
<> Specification (k, v) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification (k, v) -> Doc ann
pretty Specification (k, v)
kvs'
, Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
" simplifySpec kvs' = " Doc Any -> Doc Any -> Doc Any
forall a. Semigroup a => a -> a -> a
<> Specification (k, v) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification (k, v) -> Doc ann
pretty (Specification (k, v) -> Specification (k, v)
forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification (k, v)
kvs')
]
)
String -> GenT m (Map k v) -> GenT m (Map k v)
forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain (String
" n = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n) (GenT m (Map k v) -> GenT m (Map k v))
-> GenT m (Map k v) -> GenT m (Map k v)
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 Map k v
forall a. Monoid a => a
mempty
genFromTypeSpec (MapSpec Maybe Integer
mHint Set k
mustKeys [v]
mustVals Specification Integer
size (Specification (k, v) -> Specification (k, v)
forall a. HasSpec a => Specification a -> Specification a
simplifySpec -> Specification (k, v)
kvs) FoldSpec v
foldSpec) = do
![(k, v)]
mustMap <- String -> GenT m [(k, v)] -> GenT m [(k, v)]
forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain String
"Make the mustMap" (GenT m [(k, v)] -> GenT m [(k, v)])
-> GenT m [(k, v)] -> GenT m [(k, v)]
forall a b. (a -> b) -> a -> b
$ [k] -> (k -> GenT m (k, v)) -> GenT m [(k, v)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Set k -> [k]
forall a. Set a -> [a]
Set.toList Set k
mustKeys) ((k -> GenT m (k, v)) -> GenT m [(k, v)])
-> (k -> GenT m (k, v)) -> GenT m [(k, v)]
forall a b. (a -> b) -> a -> b
$ \k
k -> do
let vSpec :: Specification v
vSpec = (Term v -> Pred) -> Specification v
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term v -> Pred) -> Specification v)
-> (Term v -> Pred) -> Specification v
forall a b. (a -> b) -> a -> b
$ \Term v
v -> Term (k, v) -> Specification (k, v) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term k -> Term v -> Term (k, v)
forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ (k -> Term k
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit k
k) Term v
v) Specification (k, v)
kvs
v
v <- String -> GenT m v -> GenT m v
forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain (Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"vSpec =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification v -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification v -> Doc ann
pretty Specification v
vSpec) (GenT m v -> GenT m v) -> GenT m v -> GenT m v
forall a b. (a -> b) -> a -> b
$ Specification v -> GenT m v
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification v
vSpec
(k, v) -> GenT m (k, v)
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (k
k, v
v)
let haveVals :: [v]
haveVals = ((k, v) -> v) -> [(k, v)] -> [v]
forall a b. (a -> b) -> [a] -> [b]
map (k, v) -> v
forall a b. (a, b) -> b
snd [(k, v)]
mustMap
mustVals' :: [v]
mustVals' = (v -> Bool) -> [v] -> [v]
forall a. (a -> Bool) -> [a] -> [a]
filter (v -> [v] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [v]
haveVals) [v]
mustVals
size' :: Specification Integer
size' = Specification Integer -> Specification Integer
forall a. HasSpec a => Specification a -> Specification a
simplifySpec (Specification Integer -> Specification Integer)
-> Specification Integer -> Specification Integer
forall a b. (a -> b) -> a -> b
$ (Term Integer -> Pred) -> Specification Integer
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Integer -> Pred) -> Specification Integer)
-> (Term Integer -> Pred) -> Specification Integer
forall a b. (a -> b) -> a -> b
$ \Term Integer
sz ->
Term Integer -> Specification Integer -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
(Term Integer
sz Term Integer -> Term Integer -> Term Integer
forall a. Num a => a -> a -> a
+ Integer -> Term Integer
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit ([(k, v)] -> Integer
forall t. Sized t => t -> Integer
sizeOf [(k, v)]
mustMap))
( Specification Integer
-> (Integer -> Specification Integer)
-> Maybe Integer
-> Specification Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Specification Integer
forall deps a. SpecificationD deps a
TrueSpec (Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
leqSpec (Integer -> Specification Integer)
-> (Integer -> Integer) -> Integer -> Specification Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
0) Maybe Integer
mHint
Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Specification Integer
size
Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Specification Integer -> Specification Integer
maxSpec (Specification k -> Specification Integer
forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality (Specification (k, v) -> Specification k
forall k v.
(HasSpec k, HasSpec v) =>
Specification (k, v) -> Specification k
fstSpec Specification (k, v)
kvs))
Specification Integer
-> Specification Integer -> Specification Integer
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 -> FoldSpec v
forall a. FoldSpec a
NoFold
FoldSpec fn :: Fun '[v] b
fn@(Fun t '[v] b
symbol) Specification b
sumSpec -> Fun '[v] b -> Specification b -> FoldSpec v
forall b a.
(HasSpec a, HasSpec b, Foldy b) =>
Fun '[a] b -> Specification b -> FoldSpec a
FoldSpec Fun '[v] b
fn (Specification b -> FoldSpec v) -> Specification b -> FoldSpec v
forall a b. (a -> b) -> a -> b
$ IntW '[b, b] b
-> ListCtx Value '[b, b] (HOLE b)
-> Specification b
-> Specification b
forall (as :: [*]) b a.
(AppRequires IntW as b, HasSpec a) =>
IntW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
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 IntW '[b, b] b
forall a. Foldy a => IntW '[a, a] a
theAddFn (HOLE b b
forall {k} (a :: k). HOLE a a
HOLE HOLE b b -> List Value '[b] -> ListCtx Value '[b, b] (HOLE b)
forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:? b -> Value b
forall a. Show a => a -> Value a
Value b
mustSum Value b -> List Value '[] -> List Value '[b]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Value '[]
forall {k} (f :: k -> *). List f '[]
Nil) Specification b
sumSpec
where
mustSum :: b
mustSum = [b] -> b
forall a. Foldy a => [a] -> a
adds ((v -> b) -> [v] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (t '[v] b -> FunTy '[v] b
forall (d :: [*]) r. t d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t '[v] b
symbol) [v]
haveVals)
let !valsSpec :: ListSpec v
valsSpec =
Maybe Integer
-> [v]
-> Specification Integer
-> Specification v
-> FoldSpec v
-> ListSpec v
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec
Maybe Integer
forall a. Maybe a
Nothing
[v]
mustVals'
Specification Integer
size'
(Specification v -> Specification v
forall a. HasSpec a => Specification a -> Specification a
simplifySpec (Specification v -> Specification v)
-> Specification v -> Specification v
forall a b. (a -> b) -> a -> b
$ (Term v -> Pred) -> Specification v
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term v -> Pred) -> Specification v)
-> (Term v -> Pred) -> Specification v
forall a b. (a -> b) -> a -> b
$ \Term v
v -> (Term k -> Pred) -> Pred
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists ((Term k -> Pred) -> Pred) -> (Term k -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term k
k -> Term k -> Term v -> Term (k, v)
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 Term (k, v) -> Specification (k, v) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (k, v)
kvs)
FoldSpec v
foldSpec'
![v]
restVals <-
NonEmpty String -> GenT m [v] -> GenT m [v]
forall a. HasCallStack => NonEmpty String -> GenT m a -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ String
"Make the restVals"
, Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
" valsSpec =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ListSpec v -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. ListSpec v -> Doc ann
pretty ListSpec v
valsSpec
, Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
" mustMap =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [(k, v)] -> Doc Any
forall a ann. Show a => a -> Doc ann
viaShow [(k, v)]
mustMap
, Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
" size' =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification Integer -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification Integer -> Doc ann
pretty Specification Integer
size'
]
)
(GenT m [v] -> GenT m [v]) -> GenT m [v] -> GenT m [v]
forall a b. (a -> b) -> a -> b
$ TypeSpec [v] -> GenT m [v]
forall a (m :: * -> *).
(HasSpec a, HasCallStack, MonadGenError m) =>
TypeSpec a -> GenT m a
forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec [v] -> GenT m [v]
genFromTypeSpec
(TypeSpec [v] -> GenT m [v]) -> TypeSpec [v] -> GenT m [v]
forall a b. (a -> b) -> a -> b
$ TypeSpec [v]
ListSpec v
valsSpec
let go :: Map k v -> [v] -> GenT m (Map k v)
go Map k v
m [] = Map k v -> GenT m (Map k v)
forall a. a -> GenT m a
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 = Set k -> Specification k
forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec (Map k v -> Set k
forall k a. Map k a -> Set k
Map.keysSet Map k v
m) Specification k -> Specification k -> Specification k
forall a. Semigroup a => a -> a -> a
<> (Term k -> Pred) -> Specification k
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained (\Term k
k -> Term k -> Term v -> Term (k, v)
forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term k
k (v -> Term v
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit v
v) Term (k, v) -> Specification (k, v) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (k, v)
kvs)
k
k <-
NonEmpty String -> GenT m k -> GenT m k
forall a. HasCallStack => NonEmpty String -> GenT m a -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ String
"Make a key"
, Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ Doc Any
"keySpec =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification k -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification k -> Doc ann
pretty Specification k
keySpec
]
)
(GenT m k -> GenT m k) -> GenT m k -> GenT m k
forall a b. (a -> b) -> a -> b
$ Specification k -> GenT m k
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 (k -> v -> Map k v -> Map k v
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 ([(k, v)] -> Map k v
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)
_ = Specification Integer
forall deps a. SpecificationD deps 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 = ([(k, v)] -> Map k v) -> [[(k, v)]] -> [Map k v]
forall a b. (a -> b) -> [a] -> [b]
map [(k, v)] -> Map k v
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([[(k, v)]] -> [Map k v]) -> [[(k, v)]] -> [Map k v]
forall a b. (a -> b) -> a -> b
$ ((k, v) -> [(k, v)]) -> [(k, v)] -> [[(k, v)]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList (Specification (k, v) -> (k, v) -> [(k, v)]
forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification (k, v)
kvs) (Map k v -> [(k, v)]
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) =
[Pred] -> Pred
forall p. IsPred p => p -> Pred
toPred
[ Term Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Set k -> TermD Deps (Set k)
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit Set k
mustKeys TermD Deps (Set k) -> TermD Deps (Set k) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Term (Map k v) -> TermD Deps (Set k)
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
, Term [v] -> (Term v -> Term Bool) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll ([v] -> Term [v]
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit [v]
mustVals) ((Term v -> Term Bool) -> Pred) -> (Term v -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term v
val ->
Term v
val Term v -> Term [v] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` Term (Map k v) -> Term [v]
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
, Term [v] -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Map k v) -> Term [v]
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) Term Integer -> Specification Integer -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification Integer
size
, Term (Map k v) -> (Term (k, v) -> Pred) -> Pred
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 ((Term (k, v) -> Pred) -> Pred) -> (Term (k, v) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (k, v)
kv -> Term (k, v) -> Specification (k, v) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (k, v)
kv Specification (k, v)
kvs
, Term [v] -> FoldSpec v -> Pred
forall a. HasSpec a => Term [a] -> FoldSpec a -> Pred
toPredsFoldSpec (Term (Map k v) -> Term [v]
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
, Pred -> (Integer -> Pred) -> Maybe Integer -> Pred
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Pred
forall deps. PredD deps
TruePred (Hint (Map k v) -> Term (Map k v) -> Pred
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 = TypeSpec (Map k v) -> Specification (Map k v)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec (Map k v) -> Specification (Map k v))
-> TypeSpec (Map k v) -> Specification (Map k v)
forall a b. (a -> b) -> a -> b
$ MapSpec k v
forall k v. Ord k => MapSpec k v
defaultMapSpec {mapSpecHint = Just 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 = FunTy d r
Map k v -> Set k
forall k a. Map k a -> Set k
Map.keysSet
mapSem MapW d r
RngW = FunTy d r
Map k v -> [v]
forall k a. Map k a -> [a]
Map.elems
mapSem MapW d r
LookupW = FunTy d r
k -> Map k v -> Maybe v
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 = MapW d r -> FunTy d r
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 SpecificationD Deps b
s) = [String] -> Specification a -> Specification a
forall a. [String] -> Specification a -> Specification a
explainSpec [String]
es (Specification a -> Specification a)
-> Specification a -> Specification a
forall a b. (a -> b) -> a -> b
$ MapW as b
-> ListCtx Value as (HOLE a)
-> SpecificationD Deps b
-> Specification a
forall (as :: [*]) b a.
(AppRequires MapW as b, HasSpec a) =>
MapW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
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 SpecificationD Deps b
s
propagate MapW as b
_ ListCtx Value as (HOLE a)
_ SpecificationD Deps b
TrueSpec = Specification a
forall deps a. SpecificationD deps a
TrueSpec
propagate MapW as b
_ ListCtx Value as (HOLE a)
_ (ErrorSpec NonEmpty String
msgs) = NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec NonEmpty String
msgs
propagate MapW as b
f ListCtx Value as (HOLE a)
ctx (SuspendedSpec Var b
v Pred
ps) = (Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
v' -> TermD Deps b -> BinderD Deps b -> Pred
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let (MapW as b -> List Term as -> TermD Deps b
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App MapW as b
f (ListCtx Value as (HOLE a) -> Term a -> List Term as
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 Var b -> Pred -> BinderD Deps b
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Pred
ps)
propagate MapW as b
DomW (Unary HOLE a (Map k v)
HOLE) SpecificationD Deps b
spec =
case SpecificationD Deps b
spec of
MemberSpec (b
s :| []) ->
TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec a -> Specification a) -> TypeSpec a -> Specification a
forall a b. (a -> b) -> a -> b
$
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec Maybe Integer
forall a. Maybe a
Nothing b
Set k
s [] (Integer -> Specification Integer
forall a. a -> Specification a
equalSpec (Integer -> Specification Integer)
-> Integer -> Specification Integer
forall a b. (a -> b) -> a -> b
$ b -> Integer
forall t. Sized t => t -> Integer
sizeOf b
s) Specification (k, v)
forall deps a. SpecificationD deps a
TrueSpec FoldSpec v
forall a. FoldSpec a
NoFold
TypeSpec (SetSpec Set k
must Specification k
elemspec Specification Integer
size) [] ->
TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec a -> Specification a) -> TypeSpec a -> Specification a
forall a b. (a -> b) -> a -> b
$
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec
Maybe Integer
forall a. Maybe a
Nothing
Set k
must
[]
Specification Integer
size
((Term (k, v) -> Pred) -> Specification (k, v)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (k, v) -> Pred) -> Specification (k, v))
-> (Term (k, v) -> Pred) -> Specification (k, v)
forall a b. (a -> b) -> a -> b
$ \Term (k, v)
kv -> Term k -> Specification k -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term (k, v) -> Term k
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (k, v)
kv) Specification k
elemspec)
FoldSpec v
forall a. FoldSpec a
NoFold
SpecificationD Deps b
_ -> NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec ([String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String
"Dom on bad map spec", SpecificationD Deps b -> String
forall a. Show a => a -> String
show SpecificationD Deps b
spec])
propagate MapW as b
RngW (Unary HOLE a (Map k v)
HOLE) SpecificationD Deps b
spec =
case SpecificationD Deps b
spec of
TypeSpec (ListSpec Maybe Integer
listHint [v]
must Specification Integer
size Specification v
elemspec FoldSpec v
foldspec) [] ->
TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec a -> Specification a) -> TypeSpec a -> Specification a
forall a b. (a -> b) -> a -> b
$
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec
Maybe Integer
listHint
Set k
forall a. Set a
Set.empty
[v]
must
Specification Integer
size
((Term (k, v) -> Pred) -> Specification (k, v)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (k, v) -> Pred) -> Specification (k, v))
-> (Term (k, v) -> Pred) -> Specification (k, v)
forall a b. (a -> b) -> a -> b
$ \Term (k, v)
kv -> Term v -> Specification v -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term (k, v) -> Term v
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (k, v)
kv) Specification v
elemspec)
FoldSpec v
foldspec
SpecificationD Deps b
_ -> NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec ([String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String
"Rng on bad map spec", SpecificationD Deps b -> String
forall a. Show a => a -> String
show SpecificationD Deps b
spec])
propagate MapW as b
LookupW (Value a
k :! Unary HOLE a (Map k v)
HOLE) SpecificationD Deps b
spec =
(Term a -> [Pred]) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> [Pred]) -> Specification a)
-> (Term a -> [Pred]) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
m ->
[Term Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ a -> TermD Deps a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
k TermD Deps a -> Term (Set a) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` Term (Map a v) -> Term (Set a)
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
Term (Map a v)
m | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Maybe v
forall a. Maybe a
Nothing Maybe v -> Specification (Maybe v) -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` SpecificationD Deps b
Specification (Maybe v)
spec]
[Pred] -> [Pred] -> [Pred]
forall a. [a] -> [a] -> [a]
++ [ Term a -> (Term (a, v) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term a
m ((Term (a, v) -> Pred) -> Pred) -> (Term (a, v) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (a, v)
kv ->
TermD Deps a -> (TermD Deps a -> Pred) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (Term (a, v) -> TermD Deps a
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (a, v)
kv) ((TermD Deps a -> Pred) -> Pred) -> (TermD Deps a -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps a
k' ->
Term v -> (Term v -> Pred) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (Term (a, v) -> Term v
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (a, v)
kv) ((Term v -> Pred) -> Pred) -> (Term v -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term v
v ->
Term Bool -> Pred -> Pred
forall p. IsPred p => Term Bool -> p -> Pred
whenTrue (a -> TermD Deps a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
k TermD Deps a -> TermD Deps a -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. TermD Deps a
k') (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$
case SpecificationD Deps b
spec of
MemberSpec NonEmpty b
as -> Term Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term v
v Term v -> Term [v] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` [v] -> Term [v]
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit [v
a | Just v
a <- NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
as]
TypeSpec (SumSpec Maybe (Int, Int)
_ Specification ()
_ Specification v
vspec) [b]
cant ->
Term v
v Term v -> Specification v -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` (Specification v
vspec Specification v -> Specification v -> Specification v
forall a. Semigroup a => a -> a -> a
<> [v] -> Specification v
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) SpecificationD Deps b
spec =
if Maybe v
forall a. Maybe a
Nothing Maybe v -> Specification (Maybe v) -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` SpecificationD Deps b
Specification (Maybe v)
spec
then [a] -> Specification a
forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec [a
k | (a
k, v
v) <- Map a v -> [(a, v)]
forall k a. Map k a -> [(k, a)]
Map.toList a
Map a v
m, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ v -> Maybe v
forall a. a -> Maybe a
Just v
v Maybe v -> Specification (Maybe v) -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` SpecificationD Deps b
Specification (Maybe v)
spec]
else
[a] -> NonEmpty String -> Specification a
forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
(Map a v -> [a]
forall k a. Map k a -> [k]
Map.keys (Map a v -> [a]) -> Map a v -> [a]
forall a b. (a -> b) -> a -> b
$ (v -> Bool) -> Map a v -> Map a v
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter ((b -> SpecificationD Deps b -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` SpecificationD Deps b
spec) (b -> Bool) -> (v -> b) -> v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> b
v -> Maybe v
forall a. a -> Maybe a
Just) a
Map a v
m)
( [String] -> NonEmpty String
forall a. HasCallStack => [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
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SpecificationD Deps b -> String
forall a. Show a => a -> String
show SpecificationD Deps 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
_) = TypeSpec b -> Specification b
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec b -> Specification b) -> TypeSpec b -> Specification b
forall a b. (a -> b) -> a -> b
$ Set k -> Specification k -> Specification Integer -> SetSpec k
forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec Set k
mustSet (Specification (k, v) -> Specification k
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) = TypeSpec b -> Specification b
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec b -> Specification b) -> TypeSpec b -> Specification b
forall a b. (a -> b) -> a -> b
$ Maybe Integer
-> [v]
-> Specification Integer
-> Specification v
-> FoldSpec v
-> ListSpec v
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec Maybe Integer
forall a. Maybe a
Nothing [v]
mustList Specification Integer
sz (Specification (k, v) -> Specification v
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_ = MapW '[Map k v] (Set k)
-> FunTy (MapList Term '[Map k v]) (TermD Deps (Set k))
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm MapW '[Map k v] (Set k)
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_ = MapW '[Map k v] [v]
-> FunTy (MapList Term '[Map k v]) (TermD Deps [v])
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm MapW '[Map k v] [v]
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_ = MapW '[k, Map k v] (Maybe v)
-> FunTy (MapList Term '[k, Map k v]) (TermD Deps (Maybe v))
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm MapW '[k, Map k v] (Maybe v)
forall k v.
(HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) =>
MapW '[k, Map k v] (Maybe v)
LookupW