{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wno-orphans #-} -- The pattern completeness checker is much weaker before ghc-9.0. Rather than introducing redundant -- cases and turning off the overlap check in newer ghc versions we disable the check for old -- versions. #if __GLASGOW_HASKELL__ < 900 {-# OPTIONS_GHC -Wno-incomplete-patterns #-} #endif module Constrained.Spec.Map (MapSpec (..), defaultMapSpec, dom_, rng_, lookup_) where import Constrained.Base import Constrained.Core import Constrained.GenT import Constrained.Instances () import Constrained.List import Constrained.Spec.Generics import Constrained.Spec.Pairs import Constrained.Univ import Control.Monad import Data.Foldable import Data.List (nub) import Data.List.NonEmpty qualified as NE import Data.Map (Map) import Data.Map qualified as Map import Data.Set (Set) import Data.Set qualified as Set import GHC.Generics import Prettyprinter import Test.QuickCheck (Arbitrary (..), frequency, genericShrink, shrinkList) ------------------------------------------------------------------------ -- HasSpec ------------------------------------------------------------------------ instance Ord a => Sized (Map.Map a b) where sizeOf :: Map a b -> Integer sizeOf = forall a. Integral a => a -> Integer toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c . forall k a. Map k a -> Int Map.size liftSizeSpec :: forall (fn :: [*] -> * -> *). HasSpec fn (Map a b) => SizeSpec -> [Integer] -> Specification fn (Map a b) liftSizeSpec SizeSpec sz [Integer] cant = forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec forall a b. (a -> b) -> a -> b $ forall k (fn :: [*] -> * -> *) v. Ord k => MapSpec fn k v defaultMapSpec {mapSpecSize :: Specification fn Integer mapSpecSize = forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> OrdSet a -> Specification fn a TypeSpec SizeSpec sz [Integer] cant} liftMemberSpec :: forall (fn :: [*] -> * -> *). HasSpec fn (Map a b) => [Integer] -> Specification fn (Map a b) liftMemberSpec [Integer] xs = forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec forall a b. (a -> b) -> a -> b $ forall k (fn :: [*] -> * -> *) v. Ord k => MapSpec fn k v defaultMapSpec {mapSpecSize :: Specification fn Integer mapSpecSize = forall a (fn :: [*] -> * -> *). OrdSet a -> Specification fn a MemberSpec [Integer] xs} sizeOfTypeSpec :: forall (fn :: [*] -> * -> *). HasSpec fn (Map a b) => TypeSpec fn (Map a b) -> Specification fn Integer sizeOfTypeSpec (MapSpec Maybe Integer _ Set a mustk [b] mustv Specification fn Integer size Specification fn (a, b) _ FoldSpec fn b _) = forall (fn :: [*] -> * -> *) a. OrdLike fn a => a -> Specification fn a geqSpec (forall t. Sized t => t -> Integer sizeOf Set a mustk) forall a. Semigroup a => a -> a -> a <> forall (fn :: [*] -> * -> *) a. OrdLike fn a => a -> Specification fn a geqSpec (forall t. Sized t => t -> Integer sizeOf [b] mustv) forall a. Semigroup a => a -> a -> a <> Specification fn Integer size data MapSpec fn k v = MapSpec { forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> Maybe Integer mapSpecHint :: Maybe Integer , forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> Set k mapSpecMustKeys :: Set k , forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> [v] mapSpecMustValues :: [v] , forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> Specification fn Integer mapSpecSize :: Specification fn Integer , forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> Specification fn (k, v) mapSpecElem :: Specification fn (k, v) , forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> FoldSpec fn v mapSpecFold :: FoldSpec fn v } deriving (forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a forall (fn :: [*] -> * -> *) k v x. Rep (MapSpec fn k v) x -> MapSpec fn k v forall (fn :: [*] -> * -> *) k v x. MapSpec fn k v -> Rep (MapSpec fn k v) x $cto :: forall (fn :: [*] -> * -> *) k v x. Rep (MapSpec fn k v) x -> MapSpec fn k v $cfrom :: forall (fn :: [*] -> * -> *) k v x. MapSpec fn k v -> Rep (MapSpec fn k v) x Generic) -- | emptySpec without all the constraints defaultMapSpec :: Ord k => MapSpec fn k v defaultMapSpec :: forall k (fn :: [*] -> * -> *) v. Ord k => MapSpec fn k v defaultMapSpec = forall (fn :: [*] -> * -> *) k v. Maybe Integer -> Set k -> [v] -> Specification fn Integer -> Specification fn (k, v) -> FoldSpec fn v -> MapSpec fn k v MapSpec forall a. Maybe a Nothing forall a. Monoid a => a mempty forall a. Monoid a => a mempty forall (fn :: [*] -> * -> *) a. Specification fn a TrueSpec forall (fn :: [*] -> * -> *) a. Specification fn a TrueSpec forall (fn :: [*] -> * -> *) a. FoldSpec fn a NoFold -- TODO: consider making this more interesting to get fewer discarded tests -- in `prop_gen_sound` instance ( Arbitrary k , Arbitrary v , Arbitrary (TypeSpec fn k) , Arbitrary (TypeSpec fn v) , Ord k , HasSpec fn k , Foldy fn v ) => Arbitrary (MapSpec fn k v) where arbitrary :: Gen (MapSpec fn k v) arbitrary = forall (fn :: [*] -> * -> *) k v. Maybe Integer -> Set k -> [v] -> Specification fn Integer -> Specification fn (k, v) -> FoldSpec fn v -> MapSpec fn k v MapSpec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> forall a. Arbitrary a => Gen a arbitrary forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall a. Arbitrary a => Gen a arbitrary forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall a. Arbitrary a => Gen a arbitrary forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall a. Arbitrary a => Gen a arbitrary forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall a. Arbitrary a => Gen a arbitrary forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall a. [(Int, Gen a)] -> Gen a frequency [(Int 1, forall (f :: * -> *) a. Applicative f => a -> f a pure forall (fn :: [*] -> * -> *) a. FoldSpec fn a NoFold), (Int 1, forall a. Arbitrary a => Gen a arbitrary)] shrink :: MapSpec fn k v -> [MapSpec fn k v] shrink = forall a. (Generic a, RecursivelyShrink (Rep a), GSubterms (Rep a) a) => a -> [a] genericShrink instance Arbitrary (FoldSpec fn (Map k v)) where arbitrary :: Gen (FoldSpec fn (Map k v)) arbitrary = forall (f :: * -> *) a. Applicative f => a -> f a pure forall (fn :: [*] -> * -> *) a. FoldSpec fn a NoFold instance ( HasSpec fn (k, v) , HasSpec fn k , HasSpec fn v , HasSpec fn [v] ) => Pretty (WithPrec (MapSpec fn k v)) where pretty :: forall ann. WithPrec (MapSpec fn k v) -> Doc ann pretty (WithPrec Int d MapSpec fn k v s) = forall ann. Bool -> Doc ann -> Doc ann parensIf (Int d forall a. Ord a => a -> a -> Bool > Int 10) forall a b. (a -> b) -> a -> b $ Doc ann "MapSpec" forall ann. Doc ann -> Doc ann -> Doc ann /> forall ann. [Doc ann] -> Doc ann vsep [ Doc ann "hint =" forall ann. Doc ann -> Doc ann -> Doc ann <+> forall a ann. Show a => a -> Doc ann viaShow (forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> Maybe Integer mapSpecHint MapSpec fn k v s) , Doc ann "mustKeys =" forall ann. Doc ann -> Doc ann -> Doc ann <+> forall a ann. Show a => a -> Doc ann viaShow (forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> Set k mapSpecMustKeys MapSpec fn k v s) , Doc ann "mustValues =" forall ann. Doc ann -> Doc ann -> Doc ann <+> forall a ann. Show a => a -> Doc ann viaShow (forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> [v] mapSpecMustValues MapSpec fn k v s) , Doc ann "size =" forall ann. Doc ann -> Doc ann -> Doc ann <+> forall a ann. Pretty a => a -> Doc ann pretty (forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> Specification fn Integer mapSpecSize MapSpec fn k v s) , Doc ann "elem =" forall ann. Doc ann -> Doc ann -> Doc ann <+> forall a ann. Pretty a => a -> Doc ann pretty (forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> Specification fn (k, v) mapSpecElem MapSpec fn k v s) , Doc ann "fold =" forall ann. Doc ann -> Doc ann -> Doc ann <+> forall a ann. Pretty a => a -> Doc ann pretty (forall (fn :: [*] -> * -> *) k v. MapSpec fn k v -> FoldSpec fn v mapSpecFold MapSpec fn k v s) ] instance ( HasSpec fn (k, v) , HasSpec fn k , HasSpec fn v , HasSpec fn [v] ) => Show (MapSpec fn k v) where showsPrec :: Int -> MapSpec fn k v -> ShowS showsPrec Int d = forall a. Show a => a -> ShowS shows forall b c a. (b -> c) -> (a -> b) -> a -> c . forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann prettyPrec Int d instance Ord k => Forallable (Map k v) (k, v) where fromForAllSpec :: forall (fn :: [*] -> * -> *). (HasSpec fn (Map k v), HasSpec fn (k, v), BaseUniverse fn) => Specification fn (k, v) -> Specification fn (Map k v) fromForAllSpec Specification fn (k, v) kvs = forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec forall a b. (a -> b) -> a -> b $ forall k (fn :: [*] -> * -> *) v. Ord k => MapSpec fn k v defaultMapSpec {mapSpecElem :: Specification fn (k, v) mapSpecElem = Specification fn (k, v) kvs} forAllToList :: Map k v -> [(k, v)] forAllToList = forall k a. Map k a -> [(k, a)] Map.toList instance (Ord k, HasSpec fn (Prod k v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) => HasSpec fn (Map k v) where type TypeSpec fn (Map k v) = MapSpec fn k v type Prerequisites fn (Map k v) = (HasSpec fn k, HasSpec fn v) emptySpec :: TypeSpec fn (Map k v) emptySpec = forall k (fn :: [*] -> * -> *) v. Ord k => MapSpec fn k v defaultMapSpec combineSpec :: TypeSpec fn (Map k v) -> TypeSpec fn (Map k v) -> Specification fn (Map k v) combineSpec (MapSpec Maybe Integer mHint Set k mustKeys [v] mustVals Specification fn Integer size Specification fn (k, v) kvs FoldSpec fn v foldSpec) (MapSpec Maybe Integer mHint' Set k mustKeys' [v] mustVals' Specification fn Integer size' Specification fn (k, v) kvs' FoldSpec fn v foldSpec') = forall (fn :: [*] -> * -> *) a. HasCallStack => GE (Specification fn a) -> Specification fn a fromGESpec forall a b. (a -> b) -> a -> b $ do forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec forall b c a. (b -> c) -> (a -> b) -> a -> c . forall (fn :: [*] -> * -> *) k v. Maybe Integer -> Set k -> [v] -> Specification fn Integer -> Specification fn (k, v) -> FoldSpec fn v -> MapSpec fn k v MapSpec -- This is min because that allows more compositionality - if a spec specifies a -- low upper bound because some part of the spec will be slow it doesn't make sense -- to increase it somewhere else because that part isn't slow. (forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a unionWithMaybe forall a. Ord a => a -> a -> a min Maybe Integer mHint Maybe Integer mHint') (Set k mustKeys forall a. Semigroup a => a -> a -> a <> Set k mustKeys') (forall a. Eq a => [a] -> [a] nub forall a b. (a -> b) -> a -> b $ [v] mustVals forall a. Semigroup a => a -> a -> a <> [v] mustVals') (Specification fn Integer size forall a. Semigroup a => a -> a -> a <> Specification fn Integer size') (Specification fn (k, v) kvs forall a. Semigroup a => a -> a -> a <> Specification fn (k, v) kvs') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> forall (m :: * -> *) (fn :: [*] -> * -> *) a. MonadGenError m => FoldSpec fn a -> FoldSpec fn a -> m (FoldSpec fn a) combineFoldSpec FoldSpec fn v foldSpec FoldSpec fn v foldSpec' conformsTo :: HasCallStack => Map k v -> TypeSpec fn (Map k v) -> Bool conformsTo Map k v m (MapSpec Maybe Integer _ Set k mustKeys [v] mustVals Specification fn Integer size Specification fn (k, v) kvs FoldSpec fn v foldSpec) = forall (t :: * -> *). Foldable t => t Bool -> Bool and [ Set k mustKeys forall a. Ord a => Set a -> Set a -> Bool `Set.isSubsetOf` forall k a. Map k a -> Set k Map.keysSet Map k v m , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool all (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool `elem` forall k a. Map k a -> [a] Map.elems Map k v m) [v] mustVals , forall t. Sized t => t -> Integer sizeOf Map k v m forall (fn :: [*] -> * -> *) a. HasSpec fn a => a -> Specification fn a -> Bool `conformsToSpec` Specification fn Integer size , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool all (forall (fn :: [*] -> * -> *) a. HasSpec fn a => a -> Specification fn a -> Bool `conformsToSpec` Specification fn (k, v) kvs) (forall k a. Map k a -> [(k, a)] Map.toList Map k v m) , forall k a. Map k a -> [a] Map.elems Map k v m forall (fn :: [*] -> * -> *) a. [a] -> FoldSpec fn a -> Bool `conformsToFoldSpec` FoldSpec fn v foldSpec ] genFromTypeSpec :: forall (m :: * -> *). (HasCallStack, MonadGenError m) => TypeSpec fn (Map k v) -> GenT m (Map k v) genFromTypeSpec (MapSpec Maybe Integer mHint Set k mustKeys [v] mustVals Specification fn Integer size (forall (fn :: [*] -> * -> *) a. HasSpec fn a => Specification fn a -> Specification fn a simplifySpec -> Specification fn (k, v) kvs) FoldSpec fn v NoFold) | forall (t :: * -> *) a. Foldable t => t a -> Bool null Set k mustKeys , forall (t :: * -> *) a. Foldable t => t a -> Bool null [v] mustVals = do let size' :: Specification fn Integer size' = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m fold [ forall b a. b -> (a -> b) -> Maybe a -> b maybe forall (fn :: [*] -> * -> *) a. Specification fn a TrueSpec (forall (fn :: [*] -> * -> *) a. OrdLike fn a => a -> Specification fn a leqSpec forall b c a. (b -> c) -> (a -> b) -> a -> c . forall a. Ord a => a -> a -> a max Integer 0) Maybe Integer mHint , Specification fn Integer size , forall (fn :: [*] -> * -> *). BaseUniverse fn => Specification fn Integer -> Specification fn Integer maxSpec (forall (fn :: [*] -> * -> *) a. (Eq a, BaseUniverse fn, HasSpec fn a) => Specification fn a -> Specification fn Integer cardinality (forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => fn '[a] b -> Specification fn a -> Specification fn b mapSpec forall (fn :: [*] -> * -> *) a b. Member (PairFn fn) fn => fn '[Prod a b] a fstFn forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => fn '[a] b -> Specification fn a -> Specification fn b mapSpec forall (fn :: [*] -> * -> *) a. (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) => fn '[a] (SimpleRep a) toGenericFn Specification fn (k, v) kvs)) , forall (fn :: [*] -> * -> *). BaseUniverse fn => Specification fn Integer -> Specification fn Integer maxSpec (forall (fn :: [*] -> * -> *) a. HasSpec fn a => Specification fn Integer cardinalTrueSpec @fn @k) , forall (fn :: [*] -> * -> *) a. OrdLike fn a => a -> Specification fn a geqSpec Integer 0 ] Integer n <- forall (fn :: [*] -> * -> *) a (m :: * -> *). (HasCallStack, HasSpec fn a, MonadGenError m) => Specification fn a -> GenT m a genFromSpecT Specification fn Integer size' let go :: Integer -> Specification fn (k, v) -> Map k v -> GenT m (Map k v) go Integer 0 Specification fn (k, v) _ Map k v m = forall (f :: * -> *) a. Applicative f => a -> f a pure Map k v m go Integer n' Specification fn (k, v) kvs' Map k v m = do Maybe (k, v) mkv <- forall (m :: * -> *) a. MonadGenError m => GenT GE a -> GenT m (Maybe a) tryGen' forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) a (m :: * -> *). (HasCallStack, HasSpec fn a, MonadGenError m) => Specification fn a -> GenT m a genFromSpecT Specification fn (k, v) kvs' case Maybe (k, v) mkv of Maybe (k, v) Nothing | forall t. Sized t => t -> Integer sizeOf Map k v m forall (fn :: [*] -> * -> *) a. HasSpec fn a => a -> Specification fn a -> Bool `conformsToSpec` Specification fn Integer size -> forall (f :: * -> *) a. Applicative f => a -> f a pure Map k v m Just (k k, v v) -> Integer -> Specification fn (k, v) -> Map k v -> GenT m (Map k v) go (Integer n' forall a. Num a => a -> a -> a - Integer 1) (Specification fn (k, v) kvs' forall a. Semigroup a => a -> a -> a <> forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec (forall (fn :: [*] -> * -> *) a b. Specification fn a -> Specification fn b -> PairSpec fn a b Cartesian (forall (fn :: [*] -> * -> *) a. HasSpec fn a => a -> Specification fn a notEqualSpec k k) forall a. Monoid a => a mempty)) (forall k a. Ord k => k -> a -> Map k a -> Map k a Map.insert k k v v Map k v m) Maybe (k, v) _ -> forall (m :: * -> *) a. (MonadGenError m, HasCallStack) => NonEmpty String -> m a genError ( forall a. [a] -> NonEmpty a NE.fromList [ String "Failed to generate enough elements for the map:" , String " m = " forall a. [a] -> [a] -> [a] ++ forall a. Show a => a -> String show Map k v m , String " n' = " forall a. [a] -> [a] -> [a] ++ forall a. Show a => a -> String show Integer n' , forall a. Show a => a -> String show forall a b. (a -> b) -> a -> b $ Doc Any " kvs' = " forall a. Semigroup a => a -> a -> a <> forall a ann. Pretty a => a -> Doc ann pretty Specification fn (k, v) kvs' , forall a. Show a => a -> String show forall a b. (a -> b) -> a -> b $ Doc Any " simplifySpec kvs' = " forall a. Semigroup a => a -> a -> a <> forall a ann. Pretty a => a -> Doc ann pretty (forall (fn :: [*] -> * -> *) a. HasSpec fn a => Specification fn a -> Specification fn a simplifySpec Specification fn (k, v) kvs') ] ) forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a explain1 (String " n = " forall a. [a] -> [a] -> [a] ++ forall a. Show a => a -> String show Integer n) forall a b. (a -> b) -> a -> b $ Integer -> Specification fn (k, v) -> Map k v -> GenT m (Map k v) go Integer n Specification fn (k, v) kvs forall a. Monoid a => a mempty genFromTypeSpec (MapSpec Maybe Integer mHint Set k mustKeys [v] mustVals Specification fn Integer size (forall (fn :: [*] -> * -> *) a. HasSpec fn a => Specification fn a -> Specification fn a simplifySpec -> Specification fn (k, v) kvs) FoldSpec fn v foldSpec) = do [(k, v)] mustMap <- forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a explain1 String "Make the mustMap" forall a b. (a -> b) -> a -> b $ forall (t :: * -> *) (m :: * -> *) a b. (Traversable t, Monad m) => t a -> (a -> m b) -> m (t b) forM (forall a. Set a -> [a] Set.toList Set k mustKeys) forall a b. (a -> b) -> a -> b $ \k k -> do let vSpec :: Specification fn v vSpec = forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term fn v v -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn satisfies (forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn a -> Term fn b -> Term fn (a, b) pair_ (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit k k) Term fn v v) Specification fn (k, v) kvs v v <- forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a explain1 (forall a. Show a => a -> String show forall a b. (a -> b) -> a -> b $ Doc Any "vSpec =" forall ann. Doc ann -> Doc ann -> Doc ann <+> forall a ann. Pretty a => a -> Doc ann pretty Specification fn v vSpec) forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) a (m :: * -> *). (HasCallStack, HasSpec fn a, MonadGenError m) => Specification fn a -> GenT m a genFromSpecT Specification fn v vSpec forall (f :: * -> *) a. Applicative f => a -> f a pure (k k, v v) let haveVals :: [v] haveVals = forall a b. (a -> b) -> [a] -> [b] map forall a b. (a, b) -> b snd [(k, v)] mustMap mustVals' :: [v] mustVals' = forall a. (a -> Bool) -> [a] -> [a] filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool `notElem` [v] haveVals) [v] mustVals size' :: Specification fn Integer size' = forall (fn :: [*] -> * -> *) a. HasSpec fn a => Specification fn a -> Specification fn a simplifySpec forall a b. (a -> b) -> a -> b $ forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term fn Integer sz -> -- TODO, we should make sure size' is greater than or equal to 0 forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn satisfies (Term fn Integer sz forall a. Num a => a -> a -> a + forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a Lit (forall t. Sized t => t -> Integer sizeOf [(k, v)] mustMap)) ( forall b a. b -> (a -> b) -> Maybe a -> b maybe forall (fn :: [*] -> * -> *) a. Specification fn a TrueSpec (forall (fn :: [*] -> * -> *) a. OrdLike fn a => a -> Specification fn a leqSpec forall b c a. (b -> c) -> (a -> b) -> a -> c . forall a. Ord a => a -> a -> a max Integer 0) Maybe Integer mHint forall a. Semigroup a => a -> a -> a <> Specification fn Integer size forall a. Semigroup a => a -> a -> a <> forall (fn :: [*] -> * -> *). BaseUniverse fn => Specification fn Integer -> Specification fn Integer maxSpec (forall (fn :: [*] -> * -> *) a. (Eq a, BaseUniverse fn, HasSpec fn a) => Specification fn a -> Specification fn Integer cardinality (forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => fn '[a] b -> Specification fn a -> Specification fn b mapSpec forall (fn :: [*] -> * -> *) a b. Member (PairFn fn) fn => fn '[Prod a b] a fstFn forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => fn '[a] b -> Specification fn a -> Specification fn b mapSpec forall (fn :: [*] -> * -> *) a. (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) => fn '[a] (SimpleRep a) toGenericFn Specification fn (k, v) kvs)) forall a. Semigroup a => a -> a -> a <> forall (fn :: [*] -> * -> *). BaseUniverse fn => Specification fn Integer -> Specification fn Integer maxSpec (forall (fn :: [*] -> * -> *) a. HasSpec fn a => Specification fn Integer cardinalTrueSpec @fn @k) ) foldSpec' :: FoldSpec fn v foldSpec' = case FoldSpec fn v foldSpec of FoldSpec fn v NoFold -> forall (fn :: [*] -> * -> *) a. FoldSpec fn a NoFold FoldSpec fn '[v] b fn Specification fn b sumSpec -> forall b (fn :: [*] -> * -> *) a. (HasSpec fn a, HasSpec fn b, Foldy fn b, Member (ListFn fn) fn, BaseUniverse fn) => fn '[a] b -> Specification fn b -> FoldSpec fn a FoldSpec fn '[v] b fn forall a b. (a -> b) -> a -> b $ forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) a b. (Functions f fn, TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) => f as b -> ListCtx Value as (HOLE a) -> Specification fn b -> Specification fn a propagateSpecFun (forall (fn :: [*] -> * -> *) a. Foldy fn a => fn '[a, a] a theAddFn @fn) (forall a. HOLE a a HOLE forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]). c a -> List f as1 -> ListCtx f (a : as1) c :? forall a. Show a => a -> Value a Value b mustSum forall {k} (f :: k -> *) (a :: k) (as1 :: [k]). f a -> List f as1 -> List f (a : as1) :> forall {k} (f :: k -> *). List f '[] Nil) Specification fn b sumSpec where mustSum :: b mustSum = forall (fn :: [*] -> * -> *) a. Foldy fn a => [a] -> a adds @fn (forall a b. (a -> b) -> [a] -> [b] map (forall (fn :: [*] -> * -> *) (as :: [*]) b. FunctionLike fn => fn as b -> FunTy as b sem fn '[v] b fn) [v] haveVals) let valsSpec :: ListSpec fn v valsSpec = forall (fn :: [*] -> * -> *) a. Maybe Integer -> [a] -> Specification fn Integer -> Specification fn a -> FoldSpec fn a -> ListSpec fn a ListSpec forall a. Maybe a Nothing [v] mustVals' Specification fn Integer size' (forall (fn :: [*] -> * -> *) a. HasSpec fn a => Specification fn a -> Specification fn a simplifySpec forall a b. (a -> b) -> a -> b $ forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term fn v v -> forall a p (fn :: [*] -> * -> *). (HasSpec fn a, IsPred p fn) => (Term fn a -> p) -> Pred fn unsafeExists forall a b. (a -> b) -> a -> b $ \Term fn k k -> forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn a -> Term fn b -> Term fn (a, b) pair_ Term fn k k Term fn v v forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn `satisfies` Specification fn (k, v) kvs) FoldSpec fn v foldSpec' [v] restVals <- forall (m :: * -> *) a. (MonadGenError m, HasCallStack) => NonEmpty String -> m a -> m a explain ( forall a. [a] -> NonEmpty a NE.fromList [ String "Make the restVals" , forall a. Show a => a -> String show forall a b. (a -> b) -> a -> b $ Doc Any " valsSpec =" forall ann. Doc ann -> Doc ann -> Doc ann <+> forall a ann. Pretty a => a -> Doc ann pretty ListSpec fn v valsSpec , forall a. Show a => a -> String show forall a b. (a -> b) -> a -> b $ Doc Any " mustMap =" forall ann. Doc ann -> Doc ann -> Doc ann <+> forall a ann. Show a => a -> Doc ann viaShow [(k, v)] mustMap , forall a. Show a => a -> String show forall a b. (a -> b) -> a -> b $ Doc Any " size' =" forall ann. Doc ann -> Doc ann -> Doc ann <+> forall a ann. Pretty a => a -> Doc ann pretty Specification fn Integer size' ] ) forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) a (m :: * -> *). (HasSpec fn a, HasCallStack, MonadGenError m) => TypeSpec fn a -> GenT m a genFromTypeSpec forall a b. (a -> b) -> a -> b $ ListSpec fn v valsSpec let go :: Map k v -> [v] -> GenT m (Map k v) go Map k v m [] = forall (f :: * -> *) a. Applicative f => a -> f a pure Map k v m go Map k v m (v v : [v] restVals') = do let keySpec :: Specification fn k keySpec = forall (fn :: [*] -> * -> *) a (f :: * -> *). (HasSpec fn a, Foldable f) => f a -> Specification fn a notMemberSpec (forall k a. Map k a -> Set k Map.keysSet Map k v m) forall a. Semigroup a => a -> a -> a <> forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained (\Term fn k k -> forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn a -> Term fn b -> Term fn (a, b) pair_ Term fn k k (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit v v) forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn `satisfies` Specification fn (k, v) kvs) k k <- forall (m :: * -> *) a. (MonadGenError m, HasCallStack) => NonEmpty String -> m a -> m a explain ( forall a. [a] -> NonEmpty a NE.fromList [ String "Make a key" , forall a. Show a => a -> String show forall a b. (a -> b) -> a -> b $ forall ann. Int -> Doc ann -> Doc ann indent Int 4 forall a b. (a -> b) -> a -> b $ Doc Any "keySpec =" forall ann. Doc ann -> Doc ann -> Doc ann <+> forall a ann. Pretty a => a -> Doc ann pretty Specification fn k keySpec ] ) forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) a (m :: * -> *). (HasCallStack, HasSpec fn a, MonadGenError m) => Specification fn a -> GenT m a genFromSpecT Specification fn k keySpec Map k v -> [v] -> GenT m (Map k v) go (forall k a. Ord k => k -> a -> Map k a -> Map k a Map.insert k k v v Map k v m) [v] restVals' Map k v -> [v] -> GenT m (Map k v) go (forall k a. Ord k => [(k, a)] -> Map k a Map.fromList [(k, v)] mustMap) [v] restVals cardinalTypeSpec :: TypeSpec fn (Map k v) -> Specification fn Integer cardinalTypeSpec TypeSpec fn (Map k v) _ = forall (fn :: [*] -> * -> *) a. Specification fn a TrueSpec shrinkWithTypeSpec :: TypeSpec fn (Map k v) -> Map k v -> [Map k v] shrinkWithTypeSpec (MapSpec Maybe Integer _ Set k _ [v] _ Specification fn Integer _ Specification fn (k, v) kvs FoldSpec fn v _) Map k v m = forall a b. (a -> b) -> [a] -> [b] map forall k a. Ord k => [(k, a)] -> Map k a Map.fromList forall a b. (a -> b) -> a -> b $ forall a. (a -> [a]) -> [a] -> [[a]] shrinkList (forall (fn :: [*] -> * -> *) a. HasSpec fn a => Specification fn a -> a -> [a] shrinkWithSpec Specification fn (k, v) kvs) (forall k a. Map k a -> [(k, a)] Map.toList Map k v m) toPreds :: Term fn (Map k v) -> TypeSpec fn (Map k v) -> Pred fn toPreds Term fn (Map k v) m (MapSpec Maybe Integer mHint Set k mustKeys [v] mustVals Specification fn Integer size Specification fn (k, v) kvs FoldSpec fn v foldSpec) = forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, PredLike p, UnivConstr p fn) => p -> Pred fn toPred forall a b. (a -> b) -> a -> b $ [ forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit Set k mustKeys forall (fn :: [*] -> * -> *) a. (HasSpec fn a, Ord a) => Term fn (Set a) -> Term fn (Set a) -> Term fn Bool `subset_` forall (fn :: [*] -> * -> *) k v. (HasSpec fn (Map k v), HasSpec fn k, Ord k) => Term fn (Map k v) -> Term fn (Set k) dom_ Term fn (Map k v) m , forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a Lit [v] mustVals) forall a b. (a -> b) -> a -> b $ \Term fn v val -> Term fn v val forall a (fn :: [*] -> * -> *). HasSpec fn a => Term fn a -> Term fn [a] -> Term fn Bool `elem_` forall (fn :: [*] -> * -> *) k v. (HasSpec fn k, HasSpec fn v, Ord k) => Term fn (Map k v) -> Term fn [v] rng_ Term fn (Map k v) m , forall a (fn :: [*] -> * -> *). (HasSpec fn a, Sized a) => Term fn a -> Term fn Integer sizeOf_ (forall (fn :: [*] -> * -> *) k v. (HasSpec fn k, HasSpec fn v, Ord k) => Term fn (Map k v) -> Term fn [v] rng_ Term fn (Map k v) m) forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn `satisfies` Specification fn Integer size , forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term fn (Map k v) m forall a b. (a -> b) -> a -> b $ \Term fn (k, v) kv -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn satisfies Term fn (k, v) kv Specification fn (k, v) kvs , forall (fn :: [*] -> * -> *) a. BaseUniverse fn => Term fn [a] -> FoldSpec fn a -> Pred fn toPredsFoldSpec (forall (fn :: [*] -> * -> *) k v. (HasSpec fn k, HasSpec fn v, Ord k) => Term fn (Map k v) -> Term fn [v] rng_ Term fn (Map k v) m) FoldSpec fn v foldSpec , forall b a. b -> (a -> b) -> Maybe a -> b maybe forall (fn :: [*] -> * -> *). Pred fn TruePred (forall (fn :: [*] -> * -> *) t. HasGenHint fn t => Hint t -> Term fn t -> Pred fn `genHint` Term fn (Map k v) m) Maybe Integer mHint ] instance (Ord k, HasSpec fn (Prod k v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) => HasGenHint fn (Map k v) where type Hint (Map k v) = Integer giveHint :: Hint (Map k v) -> Specification fn (Map k v) giveHint Hint (Map k v) h = forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec forall a b. (a -> b) -> a -> b $ forall k (fn :: [*] -> * -> *) v. Ord k => MapSpec fn k v defaultMapSpec {mapSpecHint :: Maybe Integer mapSpecHint = forall a. a -> Maybe a Just Hint (Map k v) h} ------------------------------------------------------------------------ -- Functions ------------------------------------------------------------------------ instance BaseUniverse fn => Functions (MapFn fn) fn where propagateSpecFun :: forall (as :: [*]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) => MapFn fn as b -> ListCtx Value as (HOLE a) -> Specification fn b -> Specification fn a propagateSpecFun MapFn fn as b _ ListCtx Value as (HOLE a) _ Specification fn b TrueSpec = forall (fn :: [*] -> * -> *) a. Specification fn a TrueSpec propagateSpecFun MapFn fn as b _ ListCtx Value as (HOLE a) _ (ErrorSpec NonEmpty String err) = forall (fn :: [*] -> * -> *) a. NonEmpty String -> Specification fn a ErrorSpec NonEmpty String err propagateSpecFun MapFn fn as b fn ListCtx Value as (HOLE a) ctx Specification fn b spec = case MapFn fn as b fn of MapFn fn as b _ | SuspendedSpec Var b v Pred fn ps <- Specification fn b spec , ListCtx List Value as pre HOLE a a HOLE List Value as' suf <- ListCtx Value as (HOLE a) ctx -> forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term fn a v' -> let args :: List (Term fn) (Append as (a : as')) args = forall {a} (f :: a -> *) (as :: [a]) (bs :: [a]). List f as -> List f bs -> List f (Append as bs) appendList (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]). (forall (a :: k). f a -> g a) -> List f as -> List g as mapList (\(Value a a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a Lit a a) List Value as pre) (Term fn a v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]). f a -> List f as1 -> List f (a : as1) :> forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]). (forall (a :: k). f a -> g a) -> List f as -> List g as mapList (\(Value a a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a Lit a a) List Value as' suf) in forall (fn :: [*] -> * -> *) a. Term fn a -> Binder fn a -> Pred fn Let (forall (as :: [*]) (fn :: [*] -> * -> *) a. (Typeable as, TypeList as, All (HasSpec fn) as, HasSpec fn a, BaseUniverse fn) => fn as a -> List (Term fn) as -> Term fn a App (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn MapFn fn as b fn) List (Term fn) (Append as (a : as')) args) (Var b v forall (fn :: [*] -> * -> *) a. HasSpec fn a => Var a -> Pred fn -> Binder fn a :-> Pred fn ps) MapFn fn as b Dom -> -- No TypeAbstractions in ghc-8.10 case MapFn fn as b fn of (MapFn fn '[Map k v] (Set k) _ :: MapFn fn '[Map k v] (Set k)) | NilCtx HOLE a (Map k v) HOLE <- ListCtx Value as (HOLE a) ctx , Evidence (Prerequisites fn (Map k v)) Evidence <- forall (fn :: [*] -> * -> *) a. HasSpec fn a => Evidence (Prerequisites fn a) prerequisites @fn @(Map k v) -> case Specification fn b spec of MemberSpec [b s] -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) k v. Maybe Integer -> Set k -> [v] -> Specification fn Integer -> Specification fn (k, v) -> FoldSpec fn v -> MapSpec fn k v MapSpec forall a. Maybe a Nothing b s [] (forall a (fn :: [*] -> * -> *). a -> Specification fn a equalSpec forall a b. (a -> b) -> a -> b $ forall t. Sized t => t -> Integer sizeOf b s) forall (fn :: [*] -> * -> *) a. Specification fn a TrueSpec forall (fn :: [*] -> * -> *) a. FoldSpec fn a NoFold TypeSpec (SetSpec Set k must Specification fn k elemspec Specification fn Integer size) [] -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) k v. Maybe Integer -> Set k -> [v] -> Specification fn Integer -> Specification fn (k, v) -> FoldSpec fn v -> MapSpec fn k v MapSpec forall a. Maybe a Nothing Set k must [] Specification fn Integer size (forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term fn (k, v) kv -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn satisfies (forall (fn :: [*] -> * -> *) b (as :: [*]). (HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) => fn as b -> FunTy (MapList (Term fn) as) (Term fn b) app (forall (fn :: [*] -> * -> *) a b. Member (PairFn fn) fn => fn '[Prod a b] a fstFn @fn) (forall (fn :: [*] -> * -> *) b (as :: [*]). (HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) => fn as b -> FunTy (MapList (Term fn) as) (Term fn b) app (forall (fn :: [*] -> * -> *) a. (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) => fn '[a] (SimpleRep a) toGenericFn @fn) Term fn (k, v) kv)) Specification fn k elemspec) forall (fn :: [*] -> * -> *) a. FoldSpec fn a NoFold Specification fn b _ -> forall (fn :: [*] -> * -> *) a. NonEmpty String -> Specification fn a ErrorSpec (forall a. [a] -> NonEmpty a NE.fromList [String "Dom on bad map spec", forall a. Show a => a -> String show Specification fn b spec]) MapFn fn as b Rng -> -- No TypeAbstractions in ghc-8.10 case MapFn fn as b fn of (MapFn fn '[Map k v] [v] _ :: MapFn fn '[Map k v] [v]) | NilCtx HOLE a (Map k v) HOLE <- ListCtx Value as (HOLE a) ctx , Evidence (Prerequisites fn (Map k v)) Evidence <- forall (fn :: [*] -> * -> *) a. HasSpec fn a => Evidence (Prerequisites fn a) prerequisites @fn @(Map k v) -> case Specification fn b spec of TypeSpec (ListSpec Maybe Integer listHint [v] must Specification fn Integer size Specification fn v elemspec FoldSpec fn v foldspec) [] -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) k v. Maybe Integer -> Set k -> [v] -> Specification fn Integer -> Specification fn (k, v) -> FoldSpec fn v -> MapSpec fn k v MapSpec Maybe Integer listHint forall a. Set a Set.empty [v] must Specification fn Integer size (forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term fn (k, v) kv -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn satisfies (forall (fn :: [*] -> * -> *) b (as :: [*]). (HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) => fn as b -> FunTy (MapList (Term fn) as) (Term fn b) app (forall (fn :: [*] -> * -> *) a b. Member (PairFn fn) fn => fn '[Prod a b] b sndFn @fn) (forall (fn :: [*] -> * -> *) b (as :: [*]). (HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) => fn as b -> FunTy (MapList (Term fn) as) (Term fn b) app (forall (fn :: [*] -> * -> *) a. (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) => fn '[a] (SimpleRep a) toGenericFn @fn) Term fn (k, v) kv)) Specification fn v elemspec) FoldSpec fn v foldspec -- NOTE: you'd think `MemberSpec [r]` was a safe and easy case. However, that requires not only that the elements -- of the map are fixed to what is in `r`, but they appear in the order that they are in `r`. That's -- very difficult to achieve! Specification fn b _ -> forall (fn :: [*] -> * -> *) a. NonEmpty String -> Specification fn a ErrorSpec (forall a. [a] -> NonEmpty a NE.fromList [String "Rng on bad map spec", forall a. Show a => a -> String show Specification fn b spec]) MapFn fn as b Lookup -> case MapFn fn as b fn of MapFn fn '[k, Map k v] (Maybe v) Lookup :: MapFn fn '[k, Map k v] (Maybe v) | HOLE a a HOLE :? Value (Map k v m :: Map k v) :> List Value as1 Nil <- ListCtx Value as (HOLE a) ctx -> if forall a. Maybe a Nothing forall (fn :: [*] -> * -> *) a. HasSpec fn a => a -> Specification fn a -> Bool `conformsToSpec` Specification fn b spec then forall (fn :: [*] -> * -> *) a (f :: * -> *). (HasSpec fn a, Foldable f) => f a -> Specification fn a notMemberSpec [k k | (k k, v v) <- forall k a. Map k a -> [(k, a)] Map.toList Map k v m, Bool -> Bool not forall a b. (a -> b) -> a -> b $ forall a. a -> Maybe a Just v v forall (fn :: [*] -> * -> *) a. HasSpec fn a => a -> Specification fn a -> Bool `conformsToSpec` Specification fn b spec] else forall a (fn :: [*] -> * -> *). OrdSet a -> Specification fn a MemberSpec forall a b. (a -> b) -> a -> b $ forall k a. Map k a -> [k] Map.keys forall a b. (a -> b) -> a -> b $ forall a k. (a -> Bool) -> Map k a -> Map k a Map.filter (forall (fn :: [*] -> * -> *) a. HasSpec fn a => a -> Specification fn a -> Bool `conformsToSpec` Specification fn b spec) (forall a. a -> Maybe a Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Map k v m) | Value a k :! NilCtx HOLE a (Map k v) HOLE <- ListCtx Value as (HOLE a) ctx , Evidence (Prerequisites fn (Map k v)) Evidence <- forall (fn :: [*] -> * -> *) a. HasSpec fn a => Evidence (Prerequisites fn a) prerequisites @fn @(Map k v) -> forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term fn a m -> [forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit a k forall a (fn :: [*] -> * -> *). (HasSpec fn a, Ord a) => Term fn a -> Term fn (Set a) -> Term fn Bool `member_` forall (fn :: [*] -> * -> *) k v. (HasSpec fn (Map k v), HasSpec fn k, Ord k) => Term fn (Map k v) -> Term fn (Set k) dom_ Term fn a m | Bool -> Bool not forall a b. (a -> b) -> a -> b $ forall a. Maybe a Nothing forall (fn :: [*] -> * -> *) a. HasSpec fn a => a -> Specification fn a -> Bool `conformsToSpec` Specification fn b spec] forall a. [a] -> [a] -> [a] ++ [ forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term fn a m forall a b. (a -> b) -> a -> b $ \Term fn (a, v) kv -> forall (fn :: [*] -> * -> *) a p. (HasSpec fn a, IsPred p fn) => Term fn a -> (Term fn a -> p) -> Pred fn letBind (forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn (a, b) -> Term fn a fst_ Term fn (a, v) kv) forall a b. (a -> b) -> a -> b $ \Term fn a k' -> forall (fn :: [*] -> * -> *) a p. (HasSpec fn a, IsPred p fn) => Term fn a -> (Term fn a -> p) -> Pred fn letBind (forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn (a, b) -> Term fn b snd_ Term fn (a, v) kv) forall a b. (a -> b) -> a -> b $ \Term fn v v -> forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, IsPred p fn) => Term fn Bool -> p -> Pred fn whenTrue (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit a k forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Term fn a -> Term fn Bool ==. Term fn a k') forall a b. (a -> b) -> a -> b $ -- TODO: What you want to write is `cJust_ v `satisfies` spec` but we can't -- do that because we don't have access to `IsNormalType v` here. When -- we refactor the `IsNormalType` machinery we will be able to make -- this nicer. case Specification fn b spec of MemberSpec [b] as -> forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert forall a b. (a -> b) -> a -> b $ Term fn v v forall a (fn :: [*] -> * -> *). HasSpec fn a => Term fn a -> Term fn [a] -> Term fn Bool `elem_` forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit [v a | Just v a <- [b] as] TypeSpec (SumSpec Maybe (Int, Int) _ Specification fn () _ Specification fn v vspec) [b] cant -> Term fn v v forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn `satisfies` (Specification fn v vspec forall a. Semigroup a => a -> a -> a <> forall (fn :: [*] -> * -> *) a (f :: * -> *). (HasSpec fn a, Foldable f) => f a -> Specification fn a notMemberSpec [v a | Just v a <- [b] cant]) ] -- NOTE: this function over-approximates and returns a liberal spec. mapTypeSpec :: forall a b. (HasSpec fn a, HasSpec fn b) => MapFn fn '[a] b -> TypeSpec fn a -> Specification fn b mapTypeSpec MapFn fn '[a] b f TypeSpec fn a ts = case MapFn fn '[a] b f of -- TODO: consider checking against singleton member-specs in the other component -- interacting with cant MapFn fn '[a] b Dom -> -- No TypeAbstractions in ghc-8.10 case MapFn fn '[a] b f of (MapFn fn '[Map k v] (Set k) _ :: MapFn fn '[Map k v] (Set k)) | MapSpec Maybe Integer _ Set k mustSet [v] _ Specification fn Integer sz Specification fn (k, v) kvSpec FoldSpec fn v _ <- TypeSpec fn a ts , Evidence (Prerequisites fn (Map k v)) Evidence <- forall (fn :: [*] -> * -> *) a. HasSpec fn a => Evidence (Prerequisites fn a) prerequisites @fn @(Map k v) -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) a. Set a -> Specification fn a -> Specification fn Integer -> SetSpec fn a SetSpec Set k mustSet (forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => fn '[a] b -> Specification fn a -> Specification fn b mapSpec (forall (fn :: [*] -> * -> *) a b. Member (PairFn fn) fn => fn '[Prod a b] a fstFn @fn) forall a b. (a -> b) -> a -> b $ forall a (fn :: [*] -> * -> *). (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) => Specification fn a -> Specification fn (SimpleRep a) toSimpleRepSpec Specification fn (k, v) kvSpec) Specification fn Integer sz MapFn fn '[a] b Rng -> -- No TypeAbstractions in ghc-8.10 case MapFn fn '[a] b f of (MapFn fn '[Map k v] [v] _ :: MapFn fn '[Map k v] [v]) | MapSpec Maybe Integer _ Set k _ [v] mustList Specification fn Integer sz Specification fn (k, v) kvSpec FoldSpec fn v foldSpec <- TypeSpec fn a ts , Evidence (Prerequisites fn (Map k v)) Evidence <- forall (fn :: [*] -> * -> *) a. HasSpec fn a => Evidence (Prerequisites fn a) prerequisites @fn @(Map k v) -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) a. Maybe Integer -> [a] -> Specification fn Integer -> Specification fn a -> FoldSpec fn a -> ListSpec fn a ListSpec forall a. Maybe a Nothing [v] mustList Specification fn Integer sz (forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => fn '[a] b -> Specification fn a -> Specification fn b mapSpec (forall (fn :: [*] -> * -> *) a b. Member (PairFn fn) fn => fn '[Prod a b] b sndFn @fn) forall a b. (a -> b) -> a -> b $ forall a (fn :: [*] -> * -> *). (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) => Specification fn a -> Specification fn (SimpleRep a) toSimpleRepSpec Specification fn (k, v) kvSpec) FoldSpec fn v foldSpec ------------------------------------------------------------------------ -- Syntax ------------------------------------------------------------------------ dom_ :: (HasSpec fn (Map k v), HasSpec fn k, Ord k) => Term fn (Map k v) -> Term fn (Set k) dom_ :: forall (fn :: [*] -> * -> *) k v. (HasSpec fn (Map k v), HasSpec fn k, Ord k) => Term fn (Map k v) -> Term fn (Set k) dom_ = forall (fn :: [*] -> * -> *) b (as :: [*]). (HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) => fn as b -> FunTy (MapList (Term fn) as) (Term fn b) app forall (fn :: [*] -> * -> *) k v. (Member (MapFn fn) fn, Ord k) => fn '[Map k v] (Set k) domFn rng_ :: (HasSpec fn k, HasSpec fn v, Ord k) => Term fn (Map k v) -> Term fn [v] rng_ :: forall (fn :: [*] -> * -> *) k v. (HasSpec fn k, HasSpec fn v, Ord k) => Term fn (Map k v) -> Term fn [v] rng_ = forall (fn :: [*] -> * -> *) b (as :: [*]). (HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) => fn as b -> FunTy (MapList (Term fn) as) (Term fn b) app forall (fn :: [*] -> * -> *) k v. Member (MapFn fn) fn => fn '[Map k v] [v] rngFn lookup_ :: (HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) => Term fn k -> Term fn (Map k v) -> Term fn (Maybe v) lookup_ :: forall (fn :: [*] -> * -> *) k v. (HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) => Term fn k -> Term fn (Map k v) -> Term fn (Maybe v) lookup_ = forall (fn :: [*] -> * -> *) b (as :: [*]). (HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) => fn as b -> FunTy (MapList (Term fn) as) (Term fn b) app forall (fn :: [*] -> * -> *) k v. (Member (MapFn fn) fn, Ord k) => fn '[k, Map k v] (Maybe v) lookupFn