{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans -Wno-name-shadowing #-}

-- The pattern completeness checker is much weaker before ghc-9.0. Rather than introducing redundant
-- cases and turning off the overlap check in newer ghc versions we disable the check for old
-- versions.
#if __GLASGOW_HASKELL__ < 900
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
#endif

module Constrained.Spec.Set where

import Constrained.Base (
  Binder (..),
  Forallable (..),
  HOLE (..),
  HasSpec (..),
  Logic (..),
  Pred (..),
  Semantics (..),
  Specification (..),
  Syntax (..),
  Term (..),
  appTerm,
  constrained,
  equalSpec,
  explainSpec,
  fromListCtx,
  isErrorLike,
  memberSpecList,
  notEqualSpec,
  notMemberSpec,
  parensIf,
  prettyPrec,
  short,
  showType,
  typeSpec,
  (/>),
  pattern Unary,
 )
import Constrained.Conformance (
  conformsToSpec,
  satisfies,
 )
import Constrained.Core
import Constrained.GenT
import Constrained.List
import Constrained.NumSpec
import Constrained.SumList (knownUpperBound, maxFromSpec)
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 (Arbitrary (..), shrinkList, shuffle)

-- ===============================================================================
-- Sets and their Specifications

data SetSpec a = SetSpec (Set a) (Specification a) (Specification Integer)

instance Ord a => Sized (Set.Set a) where
  sizeOf :: Set a -> Integer
sizeOf = forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> Int
Set.size
  liftSizeSpec :: HasSpec (Set a) => SizeSpec -> [Integer] -> Specification (Set a)
liftSizeSpec SizeSpec
spec [Integer]
cant = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec forall a. Monoid a => a
mempty forall a. Specification a
TrueSpec (forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec SizeSpec
spec [Integer]
cant))
  liftMemberSpec :: HasSpec (Set a) => [Integer] -> Specification (Set a)
liftMemberSpec [Integer]
xs = case forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty [Integer]
xs of
    Maybe (NonEmpty Integer)
Nothing -> forall a. NonEmpty String -> Specification a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"In liftMemberSpec for the (Sized Set) instance, xs is the empty list"))
    Just NonEmpty Integer
zs -> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec forall a. Monoid a => a
mempty forall a. Specification a
TrueSpec (forall a. NonEmpty a -> Specification a
MemberSpec NonEmpty Integer
zs))
  sizeOfTypeSpec :: HasSpec (Set a) => TypeSpec (Set a) -> Specification Integer
sizeOfTypeSpec (SetSpec Set a
must Specification a
_ Specification Integer
sz) = Specification Integer
sz forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
geqSpec (forall t. Sized t => t -> Integer
sizeOf Set a
must)

instance (Ord a, HasSpec a) => Semigroup (SetSpec a) where
  SetSpec Set a
must Specification a
es Specification Integer
size <> :: SetSpec a -> SetSpec a -> SetSpec a
<> SetSpec Set a
must' Specification a
es' Specification Integer
size' =
    forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec (Set a
must forall a. Semigroup a => a -> a -> a
<> Set a
must') (Specification a
es forall a. Semigroup a => a -> a -> a
<> Specification a
es') (Specification Integer
size forall a. Semigroup a => a -> a -> a
<> Specification Integer
size')

instance (Ord a, HasSpec a) => Monoid (SetSpec a) where
  mempty :: SetSpec a
mempty = forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Specification a
TrueSpec

instance Ord a => Forallable (Set a) a where
  fromForAllSpec :: (HasSpec (Set a), HasSpec a) =>
Specification a -> Specification (Set a)
fromForAllSpec (Specification a
e :: Specification a)
    | Evidence (Prerequisites (Set a))
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @(Set a) = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec forall a. Monoid a => a
mempty Specification a
e forall a. Specification a
TrueSpec
  forAllToList :: Set a -> [a]
forAllToList = forall a. Set a -> [a]
Set.toList

prettySetSpec :: HasSpec a => SetSpec a -> Doc ann
prettySetSpec :: forall a ann. HasSpec a => SetSpec a -> Doc ann
prettySetSpec (SetSpec Set a
must Specification a
elemS Specification Integer
size) =
  forall ann. Doc ann -> Doc ann
parens
    ( Doc ann
"SetSpec"
        forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [Doc ann] -> Doc ann
sep [Doc ann
"must=" forall a. Semigroup a => a -> a -> a
<> forall a x. (Show a, Typeable a) => [a] -> Doc x
short (forall a. Set a -> [a]
Set.toList Set a
must), Doc ann
"elem=" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Specification a
elemS, Doc ann
"size=" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Specification Integer
size]
    )

instance HasSpec a => Show (SetSpec a) where
  show :: SetSpec a -> String
show SetSpec a
x = forall a. Show a => a -> String
show (forall a ann. HasSpec a => SetSpec a -> Doc ann
prettySetSpec SetSpec a
x)

instance (Ord a, Arbitrary (Specification a), Arbitrary a) => Arbitrary (SetSpec a) where
  arbitrary :: Gen (SetSpec a)
arbitrary = forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
  shrink :: SetSpec a -> [SetSpec a]
shrink (SetSpec Set a
a Specification a
b Specification Integer
c) = [forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec Set a
a' Specification a
b' Specification Integer
c' | (Set a
a', Specification a
b', Specification Integer
c') <- forall a. Arbitrary a => a -> [a]
shrink (Set a
a, Specification a
b, Specification Integer
c)]

-- TODO: consider improving this
instance Arbitrary (FoldSpec (Set a)) where
  arbitrary :: Gen (FoldSpec (Set a))
arbitrary = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. FoldSpec a
NoFold

guardSetSpec :: (HasSpec a, Ord a) => [String] -> SetSpec a -> Specification (Set a)
guardSetSpec :: forall a.
(HasSpec a, Ord a) =>
[String] -> SetSpec a -> Specification (Set a)
guardSetSpec [String]
es (SetSpec Set a
must Specification a
elemS ((forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
geqSpec Integer
0) -> Specification Integer
size))
  | Just Integer
u <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification Integer
size
  , Integer
u forall a. Ord a => a -> a -> Bool
< Integer
0 =
      forall a. NonEmpty String -> Specification a
ErrorSpec ((String
"guardSetSpec: negative size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
u) forall a. a -> [a] -> NonEmpty a
:| [String]
es)
  | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
elemS) Set a
must) =
      forall a. NonEmpty String -> Specification a
