input-output-hk / constrained-generators / 457

Committed 10 Dec 2025 01:30PM UTC coverage: 76.948% (-0.5%) from 77.401%

Build # 457

Build Type

push

github

Committed by

web-flow

Commit Message

Merge 7c2c067b5 into 966f65f3c

Run Details

15 of 15 new or added lines in 2 files covered. (100.0%)

24 existing lines in 5 files now uncovered.

3969 of 5158 relevant lines covered (76.95%)

1.45 hits per line

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

72.69

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

input-output-hk / constrained-generators / 457

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