Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
This module exports the user-facing interface for the library.
It is supposed to contain everything you need to write constraints
and implement HasSpec
and HasSimpleRep
instances.
Synopsis
- data Specification fn a where
- MemberSpec ∷ OrdSet a → Specification fn a
- ErrorSpec ∷ NonEmpty String → Specification fn a
- SuspendedSpec ∷ HasSpec fn a ⇒ Var a → Pred fn → Specification fn a
- TypeSpec ∷ HasSpec fn a ⇒ TypeSpec fn a → OrdSet a → Specification fn a
- TrueSpec ∷ Specification fn a
- data Pred (fn ∷ [Type] → Type → Type)
- data Term (fn ∷ [Type] → Type → Type) a
- class (Typeable a, Eq a, Show a, Show (TypeSpec fn a), BaseUniverse fn) ⇒ HasSpec fn a where
- type TypeSpec (fn ∷ [Type] → Type → Type) a
- type Prerequisites fn a ∷ Constraint
- emptySpec ∷ TypeSpec fn a
- combineSpec ∷ TypeSpec fn a → TypeSpec fn a → Specification fn a
- genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec fn a → GenT m a
- conformsTo ∷ HasCallStack ⇒ a → TypeSpec fn a → Bool
- shrinkWithTypeSpec ∷ TypeSpec fn a → a → [a]
- toPreds ∷ Term fn a → TypeSpec fn a → Pred fn
- cardinalTypeSpec ∷ TypeSpec fn a → Specification fn Integer
- cardinalTrueSpec ∷ Specification fn Integer
- typeSpecHasError ∷ TypeSpec fn a → Maybe (NonEmpty String)
- alternateShow ∷ TypeSpec fn a → BinaryShow
- monadConformsTo ∷ a → TypeSpec fn a → Writer [String] Bool
- typeSpecOpt ∷ TypeSpec fn a → [a] → Specification fn a
- prerequisites ∷ Evidence (Prerequisites fn a)
- class HasSimpleRep a where
- type SimpleRep a
- type TheSop a ∷ [Type]
- toSimpleRep ∷ a → SimpleRep a
- fromSimpleRep ∷ SimpleRep a → a
- class (Num a, HasSpec fn a) ⇒ NumLike fn a where
- subtractSpec ∷ a → TypeSpec fn a → Specification fn a
- negateSpec ∷ TypeSpec fn a → Specification fn a
- safeSubtract ∷ a → a → Maybe a
- class HasSpec fn a ⇒ OrdLike fn a where
- leqSpec ∷ a → Specification fn a
- ltSpec ∷ a → Specification fn a
- geqSpec ∷ a → Specification fn a
- gtSpec ∷ a → Specification fn a
- class Forallable t e | t → e where
- fromForAllSpec ∷ (HasSpec fn t, HasSpec fn e, BaseUniverse fn) ⇒ Specification fn e → Specification fn t
- forAllToList ∷ t → [e]
- class HasSpec fn a ⇒ Foldy fn a where
- genList ∷ (BaseUniverse fn, MonadGenError m) ⇒ Specification fn a → Specification fn a → GenT m [a]
- theAddFn ∷ fn '[a, a] a
- theZero ∷ a
- class MaybeBounded a where
- lowerBound ∷ Maybe a
- upperBound ∷ Maybe a
- class FunctionLike fn where
- class (∀ as b. Show (f as b), ∀ as b. Eq (f as b), Typeable f, FunctionLike f) ⇒ Functions f fn where
- propagateSpecFun ∷ (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ f as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a
- rewriteRules ∷ (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ f as b → List (Term fn) as → Maybe (Term fn b)
- mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ f '[a] b → TypeSpec fn a → Specification fn b
- data HOLE a b where
- type BaseUniverse fn = (Functions fn fn, Member (EqFn fn) fn, Member (SetFn fn) fn, Member (BoolFn fn) fn, Member (PairFn fn) fn, Member (IntFn fn) fn, Member (OrdFn fn) fn, Member (GenericsFn fn) fn, Member (ListFn fn) fn, Member (SumFn fn) fn, Member (MapFn fn) fn, Member (FunFn fn) fn, Member (SizeFn fn) fn)
- type Member fn univ = IsMember fn univ (Path fn univ)
- type BaseFn = Fix (OneofL BaseFns)
- type BaseFns = '[EqFn, SetFn, BoolFn, PairFn, IntFn, OrdFn, GenericsFn, ListFn, SumFn, MapFn, FunFn, SizeFn]
- data Fix (fn ∷ Univ → Univ) (as ∷ [Type]) b
- type family OneofL as where ...
- type IsPred p fn = (PredLike p, UnivConstr p fn)
- type IsNormalType a = (Cases a ~ '[a], Args a ~ '[a], IsProd a, CountCases a ~ 1)
- data Value a where
- type family SOP constrs where ...
- data (c ∷ Symbol) ::: (ts ∷ [Type])
- data MapFn (fn ∷ [Type] → Type → Type) args res
- data FunFn fn args res
- data PairSpec fn a b = Cartesian (Specification fn a) (Specification fn b)
- data NumSpec (fn ∷ [Type] → Type → Type) n = NumSpecInterval (Maybe n) (Maybe n)
- data MapSpec fn k v = MapSpec {
- mapSpecHint ∷ Maybe Integer
- mapSpecMustKeys ∷ Set k
- mapSpecMustValues ∷ [v]
- mapSpecSize ∷ Specification fn Integer
- mapSpecElem ∷ Specification fn (k, v)
- mapSpecFold ∷ FoldSpec fn v
- data FoldSpec (fn ∷ [Type] → Type → Type) a where
- simplifySpec ∷ HasSpec fn a ⇒ Specification fn a → Specification fn a
- genFromSpecT ∷ ∀ fn a m. (HasCallStack, HasSpec fn a, MonadGenError m) ⇒ Specification fn a → GenT m a
- genFromSpec ∷ ∀ fn a. (HasCallStack, HasSpec fn a) ⇒ Specification fn a → Gen a
- genFromSpecWithSeed ∷ ∀ fn a. (HasCallStack, HasSpec fn a) ⇒ Int → Int → Specification fn a → a
- shrinkWithSpec ∷ ∀ fn a. HasSpec fn a ⇒ Specification fn a → a → [a]
- conformsToSpec ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a → Bool
- conformsToSpecProp ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a → Property
- monitorSpec ∷ (FunctionLike fn, Testable p) ⇒ Specification fn a → a → p → Property
- forAllSpec ∷ (HasSpec fn a, Testable p) ⇒ Specification fn a → (a → p) → Property
- forAllSpecShow ∷ (HasSpec fn a, Testable p) ⇒ Specification fn a → (a → String) → (a → p) → Property
- giveHint ∷ HasGenHint fn a ⇒ Hint a → Specification fn a
- typeSpec ∷ HasSpec fn a ⇒ TypeSpec fn a → Specification fn a
- con ∷ ∀ c a r fn. (SimpleRep a ~ SOP (TheSop a), TypeSpec fn a ~ TypeSpec fn (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), HasSpec fn a, HasSimpleRep a, r ~ FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) (Term fn a), ResultType r ~ Term fn a, SOPTerm c fn (TheSop a), ConstrTerm fn (ConstrOf c (TheSop a))) ⇒ r
- isCon ∷ ∀ c a fn. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, HasSpec fn a, HasSpec fn (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All (HasSpec fn) (Cases (SOP (TheSop a))), HasSpec fn (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term fn a → Pred fn
- onCon ∷ ∀ c a fn p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, HasSpec fn a, HasSpec fn (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All (HasSpec fn) (Cases (SOP (TheSop a))), HasSpec fn (ProdOver (ConstrOf c (TheSop a))), IsPred p fn, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All (HasSpec fn) (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term fn a → FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) p → Pred fn
- sel ∷ ∀ n fn a c as. (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as, HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) ⇒ Term fn a → Term fn (At n as)
- caseBoolSpec ∷ HasSpec fn a ⇒ Specification fn Bool → (Bool → Specification fn a) → Specification fn a
- constrained ∷ ∀ a fn p. (IsPred p fn, HasSpec fn a) ⇒ (Term fn a → p) → Specification fn a
- constrained' ∷ ∀ a fn p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec fn a, IsPred p fn) ⇒ FunTy (MapList (Term fn) (Args (SimpleRep a))) p → Specification fn a
- name ∷ String → Term fn a → Term fn a
- satisfies ∷ ∀ fn a. HasSpec fn a ⇒ Term fn a → Specification fn a → Pred fn
- letBind ∷ (HasSpec fn a, IsPred p fn) ⇒ Term fn a → (Term fn a → p) → Pred fn
- match ∷ ∀ fn p a. (HasSpec fn a, IsProductType fn a, IsPred p fn) ⇒ Term fn a → FunTy (MapList (Term fn) (ProductAsList a)) p → Pred fn
- assert ∷ (BaseUniverse fn, IsPred p fn) ⇒ p → Pred fn
- assertExplain ∷ (BaseUniverse fn, IsPred p fn) ⇒ NonEmpty String → p → Pred fn
- caseOn ∷ ∀ fn a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) ⇒ Term fn a → FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
- branch ∷ ∀ fn p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) ⇒ FunTy (MapList (Term fn) (Args a)) p → Weighted (Binder fn) a
- branchW ∷ ∀ fn p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) ⇒ Int → FunTy (MapList (Term fn) (Args a)) p → Weighted (Binder fn) a
- chooseSpec ∷ HasSpec fn a ⇒ (Int, Specification fn a) → (Int, Specification fn a) → Specification fn a
- ifElse ∷ (BaseUniverse fn, IsPred p fn, IsPred q fn) ⇒ Term fn Bool → p → q → Pred fn
- whenTrue ∷ ∀ fn p. (BaseUniverse fn, IsPred p fn) ⇒ Term fn Bool → p → Pred fn
- onJust ∷ ∀ fn a p. (BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) ⇒ Term fn (Maybe a) → (Term fn a → p) → Pred fn
- isJust ∷ ∀ fn a. (BaseUniverse fn, HasSpec fn a, IsNormalType a) ⇒ Term fn (Maybe a) → Pred fn
- reify ∷ (HasSpec fn a, HasSpec fn b, IsPred p fn) ⇒ Term fn a → (a → b) → (Term fn b → p) → Pred fn
- reify' ∷ ∀ fn a b p. (Cases (SimpleRep b) ~ '[SimpleRep b], TypeSpec fn b ~ TypeSpec fn (SimpleRep b), HasSpec fn (SimpleRep b), HasSimpleRep b, All (HasSpec fn) (Args (SimpleRep b)), IsProd (SimpleRep b), HasSpec fn a, HasSpec fn b, IsPred p fn) ⇒ Term fn a → (a → b) → FunTy (MapList (Term fn) (Args (SimpleRep b))) p → Pred fn
- reifies ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn b → Term fn a → (a → b) → Pred fn
- assertReified ∷ HasSpec fn a ⇒ Term fn a → (a → Bool) → Pred fn
- explanation ∷ NonEmpty String → Pred fn → Pred fn
- monitor ∷ ((∀ a. Term fn a → a) → Property → Property) → Pred fn
- genHint ∷ ∀ fn t. HasGenHint fn t ⇒ Hint t → Term fn t → Pred fn
- dependsOn ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn a → Term fn b → Pred fn
- forAll ∷ (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) ⇒ Term fn t → (Term fn a → p) → Pred fn
- forAll' ∷ ∀ fn t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t, HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn, IsProd (SimpleRep a), HasSpec fn a) ⇒ Term fn t → FunTy (MapList (Term fn) (Args (SimpleRep a))) p → Pred fn
- exists ∷ ∀ a p fn. (HasSpec fn a, IsPred p fn) ⇒ ((∀ b. Term fn b → b) → GE a) → (Term fn a → p) → Pred fn
- unsafeExists ∷ ∀ a p fn. (HasSpec fn a, IsPred p fn) ⇒ (Term fn a → p) → Pred fn
- fst_ ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ Term fn (a, b) → Term fn a
- snd_ ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ Term fn (a, b) → Term fn b
- pair_ ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ Term fn a → Term fn b → Term fn (a, b)
- (<=.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool
- (>=.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool
- (<.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool
- (>.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool
- (==.) ∷ HasSpec fn a ⇒ Term fn a → Term fn a → Term fn Bool
- (/=.) ∷ HasSpec fn a ⇒ Term fn a → Term fn a → Term fn Bool
- (||.) ∷ BaseUniverse fn ⇒ Term fn Bool → Term fn Bool → Term fn Bool
- member_ ∷ ∀ a fn. (HasSpec fn a, Ord a) ⇒ Term fn a → Term fn (Set a) → Term fn Bool
- subset_ ∷ (HasSpec fn a, Ord a) ⇒ Term fn (Set a) → Term fn (Set a) → Term fn Bool
- disjoint_ ∷ (HasSpec fn a, Ord a) ⇒ Term fn (Set a) → Term fn (Set a) → Term fn Bool
- singleton_ ∷ (HasSpec fn a, Ord a) ⇒ Term fn a → Term fn (Set a)
- elem_ ∷ ∀ a fn. HasSpec fn a ⇒ Term fn a → Term fn [a] → Term fn Bool
- not_ ∷ BaseUniverse fn ⇒ Term fn Bool → Term fn Bool
- foldMap_ ∷ ∀ fn a b. (BaseUniverse fn, Foldy fn b, HasSpec fn a) ⇒ (Term fn a → Term fn b) → Term fn [a] → Term fn b
- sum_ ∷ (BaseUniverse fn, Member (FunFn fn) fn, Foldy fn a) ⇒ Term fn [a] → Term fn a
- size_ ∷ ∀ a fn. (HasSpec fn (Set a), Ord a) ⇒ Term fn (Set a) → Term fn Integer
- rng_ ∷ (HasSpec fn k, HasSpec fn v, Ord k) ⇒ Term fn (Map k v) → Term fn [v]
- dom_ ∷ (HasSpec fn (Map k v), HasSpec fn k, Ord k) ⇒ Term fn (Map k v) → Term fn (Set k)
- lookup_ ∷ (HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) ⇒ Term fn k → Term fn (Map k v) → Term fn (Maybe v)
- flip_ ∷ ∀ fn a b c. (Member (FunFn fn) fn, Typeable a, Typeable b, HasSpec fn a, HasSpec fn b, HasSpec fn c) ⇒ (Term fn a → Term fn b → Term fn c) → Term fn b → Term fn a → Term fn c
- left_ ∷ (HasSpec fn a, HasSpec fn b, IsNormalType a, IsNormalType b) ⇒ Term fn a → Term fn (Either a b)
- right_ ∷ (HasSpec fn a, HasSpec fn b, IsNormalType a, IsNormalType b) ⇒ Term fn b → Term fn (Either a b)
- toGeneric_ ∷ ∀ a fn. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Term fn a → Term fn (SimpleRep a)
- fromGeneric_ ∷ ∀ a fn. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Term fn (SimpleRep a) → Term fn a
- sizeOf_ ∷ ∀ a fn. (HasSpec fn a, Sized a) ⇒ Term fn a → Term fn Integer
- length_ ∷ ∀ a fn. HasSpec fn [a] ⇒ Term fn [a] → Term fn Integer
- cNothing_ ∷ (HasSpec fn a, IsNormalType a) ⇒ Term fn (Maybe a)
- cJust_ ∷ (HasSpec fn a, IsNormalType a) ⇒ Term fn a → Term fn (Maybe a)
- null_ ∷ (HasSpec fn a, Sized a) ⇒ Term fn a → Term fn Bool
- injectFn ∷ ∀ fn fnU as b. Member fn fnU ⇒ fn as b → fnU as b
- app ∷ (HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) ⇒ fn as b → FunTy (MapList (Term fn) as) (Term fn b)
- lit ∷ Show a ⇒ a → Term fn a
- emptyNumSpec ∷ Ord a ⇒ NumSpec fn a
- combineNumSpec ∷ (HasSpec fn n, Ord n, TypeSpec fn n ~ NumSpec fn n) ⇒ NumSpec fn n → NumSpec fn n → Specification fn n
- genFromNumSpec ∷ (MonadGenError m, Show n, Random n, Ord n, Num n, MaybeBounded n) ⇒ NumSpec fn n → GenT m n
- shrinkWithNumSpec ∷ Arbitrary n ⇒ NumSpec fn n → n → [n]
- conformsToNumSpec ∷ Ord n ⇒ n → NumSpec fn n → Bool
- toPredsNumSpec ∷ (Ord n, OrdLike fn n) ⇒ Term fn n → NumSpec fn n → Pred fn
- cardinalNumSpec ∷ ∀ n fn. (Integral n, Num n, MaybeBounded n) ⇒ NumSpec fn n → Specification fn Integer
- addFn ∷ ∀ fn a. NumLike fn a ⇒ fn '[a, a] a
- toSimpleRepSpec ∷ ∀ a fn. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Specification fn a → Specification fn (SimpleRep a)
- fromSimpleRepSpec ∷ ∀ a fn. (HasSpec fn a, HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Specification fn (SimpleRep a) → Specification fn a
- algebra ∷ SOPLike constrs r ⇒ SOP constrs → ALG constrs r
- inject ∷ ∀ c constrs. Inject c constrs (SOP constrs) ⇒ FunTy (ConstrOf c constrs) (SOP constrs)
- toPred ∷ ∀ fn p. (BaseUniverse fn, PredLike p, UnivConstr p fn) ⇒ p → Pred fn
- printPlan ∷ HasSpec fn a ⇒ Specification fn a → IO ()
- module Constrained.Syntax
- module Constrained.Spec.Tree
- module Constrained.List
- module Constrained.GenT
Documentation
data Specification fn a where Source #
A `Specification fn a` denotes a set of a
s
MemberSpec | Elements of a known set |
| |
ErrorSpec ∷ NonEmpty String → Specification fn a | The empty set |
SuspendedSpec | The set described by some predicates over the bound variable. TODO: possibly we want to use a |
| |
TypeSpec | A type-specific spec |
| |
TrueSpec ∷ Specification fn a | Anything |
Instances
data Pred (fn ∷ [Type] → Type → Type) Source #
Instances
HasVariables fn (Pred fn) Source # | |
BaseUniverse fn ⇒ Monoid (Pred fn) Source # | |
BaseUniverse fn ⇒ Semigroup (Pred fn) Source # | |
Show (Pred fn) Source # | |
PredLike (Pred fn) Source # | |
Defined in Constrained.Base type UnivConstr (Pred fn) fn Source # toPredExplain ∷ ∀ (fn0 ∷ [Type] → Type → Type). (BaseUniverse fn0, UnivConstr (Pred fn) fn0) ⇒ [String] → Pred fn → Pred fn0 Source # | |
Rename (Pred fn) Source # | |
Pretty (Pred fn) Source # | |
type UnivConstr (Pred fn) fn' Source # | |
Defined in Constrained.Base |
data Term (fn ∷ [Type] → Type → Type) a Source #
Typed first order terms with function symbols from fn
.
Instances
class (Typeable a, Eq a, Show a, Show (TypeSpec fn a), BaseUniverse fn) ⇒ HasSpec fn a where Source #
This class provides the interface that allows you to extend the language
to handle a new type. In the case of types that have a generic representation
(via HasSimpleRep
) that already has an instance of HasSpec
it is sufficient
to provide an empty instance. However, for types that are used together with
specific functions in the function universe fn
it may be necessary to provide
a specific implementation of HasSpec
. This is typically necessary when the Specification
for the generic representation does not permit an implementation of propagateSpecFun
for some function.
The basic types provided in the language, Set
, `[]`, Map
, Int
, Word64
,
(,)
, Either
, etc. have instances of this class (technically (,)
and Either
have
instances derived from the instances for their generic Prod
and Sum
implementations).
Nothing
type TypeSpec (fn ∷ [Type] → Type → Type) a Source #
The `TypeSpec fn a` is the type-specific `Specification fn a`.
type Prerequisites fn a ∷ Constraint Source #
Prerequisites for the instance that are sometimes necessary
when working with e.g. Specification
s or functions in the universe.
type Prerequisites fn a = ()
emptySpec ∷ TypeSpec fn a Source #
default emptySpec ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ TypeSpec fn a Source #
combineSpec ∷ TypeSpec fn a → TypeSpec fn a → Specification fn a Source #
default combineSpec ∷ (HasSimpleRep a, HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ TypeSpec fn a → TypeSpec fn a → Specification fn a Source #
genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec fn a → GenT m a Source #
Generate a value that satisfies the Specification
.
The key property for this generator is soundness:
∀ a ∈ genFromTypeSpec spec. a conformsTo
spec
default genFromTypeSpec ∷ (HasSimpleRep a, HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ (HasCallStack, MonadGenError m) ⇒ TypeSpec fn a → GenT m a Source #
conformsTo ∷ HasCallStack ⇒ a → TypeSpec fn a → Bool Source #
Check conformance to the spec.
default conformsTo ∷ (HasSimpleRep a, HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ HasCallStack ⇒ a → TypeSpec fn a → Bool Source #
shrinkWithTypeSpec ∷ TypeSpec fn a → a → [a] Source #
Shrink an a
with the aide of a Specification
default shrinkWithTypeSpec ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ TypeSpec fn a → a → [a] Source #
toPreds ∷ Term fn a → TypeSpec fn a → Pred fn Source #
Convert a spec to predicates:
The key property here is:
∀ a. a conformsTo
spec == a conformsTo
constrained (t -> toPreds t spec)
default toPreds ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ Term fn a → TypeSpec fn a → Pred fn Source #
cardinalTypeSpec ∷ TypeSpec fn a → Specification fn Integer Source #
Compute an upper and lower bound on the number of solutions genFromTypeSpec might return
default cardinalTypeSpec ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ TypeSpec fn a → Specification fn Integer Source #
cardinalTrueSpec ∷ Specification fn 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 fn a → Maybe (NonEmpty String) Source #
alternateShow ∷ TypeSpec fn a → BinaryShow Source #
monadConformsTo ∷ a → TypeSpec fn a → Writer [String] Bool Source #
typeSpecOpt ∷ TypeSpec fn a → [a] → Specification fn 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.
prerequisites ∷ Evidence (Prerequisites fn a) Source #
Materialize the Prerequisites
dictionary. It should not be necessary to
implement this function manually.
default prerequisites ∷ Prerequisites fn a ⇒ Evidence (Prerequisites fn a) Source #
Instances
class HasSimpleRep a where Source #
Nothing
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
HasSimpleRep Foo Source # | |
HasSimpleRep Three Source # | |
HasSimpleRep FooBarBaz Source # | |
HasSimpleRep Bool Source # | |
Ord a ⇒ HasSimpleRep (NotASet a) Source # | |
HasSimpleRep (Maybe a) Source # | |
HasSimpleRep (Either a b) Source # | |
HasSimpleRep (a, b) Source # | |
HasSimpleRep (a, b, c) Source # | |
HasSimpleRep (a, b, c, d) Source # | |
HasSimpleRep (a, b, c, d, e) Source # | |
HasSimpleRep (a, b, c, d, e, g) Source # | |
HasSimpleRep (a, b, c, d, e, g, h) Source # | |
class (Num a, HasSpec fn a) ⇒ NumLike fn a where Source #
Nothing
subtractSpec ∷ a → TypeSpec fn a → Specification fn a Source #
default subtractSpec ∷ (TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, NumLike fn (SimpleRep a)) ⇒ a → TypeSpec fn a → Specification fn a Source #
negateSpec ∷ TypeSpec fn a → Specification fn a Source #
default negateSpec ∷ (TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, NumLike fn (SimpleRep a)) ⇒ TypeSpec fn a → Specification fn a Source #
safeSubtract ∷ a → a → Maybe a Source #
default safeSubtract ∷ (HasSimpleRep a, NumLike fn (SimpleRep a)) ⇒ a → a → Maybe a Source #
Instances
(HasSpec fn a, Ord a, Num a, TypeSpec fn a ~ NumSpec fn a, MaybeBounded a) ⇒ NumLike fn a Source # | |
Defined in Constrained.Base subtractSpec ∷ a → TypeSpec fn a → Specification fn a Source # negateSpec ∷ TypeSpec fn a → Specification fn a Source # safeSubtract ∷ a → a → Maybe a Source # |
class HasSpec fn a ⇒ OrdLike fn a where Source #
Nothing
leqSpec ∷ a → Specification fn a Source #
default leqSpec ∷ (TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, OrdLike fn (SimpleRep a)) ⇒ a → Specification fn a Source #
ltSpec ∷ a → Specification fn a Source #
default ltSpec ∷ (TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, OrdLike fn (SimpleRep a)) ⇒ a → Specification fn a Source #
geqSpec ∷ a → Specification fn a Source #
default geqSpec ∷ (TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, OrdLike fn (SimpleRep a)) ⇒ a → Specification fn a Source #
gtSpec ∷ a → Specification fn a Source #
default gtSpec ∷ (TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, OrdLike fn (SimpleRep a)) ⇒ a → Specification fn a Source #
Instances
(HasSpec fn a, MaybeBounded a, Num a, TypeSpec fn a ~ NumSpec fn a) ⇒ OrdLike fn a Source # | |
Defined in Constrained.Base leqSpec ∷ a → Specification fn a Source # ltSpec ∷ a → Specification fn a Source # geqSpec ∷ a → Specification fn a Source # gtSpec ∷ a → Specification fn a Source # |
class Forallable t e | t → e where Source #
Nothing
fromForAllSpec ∷ (HasSpec fn t, HasSpec fn e, BaseUniverse fn) ⇒ Specification fn e → Specification fn t Source #
default fromForAllSpec ∷ (HasSpec fn t, HasSpec fn e, HasSimpleRep t, TypeSpec fn t ~ TypeSpec fn (SimpleRep t), Forallable (SimpleRep t) e, HasSpec fn (SimpleRep t)) ⇒ Specification fn e → Specification fn t Source #
forAllToList ∷ t → [e] Source #
default forAllToList ∷ (HasSimpleRep t, Forallable (SimpleRep t) e) ⇒ t → [e] Source #
Instances
class HasSpec fn a ⇒ Foldy fn a where Source #
genList ∷ (BaseUniverse fn, MonadGenError m) ⇒ Specification fn a → Specification fn a → GenT m [a] Source #
Instances
BaseUniverse fn ⇒ Foldy fn Int16 Source # | |
Defined in Constrained.Base | |
BaseUniverse fn ⇒ Foldy fn Int32 Source # | |
Defined in Constrained.Base | |
BaseUniverse fn ⇒ Foldy fn Int64 Source # | |
Defined in Constrained.Base | |
BaseUniverse fn ⇒ Foldy fn Int8 Source # | |
Defined in Constrained.Base | |
BaseUniverse fn ⇒ Foldy fn Word16 Source # | |
Defined in Constrained.Base | |
BaseUniverse fn ⇒ Foldy fn Word32 Source # | |
Defined in Constrained.Base | |
BaseUniverse fn ⇒ Foldy fn Word64 Source # | |
Defined in Constrained.Base | |
BaseUniverse fn ⇒ Foldy fn Word8 Source # | |
Defined in Constrained.Base | |
BaseUniverse fn ⇒ Foldy fn Integer Source # | |
Defined in Constrained.Base | |
BaseUniverse fn ⇒ Foldy fn Natural Source # | |
Defined in Constrained.Base | |
BaseUniverse fn ⇒ Foldy fn Int Source # | |
Defined in Constrained.Base |
class MaybeBounded a where Source #
Nothing
lowerBound ∷ Maybe a Source #
default lowerBound ∷ Bounded a ⇒ Maybe a Source #
upperBound ∷ Maybe a Source #
default upperBound ∷ Bounded a ⇒ Maybe a Source #
Instances
MaybeBounded Int16 Source # | |
Defined in Constrained.Base | |
MaybeBounded Int32 Source # | |
Defined in Constrained.Base | |
MaybeBounded Int64 Source # | |
Defined in Constrained.Base | |
MaybeBounded Int8 Source # | |
Defined in Constrained.Base | |
MaybeBounded Word16 Source # | |
Defined in Constrained.Base | |
MaybeBounded Word32 Source # | |
Defined in Constrained.Base | |
MaybeBounded Word64 Source # | |
Defined in Constrained.Base | |
MaybeBounded Word8 Source # | |
Defined in Constrained.Base | |
MaybeBounded Integer Source # | |
Defined in Constrained.Base | |
MaybeBounded Natural Source # | |
Defined in Constrained.Base | |
MaybeBounded Float Source # | |
Defined in Constrained.Base | |
MaybeBounded Int Source # | |
Defined in Constrained.Base | |
MaybeBounded (Ratio Integer) Source # | |
Defined in Constrained.Base |
class FunctionLike fn where Source #
Instances
FunctionLike fn ⇒ FunctionLike (FunFn fn) Source # | |
FunctionLike (GenericsFn fn) Source # | |
Defined in Constrained.Spec.Generics | |
FunctionLike (IntFn fn) Source # | |
FunctionLike fn ⇒ FunctionLike (ListFn fn) Source # | |
FunctionLike (OrdFn fn) Source # | |
FunctionLike (SizeFn fn) Source # | |
FunctionLike (TreeFn fn) Source # | |
FunctionLike (BoolFn fn) Source # | |
FunctionLike (EqFn fn) Source # | |
FunctionLike (fn (Fix fn)) ⇒ FunctionLike (Fix fn) Source # | |
FunctionLike (MapFn fn) Source # | |
FunctionLike (PairFn fn) Source # | |
FunctionLike (SetFn fn) Source # | |
FunctionLike (SumFn fn) Source # | |
(FunctionLike (fn fnU), FunctionLike (fn' fnU)) ⇒ FunctionLike (Oneof fn fn' fnU) Source # | |
class (∀ as b. Show (f as b), ∀ as b. Eq (f as b), Typeable f, FunctionLike f) ⇒ Functions f fn where Source #
propagateSpecFun ∷ (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ f as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source #
rewriteRules ∷ (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ f as b → List (Term fn) as → Maybe (Term fn b) Source #
mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ f '[a] b → TypeSpec fn a → Specification fn b Source #
Instances
This is used together with ListCtx
to form
just the arguments to `f vs Ctx vs'` - replacing
Ctx
with HOLE
- to provide to propagateSpecFun
.
type BaseUniverse fn = (Functions fn fn, Member (EqFn fn) fn, Member (SetFn fn) fn, Member (BoolFn fn) fn, Member (PairFn fn) fn, Member (IntFn fn) fn, Member (OrdFn fn) fn, Member (GenericsFn fn) fn, Member (ListFn fn) fn, Member (SumFn fn) fn, Member (MapFn fn) fn, Member (FunFn fn) fn, Member (SizeFn fn) fn) Source #
A minimal Universe contains functions for a bunch of different things.
type BaseFns = '[EqFn, SetFn, BoolFn, PairFn, IntFn, OrdFn, GenericsFn, ListFn, SumFn, MapFn, FunFn, SizeFn] Source #
data Fix (fn ∷ Univ → Univ) (as ∷ [Type]) b Source #
Instances
IsMember fn (fn' (Fix fn')) path ⇒ IsMember fn (Fix fn') ('PFix ': path) Source # | |
FunctionLike (fn (Fix fn)) ⇒ FunctionLike (Fix fn) Source # | |
(Typeable fn, Functions (fn (Fix fn)) (Fix fn)) ⇒ Functions (Fix fn) (Fix fn) Source # | |
Defined in Constrained.Instances propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec (Fix fn) a, HasSpec (Fix fn) b, All (HasSpec (Fix fn)) as) ⇒ Fix fn as b → ListCtx Value as (HOLE a) → Specification (Fix fn) b → Specification (Fix fn) a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec (Fix fn) b, All (HasSpec (Fix fn)) as) ⇒ Fix fn as b → List (Term (Fix fn)) as → Maybe (Term (Fix fn) b) Source # mapTypeSpec ∷ (HasSpec (Fix fn) a, HasSpec (Fix fn) b) ⇒ Fix fn '[a] b → TypeSpec (Fix fn) a → Specification (Fix fn) b Source # | |
Show (fn (Fix fn) as b) ⇒ Show (Fix fn as b) Source # | |
Eq (fn (Fix fn) as b) ⇒ Eq (Fix fn as b) Source # | |
type family OneofL as where ... Source #
Build a balanced tree of Oneof
from a list of function universes.
NOTE: it is important that this is a balanced tree as that reduces the amount of
overhead in injectFn
and extractFn
from `O(n)` to `O(log(n))`. Surprisingly,
we've observed this making more than 10% difference in runtime on some generation
tasks even though the list as
is typically small (< 20 elements).
type IsPred p fn = (PredLike p, UnivConstr p fn) Source #
type IsNormalType a = (Cases a ~ '[a], Args a ~ '[a], IsProd a, CountCases a ~ 1) Source #
data (c ∷ Symbol) ::: (ts ∷ [Type]) Source #
A constructor name with the types of its arguments
Instances
TypeList prod ⇒ Inject c ((c ::: prod) ': (prod' ': constrs)) r Source # | |
TypeList prod ⇒ Inject c '[c ::: prod] r Source # | |
(FunTy (ConstrOf c ((c' ::: prod) ': (con ': constrs))) r ~ FunTy (ConstrOf c (con ': constrs)) r, Inject c (con ': constrs) r) ⇒ Inject c ((c' ::: prod) ': (con ': constrs)) r Source # | |
(TypeList prod, SOPLike (con ': cases) r) ⇒ SOPLike ((c ::: prod) ': (con ': cases)) r Source # | |
TypeList prod ⇒ SOPLike '[c ::: prod] r Source # | |
SopList (x' ': xs) (y ': ys) ⇒ SopList ((c ::: x) ': (x' ': xs)) (y ': ys) Source # | |
Defined in Constrained.Base injectSOPLeft ∷ SOP ((c ::: x) ': (x' ': xs)) → SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) Source # injectSOPRight ∷ SOP (y ': ys) → SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) Source # caseSOP ∷ SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) → Sum (SOP ((c ::: x) ': (x' ': xs))) (SOP (y ': ys)) Source # | |
SopList '[c ::: x] (y ': ys) Source # | |
data MapFn (fn ∷ [Type] → Type → Type) args res Source #
Instances
FunctionLike (MapFn fn) Source # | |
BaseUniverse fn ⇒ Functions (MapFn fn) fn Source # | |
Defined in Constrained.Spec.Map propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ MapFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ MapFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ MapFn fn '[a] b → TypeSpec fn a → Specification fn b Source # | |
Show (MapFn fn args res) Source # | |
Eq (MapFn fn args res) Source # | |
data FunFn fn args res Source #
Instances
FunctionLike fn ⇒ FunctionLike (FunFn fn) Source # | |
(BaseUniverse fn, Member (FunFn fn) fn) ⇒ Functions (FunFn fn) fn Source # | |
Defined in Constrained.Base propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ FunFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ FunFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ FunFn fn '[a] b → TypeSpec fn a → Specification fn b Source # | |
Show (FunFn fn args res) Source # | |
Typeable fn ⇒ Eq (FunFn fn args res) Source # | |
Cartesian (Specification fn a) (Specification fn b) |
data NumSpec (fn ∷ [Type] → Type → Type) n Source #
NumSpecInterval (Maybe n) (Maybe n) |
Instances
(Arbitrary a, Ord a) ⇒ Arbitrary (NumSpec fn a) Source # | |
Ord n ⇒ Monoid (NumSpec fn n) Source # | |
Ord n ⇒ Semigroup (NumSpec fn n) Source # | |
Num (NumSpec fn Integer) Source # | |
Defined in Constrained.Base (+) ∷ NumSpec fn Integer → NumSpec fn Integer → NumSpec fn Integer Source # (-) ∷ NumSpec fn Integer → NumSpec fn Integer → NumSpec fn Integer Source # (*) ∷ NumSpec fn Integer → NumSpec fn Integer → NumSpec fn Integer Source # negate ∷ NumSpec fn Integer → NumSpec fn Integer Source # abs ∷ NumSpec fn Integer → NumSpec fn Integer Source # | |
Show n ⇒ Show (NumSpec fn n) Source # | |
Ord n ⇒ Eq (NumSpec fn n) Source # | |
MapSpec | |
|
Instances
data FoldSpec (fn ∷ [Type] → Type → Type) a where Source #
NoFold ∷ FoldSpec fn a | |
FoldSpec ∷ ∀ b fn a. (HasSpec fn a, HasSpec fn b, Foldy fn b, Member (ListFn fn) fn, BaseUniverse fn) ⇒ fn '[a] b → Specification fn b → FoldSpec fn a |
Instances
HasSpec fn a ⇒ Pretty (WithPrec (FoldSpec fn a)) Source # | |
Arbitrary (FoldSpec fn (Map k v)) Source # | |
Arbitrary (FoldSpec fn (Set a)) Source # | |
(HasSpec fn a, HasSpec fn b, Arbitrary (FoldSpec fn a), Arbitrary (FoldSpec fn b)) ⇒ Arbitrary (FoldSpec fn (a, b)) Source # | |
(Arbitrary a, Arbitrary (TypeSpec fn a), Foldy fn a, BaseUniverse fn) ⇒ Arbitrary (FoldSpec fn a) Source # | |
HasSpec fn a ⇒ Show (FoldSpec fn a) Source # | |
HasSpec fn a ⇒ Pretty (FoldSpec fn a) Source # | |
simplifySpec ∷ HasSpec fn a ⇒ Specification fn a → Specification fn a Source #
genFromSpecT ∷ ∀ fn a m. (HasCallStack, HasSpec fn a, MonadGenError m) ⇒ Specification fn 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.
genFromSpec ∷ ∀ fn a. (HasCallStack, HasSpec fn a) ⇒ Specification fn a → Gen a Source #
A version of genFromSpecT
that simply errors if the generator fails
genFromSpecWithSeed ∷ ∀ fn a. (HasCallStack, HasSpec fn a) ⇒ Int → Int → Specification fn a → a Source #
A version of genFromSpecT
that takes a seed and a size and gives you a result
shrinkWithSpec ∷ ∀ fn a. HasSpec fn a ⇒ Specification fn a → a → [a] Source #
conformsToSpec ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a → Bool Source #
conformsToSpecProp ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a → Property Source #
monitorSpec ∷ (FunctionLike fn, Testable p) ⇒ Specification fn 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 fn a, Testable p) ⇒ Specification fn a → (a → p) → Property Source #
forAllSpecShow ∷ (HasSpec fn a, Testable p) ⇒ Specification fn a → (a → String) → (a → p) → Property Source #
giveHint ∷ HasGenHint fn a ⇒ Hint a → Specification fn a Source #
con ∷ ∀ c a r fn. (SimpleRep a ~ SOP (TheSop a), TypeSpec fn a ~ TypeSpec fn (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), HasSpec fn a, HasSimpleRep a, r ~ FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) (Term fn a), ResultType r ~ Term fn a, SOPTerm c fn (TheSop a), ConstrTerm fn (ConstrOf c (TheSop a))) ⇒ r Source #
isCon ∷ ∀ c a fn. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, HasSpec fn a, HasSpec fn (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All (HasSpec fn) (Cases (SOP (TheSop a))), HasSpec fn (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term fn a → Pred fn Source #
onCon ∷ ∀ c a fn p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, HasSpec fn a, HasSpec fn (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All (HasSpec fn) (Cases (SOP (TheSop a))), HasSpec fn (ProdOver (ConstrOf c (TheSop a))), IsPred p fn, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All (HasSpec fn) (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term fn a → FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) p → Pred fn Source #
sel ∷ ∀ n fn a c as. (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as, HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) ⇒ Term fn a → Term fn (At n as) Source #
caseBoolSpec ∷ HasSpec fn a ⇒ Specification fn Bool → (Bool → Specification fn a) → Specification fn a Source #
If the `Specification fn Bool` doesn't constrain the boolean you will get a TrueSpec
out.
constrained ∷ ∀ a fn p. (IsPred p fn, HasSpec fn a) ⇒ (Term fn a → p) → Specification fn a Source #
constrained' ∷ ∀ a fn p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec fn a, IsPred p fn) ⇒ FunTy (MapList (Term fn) (Args (SimpleRep a))) p → Specification fn a Source #
Like constrained
but pattern matches on the bound `Term fn a`
match ∷ ∀ fn p a. (HasSpec fn a, IsProductType fn a, IsPred p fn) ⇒ Term fn a → FunTy (MapList (Term fn) (ProductAsList a)) p → Pred fn Source #
assertExplain ∷ (BaseUniverse fn, IsPred p fn) ⇒ NonEmpty String → p → Pred fn Source #
caseOn ∷ ∀ fn a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) ⇒ Term fn a → FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) Source #
branch ∷ ∀ fn p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) ⇒ FunTy (MapList (Term fn) (Args a)) p → Weighted (Binder fn) a Source #
branchW ∷ ∀ fn p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) ⇒ Int → FunTy (MapList (Term fn) (Args a)) p → Weighted (Binder fn) a Source #
chooseSpec ∷ HasSpec fn a ⇒ (Int, Specification fn a) → (Int, Specification fn a) → Specification fn a Source #
onJust ∷ ∀ fn a p. (BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) ⇒ Term fn (Maybe a) → (Term fn a → p) → Pred fn Source #
isJust ∷ ∀ fn a. (BaseUniverse fn, HasSpec fn a, IsNormalType a) ⇒ Term fn (Maybe a) → Pred fn Source #
reify ∷ (HasSpec fn a, HasSpec fn b, IsPred p fn) ⇒ Term fn a → (a → b) → (Term fn b → p) → Pred fn Source #
reify' ∷ ∀ fn a b p. (Cases (SimpleRep b) ~ '[SimpleRep b], TypeSpec fn b ~ TypeSpec fn (SimpleRep b), HasSpec fn (SimpleRep b), HasSimpleRep b, All (HasSpec fn) (Args (SimpleRep b)), IsProd (SimpleRep b), HasSpec fn a, HasSpec fn b, IsPred p fn) ⇒ Term fn a → (a → b) → FunTy (MapList (Term fn) (Args (SimpleRep b))) p → Pred fn Source #
Like reify
but pattern matches on the bound `Term fn b`
monitor ∷ ((∀ a. Term fn a → a) → Property → Property) → Pred fn 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.
forAll ∷ (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) ⇒ Term fn t → (Term fn a → p) → Pred fn Source #
forAll' ∷ ∀ fn t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t, HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn, IsProd (SimpleRep a), HasSpec fn a) ⇒ Term fn t → FunTy (MapList (Term fn) (Args (SimpleRep a))) p → Pred fn Source #
Like forAll
but pattern matches on the `Term fn a`
exists ∷ ∀ a p fn. (HasSpec fn a, IsPred p fn) ⇒ ((∀ b. Term fn b → b) → GE a) → (Term fn a → p) → Pred fn Source #
foldMap_ ∷ ∀ fn a b. (BaseUniverse fn, Foldy fn b, HasSpec fn a) ⇒ (Term fn a → Term fn b) → Term fn [a] → Term fn b Source #
size_ ∷ ∀ a fn. (HasSpec fn (Set a), Ord a) ⇒ Term fn (Set a) → Term fn Integer Source #
special instance of sizeOf (for Sets) for backward compatibility
lookup_ ∷ (HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) ⇒ Term fn k → Term fn (Map k v) → Term fn (Maybe v) Source #
flip_ ∷ ∀ fn a b c. (Member (FunFn fn) fn, Typeable a, Typeable b, HasSpec fn a, HasSpec fn b, HasSpec fn c) ⇒ (Term fn a → Term fn b → Term fn c) → Term fn b → Term fn a → Term fn c Source #
left_ ∷ (HasSpec fn a, HasSpec fn b, IsNormalType a, IsNormalType b) ⇒ Term fn a → Term fn (Either a b) Source #
right_ ∷ (HasSpec fn a, HasSpec fn b, IsNormalType a, IsNormalType b) ⇒ Term fn b → Term fn (Either a b) Source #
toGeneric_ ∷ ∀ a fn. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Term fn a → Term fn (SimpleRep a) Source #
fromGeneric_ ∷ ∀ a fn. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Term fn (SimpleRep a) → Term fn a Source #
length_ ∷ ∀ a fn. HasSpec fn [a] ⇒ Term fn [a] → Term fn Integer Source #
special instance of sizeOf (for Lists) for backward compatibility
app ∷ (HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) ⇒ fn as b → FunTy (MapList (Term fn) as) (Term fn b) Source #
emptyNumSpec ∷ Ord a ⇒ NumSpec fn a Source #
combineNumSpec ∷ (HasSpec fn n, Ord n, TypeSpec fn n ~ NumSpec fn n) ⇒ NumSpec fn n → NumSpec fn n → Specification fn n Source #
genFromNumSpec ∷ (MonadGenError m, Show n, Random n, Ord n, Num n, MaybeBounded n) ⇒ NumSpec fn n → GenT m n Source #
shrinkWithNumSpec ∷ Arbitrary n ⇒ NumSpec fn n → n → [n] Source #
cardinalNumSpec ∷ ∀ n fn. (Integral n, Num n, MaybeBounded n) ⇒ NumSpec fn n → Specification fn Integer Source #
A generic function to use as an instance for the HasSpec method
cardinalTypeSpec :: HasSpec fn a => TypeSpec fn a -> Specification fn Integer
for types n
such that (TypeSpec n ~ NumSpec n)
toSimpleRepSpec ∷ ∀ a fn. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Specification fn a → Specification fn (SimpleRep a) Source #
fromSimpleRepSpec ∷ ∀ a fn. (HasSpec fn a, HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Specification fn (SimpleRep a) → Specification fn a Source #
inject ∷ ∀ c constrs. Inject c constrs (SOP constrs) ⇒ FunTy (ConstrOf c constrs) (SOP constrs) Source #
toPred ∷ ∀ fn p. (BaseUniverse fn, PredLike p, UnivConstr p fn) ⇒ p → Pred fn Source #
module Constrained.Syntax
module Constrained.Spec.Tree
module Constrained.List
module Constrained.GenT