ErrorSpec ((String
"Some 'must' items do not conform to 'element' spec: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
elemS) forall a. a -> [a] -> NonEmpty a
:| [String]
es)
  | forall a. Specification a -> Bool
isErrorLike Specification Integer
size = forall a. NonEmpty String -> Specification a
ErrorSpec (String
"guardSetSpec: error in size" forall a. a -> [a] -> NonEmpty a
:| [String]
es)
  | forall a. Specification a -> Bool
isErrorLike (forall a. OrdLike a => a -> Specification a
geqSpec (forall t. Sized t => t -> Integer
sizeOf Set a
must) forall a. Semigroup a => a -> a -> a
<> Specification Integer
size) =
      forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$
        (String
"Must set size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall t. Sized t => t -> Integer
sizeOf Set a
must) forall a. [a] -> [a] -> [a]
++ String
", is inconsistent with SetSpec size" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification Integer
size) forall a. a -> [a] -> NonEmpty a
:| [String]
es
  | forall a. Specification a -> Bool
isErrorLike (Specification Integer -> Specification Integer
maxSpec (forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality Specification a
elemS) forall a. Semigroup a => a -> a -> a
<> Specification Integer
size) =
      forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$
        forall a. [a] -> NonEmpty a
NE.fromList forall a b. (a -> b) -> a -> b
$
          [ String
"Cardinality of SetSpec elemSpec (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Specification a
elemS) forall a. [a] -> [a] -> [a]
++ String
") = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Specification Integer -> Specification Integer
maxSpec (forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality Specification a
elemS))
          , String
"   This is inconsistent with SetSpec size (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification Integer
size forall a. [a] -> [a] -> [a]
++ String
")"
          ]
            forall a. [a] -> [a] -> [a]
++ [String]
es
  | Bool
otherwise = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec Set a
must Specification a
elemS Specification Integer
size)

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

  type Prerequisites (Set a) = HasSpec a

  emptySpec :: TypeSpec (Set a)
emptySpec = forall a. Monoid a => a
mempty

  combineSpec :: TypeSpec (Set a) -> TypeSpec (Set a) -> Specification (Set a)
combineSpec TypeSpec (Set a)
s TypeSpec (Set a)
s' = forall a.
(HasSpec a, Ord a) =>
[String] -> SetSpec a -> Specification (Set a)
guardSetSpec [String
"While combining 2 SetSpecs", String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeSpec (Set a)
s, String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeSpec (Set a)
s'] (TypeSpec (Set a)
s forall a. Semigroup a => a -> a -> a
<> TypeSpec (Set a)
s')

  conformsTo :: HasCallStack => Set a -> TypeSpec (Set a) -> Bool
conformsTo Set a
s (SetSpec Set a
must Specification a
es Specification Integer
size) =
    forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      [ forall t. Sized t => t -> Integer
sizeOf Set a
s forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification Integer
size
      , Set a
must forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set a
s
      , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
es) Set a
s
      ]

  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec (Set a) -> GenT m (Set a)
genFromTypeSpec (SetSpec Set a
must Specification a
e Specification Integer
_)
    | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
e)) Set a
must =
        forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
genErrorNE
          ( forall a. [a] -> NonEmpty a
NE.fromList
              [ String
"Failed to generate set"
              , String
"Some element in the must set does not conform to the elem specification"
              , String
"Unconforming elements from the must set:"
              , [String] -> String
unlines (forall a b. (a -> b) -> [a] -> [b]
map (\a
x -> String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
x) (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
e)) (forall a. Set a -> [a]
Set.toList Set a
must)))
              , String
"Element Specifcation"
              , String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
e
              ]
          )
  -- Special case when elemS is a MemberSpec.
  -- Just union 'must' with enough elements of 'xs' to meet  'szSpec'
  genFromTypeSpec (SetSpec Set a
must (ExplainSpec [] Specification a
elemspec) Specification Integer
szSpec) =
    forall a (m :: * -> *).
