{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# 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 UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans -Wno-name-shadowing #-}

module Constrained.Spec.Set where

import Constrained.AbstractSyntax
import Constrained.Base (
  Forallable (..),
  HOLE (..),
  HasSpec (..),
  Logic (..),
  Specification,
  Term,
  appTerm,
  constrained,
  equalSpec,
  explainSpec,
  fromListCtx,
  isErrorLike,
  memberSpecList,
  notEqualSpec,
  notMemberSpec,
  typeSpec,
  pattern TypeSpec,
  pattern Unary,
 )
import Constrained.Conformance (
  conformsToSpec,
  satisfies,
 )
import Constrained.Core
import Constrained.FunctionSymbol
import Constrained.GenT
import Constrained.List
import Constrained.NumOrd
import Constrained.PrettyUtils
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 = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> (Set a -> Int) -> Set a -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> Int
forall a. Set a -> Int
Set.size
  liftSizeSpec :: HasSpec (Set a) => SizeSpec -> [Integer] -> Specification (Set a)
liftSizeSpec SizeSpec
spec [Integer]
cant = TypeSpec (Set a) -> Specification (Set a)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Set a -> Specification a -> Specification Integer -> SetSpec a
forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec Set a
forall a. Monoid a => a
mempty Specification a
forall deps a. SpecificationD deps a
TrueSpec (TypeSpec Integer -> [Integer] -> Specification Integer
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec Integer
SizeSpec
spec [Integer]
cant))
  liftMemberSpec :: HasSpec (Set a) => [Integer] -> Specification (Set a)
liftMemberSpec [Integer]
xs = case [Integer] -> Maybe (NonEmpty Integer)
forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty [Integer]
xs of
    Maybe (NonEmpty Integer)
Nothing -> NonEmpty String -> Specification (Set a)
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (String -> NonEmpty String
forall a. a -> NonEmpty a
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 -> TypeSpec (Set a) -> Specification (Set a)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Set a -> Specification a -> Specification Integer -> SetSpec a
forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec Set a
forall a. Monoid a => a
mempty Specification a
forall deps a. SpecificationD deps a
TrueSpec (NonEmpty Integer -> Specification Integer
forall a deps. NonEmpty a -> SpecificationD deps 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 Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
geqSpec (Set a -> Integer
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' =
    Set a -> Specification a -> Specification Integer -> SetSpec a
forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec (Set a
must Set a -> Set a -> Set a
forall a. Semigroup a => a -> a -> a
<> Set a
must') (Specification a
es Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> Specification a
es') (Specification Integer
size Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Specification Integer
size')

instance (Ord a, HasSpec a) => Monoid (SetSpec a) where
  mempty :: SetSpec a
mempty = Set a -> Specification a -> Specification Integer -> SetSpec a
forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec Set a
forall a. Monoid a => a
mempty Specification a
forall a. Monoid a => a
mempty Specification Integer
forall deps a. SpecificationD deps 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) = TypeSpec (Set a) -> Specification (Set a)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec (Set a) -> Specification (Set a))
-> TypeSpec (Set a) -> Specification (Set a)
forall a b. (a -> b) -> a -> b
$ Set a -> Specification a -> Specification Integer -> SetSpec a
forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec Set a
forall a. Monoid a => a
mempty Specification a
e Specification Integer
forall deps a. SpecificationD deps a
TrueSpec
  forAllToList :: Set a -> [a]
forAllToList = Set a -> [a]
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) =
  Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens
    ( Doc ann
"SetSpec"
        Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
/> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
sep [Doc ann
"must=" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> [a] -> Doc ann
forall a x. (Show a, Typeable a) => [a] -> Doc x
short (Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
must), Doc ann
"elem=" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Specification a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification a -> Doc ann
pretty Specification a
elemS, Doc ann
"size=" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Specification Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification Integer -> Doc ann
pretty Specification Integer
size]
    )

instance HasSpec a => Show (SetSpec a) where
  show :: SetSpec a -> String
show SetSpec a
x = Doc Any -> String
forall a. Show a => a -> String
show (SetSpec a -> Doc Any
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 = Set a -> Specification a -> Specification Integer -> SetSpec a
forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec (Set a -> Specification a -> Specification Integer -> SetSpec a)
-> Gen (Set a)
-> Gen (Specification a -> Specification Integer -> SetSpec a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Set a)
forall a. Arbitrary a => Gen a
arbitrary Gen (Specification a -> Specification Integer -> SetSpec a)
-> Gen (Specification a)
-> Gen (Specification Integer -> SetSpec a)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Specification a)
forall a. Arbitrary a => Gen a
arbitrary Gen (Specification Integer -> SetSpec a)
-> Gen (Specification Integer) -> Gen (SetSpec a)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Specification Integer)
forall a. Arbitrary a => Gen a
arbitrary
  shrink :: SetSpec a -> [SetSpec a]
