Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions src/Constrained/Conformance.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ module Constrained.Conformance (
monitorSpec,
conformsToSpec,
conformsToSpecE,
allConformToSpec,
satisfies,
checkPredE,
checkPredsE,
Expand All @@ -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)
Expand Down Expand Up @@ -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
Expand Down
17 changes: 9 additions & 8 deletions src/Constrained/Spec/Map.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Constrained/Spec/Set.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down