(HasSpec a, HasCallStack, MonadGenError m) =>
TypeSpec a -> GenT m a
genFromTypeSpec (forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec Set a
must Specification a
elemspec Specification Integer
szSpec)
  genFromTypeSpec (SetSpec Set a
must (ExplainSpec (String
e : [String]
es) Specification a
elemspec) Specification Integer
szSpec) =
    forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE (String
e forall a. a -> [a] -> NonEmpty a
:| [String]
es) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(HasSpec a, HasCallStack, MonadGenError m) =>
TypeSpec a -> GenT m a
genFromTypeSpec (forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec Set a
must Specification a
elemspec Specification Integer
szSpec)
  genFromTypeSpec (SetSpec Set a
must elemS :: Specification a
elemS@(MemberSpec NonEmpty a
xs) Specification Integer
szSpec) = do
    let szSpec' :: Specification Integer
szSpec' = Specification Integer
szSpec forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
geqSpec (forall t. Sized t => t -> Integer
sizeOf Set a
must) forall a. Semigroup a => a -> a -> a
<> Specification Integer -> Specification Integer
maxSpec (forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality Specification a
elemS)
    [a]
choices <- forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Gen [a]
shuffle (forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
xs forall a. Eq a => [a] -> [a] -> [a]
\\ forall a. Set a -> [a]
Set.toList Set a
must)
    Int
size <- forall a. Num a => Integer -> a
fromInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification Integer
szSpec'
    let additions :: Set a
additions = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take (Int
size forall a. Num a => a -> a -> a
- forall a. Set a -> Int
Set.size Set a
must) [a]
choices
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Ord a => Set a -> Set a -> Set a
Set.union Set a
must Set a
additions)
  genFromTypeSpec (SetSpec Set a
must Specification a
elemS Specification Integer
szSpec) = do
    let szSpec' :: Specification Integer
szSpec' = (Specification Integer
szSpec forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
geqSpec (forall t. Sized t => t -> Integer
sizeOf Set a
must) forall a. Semigroup a => a -> a -> a
<> Specification Integer -> Specification Integer
maxSpec (forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality Specification a
elemS))
    Integer
count <-
      forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain String
"Choose a size for the Set to be generated" forall a b. (a -> b) -> a -> b
$
        forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification Integer
szSpec'
    let targetSize :: Integer
targetSize = Integer
count forall a. Num a => a -> a -> a
- forall t. Sized t => t -> Integer
sizeOf Set a
must
    forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
      ( forall a. [a] -> NonEmpty a
NE.fromList
          [ String
"Choose size count = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
count
          , String
"szSpec' = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification Integer
szSpec'
          , String
"Picking items not in must = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a x. (Show a, Typeable a) => [a] -> Doc x
short (forall a. Set a -> [a]
Set.toList Set a
must))
          , String
"that also meet the element test: "
          , String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
elemS
          ]
      )
      forall a b. (a -> b) -> a -> b
$ case Integer
theMostWeCanExpect of
        -- 0 means TrueSpec or SuspendedSpec so we can't rule anything out
        Integer
0 -> Int -> Integer -> Set a -> GenT m (Set a)
go Int
100 Integer
targetSize Set a
must
        Integer
n -> case forall a. Ord a => a -> a -> Ordering
compare Integer
n Integer
targetSize of
          Ordering
LT -> forall (m :: * -> *) a. MonadGenError m => String -> m a
fatalError String
"The number of things that meet the element test is too small."
          Ordering
GT -> Int -> Integer -> Set a -> GenT m (Set a)
go Int
100 Integer
targetSize Set a
must
          Ordering
EQ -> Int -> Integer -> Set a -> GenT m (Set a)
go Int
100 Integer
targetSize Set a
must
    where
      theMostWeCanExpect :: Integer
theMostWeCanExpect = forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
maxFromSpec Integer
0 (forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality (forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification a
elemS))
      go :: Int -> Integer -> Set a -> GenT m (Set a)
go Int
_ Integer
n Set a
s | Integer
n forall a. Ord a => a -> a -> Bool
<= Integer
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Set a
s
      go Int
tries Integer
n Set a
s = do
        a
e <-
          forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
            ( forall a. [a] -> NonEmpty a
NE.fromList
                [ String
"Generate set member at type " forall a. [a] -> [a] -> [a]
++ forall {k} (t :: k). Typeable t => String
showType @a
                , String
"  number of items starting with  = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Set a -> Int
Set.size Set a
must)
                , String
"  number of items left to pick   = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n
                , String
"  number of items already picked = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Set a -> Int
Set.size Set a
s)
                , String
"  the most items we can expect is " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
theMostWeCanExpect forall a. [a] -> [a] -> [a]
++ String
" (a SuspendedSpec)"
                ]
            )
            forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. GenMode -> GenT m a -> GenT m a
withMode GenMode
Strict
            forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
