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
- ExplainSpec ∷ [String] → Specification fn a → Specification fn a
- MemberSpec ∷ NonEmpty 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
- guardTypeSpec ∷ [String] → TypeSpec fn 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
- genSizedList ∷ (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Integer → Specification fn a → Specification fn a → GenT m [a]
- noNegativeValues ∷ Bool
- 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
- class Sized fn t where
- sizeOf ∷ t → Integer
- liftSizeSpec ∷ HasSpec fn t ⇒ SizeSpec fn → [Integer] → Specification fn t
- liftMemberSpec ∷ HasSpec fn t ⇒ OrdSet Integer → Specification fn t
- sizeOfTypeSpec ∷ HasSpec fn t ⇒ TypeSpec fn t → Specification fn Integer
- simplifySpec ∷ HasSpec fn a ⇒ Specification fn a → Specification fn a
- addToErrorSpec ∷ NonEmpty String → 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 (Set a), Ord a, Show a, Typeable 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)
- union_ ∷ ∀ a fn. (HasSpec fn a, Ord a) ⇒ Term fn (Set a) → Term fn (Set a) → Term fn (Set a)
- fromList_ ∷ ∀ a fn. (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. (Foldy fn b, HasSpec fn a) ⇒ (Term fn a → Term fn b) → Term fn [a] → Term fn b
- sum_ ∷ Foldy fn a ⇒ Term fn [a] → Term fn a
- (++.) ∷ HasSpec fn a ⇒ Term fn [a] → Term fn [a] → Term fn [a]
- singletonList_ ∷ HasSpec 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. (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 fn 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 fn a) ⇒ Term fn a → Term fn Bool
- rangeSize ∷ Integer → Integer → SizeSpec fn
- hasSize ∷ (HasSpec fn t, Sized fn t) ⇒ SizeSpec fn → Specification fn t
- 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, 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
ExplainSpec ∷ [String] → Specification fn a → Specification fn a | Explain a Specification |
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
HasVariables fn (Term fn a) Source # | |
HasVariables fn (List (Term fn) as) Source # | |
HasSpec fn a ⇒ Pretty (WithPrec (Term fn a)) Source # | |
(Ord a, Show a, Typeable a, HasSpec fn (Set a)) ⇒ Monoid (Term fn (Set a)) Source # | |
(Ord a, Show a, Typeable a, HasSpec fn (Set a)) ⇒ Semigroup (Term fn (Set a)) Source # | |
NumLike fn a ⇒ Num (Term fn a) Source # | |
HasSpec fn a ⇒ Show (Term fn a) Source # | |
BaseUniverse fn ⇒ PredLike (Term fn Bool) Source # | |
Defined in Constrained.Base type UnivConstr (Term fn Bool) fn Source # toPredExplain ∷ ∀ (fn0 ∷ [Type] → Type → Type). (BaseUniverse fn0, UnivConstr (Term fn Bool) fn0) ⇒ [String] → Term fn Bool → Pred fn0 Source # | |
Rename (Term fn a) Source # | |
HasSpec fn a ⇒ Eq (Term fn a) Source # | |
HasSpec fn a ⇒ Pretty (Term fn a) Source # | |
type UnivConstr (Term fn Bool) fn' Source # | |
Defined in Constrained.Base |
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.
guardTypeSpec ∷ [String] → TypeSpec fn a → Specification fn a Source #
This can be used to detect self inconsistencies in a (TypeSpec fn t)
Note this is similar to typeSpecHasError
, and the default
value for typeSpecHasError
is written in terms of guadTypeSpec
Both typeSpecHasError
and guardTypeSpec
can be set individually.
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
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 #
theAddFn ∷ fn '[a, a] a Source #
genSizedList ∷ (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Integer → Specification fn a → Specification fn a → GenT m [a] Source #
noNegativeValues ∷ Bool Source #
Instances
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
class FunctionLike fn where Source #
Instances
FunctionLike fn ⇒ FunctionLike (FunFn fn) Source # | |
FunctionLike (GenericsFn fn) Source # | |
Defined in Constrained.Spec.Generics sem ∷ ∀ (as ∷ [Type]) b. GenericsFn fn as b → FunTy as b Source # | |
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
BaseUniverse 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 # | |
BaseUniverse fn ⇒ Functions (GenericsFn fn) fn Source # | |
Defined in Constrained.Spec.Generics propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ GenericsFn 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) ⇒ GenericsFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ GenericsFn fn '[a] b → TypeSpec fn a → Specification fn b Source # | |
BaseUniverse fn ⇒ Functions (IntFn 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) ⇒ IntFn 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) ⇒ IntFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ IntFn fn '[a] b → TypeSpec fn a → Specification fn b Source # | |
BaseUniverse fn ⇒ Functions (ListFn 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) ⇒ ListFn 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) ⇒ ListFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ ListFn fn '[a] b → TypeSpec fn a → Specification fn b Source # | |
BaseUniverse fn ⇒ Functions (OrdFn 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) ⇒ OrdFn 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) ⇒ OrdFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ OrdFn fn '[a] b → TypeSpec fn a → Specification fn b Source # | |
(BaseUniverse fn, HasSpec fn Integer) ⇒ Functions (SizeFn 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) ⇒ SizeFn 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) ⇒ SizeFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ SizeFn fn '[a] b → TypeSpec fn a → Specification fn b Source # | |
(Member (TreeFn fn) fn, BaseUniverse fn) ⇒ Functions (TreeFn fn) fn Source # | |
Defined in Constrained.Spec.Tree propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ TreeFn 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) ⇒ TreeFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ TreeFn fn '[a] b → TypeSpec fn a → Specification fn b Source # | |
BaseUniverse fn ⇒ Functions (BoolFn fn) fn Source # | |
Defined in Constrained.Instances propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ BoolFn 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) ⇒ BoolFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ BoolFn fn '[a] b → TypeSpec fn a → Specification fn b Source # | |
BaseUniverse fn ⇒ Functions (EqFn fn) fn Source # | |
Defined in Constrained.Instances propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ EqFn 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) ⇒ EqFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ EqFn fn '[a] b → TypeSpec fn a → Specification fn b 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 # | |
BaseUniverse fn ⇒ Functions (PairFn fn) fn Source # | |
Defined in Constrained.Spec.Pairs propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ PairFn 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) ⇒ PairFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ PairFn fn '[a] b → TypeSpec fn a → Specification fn b Source # | |
BaseUniverse fn ⇒ Functions (SetFn 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) ⇒ SetFn 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) ⇒ SetFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ SetFn fn '[a] b → TypeSpec fn a → Specification fn b Source # | |
BaseUniverse fn ⇒ Functions (SumFn fn) fn Source # | |
Defined in Constrained.Spec.Generics propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ SumFn 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) ⇒ SumFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ SumFn fn '[a] b → TypeSpec fn a → Specification fn b 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 # | |
(Typeable fn, Typeable fn', Typeable fnU, Functions (fn fnU) fnU, Functions (fn' fnU) fnU) ⇒ Functions (Oneof fn fn' fnU) fnU Source # | |
Defined in Constrained.Instances propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fnU a, HasSpec fnU b, All (HasSpec fnU) as) ⇒ Oneof fn fn' fnU as b → ListCtx Value as (HOLE a) → Specification fnU b → Specification fnU a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fnU b, All (HasSpec fnU) as) ⇒ Oneof fn fn' fnU as b → List (Term fnU) as → Maybe (Term fnU b) Source # mapTypeSpec ∷ (HasSpec fnU a, HasSpec fnU b) ⇒ Oneof fn fn' fnU '[a] b → TypeSpec fnU a → Specification fnU b Source # |
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 # | |
Defined in Constrained.Univ | |
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 ⇒ 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 (-) ∷ NumSpec fn Integer → NumSpec fn Integer → NumSpec fn Integer (*) ∷ NumSpec fn Integer → NumSpec fn Integer → NumSpec fn Integer negate ∷ NumSpec fn Integer → NumSpec fn Integer abs ∷ NumSpec fn Integer → NumSpec fn Integer signum ∷ NumSpec fn Integer → NumSpec fn Integer fromInteger ∷ Integer → NumSpec fn Integer | |
Show n ⇒ Show (NumSpec fn n) Source # | |
Ord n ⇒ Eq (NumSpec fn n) Source # | |
MapSpec | |
|
Instances
(HasSpec fn (k, v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) ⇒ Pretty (WithPrec (MapSpec fn k v)) Source # | |
(Arbitrary k, Arbitrary v, Arbitrary (TypeSpec fn k), Arbitrary (TypeSpec fn v), Ord k, HasSpec fn k, Foldy fn v) ⇒ Arbitrary (MapSpec fn k v) Source # | |
Generic (MapSpec fn k v) Source # | |
(HasSpec fn (k, v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) ⇒ Show (MapSpec fn k v) Source # | |
type Rep (MapSpec fn k v) Source # | |
Defined in Constrained.Spec.Map type Rep (MapSpec fn k v) = D1 ('MetaData "MapSpec" "Constrained.Spec.Map" "constrained-generators-0.2.0.0-inplace" 'False) (C1 ('MetaCons "MapSpec" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mapSpecHint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Integer)) :*: (S1 ('MetaSel ('Just "mapSpecMustKeys") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set k)) :*: S1 ('MetaSel ('Just "mapSpecMustValues") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [v]))) :*: (S1 ('MetaSel ('Just "mapSpecSize") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Specification fn Integer)) :*: (S1 ('MetaSel ('Just "mapSpecElem") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Specification fn (k, v))) :*: S1 ('MetaSel ('Just "mapSpecFold") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FoldSpec fn v)))))) |
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 (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 # | |
class Sized fn t where Source #
Nothing
liftSizeSpec ∷ HasSpec fn t ⇒ SizeSpec fn → [Integer] → Specification fn t Source #
default liftSizeSpec ∷ (HasSpec fn t, HasSimpleRep t, Sized fn (SimpleRep t), HasSpec fn (SimpleRep t), TypeSpec fn t ~ TypeSpec fn (SimpleRep t)) ⇒ SizeSpec fn → [Integer] → Specification fn t Source #
liftMemberSpec ∷ HasSpec fn t ⇒ OrdSet Integer → Specification fn t Source #
default liftMemberSpec ∷ (HasSpec fn t, HasSpec fn (SimpleRep t), HasSimpleRep t, Sized fn (SimpleRep t), TypeSpec fn t ~ TypeSpec fn (SimpleRep t)) ⇒ OrdSet Integer → Specification fn t Source #
sizeOfTypeSpec ∷ HasSpec fn t ⇒ TypeSpec fn t → Specification fn Integer Source #
Instances
Ord a ⇒ Sized fn (Set a) Source # | |
Defined in Constrained.Base sizeOf ∷ Set a → Integer Source # liftSizeSpec ∷ SizeSpec fn → [Integer] → Specification fn (Set a) Source # liftMemberSpec ∷ OrdSet Integer → Specification fn (Set a) Source # sizeOfTypeSpec ∷ TypeSpec fn (Set a) → Specification fn Integer Source # | |
Sized fn [a] Source # | |
Defined in Constrained.Base sizeOf ∷ [a] → Integer Source # liftSizeSpec ∷ SizeSpec fn → [Integer] → Specification fn [a] Source # liftMemberSpec ∷ OrdSet Integer → Specification fn [a] Source # sizeOfTypeSpec ∷ TypeSpec fn [a] → Specification fn Integer Source # | |
Ord a ⇒ Sized fn (Map a b) Source # | |
Defined in Constrained.Spec.Map sizeOf ∷ Map a b → Integer Source # liftSizeSpec ∷ SizeSpec fn → [Integer] → Specification fn (Map a b) Source # liftMemberSpec ∷ OrdSet Integer → Specification fn (Map a b) Source # sizeOfTypeSpec ∷ TypeSpec fn (Map a b) → Specification fn Integer Source # |
simplifySpec ∷ HasSpec fn a ⇒ Specification fn a → Specification fn a Source #
addToErrorSpec ∷ NonEmpty String → Specification fn a → Specification fn a Source #
Add the explanations, if it's an ErrorSpec, else drop them
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`
explanation ∷ NonEmpty String → Pred fn → Pred fn Source #
Wrap an Explain
around a Pred, unless there is a simpler form.
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 #
subset_ ∷ (HasSpec fn (Set a), Ord a, Show a, Typeable a) ⇒ Term fn (Set a) → Term fn (Set a) → Term fn Bool Source #
union_ ∷ ∀ a fn. (HasSpec fn a, Ord a) ⇒ Term fn (Set a) → Term fn (Set a) → Term fn (Set a) Source #
foldMap_ ∷ ∀ fn a b. (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. (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 #
conformsToNumSpec ∷ Ord n ⇒ n → NumSpec fn n → Bool Source #
cardinalNumSpec ∷ ∀ n fn. (Integral 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 #
printPlan ∷ HasSpec fn a ⇒ Specification fn a → IO () Source #
module Constrained.Syntax
module Constrained.Spec.Tree
module Constrained.List
module Constrained.GenT