Safe Haskell	Safe-Inferred
Language	Haskell2010

Constrained.Spec.ListFoldy

Contents

Orphan instances

Description

Code for the Foldy class, the FunW witness (compose_,id_,flip_) and HasSpec instance for List. These things are all mutually recursive.

Synopsis

data FunW (sym ∷ Symbol) (dom ∷ [Type]) (rng ∷ Type) where
- IdW ∷ ∀ a. FunW "id_" '[a] a
- ComposeW ∷ ∀ b s1 s2 t1 t2 a r. (Logic s1 t1 '[b] r, Logic s2 t2 '[a] b, HasSpec b) ⇒ t1 s1 '[b] r → t2 s2 '[a] b → FunW "composeFn" '[a] r
- FlipW ∷ ∀ sym t a b r. Logic sym t '[a, b] r ⇒ t sym '[a, b] r → FunW "flip_" '[b, a] r
funSem ∷ FunW sym dom rng → FunTy dom rng
compareWit ∷ ∀ s1 t1 bs1 r1 s2 t2 bs2 r2. (Logic s1 t1 bs1 r1, Logic s2 t2 bs2 r2) ⇒ t1 s1 bs1 r1 → t2 s2 bs2 r2 → Bool
id_ ∷ ∀ a. HasSpec a ⇒ Term a → Term a
flip_ ∷ ∀ (t ∷ FSType) (sym ∷ Symbol) a b r. (HasSpec b, HasSpec a, HasSpec r, ∀ sym1 t1. Logic sym1 t1 '[a, b] r) ⇒ t sym '[a, b] r → Term b → Term a → Term r
compose_ ∷ ∀ b s1 s2 t1 t2 a r. (AppRequires s1 t1 '[b] r, AppRequires s2 t2 '[a] b) ⇒ t1 s1 '[b] r → t2 s2 '[a] b → Term a → Term r
composeFn ∷ (HasSpec b, HasSpec a, HasSpec c) ⇒ Fun '[b] c → Fun '[a] b → Fun '[a] c
idFn ∷ HasSpec a ⇒ Fun '[a] a
class (HasSpec a, NumLike a, Logic "addFn" IntW '[a, a] a) ⇒ Foldy a where
- genList ∷ MonadGenError m ⇒ Specification a → Specification a → GenT m [a]
- theAddFn ∷ IntW "addFn" '[a, a] a
- theZero ∷ a
- genSizedList ∷ MonadGenError m ⇒ Specification Integer → Specification a → Specification a → GenT m [a]
- noNegativeValues ∷ Bool
genInverse ∷ (MonadGenError m, HasSpec a, HasSpec b) ⇒ Fun '[a] b → Specification a → b → GenT m a
genFromFold ∷ ∀ m a b. (MonadGenError m, Foldy b, HasSpec a) ⇒ [a] → Specification Integer → Specification a → Fun '[a] b → Specification b → GenT m [a]
adds ∷ Foldy a ⇒ [a] → a
addFun ∷ NumLike n ⇒ Fun '[n, n] n
data FoldSpec a where
- NoFold ∷ FoldSpec a
- FoldSpec ∷ ∀ b a. (HasSpec a, HasSpec b, Foldy b) ⇒ Fun '[a] b → Specification b → FoldSpec a
preMapFoldSpec ∷ HasSpec a ⇒ Fun '[a] b → FoldSpec b → FoldSpec a
combineFoldSpec ∷ FoldSpec a → FoldSpec a → Either [String] (FoldSpec a)
conformsToFoldSpec ∷ ∀ a. [a] → FoldSpec a → Bool
data ListW (s ∷ Symbol) (args ∷ [Type]) (res ∷ Type) where
- FoldMapW ∷ ∀ a b. (Foldy b, HasSpec a) ⇒ Fun '[a] b → ListW "foldMap_" '[[a]] b
- SingletonListW ∷ ListW "singeltonList_" '[a] [a]
- AppendW ∷ (Typeable a, Show a) ⇒ ListW "append_" '[[a], [a]] [a]
listSem ∷ ListW s dom rng → FunTy dom rng
foldMap_ ∷ ∀ a b. (Sized [a], Foldy b, HasSpec a) ⇒ (Term a → Term b) → Term [a] → Term b
sum_ ∷ Foldy a ⇒ Term [a] → Term a
foldMapFn ∷ ∀ a b. (HasSpec a, Foldy b) ⇒ Fun '[a] b → Fun '[[a]] b
toPredsFoldSpec ∷ (HasSpec a, HasSpec [a]) ⇒ Term [a] → FoldSpec a → Pred
elem_ ∷ (Sized [a], HasSpec a) ⇒ Term a → Term [a] → Term Bool
elemFn ∷ HasSpec a ⇒ Fun '[a, [a]] Bool
reverseFoldSpec ∷ FoldSpec a → Specification a
singletonList_ ∷ (Sized [a], HasSpec a) ⇒ Term a → Term [a]
singletonListFn ∷ ∀ a. HasSpec a ⇒ Fun '[a] [a]
prefixedBy ∷ Eq a ⇒ [a] → [[a]] → [[a]]
suffixedBy ∷ Eq a ⇒ [a] → [[a]] → [[a]]
alreadyHave ∷ Eq a ⇒ [a] → ListSpec a → ListSpec a
alreadyHaveFold ∷ [a] → FoldSpec a → FoldSpec a
appendFn ∷ ∀ a. (Sized [a], HasSpec a) ⇒ Fun '[[a], [a]] [a]
append_ ∷ (Sized [a], HasSpec a) ⇒ Term [a] → Term [a] → Term [a]
data ListSpec a = ListSpec {
- listSpecHint ∷ Maybe Integer
- listSpecMust ∷ [a]
- listSpecSize ∷ Specification Integer
- listSpecElem ∷ Specification a
- listSpecFold ∷ FoldSpec a
}
guardListSpec ∷ HasSpec a ⇒ [String] → ListSpec a → Specification [a]
knownUpperBound ∷ (TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) ⇒ Specification a → Maybe a
knownLowerBound ∷ (TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) ⇒ Specification a → Maybe a
isEmptyNumSpec ∷ (TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) ⇒ Specification a → Bool
enumerateInterval ∷ (Enum a, Num a, MaybeBounded a) ⇒ NumSpec a → [a]
genNumList ∷ ∀ a m. (MonadGenError m, Arbitrary a, Integral a, MaybeBounded a, TypeSpec a ~ NumSpec a, Foldy a, Random a) ⇒ Specification a → Specification a → GenT m [a]
narrowByFuelAndSize ∷ ∀ a. (TypeSpec a ~ NumSpec a, HasSpec a, Arbitrary a, Integral a, Random a, MaybeBounded a) ⇒ a → Int → (Specification a, Specification a) → (Specification a, Specification a)
narrowFoldSpecs ∷ ∀ a. (TypeSpec a ~ NumSpec a, HasSpec a, Arbitrary a, Integral a, Random a, MaybeBounded a) ⇒ (Specification a, Specification a) → (Specification a, Specification a)
genListWithSize ∷ ∀ a m. (Foldy a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a, Integral a) ⇒ Specification Integer → Specification a → Specification a → GenT m [a]
pickPositive ∷ ∀ t m. (Integral t, Random t, MonadGenError m, TypeSpec t ~ NumSpec t, Foldy t) ⇒ Specification t → t → Integer → GenT m [t]
pickNegative ∷ ∀ t m. (Integral t, Random t, MonadGenError m, TypeSpec t ~ NumSpec t, HasSpec t) ⇒ Specification t → t → Integer → GenT m [t]
specName ∷ ∀ a. HasSpec a ⇒ Specification a → String
predSpecPair ∷ ∀ a. HasSpec a ⇒ Specification a → (String, a → Bool)
minFromSpec ∷ ∀ n. (Ord n, TypeSpec n ~ NumSpec n) ⇒ n → Specification n → n
maxFromSpec ∷ ∀ n. (Ord n, TypeSpec n ~ NumSpec n) ⇒ n → Specification n → n

Documentation

data FunW (sym ∷ Symbol) (dom ∷ [Type]) (rng ∷ Type) where Source #

Constructors

IdW ∷ ∀ a. FunW "id_" '[a] a
ComposeW ∷ ∀ b s1 s2 t1 t2 a r. (Logic s1 t1 '[b] r, Logic s2 t2 '[a] b, HasSpec b) ⇒ t1 s1 '[b] r → t2 s2 '[a] b → FunW "composeFn" '[a] r
FlipW ∷ ∀ sym t a b r. Logic sym t '[a, b] r ⇒ t sym '[a, b] r → FunW "flip_" '[b, a] r

Instances

Instances details

Semantics FunW Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods semantics ∷ ∀ (s ∷ Symbol) (d ∷ [Type]) r. FunW s d r → FunTy d r Source #
Syntax FunW Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods isInFix ∷ ∀ (s ∷ Symbol) (dom ∷ [Type]) rng. FunW s dom rng → Bool Source # prettyWit ∷ ∀ (s ∷ Symbol) (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ FunW s dom rng → List Term dom → Int → Maybe (Doc ann) Source #
(All (Typeable ∷ Type → Constraint) '[a, r], HasSpec r) ⇒ Logic "composeFn" FunW '[a] r Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods info ∷ FunW "composeFn" '[a] r → String Source # propagate ∷ Context "composeFn" FunW '[a] r hole → Specification r → Specification hole Source # rewriteRules ∷ FunW "composeFn" '[a] r → List Term '[a] → Evidence (AppRequires "composeFn" FunW '[a] r) → Maybe (Term r) Source # mapTypeSpec ∷ ('[a] ~ '[a0], r ~ b, HasSpec a0, HasSpec b) ⇒ FunW "composeFn" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ FunW "composeFn" '[a] Bool → List Term '[a] → [Pred] Source #
(∀ (sym ∷ Symbol) (t ∷ Symbol → [Type] → Type → Type). Logic sym t '[a, b] r, All (Typeable ∷ Type → Constraint) '[a, b, r]) ⇒ Logic "flip_" FunW '[b, a] r Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods info ∷ FunW "flip_" '[b, a] r → String Source # propagate ∷ Context "flip_" FunW '[b, a] r hole → Specification r → Specification hole Source # rewriteRules ∷ FunW "flip_" '[b, a] r → List Term '[b, a] → Evidence (AppRequires "flip_" FunW '[b, a] r) → Maybe (Term r) Source # mapTypeSpec ∷ ('[b, a] ~ '[a0], r ~ b0, HasSpec a0, HasSpec b0) ⇒ FunW "flip_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ FunW "flip_" '[b, a] Bool → List Term '[b, a] → [Pred] Source #
HasSpec a ⇒ Logic "id_" FunW '[a] a Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods info ∷ FunW "id_" '[a] a → String Source # propagate ∷ Context "id_" FunW '[a] a hole → Specification a → Specification hole Source # rewriteRules ∷ FunW "id_" '[a] a → List Term '[a] → Evidence (AppRequires "id_" FunW '[a] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[a] ~ '[a0], a ~ b, HasSpec a0, HasSpec b) ⇒ FunW "id_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ FunW "id_" '[a] Bool → List Term '[a] → [Pred] Source #
KnownSymbol s ⇒ Show (FunW s dom rng) Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods showsPrec ∷ Int → FunW s dom rng → ShowS show ∷ FunW s dom rng → String showList ∷ [FunW s dom rng] → ShowS
Eq (FunW s dom rng) Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods (==) ∷ FunW s dom rng → FunW s dom rng → Bool (/=) ∷ FunW s dom rng → FunW s dom rng → Bool

funSem ∷ FunW sym dom rng → FunTy dom rng Source #

compareWit ∷ ∀ s1 t1 bs1 r1 s2 t2 bs2 r2. (Logic s1 t1 bs1 r1, Logic s2 t2 bs2 r2) ⇒ t1 s1 bs1 r1 → t2 s2 bs2 r2 → Bool Source #

id_ ∷ ∀ a. HasSpec a ⇒ Term a → Term a Source #

flip_ ∷ ∀ (t ∷ FSType) (sym ∷ Symbol) a b r. (HasSpec b, HasSpec a, HasSpec r, ∀ sym1 t1. Logic sym1 t1 '[a, b] r) ⇒ t sym '[a, b] r → Term b → Term a → Term r Source #

compose_ ∷ ∀ b s1 s2 t1 t2 a r. (AppRequires s1 t1 '[b] r, AppRequires s2 t2 '[a] b) ⇒ t1 s1 '[b] r → t2 s2 '[a] b → Term a → Term r Source #

composeFn ∷ (HasSpec b, HasSpec a, HasSpec c) ⇒ Fun '[b] c → Fun '[a] b → Fun '[a] c Source #

idFn ∷ HasSpec a ⇒ Fun '[a] a Source #

class (HasSpec a, NumLike a, Logic "addFn" IntW '[a, a] a) ⇒ Foldy a where Source #

Minimal complete definition

genList, genSizedList, noNegativeValues

Methods

genList ∷ MonadGenError m ⇒ Specification a → Specification a → GenT m [a] Source #

theAddFn ∷ IntW "addFn" '[a, a] a Source #

theZero ∷ a Source #

genSizedList ∷ MonadGenError m ⇒ Specification Integer → Specification a → Specification a → GenT m [a] Source #

noNegativeValues ∷ Bool Source #

Instances

Instances details

Foldy Int16 Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Int16 → Specification Int16 → GenT m [Int16] Source # theAddFn ∷ IntW "addFn" '[Int16, Int16] Int16 Source # theZero ∷ Int16 Source # genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Int16 → Specification Int16 → GenT m [Int16] Source # noNegativeValues ∷ Bool Source #
Foldy Int32 Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Int32 → Specification Int32 → GenT m [Int32] Source # theAddFn ∷ IntW "addFn" '[Int32, Int32] Int32 Source # theZero ∷ Int32 Source # genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Int32 → Specification Int32 → GenT m [Int32] Source # noNegativeValues ∷ Bool Source #
Foldy Int64 Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Int64 → Specification Int64 → GenT m [Int64] Source # theAddFn ∷ IntW "addFn" '[Int64, Int64] Int64 Source # theZero ∷ Int64 Source # genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Int64 → Specification Int64 → GenT m [Int64] Source # noNegativeValues ∷ Bool Source #
Foldy Int8 Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Int8 → Specification Int8 → GenT m [Int8] Source # theAddFn ∷ IntW "addFn" '[Int8, Int8] Int8 Source # theZero ∷ Int8 Source # genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Int8 → Specification Int8 → GenT m [Int8] Source # noNegativeValues ∷ Bool Source #
Foldy Word16 Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Word16 → Specification Word16 → GenT m [Word16] Source # theAddFn ∷ IntW "addFn" '[Word16, Word16] Word16 Source # theZero ∷ Word16 Source # genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Word16 → Specification Word16 → GenT m [Word16] Source # noNegativeValues ∷ Bool Source #
Foldy Word32 Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Word32 → Specification Word32 → GenT m [Word32] Source # theAddFn ∷ IntW "addFn" '[Word32, Word32] Word32 Source # theZero ∷ Word32 Source # genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Word32 → Specification Word32 → GenT m [Word32] Source # noNegativeValues ∷ Bool Source #
Foldy Word64 Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Word64 → Specification Word64 → GenT m [Word64] Source # theAddFn ∷ IntW "addFn" '[Word64, Word64] Word64 Source # theZero ∷ Word64 Source # genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Word64 → Specification Word64 → GenT m [Word64] Source # noNegativeValues ∷ Bool Source #
Foldy Word8 Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Word8 → Specification Word8 → GenT m [Word8] Source # theAddFn ∷ IntW "addFn" '[Word8, Word8] Word8 Source # theZero ∷ Word8 Source # genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Word8 → Specification Word8 → GenT m [Word8] Source # noNegativeValues ∷ Bool Source #
Foldy Integer Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Integer → GenT m [Integer] Source # theAddFn ∷ IntW "addFn" '[Integer, Integer] Integer Source # theZero ∷ Integer Source # genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Integer → Specification Integer → GenT m [Integer] Source # noNegativeValues ∷ Bool Source #
Foldy Natural Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Natural → Specification Natural → GenT m [Natural] Source # theAddFn ∷ IntW "addFn" '[Natural, Natural] Natural Source # theZero ∷ Natural Source # genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Natural → Specification Natural → GenT m [Natural] Source # noNegativeValues ∷ Bool Source #
Foldy Int Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Int → Specification Int → GenT m [Int] Source # theAddFn ∷ IntW "addFn" '[Int, Int] Int Source # theZero ∷ Int Source # genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Int → Specification Int → GenT m [Int] Source # noNegativeValues ∷ Bool Source #

genInverse ∷ (MonadGenError m, HasSpec a, HasSpec b) ⇒ Fun '[a] b → Specification a → b → GenT m a Source #

genFromFold ∷ ∀ m a b. (MonadGenError m, Foldy b, HasSpec a) ⇒ [a] → Specification Integer → Specification a → Fun '[a] b → Specification b → GenT m [a] Source #

adds ∷ Foldy a ⇒ [a] → a Source #

addFun ∷ NumLike n ⇒ Fun '[n, n] n Source #

data FoldSpec a where Source #

Constructors

NoFold ∷ FoldSpec a
FoldSpec ∷ ∀ b a. (HasSpec a, HasSpec b, Foldy b) ⇒ Fun '[a] b → Specification b → FoldSpec a

Instances

Instances details

Arbitrary (FoldSpec (Map k v)) Source #
Instance details Defined in Constrained.Spec.Map Methods arbitrary ∷ Gen (FoldSpec (Map k v)) Source # shrink ∷ FoldSpec (Map k v) → [FoldSpec (Map k v)] Source #
Arbitrary (FoldSpec (Set a)) Source #
Instance details Defined in Constrained.Spec.Set Methods arbitrary ∷ Gen (FoldSpec (Set a)) Source # shrink ∷ FoldSpec (Set a) → [FoldSpec (Set a)] Source #
(HasSpec a, HasSpec b, Arbitrary (FoldSpec a), Arbitrary (FoldSpec b)) ⇒ Arbitrary (FoldSpec (a, b)) Source #
Instance details Defined in Constrained.Spec.SumProd Methods arbitrary ∷ Gen (FoldSpec (a, b)) Source # shrink ∷ FoldSpec (a, b) → [FoldSpec (a, b)] Source #
(Arbitrary (Specification a), Foldy a) ⇒ Arbitrary (FoldSpec a) Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods arbitrary ∷ Gen (FoldSpec a) Source # shrink ∷ FoldSpec a → [FoldSpec a] Source #
HasSpec a ⇒ Show (FoldSpec a) Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods showsPrec ∷ Int → FoldSpec a → ShowS show ∷ FoldSpec a → String showList ∷ [FoldSpec a] → ShowS
HasSpec a ⇒ Pretty (WithPrec (FoldSpec a)) Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods pretty ∷ WithPrec (FoldSpec a) → Doc ann Source # prettyList ∷ [WithPrec (FoldSpec a)] → Doc ann Source #
HasSpec a ⇒ Pretty (FoldSpec a) Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods pretty ∷ FoldSpec a → Doc ann Source # prettyList ∷ [FoldSpec a] → Doc ann Source #

preMapFoldSpec ∷ HasSpec a ⇒ Fun '[a] b → FoldSpec b → FoldSpec a Source #

combineFoldSpec ∷ FoldSpec a → FoldSpec a → Either [String] (FoldSpec a) Source #

conformsToFoldSpec ∷ ∀ a. [a] → FoldSpec a → Bool Source #

data ListW (s ∷ Symbol) (args ∷ [Type]) (res ∷ Type) where Source #

Constructors

FoldMapW ∷ ∀ a b. (Foldy b, HasSpec a) ⇒ Fun '[a] b → ListW "foldMap_" '[[a]] b
SingletonListW ∷ ListW "singeltonList_" '[a] [a]
AppendW ∷ (Typeable a, Show a) ⇒ ListW "append_" '[[a], [a]] [a]

Instances

Instances details

Semantics ListW Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods semantics ∷ ∀ (s ∷ Symbol) (d ∷ [Type]) r. ListW s d r → FunTy d r Source #
Syntax ListW Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods isInFix ∷ ∀ (s ∷ Symbol) (dom ∷ [Type]) rng. ListW s dom rng → Bool Source # prettyWit ∷ ∀ (s ∷ Symbol) (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ ListW s dom rng → List Term dom → Int → Maybe (Doc ann) Source #
(Typeable a, Foldy b) ⇒ Logic "foldMap_" ListW '[[a]] b Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods info ∷ ListW "foldMap_" '[[a]] b → String Source # propagate ∷ Context "foldMap_" ListW '[[a]] b hole → Specification b → Specification hole Source # rewriteRules ∷ ListW "foldMap_" '[[a]] b → List Term '[[a]] → Evidence (AppRequires "foldMap_" ListW '[[a]] b) → Maybe (Term b) Source # mapTypeSpec ∷ ('[[a]] ~ '[a0], b ~ b0, HasSpec a0, HasSpec b0) ⇒ ListW "foldMap_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ ListW "foldMap_" '[[a]] Bool → List Term '[[a]] → [Pred] Source #
(Sized [a], HasSpec a) ⇒ Logic "append_" ListW '[[a], [a]] [a] Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods info ∷ ListW "append_" '[[a], [a]] [a] → String Source # propagate ∷ Context "append_" ListW '[[a], [a]] [a] hole → Specification [a] → Specification hole Source # rewriteRules ∷ ListW "append_" '[[a], [a]] [a] → List Term '[[a], [a]] → Evidence (AppRequires "append_" ListW '[[a], [a]] [a]) → Maybe (Term [a]) Source # mapTypeSpec ∷ ('[[a], [a]] ~ '[a0], [a] ~ b, HasSpec a0, HasSpec b) ⇒ ListW "append_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ ListW "append_" '[[a], [a]] Bool → List Term '[[a], [a]] → [Pred] Source #
HasSpec a ⇒ Logic "singeltonList_" ListW '[a] [a] Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods info ∷ ListW "singeltonList_" '[a] [a] → String Source # propagate ∷ Context "singeltonList_" ListW '[a] [a] hole → Specification [a] → Specification hole Source # rewriteRules ∷ ListW "singeltonList_" '[a] [a] → List Term '[a] → Evidence (AppRequires "singeltonList_" ListW '[a] [a]) → Maybe (Term [a]) Source # mapTypeSpec ∷ ('[a] ~ '[a0], [a] ~ b, HasSpec a0, HasSpec b) ⇒ ListW "singeltonList_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ ListW "singeltonList_" '[a] Bool → List Term '[a] → [Pred] Source #
Show (ListW s d r) Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods showsPrec ∷ Int → ListW s d r → ShowS show ∷ ListW s d r → String showList ∷ [ListW s d r] → ShowS
Eq (ListW s d r) Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods (==) ∷ ListW s d r → ListW s d r → Bool (/=) ∷ ListW s d r → ListW s d r → Bool

listSem ∷ ListW s dom rng → FunTy dom rng Source #

foldMap_ ∷ ∀ a b. (Sized [a], Foldy b, HasSpec a) ⇒ (Term a → Term b) → Term [a] → Term b Source #

sum_ ∷ Foldy a ⇒ Term [a] → Term a Source #

foldMapFn ∷ ∀ a b. (HasSpec a, Foldy b) ⇒ Fun '[a] b → Fun '[[a]] b Source #

toPredsFoldSpec ∷ (HasSpec a, HasSpec [a]) ⇒ Term [a] → FoldSpec a → Pred Source #

Used in the HasSpec [a] instance

elem_ ∷ (Sized [a], HasSpec a) ⇒ Term a → Term [a] → Term Bool infix 4 Source #

elemFn ∷ HasSpec a ⇒ Fun '[a, [a]] Bool Source #

reverseFoldSpec ∷ FoldSpec a → Specification a Source #

singletonList_ ∷ (Sized [a], HasSpec a) ⇒ Term a → Term [a] Source #

singletonListFn ∷ ∀ a. HasSpec a ⇒ Fun '[a] [a] Source #

prefixedBy ∷ Eq a ⇒ [a] → [[a]] → [[a]] Source #

suffixedBy ∷ Eq a ⇒ [a] → [[a]] → [[a]] Source #

alreadyHave ∷ Eq a ⇒ [a] → ListSpec a → ListSpec a Source #

alreadyHaveFold ∷ [a] → FoldSpec a → FoldSpec a Source #

appendFn ∷ ∀ a. (Sized [a], HasSpec a) ⇒ Fun '[[a], [a]] [a] Source #

append_ ∷ (Sized [a], HasSpec a) ⇒ Term [a] → Term [a] → Term [a] Source #

data ListSpec a Source #

Constructors

ListSpec
Fields listSpecHint ∷ Maybe Integer listSpecMust ∷ [a] listSpecSize ∷ Specification Integer listSpecElem ∷ Specification a listSpecFold ∷ FoldSpec a

Instances

Instances details

(Arbitrary a, Arbitrary (FoldSpec a), Arbitrary (TypeSpec a), HasSpec a) ⇒ Arbitrary (ListSpec a) Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods arbitrary ∷ Gen (ListSpec a) Source # shrink ∷ ListSpec a → [ListSpec a] Source #
HasSpec a ⇒ Show (ListSpec a) Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods showsPrec ∷ Int → ListSpec a → ShowS show ∷ ListSpec a → String showList ∷ [ListSpec a] → ShowS
HasSpec a ⇒ Pretty (WithPrec (ListSpec a)) Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods pretty ∷ WithPrec (ListSpec a) → Doc ann Source # prettyList ∷ [WithPrec (ListSpec a)] → Doc ann Source #
HasSpec a ⇒ Pretty (ListSpec a) Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods pretty ∷ ListSpec a → Doc ann Source # prettyList ∷ [ListSpec a] → Doc ann Source #

guardListSpec ∷ HasSpec a ⇒ [String] → ListSpec a → Specification [a] Source #

knownUpperBound ∷ (TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) ⇒ Specification a → Maybe a Source #

knownLowerBound ∷ (TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) ⇒ Specification a → Maybe a Source #

isEmptyNumSpec ∷ (TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) ⇒ Specification a → Bool Source #

enumerateInterval ∷ (Enum a, Num a, MaybeBounded a) ⇒ NumSpec a → [a] Source #

Note: potentially infinite list

genNumList ∷ ∀ a m. (MonadGenError m, Arbitrary a, Integral a, MaybeBounded a, TypeSpec a ~ NumSpec a, Foldy a, Random a) ⇒ Specification a → Specification a → GenT m [a] Source #

narrowByFuelAndSize Source #

Arguments

∷ ∀ a. (TypeSpec a ~ NumSpec a, HasSpec a, Arbitrary a, Integral a, Random a, MaybeBounded a)
⇒ a	Fuel
→ Int	Integer
→ (Specification a, Specification a)
→ (Specification a, Specification a)

narrowFoldSpecs ∷ ∀ a. (TypeSpec a ~ NumSpec a, HasSpec a, Arbitrary a, Integral a, Random a, MaybeBounded a) ⇒ (Specification a, Specification a) → (Specification a, Specification a) Source #

genListWithSize ∷ ∀ a m. (Foldy a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a, Integral a) ⇒ Specification Integer → Specification a → Specification a → GenT m [a] Source #

Generate a list with sizeSpec elements, that add up to a total that conforms to foldSpec. Every element in the list should conform to elemSpec

pickPositive ∷ ∀ t m. (Integral t, Random t, MonadGenError m, TypeSpec t ~ NumSpec t, Foldy t) ⇒ Specification t → t → Integer → GenT m [t] Source #

pickNegative ∷ ∀ t m. (Integral t, Random t, MonadGenError m, TypeSpec t ~ NumSpec t, HasSpec t) ⇒ Specification t → t → Integer → GenT m [t] Source #

total can be either negative, or 0. If it is 0, we want count numbers that add to zero

specName ∷ ∀ a. HasSpec a ⇒ Specification a → String Source #

predSpecPair ∷ ∀ a. HasSpec a ⇒ Specification a → (String, a → Bool) Source #

minFromSpec ∷ ∀ n. (Ord n, TypeSpec n ~ NumSpec n) ⇒ n → Specification n → n Source #

The smallest number admitted by the spec, if we can find one. if not return the defaultValue dv

maxFromSpec ∷ ∀ n. (Ord n, TypeSpec n ~ NumSpec n) ⇒ n → Specification n → n Source #

The largest number admitted by the spec, if we can find one. if not return the defaultValue dv

Orphan instances

(All (Typeable ∷ Type → Constraint) '[a, r], HasSpec r) ⇒ Logic "composeFn" FunW '[a] r Source #
Instance details Methods info ∷ FunW "composeFn" '[a] r → String Source # propagate ∷ Context "composeFn" FunW '[a] r hole → Specification r → Specification hole Source # rewriteRules ∷ FunW "composeFn" '[a] r → List Term '[a] → Evidence (AppRequires "composeFn" FunW '[a] r) → Maybe (Term r) Source # mapTypeSpec ∷ ('[a] ~ '[a0], r ~ b, HasSpec a0, HasSpec b) ⇒ FunW "composeFn" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ FunW "composeFn" '[a] Bool → List Term '[a] → [Pred] Source #
HasSpec a ⇒ Logic "elem_" BaseW '[a, [a]] Bool Source #
Instance details Methods info ∷ BaseW "elem_" '[a, [a]] Bool → String Source # propagate ∷ Context "elem_" BaseW '[a, [a]] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ BaseW "elem_" '[a, [a]] Bool → List Term '[a, [a]] → Evidence (AppRequires "elem_" BaseW '[a, [a]] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, [a]] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ BaseW "elem_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ BaseW "elem_" '[a, [a]] Bool → List Term '[a, [a]] → [Pred] Source #
(∀ (sym ∷ Symbol) (t ∷ Symbol → [Type] → Type → Type). Logic sym t '[a, b] r, All (Typeable ∷ Type → Constraint) '[a, b, r]) ⇒ Logic "flip_" FunW '[b, a] r Source #
Instance details Methods info ∷ FunW "flip_" '[b, a] r → String Source # propagate ∷ Context "flip_" FunW '[b, a] r hole → Specification r → Specification hole Source # rewriteRules ∷ FunW "flip_" '[b, a] r → List Term '[b, a] → Evidence (AppRequires "flip_" FunW '[b, a] r) → Maybe (Term r) Source # mapTypeSpec ∷ ('[b, a] ~ '[a0], r ~ b0, HasSpec a0, HasSpec b0) ⇒ FunW "flip_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ FunW "flip_" '[b, a] Bool → List Term '[b, a] → [Pred] Source #
(Typeable a, Foldy b) ⇒ Logic "foldMap_" ListW '[[a]] b Source #
Instance details Methods info ∷ ListW "foldMap_" '[[a]] b → String Source # propagate ∷ Context "foldMap_" ListW '[[a]] b hole → Specification b → Specification hole Source # rewriteRules ∷ ListW "foldMap_" '[[a]] b → List Term '[[a]] → Evidence (AppRequires "foldMap_" ListW '[[a]] b) → Maybe (Term b) Source # mapTypeSpec ∷ ('[[a]] ~ '[a0], b ~ b0, HasSpec a0, HasSpec b0) ⇒ ListW "foldMap_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ ListW "foldMap_" '[[a]] Bool → List Term '[[a]] → [Pred] Source #
HasSpec a ⇒ Logic "id_" FunW '[a] a Source #
Instance details Methods info ∷ FunW "id_" '[a] a → String Source # propagate ∷ Context "id_" FunW '[a] a hole → Specification a → Specification hole Source # rewriteRules ∷ FunW "id_" '[a] a → List Term '[a] → Evidence (AppRequires "id_" FunW '[a] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[a] ~ '[a0], a ~ b, HasSpec a0, HasSpec b) ⇒ FunW "id_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ FunW "id_" '[a] Bool → List Term '[a] → [Pred] Source #
(Sized [a], HasSpec a) ⇒ Logic "append_" ListW '[[a], [a]] [a] Source #
Instance details Methods info ∷ ListW "append_" '[[a], [a]] [a] → String Source # propagate ∷ Context "append_" ListW '[[a], [a]] [a] hole → Specification [a] → Specification hole Source # rewriteRules ∷ ListW "append_" '[[a], [a]] [a] → List Term '[[a], [a]] → Evidence (AppRequires "append_" ListW '[[a], [a]] [a]) → Maybe (Term [a]) Source # mapTypeSpec ∷ ('[[a], [a]] ~ '[a0], [a] ~ b, HasSpec a0, HasSpec b) ⇒ ListW "append_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ ListW "append_" '[[a], [a]] Bool → List Term '[[a], [a]] → [Pred] Source #
HasSpec a ⇒ Logic "singeltonList_" ListW '[a] [a] Source #
Instance details Methods info ∷ ListW "singeltonList_" '[a] [a] → String Source # propagate ∷ Context "singeltonList_" ListW '[a] [a] hole → Specification [a] → Specification hole Source # rewriteRules ∷ ListW "singeltonList_" '[a] [a] → List Term '[a] → Evidence (AppRequires "singeltonList_" ListW '[a] [a]) → Maybe (Term [a]) Source # mapTypeSpec ∷ ('[a] ~ '[a0], [a] ~ b, HasSpec a0, HasSpec b) ⇒ ListW "singeltonList_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ ListW "singeltonList_" '[a] Bool → List Term '[a] → [Pred] Source #
(Sized [a], HasSpec a) ⇒ HasGenHint [a] Source #
Instance details Associated Types type Hint [a] Source # Methods giveHint ∷ Hint [a] → Specification [a] Source #
(Sized [a], HasSpec a) ⇒ HasSpec [a] Source #
Instance details Associated Types type TypeSpec [a] Source # type Prerequisites [a] Source # Methods emptySpec ∷ TypeSpec [a] Source # combineSpec ∷ TypeSpec [a] → TypeSpec [a] → Specification [a] Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec [a] → GenT m [a] Source # conformsTo ∷ [a] → TypeSpec [a] → Bool Source # shrinkWithTypeSpec ∷ TypeSpec [a] → [a] → [[a]] Source # toPreds ∷ Term [a] → TypeSpec [a] → Pred Source # cardinalTypeSpec ∷ TypeSpec [a] → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec [a] → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec [a] → BinaryShow Source # monadConformsTo ∷ [a] → TypeSpec [a] → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec [a] → [[a]] → Specification [a] Source # guardTypeSpec ∷ [String] → TypeSpec [a] → Specification [a] Source # prerequisites ∷ Evidence (Prerequisites [a]) Source #
Sized [a] Source #
Instance details Methods sizeOf ∷ [a] → Integer Source # liftSizeSpec ∷ SizeSpec → [Integer] → Specification [a] Source # liftMemberSpec ∷ [Integer] → Specification [a] Source # sizeOfTypeSpec ∷ TypeSpec [a] → Specification Integer Source #
Forallable [a] a Source #
Instance details Methods fromForAllSpec ∷ Specification a → Specification [a] Source # forAllToList ∷ [a] → [a] Source #