Int -> GenT m a -> (a -> Bool) -> GenT m a
suchThatWithTryT Int
tries (forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
elemS) (forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set a
s)

        Int -> Integer -> Set a -> GenT m (Set a)
go Int
tries (Integer
n forall a. Num a => a -> a -> a
- Integer
1) (forall a. Ord a => a -> Set a -> Set a
Set.insert a
e Set a
s)

  cardinalTypeSpec :: TypeSpec (Set a) -> Specification Integer
cardinalTypeSpec (SetSpec Set a
_ Specification a
es Specification Integer
_)
    | Just Integer
ub <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound (forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality Specification a
es) = forall a. OrdLike a => a -> Specification a
leqSpec (Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
ub)
  cardinalTypeSpec TypeSpec (Set a)
_ = forall a. Specification a
TrueSpec

  cardinalTrueSpec :: Specification Integer
cardinalTrueSpec
    | Just Integer
ub <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Specification Integer
cardinalTrueSpec @a = forall a. OrdLike a => a -> Specification a
leqSpec (Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
ub)
    | Bool
otherwise = forall a. Specification a
TrueSpec

  shrinkWithTypeSpec :: TypeSpec (Set a) -> Set a -> [Set a]
shrinkWithTypeSpec (SetSpec Set a
_ Specification a
es Specification Integer
_) Set a
as = forall a b. (a -> b) -> [a] -> [b]
map forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList (forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification a
es) (forall a. Set a -> [a]
Set.toList Set a
as)

  toPreds :: Term (Set a) -> TypeSpec (Set a) -> Pred
toPreds Term (Set a)
s (SetSpec Set a
m Specification a
es Specification Integer
size) =
    forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold forall a b. (a -> b) -> a -> b
$
      -- Don't include this if the must set is empty
      [ NonEmpty String -> Pred -> Pred
Explain (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Show a => a -> String
show Set a
m forall a. [a] -> [a] -> [a]
++ String
" is a subset of the set.")) forall a b. (a -> b) -> a -> b
$ Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Set a
m) Term (Set a)
s
      | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Set a -> Bool
Set.null Set a
m
      ]
        forall a. [a] -> [a] -> [a]
++ [ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set a)
s (\Term a
e -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term a
e Specification a
es)
           , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Set a)
s) Specification Integer
size
           ]

  guardTypeSpec :: [String] -> TypeSpec (Set a) -> Specification (Set a)
guardTypeSpec = forall a.
(HasSpec a, Ord a) =>
[String] -> SetSpec a -> Specification (Set a)
guardSetSpec

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 :: SetW ds r -> String
show SetW ds r
SingletonW = String
"singleton_"
  show SetW ds r
UnionW = String
"union_"
  show SetW ds r
SubsetW = String
"subset_"
  show SetW ds r
MemberW = String
"member_"
  show SetW ds r
DisjointW = String
"disjoint_"
  show SetW ds r
FromListW = String
"fromList_"

setSem :: SetW ds r -> FunTy ds r
setSem :: forall (ds :: [*]) r. SetW ds r -> FunTy ds r
setSem SetW ds r
SingletonW = forall a. a -> Set a
Set.singleton
setSem SetW ds r
UnionW = forall a. Ord a => Set a -> Set a -> Set a
Set.union
setSem SetW ds r
SubsetW = forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf
setSem SetW ds r
MemberW = forall a. Ord a => a -> Set a -> Bool
Set.member
setSem SetW ds r
DisjointW = forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint
setSem SetW ds r
FromListW = forall a. Ord a => [a] -> Set a
Set.fromList

instance Semantics SetW where
  semantics :: forall (ds :: [*]) r. SetW ds r -> FunTy ds r
semantics = forall (ds :: [*]) r. SetW ds r -> FunTy ds r
setSem

instance Syntax SetW where
  prettyWit :: forall (dom :: [*]) rng ann.
(All HasSpec dom, HasSpec rng) =>
SetW dom rng -> List Term dom -> Int -> Maybe (Doc ann)
prettyWit SetW dom rng
SubsetW (Lit a
n :> Term a
y :> List Term as1
Nil) Int
p = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ Doc ann
"subset_" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a x. (Show a, Typeable a) => [a] -> Doc x
short (forall a. Set a -> [a]
Set.toList a
n) forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 Term a
y
  prettyWit SetW dom rng
SubsetW (Term a
y :> Lit a
n :> List Term as1
Nil) Int
p = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ Doc ann
"subset_" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 Term a
y forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a x. (Show a, Typeable a) => [a] -> Doc x
short (forall a. Set a -> [a]
Set.toList a
n)
  prettyWit SetW dom rng
DisjointW (Lit a
n :> Term a
y :> List Term as1
Nil) Int
p = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ Doc ann
"disjoint_" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a x. (Show a, Typeable a) => [a] -> Doc x
short (forall a. Set a -> [a]
Set.toList a
n) forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 Term a
y
  prettyWit SetW dom rng
DisjointW (Term a
y :> Lit a
n :> List Term as1
Nil) Int
p = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ Doc ann
"disjoint_" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 Term a
y forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a x. (Show a, Typeable a) => [a] -> Doc x
short (forall a. Set a -> [a]
Set.toList a
n)
  prettyWit SetW dom rng