shrink (SetSpec Set a
a Specification a
b Specification Integer
c) = [Set a -> Specification a -> Specification Integer -> SetSpec a
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') <- (Set a, Specification a, Specification Integer)
-> [(Set a, Specification a, Specification Integer)]
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 = FoldSpec (Set a) -> Gen (FoldSpec (Set a))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FoldSpec (Set a)
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 ((Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
geqSpec Integer
0) -> Specification Integer
size))
  | Just Integer
u <- Specification Integer -> Maybe Integer
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification Integer
size
  , Integer
u Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 =
      NonEmpty String -> SpecificationD Deps (Set a)
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec ((String
"guardSetSpec: negative size " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
u) String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [String]
es)
  | Bool -> Bool
not ((a -> Bool) -> Set a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
elemS) Set a
must) =
      NonEmpty String -> SpecificationD Deps (Set a)
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec ((String
"Some 'must' items do not conform to 'element' spec: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification a -> String
forall a. Show a => a -> String
show Specification a
elemS) String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [String]
es)
  | Specification Integer -> Bool
forall a. Specification a -> Bool
isErrorLike Specification Integer
size = NonEmpty String -> SpecificationD Deps (Set a)
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (String
"guardSetSpec: error in size" String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [String]
es)
  | Specification Integer -> Bool
forall a. Specification a -> Bool
isErrorLike (Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
geqSpec (Set a -> Integer
forall t. Sized t => t -> Integer
sizeOf Set a
must) Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Specification Integer
size) =
      NonEmpty String -> SpecificationD Deps (Set a)
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (NonEmpty String -> SpecificationD Deps (Set a))
-> NonEmpty String -> SpecificationD Deps (Set a)
forall a b. (a -> b) -> a -> b
$
        (String
"Must set size " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Set a -> Integer
forall t. Sized t => t -> Integer
sizeOf Set a
must) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", is inconsistent with SetSpec size" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification Integer -> String
forall a. Show a => a -> String
show Specification Integer
size) String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [String]
es
  | Specification Integer -> Bool
forall a. Specification a -> Bool
isErrorLike (Specification Integer -> Specification Integer
maxSpec (Specification a -> Specification Integer
forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality Specification a
elemS) Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Specification Integer
size) =
      NonEmpty String -> SpecificationD Deps (Set a)
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (NonEmpty String -> SpecificationD Deps (Set a))
-> NonEmpty String -> SpecificationD Deps (Set a)
forall a b. (a -> b) -> a -> b
$
        [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList ([String] -> NonEmpty String) -> [String] -> NonEmpty String
forall a b. (a -> b) -> a -> b
$
          [ String
"Cardinality of SetSpec elemSpec (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification a -> String
forall a. Show a => a -> String
show Specification a
elemS String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification Integer -> String
forall a. Show a => a -> String
show (Specification Integer -> Specification Integer
maxSpec (Specification a -> Specification Integer
forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality Specification a
elemS))
          , String
"   This is inconsistent with SetSpec size (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification Integer -> String
forall a. Show a => a -> String
show Specification Integer
size String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
          ]
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
es
  | Bool
otherwise = TypeSpec (Set a) -> SpecificationD Deps (Set a)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Set a -> Specification a -> Specification Integer -> SetSpec a
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 = TypeSpec (Set a)
SetSpec a
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' = [String] -> SetSpec a -> Specification (Set a)
forall a.
(HasSpec a, Ord a) =>
[String] -> SetSpec a -> Specification (Set a)
guardSetSpec [String
"While combining 2 SetSpecs", String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SetSpec a -> String
forall a. Show a => a -> String
show TypeSpec (Set a)
SetSpec a
s, String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SetSpec a -> String
forall a. Show a => a -> String
show TypeSpec (Set a)
SetSpec a
s'] (TypeSpec (Set a)
SetSpec a
s SetSpec a -> SetSpec a -> SetSpec a
forall a. Semigroup a => a -> a -> a
<> TypeSpec (Set a)
SetSpec a
s')

  conformsTo :: HasCallStack => Set a -> TypeSpec (Set a) -> Bool
conformsTo Set a
s (SetSpec Set a
must Specification a
es Specification Integer
size) =
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      [ Set a -> Integer
forall t. Sized t => t -> Integer
sizeOf Set a
s Integer -> Specification Integer -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification Integer
size
      , Set a
must Set a -> Set a -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set a
s
      , (a -> Bool) -> Set a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a -> Specification a -> Bool
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
_)
    | (a -> Bool) -> Set a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
e)) Set a
must =
        NonEmpty String -> GenT m (Set a)
