Use MinValSize in genFromTypeSpec for Maps

IntersectMBO · May 15, 2024 · e132b2d · e132b2d
1 parent 3886dcd
commit e132b2d
Show file tree

Hide file tree

Showing 2 changed files with 127 additions and 72 deletions.
diff --git 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
@@ -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)