UnionW (Lit a
n :> Term a
y :> List Term as1
Nil) Int
p = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ Doc ann
"union_" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a x. (Show a, Typeable a) => [a] -> Doc x
short (forall a. Set a -> [a]
Set.toList a
n) forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 Term a
y
  prettyWit SetW dom rng
UnionW (Term a
y :> Lit a
n :> List Term as1
Nil) Int
p = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ Doc ann
"union_" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 Term a
y forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a x. (Show a, Typeable a) => [a] -> Doc x
short (forall a. Set a -> [a]
Set.toList a
n)
  prettyWit SetW dom rng
MemberW (Term a
y :> Lit a
n :> List Term as1
Nil) Int
p = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ Doc ann
"member_" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 Term a
y forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a x. (Show a, Typeable a) => [a] -> Doc x
short (forall a. Set a -> [a]
Set.toList a
n)
  prettyWit SetW dom rng
_ List Term dom
_ Int
_ = forall a. Maybe a
Nothing

instance (Ord a, HasSpec a, HasSpec (Set a)) => Semigroup (Term (Set a)) where
  <> :: Term (Set a) -> Term (Set a) -> Term (Set a)
(<>) = forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term (Set a)
union_

instance (Ord a, HasSpec a, HasSpec (Set a)) => Monoid (Term (Set a)) where
  mempty :: Term (Set a)
mempty = forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit forall a. Monoid a => a
mempty

-- ================= Logic instances ================

-- ==== SingletonW

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

instance Logic SetW where
  propagate :: forall (as :: [*]) b a.
(AppRequires SetW as b, HasSpec a) =>
SetW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate SetW as b
f ListCtx Value as (HOLE a)
ctxt (ExplainSpec [String]
es Specification b
s) = forall a. [String] -> Specification a -> Specification a
explainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate SetW as b
f ListCtx Value as (HOLE a)
ctxt Specification b
s
  propagate SetW as b
_ ListCtx Value as (HOLE a)
_ Specification b
TrueSpec = forall a. Specification a
TrueSpec
  propagate SetW as b
_ ListCtx Value as (HOLE a)
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate SetW as b
f ListCtx Value as (HOLE a)
ctx (SuspendedSpec Var b
v Pred
ps) = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term a
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App SetW as b
f (forall (as :: [*]) a.
All HasSpec as =>
ListCtx Value as (HOLE a) -> Term a -> List Term as
fromListCtx ListCtx Value as (HOLE a)
ctx Term a
v')) (Var b
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate SetW as b
SingletonW (Unary HOLE a a
HOLE) (TypeSpec (SetSpec Set a
must Specification a
es Specification Integer
size) [b]
cant)
    | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Integer
1 forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification Integer
size =
        forall a. NonEmpty String -> Specification a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"propagateSpecFun Singleton with spec that doesn't accept 1 size set")
    | [a
a] <- forall a. Set a -> [a]
Set.toList Set a
must
    , a
a forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
es
    , forall a. a -> Set a
Set.singleton a
a forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [b]
cant =
        forall a. a -> Specification a
equalSpec a
a
    | forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set a
must = Specification a
es forall a. Semigroup a => a -> a -> a
<> forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec (forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold forall a b. (a -> b) -> a -> b
$ forall a. [Set a] -> [Set a]
singletons [b]
cant)
    | Bool
otherwise = forall a. NonEmpty String -> Specification a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"propagateSpecFun Singleton with `must` of size > 1")
  propagate SetW as b
SingletonW (Unary HOLE a a
HOLE) (MemberSpec NonEmpty b
es) =
    case forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold forall a b. (a -> b) -> a -> b
$ forall a. [Set a] -> [Set a]
singletons (forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es) of
      [] -> forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"In propagateSpecFun Singleton, the sets of size 1, in MemberSpec is empty"
      (a
x : [a]
xs) -> forall a. NonEmpty a -> Specification a
MemberSpec (a
x forall a. a -> [a] -> NonEmpty a
:| [a]
xs)
  propagate SetW as b
UnionW ListCtx Value as (HOLE a)
ctx Specification b
spec
    | (Value a
s :! Unary HOLE a (Set a)
HOLE) <- ListCtx Value as (HOLE a)
ctx =
        forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate forall a. (HasSpec a, Ord a) => SetW '[Set a, Set a] (Set a)
UnionW (forall {k} (a :: k). HOLE a a
HOLE forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:? forall a. Show a => a -> Value a
Value a
s forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil) Specification b
spec
    | (HOLE a a
HOLE :? Value (Set a
s :: Set a) :> List Value as1
Nil) <- ListCtx Value as (HOLE a)
ctx
    , Evidence (Prerequisites (Set a))
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @(Set a) =
        case Specification b
spec of
          Specification b
_ | forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set a
s -> Specification b
spec
          TypeSpec (SetSpec Set a
must Specification a
es Specification Integer
size) [b]
cant
            | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
es) Set a
s ->
                forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$
                  forall a. [a] -> NonEmpty a
