diff --git a/libs/constrained-generators/src/Constrained/Base.hs b/libs/constrained-generators/src/Constrained/Base.hs index 47e7d139062..f3a55785946 100644 --- a/libs/constrained-generators/src/Constrained/Base.hs +++ b/libs/constrained-generators/src/Constrained/Base.hs @@ -2865,15 +2865,7 @@ instance (Ord a, HasSpec fn a) => HasSpec fn (Set a) where n <- explain ["Choose a possible size Bounds for the Sets to be generated"] $ genFromSizeSpec (szSpec <> geqSpec @fn (sizeOf must) <> maxSpec (cardinality elemS)) - go (n - sizeOf must) must - where - go 0 s = pure s - go n s = do - e <- - explain ["generate set member"] $ - withMode Strict $ - genFromSpec elemS `suchThatT` (`Set.notMember` s) - go (n - 1) (Set.insert e s) + Set.fromList <$> genDistinctList elemS (n - sizeOf must) (Set.toList must) shrinkWithTypeSpec (SetSpec _ es _) as = map Set.fromList $ shrinkList (shrinkWithSpec es) (Set.toList as) @@ -4566,3 +4558,13 @@ checkForNegativeSize spec@(TypeSpec (NumSpecInterval x y) _) = (_, _) -> spec checkForNegativeSize (MemberSpec xs) | any (< 0) xs = ErrorSpec ["Negative Size in MemberSpec " ++ show xs] checkForNegativeSize spec = spec + +genDistinctList :: + (MonadGenError m, HasSpec fn a) => Specification fn a -> Integer -> [a] -> GenT m [a] +genDistinctList _ 0 s = pure s +genDistinctList elemS n s = do + e <- + explain ["generate a new distinct member not in:", "\n " ++ show s] $ + withMode Strict $ + genFromSpec elemS `suchThatT` (`notElem` s) + genDistinctList elemS (n - 1) (e : s) diff --git a/libs/constrained-generators/src/Constrained/Spec/Map.hs b/libs/constrained-generators/src/Constrained/Spec/Map.hs index cf499b51343..3a42293afd0 100644 --- a/libs/constrained-generators/src/Constrained/Spec/Map.hs +++ b/libs/constrained-generators/src/Constrained/Spec/Map.hs @@ -2,6 +2,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE GADTs #-} {-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -21,7 +22,8 @@ import Constrained.Instances () import Constrained.List import Constrained.Spec.Generics import Constrained.Univ -import Control.Monad + +-- import Control.Monad import Data.List (nub) import Data.Map (Map) import Data.Map qualified as Map @@ -47,7 +49,7 @@ instance Ord a => Sized (Map.Map a b) where sizeOfTypeSpec (MapSpec _ mustk mustv size _ _ smallest) = typeSpec (atLeastSize (sizeOf mustk)) <> typeSpec (atLeastSize (sizeOf mustv)) - <> smallestSpec smallest + <> extractFromMinValSize smallest <> size data MapSpec fn k v = MapSpec @@ -57,17 +59,18 @@ data MapSpec fn k v = MapSpec , mapSpecSize :: Specification fn Integer , mapSpecElem :: Specification fn (k, v) , mapSpecFold :: FoldSpec fn v - , mapSpecMinValSize :: Maybe (MinValSize v) - -- The smallest number of unique Values that meet spec. - -- This should look like: Nothing or (Just n), - -- if it is (Just n), it means the size of the rngSet is constrained by (NumspecInterval (Just n) Nothing) + , mapSpecMinValSize :: Maybe (MinValSize fn v) + -- Specifaction of the number of unique Values in the range of the Map that meet the Mapspec. + -- The Maybe is there because Nothing means (MinValSpec TrueSpec), + -- but does require the (Ord v) constraint } -data MinValSize v where - MinValSize :: Ord v => Integer -> MinValSize v +-- | Spec of the the number of unique values in the range of a map, needed to conform to the MapSpec +-- Just a Spec, but carries the (Ord v) constraint +data MinValSize fn v where + MinValSize :: Ord v => Specification fn Integer -> MinValSize fn v -deriving instance Eq (MinValSize v) -deriving instance Show (MinValSize v) +deriving instance BaseUniverse fn => Show (MinValSize fn v) -- | emptySpec without all the constraints defaultMapSpec :: Ord k => MapSpec fn k v @@ -85,7 +88,7 @@ instance Ord k => Forallable (Map k v) (k, v) where forAllToList = Map.toList instance - (Ord k, Functions fn fn, HasSpec fn (Prod k v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) => + (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 @@ -118,21 +121,24 @@ instance , trace "size" $ sizeOf m `conformsToSpec` size , trace "conforms pairs" $ all (`conformsToSpec` kvs) (Map.toList m) , trace "conforms fold" $ Map.elems m `conformsToFoldSpec` foldSpec - , trace "conformms smallest" $ conformsToSpec @fn (sizeOf (nub (Map.elems m))) (smallestSpec minval) + , trace "conformms smallest" $ + conformsToSpec @fn (sizeOf (nub (Map.elems m))) (extractFromMinValSize minval) ] - genFromTypeSpec m@(MapSpec mHint mustKeys mustVals size (simplifySpec -> kvs) foldSpec _smallest) = trace ("\nGENMAP\n" ++ show m) $ do - mustMap <- explain ["Make the mustMap"] $ forM (Set.toList mustKeys) $ \k -> do - let vSpec = constrained $ \v -> satisfies (pair_ (lit k) v) kvs - v <- explain [show $ "vSpec =" <+> pretty vSpec] $ genFromSpec vSpec - pure (k, v) + genFromTypeSpec m@(MapSpec mHint mustKeys mustVals size (simplifySpec -> kvs) foldSpec vsize) = trace ("\nGENMAP\n" ++ show m) $ do + (mustMap, residualCount) <- freshMust (Set.toList mustKeys) vsize kvs let haveVals = map snd mustMap mustVals' = filter (`notElem` haveVals) mustVals + size' :: Specification fn Integer size' = constrained $ \sz -> -- TODO, we should make sure size' is greater than or equal to 0 satisfies (sz + Lit (sizeOf mustMap)) - (maybe TrueSpec leqSpec mHint <> size <> cardinality (mapSpec fstFn $ mapSpec toGenericFn kvs)) + ( maybe TrueSpec leqSpec mHint + <> geqSpec residualCount + <> size + <> cardinality (mapSpec fstFn $ mapSpec toGenericFn kvs) + ) foldSpec' = case foldSpec of NoFold -> NoFold FoldSpec fn sumSpec -> FoldSpec fn $ propagateSpecFun (theAddFn @fn) (HOLE :? Value mustSum :> Nil) sumSpec @@ -144,27 +150,29 @@ instance mustVals' size' (simplifySpec $ constrained $ \v -> unsafeExists $ \k -> pair_ k v `satisfies` kvs) - -- old before rebase on master - -- (constrained $ \v -> unsafeExists $ \p -> p `satisfies` kvs <> assert (snd_ p ==. v)) foldSpec' - restVals <- explain - [ "Make the restVals" - , " valsSpec = " ++ show valsSpec - ] - $ genFromTypeSpec - $ valsSpec - let go m [] = pure m - go m (v : restVals') = do - let keySpec = notMemberSpec (Map.keysSet m) <> constrained (\k -> pair_ k (lit v) `satisfies` kvs) + ["Make the restVals", " valsSpec = " ++ show valsSpec] + $ case vsize of + Nothing -> genFromTypeSpec @fn valsSpec + Just (MinValSize _) -> do + vcount <- genFromSpec size' + genDistinctList + (simplifySpec $ constrained $ \v -> unsafeExists $ \k -> pair_ k v `satisfies` kvs) + vcount + mustVals' + + let go ms [] = pure ms + go ms (v : restVals') = do + let keySpec = notMemberSpec (Map.keysSet ms) <> constrained (\k -> pair_ k (lit v) `satisfies` kvs) k <- explain [ "Make a key" , show $ indent 4 $ "keySpec =" <+> pretty keySpec ] $ genFromSpec keySpec - go (Map.insert k v m) restVals' + go (Map.insert k v ms) restVals' go (Map.fromList mustMap) restVals shrinkWithTypeSpec (MapSpec _ _ _ _ kvs _ _) m = map Map.fromList $ shrinkList (shrinkWithSpec kvs) (Map.toList m) @@ -177,7 +185,7 @@ instance , sizeOf_ (rng_ m) `satisfies` size , case minvalsize of Nothing -> TruePred - Just (MinValSize n) -> sizeOf_ (rngSet_ m) `satisfies` (leqSpec n) + Just (MinValSize n) -> sizeOf_ (rngSet_ m) `satisfies` n , forAll m $ \kv -> satisfies kv kvs , toPredsFoldSpec (rng_ m) foldSpec , maybe TruePred (`genHint` m) mHint @@ -261,7 +269,7 @@ instance BaseUniverse fn => Functions (MapFn fn) fn where (equalSpec $ sizeOf r) TrueSpec NoFold - (Just (MinValSize (sizeOf r))) + (Just (MinValSize (equalSpec (sizeOf r)))) TypeSpec (ss@(SetSpec must elemspec setsize)) [] -> trace ("\nSETSPEC (" ++ show ss ++ ")") $ let mp = @@ -272,18 +280,8 @@ instance BaseUniverse fn => Functions (MapFn fn) fn where ((geqSpec (fromIntegral (Set.size must))) <> setsize) -- This might be overconstrained. (constrained $ \kv -> satisfies (app (sndFn @fn) (app (toGenericFn @fn) kv)) elemspec) NoFold - (smallest setsize) + (injectMinValSize setsize) in trace ("\nMAPSPEC " ++ show mp) (typeSpec mp) - {- - - typeSpec $ - MapSpec - Nothing - Set.empty - (Set.toList must) - ((geqSpec (fromIntegral (Set.size must))) <> setsize) -- This might be overconstrained. - (constrained $ \kv -> satisfies (app (sndFn @fn) (app (toGenericFn @fn) kv)) elemspec) - NoFold -} _ -> ErrorSpec ["RngSet on bad map spec", show spec] -- NOTE: this function over-approximates and returns a liberal spec. @@ -352,26 +350,81 @@ soundSpec specx = do _zzz :: Bool _zzz = conformsToSpec (Map.fromList [(-1, 0), (0, 0), (1, 0)] :: Map Int Int) rngSpec --- ==================== -{- -smallestAcceptableSize :: NumSpec Integer -> NumSpec Integer -> NumSpec Integer -smallestAcceptableSize (NumSpecInterval x y) (NumSpecInterval a b) = NumSpecInterval (maxL x a) (max <$> y <*> b) - where maxL Nothing Nothing = Nothing - maxL Nothing (Just x) = Just x - maxL (Just x) Nothing = Just x - maxL (Just x) (Just y) = Just(max x y) --} +-- ====================================================================== +-- How to deal with size constraints on the RngSet of a Map -smallestAcceptableSize :: Maybe (MinValSize v) -> Maybe (MinValSize v) -> Maybe (MinValSize v) -smallestAcceptableSize Nothing Nothing = Nothing -smallestAcceptableSize Nothing (Just x) = Just x -smallestAcceptableSize (Just x) Nothing = Just x -smallestAcceptableSize (Just (MinValSize x)) (Just (MinValSize y)) = Just (MinValSize (max x y)) +-- | Merge two MinValeSizes, each in a separate MapSpec +smallestAcceptableSize :: + BaseUniverse fn => Maybe (MinValSize fn v) -> Maybe (MinValSize fn v) -> Maybe (MinValSize fn v) +smallestAcceptableSize (Just (MinValSize x)) (Just (MinValSize y)) = Just (MinValSize (x <> y)) +smallestAcceptableSize Nothing x = x +smallestAcceptableSize x Nothing = x -smallestSpec :: BaseUniverse fn => Maybe (MinValSize v) -> Specification fn Integer -smallestSpec smallest = case smallest of - Just (MinValSize n) -> leqSpec n - Nothing -> TrueSpec +-- | Extract a Specification from (Maybe (MinValSize fn v)), Nothing extracts TrueSpec +extractFromMinValSize :: Maybe (MinValSize fn v) -> Specification fn Integer +extractFromMinValSize (Just (MinValSize s)) = s +extractFromMinValSize Nothing = TrueSpec -smallest :: Ord v => Specification fn Integer -> Maybe (MinValSize v) -smallest TrueSpec = Nothing +-- | Inject a Specification into a (Maybe (MinValSize fn v)) +injectMinValSize :: Ord v => Specification fn Integer -> Maybe (MinValSize fn v) +injectMinValSize TrueSpec = Nothing +injectMinValSize spec = Just (MinValSize spec) + +{- +-- | Extend a list of map pairs, until the range has an acceptable size. +extendMapPairs :: forall fn m k v. (Ord k,HasSpec fn k, HasSpec fn v,IsNormalType v,IsNormalType k,MonadGenError m) => + [(k,v)] -> + Specification fn (k, v) -> + Maybe(MinValSize fn v) -> + GenT m [(k,v)] +extendMapPairs pairs _ Nothing = pure pairs +extendMapPairs pairs okpair (Just (MinValSize minSizeSpec)) = do + minSize <- genFromSpec minSizeSpec + let n = minSize - sizeOf pairs + go :: [(k,v)] -> Integer -> GenT m [(k,v)] + go newpairs count | count<=0 = pure newpairs + go newpairs count = do + pair <- genFromSpec (fresh newpairs okpair) + go (pair : newpairs) (count -1) + go pairs n +-} + +freshU :: + forall fn k v. + (Ord v, HasSpec fn k, HasSpec fn v) => + [(k, v)] -> + k -> + Specification fn (k, v) -> + Specification fn (k, v) +freshU ps mustk okpair = + constrained + ( \pair -> + [ satisfies pair okpair + , assert $ lit mustk ==. (fst_ pair) + , assert $ not_ (member_ (snd_ pair) (lit (Set.fromList (map snd ps)))) + ] + ) + +freshMust :: + forall fn k v m. + (HasSpec fn k, HasSpec fn v, MonadGenError m) => + [k] -> + Maybe (MinValSize fn v) -> + Specification fn (k, v) -> + GenT m ([(k, v)], Integer) +freshMust keys size ok = case size of + Nothing -> go2 keys [] + Just (MinValSize szspec) -> do countx <- genFromSpec szspec; go keys countx [] + where + go :: Ord v => [k] -> Integer -> [(k, v)] -> GenT m ([(k, v)], Integer) + go [] countx pairs = pure (reverse pairs, countx) + go ks 0 pairs = go2 ks pairs + go (k : ks) countx pairs = do + let freshVSpec = (freshU pairs k ok) + pair <- explain [show $ "vSpec =" <+> pretty freshVSpec] (genFromSpec freshVSpec) + go ks (countx - 1) (pair : pairs) + go2 :: [k] -> [(k, v)] -> GenT m ([(k, v)], Integer) + go2 [] pairs = pure (reverse pairs, 0) + go2 (k : ks) pairs = do + pair <- genFromSpec (constrained (\p -> [satisfies p ok, assert $ lit k ==. (fst_ p)])) + go2 ks (pair : pairs)