forall a. HasCallStack => NonEmpty String -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
genErrorNE
          ( [String] -> NonEmpty String
forall a. HasCallStack => [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 ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\a
x -> String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
x) ((a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
e)) (Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
must)))
              , String
"Element Specifcation"
              , String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification a -> String
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) =
    TypeSpec (Set a) -> GenT m (Set a)
forall a (m :: * -> *).
(HasSpec a, HasCallStack, MonadGenError m) =>
TypeSpec a -> GenT m a
forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec (Set a) -> GenT m (Set a)
genFromTypeSpec (Set a -> Specification a -> Specification Integer -> SetSpec a
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) =
    NonEmpty String -> GenT m (Set a) -> GenT m (Set a)
forall a. HasCallStack => NonEmpty String -> GenT m a -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE (String
e String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [String]
es) (GenT m (Set a) -> GenT m (Set a))
-> GenT m (Set a) -> GenT m (Set a)
forall a b. (a -> b) -> a -> b
$ TypeSpec (Set a) -> GenT m (Set a)
forall a (m :: * -> *).
(HasSpec a, HasCallStack, MonadGenError m) =>
TypeSpec a -> GenT m a
forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec (Set a) -> GenT m (Set a)
genFromTypeSpec (Set a -> Specification a -> Specification Integer -> SetSpec a
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 Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
geqSpec (Set a -> Integer
forall t. Sized t => t -> Integer
sizeOf Set a
must) Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Specification Integer -> Specification Integer
maxSpec (Specification a -> Specification Integer
forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality Specification a
elemS)
    [a]
choices <- Gen [a] -> GenT m [a]
forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen (Gen [a] -> GenT m [a]) -> Gen [a] -> GenT m [a]
forall a b. (a -> b) -> a -> b
$ [a] -> Gen [a]
forall a. [a] -> Gen [a]
shuffle (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
xs [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
\\ Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
must)
    Int
size <- Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> GenT m Integer -> GenT m Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Specification Integer -> GenT m Integer
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification Integer
szSpec'
    let additions :: Set a
additions = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList ([a] -> Set a) -> [a] -> Set a
forall a b. (a -> b) -> a -> b
$ Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take (Int
size Int -> Int -> Int
forall a. Num a => a -> a -> a
- Set a -> Int
forall a. Set a -> Int
Set.size Set a
must) [a]
choices
    Set a -> GenT m (Set a)
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set a -> Set a -> Set a
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 Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
geqSpec (Set a -> Integer
forall t. Sized t => t -> Integer
sizeOf Set a
must) Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Specification Integer -> Specification Integer
maxSpec (Specification a -> Specification Integer
forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality Specification a
elemS)
    Integer
count <-
      String -> GenT m Integer -> GenT m Integer
forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain String
"Choose a size for the Set to be generated" (GenT m Integer -> GenT m Integer)
-> GenT m Integer -> GenT m Integer
forall a b. (a -> b) -> a -> b
$
        Specification Integer -> GenT m Integer
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification Integer
szSpec'
    let targetSize :: Integer
targetSize = Integer
count Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Set a -> Integer
forall t. Sized t => t -> Integer
sizeOf Set a
must
    NonEmpty String -> GenT m (Set a) -> GenT m (Set a)
forall a. HasCallStack => NonEmpty String -> GenT m a -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
      ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
          [ String
"Choose size count = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
count
          , String
"szSpec' = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification Integer -> String
forall a. Show a => a -> String
show Specification Integer
szSpec'
          , String
"Picking items not in must = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show ([a] -> Doc Any
forall a x. (Show a, Typeable a) => [a] -> Doc x
short (Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
must))
          , String
"that also meet the element test: "
          , String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification a -> String
forall a. Show a => a -> String
show Specification a
elemS
          ]
      )
      (GenT m (Set a) -> GenT m (Set a))