NE.fromList
                    [ String
"Elements in union argument does not conform to elem spec"
                    , String
"  spec: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
es
                    , String
"  elems: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
es)) (forall a. Set a -> [a]
Set.toList Set a
s))
                    ]
            | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [b]
cant -> forall a. NonEmpty String -> Specification a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"propagateSpecFun Union TypeSpec, not (null cant)")
            | Specification Integer
TrueSpec <- Specification Integer
size -> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec (forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set a
must Set a
s) Specification a
es forall a. Specification a
TrueSpec
            | TypeSpec (NumSpecInterval Maybe Integer
mlb Maybe Integer
Nothing) [] <- Specification Integer
size
            , forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (forall a. Ord a => a -> a -> Bool
<= forall t. Sized t => t -> Integer
sizeOf Set a
s) Maybe Integer
mlb ->
                forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec (forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set a
must Set a
s) Specification a
es forall a. Specification a
TrueSpec
            | Bool
otherwise -> forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term a
x ->
                forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (forall b. Term b -> b
eval Term a
x) Set a
s) forall a b. (a -> b) -> a -> b
$ \Term (Set a)
overlap ->
                  forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
Set.difference (forall b. Term b -> b
eval Term a
x) Set a
s) forall a b. (a -> b) -> a -> b
$ \Term (Set a)
disjoint ->
                    [ Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ Term (Set a)
overlap forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Set a
s
                    , Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ Term (Set a)
disjoint forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`disjoint_` forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Set a
s
                    , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Set a)
disjoint forall a. Num a => a -> a -> a
+ forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit (forall t. Sized t => t -> Integer
sizeOf Set a
s)) Specification Integer
size
                    , Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ Term a
x forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (Term (Set a)
overlap forall a. Semigroup a => a -> a -> a
<> Term (Set a)
disjoint) -- depends on Semigroup (Term (Set a))
                    , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set a)
disjoint forall a b. (a -> b) -> a -> b
$ \Term a
e -> Term a
e forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
es
                    , Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit (Set a
must forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set a
s) forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Term (Set a)
disjoint
                    ]
          -- We only do singleton MemberSpec to avoid really bad blowup
          MemberSpec (b
e :| [])
            | Set a
s forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` b
e ->
                forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec
                  ( forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec
                      (forall a. Ord a => Set a -> Set a -> Set a
Set.difference b
e Set a
s)
                      ( forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
                          (forall a. Set a -> [a]
Set.toList b
e)
                          (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"propagateSpec (union_ s HOLE) on (MemberSpec [e]) where e is the empty set")
                      )
                      forall a. Monoid a => a
mempty
                  )
          -- TODO: improve this error message
          Specification b
_ ->
            forall a. NonEmpty String -> Specification a
ErrorSpec
              ( forall a. [a] -> NonEmpty a
NE.fromList
                  [ String
"propagateSpecFun (union_ s HOLE) with spec"
                  , String
"s = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Set a
s
                  , String
"spec = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification b
spec
                  ]
              )
  propagate SetW as b
SubsetW ListCtx Value as (HOLE a)
ctx Specification b
spec
    | (HOLE a a
HOLE :? Value (Set a
s :: Set a) :> List Value as1
Nil) <- ListCtx Value as (HOLE a)
ctx
    , Evidence (Prerequisites (Set a))
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @(Set a) = forall a.
HasSpec a =>
Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec Specification b
spec forall a b. (a -> b) -> a -> b
$ \case
        Bool
True ->
          case forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty (forall a. Set a -> [a]
Set.toList Set a
s) of
            Maybe (NonEmpty a)
Nothing -> forall a. NonEmpty a -> Specification a
MemberSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Set a
Set.empty)
            Just NonEmpty a
slist -> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec forall a. Monoid a => a
mempty (forall a. NonEmpty a -> Specification a
MemberSpec NonEmpty a
slist) forall a. Monoid a => a
mempty
        Bool
False -> forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term a
set ->
          forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
eval -> forall (t :: * -> *) a. Foldable t => t a -> GE a
headGE forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
Set.difference (forall b. Term b -> b
eval Term a
set) Set a
s) forall a b. (a -> b) -> a -> b
$ \Term a
e ->
            [ Term a
set forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`DependsOn` Term a
e
            , Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ forall a b. (a -> b) -> a -> b
$ forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term a
e (forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Set a
s)
            , Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term a
e Term a
set
            ]
    | (Value (Set a
s :: Set a) :! Unary HOLE a (Set a)
HOLE) <- ListCtx Value as (HOLE a)
ctx
    , Evidence (Prerequisites (Set a))
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @(Set a) = forall a.
HasSpec a =>
Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec Specification b
spec forall a b. (a -> b) -> a -> b
$ \case
        Bool
True -> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec Set a
s forall a. Specification a
TrueSpec forall a. Monoid a => a
mempty
        Bool
False -> forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term a
set ->
          forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
eval -> forall (t :: * -> *) a. Foldable t => t a -> GE a
headGE forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
Set.difference (forall b. Term b -> b
eval Term a
set) Set a
s) forall a b. (a -> b) -> a -> b
$ \Term a
e ->
            [ Term a
set forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`DependsOn` Term a
e
            , Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term a
e (forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Set a
s)
            , Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ forall a b. (a -> b) -> a -> b
$ forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term a
e Term a
set
            ]
  propagate SetW as b
MemberW ListCtx Value as (HOLE a)
ctx Specification b
spec
    | (HOLE a a
HOLE :? Value a
s :> List Value as1
Nil) <- ListCtx Value as (HOLE a)
ctx = forall a.
HasSpec a =>
Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec Specification b
spec forall a b. (a -> b) -> a -> b
$ \case
        Bool
True -> forall a. [a] -> NonEmpty String -> Specification a
memberSpecList (forall a. Set a -> [a]
Set.toList a
s) (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"propagateSpecFun on (Member x s) where s is Set.empty")
        Bool
False -> forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec a
s
    | (Value a
e :! Unary HOLE a (Set a)
HOLE) <- ListCtx Value as (HOLE a)
ctx = forall a.
HasSpec a =>
Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec Specification b
spec forall a b. (a -> b) -> a -> b
$ \case
        Bool
True -> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec (forall a. a -> Set a
Set.singleton a
e) forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
        Bool
False -> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec forall a. Monoid a => a
mempty (forall a. HasSpec a => a -> Specification a
notEqualSpec a
e) forall a. Monoid a => a
mempty
  propagate SetW as b
DisjointW ListCtx Value as (HOLE a)
ctx Specification b
spec
    | (HOLE a a
HOLE :? Value (Set a
s :: Set a) :> List Value as1
Nil) <- ListCtx Value as (HOLE a)
ctx =
        forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate forall a. (HasSpec a, Ord a) => SetW '[Set a, Set a] Bool
DisjointW (forall a. Show a => a -> Value a
Value Set a
s forall (f :: * -> *) a (as1 :: [*]) (c :: * -> *).
f a -> ListCtx f as1 c -> ListCtx f (a : as1) c
:! forall a' a (f :: * -> *). HOLE a' a -> ListCtx f '[a] (HOLE a')
Unary forall {k} (a :: k). HOLE a a
HOLE) Specification b
spec
    | (Value (Set a
s :: Set a) :! Unary HOLE a (Set a)
HOLE) <- ListCtx Value as (HOLE a)
ctx
    , Evidence (Prerequisites (Set a))
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @(Set a) = forall a.
HasSpec a =>
Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec Specification b
spec forall a b. (a -> b) -> a -> b
$ \case
        Bool
True -> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec forall a. Monoid a => a
mempty (forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec Set a
s) forall a. Monoid a => a
mempty
        Bool
False -> forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term a
set ->
          forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
eval -> forall (t :: * -> *) a. Foldable t => t a -> GE a
headGE (forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (forall b. Term b -> b
eval Term a
set) Set a
s)) forall a b. (a -> b) -> a -> b
$ \Term a
e ->
            [ Term a
set forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`DependsOn` Term a
e
            , Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term a
e (forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Set a
s)
            , Term Bool -> Pred
Assert forall a b. (a -> b) -> a -> b
$ forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term a
e Term a
set
            ]
  propagate SetW as b
FromListW (Unary HOLE a [a]
HOLE) Specification b
spec =
    case Specification b
spec of
      MemberSpec (b
xs :| []) ->
        forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$
          forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec
            forall a. Maybe a
Nothing
            (forall a. Set a -> [a]
Set.toList b
xs)
            forall a. Specification a
TrueSpec
            ( forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
                (forall a. Set a -> [a]
Set.toList b
xs)
                (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"propagateSpec (fromList_ HOLE) on (MemberSpec xs) where the set 'xs' is empty")
            )
            forall a. FoldSpec a
NoFold
      TypeSpec (SetSpec Set a
must Specification a
elemSpec Specification Integer
sizeSpec) []
        | Specification Integer
TrueSpec <- Specification Integer
sizeSpec -> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec forall a. Maybe a
Nothing (forall a. Set a -> [a]
Set.toList Set a
must) forall a. Specification a
TrueSpec Specification a
elemSpec forall a. FoldSpec a
NoFold
        | TypeSpec (NumSpecInterval (Just Integer
l) Maybe Integer
Nothing) [Integer]
cantSize <- Specification Integer
sizeSpec
        , Integer
l forall a. Ord a => a -> a -> Bool
<= forall t. Sized t => t -> Integer
sizeOf Set a
must
        , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Ord a => a -> a -> Bool
< forall t. Sized t => t -> Integer
sizeOf Set a
must) [Integer]
cantSize ->
            forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec forall a. Maybe a
Nothing (forall a. Set a -> [a]
Set.toList Set a
must) forall a. Specification a
TrueSpec Specification a
elemSpec forall a. FoldSpec a
NoFold
      Specification b
_ ->
        -- 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.
        forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term a
xs ->
          forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList (forall b. Term b -> b
eval Term a
xs)) forall a b. (a -> b) -> a -> b
$ \Term (Set a)
s ->
            [ Term (Set a)
s forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification b
spec
            , Term a
xs forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`DependsOn` Term (Set a)
s
            , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term a
xs forall a b. (a -> b) -> a -> b
$ \Term a
e -> Term a
e forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` Term (Set a)
s
            , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set a)
