| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Constrained.API
Synopsis
- type Specification = SpecificationD Deps
- type Pred = PredD Deps
- type Term = TermD Deps
- data NonEmpty a = a :| [a]
- class (Typeable a, Eq a, Show a, TypeSpecEqShow a) ⇒ HasSpec a where
- type TypeSpec a
- type Prerequisites a ∷ Constraint
- emptySpec ∷ TypeSpec a
- combineSpec ∷ TypeSpec a → TypeSpec a → Specification a
- genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a
- conformsTo ∷ HasCallStack ⇒ a → TypeSpec a → Bool
- shrinkWithTypeSpec ∷ TypeSpec a → a → [a]
- toPreds ∷ Term a → TypeSpec a → Pred
- cardinalTypeSpec ∷ TypeSpec a → Specification Integer
- cardinalTrueSpec ∷ Specification Integer
- typeSpecHasError ∷ TypeSpec a → Maybe (NonEmpty String)
- alternateShow ∷ TypeSpec a → BinaryShow
- monadConformsTo ∷ a → TypeSpec a → Writer [String] Bool
- typeSpecOpt ∷ TypeSpec a → [a] → Specification a
- guardTypeSpec ∷ [String] → TypeSpec a → Specification a
- prerequisites ∷ Evidence (Prerequisites a)
- class Typeable (SimpleRep a) ⇒ HasSimpleRep a where
- type SimpleRep a
- type TheSop a ∷ [Type]
- toSimpleRep ∷ a → SimpleRep a
- fromSimpleRep ∷ SimpleRep a → a
- class (HasSpec a, NumLike a) ⇒ Foldy a where
- genList ∷ MonadGenError m ⇒ Specification a → Specification a → GenT m [a]
- theAddFn ∷ IntW '[a, a] a
- theZero ∷ a
- genSizedList ∷ MonadGenError m ⇒ Specification Integer → Specification a → Specification a → GenT m [a]
- noNegativeValues ∷ Bool
- class (Ord a, HasSpec a) ⇒ OrdLike a where
- leqSpec ∷ a → Specification a
- ltSpec ∷ a → Specification a
- geqSpec ∷ a → Specification a
- gtSpec ∷ a → Specification a
- class Forallable t e | t → e where
- fromForAllSpec ∷ (HasSpec t, HasSpec e) ⇒ Specification e → Specification t
- forAllToList ∷ t → [e]
- class (HasSpec a, Show (Hint a)) ⇒ HasGenHint a where
- type Hint a
- giveHint ∷ Hint a → Specification a
- class Sized t where
- sizeOf ∷ t → Integer
- liftSizeSpec ∷ HasSpec t ⇒ SizeSpec → [Integer] → Specification t
- liftMemberSpec ∷ HasSpec t ⇒ [Integer] → Specification t
- sizeOfTypeSpec ∷ HasSpec t ⇒ TypeSpec t → Specification Integer
- class (Num a, HasSpec a) ⇒ NumLike a where
- subtractSpec ∷ a → TypeSpec a → Specification a
- negateSpec ∷ TypeSpec a → Specification a
- safeSubtract ∷ a → a → Maybe a
- type GenericallyInstantiated a = (AssertComputes (SimpleRep a) (((Text "Trying to use a generic instantiation of " :<>: ShowType a) :<>: Text ", likely in a HasSpec instance.") :$$: Text "However, the type has no definition of SimpleRep, likely because of a missing instance of HasSimpleRep."), HasSimpleRep a, HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a))
- class Show p ⇒ IsPred p
- class (Typeable t, Semantics t, Syntax t) ⇒ Logic t
- class Semantics (t ∷ [Type] → Type → Type)
- class Syntax (t ∷ [Type] → Type → Type)
- type Numeric a = (HasSpec a, Ord a, Num a, TypeSpec a ~ NumSpec a, MaybeBounded a)
- type IsNormalType a = (AssertComputes (Cases a) (Text "Failed to compute Cases in a use of IsNormalType for " :$$: (ShowType a :<>: Text ", are you missing an IsNormalType constraint?")), Cases a ~ '[a], AssertComputes (Args a) ((Text "Failed to compute Args in a use of IsNormalType for " :<>: ShowType a) :<>: Text ", are you missing an IsNormalType constraint?"), Args a ~ '[a], IsProd a, CountCases a ~ 1)
- constrained ∷ ∀ a p. (IsPred p, HasSpec a) ⇒ (Term a → p) → Specification a
- constrained' ∷ ∀ a p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p, GenericRequires a, ProdAsListComputes a) ⇒ FunTy (MapList Term (ProductAsList a)) p → Specification a
- match ∷ ∀ p a. (IsProductType a, IsPred p, GenericRequires a, ProdAsListComputes a) ⇒ Term a → FunTy (MapList Term (ProductAsList a)) p → Pred
- letBind ∷ (HasSpec a, IsPred p) ⇒ Term a → (Term a → p) → Pred
- assert ∷ IsPred p ⇒ p → Pred
- assertExplain ∷ IsPred p ⇒ NonEmpty String → p → Pred
- assertReified ∷ HasSpec a ⇒ Term a → (a → Bool) → Pred
- forAll ∷ ∀ p t a. (Forallable t a, HasSpec t, HasSpec a, IsPred p) ⇒ Term t → (Term a → p) → Pred
- forAll' ∷ ∀ t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t, HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a), IsProductType a, HasSpec a, GenericRequires a, ProdAsListComputes a) ⇒ Term t → FunTy (MapList Term (ProductAsList a)) p → Pred
- exists ∷ ∀ a p. (HasSpec a, IsPred p) ⇒ ((∀ b. Term b → b) → GE a) → (Term a → p) → Pred
- unsafeExists ∷ ∀ a p. (HasSpec a, IsPred p) ⇒ (Term a → p) → Pred
- whenTrue ∷ ∀ p. IsPred p ⇒ Term Bool → p → Pred
- ifElse ∷ (IsPred p, IsPred q) ⇒ Term Bool → p → q → Pred
- dependsOn ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Pred
- reify ∷ (HasSpec a, HasSpec b, IsPred p) ⇒ Term a → (a → b) → (Term b → p) → Pred
- reify' ∷ ∀ a b p. (Cases (SimpleRep b) ~ '[SimpleRep b], TypeSpec b ~ TypeSpec (SimpleRep b), HasSpec (SimpleRep b), HasSimpleRep b, All HasSpec (Args (SimpleRep b)), IsProd (SimpleRep b), HasSpec a, HasSpec b, IsProductType b, IsProd a, IsPred p, GenericRequires b, ProdAsListComputes b) ⇒ Term a → (a → b) → FunTy (MapList Term (ProductAsList b)) p → Pred
- reifies ∷ (HasSpec a, HasSpec b) ⇒ Term b → Term a → (a → b) → Pred
- explanation ∷ NonEmpty String → Pred → Pred
- monitor ∷ ((∀ a. Term a → a) → Property → Property) → Pred
- genHint ∷ ∀ t. HasGenHint t ⇒ Hint t → Term t → Pred
- caseOn ∷ ∀ a. (GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) ⇒ Term a → FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
- branch ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ FunTy (MapList Term (Args a)) p → Weighted Binder a
- branchW ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ Int → FunTy (MapList Term (Args a)) p → Weighted Binder a
- onCon ∷ ∀ c a p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All HasSpec (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term a → FunTy (MapList Term (ConstrOf c (TheSop a))) p → Pred
- isCon ∷ ∀ c a. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), GenericRequires a) ⇒ Term a → Pred
- onJust ∷ ∀ a p. (HasSpec a, IsNormalType a, IsPred p) ⇒ Term (Maybe a) → (Term a → p) → Pred
- isJust ∷ ∀ a. (HasSpec a, IsNormalType a) ⇒ Term (Maybe a) → Pred
- lit ∷ HasSpec a ⇒ a → Term a
- con ∷ ∀ c a r. (SimpleRep a ~ SOP (TheSop a), TypeSpec a ~ TypeSpec (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a), ResultType r ~ Term a, SOPTerm c (TheSop a), ConstrTerm (ConstrOf c (TheSop a)), GenericRequires a) ⇒ r
- sel ∷ ∀ n a c as. (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a, HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) ⇒ Term a → Term (At n as)
- var ∷ QuasiQuoter
- name ∷ String → Term a → Term a
- (<.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool
- (<=.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool
- (>=.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool
- (>.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool
- (==.) ∷ HasSpec a ⇒ Term a → Term a → Term Bool
- (/=.) ∷ HasSpec a ⇒ Term a → Term a → Term Bool
- (+.) ∷ NumLike a ⇒ Term a → Term a → Term a
- (-.) ∷ Numeric n ⇒ Term n → Term n → Term n
- negate_ ∷ NumLike a ⇒ Term a → Term a
- not_ ∷ Term Bool → Term Bool
- (||.) ∷ Term Bool → Term Bool → Term Bool
- pair_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term b → Term (a, b)
- fst_ ∷ (HasSpec x, HasSpec y) ⇒ Term (x, y) → Term x
- snd_ ∷ (HasSpec x, HasSpec y) ⇒ Term (x, y) → Term y
- left_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term (Either a b)
- right_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term b → Term (Either a b)
- just_ ∷ (HasSpec a, IsNormalType a) ⇒ Term a → Term (Maybe a)
- nothing_ ∷ (HasSpec a, IsNormalType a) ⇒ Term (Maybe a)
- id_ ∷ ∀ a. HasSpec a ⇒ Term a → Term a
- flip_ ∷ ∀ (t ∷ [Type] → Type → Type) a b r. (HasSpec b, HasSpec a, AppRequires t '[a, b] r) ⇒ t '[a, b] r → Term b → Term a → Term r
- compose_ ∷ ∀ b t1 t2 a r. (AppRequires t1 '[b] r, AppRequires t2 '[a] b) ⇒ t1 '[b] r → t2 '[a] b → Term a → Term r
- foldMap_ ∷ ∀ a b. (Foldy b, HasSpec a) ⇒ (Term a → Term b) → Term [a] → Term b
- sum_ ∷ Foldy a ⇒ Term [a] → Term a
- elem_ ∷ (Sized [a], HasSpec a) ⇒ Term a → Term [a] → Term Bool
- singletonList_ ∷ (Sized [a], HasSpec a) ⇒ Term a → Term [a]
- append_ ∷ (Sized [a], HasSpec a) ⇒ Term [a] → Term [a] → Term [a]
- (++.) ∷ HasSpec a ⇒ Term [a] → Term [a] → Term [a]
- sizeOf_ ∷ (HasSpec a, Sized a) ⇒ Term a → Term Integer
- null_ ∷ (HasSpec a, Sized a) ⇒ Term a → Term Bool
- length_ ∷ HasSpec a ⇒ Term [a] → Term Integer
- singleton_ ∷ (Ord a, HasSpec a) ⇒ Term a → Term (Set a)
- member_ ∷ (Ord a, HasSpec a) ⇒ Term a → Term (Set a) → Term Bool
- union_ ∷ (Ord a, HasSpec a) ⇒ Term (Set a) → Term (Set a) → Term (Set a)
- subset_ ∷ (Ord a, HasSpec a) ⇒ Term (Set a) → Term (Set a) → Term Bool
- disjoint_ ∷ (Ord a, HasSpec a) ⇒ Term (Set a) → Term (Set a) → Term Bool
- fromList_ ∷ ∀ a. (Ord a, HasSpec a) ⇒ Term [a] → Term (Set a)
- dom_ ∷ (HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term (Set k)
- rng_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term [v]
- lookup_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term k → Term (Map k v) → Term (Maybe v)
- mapMember_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term k → Term (Map k v) → Term Bool
- rootLabel_ ∷ ∀ a. HasSpec a ⇒ Term (Tree a) → Term a
- fromGeneric_ ∷ ∀ a. (GenericRequires a, AppRequires BaseW '[SimpleRep a] a) ⇒ Term (SimpleRep a) → Term a
- toGeneric_ ∷ ∀ a. GenericRequires a ⇒ Term a → Term (SimpleRep a)
- satisfies ∷ ∀ a. HasSpec a ⇒ Term a → Specification a → Pred
- chooseSpec ∷ HasSpec a ⇒ (Int, Specification a) → (Int, Specification a) → Specification a
- trueSpec ∷ Specification a
- equalSpec ∷ a → Specification a
- notEqualSpec ∷ ∀ a. HasSpec a ⇒ a → Specification a
- notMemberSpec ∷ ∀ a f. (HasSpec a, Foldable f) ⇒ f a → Specification a
- hasSize ∷ (HasSpec t, Sized t) ⇒ SizeSpec → Specification t
- explainSpec ∷ [String] → Specification a → Specification a
- rangeSize ∷ Integer → Integer → SizeSpec
- between ∷ (HasSpec a, TypeSpec a ~ NumSpec a) ⇒ a → a → Specification a
- typeSpec ∷ HasSpec a ⇒ TypeSpec a → Specification a
- defaultMapSpec ∷ Ord k ⇒ MapSpec k v
- genFromSpec ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Specification a → Gen a
- genFromSpecT ∷ ∀ a m. (HasCallStack, HasSpec a, MonadGenError m) ⇒ Specification a → GenT m a
- genFromSpecWithSeed ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Int → Int → Specification a → a
- genFromSizeSpec ∷ MonadGenError m ⇒ Specification Integer → GenT m Integer
- shrinkWithSpec ∷ ∀ a. HasSpec a ⇒ Specification a → a → [a]
- debugSpec ∷ ∀ a. HasSpec a ⇒ Specification a → IO ()
- printPlan ∷ HasSpec a ⇒ Specification a → IO ()
- conformsToSpec ∷ HasSpec a ⇒ a → Specification a → Bool
- conformsToSpecE ∷ ∀ a. HasSpec a ⇒ a → Specification a → NonEmpty String → Maybe (NonEmpty String)
- conformsToSpecProp ∷ ∀ a. HasSpec a ⇒ a → Specification a → Property
- monitorSpec ∷ Testable p ⇒ Specification a → a → p → Property
- forAllSpec ∷ (HasSpec a, Testable p) ⇒ Specification a → (a → p) → Property
- forAllSpecShow ∷ (HasSpec a, Testable p) ⇒ Specification a → (a → String) → (a → p) → Property
- forAllSpecDiscard ∷ (HasSpec a, Testable p) ⇒ Specification a → (a → p) → Property
Types
type Specification = SpecificationD Deps Source #
Non-empty (and non-strict) list type.
Since: base-4.9.0.0
Constructors
| a :| [a] infixr 5 |
Instances
Type classes and constraints
class (Typeable a, Eq a, Show a, TypeSpecEqShow a) ⇒ HasSpec a where Source #
Minimal complete definition
Nothing
Associated Types
The `TypeSpec a` is the type-specific `Specification a`.
type Prerequisites a ∷ Constraint Source #
Prerequisites for the instance that are sometimes necessary
when working with e.g. Specifications or functions in the universe.
type Prerequisites a = ()
Methods
emptySpec ∷ TypeSpec a Source #
default emptySpec ∷ GenericallyInstantiated a ⇒ TypeSpec a Source #
combineSpec ∷ TypeSpec a → TypeSpec a → Specification a Source #
default combineSpec ∷ GenericallyInstantiated a ⇒ TypeSpec a → TypeSpec a → Specification a Source #
genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a Source #
Generate a value that satisfies the HasSpec.
The key property for this generator is soundness:
∀ a ∈ genFromTypeSpec spec. a conformsTo spec
default genFromTypeSpec ∷ (GenericallyInstantiated a, HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a Source #
conformsTo ∷ HasCallStack ⇒ a → TypeSpec a → Bool Source #
Check conformance to the spec.
default conformsTo ∷ (GenericallyInstantiated a, HasCallStack) ⇒ a → TypeSpec a → Bool Source #
shrinkWithTypeSpec ∷ TypeSpec a → a → [a] Source #
Shrink an a with the aide of a HasSpec
default shrinkWithTypeSpec ∷ GenericallyInstantiated a ⇒ TypeSpec a → a → [a] Source #
toPreds ∷ Term a → TypeSpec a → Pred Source #
Convert a spec to predicates:
The key property here is:
∀ a. a conformsTo spec == a conformsTo constrained (t -> toPreds t spec)
cardinalTypeSpec ∷ TypeSpec a → Specification Integer Source #
Compute an upper and lower bound on the number of solutions genFromTypeSpec might return
default cardinalTypeSpec ∷ GenericallyInstantiated a ⇒ TypeSpec a → Specification Integer Source #
cardinalTrueSpec ∷ Specification Integer Source #
A bound on the number of solutions `genFromTypeSpec TrueSpec` can produce. For a type with finite elements, we can get a much more accurate answer than TrueSpec
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 #
For some types (especially finite ones) there may be much better ways to construct
a Specification than the default method of just adding a large bad list to TypSpec. This
function allows each HasSpec instance to decide.
guardTypeSpec ∷ [String] → TypeSpec a → Specification a Source #
This can be used to detect self inconsistencies in a (TypeSpec t)
Note this is similar to typeSpecHasError, and the default
value for typeSpecHasError is written in terms of guardTypeSpec
Both typeSpecHasError and guardTypeSpec can be set individually.
prerequisites ∷ Evidence (Prerequisites a) Source #
Materialize the Prerequisites dictionary. It should not be necessary to
implement this function manually.
default prerequisites ∷ Prerequisites a ⇒ Evidence (Prerequisites a) Source #
Instances
class Typeable (SimpleRep a) ⇒ HasSimpleRep a where Source #
Minimal complete definition
Nothing
Associated Types
Methods
toSimpleRep ∷ a → SimpleRep a Source #
default toSimpleRep ∷ (Generic a, SimpleGeneric (Rep a), SimpleRep a ~ SimplifyRep (Rep a)) ⇒ a → SimpleRep a Source #
fromSimpleRep ∷ SimpleRep a → a Source #
default fromSimpleRep ∷ (Generic a, SimpleGeneric (Rep a), SimpleRep a ~ SimplifyRep (Rep a)) ⇒ SimpleRep a → a Source #
Instances
class (HasSpec a, NumLike a) ⇒ Foldy a where Source #
Minimal complete definition
Nothing
Methods
genList ∷ MonadGenError m ⇒ Specification a → Specification a → GenT m [a] Source #
default genList ∷ (MonadGenError m, GenericallyInstantiated a, Foldy (SimpleRep a)) ⇒ Specification a → Specification a → GenT m [a] Source #
theAddFn ∷ IntW '[a, a] a Source #
genSizedList ∷ MonadGenError m ⇒ Specification Integer → Specification a → Specification a → GenT m [a] Source #
default genSizedList ∷ (MonadGenError m, GenericallyInstantiated a, Foldy (SimpleRep a)) ⇒ Specification Integer → Specification a → Specification a → GenT m [a] Source #
Instances
class (Ord a, HasSpec a) ⇒ OrdLike a where Source #
Minimal complete definition
Nothing
Methods
leqSpec ∷ a → Specification a Source #
default leqSpec ∷ (GenericRequires a, OrdLike (SimpleRep a)) ⇒ a → Specification a Source #
ltSpec ∷ a → Specification a Source #
default ltSpec ∷ (OrdLike (SimpleRep a), GenericRequires a) ⇒ a → Specification a Source #
geqSpec ∷ a → Specification a Source #
default geqSpec ∷ (OrdLike (SimpleRep a), GenericRequires a) ⇒ a → Specification a Source #
gtSpec ∷ a → Specification a Source #
default gtSpec ∷ (OrdLike (SimpleRep a), GenericRequires a) ⇒ a → Specification a Source #
Instances
| (Ord a, HasSpec a, MaybeBounded a, Num a, TypeSpec a ~ NumSpec a) ⇒ OrdLike a Source # | This instance should be general enough for every type of Number that has a NumSpec as its TypeSpec |
Defined in Constrained.NumOrd Methods leqSpec ∷ a → Specification a Source # ltSpec ∷ a → Specification a Source # geqSpec ∷ a → Specification a Source # gtSpec ∷ a → Specification a Source # | |
class Forallable t e | t → e where Source #
Minimal complete definition
Nothing
Methods
fromForAllSpec ∷ (HasSpec t, HasSpec e) ⇒ Specification e → Specification t Source #
default fromForAllSpec ∷ (HasSpec e, Forallable (SimpleRep t) e, GenericRequires t) ⇒ Specification e → Specification t Source #
forAllToList ∷ t → [e] Source #
default forAllToList ∷ (HasSimpleRep t, Forallable (SimpleRep t) e) ⇒ t → [e] Source #
Instances
class (HasSpec a, Show (Hint a)) ⇒ HasGenHint a where Source #
Hints are things that only affect generation, and not validation. For instance, parameters to control distribution of generated values.
Methods
giveHint ∷ Hint a → Specification a Source #
Instances
| HasSpec a ⇒ HasGenHint (BinTree a) Source # | |
| HasSpec a ⇒ HasGenHint (Tree a) Source # | |
| (Sized [a], HasSpec a) ⇒ HasGenHint [a] Source # | |
Defined in Constrained.TheKnot Methods giveHint ∷ Hint [a] → Specification [a] Source # | |
| (Ord k, HasSpec k, HasSpec v, HasSpec [v], IsNormalType k, IsNormalType v) ⇒ HasGenHint (Map k v) Source # | |
Minimal complete definition
Nothing
Methods
liftSizeSpec ∷ HasSpec t ⇒ SizeSpec → [Integer] → Specification t Source #
default liftSizeSpec ∷ (Sized (SimpleRep t), GenericRequires t) ⇒ SizeSpec → [Integer] → Specification t Source #
liftMemberSpec ∷ HasSpec t ⇒ [Integer] → Specification t Source #
default liftMemberSpec ∷ (Sized (SimpleRep t), GenericRequires t) ⇒ [Integer] → Specification t Source #
sizeOfTypeSpec ∷ HasSpec t ⇒ TypeSpec t → Specification Integer Source #
Instances
| Ord a ⇒ Sized (Set a) Source # | |
Defined in Constrained.Spec.Set 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 # | |
| Sized [a] Source # | |
Defined in Constrained.TheKnot Methods sizeOf ∷ [a] → Integer Source # liftSizeSpec ∷ SizeSpec → [Integer] → Specification [a] Source # liftMemberSpec ∷ [Integer] → Specification [a] Source # sizeOfTypeSpec ∷ TypeSpec [a] → Specification Integer Source # | |
| Ord a ⇒ Sized (Map a b) Source # | |
Defined in Constrained.Spec.Map Methods sizeOf ∷ Map a b → Integer Source # liftSizeSpec ∷ SizeSpec → [Integer] → Specification (Map a b) Source # liftMemberSpec ∷ [Integer] → Specification (Map a b) Source # sizeOfTypeSpec ∷ TypeSpec (Map a b) → Specification Integer Source # | |
class (Num a, HasSpec a) ⇒ NumLike a where Source #
Minimal complete definition
Nothing
Methods
subtractSpec ∷ a → TypeSpec a → Specification a Source #
default subtractSpec ∷ (NumLike (SimpleRep a), GenericRequires a) ⇒ a → TypeSpec a → Specification a Source #
negateSpec ∷ TypeSpec a → Specification a Source #
default negateSpec ∷ (NumLike (SimpleRep a), GenericRequires a) ⇒ TypeSpec a → Specification a Source #
safeSubtract ∷ a → a → Maybe a Source #
default safeSubtract ∷ (HasSimpleRep a, NumLike (SimpleRep a)) ⇒ a → a → Maybe a Source #
Instances
| Numeric a ⇒ NumLike a Source # | |
Defined in Constrained.NumOrd Methods subtractSpec ∷ a → TypeSpec a → Specification a Source # negateSpec ∷ TypeSpec a → Specification a Source # safeSubtract ∷ a → a → Maybe a Source # | |
type GenericallyInstantiated a = (AssertComputes (SimpleRep a) (((Text "Trying to use a generic instantiation of " :<>: ShowType a) :<>: Text ", likely in a HasSpec instance.") :$$: Text "However, the type has no definition of SimpleRep, likely because of a missing instance of HasSimpleRep."), HasSimpleRep a, HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) Source #
class Show p ⇒ IsPred p Source #
Minimal complete definition
class (Typeable t, Semantics t, Syntax t) ⇒ Logic t Source #
A First-order typed logic has 4 components 1. Terms (Variables (x), Constants (5), and Applications (F x 5) Applications, apply a function symbol to a list of arguments: (FunctionSymbol term1 .. termN) 2. Predicates (Ordered, Odd, ...) 3. Connectives (And, Or, Not, =>, ...) 4. Quantifiers (Forall, Exists)
The Syntax, Semantics, and Logic classes implement new function symbols in the first order logic. Note that a function symbol is first order data, that uniquely identifies a higher order function. The three classes supply varying levels of functionality, relating to the Syntax, Semantics, and Logical operations of the function symbol.
Logical operations are one that support reasoning about how a function symbol relates to logical properties, that we call Specification's
Minimal complete definition
Instances
class Semantics (t ∷ [Type] → Type → Type) Source #
Semantic operations are ones that give the function symbol, meaning as a function. I.e. how to apply the function to a list of arguments and return a value.
Minimal complete definition
Instances
class Syntax (t ∷ [Type] → Type → Type) Source #
Syntactic operations are ones that have to do with the structure and appearence of the type.
See DependencyInjection to better understand deps - it's a
pointer to postpone having to define HasSpec and friends here.
Instances
type IsNormalType a = (AssertComputes (Cases a) (Text "Failed to compute Cases in a use of IsNormalType for " :$$: (ShowType a :<>: Text ", are you missing an IsNormalType constraint?")), Cases a ~ '[a], AssertComputes (Args a) ((Text "Failed to compute Args in a use of IsNormalType for " :<>: ShowType a) :<>: Text ", are you missing an IsNormalType constraint?"), Args a ~ '[a], IsProd a, CountCases a ~ 1) Source #
Core syntax
constrained ∷ ∀ a p. (IsPred p, HasSpec a) ⇒ (Term a → p) → Specification a Source #
constrained' ∷ ∀ a p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p, GenericRequires a, ProdAsListComputes a) ⇒ FunTy (MapList Term (ProductAsList a)) p → Specification a Source #
Like constrained but pattern matches on the bound `Term a`
match ∷ ∀ p a. (IsProductType a, IsPred p, GenericRequires a, ProdAsListComputes a) ⇒ Term a → FunTy (MapList Term (ProductAsList a)) p → Pred Source #
forAll ∷ ∀ p t a. (Forallable t a, HasSpec t, HasSpec a, IsPred p) ⇒ Term t → (Term a → p) → Pred Source #
forAll' ∷ ∀ t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t, HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a), IsProductType a, HasSpec a, GenericRequires a, ProdAsListComputes a) ⇒ Term t → FunTy (MapList Term (ProductAsList a)) p → Pred Source #
Like forAll but pattern matches on the `Term a`
ifElse ∷ (IsPred p, IsPred q) ⇒ Term Bool → p → q → Pred Source #
If the `Specification Bool` doesn't constrain the boolean you will get a TrueSpec out.
reify' ∷ ∀ a b p. (Cases (SimpleRep b) ~ '[SimpleRep b], TypeSpec b ~ TypeSpec (SimpleRep b), HasSpec (SimpleRep b), HasSimpleRep b, All HasSpec (Args (SimpleRep b)), IsProd (SimpleRep b), HasSpec a, HasSpec b, IsProductType b, IsProd a, IsPred p, GenericRequires b, ProdAsListComputes b) ⇒ Term a → (a → b) → FunTy (MapList Term (ProductAsList b)) p → Pred Source #
Like reify but pattern matches on the bound `Term b`
explanation ∷ NonEmpty String → Pred → Pred Source #
Wrap an Explain around a Pred, unless there is a simpler form.
monitor ∷ ((∀ a. Term a → a) → Property → Property) → Pred Source #
Add QuickCheck monitoring (e.g. collect or counterexample)
to a predicate. To use the monitoring in a property call monitorSpec on the Specification
containing the monitoring and a value generated from the specification.
caseOn ∷ ∀ a. (GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) ⇒ Term a → FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred Source #
branch ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ FunTy (MapList Term (Args a)) p → Weighted Binder a Source #
branchW ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ Int → FunTy (MapList Term (Args a)) p → Weighted Binder a Source #
onCon ∷ ∀ c a p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All HasSpec (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term a → FunTy (MapList Term (ConstrOf c (TheSop a))) p → Pred Source #
isCon ∷ ∀ c a. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), GenericRequires a) ⇒ Term a → Pred Source #
onJust ∷ ∀ a p. (HasSpec a, IsNormalType a, IsPred p) ⇒ Term (Maybe a) → (Term a → p) → Pred Source #
con ∷ ∀ c a r. (SimpleRep a ~ SOP (TheSop a), TypeSpec a ~ TypeSpec (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a), ResultType r ~ Term a, SOPTerm c (TheSop a), ConstrTerm (ConstrOf c (TheSop a)), GenericRequires a) ⇒ r Source #
sel ∷ ∀ n a c as. (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a, HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) ⇒ Term a → Term (At n as) Source #
Function symbols
Numbers
Booleans
Pairs
pair_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term b → Term (a, b) Source #
Either
left_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term (Either a b) Source #
right_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term b → Term (Either a b) Source #
Maybe
Higher-order functions
flip_ ∷ ∀ (t ∷ [Type] → Type → Type) a b r. (HasSpec b, HasSpec a, AppRequires t '[a, b] r) ⇒ t '[a, b] r → Term b → Term a → Term r Source #
compose_ ∷ ∀ b t1 t2 a r. (AppRequires t1 '[b] r, AppRequires t2 '[a] b) ⇒ t1 '[b] r → t2 '[a] b → Term a → Term r Source #
List
Set
Map
dom_ ∷ (HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term (Set k) Source #
rng_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term [v] Source #
lookup_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term k → Term (Map k v) → Term (Maybe v) Source #
mapMember_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term k → Term (Map k v) → Term Bool Source #
Generics
fromGeneric_ ∷ ∀ a. (GenericRequires a, AppRequires BaseW '[SimpleRep a] a) ⇒ Term (SimpleRep a) → Term a Source #
toGeneric_ ∷ ∀ a. GenericRequires a ⇒ Term a → Term (SimpleRep a) Source #
Composing specifications
chooseSpec ∷ HasSpec a ⇒ (Int, Specification a) → (Int, Specification a) → Specification a Source #
ChooseSpec is one of the ways we can Or two Specs together
This works for any kind of type that has a HasSpec instance.
If your type is a Sum type. One can use CaseOn which is much easier.
trueSpec ∷ Specification a Source #
equalSpec ∷ a → Specification a Source #
notEqualSpec ∷ ∀ a. HasSpec a ⇒ a → Specification a Source #
notMemberSpec ∷ ∀ a f. (HasSpec a, Foldable f) ⇒ f a → Specification a Source #
explainSpec ∷ [String] → Specification a → Specification a Source #
defaultMapSpec ∷ Ord k ⇒ MapSpec k v Source #
emptySpec without all the constraints
Generation, Shrinking, and Testing
Generating
genFromSpec ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Specification a → Gen a Source #
A version of genFromSpecT that simply errors if the generator fails
genFromSpecT ∷ ∀ a m. (HasCallStack, HasSpec a, MonadGenError m) ⇒ Specification a → GenT m a Source #
Generate a value that satisfies the spec. This function can fail if the spec is inconsistent, there is a dependency error, or if the underlying generators are not flexible enough.
genFromSpecWithSeed ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Int → Int → Specification a → a Source #
A version of genFromSpecT that takes a seed and a size and gives you a result
genFromSizeSpec ∷ MonadGenError m ⇒ Specification Integer → GenT m Integer Source #
Because Sizes should always be >= 0, We provide this alternate generator that can be used to replace (genFromSpecT @Integer), to ensure this important property
Shrinking
shrinkWithSpec ∷ ∀ a. HasSpec a ⇒ Specification a → a → [a] Source #
Debugging
debugSpec ∷ ∀ a. HasSpec a ⇒ Specification a → IO () Source #
A version of genFromSpecT that runs in the IO monad. Good for debugging.
Testing
conformsToSpec ∷ HasSpec a ⇒ a → Specification a → Bool Source #
conformsToSpecE ∷ ∀ a. HasSpec a ⇒ a → Specification a → NonEmpty String → Maybe (NonEmpty String) Source #
conformsToSpec with explanation. Nothing if (conformsToSpec a spec),
but (Just explanations) if not(conformsToSpec a spec).
conformsToSpecProp ∷ ∀ a. HasSpec a ⇒ a → Specification a → Property Source #
Like Constrained.Conformance.conformsToSpec but in Test.QuickCheck.Property form.
Building properties
monitorSpec ∷ Testable p ⇒ Specification a → a → p → Property Source #
Collect the monitor calls from a specification instantiated to the given value. Typically,
quickCheck $ forAll (genFromSpec spec) $ \ x -> monitorSpec spec x $ ...
forAllSpec ∷ (HasSpec a, Testable p) ⇒ Specification a → (a → p) → Property Source #
Quanitfy over a Constrained.Base.Specification.
forAllSpecShow ∷ (HasSpec a, Testable p) ⇒ Specification a → (a → String) → (a → p) → Property Source #
forAllSpecDiscard ∷ (HasSpec a, Testable p) ⇒ Specification a → (a → p) → Property Source #
Quanitfy over a Constrained.Base.Specification and discard any test where generation fails.