-> GenT m (Set a) -> GenT m (Set a)
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 Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
n Integer
targetSize of
          Ordering
LT -> String -> GenT m (Set a)
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 = Integer -> Specification Integer -> Integer
forall n.
(Ord n, Complete n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
maxFromSpec Integer
0 (Specification a -> Specification Integer
forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality (Specification a -> Specification a
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0 = Set a -> GenT m (Set a)
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Set a
s
      go Int
tries Integer
n Set a
s = do
        a
e <-
          NonEmpty String -> GenT m a -> GenT m a
forall a. HasCallStack => NonEmpty String -> GenT m a -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
            ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
                [ String
"Generate set member at type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ forall t. Typeable t => String
forall {k} (t :: k). Typeable t => String
showType @a
                , String
"  number of items starting with  = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Set a -> Int
forall a. Set a -> Int
Set.size Set a
must)
                , String
"  number of items left to pick   = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
                , String
"  number of items already picked = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Set a -> Int
forall a. Set a -> Int
Set.size Set a
s)
                , String
"  the most items we can expect is " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
theMostWeCanExpect String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (a SuspendedSpec)"
                ]
            )
            (GenT m a -> GenT m a) -> GenT m a -> GenT m a
forall a b. (a -> b) -> a -> b
$ GenMode -> GenT m a -> GenT m a
forall (m :: * -> *) a. GenMode -> GenT m a -> GenT m a
withMode GenMode
Strict
            (GenT m a -> GenT m a) -> GenT m a -> GenT m a
forall a b. (a -> b) -> a -> b
$ Int -> GenT m a -> (a -> Bool) -> GenT m a
forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
Int -> GenT m a -> (a -> Bool) -> GenT m a
suchThatWithTryT Int
tries (Specification a -> GenT m a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
elemS) (a -> Set a -> Bool
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 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) (a -> Set a -> Set a
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 <- Specification Integer -> Maybe Integer
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound (Specification a -> Specification Integer
forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality Specification a
es) = Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
leqSpec (Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
ub)
  cardinalTypeSpec TypeSpec (Set a)
_ = Specification Integer
forall deps a. SpecificationD deps a
TrueSpec

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

  shrinkWithTypeSpec :: TypeSpec (Set a) -> Set a -> [Set a]
shrinkWithTypeSpec (SetSpec Set a
_ Specification a
es Specification Integer
_) Set a
as = ([a] -> Set a) -> [[a]] -> [Set a]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList ([[a]] -> [Set a]) -> [[a]] -> [Set a]
forall a b. (a -> b) -> a -> b
$ (a -> [a]) -> [a] -> [[a]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList (Specification a -> a -> [a]
forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification a
es) (Set a -> [a]
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) =
    [Pred] -> Pred
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold ([Pred] -> Pred) -> [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$
      -- Don't include this if the must set is empty
      [ NonEmpty String -> Pred -> Pred
forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set a -> String
forall a. Show a => a -> String
show Set a
m String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is a subset of the set.")) (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (TermD Deps Bool -> Pred) -> TermD Deps Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set a) -> Term (Set a) -> TermD Deps Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> TermD Deps Bool
subset_ (Set a -> Term (Set a)
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit Set a
m) Term (Set a)
s
      | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
m
      ]
        [Pred] -> [Pred] -> [Pred]
forall a. [a] -> [a] -> [a]
++ [ Term (Set a) -> (Term a -> Pred) -> Pred
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 -> Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term a
e Specification a
es)
           , Term Integer -> Specification Integer -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term (Set a) -> Term Integer
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 = [String] -> TypeSpec (Set a) -> Specification (Set a)
[String] -> SetSpec a -> Specification (Set a)
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 = FunTy ds r
a -> Set a
forall a. a -> Set a
Set.singleton
setSem SetW ds r
UnionW = FunTy ds r
Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union
setSem SetW ds r
SubsetW = FunTy ds r
Set a -> Set a -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf
setSem SetW ds r
MemberW = FunTy ds r
a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member
setSem SetW ds r
DisjointW = FunTy ds r
Set a -> Set a -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint
setSem SetW ds r
FromListW = FunTy ds r
[a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList

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

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