s forall a b. (a -> b) -> a -> b
$ \Term a
e -> Term a
e forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` Term a
xs
            ]

  mapTypeSpec :: forall a b.
(HasSpec a, HasSpec b) =>
SetW '[a] b -> TypeSpec a -> Specification b
mapTypeSpec SetW '[a] b
FromListW TypeSpec a
ts =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term b
x ->
      forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists forall a b. (a -> b) -> a -> b
$ \Term [a]
x' -> Term Bool -> Pred
Assert (Term b
x forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
fromList_ Term [a]
x') forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => Term a -> TypeSpec a -> Pred
toPreds Term [a]
x' TypeSpec a
ts
  mapTypeSpec SetW '[a] b
SingletonW TypeSpec a
ts =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term b
x ->
      forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists forall a b. (a -> b) -> a -> b
$ \Term a
x' ->
        Term Bool -> Pred
Assert (Term b
x forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. (Ord a, HasSpec a) => Term a -> Term (Set a)
singleton_ Term a
x') forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => Term a -> TypeSpec a -> Pred
toPreds Term a
x' TypeSpec a
ts

  rewriteRules :: forall (dom :: [*]) rng.
(TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) =>
SetW dom rng
-> List Term dom
-> Evidence (AppRequires SetW dom rng)
-> Maybe (Term rng)
rewriteRules SetW dom rng
SubsetW (Lit a
s :> Term a
_ :> List Term as1
Nil) Evidence (AppRequires SetW dom rng)
Evidence | forall (t :: * -> *) a. Foldable t => t a -> Bool
null a
s = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Bool
True
  rewriteRules SetW dom rng
SubsetW (Term a
x :> Lit a
s :> List Term as1
Nil) Evidence (AppRequires SetW dom rng)
Evidence | forall (t :: * -> *) a. Foldable t => t a -> Bool
null a
s = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term a
x forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit forall a. Set a
Set.empty
  rewriteRules SetW dom rng
UnionW (Term a
x :> Lit a
s :> List Term as1
Nil) Evidence (AppRequires SetW dom rng)
Evidence | forall (t :: * -> *) a. Foldable t => t a -> Bool
null a
s = forall a. a -> Maybe a
Just Term a
x
  rewriteRules SetW dom rng
UnionW (Lit a
s :> Term a
x :> List Term as1
Nil) Evidence (AppRequires SetW dom rng)
Evidence | forall (t :: * -> *) a. Foldable t => t a -> Bool
null a
s = forall a. a -> Maybe a
Just Term a
x
  rewriteRules SetW dom rng
MemberW (Term a
t :> Lit a
s :> List Term as1
Nil) Evidence (AppRequires SetW dom rng)
Evidence
    | forall (t :: * -> *) a. Foldable t => t a -> Bool
null a
s = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Bool
False
    | [a
a] <- forall a. Set a -> [a]
Set.toList a
s = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term a
t forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
a
  rewriteRules SetW dom rng
DisjointW (Lit a
s :> Term a
_ :> List Term as1
Nil) Evidence (AppRequires SetW dom rng)
Evidence | forall (t :: * -> *) a. Foldable t => t a -> Bool
null a
s = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Bool
True
  rewriteRules SetW dom rng
DisjointW (Term a
_ :> Lit a
s :> List Term as1
Nil) Evidence (AppRequires SetW dom rng)
Evidence | forall (t :: * -> *) a. Foldable t => t a -> Bool
null a
s = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Bool
True
  rewriteRules SetW dom rng
_ List Term dom
_ Evidence (AppRequires SetW dom rng)
_ = forall a. Maybe a
Nothing

singleton_ :: (Ord a, HasSpec a) => Term a -> Term (Set a)
singleton_ :: forall a. (Ord a, HasSpec a) => Term a -> Term (Set a)
singleton_ = forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. (HasSpec a, Ord a) => SetW '[a] (Set a)
SingletonW

subset_ :: (Ord a, HasSpec a) => Term (Set a) -> Term (Set a) -> Term Bool
subset_ :: forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ = forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a.
(HasSpec a, Ord a, HasSpec a) =>
SetW '[Set a, Set a] Bool
SubsetW

-- ==== MemberW =====

member_ :: (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ :: forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ = forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. (HasSpec a, Ord a) => SetW '[a, Set a] Bool
MemberW

-- ==== UnionW =====

union_ :: (Ord a, HasSpec a) => Term (Set a) -> Term (Set a) -> Term (Set a)
union_ :: forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term (Set a)
union_ = forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. (HasSpec a, Ord a) => SetW '[Set a, Set a] (Set a)
UnionW

-- ==== DisjointW =====

disjoint_ :: (Ord a, HasSpec a) => Term (Set a) -> Term (Set a) -> Term Bool
disjoint_ :: forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
disjoint_ = forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. (HasSpec a, Ord a) => SetW '[Set a, Set a] Bool
DisjointW

-- ==== FromListW =====

fromList_ :: forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
fromList_ :: forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
fromList_ = forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. (HasSpec a, Ord a) => SetW '[[a]] (Set a)
FromListW