input-output-hk / constrained-generators / 414

Committed 21 Nov 2025 07:55AM UTC coverage: 76.458% (-0.8%) from 77.228%

Build # 414

Build Type

push

github

Committed by

web-flow

Commit Message

Speed up generation by threading seeds instead of splitting them in non-`Gen` part of `GenT` (#57)

Run Details

33 of 44 new or added lines in 1 file covered. (75.0%)

58 existing lines in 7 files now uncovered.

3907 of 5110 relevant lines covered (76.46%)

1.44 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

73.23

/src/Constrained/Spec/Set.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | `HasSpec` instance for `Set`s and functions for writing
-- constraints about sets
module Constrained.Spec.Set (
  SetSpec (..),
  SetW (..),
  singleton_,
  subset_,
  member_,
  union_,
  disjoint_,
  fromList_,
) where

import Constrained.AbstractSyntax
import Constrained.Base
import Constrained.Conformance
import Constrained.Core
import Constrained.FunctionSymbol
import Constrained.GenT
import Constrained.Generation
import Constrained.List
import Constrained.NumOrd
import Constrained.PrettyUtils
import Constrained.Spec.List
import Constrained.SumList
import Constrained.Syntax
import Constrained.TheKnot
import Data.Foldable
import Data.Kind
import Data.List ((\\))
import qualified Data.List.NonEmpty as NE
import Data.Set (Set)
import qualified Data.Set as Set
import Prettyprinter hiding (cat)
import Test.QuickCheck (shrinkList, shuffle)

------------------------------------------------------------------------
-- HasSpec instance for Set
------------------------------------------------------------------------

-- | `TypeSpec` for `Set`
data SetSpec a
  = SetSpec
      -- | Required elements
      (Set a)
      -- | Specification for elements
      (Specification a)
      -- | Specification for size
      (Specification Integer)

instance Ord a => Sized (Set.Set a) where
  sizeOf = toInteger . Set.size
  liftSizeSpec spec cant = typeSpec (SetSpec mempty TrueSpec (TypeSpec spec cant))
  liftMemberSpec xs = case NE.nonEmpty xs of
    Nothing -> ErrorSpec (pure "In liftMemberSpec for the (Sized Set) instance, xs is the empty list")
    Just zs -> typeSpec (SetSpec mempty TrueSpec (MemberSpec zs))
  sizeOfTypeSpec (SetSpec must _ sz) = sz <> geqSpec (sizeOf must)

instance (Ord a, HasSpec a) => Semigroup (SetSpec a) where
  SetSpec must es size <> SetSpec must' es' size' =
    SetSpec (must <> must') (es <> es') (size <> size')

instance (Ord a, HasSpec a) => Monoid (SetSpec a) where
  mempty = SetSpec mempty mempty TrueSpec

instance Ord a => Forallable (Set a) a where
  fromForAllSpec (e :: Specification a)
    | Evidence <- prerequisites @(Set a) = typeSpec $ SetSpec mempty e TrueSpec
  forAllToList = Set.toList

prettySetSpec :: HasSpec a => SetSpec a -> Doc ann
prettySetSpec (SetSpec must elemS size) =
  parens
    ( "SetSpec"
        /> sep ["must=" <> viaShow (Set.toList must), "elem=" <> pretty elemS, "size=" <> pretty size]
    )

instance HasSpec a => Show (SetSpec a) where
  show x = show (prettySetSpec x)

guardSetSpec :: (HasSpec a, Ord a) => [String] -> SetSpec a -> Specification (Set a)
guardSetSpec es (SetSpec must elemS ((<> geqSpec 0) -> size))
  | Just u <- knownUpperBound size
  , u < 0 =
      ErrorSpec (("guardSetSpec: negative size " ++ show u) :| es)
  | not (all (`conformsToSpec` elemS) must) =
      ErrorSpec (("Some 'must' items do not conform to 'element' spec: " ++ show elemS) :| es)
  | isErrorLike size = ErrorSpec ("guardSetSpec: error in size" :| es)
  | isErrorLike (geqSpec (sizeOf must) <> size) =
      ErrorSpec $
        ("Must set size " ++ show (sizeOf must) ++ ", is inconsistent with SetSpec size" ++ show size) :| es
  | isErrorLike (maxSpec (cardinality elemS) <> size) =
      ErrorSpec $
        NE.fromList $
          [ "Cardinality of SetSpec elemSpec (" ++ show elemS ++ ") = " ++ show (maxSpec (cardinality elemS))
          , "   This is inconsistent with SetSpec size (" ++ show size ++ ")"
          ]
            ++ es
  | otherwise = typeSpec (SetSpec must elemS size)

instance (Ord a, HasSpec a) => HasSpec (Set a) where
  type TypeSpec (Set a) = SetSpec a

  type Prerequisites (Set a) = HasSpec a

  emptySpec = mempty

  combineSpec s s' = guardSetSpec ["While combining 2 SetSpecs", "  " ++ show s, "  " ++ show s'] (s <> s')

  conformsTo s (SetSpec must es size) =
    and
      [ sizeOf s `conformsToSpec` size
      , must `Set.isSubsetOf` s
      , all (`conformsToSpec` es) s
      ]

  genFromTypeSpec (SetSpec must e _)
    | not $ allConformToSpec must e =
        genErrorNE
          ( NE.fromList
              [ "Failed to generate set"
              , "Some element in the must set does not conform to the elem specification"
              , "Unconforming elements from the must set:"
              , unlines (map (\x -> "  " ++ show x) (filter (not . (`conformsToSpec` e)) (Set.toList must)))
              , "Element Specifcation"
              , "  " ++ show e
              ]
          )
  -- Special case when elemS is a MemberSpec.
  -- Just union 'must' with enough elements of 'xs' to meet  'szSpec'
  genFromTypeSpec (SetSpec must (ExplainSpec [] elemspec) szSpec) =
    genFromTypeSpec (SetSpec must elemspec szSpec)
  genFromTypeSpec (SetSpec must (ExplainSpec (e : es) elemspec) szSpec) =
    explainNE (e :| es) $ genFromTypeSpec (SetSpec must elemspec szSpec)
  genFromTypeSpec (SetSpec must elemS@(MemberSpec xs) szSpec) = do
    let szSpec' = szSpec <> geqSpec (sizeOf must) <> maxSpec (cardinality elemS)
    choices <- pureGen $ shuffle (NE.toList xs \\ Set.toList must)
    size <- fromInteger <$> genFromSpecT szSpec'
    let additions = Set.fromList $ take (size - Set.size must) choices
    pure (Set.union must additions)
  genFromTypeSpec (SetSpec must elemS szSpec) = do
    let szSpec' = szSpec <> geqSpec (sizeOf must) <> maxSpec (cardinality elemS)
    chosenSize <-
      explain "Choose a size for the Set to be generated" $
        genFromSpecT szSpec'
    let targetSize = chosenSize - sizeOf must
    explainNE
      ( NE.fromList
          [ "Choose size = " ++ show chosenSize
          , "szSpec' = " ++ show szSpec'
          , "Picking items not in must = " ++ show (Set.toList must)
          , "that also meet the element test: "
          , "  " ++ show elemS
          ]
      )
      $ case theMostWeCanExpect of
        -- 0 means TrueSpec or SuspendedSpec so we can't rule anything out
        0 -> go 100 targetSize must
        n -> case compare n targetSize of
          LT -> fatalError "The number of things that meet the element test is too small."
          GT -> go 100 targetSize must
          EQ -> go 100 targetSize must
    where
      theMostWeCanExpect = maxFromSpec 0 (cardinality (simplifySpec elemS))
      go _ n s | n <= 0 = pure s
      go tries n s = do
        e <-
          explainNE
            ( NE.fromList
                [ "Generate set member at type " ++ showType @a
                , "  number of items starting with  = " ++ show (Set.size must)
                , "  number of items left to pick   = " ++ show n
                , "  number of items already picked = " ++ show (Set.size s)
                , "  the most items we can expect is " ++ show theMostWeCanExpect ++ " (a SuspendedSpec)"
                ]
            )
            $ withMode Strict
            $ suchThatWithTryT tries (genFromSpecT elemS) (`Set.notMember` s)

        go tries (n - 1) (Set.insert e s)

  cardinalTypeSpec (SetSpec _ es _)
    | Just ub <- knownUpperBound (cardinality es) = leqSpec (2 ^ ub)
  cardinalTypeSpec _ = TrueSpec

  cardinalTrueSpec
    | Just ub <- knownUpperBound $ cardinalTrueSpec @a = leqSpec (2 ^ ub)
    | otherwise = TrueSpec

  shrinkWithTypeSpec (SetSpec _ es _) as = map Set.fromList $ shrinkList (shrinkWithSpec es) (Set.toList as)

  -- TODO: fixme
  fixupWithTypeSpec _ _ = Nothing

  toPreds s (SetSpec m es size) =
    fold $
      -- Don't include this if the must set is empty
      [ Explain (pure (show m ++ " is a subset of the set.")) $ Assert $ subset_ (Lit m) s
      | not $ Set.null m
      ]
        ++ [ forAll s (\e -> satisfies e es)
           , satisfies (sizeOf_ s) size
           ]

  guardTypeSpec = guardSetSpec

------------------------------------------------------------------------
-- Functions that deal with sets
------------------------------------------------------------------------

-- | Symbols for working on sets
data SetW (d :: [Type]) (r :: Type) where
  SingletonW :: (HasSpec a, Ord a) => SetW '[a] (Set a)
  UnionW :: (HasSpec a, Ord a) => SetW '[Set a, Set a] (Set a)
  SubsetW :: (HasSpec a, Ord a, HasSpec a) => SetW '[Set a, Set a] Bool
  MemberW :: (HasSpec a, Ord a) => SetW '[a, Set a] Bool
  DisjointW :: (HasSpec a, Ord a) => SetW '[Set a, Set a] Bool
  FromListW :: (HasSpec a, Ord a) => SetW '[[a]] (Set a)

deriving instance Eq (SetW dom rng)

instance Show (SetW ds r) where
  show SingletonW = "singleton_"
  show UnionW = "union_"
  show SubsetW = "subset_"
  show MemberW = "member_"
  show DisjointW = "disjoint_"
  show FromListW = "fromList_"

setSem :: SetW ds r -> FunTy ds r
setSem SingletonW = Set.singleton
setSem UnionW = Set.union
setSem SubsetW = Set.isSubsetOf
setSem MemberW = Set.member
setSem DisjointW = Set.disjoint
setSem FromListW = Set.fromList

instance Semantics SetW where
  semantics = setSem

instance Syntax SetW where
  prettySymbol SubsetW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "subset_" <+> prettyShowSet n <+> prettyPrec 11 y
  prettySymbol SubsetW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "subset_" <+> prettyPrec 11 y <+> prettyShowSet n
  prettySymbol DisjointW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "disjoint_" <+> prettyShowSet n <+> prettyPrec 11 y
  prettySymbol DisjointW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "disjoint_" <+> prettyPrec 11 y <+> prettyShowSet n
  prettySymbol UnionW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "union_" <+> prettyShowSet n <+> prettyPrec 11 y
  prettySymbol UnionW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "union_" <+> prettyPrec 11 y <+> prettyShowSet n
  prettySymbol MemberW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "member_" <+> prettyPrec 11 y <+> prettyShowSet n
  prettySymbol _ _ _ = Nothing

instance (Ord a, HasSpec a, HasSpec (Set a)) => Semigroup (Term (Set a)) where
  (<>) = union_

instance (Ord a, HasSpec a, HasSpec (Set a)) => Monoid (Term (Set a)) where
  mempty = Lit mempty

-- Logic instance for SetW ------------------------------------------------

singletons :: [Set a] -> [Set a] -- Every Set in the filterd output has size 1 (if there are any)
singletons = filter ((1 ==) . Set.size)

instance Logic SetW where
  propagate f ctxt (ExplainSpec es s) = explainSpec es $ propagate f ctxt s
  propagate _ _ TrueSpec = TrueSpec
  propagate _ _ (ErrorSpec msgs) = ErrorSpec msgs
  propagate f ctx (SuspendedSpec v ps) = constrained $ \v' -> Let (App f (fromListCtx ctx v')) (v :-> ps)
  propagate SingletonW (Unary HOLE) (TypeSpec (SetSpec must es size) cant)
    | not $ 1 `conformsToSpec` size =
        ErrorSpec (pure "propagateSpecFun Singleton with spec that doesn't accept 1 size set")
    | [a] <- Set.toList must
    , a `conformsToSpec` es
    , Set.singleton a `notElem` cant =
        equalSpec a
    | null must = es <> notMemberSpec (Set.toList $ fold $ singletons cant)
    | otherwise = ErrorSpec (pure "propagateSpecFun Singleton with `must` of size > 1")
  propagate SingletonW (Unary HOLE) (MemberSpec es) =
    case Set.toList $ fold $ singletons (NE.toList es) of
      [] -> ErrorSpec $ pure "In propagateSpecFun Singleton, the sets of size 1, in MemberSpec is empty"
      (x : xs) -> MemberSpec (x :| xs)
  propagate UnionW ctx spec
    | (Value s :! Unary HOLE) <- ctx =
        propagate UnionW (HOLE :? Value s :> Nil) spec
    | (HOLE :? Value (s :: Set a) :> Nil) <- ctx
    , Evidence <- prerequisites @(Set a) =
        case spec of
          _ | null s -> spec
          TypeSpec (SetSpec must es size) cant
            | not $ all (`conformsToSpec` es) s ->
                ErrorSpec $
                  NE.fromList
                    [ "Elements in union argument does not conform to elem spec"
                    , "  spec: " ++ show es
                    , "  elems: " ++ show (filter (not . (`conformsToSpec` es)) (Set.toList s))
                    ]
            | not $ null cant -> ErrorSpec (pure "propagateSpecFun Union TypeSpec, not (null cant)")
            | TrueSpec <- size -> typeSpec $ SetSpec (Set.difference must s) es TrueSpec
            | TypeSpec (NumSpecInterval mlb Nothing) [] <- size
            , maybe True (<= sizeOf s) mlb ->
                typeSpec $ SetSpec (Set.difference must s) es TrueSpec
            | otherwise -> constrained $ \x ->
                exists (\eval -> pure $ Set.intersection (eval x) s) $ \overlap ->
                  exists (\eval -> pure $ Set.difference (eval x) s) $ \disjoint ->
                    [ Assert $ overlap `subset_` Lit s
                    , Assert $ disjoint `disjoint_` Lit s
                    , satisfies (sizeOf_ disjoint + Lit (sizeOf s)) size
                    , Assert $ x ==. (overlap <> disjoint) -- depends on Semigroup (Term (Set a))
                    , forAll disjoint $ \e -> e `satisfies` es
                    , Assert $ Lit (must Set.\\ s) `subset_` disjoint
                    ]
          -- We only do singleton MemberSpec to avoid really bad blowup
          MemberSpec (e :| [])
            | s `Set.isSubsetOf` e ->
                typeSpec
                  ( SetSpec
                      (Set.difference e s)
                      ( memberSpec
                          (Set.toList e)
                          (pure "propagateSpec (union_ s HOLE) on (MemberSpec [e]) where e is the empty set")
                      )
                      mempty
                  )
          -- TODO: improve this error message
          _ ->
            ErrorSpec
              ( NE.fromList
                  [ "propagateSpecFun (union_ s HOLE) with spec"
                  , "s = " ++ show s
                  , "spec = " ++ show spec
                  ]
              )
  propagate SubsetW ctx spec
    | (HOLE :? Value (s :: Set a) :> Nil) <- ctx
    , Evidence <- prerequisites @(Set a) = caseBoolSpec spec $ \case
        True ->
          case NE.nonEmpty (Set.toList s) of
            Nothing -> MemberSpec (pure Set.empty)
            Just slist -> typeSpec $ SetSpec mempty (MemberSpec slist) mempty
        False -> constrained $ \set ->
          exists (\eval -> headGE $ Set.difference (eval set) s) $ \e ->
            [ set `DependsOn` e
            , Assert $ not_ $ member_ e (Lit s)
            , Assert $ member_ e set
            ]
    | (Value (s :: Set a) :! Unary HOLE) <- ctx
    , Evidence <- prerequisites @(Set a) = caseBoolSpec spec $ \case
        True -> typeSpec $ SetSpec s TrueSpec mempty
        False -> constrained $ \set ->
          exists (\eval -> headGE $ Set.difference (eval set) s) $ \e ->
            [ set `DependsOn` e
            , Assert $ member_ e (Lit s)
            , Assert $ not_ $ member_ e set
            ]
  propagate MemberW ctx spec
    | (HOLE :? Value s :> Nil) <- ctx = caseBoolSpec spec $ \case
        True -> memberSpec (Set.toList s) (pure "propagateSpecFun on (Member x s) where s is Set.empty")
        False -> notMemberSpec s
    | (Value e :! Unary HOLE) <- ctx = caseBoolSpec spec $ \case
        True -> typeSpec $ SetSpec (Set.singleton e) mempty mempty
        False -> typeSpec $ SetSpec mempty (notEqualSpec e) mempty
  propagate DisjointW ctx spec
    | (HOLE :? Value (s :: Set a) :> Nil) <- ctx =
        propagate DisjointW (Value s :! Unary HOLE) spec
    | (Value (s :: Set a) :! Unary HOLE) <- ctx
    , Evidence <- prerequisites @(Set a) = caseBoolSpec spec $ \case
        True -> typeSpec $ SetSpec mempty (notMemberSpec s) mempty
        False -> constrained $ \set ->
          exists (\eval -> headGE (Set.intersection (eval set) s)) $ \e ->
            [ set `DependsOn` e
            , Assert $ member_ e (Lit s)
            , Assert $ member_ e set
            ]
  propagate FromListW (Unary HOLE) spec =
    case spec of
      MemberSpec (xs :| []) ->
        typeSpec $
          ListSpec
            Nothing
            (Set.toList xs)
            TrueSpec
            ( memberSpec
                (Set.toList xs)
                (pure "propagateSpec (fromList_ HOLE) on (MemberSpec xs) where the set 'xs' is empty")
            )
            NoFold
      TypeSpec (SetSpec must elemSpec sizeSpec) []
        | TrueSpec <- sizeSpec -> typeSpec $ ListSpec Nothing (Set.toList must) TrueSpec elemSpec NoFold
        | TypeSpec (NumSpecInterval (Just l) Nothing) cantSize <- sizeSpec
        , l <= sizeOf must
        , all (< sizeOf must) cantSize ->
            typeSpec $ ListSpec Nothing (Set.toList must) TrueSpec elemSpec NoFold
      _ ->
        -- Here we simply defer to basically generating the universe that we can
        -- draw from according to `spec` first and then fold that into the spec for the list.
        -- The tricky thing about this is that it may not play super nicely with other constraints
        -- on the list. For this reason it's important to try to find as many possible work-arounds
        -- in the above cases as possible.
        constrained $ \xs ->
          exists (\eval -> pure $ Set.fromList (eval xs)) $ \s ->
            [ s `satisfies` spec
            , xs `DependsOn` s
            , forAll xs $ \e -> e `member_` s
            , forAll s $ \e -> e `elem_` xs
            ]

  mapTypeSpec FromListW ts =
    constrained $ \x ->
      unsafeExists $ \x' -> Assert (x ==. fromList_ x') <> toPreds x' ts
  mapTypeSpec SingletonW ts =
    constrained $ \x ->
      unsafeExists $ \x' ->
        Assert (x ==. singleton_ x') <> toPreds x' ts

  rewriteRules SubsetW (Lit s :> _ :> Nil) Evidence | null s = Just $ Lit True
  rewriteRules SubsetW (x :> Lit s :> Nil) Evidence | null s = Just $ x ==. Lit Set.empty
  rewriteRules UnionW (x :> Lit s :> Nil) Evidence | null s = Just x
  rewriteRules UnionW (Lit s :> x :> Nil) Evidence | null s = Just x
  rewriteRules MemberW (t :> Lit s :> Nil) Evidence
    | null s = Just $ Lit False
    | [a] <- Set.toList s = Just $ t ==. Lit a
  rewriteRules DisjointW (Lit s :> _ :> Nil) Evidence | null s = Just $ Lit True
  rewriteRules DisjointW (_ :> Lit s :> Nil) Evidence | null s = Just $ Lit True
  rewriteRules _ _ _ = Nothing

-- Functions for writing constraints on sets ------------------------------

-- | Create a set with a single element
singleton_ :: (Ord a, HasSpec a) => Term a -> Term (Set a)
singleton_ = appTerm SingletonW

-- | Check if the first argument is a subset of the second
subset_ :: (Ord a, HasSpec a) => Term (Set a) -> Term (Set a) -> Term Bool
subset_ = appTerm SubsetW

-- | Check if an element is a member of the set
member_ :: (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ = appTerm MemberW

-- | Take the union of two sets
union_ :: (Ord a, HasSpec a) => Term (Set a) -> Term (Set a) -> Term (Set a)
union_ = appTerm UnionW

-- | Check if two sets have no elements in common
disjoint_ :: (Ord a, HasSpec a) => Term (Set a) -> Term (Set a) -> Term Bool
disjoint_ = appTerm DisjointW

-- | Convert a list to a set
fromList_ :: forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
fromList_ = appTerm FromListW

1	{-# LANGUAGE DataKinds #-}
2	{-# LANGUAGE FlexibleContexts #-}
3	{-# LANGUAGE FlexibleInstances #-}
4	{-# LANGUAGE GADTs #-}
5	{-# LANGUAGE LambdaCase #-}
6	{-# LANGUAGE MultiParamTypeClasses #-}
7	{-# LANGUAGE OverloadedStrings #-}
8	{-# LANGUAGE PatternSynonyms #-}
9	{-# LANGUAGE ScopedTypeVariables #-}
10	{-# LANGUAGE StandaloneDeriving #-}
11	{-# LANGUAGE TypeApplications #-}
12	{-# LANGUAGE TypeFamilies #-}
13	{-# LANGUAGE ViewPatterns #-}
14	{-# OPTIONS_GHC -Wno-orphans #-}
15
16	-- \| `HasSpec` instance for `Set`s and functions for writing
17	-- constraints about sets
18	module Constrained.Spec.Set (
19	SetSpec (..),
20	SetW (..),
21	singleton_,
22	subset_,
23	member_,
24	union_,
25	disjoint_,
26	fromList_,
27	) where
28
29	import Constrained.AbstractSyntax
30	import Constrained.Base
31	import Constrained.Conformance
32	import Constrained.Core
33	import Constrained.FunctionSymbol
34	import Constrained.GenT
35	import Constrained.Generation
36	import Constrained.List
37	import Constrained.NumOrd
38	import Constrained.PrettyUtils
39	import Constrained.Spec.List
40	import Constrained.SumList
41	import Constrained.Syntax
42	import Constrained.TheKnot
43	import Data.Foldable
44	import Data.Kind
45	import Data.List ((\\))
46	import qualified Data.List.NonEmpty as NE
47	import Data.Set (Set)
48	import qualified Data.Set as Set
49	import Prettyprinter hiding (cat)
50	import Test.QuickCheck (shrinkList, shuffle)
51
52	------------------------------------------------------------------------
53	-- HasSpec instance for Set
54	------------------------------------------------------------------------
55
56	-- \| `TypeSpec` for `Set`
57	data SetSpec a
58	= SetSpec
59	-- \| Required elements
60	(Set a)
61	-- \| Specification for elements
62	(Specification a)
63	-- \| Specification for size
64	(Specification Integer)
65
66	instance Ord a => Sized (Set.Set a) where
67	sizeOf = toInteger . Set.size	2✔
68	liftSizeSpec spec cant = typeSpec (SetSpec mempty TrueSpec (TypeSpec spec cant))	2✔
69	liftMemberSpec xs = case NE.nonEmpty xs of	2✔
70	Nothing -> ErrorSpec (pure "In liftMemberSpec for the (Sized Set) instance, xs is the empty list")	×
71	Just zs -> typeSpec (SetSpec mempty TrueSpec (MemberSpec zs))	2✔
72	sizeOfTypeSpec (SetSpec must _ sz) = sz <> geqSpec (sizeOf must)	×
73
74	instance (Ord a, HasSpec a) => Semigroup (SetSpec a) where	×
75	SetSpec must es size <> SetSpec must' es' size' =	2✔
76	SetSpec (must <> must') (es <> es') (size <> size')	2✔
77
78	instance (Ord a, HasSpec a) => Monoid (SetSpec a) where	×
79	mempty = SetSpec mempty mempty TrueSpec	2✔
80
81	instance Ord a => Forallable (Set a) a where
82	fromForAllSpec (e :: Specification a)	2✔
83	\| Evidence <- prerequisites @(Set a) = typeSpec $ SetSpec mempty e TrueSpec	2✔
84	forAllToList = Set.toList	2✔
85
86	prettySetSpec :: HasSpec a => SetSpec a -> Doc ann
87	prettySetSpec (SetSpec must elemS size) =	×
88	parens	×
89	( "SetSpec"	×
90	/> sep ["must=" <> viaShow (Set.toList must), "elem=" <> pretty elemS, "size=" <> pretty size]	×
91	)
92
93	instance HasSpec a => Show (SetSpec a) where	×
94	show x = show (prettySetSpec x)	×
95
96	guardSetSpec :: (HasSpec a, Ord a) => [String] -> SetSpec a -> Specification (Set a)
97	guardSetSpec es (SetSpec must elemS ((<> geqSpec 0) -> size))	2✔
98	\| Just u <- knownUpperBound size	2✔
99	, u < 0 =	1✔
100	ErrorSpec (("guardSetSpec: negative size " ++ show u) :\| es)	×
101	\| not (all (`conformsToSpec` elemS) must) =	2✔
102	ErrorSpec (("Some 'must' items do not conform to 'element' spec: " ++ show elemS) :\| es)	1✔
103	\| isErrorLike size = ErrorSpec ("guardSetSpec: error in size" :\| es)	1✔
104	\| isErrorLike (geqSpec (sizeOf must) <> size) =	2✔
105	ErrorSpec $	2✔
106	("Must set size " ++ show (sizeOf must) ++ ", is inconsistent with SetSpec size" ++ show size) :\| es	×
107	\| isErrorLike (maxSpec (cardinality elemS) <> size) =	2✔
108	ErrorSpec $	2✔
109	NE.fromList $	×
110	[ "Cardinality of SetSpec elemSpec (" ++ show elemS ++ ") = " ++ show (maxSpec (cardinality elemS))	×
111	, " This is inconsistent with SetSpec size (" ++ show size ++ ")"	×
112	]
113	++ es	×
114	\| otherwise = typeSpec (SetSpec must elemS size)	1✔
115
116	instance (Ord a, HasSpec a) => HasSpec (Set a) where	1✔
117	type TypeSpec (Set a) = SetSpec a
118
119	type Prerequisites (Set a) = HasSpec a
120
121	emptySpec = mempty	2✔
122
123	combineSpec s s' = guardSetSpec ["While combining 2 SetSpecs", " " ++ show s, " " ++ show s'] (s <> s')	1✔
124
125	conformsTo s (SetSpec must es size) =	2✔
126	and	2✔
127	[ sizeOf s `conformsToSpec` size	2✔
128	, must `Set.isSubsetOf` s	2✔
129	, all (`conformsToSpec` es) s	2✔
130	]
131
132	genFromTypeSpec (SetSpec must e _)	2✔
133	\| not $ allConformToSpec must e =	2✔
134	genErrorNE	2✔
135	( NE.fromList	×
136	[ "Failed to generate set"	×
137	, "Some element in the must set does not conform to the elem specification"	×
138	, "Unconforming elements from the must set:"	×
139	, unlines (map (\x -> " " ++ show x) (filter (not . (`conformsToSpec` e)) (Set.toList must)))	×
140	, "Element Specifcation"	×
141	, " " ++ show e	×
142	]
143	)
144	-- Special case when elemS is a MemberSpec.
145	-- Just union 'must' with enough elements of 'xs' to meet 'szSpec'
146	genFromTypeSpec (SetSpec must (ExplainSpec [] elemspec) szSpec) =
147	genFromTypeSpec (SetSpec must elemspec szSpec)	×
148	genFromTypeSpec (SetSpec must (ExplainSpec (e : es) elemspec) szSpec) =
149	explainNE (e :\| es) $ genFromTypeSpec (SetSpec must elemspec szSpec)	1✔
150	genFromTypeSpec (SetSpec must elemS@(MemberSpec xs) szSpec) = do	2✔
151	let szSpec' = szSpec <> geqSpec (sizeOf must) <> maxSpec (cardinality elemS)	2✔
152	choices <- pureGen $ shuffle (NE.toList xs \\ Set.toList must)	2✔
153	size <- fromInteger <$> genFromSpecT szSpec'	2✔
154	let additions = Set.fromList $ take (size - Set.size must) choices	2✔
155	pure (Set.union must additions)	2✔
156	genFromTypeSpec (SetSpec must elemS szSpec) = do	2✔
157	let szSpec' = szSpec <> geqSpec (sizeOf must) <> maxSpec (cardinality elemS)	2✔
158	chosenSize <-
159	explain "Choose a size for the Set to be generated" $	2✔
160	genFromSpecT szSpec'	2✔
161	let targetSize = chosenSize - sizeOf must	2✔
162	explainNE	2✔
163	( NE.fromList	×
164	[ "Choose size = " ++ show chosenSize	×
165	, "szSpec' = " ++ show szSpec'	×
166	, "Picking items not in must = " ++ show (Set.toList must)	×
167	, "that also meet the element test: "	×
168	, " " ++ show elemS	×
169	]
170	)
171	$ case theMostWeCanExpect of	2✔
172	-- 0 means TrueSpec or SuspendedSpec so we can't rule anything out
173	0 -> go 100 targetSize must	2✔
174	n -> case compare n targetSize of	2✔
175	LT -> fatalError "The number of things that meet the element test is too small."	1✔
176	GT -> go 100 targetSize must	2✔
177	EQ -> go 100 targetSize must	2✔
178	where
179	theMostWeCanExpect = maxFromSpec 0 (cardinality (simplifySpec elemS))	2✔
180	go _ n s \| n <= 0 = pure s	2✔
181	go tries n s = do	2✔
182	e <-
183	explainNE	2✔
184	( NE.fromList	×
185	[ "Generate set member at type " ++ showType @a	×
186	, " number of items starting with = " ++ show (Set.size must)	×
187	, " number of items left to pick = " ++ show n	×
188	, " number of items already picked = " ++ show (Set.size s)	×
189	, " the most items we can expect is " ++ show theMostWeCanExpect ++ " (a SuspendedSpec)"	×
190	]
191	)
192	$ withMode Strict	2✔
193	$ suchThatWithTryT tries (genFromSpecT elemS) (`Set.notMember` s)	2✔
194
195	go tries (n - 1) (Set.insert e s)	2✔
196
197	cardinalTypeSpec (SetSpec _ es _)	2✔
198	\| Just ub <- knownUpperBound (cardinality es) = leqSpec (2 ^ ub)	2✔
199	cardinalTypeSpec _ = TrueSpec	×
200
201	cardinalTrueSpec	2✔
202	\| Just ub <- knownUpperBound $ cardinalTrueSpec @a = leqSpec (2 ^ ub)	2✔
203	\| otherwise = TrueSpec	1✔
204
205	shrinkWithTypeSpec (SetSpec _ es _) as = map Set.fromList $ shrinkList (shrinkWithSpec es) (Set.toList as)	2✔
206
207	-- TODO: fixme
208	fixupWithTypeSpec _ _ = Nothing	2✔
209
210	toPreds s (SetSpec m es size) =	2✔
211	fold $	2✔
212	-- Don't include this if the must set is empty
213	[ Explain (pure (show m ++ " is a subset of the set.")) $ Assert $ subset_ (Lit m) s	1✔
214	\| not $ Set.null m	2✔
215	]
216	++ [ forAll s (\e -> satisfies e es)	2✔
217	, satisfies (sizeOf_ s) size	2✔
218	]
219
220	guardTypeSpec = guardSetSpec	2✔
221
222	------------------------------------------------------------------------
223	-- Functions that deal with sets
224	------------------------------------------------------------------------
225
226	-- \| Symbols for working on sets
227	data SetW (d :: [Type]) (r :: Type) where
228	SingletonW :: (HasSpec a, Ord a) => SetW '[a] (Set a)
229	UnionW :: (HasSpec a, Ord a) => SetW '[Set a, Set a] (Set a)
230	SubsetW :: (HasSpec a, Ord a, HasSpec a) => SetW '[Set a, Set a] Bool
231	MemberW :: (HasSpec a, Ord a) => SetW '[a, Set a] Bool
232	DisjointW :: (HasSpec a, Ord a) => SetW '[Set a, Set a] Bool
233	FromListW :: (HasSpec a, Ord a) => SetW '[[a]] (Set a)
234
235	deriving instance Eq (SetW dom rng)	×
236
237	instance Show (SetW ds r) where	×
238	show SingletonW = "singleton_"	2✔
239	show UnionW = "union_"	2✔
240	show SubsetW = "subset_"	2✔
241	show MemberW = "member_"	2✔
242	show DisjointW = "disjoint_"	2✔
243	show FromListW = "fromList_"	2✔
244
245	setSem :: SetW ds r -> FunTy ds r
246	setSem SingletonW = Set.singleton	2✔
247	setSem UnionW = Set.union	2✔
248	setSem SubsetW = Set.isSubsetOf	2✔
249	setSem MemberW = Set.member	2✔
250	setSem DisjointW = Set.disjoint	2✔
251	setSem FromListW = Set.fromList	2✔
252
253	instance Semantics SetW where
254	semantics = setSem	2✔
255
256	instance Syntax SetW where	×
257	prettySymbol SubsetW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "subset_" <+> prettyShowSet n <+> prettyPrec 11 y	×
258	prettySymbol SubsetW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "subset_" <+> prettyPrec 11 y <+> prettyShowSet n	×
259	prettySymbol DisjointW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "disjoint_" <+> prettyShowSet n <+> prettyPrec 11 y	×
260	prettySymbol DisjointW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "disjoint_" <+> prettyPrec 11 y <+> prettyShowSet n	×
261	prettySymbol UnionW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "union_" <+> prettyShowSet n <+> prettyPrec 11 y	×
262	prettySymbol UnionW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "union_" <+> prettyPrec 11 y <+> prettyShowSet n	×
263	prettySymbol MemberW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "member_" <+> prettyPrec 11 y <+> prettyShowSet n	×
264	prettySymbol _ _ _ = Nothing	×
265
266	instance (Ord a, HasSpec a, HasSpec (Set a)) => Semigroup (Term (Set a)) where	×
267	(<>) = union_	2✔
268
269	instance (Ord a, HasSpec a, HasSpec (Set a)) => Monoid (Term (Set a)) where	×
270	mempty = Lit mempty	2✔
271
272	-- Logic instance for SetW ------------------------------------------------
273
274	singletons :: [Set a] -> [Set a] -- Every Set in the filterd output has size 1 (if there are any)
275	singletons = filter ((1 ==) . Set.size)	2✔
276
277	instance Logic SetW where	1✔
278	propagate f ctxt (ExplainSpec es s) = explainSpec es $ propagate f ctxt s	2✔
279	propagate _ _ TrueSpec = TrueSpec	2✔
280	propagate _ _ (ErrorSpec msgs) = ErrorSpec msgs	1✔
281	propagate f ctx (SuspendedSpec v ps) = constrained $ \v' -> Let (App f (fromListCtx ctx v')) (v :-> ps)	2✔
282	propagate SingletonW (Unary HOLE) (TypeSpec (SetSpec must es size) cant)
283	\| not $ 1 `conformsToSpec` size =	2✔
284	ErrorSpec (pure "propagateSpecFun Singleton with spec that doesn't accept 1 size set")	1✔
285	\| [a] <- Set.toList must	2✔
286	, a `conformsToSpec` es	2✔
287	, Set.singleton a `notElem` cant =	1✔
288	equalSpec a	2✔
289	\| null must = es <> notMemberSpec (Set.toList $ fold $ singletons cant)	2✔
290	\| otherwise = ErrorSpec (pure "propagateSpecFun Singleton with `must` of size > 1")	1✔
291	propagate SingletonW (Unary HOLE) (MemberSpec es) =
292	case Set.toList $ fold $ singletons (NE.toList es) of	2✔
293	[] -> ErrorSpec $ pure "In propagateSpecFun Singleton, the sets of size 1, in MemberSpec is empty"	1✔
294	(x : xs) -> MemberSpec (x :\| xs)	2✔
295	propagate UnionW ctx spec
296	\| (Value s :! Unary HOLE) <- ctx =	2✔
297	propagate UnionW (HOLE :? Value s :> Nil) spec	2✔
298	\| (HOLE :? Value (s :: Set a) :> Nil) <- ctx	2✔
299	, Evidence <- prerequisites @(Set a) =	2✔
300	case spec of	2✔
301	_ \| null s -> spec	2✔
302	TypeSpec (SetSpec must es size) cant
303	\| not $ all (`conformsToSpec` es) s ->	2✔
304	ErrorSpec $	2✔
305	NE.fromList	×
306	[ "Elements in union argument does not conform to elem spec"	×
307	, " spec: " ++ show es	×
308	, " elems: " ++ show (filter (not . (`conformsToSpec` es)) (Set.toList s))	×
309	]
310	\| not $ null cant -> ErrorSpec (pure "propagateSpecFun Union TypeSpec, not (null cant)")	1✔
311	\| TrueSpec <- size -> typeSpec $ SetSpec (Set.difference must s) es TrueSpec	2✔
312	\| TypeSpec (NumSpecInterval mlb Nothing) [] <- size	2✔
313	, maybe True (<= sizeOf s) mlb ->	1✔
314	typeSpec $ SetSpec (Set.difference must s) es TrueSpec	2✔
315	\| otherwise -> constrained $ \x ->	1✔
316	exists (\eval -> pure $ Set.intersection (eval x) s) $ \overlap ->	2✔
317	exists (\eval -> pure $ Set.difference (eval x) s) $ \disjoint ->	2✔
318	[ Assert $ overlap `subset_` Lit s	2✔
319	, Assert $ disjoint `disjoint_` Lit s	2✔
320	, satisfies (sizeOf_ disjoint + Lit (sizeOf s)) size	2✔
321	, Assert $ x ==. (overlap <> disjoint) -- depends on Semigroup (Term (Set a))	2✔
322	, forAll disjoint $ \e -> e `satisfies` es	2✔
323	, Assert $ Lit (must Set.\\ s) `subset_` disjoint	2✔
324	]
325	-- We only do singleton MemberSpec to avoid really bad blowup
326	MemberSpec (e :\| [])
327	\| s `Set.isSubsetOf` e ->	1✔
UNCOV 328	typeSpec	×
UNCOV 329	( SetSpec	×
UNCOV 330	(Set.difference e s)	×
UNCOV 331	( memberSpec	×
UNCOV 332	(Set.toList e)	×
333	(pure "propagateSpec (union_ s HOLE) on (MemberSpec [e]) where e is the empty set")	×
334	)
UNCOV 335	mempty	×
336	)
337	-- TODO: improve this error message
338	_ ->
339	ErrorSpec	2✔
340	( NE.fromList	×
341	[ "propagateSpecFun (union_ s HOLE) with spec"	×
342	, "s = " ++ show s	×
343	, "spec = " ++ show spec	×
344	]
345	)
346	propagate SubsetW ctx spec
347	\| (HOLE :? Value (s :: Set a) :> Nil) <- ctx	2✔
348	, Evidence <- prerequisites @(Set a) = caseBoolSpec spec $ \case	2✔
349	True ->
350	case NE.nonEmpty (Set.toList s) of	2✔
351	Nothing -> MemberSpec (pure Set.empty)	2✔
352	Just slist -> typeSpec $ SetSpec mempty (MemberSpec slist) mempty	2✔
353	False -> constrained $ \set ->	2✔
354	exists (\eval -> headGE $ Set.difference (eval set) s) $ \e ->	2✔
355	[ set `DependsOn` e	2✔
356	, Assert $ not_ $ member_ e (Lit s)	2✔
357	, Assert $ member_ e set	2✔
358	]
359	\| (Value (s :: Set a) :! Unary HOLE) <- ctx	2✔
360	, Evidence <- prerequisites @(Set a) = caseBoolSpec spec $ \case	2✔
361	True -> typeSpec $ SetSpec s TrueSpec mempty	2✔
362	False -> constrained $ \set ->	2✔
363	exists (\eval -> headGE $ Set.difference (eval set) s) $ \e ->	1✔
364	[ set `DependsOn` e	2✔
365	, Assert $ member_ e (Lit s)	2✔
366	, Assert $ not_ $ member_ e set	2✔
367	]
368	propagate MemberW ctx spec
369	\| (HOLE :? Value s :> Nil) <- ctx = caseBoolSpec spec $ \case	2✔
370	True -> memberSpec (Set.toList s) (pure "propagateSpecFun on (Member x s) where s is Set.empty")	1✔
371	False -> notMemberSpec s	2✔
372	\| (Value e :! Unary HOLE) <- ctx = caseBoolSpec spec $ \case	2✔
373	True -> typeSpec $ SetSpec (Set.singleton e) mempty mempty	2✔
374	False -> typeSpec $ SetSpec mempty (notEqualSpec e) mempty	2✔
375	propagate DisjointW ctx spec
376	\| (HOLE :? Value (s :: Set a) :> Nil) <- ctx =	2✔
377	propagate DisjointW (Value s :! Unary HOLE) spec	2✔
378	\| (Value (s :: Set a) :! Unary HOLE) <- ctx	2✔
379	, Evidence <- prerequisites @(Set a) = caseBoolSpec spec $ \case	2✔
380	True -> typeSpec $ SetSpec mempty (notMemberSpec s) mempty	2✔
381	False -> constrained $ \set ->	2✔
382	exists (\eval -> headGE (Set.intersection (eval set) s)) $ \e ->	1✔
383	[ set `DependsOn` e	2✔
384	, Assert $ member_ e (Lit s)	2✔
385	, Assert $ member_ e set	2✔
386	]
387	propagate FromListW (Unary HOLE) spec =
388	case spec of	2✔
389	MemberSpec (xs :\| []) ->
390	typeSpec $	2✔
391	ListSpec	2✔
392	Nothing	2✔
393	(Set.toList xs)	2✔
394	TrueSpec	2✔
395	( memberSpec	2✔
396	(Set.toList xs)	2✔
397	(pure "propagateSpec (fromList_ HOLE) on (MemberSpec xs) where the set 'xs' is empty")	×
398	)
399	NoFold	2✔
400	TypeSpec (SetSpec must elemSpec sizeSpec) []
401	\| TrueSpec <- sizeSpec -> typeSpec $ ListSpec Nothing (Set.toList must) TrueSpec elemSpec NoFold	2✔
402	\| TypeSpec (NumSpecInterval (Just l) Nothing) cantSize <- sizeSpec	2✔
403	, l <= sizeOf must	2✔
404	, all (< sizeOf must) cantSize ->	1✔
405	typeSpec $ ListSpec Nothing (Set.toList must) TrueSpec elemSpec NoFold	2✔
406	_ ->
407	-- Here we simply defer to basically generating the universe that we can
408	-- draw from according to `spec` first and then fold that into the spec for the list.
409	-- The tricky thing about this is that it may not play super nicely with other constraints
410	-- on the list. For this reason it's important to try to find as many possible work-arounds
411	-- in the above cases as possible.
412	constrained $ \xs ->	2✔
413	exists (\eval -> pure $ Set.fromList (eval xs)) $ \s ->	1✔
414	[ s `satisfies` spec	2✔
415	, xs `DependsOn` s	2✔
416	, forAll xs $ \e -> e `member_` s	2✔
417	, forAll s $ \e -> e `elem_` xs	2✔
418	]
419
420	mapTypeSpec FromListW ts =	×
421	constrained $ \x ->	×
422	unsafeExists $ \x' -> Assert (x ==. fromList_ x') <> toPreds x' ts	×
423	mapTypeSpec SingletonW ts =
424	constrained $ \x ->	×
425	unsafeExists $ \x' ->	×
426	Assert (x ==. singleton_ x') <> toPreds x' ts	×
427
428	rewriteRules SubsetW (Lit s :> _ :> Nil) Evidence \| null s = Just $ Lit True	2✔
429	rewriteRules SubsetW (x :> Lit s :> Nil) Evidence \| null s = Just $ x ==. Lit Set.empty	2✔
430	rewriteRules UnionW (x :> Lit s :> Nil) Evidence \| null s = Just x	2✔
431	rewriteRules UnionW (Lit s :> x :> Nil) Evidence \| null s = Just x	2✔
432	rewriteRules MemberW (t :> Lit s :> Nil) Evidence
433	\| null s = Just $ Lit False	2✔
434	\| [a] <- Set.toList s = Just $ t ==. Lit a	2✔
435	rewriteRules DisjointW (Lit s :> _ :> Nil) Evidence \| null s = Just $ Lit True	1✔
436	rewriteRules DisjointW (_ :> Lit s :> Nil) Evidence \| null s = Just $ Lit True	1✔
437	rewriteRules _ _ _ = Nothing	2✔
438
439	-- Functions for writing constraints on sets ------------------------------
440
441	-- \| Create a set with a single element
442	singleton_ :: (Ord a, HasSpec a) => Term a -> Term (Set a)
443	singleton_ = appTerm SingletonW	2✔
444
445	-- \| Check if the first argument is a subset of the second
446	subset_ :: (Ord a, HasSpec a) => Term (Set a) -> Term (Set a) -> Term Bool
447	subset_ = appTerm SubsetW	2✔
448
449	-- \| Check if an element is a member of the set
450	member_ :: (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
451	member_ = appTerm MemberW	2✔
452
453	-- \| Take the union of two sets
454	union_ :: (Ord a, HasSpec a) => Term (Set a) -> Term (Set a) -> Term (Set a)
455	union_ = appTerm UnionW	2✔
456
457	-- \| Check if two sets have no elements in common
458	disjoint_ :: (Ord a, HasSpec a) => Term (Set a) -> Term (Set a) -> Term Bool
459	disjoint_ = appTerm DisjointW	2✔
460
461	-- \| Convert a list to a set
462	fromList_ :: forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
463	fromList_ = appTerm FromListW	2✔

input-output-hk / constrained-generators / 414

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous