Safe Haskell	Safe-Inferred
Language	Haskell2010

Constrained.Spec.Set

Contents

Orphan instances

Documentation

data SetSpec a Source #

Constructors

SetSpec (Set a) (Specification a) (Specification Integer)

Instances

Instances details

(Ord a, Arbitrary (Specification a), Arbitrary a) ⇒ Arbitrary (SetSpec a) Source #
Instance details Defined in Constrained.Spec.Set Methods arbitrary ∷ Gen (SetSpec a) Source # shrink ∷ SetSpec a → [SetSpec a] Source #
(Ord a, HasSpec a) ⇒ Monoid (SetSpec a) Source #
Instance details Defined in Constrained.Spec.Set Methods mempty ∷ SetSpec a mappend ∷ SetSpec a → SetSpec a → SetSpec a mconcat ∷ [SetSpec a] → SetSpec a
(Ord a, HasSpec a) ⇒ Semigroup (SetSpec a) Source #
Instance details Defined in Constrained.Spec.Set Methods (<>) ∷ SetSpec a → SetSpec a → SetSpec a # sconcat ∷ NonEmpty (SetSpec a) → SetSpec a stimes ∷ Integral b ⇒ b → SetSpec a → SetSpec a
HasSpec a ⇒ Show (SetSpec a) Source #
Instance details Defined in Constrained.Spec.Set Methods showsPrec ∷ Int → SetSpec a → ShowS show ∷ SetSpec a → String showList ∷ [SetSpec a] → ShowS

prettySetSpec ∷ HasSpec a ⇒ SetSpec a → Doc ann Source #

guardSetSpec ∷ (HasSpec a, Ord a) ⇒ [String] → SetSpec a → Specification (Set a) Source #

data SetW (s ∷ Symbol) (d ∷ [Type]) (r ∷ Type) where Source #

Constructors

SingletonW ∷ Ord a ⇒ SetW "singleton_" '[a] (Set a)
UnionW ∷ (Literal a, Ord a) ⇒ SetW "union_" '[Set a, Set a] (Set a)
SubsetW ∷ (Literal a, Ord a) ⇒ SetW "subset_" '[Set a, Set a] Bool
MemberW ∷ (Literal a, Ord a) ⇒ SetW "member_" '[a, Set a] Bool
DisjointW ∷ (Literal a, Ord a) ⇒ SetW "disjoint_" '[Set a, Set a] Bool
FromListW ∷ ∀ a. (HasSpec a, Ord a) ⇒ SetW "fromList_" '[[a]] (Set a)

Instances

Instances details

Semantics SetW Source #
Instance details Defined in Constrained.Spec.Set Methods semantics ∷ ∀ (s ∷ Symbol) (d ∷ [Type]) r. SetW s d r → FunTy d r Source #
Syntax SetW Source #
Instance details Defined in Constrained.Spec.Set Methods isInFix ∷ ∀ (s ∷ Symbol) (dom ∷ [Type]) rng. SetW s dom rng → Bool Source # prettyWit ∷ ∀ (s ∷ Symbol) (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ SetW s dom rng → List Term dom → Int → Maybe (Doc ann) Source #
(HasSpec a, Ord a) ⇒ Logic "disjoint_" SetW '[Set a, Set a] Bool Source #
Instance details Defined in Constrained.Spec.Set Methods info ∷ SetW "disjoint_" '[Set a, Set a] Bool → String Source # propagate ∷ Context "disjoint_" SetW '[Set a, Set a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ SetW "disjoint_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → Evidence (AppRequires "disjoint_" SetW '[Set a, Set a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[Set a, Set a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ SetW "disjoint_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "disjoint_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → [Pred] Source #
(HasSpec a, Ord a) ⇒ Logic "member_" SetW '[a, Set a] Bool Source #
Instance details Defined in Constrained.Spec.Set Methods info ∷ SetW "member_" '[a, Set a] Bool → String Source # propagate ∷ Context "member_" SetW '[a, Set a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ SetW "member_" '[a, Set a] Bool → List Term '[a, Set a] → Evidence (AppRequires "member_" SetW '[a, Set a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, Set a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ SetW "member_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "member_" '[a, Set a] Bool → List Term '[a, Set a] → [Pred] Source #
(HasSpec a, Ord a) ⇒ Logic "subset_" SetW '[Set a, Set a] Bool Source #
Instance details Defined in Constrained.Spec.Set Methods info ∷ SetW "subset_" '[Set a, Set a] Bool → String Source # propagate ∷ Context "subset_" SetW '[Set a, Set a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ SetW "subset_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → Evidence (AppRequires "subset_" SetW '[Set a, Set a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[Set a, Set a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ SetW "subset_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "subset_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → [Pred] Source #
(HasSpec a, Ord a) ⇒ Logic "fromList_" SetW '[[a]] (Set a) Source #
Instance details Defined in Constrained.Spec.Set Methods info ∷ SetW "fromList_" '[[a]] (Set a) → String Source # propagate ∷ Context "fromList_" SetW '[[a]] (Set a) hole → Specification (Set a) → Specification hole Source # rewriteRules ∷ SetW "fromList_" '[[a]] (Set a) → List Term '[[a]] → Evidence (AppRequires "fromList_" SetW '[[a]] (Set a)) → Maybe (Term (Set a)) Source # mapTypeSpec ∷ ('[[a]] ~ '[a0], Set a ~ b, HasSpec a0, HasSpec b) ⇒ SetW "fromList_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "fromList_" '[[a]] Bool → List Term '[[a]] → [Pred] Source #
(HasSpec a, Ord a) ⇒ Logic "singleton_" SetW '[a] (Set a) Source #
Instance details Defined in Constrained.Spec.Set Methods info ∷ SetW "singleton_" '[a] (Set a) → String Source # propagate ∷ Context "singleton_" SetW '[a] (Set a) hole → Specification (Set a) → Specification hole Source # rewriteRules ∷ SetW "singleton_" '[a] (Set a) → List Term '[a] → Evidence (AppRequires "singleton_" SetW '[a] (Set a)) → Maybe (Term (Set a)) Source # mapTypeSpec ∷ ('[a] ~ '[a0], Set a ~ b, HasSpec a0, HasSpec b) ⇒ SetW "singleton_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "singleton_" '[a] Bool → List Term '[a] → [Pred] Source #
(HasSpec a, Ord a) ⇒ Logic "union_" SetW '[Set a, Set a] (Set a) Source #
Instance details Defined in Constrained.Spec.Set Methods info ∷ SetW "union_" '[Set a, Set a] (Set a) → String Source # propagate ∷ Context "union_" SetW '[Set a, Set a] (Set a) hole → Specification (Set a) → Specification hole Source # rewriteRules ∷ SetW "union_" '[Set a, Set a] (Set a) → List Term '[Set a, Set a] → Evidence (AppRequires "union_" SetW '[Set a, Set a] (Set a)) → Maybe (Term (Set a)) Source # mapTypeSpec ∷ ('[Set a, Set a] ~ '[a0], Set a ~ b, HasSpec a0, HasSpec b) ⇒ SetW "union_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "union_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → [Pred] Source #
Show (SetW s ds r) Source #
Instance details Defined in Constrained.Spec.Set Methods showsPrec ∷ Int → SetW s ds r → ShowS show ∷ SetW s ds r → String showList ∷ [SetW s ds r] → ShowS
Eq (SetW s dom rng) Source #
Instance details Defined in Constrained.Spec.Set Methods (==) ∷ SetW s dom rng → SetW s dom rng → Bool (/=) ∷ SetW s dom rng → SetW s dom rng → Bool

setSem ∷ SetW s ds r → FunTy ds r Source #

singletons ∷ [Set a] → [Set a] Source #

singleton_ ∷ (Ord a, HasSpec a) ⇒ Term a → Term (Set a) Source #

subset_ ∷ (Ord a, HasSpec a) ⇒ Term (Set a) → Term (Set a) → Term Bool Source #

member_ ∷ (Ord a, HasSpec a) ⇒ Term a → Term (Set a) → Term Bool Source #

union_ ∷ (Ord a, HasSpec a) ⇒ Term (Set a) → Term (Set a) → Term (Set a) Source #

disjoint_ ∷ (Ord a, HasSpec a) ⇒ Term (Set a) → Term (Set a) → Term Bool Source #

fromList_ ∷ ∀ a. (Ord a, HasSpec a) ⇒ Term [a] → Term (Set a) Source #

Orphan instances

(HasSpec a, Ord a) ⇒ Logic "disjoint_" SetW '[Set a, Set a] Bool Source #
Instance details Methods info ∷ SetW "disjoint_" '[Set a, Set a] Bool → String Source # propagate ∷ Context "disjoint_" SetW '[Set a, Set a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ SetW "disjoint_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → Evidence (AppRequires "disjoint_" SetW '[Set a, Set a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[Set a, Set a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ SetW "disjoint_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "disjoint_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → [Pred] Source #
(HasSpec a, Ord a) ⇒ Logic "member_" SetW '[a, Set a] Bool Source #
Instance details Methods info ∷ SetW "member_" '[a, Set a] Bool → String Source # propagate ∷ Context "member_" SetW '[a, Set a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ SetW "member_" '[a, Set a] Bool → List Term '[a, Set a] → Evidence (AppRequires "member_" SetW '[a, Set a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, Set a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ SetW "member_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "member_" '[a, Set a] Bool → List Term '[a, Set a] → [Pred] Source #
(HasSpec a, Ord a) ⇒ Logic "subset_" SetW '[Set a, Set a] Bool Source #
Instance details Methods info ∷ SetW "subset_" '[Set a, Set a] Bool → String Source # propagate ∷ Context "subset_" SetW '[Set a, Set a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ SetW "subset_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → Evidence (AppRequires "subset_" SetW '[Set a, Set a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[Set a, Set a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ SetW "subset_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "subset_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → [Pred] Source #
(HasSpec a, Ord a) ⇒ Logic "fromList_" SetW '[[a]] (Set a) Source #
Instance details Methods info ∷ SetW "fromList_" '[[a]] (Set a) → String Source # propagate ∷ Context "fromList_" SetW '[[a]] (Set a) hole → Specification (Set a) → Specification hole Source # rewriteRules ∷ SetW "fromList_" '[[a]] (Set a) → List Term '[[a]] → Evidence (AppRequires "fromList_" SetW '[[a]] (Set a)) → Maybe (Term (Set a)) Source # mapTypeSpec ∷ ('[[a]] ~ '[a0], Set a ~ b, HasSpec a0, HasSpec b) ⇒ SetW "fromList_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "fromList_" '[[a]] Bool → List Term '[[a]] → [Pred] Source #
(HasSpec a, Ord a) ⇒ Logic "singleton_" SetW '[a] (Set a) Source #
Instance details Methods info ∷ SetW "singleton_" '[a] (Set a) → String Source # propagate ∷ Context "singleton_" SetW '[a] (Set a) hole → Specification (Set a) → Specification hole Source # rewriteRules ∷ SetW "singleton_" '[a] (Set a) → List Term '[a] → Evidence (AppRequires "singleton_" SetW '[a] (Set a)) → Maybe (Term (Set a)) Source # mapTypeSpec ∷ ('[a] ~ '[a0], Set a ~ b, HasSpec a0, HasSpec b) ⇒ SetW "singleton_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "singleton_" '[a] Bool → List Term '[a] → [Pred] Source #
(HasSpec a, Ord a) ⇒ Logic "union_" SetW '[Set a, Set a] (Set a) Source #
Instance details Methods info ∷ SetW "union_" '[Set a, Set a] (Set a) → String Source # propagate ∷ Context "union_" SetW '[Set a, Set a] (Set a) hole → Specification (Set a) → Specification hole Source # rewriteRules ∷ SetW "union_" '[Set a, Set a] (Set a) → List Term '[Set a, Set a] → Evidence (AppRequires "union_" SetW '[Set a, Set a] (Set a)) → Maybe (Term (Set a)) Source # mapTypeSpec ∷ ('[Set a, Set a] ~ '[a0], Set a ~ b, HasSpec a0, HasSpec b) ⇒ SetW "union_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "union_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → [Pred] Source #
Arbitrary (FoldSpec (Set a)) Source #
Instance details Methods arbitrary ∷ Gen (FoldSpec (Set a)) Source # shrink ∷ FoldSpec (Set a) → [FoldSpec (Set a)] Source #
(Ord a, HasSpec a, HasSpec (Set a)) ⇒ Monoid (Term (Set a)) Source #
Instance details Methods mempty ∷ Term (Set a) mappend ∷ Term (Set a) → Term (Set a) → Term (Set a) mconcat ∷ [Term (Set a)] → Term (Set a)
(Ord a, HasSpec a, HasSpec (Set a)) ⇒ Semigroup (Term (Set a)) Source #
Instance details Methods (<>) ∷ Term (Set a) → Term (Set a) → Term (Set a) # sconcat ∷ NonEmpty (Term (Set a)) → Term (Set a) stimes ∷ Integral b ⇒ b → Term (Set a) → Term (Set a)
(Ord a, HasSpec a) ⇒ HasSpec (Set a) Source #
Instance details Associated Types type TypeSpec (Set a) Source # type Prerequisites (Set a) Source # Methods emptySpec ∷ TypeSpec (Set a) Source # combineSpec ∷ TypeSpec (Set a) → TypeSpec (Set a) → Specification (Set a) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (Set a) → GenT m (Set a) Source # conformsTo ∷ Set a → TypeSpec (Set a) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (Set a) → Set a → [Set a] Source # toPreds ∷ Term (Set a) → TypeSpec (Set a) → Pred Source # cardinalTypeSpec ∷ TypeSpec (Set a) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (Set a) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (Set a) → BinaryShow Source # monadConformsTo ∷ Set a → TypeSpec (Set a) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (Set a) → [Set a] → Specification (Set a) Source # guardTypeSpec ∷ [String] → TypeSpec (Set a) → Specification (Set a) Source # prerequisites ∷ Evidence (Prerequisites (Set a)) Source #
Ord a ⇒ Sized (Set a) Source #
Instance details Methods sizeOf ∷ Set a → Integer Source # liftSizeSpec ∷ SizeSpec → [Integer] → Specification (Set a) Source # liftMemberSpec ∷ [Integer] → Specification (Set a) Source # sizeOfTypeSpec ∷ TypeSpec (Set a) → Specification Integer Source #
Ord a ⇒ Forallable (Set a) a Source #
Instance details Methods fromForAllSpec ∷ Specification a → Specification (Set a) Source # forAllToList ∷ Set a → [a] Source #