constrained-generators: Fix bug in sizeOf + improve some generators

for soundness tests

[no ci]

libs/constrained-generators/src/Constrained/Base.hs

@@ -618,6 +618,25 @@ instance HasSpec fn a => Semigroup (Specification fn a) where
 instance HasSpec fn a => Monoid (Specification fn a) where
   mempty = TrueSpec
 
+instance (HasSpec fn a, Arbitrary (TypeSpec fn a)) => Arbitrary (Specification fn a) where
+  arbitrary =
+    frequency [ (2, pure TrueSpec)
+              , (7, MemberSpec <$> listOf (genFromSpec_ @fn TrueSpec))
+              , (7, TypeSpec <$> arbitrary <*> listOf (genFromSpec_ @fn TrueSpec))
+              , (1, ErrorSpec <$> arbitrary)
+              ]
+
+  shrink TrueSpec = []
+  shrink (MemberSpec xs) = TrueSpec : (MemberSpec <$> shrinkList (shrinkWithSpec @fn TrueSpec) xs)
+  shrink (TypeSpec ts cant)
+    | null cant = TrueSpec : map typeSpec (shrink ts)
+    | otherwise =
+        [ TrueSpec, typeSpec ts ] ++
+        map typeSpec (shrink ts) ++
+        map (TypeSpec ts) (shrinkList (shrinkWithSpec @fn TrueSpec) cant)
+  shrink SuspendedSpec{} = [TrueSpec, MemberSpec []]
+  shrink ErrorSpec{} = [TrueSpec, MemberSpec []]
+
 equalSpec :: a -> Specification fn a
 equalSpec = MemberSpec . pure
 
@@ -3098,6 +3117,17 @@ instance Ord n => Semigroup (NumSpec n) where
 instance Ord n => Monoid (NumSpec n) where
   mempty = NumSpecInterval Nothing Nothing
 
+instance (Arbitrary a, Ord a) => Arbitrary (NumSpec a) where
+  arbitrary = do
+    m <- arbitrary
+    m' <- arbitrary
+    frequency [(10, pure $ mkLoHiInterval m m'), (1, pure $ NumSpecInterval m m')]
+    where
+      mkLoHiInterval (Just a) (Just b) = NumSpecInterval (Just $ min a b) (Just $ max a b)
+      mkLoHiInterval m m' = NumSpecInterval m m'
+  shrink (NumSpecInterval m m') =
+    uncurry NumSpecInterval <$> shrink (m, m')
+
 instance Arbitrary Natural where
   arbitrary = wordToNatural . abs <$> arbitrary
   shrink n = [wordToNatural w | w <- shrink (naturalToWord n)]
@@ -4178,7 +4208,8 @@ instance (BaseUniverse fn, HasSpec fn Integer) => Functions (SizeFn fn) fn where
     constrained $ \x' ->
       let args = appendList (mapList (\(Value a) -> Lit a) pre) (x' :> mapList (\(Value a) -> Lit a) suf)
        in Let (App (injectFn fn) args) (x :-> p)
-  propagateSpecFun SizeOf (NilCtx HOLE) (TypeSpec x _) = liftSizeSpec x
+  -- TODO: there is a bug here! Need to account for the `cant` set!
+  propagateSpecFun SizeOf (NilCtx HOLE) (TypeSpec x cant) = liftSizeSpec x cant
   propagateSpecFun SizeOf (NilCtx HOLE) (MemberSpec xs) = liftMemberSpec xs
 
   mapTypeSpec f ts = mapTypeSpecSize f ts
@@ -4232,26 +4263,26 @@ maxSpec (TypeSpec (NumSpecInterval _ hi) bad) = TypeSpec (NumSpecInterval Nothin
 
 class Sized t where
   sizeOf :: t -> Integer
-  liftSizeSpec :: HasSpec fn t => SizeSpec -> Specification fn t
+  liftSizeSpec :: HasSpec fn t => SizeSpec -> [Integer] -> Specification fn t
   liftMemberSpec :: HasSpec fn t => OrdSet Integer -> Specification fn t
   sizeOfTypeSpec :: HasSpec fn t => TypeSpec fn t -> Specification fn Integer
 
 instance Ord a => Sized (Set.Set a) where
   sizeOf = toInteger . Set.size
-  liftSizeSpec spec = typeSpec (SetSpec mempty TrueSpec (typeSpec spec))
+  liftSizeSpec spec cant = typeSpec (SetSpec mempty TrueSpec (TypeSpec spec cant))
   liftMemberSpec xs = typeSpec (SetSpec mempty TrueSpec (MemberSpec xs))
   sizeOfTypeSpec (SetSpec must _ sz) = sz <> (TypeSpec (atLeastSize (sizeOf must)) [])
 
 instance Sized [a] where
   sizeOf = toInteger . length
-  liftSizeSpec spec = typeSpec (ListSpec Nothing mempty (typeSpec spec) TrueSpec NoFold)
+  liftSizeSpec spec cant = typeSpec (ListSpec Nothing mempty (TypeSpec spec cant) TrueSpec NoFold)
   liftMemberSpec xs = typeSpec (ListSpec Nothing mempty (MemberSpec xs) TrueSpec NoFold)
   sizeOfTypeSpec (ListSpec _ _ _ ErrorSpec {} _) = equalSpec 0
   sizeOfTypeSpec (ListSpec _ must sizespec _ _) = sizespec <> (TypeSpec (atLeastSize (sizeOf must)) [])
 
 -- How to constrain the size of any type, with a Sized instance
 hasSize :: (HasSpec fn t, Sized t) => SizeSpec -> Specification fn t
-hasSize sz = liftSizeSpec sz
+hasSize sz = liftSizeSpec sz []
 
 -- ==================================================================================
 -- (NumSpec Integer) can support interval arithmetic, so we can make a (Num (NumSpec fn Integer)) instance

libs/constrained-generators/src/Constrained/Properties.hs

@@ -12,7 +12,6 @@
 -- | Useful properties for debugging custom @HasSpec@ instances.
 module Constrained.Properties where
 
-import Data.List (sort)
 import Data.Map (Map)
 import Data.Typeable
 import Constrained.Base
@@ -110,7 +109,7 @@ prop_propagateSpecFun fn ctx spec =
 prop_univSound :: forall fn. TestableFn fn -> QC.Property
 prop_univSound (TestableFn fn) =
     QC.label (show fn) $
-      QC.forAllShow QC.arbitrary (\ (TestableCtx ctx) -> "<<PLACEHOLDER>>") $ \ (TestableCtx theCtx :: TestableCtx fn as) ->
+      QC.forAllShow QC.arbitrary (\ (TestableCtx _ctx) -> "<<PLACEHOLDER>>") $ \ (TestableCtx theCtx :: TestableCtx fn as) ->
         QC.forAllShrink QC.arbitrary QC.shrink $ \ theSpec ->
           prop_propagateSpecFun fn theCtx theSpec
 
@@ -120,11 +119,13 @@ data TestableFn fn where
                 , HasSpec fn b
                 , Typeable as
                 , QC.Arbitrary (Specification fn b)
+                , Typeable (FunTy as b)
                 ) => fn as b -> TestableFn fn
 
 -- TODO: also show type here
 instance BaseUniverse fn => Show (TestableFn fn) where
-  show (TestableFn fn) = show fn
+  show (TestableFn (fn :: fn as b)) =
+    show fn ++ " :: " ++ show (typeOf (undefined :: FunTy as b))
 
 data TestableCtx fn as where
   TestableCtx :: HasSpec fn a
@@ -145,31 +146,7 @@ instance forall fn as. (All (HasSpec fn) as, TypeList as) => QC.Arbitrary (Testa
         TestableCtx . (:! ctx) . Value <$> genFromSpec_ @fn TrueSpec
       go _ _ = error "The impossible happened in Arbitrary for TestableCtx"
 
-instance (QC.Arbitrary a, Ord a) => QC.Arbitrary (NumSpec a) where
-  arbitrary = do
-    m <- QC.arbitrary
-    m' <- QC.arbitrary
-    case (m, m') of
-      (Just a, Just b) -> pure $ NumSpecInterval (Just $ min a b) (Just $ max a b)
-      _ -> pure $ NumSpecInterval m m'
-
-instance (HasSpec fn a, QC.Arbitrary (TypeSpec fn a)) => QC.Arbitrary (Specification fn a) where
-  arbitrary = QC.oneof [ pure TrueSpec
-                       , do a <- genFromSpec_ @fn TrueSpec
-                            as <- QC.listOf (genFromSpec_ @fn TrueSpec)
-                            pure $ MemberSpec (a : as)
-                       , TypeSpec <$> QC.arbitrary <*> QC.listOf (genFromSpec_ @fn TrueSpec)
-                       ]
-  shrink TrueSpec = []
-  shrink (MemberSpec xs) = TrueSpec : (MemberSpec <$> QC.shrinkList (shrinkWithSpec @fn TrueSpec) xs)
-  shrink (TypeSpec ts cant)
-    | null cant = typeSpec <$> QC.shrink ts
-    | otherwise =
-        [ typeSpec ts ] ++
-        map typeSpec (QC.shrink ts) ++
-        map (TypeSpec ts) (QC.shrinkList (shrinkWithSpec @fn TrueSpec) cant)
-
-
+-- TODO: we should improve these
 instance (fn ~ BaseFn) => QC.Arbitrary (TestableFn fn) where
   arbitrary = QC.elements [ TestableFn $ addFn @fn @Int
                           , TestableFn $ negateFn @fn @Int

libs/constrained-generators/src/Constrained/Spec/Map.hs

@@ -36,7 +36,7 @@ import Test.QuickCheck (shrinkList)
 
 instance Ord a => Sized (Map.Map a b) where
   sizeOf = toInteger . Map.size
-  liftSizeSpec sz = typeSpec $ defaultMapSpec {mapSpecSize = typeSpec sz}
+  liftSizeSpec sz cant = typeSpec $ defaultMapSpec {mapSpecSize = TypeSpec sz cant}
   liftMemberSpec xs = typeSpec $ defaultMapSpec {mapSpecSize = MemberSpec xs}
   sizeOfTypeSpec (MapSpec _ mustk mustv size _ _) =
     typeSpec (atLeastSize (sizeOf mustk))

libs/constrained-generators/test/Constrained/Test.hs

@@ -135,6 +135,7 @@ tests =
       prop "Map Int Int" $ prop_conformEmpty @BaseFn @(Map Int Int)
       prop "[Int]" $ prop_conformEmpty @BaseFn @[Int]
       prop "[(Int, Int)]" $ prop_conformEmpty @BaseFn @[(Int, Int)]
+    prop "prop_univSound @BaseFn" $ withMaxSuccess 10000 $ prop_univSound @BaseFn
     negativeTests
 
 negativeTests :: Spec
@@ -235,15 +236,6 @@ testSpec' withShrink n s =
 -- Test properties of the instance Num (NumSpec Integer)
 ------------------------------------------------------------------------
 
-instance Arbitrary (NumSpec Integer) where
-  arbitrary = do
-    lo <- arbitrary
-    hi <- next lo
-    pure $ NumSpecInterval lo hi
-    where
-      next Nothing = arbitrary
-      next (Just n) = frequency [(1, pure Nothing), (3, Just <$> suchThat arbitrary (> n))]
-
 -- | When we multiply intervals, we get a bounding box, around the possible values.
 --   When the intervals have infinities, the bounding box can be very loose. In fact the
 --   order in which we multiply intervals with infinities can affect how loose the bounding box is.