{-# 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 QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- 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
import Constrained.Conformance (conformsToSpec, satisfies)
import Constrained.Core (Evidence (..), NonEmpty ((:|)))
import Constrained.GenT
import Constrained.List
import Constrained.NumSpec
import Constrained.Spec.ListFoldy (
  FoldSpec (..),
  ListSpec (..),
  elem_,
  knownUpperBound,
  maxFromSpec,
 )
import Constrained.Spec.Size (Sized (..), maxSpec, sizeOf_)
import Constrained.Syntax (exists, forAll, unsafeExists)
import Constrained.TheKnot (caseBoolSpec, genFromSpecT, not_, shrinkWithSpec, simplifySpec, (==.))
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 GHC.TypeLits
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
genError
          ( 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
explain (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
explain1 (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
explain
      ( 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, HasCallStack) =>
NonEmpty String -> m a
fatalError (forall (f :: * -> *) a. Applicative f => a -> f a
pure 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, 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
explain
            ( 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. Literal 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 t. (HasSpec t, Sized t) => Term t -> 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 (s :: Symbol) (d :: [Type]) (r :: Type) where
  SingletonW :: Ord a => SetW "singleton_" '[a] (Set a)
  UnionW :: (Literal a, Ord a) => SetW "union_" '[Set a, Set a] (Set a)
  SubsetW :: (Literal a, Ord a) => SetW "subset_" '[Set a, Set a] Bool
  MemberW :: (Literal a, Ord a) => SetW "member_" '[a, Set a] Bool
  DisjointW :: (Literal a, Ord a) => SetW "disjoint_" '[Set a, Set a] Bool
  FromListW :: forall a. (HasSpec a, Ord a) => SetW "fromList_" '[[a]] (Set a)

deriving instance Eq (SetW s dom rng)

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

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

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

instance Syntax SetW where
  prettyWit :: forall (s :: Symbol) (dom :: [*]) rng ann.
(All HasSpec dom, HasSpec rng) =>
SetW s dom rng -> List Term dom -> Int -> Maybe (Doc ann)
prettyWit SetW s 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 s 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 s 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 s 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 s 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 s 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 s 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 s 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. Literal 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 (HasSpec a, Ord a) => Logic "singleton_" SetW '[a] (Set a) where
  propagate :: forall hole.
Context "singleton_" SetW '[a] (Set a) hole
-> Specification (Set a) -> Specification hole
propagate Context "singleton_" SetW '[a] (Set a) hole
ctxt (ExplainSpec [] Specification (Set a)
s) = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "singleton_" SetW '[a] (Set a) hole
ctxt Specification (Set a)
s
  propagate Context "singleton_" SetW '[a] (Set a) hole
ctxt (ExplainSpec [String]
es Specification (Set a)
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "singleton_" SetW '[a] (Set a) hole
ctxt Specification (Set a)
s
  propagate Context "singleton_" SetW '[a] (Set a) hole
_ Specification (Set a)
TrueSpec = forall a. Specification a
TrueSpec
  propagate Context "singleton_" SetW '[a] (Set a) hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context SetW "singleton_" '[a] (Set a)
SingletonW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (SuspendedSpec Var (Set a)
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a. Ord a => SetW "singleton_" '[a] (Set a)
SingletonW (Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var (Set a)
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context SetW "singleton_" '[a] (Set a)
SingletonW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (TypeSpec (SetSpec Set a
must Specification a
es Specification Integer
size) [Set a]
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` [Set a]
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 [Set a]
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 (Context SetW "singleton_" '[a] (Set a)
SingletonW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (MemberSpec NonEmpty (Set a)
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 (Set a)
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 Context "singleton_" SetW '[a] (Set a) hole
ctx Specification (Set a)
_ =
    forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Logic instance for SingletonW with wrong number of arguments. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Context "singleton_" SetW '[a] (Set a) hole
ctx)

  mapTypeSpec :: forall a b.
('[a] ~ '[a], Set a ~ b, HasSpec a, HasSpec b) =>
SetW "singleton_" '[a] b -> TypeSpec a -> Specification b
mapTypeSpec SetW "singleton_" '[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

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

-- ==== SubsetW =====

instance (HasSpec a, Ord a) => Logic "subset_" SetW '[Set a, Set a] Bool where
  propagate :: forall hole.
Context "subset_" SetW '[Set a, Set a] Bool hole
-> Specification Bool -> Specification hole
propagate Context "subset_" SetW '[Set a, Set a] Bool hole
ctxt (ExplainSpec [String]
es Specification Bool
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "subset_" SetW '[Set a, Set a] Bool hole
ctxt Specification Bool
s
  propagate Context "subset_" SetW '[Set a, Set a] Bool hole
_ Specification Bool
TrueSpec = forall a. Specification a
TrueSpec
  propagate Context "subset_" SetW '[Set a, Set a] Bool hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context SetW "subset_" '[Set a, Set a] Bool
SubsetW (Ctx hole y
HOLE :<> a
x :<| CList 'Post as1 Any Any
End)) (SuspendedSpec Var Bool
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a. (Literal a, Ord a) => SetW "subset_" '[Set a, Set a] Bool
SubsetW (Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall a. Literal a => a -> Term a
Lit a
x forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var Bool
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context SetW "subset_" '[Set a, Set a] Bool
SubsetW (a
x :|> Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (SuspendedSpec Var Bool
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a. (Literal a, Ord a) => SetW "subset_" '[Set a, Set a] Bool
SubsetW (forall a. Literal a => a -> Term a
Lit a
x forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var Bool
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context SetW "subset_" '[Set a, Set a] Bool
SubsetW CList 'Pre '[Set a, Set a] hole y
ctx) Specification Bool
spec
    | (Ctx hole y
HOLE :<> (Set a
s :: Set a) :<| CList 'Post as1 Any Any
End) <- CList 'Pre '[Set a, Set a] hole y
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 Bool
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 hole
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 hole
set) Set a
s) forall a b. (a -> b) -> a -> b
$ \Term a
e ->
            [ Term hole
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. Literal 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 hole
set
            ]
    | ((Set a
s :: Set a) :|> Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End) <- CList 'Pre '[Set a, Set a] hole y
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 Bool
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 hole
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 hole
set) Set a
s) forall a b. (a -> b) -> a -> b
$ \Term a
e ->
            [ Term hole
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. Literal 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 hole
set
            ]
  propagate Context "subset_" SetW '[Set a, Set a] Bool hole
ctx Specification Bool
_ = forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Logic instance for SubsetW with wrong number of arguments. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Context "subset_" SetW '[Set a, Set a] Bool hole
ctx)

  rewriteRules :: (TypeList '[Set a, Set a], Typeable '[Set a, Set a], HasSpec Bool,
 All HasSpec '[Set a, Set a]) =>
SetW "subset_" '[Set a, Set a] Bool
-> List Term '[Set a, Set a]
-> Evidence (AppRequires "subset_" SetW '[Set a, Set a] Bool)
-> Maybe (Term Bool)
rewriteRules SetW "subset_" '[Set a, Set a] Bool
SubsetW (Lit a
s :> Term a
_ :> List Term as1
Nil) Evidence (AppRequires "subset_" SetW '[Set a, Set a] Bool)
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. Literal a => a -> Term a
Lit Bool
True
  rewriteRules SetW "subset_" '[Set a, Set a] Bool
SubsetW (Term a
x :> Lit a
s :> List Term as1
Nil) Evidence (AppRequires "subset_" SetW '[Set a, Set a] Bool)
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. Literal a => a -> Term a
Lit forall a. Set a
Set.empty
  rewriteRules SetW "subset_" '[Set a, Set a] Bool
_ List Term '[Set a, Set a]
_ Evidence (AppRequires "subset_" SetW '[Set a, Set a] Bool)
_ = forall a. Maybe a
Nothing

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 (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. (Literal a, Ord a) => SetW "subset_" '[Set a, Set a] Bool
SubsetW

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

instance (HasSpec a, Ord a) => Logic "member_" SetW '[a, Set a] Bool where
  propagate :: forall hole.
Context "member_" SetW '[a, Set a] Bool hole
-> Specification Bool -> Specification hole
propagate Context "member_" SetW '[a, Set a] Bool hole
ctxt (ExplainSpec [String]
es Specification Bool
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "member_" SetW '[a, Set a] Bool hole
ctxt Specification Bool
s
  propagate Context "member_" SetW '[a, Set a] Bool hole
_ Specification Bool
TrueSpec = forall a. Specification a
TrueSpec
  propagate Context "member_" SetW '[a, Set a] Bool hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context SetW "member_" '[a, Set a] Bool
MemberW (Ctx hole y
HOLE :<> a
x :<| CList 'Post as1 Any Any
End)) (SuspendedSpec Var Bool
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a. (Literal a, Ord a) => SetW "member_" '[a, Set a] Bool
MemberW (Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall a. Literal a => a -> Term a
Lit a
x forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var Bool
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context SetW "member_" '[a, Set a] Bool
MemberW (a
x :|> Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (SuspendedSpec Var Bool
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a. (Literal a, Ord a) => SetW "member_" '[a, Set a] Bool
MemberW (forall a. Literal a => a -> Term a
Lit (a
x :: a) forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var Bool
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate Context "member_" SetW '[a, Set a] Bool hole
ctx (SuspendedSpec Var Bool
_ Pred
_) = forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Logic instance for MemberW with wrong number of arguments. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Context "member_" SetW '[a, Set a] Bool hole
ctx)
  propagate (Context SetW "member_" '[a, Set a] Bool
MemberW CList 'Pre '[a, Set a] hole y
ctx) Specification Bool
spec
    | (Ctx hole y
HOLE :<> a
s :<| CList 'Post as1 Any Any
End) <- CList 'Pre '[a, Set a] hole y
ctx = forall a.
HasSpec a =>
Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec Specification Bool
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
    | (a
e :|> Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End) <- CList 'Pre '[a, Set a] hole y
ctx = forall a.
HasSpec a =>
Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec Specification Bool
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 Context "member_" SetW '[a, Set a] Bool hole
ctx Specification Bool
_ = forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Logic instance for MemberW with wrong number of arguments. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Context "member_" SetW '[a, Set a] Bool hole
ctx)

  rewriteRules :: (TypeList '[a, Set a], Typeable '[a, Set a], HasSpec Bool,
 All HasSpec '[a, Set a]) =>
SetW "member_" '[a, Set a] Bool
-> List Term '[a, Set a]
-> Evidence (AppRequires "member_" SetW '[a, Set a] Bool)
-> Maybe (Term Bool)
rewriteRules SetW "member_" '[a, Set a] Bool
MemberW (Term a
t :> Lit a
s :> List Term as1
Nil) Evidence (AppRequires "member_" SetW '[a, Set a] Bool)
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. Literal 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. Literal a => a -> Term a
Lit a
a
  rewriteRules SetW "member_" '[a, Set a] Bool
_ List Term '[a, Set a]
_ Evidence (AppRequires "member_" SetW '[a, Set a] Bool)
_ = forall a. Maybe a
Nothing

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 (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. (Literal a, Ord a) => SetW "member_" '[a, Set a] Bool
MemberW

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

instance (HasSpec a, Ord a) => Logic "union_" SetW '[Set a, Set a] (Set a) where
  propagate :: forall hole.
Context "union_" SetW '[Set a, Set a] (Set a) hole
-> Specification (Set a) -> Specification hole
propagate Context "union_" SetW '[Set a, Set a] (Set a) hole
ctxt (ExplainSpec [String]
es Specification (Set a)
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "union_" SetW '[Set a, Set a] (Set a) hole
ctxt Specification (Set a)
s
  propagate Context "union_" SetW '[Set a, Set a] (Set a) hole
_ Specification (Set a)
TrueSpec = forall a. Specification a
TrueSpec
  propagate Context "union_" SetW '[Set a, Set a] (Set a) hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context SetW "union_" '[Set a, Set a] (Set a)
UnionW (Ctx hole y
HOLE :<> a
x :<| CList 'Post as1 Any Any
End)) (SuspendedSpec Var (Set a)
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a.
(Literal a, Ord a) =>
SetW "union_" '[Set a, Set a] (Set a)
UnionW (Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall a. Literal a => a -> Term a
Lit a
x forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var (Set a)
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context SetW "union_" '[Set a, Set a] (Set a)
UnionW (a
x :|> Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (SuspendedSpec Var (Set a)
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a.
(Literal a, Ord a) =>
SetW "union_" '[Set a, Set a] (Set a)
UnionW (forall a. Literal a => a -> Term a
Lit a
x forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var (Set a)
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context SetW "union_" '[Set a, Set a] (Set a)
UnionW CList 'Pre '[Set a, Set a] hole y
ctx) Specification (Set a)
spec
    | (a
s :|> Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End) <- CList 'Pre '[Set a, Set a] hole y
ctx =
        forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole y.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole y -> Context s t dom rng hole
Context forall a.
(Literal a, Ord a) =>
SetW "union_" '[Set a, Set a] (Set a)
UnionW (forall hole. HasSpec hole => Ctx hole hole
HOLE forall y hole (as1 :: [*]).
HasSpec y =>
Ctx hole y
-> (forall i j. CList 'Post as1 i j) -> CList 'Pre (y : as1) hole y
:<> a
s forall a (as1 :: [*]) hole y.
Literal a =>
a -> CList 'Post as1 hole y -> CList 'Post (a : as1) hole y
:<| forall hole y. CList 'Post '[] hole y
End)) Specification (Set a)
spec
    | (Ctx hole y
HOLE :<> (Set a
s :: Set a) :<| CList 'Post as1 Any Any
End) <- CList 'Pre '[Set a, Set a] hole y
ctx
    , Evidence (Prerequisites (Set a))
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @(Set a) =
        case Specification (Set a)
spec of
          Specification (Set a)
_ | forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set a
s -> Specification (Set a)
spec
          TypeSpec (SetSpec Set a
must Specification a
es Specification Integer
size) [Set a]
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 [Set a]
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 hole
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 hole
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 hole
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. Literal 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. Literal a => a -> Term a
Lit Set a
s
                    , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (forall t. (HasSpec t, Sized t) => Term t -> Term Integer
sizeOf_ Term (Set a)
disjoint forall a. Num a => a -> a -> a
+ forall a. Literal 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 hole
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. Literal 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 (Set a
e :| [])
            | Set a
s forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set a
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 Set a
e Set a
s)
                      ( forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
                          (forall a. Set a -> [a]
Set.toList Set a
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 (Set a)
_ ->
            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 (Set a)
spec
                  ]
              )
  propagate Context "union_" SetW '[Set a, Set a] (Set a) hole
ctx Specification (Set a)
_ = forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Logic instance for UnionW   with wrong number of arguments. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Context "union_" SetW '[Set a, Set a] (Set a) hole
ctx)

  rewriteRules :: (TypeList '[Set a, Set a], Typeable '[Set a, Set a],
 HasSpec (Set a), All HasSpec '[Set a, Set a]) =>
SetW "union_" '[Set a, Set a] (Set a)
-> List Term '[Set a, Set a]
-> Evidence (AppRequires "union_" SetW '[Set a, Set a] (Set a))
-> Maybe (Term (Set a))
rewriteRules SetW "union_" '[Set a, Set a] (Set a)
UnionW (Term a
x :> Lit a
s :> List Term as1
Nil) Evidence (AppRequires "union_" SetW '[Set a, Set a] (Set a))
Evidence | forall (t :: * -> *) a. Foldable t => t a -> Bool
null a
s = forall a. a -> Maybe a
Just Term a
x
  rewriteRules SetW "union_" '[Set a, Set a] (Set a)
UnionW (Lit a
s :> Term a
x :> List Term as1
Nil) Evidence (AppRequires "union_" SetW '[Set a, Set a] (Set a))
Evidence | forall (t :: * -> *) a. Foldable t => t a -> Bool
null a
s = forall a. a -> Maybe a
Just Term a
x
  rewriteRules SetW "union_" '[Set a, Set a] (Set a)
_ List Term '[Set a, Set a]
_ Evidence (AppRequires "union_" SetW '[Set a, Set a] (Set a))
_ = forall a. Maybe a
Nothing

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 (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a.
(Literal a, Ord a) =>
SetW "union_" '[Set a, Set a] (Set a)
UnionW

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

instance (HasSpec a, Ord a) => Logic "disjoint_" SetW '[Set a, Set a] Bool where
  propagate :: forall hole.
Context "disjoint_" SetW '[Set a, Set a] Bool hole
-> Specification Bool -> Specification hole
propagate Context "disjoint_" SetW '[Set a, Set a] Bool hole
ctxt (ExplainSpec [String]
es Specification Bool
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "disjoint_" SetW '[Set a, Set a] Bool hole
ctxt Specification Bool
s
  propagate Context "disjoint_" SetW '[Set a, Set a] Bool hole
_ Specification Bool
TrueSpec = forall a. Specification a
TrueSpec
  propagate Context "disjoint_" SetW '[Set a, Set a] Bool hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context SetW "disjoint_" '[Set a, Set a] Bool
DisjointW (Ctx hole y
HOLE :<> a
x :<| CList 'Post as1 Any Any
End)) (SuspendedSpec Var Bool
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a.
(Literal a, Ord a) =>
SetW "disjoint_" '[Set a, Set a] Bool
DisjointW (Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall a. Literal a => a -> Term a
Lit a
x forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var Bool
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context SetW "disjoint_" '[Set a, Set a] Bool
DisjointW (a
x :|> Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (SuspendedSpec Var Bool
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a.
(Literal a, Ord a) =>
SetW "disjoint_" '[Set a, Set a] Bool
DisjointW (forall a. Literal a => a -> Term a
Lit a
x forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var Bool
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context SetW "disjoint_" '[Set a, Set a] Bool
DisjointW CList 'Pre '[Set a, Set a] hole y
ctx) Specification Bool
spec
    | (Ctx hole y
HOLE :<> (Set a
s :: Set a) :<| CList 'Post as1 Any Any
End) <- CList 'Pre '[Set a, Set a] hole y
ctx =
        forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole y.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole y -> Context s t dom rng hole
Context forall a.
(Literal a, Ord a) =>
SetW "disjoint_" '[Set a, Set a] Bool
DisjointW (Set a
s forall a (as1 :: [*]) hole y.
Literal a =>
a -> CList 'Pre as1 hole y -> CList 'Pre (a : as1) hole y
:|> forall hole. HasSpec hole => Ctx hole hole
HOLE forall y hole (as1 :: [*]).
HasSpec y =>
Ctx hole y
-> (forall i j. CList 'Post as1 i j) -> CList 'Pre (y : as1) hole y
:<> forall hole y. CList 'Post '[] hole y
End)) Specification Bool
spec
    | ((Set a
s :: Set a) :|> Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End) <- CList 'Pre '[Set a, Set a] hole y
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 Bool
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 hole
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 hole
set) Set a
s)) forall a b. (a -> b) -> a -> b
$ \Term a
e ->
            [ Term hole
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. Literal 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 hole
set
            ]
  propagate Context "disjoint_" SetW '[Set a, Set a] Bool hole
ctx Specification Bool
_ = forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Logic instance for DisjointW with wrong number of arguments. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Context "disjoint_" SetW '[Set a, Set a] Bool hole
ctx)

  rewriteRules :: (TypeList '[Set a, Set a], Typeable '[Set a, Set a], HasSpec Bool,
 All HasSpec '[Set a, Set a]) =>
SetW "disjoint_" '[Set a, Set a] Bool
-> List Term '[Set a, Set a]
-> Evidence (AppRequires "disjoint_" SetW '[Set a, Set a] Bool)
-> Maybe (Term Bool)
rewriteRules SetW "disjoint_" '[Set a, Set a] Bool
DisjointW (Lit a
s :> Term a
_ :> List Term as1
Nil) Evidence (AppRequires "disjoint_" SetW '[Set a, Set a] Bool)
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. Literal a => a -> Term a
Lit Bool
True
  rewriteRules SetW "disjoint_" '[Set a, Set a] Bool
DisjointW (Term a
_ :> Lit a
s :> List Term as1
Nil) Evidence (AppRequires "disjoint_" SetW '[Set a, Set a] Bool)
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. Literal a => a -> Term a
Lit Bool
True
  rewriteRules SetW "disjoint_" '[Set a, Set a] Bool
_ List Term '[Set a, Set a]
_ Evidence (AppRequires "disjoint_" SetW '[Set a, Set a] Bool)
_ = forall a. Maybe a
Nothing

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 (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a.
(Literal a, Ord a) =>
SetW "disjoint_" '[Set a, Set a] Bool
DisjointW

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

instance (HasSpec a, Ord a) => Logic "fromList_" SetW '[[a]] (Set a) where
  propagate :: forall hole.
Context "fromList_" SetW '[[a]] (Set a) hole
-> Specification (Set a) -> Specification hole
propagate Context "fromList_" SetW '[[a]] (Set a) hole
ctxt (ExplainSpec [String]
es Specification (Set a)
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "fromList_" SetW '[[a]] (Set a) hole
ctxt Specification (Set a)
s
  propagate Context "fromList_" SetW '[[a]] (Set a) hole
_ Specification (Set a)
TrueSpec = forall a. Specification a
TrueSpec
  propagate Context "fromList_" SetW '[[a]] (Set a) hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context SetW "fromList_" '[[a]] (Set a)
FromListW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (SuspendedSpec Var (Set a)
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a. (HasSpec a, Ord a) => SetW "fromList_" '[[a]] (Set a)
FromListW (Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var (Set a)
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context SetW "fromList_" '[[a]] (Set a)
FromListW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) Specification (Set a)
spec
    | Evidence (Prerequisites [a])
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @[a] =
        case Specification (Set a)
spec of
          MemberSpec (Set a
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 Set a
xs)
                forall a. Specification a
TrueSpec
                ( forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
                    (forall a. Set a -> [a]
Set.toList Set a
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 (Set a)
_ ->
            -- 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 hole
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 hole
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 (Set a)
spec
                , Term hole
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 hole
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 hole
xs
                ]
  propagate Context "fromList_" SetW '[[a]] (Set a) hole
ctx Specification (Set a)
_ = forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Logic instance for FromListW with wrong number of arguments. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Context "fromList_" SetW '[[a]] (Set a) hole
ctx)

  mapTypeSpec :: forall a b.
('[[a]] ~ '[a], Set a ~ b, HasSpec a, HasSpec b) =>
SetW "fromList_" '[a] b -> TypeSpec a -> Specification b
mapTypeSpec SetW "fromList_" '[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

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 (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. (HasSpec a, Ord a) => SetW "fromList_" '[[a]] (Set a)
FromListW