input-output-hk / constrained-generators / 315

Committed 17 Oct 2025 06:03AM UTC coverage: 73.983% (-0.7%) from 74.661%

Build # 315

Build Type

push

github

Committed by

web-flow

Commit Message

Coveralls and stack support (#44)

* Implement coveralls support

Run Details

12 of 20 new or added lines in 2 files covered. (60.0%)

88 existing lines in 5 files now uncovered.

3711 of 5016 relevant lines covered (73.98%)

1.39 hits per line

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

72.01

/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 _)
    | any (not . (`conformsToSpec` e)) must =
        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)

  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	\| any (not . (`conformsToSpec` e)) must =	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✔
UNCOV 175	LT -> fatalError "The number of things that meet the element test is too small."	×
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)	×
206
207	toPreds s (SetSpec m es size) =	2✔
208	fold $	2✔
209	-- Don't include this if the must set is empty
210	[ Explain (pure (show m ++ " is a subset of the set.")) $ Assert $ subset_ (Lit m) s	1✔
211	\| not $ Set.null m	2✔
212	]
213	++ [ forAll s (\e -> satisfies e es)	2✔
214	, satisfies (sizeOf_ s) size	2✔
215	]
216
217	guardTypeSpec = guardSetSpec	2✔
218
219	------------------------------------------------------------------------
220	-- Functions that deal with sets
221	------------------------------------------------------------------------
222
223	-- \| Symbols for working on sets
224	data SetW (d :: [Type]) (r :: Type) where
225	SingletonW :: (HasSpec a, Ord a) => SetW '[a] (Set a)
226	UnionW :: (HasSpec a, Ord a) => SetW '[Set a, Set a] (Set a)
227	SubsetW :: (HasSpec a, Ord a, HasSpec a) => SetW '[Set a, Set a] Bool
228	MemberW :: (HasSpec a, Ord a) => SetW '[a, Set a] Bool
229	DisjointW :: (HasSpec a, Ord a) => SetW '[Set a, Set a] Bool
230	FromListW :: (HasSpec a, Ord a) => SetW '[[a]] (Set a)
231
232	deriving instance Eq (SetW dom rng)	×
233
234	instance Show (SetW ds r) where	×
235	show SingletonW = "singleton_"	2✔
236	show UnionW = "union_"	2✔
237	show SubsetW = "subset_"	2✔
238	show MemberW = "member_"	2✔
239	show DisjointW = "disjoint_"	2✔
240	show FromListW = "fromList_"	2✔
241
242	setSem :: SetW ds r -> FunTy ds r
243	setSem SingletonW = Set.singleton	2✔
244	setSem UnionW = Set.union	2✔
245	setSem SubsetW = Set.isSubsetOf	2✔
246	setSem MemberW = Set.member	2✔
247	setSem DisjointW = Set.disjoint	2✔
248	setSem FromListW = Set.fromList	2✔
249
250	instance Semantics SetW where
251	semantics = setSem	2✔
252
253	instance Syntax SetW where	×
254	prettySymbol SubsetW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "subset_" <+> prettyShowSet n <+> prettyPrec 11 y	×
255	prettySymbol SubsetW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "subset_" <+> prettyPrec 11 y <+> prettyShowSet n	×
256	prettySymbol DisjointW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "disjoint_" <+> prettyShowSet n <+> prettyPrec 11 y	×
257	prettySymbol DisjointW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "disjoint_" <+> prettyPrec 11 y <+> prettyShowSet n	×
258	prettySymbol UnionW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "union_" <+> prettyShowSet n <+> prettyPrec 11 y	×
259	prettySymbol UnionW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "union_" <+> prettyPrec 11 y <+> prettyShowSet n	×
260	prettySymbol MemberW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "member_" <+> prettyPrec 11 y <+> prettyShowSet n	×
261	prettySymbol _ _ _ = Nothing	×
262
263	instance (Ord a, HasSpec a, HasSpec (Set a)) => Semigroup (Term (Set a)) where	×
264	(<>) = union_	2✔
265
266	instance (Ord a, HasSpec a, HasSpec (Set a)) => Monoid (Term (Set a)) where	×
267	mempty = Lit mempty	2✔
268
269	-- Logic instance for SetW ------------------------------------------------
270
271	singletons :: [Set a] -> [Set a] -- Every Set in the filterd output has size 1 (if there are any)
272	singletons = filter ((1 ==) . Set.size)	2✔
273
274	instance Logic SetW where	1✔
275	propagate f ctxt (ExplainSpec es s) = explainSpec es $ propagate f ctxt s	2✔
276	propagate _ _ TrueSpec = TrueSpec	2✔
277	propagate _ _ (ErrorSpec msgs) = ErrorSpec msgs	1✔
278	propagate f ctx (SuspendedSpec v ps) = constrained $ \v' -> Let (App f (fromListCtx ctx v')) (v :-> ps)	2✔
279	propagate SingletonW (Unary HOLE) (TypeSpec (SetSpec must es size) cant)
280	\| not $ 1 `conformsToSpec` size =	2✔
281	ErrorSpec (pure "propagateSpecFun Singleton with spec that doesn't accept 1 size set")	1✔
282	\| [a] <- Set.toList must	2✔
283	, a `conformsToSpec` es	2✔
284	, Set.singleton a `notElem` cant =	1✔
285	equalSpec a	2✔
286	\| null must = es <> notMemberSpec (Set.toList $ fold $ singletons cant)	2✔
287	\| otherwise = ErrorSpec (pure "propagateSpecFun Singleton with `must` of size > 1")	1✔
288	propagate SingletonW (Unary HOLE) (MemberSpec es) =
289	case Set.toList $ fold $ singletons (NE.toList es) of	2✔
290	[] -> ErrorSpec $ pure "In propagateSpecFun Singleton, the sets of size 1, in MemberSpec is empty"	1✔
291	(x : xs) -> MemberSpec (x :\| xs)	2✔
292	propagate UnionW ctx spec
293	\| (Value s :! Unary HOLE) <- ctx =	2✔
294	propagate UnionW (HOLE :? Value s :> Nil) spec	2✔
295	\| (HOLE :? Value (s :: Set a) :> Nil) <- ctx	2✔
296	, Evidence <- prerequisites @(Set a) =	2✔
297	case spec of	2✔
298	_ \| null s -> spec	2✔
299	TypeSpec (SetSpec must es size) cant
300	\| not $ all (`conformsToSpec` es) s ->	2✔
301	ErrorSpec $	2✔
302	NE.fromList	×
303	[ "Elements in union argument does not conform to elem spec"	×
304	, " spec: " ++ show es	×
305	, " elems: " ++ show (filter (not . (`conformsToSpec` es)) (Set.toList s))	×
306	]
307	\| not $ null cant -> ErrorSpec (pure "propagateSpecFun Union TypeSpec, not (null cant)")	1✔
308	\| TrueSpec <- size -> typeSpec $ SetSpec (Set.difference must s) es TrueSpec	2✔
309	\| TypeSpec (NumSpecInterval mlb Nothing) [] <- size	2✔
310	, maybe True (<= sizeOf s) mlb ->	1✔
311	typeSpec $ SetSpec (Set.difference must s) es TrueSpec	1✔
312	\| otherwise -> constrained $ \x ->	1✔
313	exists (\eval -> pure $ Set.intersection (eval x) s) $ \overlap ->	2✔
314	exists (\eval -> pure $ Set.difference (eval x) s) $ \disjoint ->	2✔
315	[ Assert $ overlap `subset_` Lit s	2✔
316	, Assert $ disjoint `disjoint_` Lit s	2✔
317	, satisfies (sizeOf_ disjoint + Lit (sizeOf s)) size	2✔
318	, Assert $ x ==. (overlap <> disjoint) -- depends on Semigroup (Term (Set a))	2✔
319	, forAll disjoint $ \e -> e `satisfies` es	2✔
320	, Assert $ Lit (must Set.\\ s) `subset_` disjoint	2✔
321	]
322	-- We only do singleton MemberSpec to avoid really bad blowup
323	MemberSpec (e :\| [])
324	\| s `Set.isSubsetOf` e ->	1✔
UNCOV 325	typeSpec	×
UNCOV 326	( SetSpec	×
UNCOV 327	(Set.difference e s)	×
UNCOV 328	( memberSpec	×
UNCOV 329	(Set.toList e)	×
330	(pure "propagateSpec (union_ s HOLE) on (MemberSpec [e]) where e is the empty set")	×
331	)
UNCOV 332	mempty	×
333	)
334	-- TODO: improve this error message
335	_ ->
336	ErrorSpec	2✔
337	( NE.fromList	×
338	[ "propagateSpecFun (union_ s HOLE) with spec"	×
339	, "s = " ++ show s	×
340	, "spec = " ++ show spec	×
341	]
342	)
343	propagate SubsetW ctx spec
344	\| (HOLE :? Value (s :: Set a) :> Nil) <- ctx	2✔
345	, Evidence <- prerequisites @(Set a) = caseBoolSpec spec $ \case	2✔
346	True ->
347	case NE.nonEmpty (Set.toList s) of	2✔
348	Nothing -> MemberSpec (pure Set.empty)	×
349	Just slist -> typeSpec $ SetSpec mempty (MemberSpec slist) mempty	2✔
350	False -> constrained $ \set ->	2✔
351	exists (\eval -> headGE $ Set.difference (eval set) s) $ \e ->	2✔
352	[ set `DependsOn` e	2✔
353	, Assert $ not_ $ member_ e (Lit s)	2✔
354	, Assert $ member_ e set	2✔
355	]
356	\| (Value (s :: Set a) :! Unary HOLE) <- ctx	2✔
357	, Evidence <- prerequisites @(Set a) = caseBoolSpec spec $ \case	2✔
358	True -> typeSpec $ SetSpec s TrueSpec mempty	2✔
359	False -> constrained $ \set ->	2✔
360	exists (\eval -> headGE $ Set.difference (eval set) s) $ \e ->	1✔
361	[ set `DependsOn` e	2✔
362	, Assert $ member_ e (Lit s)	2✔
363	, Assert $ not_ $ member_ e set	2✔
364	]
365	propagate MemberW ctx spec
366	\| (HOLE :? Value s :> Nil) <- ctx = caseBoolSpec spec $ \case	2✔
367	True -> memberSpec (Set.toList s) (pure "propagateSpecFun on (Member x s) where s is Set.empty")	1✔
368	False -> notMemberSpec s	2✔
369	\| (Value e :! Unary HOLE) <- ctx = caseBoolSpec spec $ \case	2✔
370	True -> typeSpec $ SetSpec (Set.singleton e) mempty mempty	2✔
371	False -> typeSpec $ SetSpec mempty (notEqualSpec e) mempty	2✔
372	propagate DisjointW ctx spec
373	\| (HOLE :? Value (s :: Set a) :> Nil) <- ctx =	2✔
374	propagate DisjointW (Value s :! Unary HOLE) spec	2✔
375	\| (Value (s :: Set a) :! Unary HOLE) <- ctx	2✔
376	, Evidence <- prerequisites @(Set a) = caseBoolSpec spec $ \case	2✔
377	True -> typeSpec $ SetSpec mempty (notMemberSpec s) mempty	2✔
378	False -> constrained $ \set ->	2✔
379	exists (\eval -> headGE (Set.intersection (eval set) s)) $ \e ->	1✔
380	[ set `DependsOn` e	2✔
381	, Assert $ member_ e (Lit s)	2✔
382	, Assert $ member_ e set	2✔
383	]
384	propagate FromListW (Unary HOLE) spec =
385	case spec of	2✔
386	MemberSpec (xs :\| []) ->
387	typeSpec $	2✔
388	ListSpec	2✔
389	Nothing	2✔
390	(Set.toList xs)	2✔
391	TrueSpec	2✔
392	( memberSpec	2✔
393	(Set.toList xs)	2✔
394	(pure "propagateSpec (fromList_ HOLE) on (MemberSpec xs) where the set 'xs' is empty")	×
395	)
396	NoFold	2✔
397	TypeSpec (SetSpec must elemSpec sizeSpec) []
398	\| TrueSpec <- sizeSpec -> typeSpec $ ListSpec Nothing (Set.toList must) TrueSpec elemSpec NoFold	2✔
399	\| TypeSpec (NumSpecInterval (Just l) Nothing) cantSize <- sizeSpec	2✔
400	, l <= sizeOf must	2✔
401	, all (< sizeOf must) cantSize ->	2✔
402	typeSpec $ ListSpec Nothing (Set.toList must) TrueSpec elemSpec NoFold	2✔
403	_ ->
404	-- Here we simply defer to basically generating the universe that we can
405	-- draw from according to `spec` first and then fold that into the spec for the list.
406	-- The tricky thing about this is that it may not play super nicely with other constraints
407	-- on the list. For this reason it's important to try to find as many possible work-arounds
408	-- in the above cases as possible.
409	constrained $ \xs ->	2✔
410	exists (\eval -> pure $ Set.fromList (eval xs)) $ \s ->	1✔
411	[ s `satisfies` spec	2✔
412	, xs `DependsOn` s	2✔
413	, forAll xs $ \e -> e `member_` s	2✔
414	, forAll s $ \e -> e `elem_` xs	2✔
415	]
416
417	mapTypeSpec FromListW ts =	×
418	constrained $ \x ->	×
419	unsafeExists $ \x' -> Assert (x ==. fromList_ x') <> toPreds x' ts	×
420	mapTypeSpec SingletonW ts =
421	constrained $ \x ->	×
422	unsafeExists $ \x' ->	×
423	Assert (x ==. singleton_ x') <> toPreds x' ts	×
424
425	rewriteRules SubsetW (Lit s :> _ :> Nil) Evidence \| null s = Just $ Lit True	2✔
426	rewriteRules SubsetW (x :> Lit s :> Nil) Evidence \| null s = Just $ x ==. Lit Set.empty	2✔
427	rewriteRules UnionW (x :> Lit s :> Nil) Evidence \| null s = Just x	2✔
428	rewriteRules UnionW (Lit s :> x :> Nil) Evidence \| null s = Just x	2✔
429	rewriteRules MemberW (t :> Lit s :> Nil) Evidence
430	\| null s = Just $ Lit False	2✔
431	\| [a] <- Set.toList s = Just $ t ==. Lit a	2✔
432	rewriteRules DisjointW (Lit s :> _ :> Nil) Evidence \| null s = Just $ Lit True	2✔
433	rewriteRules DisjointW (_ :> Lit s :> Nil) Evidence \| null s = Just $ Lit True	1✔
434	rewriteRules _ _ _ = Nothing	2✔
435
436	-- Functions for writing constraints on sets ------------------------------
437
438	-- \| Create a set with a single element
439	singleton_ :: (Ord a, HasSpec a) => Term a -> Term (Set a)
440	singleton_ = appTerm SingletonW	2✔
441
442	-- \| Check if the first argument is a subset of the second
443	subset_ :: (Ord a, HasSpec a) => Term (Set a) -> Term (Set a) -> Term Bool
444	subset_ = appTerm SubsetW	2✔
445
446	-- \| Check if an element is a member of the set
447	member_ :: (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
448	member_ = appTerm MemberW	2✔
449
450	-- \| Take the union of two sets
451	union_ :: (Ord a, HasSpec a) => Term (Set a) -> Term (Set a) -> Term (Set a)
452	union_ = appTerm UnionW	2✔
453
454	-- \| Check if two sets have no elements in common
455	disjoint_ :: (Ord a, HasSpec a) => Term (Set a) -> Term (Set a) -> Term Bool
456	disjoint_ = appTerm DisjointW	2✔
457
458	-- \| Convert a list to a set
459	fromList_ :: forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
460	fromList_ = appTerm FromListW	2✔

input-output-hk / constrained-generators / 315

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