initial stab at speeding up maps with more optimistic first assumption

Author: MaximilianAlgehed

src/Constrained/Conformance.hs

@@ -13,6 +13,7 @@ module Constrained.Conformance (
   monitorSpec,
   conformsToSpec,
   conformsToSpecE,
+  allConformToSpec,
   satisfies,
   checkPredE,
   checkPredsE,
@@ -30,6 +31,8 @@ import Constrained.Syntax
 import Data.List (intersect, nub)
 import Data.List.NonEmpty qualified as NE
 import Data.Maybe
+import Data.Set (Set)
+import Data.Set qualified as Set
 import Data.Semigroup (sconcat)
 import Prettyprinter hiding (cat)
 import Test.QuickCheck (Property, Testable, property)
@@ -171,6 +174,11 @@ conformsToSpec a x = case conformsToSpecE a x (pure "call to conformsToSpecE") o
   Nothing -> True
   Just _ -> False
 
+allConformToSpec :: (HasSpec a, Ord a) => Set a -> Specification a -> Bool
+allConformToSpec xs (MemberSpec ys) = null $ xs Set.\\ Set.fromList (NE.toList ys)
+allConformToSpec _ TrueSpec = True
+allConformToSpec xs spec = all (`conformsToSpec` spec) xs
+
 -- | Embed a `Specification` in a `Pred`. Useful for re-using `Specification`s
 satisfies :: forall a. HasSpec a => Term a -> Specification a -> Pred
 satisfies e (ExplainSpec [] s) = satisfies e s

src/Constrained/Spec/Map.hs

@@ -184,14 +184,19 @@ instance
                 , geqSpec 0
                 ]
         n <- genFromSpecT size'
-        let go 0 _ m = pure m
-            go n' kvs' m = do
+        let go sz 0 slow kvs' m
+              | fromInteger sz == Map.size m = pure m
+              | not slow = go sz (sz - fromIntegral (Map.size m)) True (kvs' <> typeSpec (Cartesian (notMemberSpec (Map.keys m)) mempty)) m
+              | otherwise = fatalError "The impossible happened"
+            go sz n' slow kvs' m = do
               mkv <- inspect $ genFromSpecT kvs'
               case mkv of
                 Result (k, v) ->
                   go
+                    sz
                     (n' - 1)
-                    (kvs' <> typeSpec (Cartesian (notEqualSpec k) mempty))
+                    slow
+                    (kvs' <> if slow then typeSpec (Cartesian (notEqualSpec k) mempty) else mempty)
                     (Map.insert k v m)
                 GenError msgs ->
                   if sizeOf m `conformsToSpec` size
@@ -210,15 +215,11 @@ instance
                         , "The computed target size " ++ show n
                         , "Fatal error messages"
                         , "<<<---"
-                        -- , "The kvs Spec"
-                        -- , " >>>> "++ show $ "  kvs' = " <> pretty kvs'
-                        -- , "The simplified kvs Spec"
-                        -- , " >>>> "++ show(pretty (simplifySpec kvs'))
                         ]
                         <> catMessageList msgs
                         <> (pure "--->>>")
                     )
-        explain ("  The number we are trying for: n = " ++ show n) $ go n kvs mempty
+        explain ("  The number we are trying for: n = " ++ show n) $ go n n False kvs mempty
   genFromTypeSpec (MapSpec mHint mustKeys mustVals size (simplifySpec -> kvs) foldSpec) = do
     !mustMap <- explain "Make the mustMap" $ forM (Set.toList mustKeys) $ \k -> do
       let vSpec = constrained $ \v -> satisfies (pair_ (Lit k) v) kvs

src/Constrained/Spec/Set.hs

@@ -130,7 +130,7 @@ instance (Ord a, HasSpec a) => HasSpec (Set a) where
       ]
 
   genFromTypeSpec (SetSpec must e _)
-    | any (not . (`conformsToSpec` e)) must =
+    | not $ allConformToSpec must e =
         genErrorNE
           ( NE.fromList
               [ "Failed to generate set"