Safe Haskell	Safe-Inferred
Language	Haskell2010

Constrained.Base

Contents

Orphan instances

Description

This module contains most of the implementation of the framework.

NOTE: This is a very big module. Splitting it up would be a nice thing to do but it's not very easy. The problem is that a lot of the things in here depend on each other via a cycle like Pred depends on Term which depend on HasSpec which depends on Specification and Generic and Specification depends in turn on Pred and so on.

Synopsis

data Term (fn ∷ [Type] → Type → Type) a where
- App ∷ (Typeable as, TypeList as, All (HasSpec fn) as, HasSpec fn b, BaseUniverse fn) ⇒ fn as b → List (Term fn) as → Term fn b
- Lit ∷ Show a ⇒ a → Term fn a
- V ∷ HasSpec fn a ⇒ Var a → Term fn a
type HasSpecImpliesEq fn a f = HasSpec fn a ⇒ Eq (f a) ∷ Constraint
data Binder fn a where
- (:->) ∷ HasSpec fn a ⇒ Var a → Pred fn → Binder fn a
data Pred (fn ∷ [Type] → Type → Type) where
- Monitor ∷ ((∀ a. Term fn a → a) → Property → Property) → Pred fn
- Block ∷ [Pred fn] → Pred fn
- Exists ∷ ((∀ b. Term fn b → b) → GE a) → Binder fn a → Pred fn
- Subst ∷ HasSpec fn a ⇒ Var a → Term fn a → Pred fn → Pred fn
- Let ∷ Term fn a → Binder fn a → Pred fn
- Assert ∷ BaseUniverse fn ⇒ Term fn Bool → Pred fn
- Reifies ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn b → Term fn a → (a → b) → 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) ⇒ Term fn t → Binder fn a → Pred fn
- Case ∷ HasSpec fn (SumOver as) ⇒ Term fn (SumOver as) → List (Weighted (Binder fn)) as → Pred fn
- When ∷ HasSpec fn Bool ⇒ Term fn Bool → Pred fn → Pred fn
- GenHint ∷ HasGenHint fn a ⇒ Hint a → Term fn a → Pred fn
- TruePred ∷ Pred fn
- FalsePred ∷ NonEmpty String → Pred fn
- Explain ∷ NonEmpty String → Pred fn → Pred fn
falsePred1 ∷ String → Pred fn
data Weighted f a = Weighted {
- weight ∷ Maybe Int
- thing ∷ f a
}
mapWeighted ∷ (f a → g b) → Weighted f a → Weighted g b
traverseWeighted ∷ Applicative m ⇒ (f a → m (g a)) → Weighted f a → m (Weighted g a)
data Ctx (fn ∷ [Type] → Type → Type) v a where
- CtxHOLE ∷ HasSpec fn v ⇒ Ctx fn v v
- CtxApp ∷ (HasSpec fn b, TypeList as, Typeable as, All (HasSpec fn) as) ⇒ fn as b → ListCtx Value as (Ctx fn v) → Ctx fn v b
data HOLE a b where
- HOLE ∷ HOLE a a
toCtx ∷ ∀ m fn v a. (BaseUniverse fn, Typeable v, MonadGenError m, HasCallStack, HasSpec fn a, HasSpec fn v) ⇒ Var v → Term fn a → m (Ctx fn v a)
toCtxList ∷ ∀ m fn v as. (BaseUniverse fn, All (HasSpec fn) as, HasSpec fn v, Typeable v, MonadGenError m, HasCallStack) ⇒ Var v → List (Term fn) as → m (ListCtx Value as (Ctx fn v))
runTerm ∷ MonadGenError m ⇒ Env → Term fn a → m a
monitorSpec ∷ (FunctionLike fn, Testable p) ⇒ Specification fn a → a → p → Property
monitorPred ∷ ∀ fn m. (FunctionLike fn, MonadGenError m) ⇒ Env → Pred fn → m (Property → Property)
checkPred ∷ ∀ fn m. (FunctionLike fn, MonadGenError m) ⇒ Env → Pred fn → m Bool
checkPreds ∷ (MonadGenError m, Traversable t, FunctionLike fn) ⇒ Env → t (Pred fn) → m Bool
checkPredPure ∷ FunctionLike fn ⇒ Env → Pred fn → Bool
runCaseOn ∷ SumOver as → List (Binder fn) as → (∀ a. HasSpec fn a ⇒ Var a → a → Pred fn → r) → r
type OrdSet a = [a]
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
explainSpecOpt ∷ [String] → Specification fn a → Specification fn a
memberSpecList ∷ [a] → NonEmpty String → Specification fn a
shrinkPred ∷ Pred fn → [Pred fn]
isSuspendedSpec ∷ Specification fn a → Bool
equalSpec ∷ a → Specification fn a
notEqualSpec ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a
notMemberSpec ∷ ∀ fn a f. (HasSpec fn a, Foldable f) ⇒ f a → Specification fn a
typeSpec ∷ HasSpec fn a ⇒ TypeSpec fn a → Specification fn a
data BinaryShow where
- BinaryShow ∷ ∀ a. String → [Doc a] → BinaryShow
- NonBinary ∷ BinaryShow
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)
data WithHasSpec fn f a where
- WithHasSpec ∷ HasSpec fn a ⇒ f a → WithHasSpec fn f 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, Show (Hint a)) ⇒ HasGenHint fn a where
- type Hint a
- giveHint ∷ Hint a → Specification fn a
conformsToSpecM ∷ ∀ fn a m. (HasSpec fn a, MonadGenError m) ⇒ a → Specification fn a → m ()
conformsToSpecProp ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a → Property
conformsToSpec ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a → Bool
satisfies ∷ ∀ fn a. HasSpec fn a ⇒ Term fn a → Specification fn a → Pred fn
genFromSpecT ∷ ∀ fn a m. (HasCallStack, HasSpec fn a, MonadGenError m) ⇒ Specification fn a → GenT m a
shrinkWithSpec ∷ ∀ fn a. HasSpec fn a ⇒ Specification fn a → a → [a]
shrinkFromPreds ∷ HasSpec fn a ⇒ Pred fn → Var a → a → [a]
shrinkEnvFromPlan ∷ Env → SolverPlan fn → [Env]
fixupWithSpec ∷ ∀ fn a. HasSpec fn a ⇒ Specification fn a → a → Maybe a
envFromPred ∷ Env → Pred fn → GE Env
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
genInverse ∷ (MonadGenError m, HasSpec fn a, Show b, Functions fn fn, HasSpec fn b) ⇒ fn '[a] b → Specification fn a → b → GenT m a
flattenPred ∷ ∀ fn. BaseUniverse fn ⇒ Pred fn → [Pred fn]
computeDependencies ∷ Pred fn → DependGraph fn
data SolverStage fn where
- SolverStage ∷ HasSpec fn a ⇒ {..} → SolverStage fn
data SolverPlan fn = SolverPlan {
- solverPlan ∷ [SolverStage fn]
- solverDependencies ∷ Graph (Name fn)
}
isTrueSpec ∷ Specification fn a → Bool
prettyLinear ∷ [SolverStage fn] → Doc ann
prepareLinearization ∷ ∀ fn. BaseUniverse fn ⇒ Pred fn → GE (SolverPlan fn)
saturatePred ∷ ∀ fn. Pred fn → [Pred fn]
mergeSolverStage ∷ SolverStage fn → [SolverStage fn] → [SolverStage fn]
backPropagation ∷ ∀ fn. SolverPlan fn → SolverPlan fn
pattern Eql ∷ ∀ fn. () ⇒ ∀ a. HasSpec fn a ⇒ Term fn a → Term fn a → Term fn Bool
pattern FromG ∷ ∀ fn a. () ⇒ (HasSpec fn a, HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Term fn (SimpleRep a) → Term fn a
pattern SLeft ∷ ∀ fn a. () ⇒ ∀ b c. (HasSpec fn b, a ~ Sum b c) ⇒ Term fn b → Term fn a
pattern SRight ∷ ∀ fn a. () ⇒ ∀ b c. (HasSpec fn c, a ~ Sum b c) ⇒ Term fn c → Term fn a
pattern SubsetPat ∷ ∀ fn a. () ⇒ ∀ b. (Ord b, HasSpec fn (Set b), Show b, Typeable b, a ~ Bool) ⇒ Term fn (Set b) → Term fn (Set b) → Term fn a
pattern DisjointPat ∷ ∀ fn a. () ⇒ ∀ b. (Ord b, HasSpec fn (Set b), Show b, Typeable b, a ~ Bool) ⇒ Term fn (Set b) → Term fn (Set b) → Term fn a
pattern UnionPat ∷ ∀ fn a. () ⇒ ∀ b. (Ord b, HasSpec fn (Set b), Show b, Typeable b, a ~ Set b) ⇒ Term fn (Set b) → Term fn (Set b) → Term fn a
pattern MemberPat ∷ ∀ fn a. () ⇒ ∀ b. (HasSpec fn b, HasSpec fn (Set b), Show b, Typeable b, a ~ Bool) ⇒ Term fn b → Term fn (Set b) → Term fn a
pattern ElemPat ∷ ∀ fn a. () ⇒ ∀ b. (HasSpec fn b, HasSpec fn [b], Show b, Typeable b, a ~ Bool) ⇒ Term fn b → Term fn [b] → Term fn a
pattern AppendPat ∷ ∀ fn a. () ⇒ ∀ b. (HasSpec fn [b], Show b, Typeable b, a ~ [b]) ⇒ Term fn [b] → Term fn [b] → Term fn a
short ∷ ∀ a x. (Show a, Typeable a) ⇒ [a] → Doc x
prettyPlan ∷ HasSpec fn a ⇒ Specification fn a → Doc ann
printPlan ∷ HasSpec fn a ⇒ Specification fn a → IO ()
isEmptyPlan ∷ SolverPlan fn → Bool
stepPlan ∷ MonadGenError m ⇒ Env → SolverPlan fn → GenT m (Env, SolverPlan fn)
substStage ∷ Env → SolverStage fn → SolverStage fn
genFromPreds ∷ ∀ fn m. (MonadGenError m, BaseUniverse fn) ⇒ Env → Pred fn → GenT m Env
computeHints ∷ ∀ fn. [Pred fn] → Hints fn
computeBinderDependencies ∷ Binder fn a → DependGraph fn
computeTermDependencies ∷ Term fn a → DependGraph fn
computeTermDependencies' ∷ Term fn a → (DependGraph fn, Set (Name fn))
linearize ∷ (MonadGenError m, BaseUniverse fn) ⇒ [Pred fn] → DependGraph fn → m [SolverStage fn]
normalizeSolverStage ∷ SolverStage fn → SolverStage fn
fromGESpec ∷ (HasCallStack, HasSpec fn a) ⇒ GE (Specification fn a) → Specification fn a
addToErrorSpec ∷ NonEmpty String → Specification fn a → Specification fn a
regularize ∷ HasVariables fn t ⇒ Var a → t → Var a
regularizeBinder ∷ Binder fn a → Binder fn a
regularizeNamesPred ∷ Pred fn → Pred fn
regularizeNames ∷ Specification fn a → Specification fn a
simplifySpec ∷ HasSpec fn a ⇒ Specification fn a → Specification fn a
computeSpecSimplified ∷ ∀ fn a. (HasSpec fn a, HasCallStack) ⇒ Var a → Pred fn → GE (Specification fn a)
computeSpec ∷ ∀ fn a. (HasSpec fn a, HasCallStack) ⇒ Var a → Pred fn → GE (Specification fn a)
computeSpecBinder ∷ Binder fn a → GE (Specification fn a)
computeSpecBinderSimplified ∷ Binder fn a → GE (Specification fn a)
caseSpec ∷ ∀ fn as. HasSpec fn (SumOver as) ⇒ Maybe String → List (Weighted (Specification fn)) as → Specification fn (SumOver as)
totalWeight ∷ List (Weighted f) as → Maybe Int
propagateSpec ∷ ∀ fn v a. HasSpec fn v ⇒ Specification fn a → Ctx fn v a → Specification fn v
ctxHasSpec ∷ Ctx fn v a → Evidence (HasSpec fn a)
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
mapSpec ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ fn '[a] b → Specification fn a → Specification fn b
caseBoolSpec ∷ HasSpec fn a ⇒ Specification fn Bool → (Bool → Specification fn a) → Specification fn a
isErrorLike ∷ ∀ fn a. Specification fn a → Bool
errorLikeMessage ∷ ∀ fn a. Specification fn a → NonEmpty String
type DependGraph fn = Graph (Name fn)
dependency ∷ HasVariables fn t ⇒ Name fn → t → DependGraph fn
irreflexiveDependencyOn ∷ ∀ fn t t'. (HasVariables fn t, HasVariables fn t') ⇒ t → t' → DependGraph fn
noDependencies ∷ HasVariables fn t ⇒ t → DependGraph fn
type Hints fn = DependGraph fn
respecting ∷ Hints f → DependGraph f → DependGraph f
solvableFrom ∷ Name f → Set (Name f) → DependGraph f → Bool
freeVarNames ∷ ∀ fn t. HasVariables fn t ⇒ t → Set Int
data Name fn where
- Name ∷ HasSpec fn a ⇒ Var a → Name fn
newtype FreeVars fn = FreeVars {
- unFreeVars ∷ Map (Name fn) Int
}
restrictedTo ∷ FreeVars fn → Set (Name fn) → FreeVars fn
memberOf ∷ Name fn → FreeVars fn → Bool
count ∷ Name fn → FreeVars fn → Int
freeVar ∷ Name fn → FreeVars fn
singleton ∷ Name fn → Int → FreeVars fn
without ∷ Foldable t ⇒ FreeVars fn → t (Name fn) → FreeVars fn
class HasVariables fn a | a → fn where
- freeVars ∷ a → FreeVars fn
- freeVarSet ∷ a → Set (Name fn)
- countOf ∷ Name fn → a → Int
- appearsIn ∷ Name fn → a → Bool
type Subst fn = [SubstEntry fn]
data SubstEntry fn where
- (:=) ∷ HasSpec fn a ⇒ Var a → Term fn a → SubstEntry fn
backwardsSubstitution ∷ ∀ fn a. HasSpec fn a ⇒ Subst fn → Term fn a → Term fn a
fastInequality ∷ Term fn a → Term fn b → Bool
substituteTerm ∷ ∀ fn a. Subst fn → Term fn a → Term fn a
substituteTerm' ∷ ∀ fn a. Subst fn → Term fn a → Writer Any (Term fn a)
substituteBinder ∷ HasSpec fn a ⇒ Var a → Term fn a → Binder fn b → Binder fn b
substitutePred ∷ HasSpec fn a ⇒ Var a → Term fn a → Pred fn → Pred fn
substTerm ∷ Env → Term fn a → Term fn a
substBinder ∷ Env → Binder fn a → Binder fn a
substPred ∷ BaseUniverse fn ⇒ Env → Pred fn → Pred fn
unBind ∷ a → Binder fn a → Pred fn
simplifyTerm ∷ ∀ fn a. BaseUniverse fn ⇒ Term fn a → Term fn a
fromLits ∷ List (Term fn) as → Maybe (List Value as)
fromLit ∷ Term fn a → Maybe (Value a)
isLit ∷ Term fn a → Bool
simplifyPred ∷ ∀ fn. BaseUniverse fn ⇒ Pred fn → Pred fn
simplifyPreds ∷ BaseUniverse fn ⇒ [Pred fn] → [Pred fn]
simplifyBinder ∷ Binder fn a → Binder fn a
pinnedBy ∷ ∀ fn a. (BaseUniverse fn, Typeable a) ⇒ Var a → Pred fn → Maybe (Term fn a)
optimisePred ∷ BaseUniverse fn ⇒ Pred fn → Pred fn
letSubexpressionElimination ∷ BaseUniverse fn ⇒ Pred fn → Pred fn
letFloating ∷ BaseUniverse fn ⇒ Pred fn → Pred fn
aggressiveInlining ∷ BaseUniverse fn ⇒ Pred fn → Pred fn
substituteAndSimplifyTerm ∷ BaseUniverse fn ⇒ Subst fn → Term fn a → Term fn a
class HasSimpleRep a where
- type SimpleRep a
- type TheSop a ∷ [Type]
- toSimpleRep ∷ a → SimpleRep a
- fromSimpleRep ∷ SimpleRep a → a
type family SimplifyRep f where ...
toGenericFn ∷ ∀ fn a. (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ fn '[a] (SimpleRep a)
fromGenericFn ∷ ∀ fn a. (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ fn '[SimpleRep a] a
data GenericsFn fn args res where
- ToGeneric ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ GenericsFn fn '[a] (SimpleRep a)
- FromGeneric ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ GenericsFn fn '[SimpleRep a] a
fromSimpleRepSpec ∷ ∀ a fn. (HasSpec fn a, HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Specification fn (SimpleRep a) → Specification fn 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)
data (c ∷ Symbol) ::: (ts ∷ [Type])
type family SOPOf f where ...
type family Constr f where ...
type family SOP constrs where ...
type family ConstrOf c sop where ...
class Inject c constrs r where
- inject' ∷ (SOP constrs → r) → FunTy (ConstrOf c constrs) r
inject ∷ ∀ c constrs. Inject c constrs (SOP constrs) ⇒ FunTy (ConstrOf c constrs) (SOP constrs)
type family ALG constrs r where ...
class SOPLike constrs r where
- algebra ∷ SOP constrs → ALG constrs r
- consts ∷ r → ALG constrs r
class SimpleConstructor rep where
- toSimpleCon' ∷ rep p → ProdOver (Constr rep)
- fromSimpleCon' ∷ ProdOver (Constr rep) → rep p
class SopList xs ys where
- injectSOPLeft ∷ SOP xs → SOP (Append xs ys)
- injectSOPRight ∷ SOP ys → SOP (Append xs ys)
- caseSOP ∷ SOP (Append xs ys) → Sum (SOP xs) (SOP ys)
class SimpleGeneric rep where
- toSimpleRep' ∷ rep p → SimplifyRep rep
- fromSimpleRep' ∷ SimplifyRep rep → rep p
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
adds ∷ ∀ fn a. Foldy fn a ⇒ [a] → a
data FoldSpec (fn ∷ [Type] → Type → Type) a where
- 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
preMapFoldSpec ∷ HasSpec fn a ⇒ fn '[a] b → FoldSpec fn b → FoldSpec fn a
combineFoldSpec ∷ FoldSpec fn a → FoldSpec fn a → Either [String] (FoldSpec fn a)
conformsToFoldSpec ∷ ∀ fn a. [a] → FoldSpec fn a → Bool
toPredsFoldSpec ∷ ∀ fn a. BaseUniverse fn ⇒ Term fn [a] → FoldSpec fn a → Pred fn
enumerateInterval ∷ (Enum a, Num a, Ord a, MaybeBounded a) ⇒ NumSpec fn a → [a]
isEmptyNumSpec ∷ (TypeSpec fn a ~ NumSpec fn a, Ord a, Enum a, Num a, MaybeBounded a) ⇒ Specification fn a → Bool
knownUpperBound ∷ (TypeSpec fn a ~ NumSpec fn a, Ord a, Enum a, Num a, MaybeBounded a) ⇒ Specification fn a → Maybe a
knownLowerBound ∷ (TypeSpec fn a ~ NumSpec fn a, Ord a, Enum a, Num a, MaybeBounded a) ⇒ Specification fn a → Maybe a
narrowByFuelAndSize ∷ ∀ a fn. (BaseUniverse fn, TypeSpec fn a ~ NumSpec fn a, HasSpec fn a, Arbitrary a, Integral a, Ord a, Random a, MaybeBounded a) ⇒ a → Int → (Specification fn a, Specification fn a) → (Specification fn a, Specification fn a)
narrowFoldSpecs ∷ ∀ a fn. (BaseUniverse fn, TypeSpec fn a ~ NumSpec fn a, HasSpec fn a, Arbitrary a, Integral a, Ord a, Random a, MaybeBounded a) ⇒ (Specification fn a, Specification fn a) → (Specification fn a, Specification fn a)
genNumList ∷ ∀ a fn m. (BaseUniverse fn, MonadGenError m, TypeSpec fn a ~ NumSpec fn a, HasSpec fn a, Arbitrary a, Integral a, Ord a, Random a, MaybeBounded a, Foldy fn a) ⇒ Specification fn a → Specification fn a → GenT m [a]
genFromFold ∷ ∀ m fn a b. (MonadGenError m, Foldy fn b, HasSpec fn a) ⇒ [a] → Specification fn Integer → Specification fn a → fn '[a] b → Specification fn b → GenT m [a]
guardSumSpec ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b, KnownNat (CountCases b)) ⇒ [String] → SumSpec fn a b → Specification fn (Sum a b)
data SumSpec fn a b = SumSpecRaw (Maybe String) (Maybe (Int, Int)) (Specification fn a) (Specification fn b)
pattern SumSpec ∷ Maybe (Int, Int) → Specification fn a → Specification fn b → SumSpec fn a b
combTypeName ∷ Maybe String → Maybe String → Maybe String
type family CountCases a where ...
countCases ∷ ∀ a. KnownNat (CountCases a) ⇒ Int
sumType ∷ Maybe String → String
sumWeightL ∷ Maybe (Int, Int) → Doc a
sumWeightR ∷ Maybe (Int, Int) → Doc a
data SetSpec fn a = SetSpec (Set a) (Specification fn a) (Specification fn Integer)
guardSetSpec ∷ (HasSpec fn a, Ord a) ⇒ [String] → SetSpec fn a → Specification fn (Set a)
prettySetSpec ∷ HasSpec fn a ⇒ SetSpec fn a → Doc ann
data ListSpec fn a = ListSpec {
- listSpecHint ∷ Maybe Integer
- listSpecMust ∷ [a]
- listSpecSize ∷ Specification fn Integer
- listSpecElem ∷ Specification fn a
- listSpecFold ∷ FoldSpec fn a
}
guardListSpec ∷ HasSpec fn a ⇒ [String] → ListSpec fn a → Specification fn [a]
class MaybeBounded a where
- lowerBound ∷ Maybe a
- upperBound ∷ Maybe a
data NumSpec (fn ∷ [Type] → Type → Type) n = NumSpecInterval (Maybe n) (Maybe n)
emptyNumSpec ∷ Ord a ⇒ NumSpec fn a
guardNumSpec ∷ (Ord n, HasSpec fn n, TypeSpec fn n ~ NumSpec fn n) ⇒ [String] → NumSpec fn n → Specification fn n
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]
constrainInterval ∷ (MonadGenError m, Ord a, Num a, Show a) ⇒ Maybe a → Maybe a → Integer → m (a, a)
conformsToNumSpec ∷ Ord n ⇒ n → NumSpec fn n → Bool
toPredsNumSpec ∷ (Ord n, OrdLike fn n) ⇒ Term fn n → NumSpec fn n → Pred fn
type BaseFns = '[EqFn, SetFn, BoolFn, PairFn, IntFn, OrdFn, GenericsFn, ListFn, SumFn, MapFn, FunFn, SizeFn]
type BaseFn = Fix (OneofL BaseFns)
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)
idFn ∷ ∀ fn a. Member (FunFn fn) fn ⇒ fn '[a] a
composeFn ∷ (Member (FunFn fn) fn, HasSpec fn b, Show (fn '[a] b), Show (fn '[b] c), Eq (fn '[a] b), Eq (fn '[b] c)) ⇒ fn '[b] c → fn '[a] b → fn '[a] c
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
data FunFn fn args res where
- Id ∷ FunFn fn '[a] a
- Compose ∷ (Typeable b, HasSpec fn b, Show (fn '[a] b), Show (fn '[b] c), Eq (fn '[a] b), Eq (fn '[b] c)) ⇒ fn '[b] c → fn '[a] b → FunFn fn '[a] c
- Flip ∷ (Show (fn '[a, b] c), Eq (fn '[a, b] c), HasSpec fn a, HasSpec fn b) ⇒ fn '[a, b] c → FunFn fn '[b, a] c
lessOrEqualFn ∷ ∀ fn a. (Ord a, OrdLike fn a) ⇒ fn '[a, a] Bool
lessFn ∷ ∀ fn a. (Ord a, OrdLike fn a) ⇒ fn '[a, a] Bool
data OrdFn (fn ∷ [Type] → Type → Type) as b where
- LessOrEqual ∷ (Ord a, OrdLike fn a) ⇒ OrdFn fn '[a, a] Bool
- Less ∷ (Ord a, OrdLike fn a) ⇒ OrdFn fn '[a, a] Bool
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
data ListFn fn args res where
- FoldMap ∷ (HasSpec fn a, Foldy fn b, Show (fn '[a] b), Eq (fn '[a] b)) ⇒ fn '[a] b → ListFn fn '[[a]] b
- SingletonList ∷ ListFn fn '[a] [a]
- AppendFn ∷ (Typeable a, Show a) ⇒ ListFn fn '[[a], [a]] [a]
foldMapFn ∷ ∀ fn a b. (HasSpec fn a, Foldy fn b, Show (fn '[a] b), Eq (fn '[a] b)) ⇒ fn '[a] b → fn '[[a]] b
singletonListFn ∷ ∀ fn a. HasSpec fn a ⇒ fn '[a] [a]
appendFn ∷ ∀ fn a. (HasSpec fn a, Show a, Typeable a) ⇒ fn '[[a], [a]] [a]
addFn ∷ ∀ fn a. NumLike fn a ⇒ fn '[a, a] a
negateFn ∷ ∀ fn a. NumLike fn a ⇒ fn '[a] a
data IntFn (fn ∷ [Type] → Type → Type) as b where
- Add ∷ NumLike fn a ⇒ IntFn fn '[a, a] a
- Negate ∷ NumLike fn a ⇒ IntFn fn '[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
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
not_ ∷ BaseUniverse fn ⇒ Term fn Bool → Term fn Bool
(||.) ∷ BaseUniverse fn ⇒ Term fn Bool → Term fn Bool → Term fn Bool
elem_ ∷ ∀ a fn. HasSpec fn a ⇒ Term fn a → Term fn [a] → 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)
sizeOf_ ∷ ∀ a fn. (HasSpec fn a, Sized a) ⇒ Term fn a → Term fn Integer
size_ ∷ ∀ a fn. (HasSpec fn (Set a), Ord a) ⇒ Term fn (Set a) → Term fn Integer
length_ ∷ ∀ a fn. HasSpec fn [a] ⇒ Term fn [a] → Term fn Integer
null_ ∷ (HasSpec fn a, Sized 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
(>.) ∷ (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
sum_ ∷ (BaseUniverse fn, Member (FunFn fn) fn, Foldy fn a) ⇒ Term fn [a] → Term fn a
foldMap_ ∷ ∀ fn a b. (BaseUniverse fn, Foldy fn b, HasSpec fn a) ⇒ (Term fn a → Term fn b) → Term fn [a] → Term fn b
(++.) ∷ HasSpec fn a ⇒ Term fn [a] → Term fn [a] → Term fn [a]
singletonList_ ∷ HasSpec fn a ⇒ Term fn a → Term fn [a]
constrained ∷ ∀ a fn p. (IsPred p fn, HasSpec fn a) ⇒ (Term fn a → p) → Specification fn a
assertExplain ∷ (BaseUniverse fn, IsPred p fn) ⇒ NonEmpty String → p → Pred fn
assert ∷ (BaseUniverse fn, IsPred p fn) ⇒ p → Pred fn
forAll ∷ (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) ⇒ Term fn t → (Term fn a → p) → Pred fn
mkForAll ∷ (Forallable t a, HasSpec fn t, HasSpec fn a) ⇒ Term fn t → Binder fn a → 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
letBind ∷ (HasSpec fn a, IsPred p fn) ⇒ Term fn a → (Term fn a → p) → Pred fn
reify ∷ (HasSpec fn a, HasSpec fn b, IsPred p fn) ⇒ Term fn a → (a → b) → (Term fn b → p) → Pred fn
explanation ∷ NonEmpty String → Pred fn → Pred fn
monitor ∷ ((∀ a. Term fn a → a) → Property → Property) → Pred fn
assertReified ∷ HasSpec fn a ⇒ Term fn a → (a → Bool) → Pred fn
reifies ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn b → Term fn a → (a → b) → Pred fn
dependsOn ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn a → Term fn b → Pred fn
lit ∷ Show a ⇒ a → Term 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
genHint ∷ ∀ fn t. HasGenHint fn t ⇒ Hint t → Term fn t → Pred fn
app ∷ (HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) ⇒ fn as b → FunTy (MapList (Term fn) as) (Term fn b)
name ∷ String → Term fn a → Term fn a
named ∷ String → Term fn a → Term fn a
bind ∷ (HasSpec fn a, IsPred p fn) ⇒ (Term fn a → p) → Binder fn a
mkCase ∷ HasSpec fn (SumOver as) ⇒ Term fn (SumOver as) → List (Weighted (Binder fn)) as → Pred fn
type IsPred p fn = (PredLike p, UnivConstr p fn)
class Show p ⇒ PredLike p where
- type UnivConstr p (fn ∷ [Type] → Type → Type) ∷ Constraint
- toPredExplain ∷ (BaseUniverse fn, UnivConstr p fn) ⇒ [String] → p → Pred fn
toPred ∷ ∀ fn p. (BaseUniverse fn, PredLike p, UnivConstr p fn) ⇒ p → Pred fn
data WithPrec a = WithPrec Int a
parensIf ∷ Bool → Doc ann → Doc ann
prettyPrec ∷ Pretty (WithPrec a) ⇒ Int → a → Doc ann
ppList ∷ ∀ fn f as ann. All (HasSpec fn) as ⇒ (∀ a. HasSpec fn a ⇒ f a → Doc ann) → List f as → [Doc ann]
ppList_ ∷ ∀ f as ann. (∀ a. f a → Doc ann) → List f as → [Doc ann]
vsep' ∷ [Doc ann] → Doc ann
(/>) ∷ Doc ann → Doc ann → Doc ann
genFromSizeSpec ∷ (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Integer → GenT m Integer
data SizeFn (fn ∷ [Type] → Type → Type) as b where
- SizeOf ∷ ∀ fn a. (Sized a, HasSpec fn a) ⇒ SizeFn fn '[a] Integer
sizeOfFn ∷ ∀ fn a. (HasSpec fn a, Member (SizeFn fn) fn, Sized a) ⇒ fn '[a] Integer
mapTypeSpecSize ∷ ∀ fn a b f. f ~ SizeFn fn ⇒ f '[a] b → TypeSpec fn a → Specification fn b
type SizeSpec fn = NumSpec fn Integer
rangeSize ∷ Integer → Integer → SizeSpec fn
maxSpec ∷ BaseUniverse fn ⇒ Specification fn Integer → Specification fn Integer
class Sized 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
hasSize ∷ (HasSpec fn t, Sized t) ⇒ SizeSpec fn → Specification fn t
guardEmpty ∷ Maybe Integer → Maybe Integer → NumSpec fn Integer → NumSpec fn Integer
addNumSpec ∷ NumSpec fn Integer → NumSpec fn Integer → NumSpec fn Integer
subNumSpec ∷ NumSpec fn Integer → NumSpec fn Integer → NumSpec fn Integer
multNumSpec ∷ NumSpec fn Integer → NumSpec fn Integer → NumSpec fn Integer
negNumSpec ∷ NumSpec fn Integer → NumSpec fn Integer
addSpecInt ∷ BaseUniverse fn ⇒ Specification fn Integer → Specification fn Integer → Specification fn Integer
subSpecInt ∷ BaseUniverse fn ⇒ Specification fn Integer → Specification fn Integer → Specification fn Integer
multSpecInt ∷ BaseUniverse fn ⇒ Specification fn Integer → Specification fn Integer → Specification fn Integer
operateSpec ∷ (TypeSpec fn n ~ NumSpec fn n, Enum n, Ord n, HasSpec fn n) ⇒ String → (n → n → n) → (TypeSpec fn n → TypeSpec fn n → TypeSpec fn n) → Specification fn n → Specification fn n → Specification fn n
cardinality ∷ ∀ fn a. (Eq a, BaseUniverse fn, HasSpec fn a) ⇒ Specification fn a → Specification fn Integer
cardinalNumSpec ∷ ∀ n fn. (Integral n, Num n, MaybeBounded n) ⇒ NumSpec fn n → Specification fn Integer
lowBound ∷ Bounded n ⇒ Maybe n → n
highBound ∷ Bounded n ⇒ Maybe n → n
countSpec ∷ ∀ n fn. (Bounded n, Integral n) ⇒ NumSpec fn n → Integer
finiteSize ∷ ∀ n. (Integral n, Bounded n) ⇒ Integer
notInNumSpec ∷ ∀ fn n. (Functions fn fn, BaseUniverse fn, HasSpec fn n, TypeSpec fn n ~ NumSpec fn n, Bounded n, Integral n) ⇒ NumSpec fn n → [n] → Specification fn n
data T x
- = NegInf
- | Ok x
- | PosInf
unT ∷ T x → Maybe x
neg ∷ Maybe x → T x
pos ∷ Maybe x → T x
multT ∷ Num x ⇒ T x → T x → T x
sizeOfSpec ∷ ∀ fn t. (BaseUniverse fn, Sized t, HasSpec fn t) ⇒ Specification fn t → Specification fn Integer
checkForNegativeSize ∷ Specification fn Integer → Specification fn Integer
nubOrd ∷ Ord a ⇒ [a] → [a]
nubOrdMemberSpec ∷ Ord a ⇒ String → [a] → Specification fn a

Documentation

data Term (fn ∷ [Type] → Type → Type) a where Source #

Typed first order terms with function symbols from fn.

Constructors

App ∷ (Typeable as, TypeList as, All (HasSpec fn) as, HasSpec fn b, BaseUniverse fn) ⇒ fn as b → List (Term fn) as → Term fn b
Lit ∷ Show a ⇒ a → Term fn a
V ∷ HasSpec fn a ⇒ Var a → Term fn a

Instances

Instances details

HasVariables fn (Term fn a) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ Term fn a → FreeVars fn Source # freeVarSet ∷ Term fn a → Set (Name fn) Source # countOf ∷ Name fn → Term fn a → Int Source # appearsIn ∷ Name fn → Term fn a → Bool Source #
HasVariables fn (List (Term fn) as) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ List (Term fn) as → FreeVars fn Source # freeVarSet ∷ List (Term fn) as → Set (Name fn) Source # countOf ∷ Name fn → List (Term fn) as → Int Source # appearsIn ∷ Name fn → List (Term fn) as → Bool Source #
HasSpec fn a ⇒ Pretty (WithPrec (Term fn a)) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ WithPrec (Term fn a) → Doc ann Source # prettyList ∷ [WithPrec (Term fn a)] → Doc ann Source #
(Ord a, Show a, Typeable a, HasSpec fn (Set a)) ⇒ Monoid (Term fn (Set a)) Source #
Instance details Defined in Constrained.Base Methods mempty ∷ Term fn (Set a) Source # mappend ∷ Term fn (Set a) → Term fn (Set a) → Term fn (Set a) Source # mconcat ∷ [Term fn (Set a)] → Term fn (Set a) Source #
(Ord a, Show a, Typeable a, HasSpec fn (Set a)) ⇒ Semigroup (Term fn (Set a)) Source #
Instance details Defined in Constrained.Base Methods (<>) ∷ Term fn (Set a) → Term fn (Set a) → Term fn (Set a) Source # sconcat ∷ NonEmpty (Term fn (Set a)) → Term fn (Set a) Source # stimes ∷ Integral b ⇒ b → Term fn (Set a) → Term fn (Set a) Source #
NumLike fn a ⇒ Num (Term fn a) Source #
Instance details Defined in Constrained.Base Methods (+) ∷ Term fn a → Term fn a → Term fn a Source # (-) ∷ Term fn a → Term fn a → Term fn a Source # (*) ∷ Term fn a → Term fn a → Term fn a Source # negate ∷ Term fn a → Term fn a Source # abs ∷ Term fn a → Term fn a Source # signum ∷ Term fn a → Term fn a Source # fromInteger ∷ Integer → Term fn a Source #
HasSpec fn a ⇒ Show (Term fn a) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → Term fn a → ShowS Source # show ∷ Term fn a → String Source # showList ∷ [Term fn a] → ShowS Source #
BaseUniverse fn ⇒ PredLike (Term fn Bool) Source #
Instance details Defined in Constrained.Base Associated Types type UnivConstr (Term fn Bool) fn Source # Methods toPredExplain ∷ ∀ (fn0 ∷ [Type] → Type → Type). (BaseUniverse fn0, UnivConstr (Term fn Bool) fn0) ⇒ [String] → Term fn Bool → Pred fn0 Source #
Rename (Term fn a) Source #
Instance details Defined in Constrained.Base Methods rename ∷ Typeable x ⇒ Var x → Var x → Term fn a → Term fn a Source #
HasSpec fn a ⇒ Eq (Term fn a) Source #
Instance details Defined in Constrained.Base Methods (==) ∷ Term fn a → Term fn a → Bool Source # (/=) ∷ Term fn a → Term fn a → Bool Source #
HasSpec fn a ⇒ Pretty (Term fn a) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ Term fn a → Doc ann Source # prettyList ∷ [Term fn a] → Doc ann Source #
type UnivConstr (Term fn Bool) fn' Source #
Instance details Defined in Constrained.Base type UnivConstr (Term fn Bool) fn' = fn ~ fn'

type HasSpecImpliesEq fn a f = HasSpec fn a ⇒ Eq (f a) ∷ Constraint Source #

data Binder fn a where Source #

Constructors

(:->) ∷ HasSpec fn a ⇒ Var a → Pred fn → Binder fn a

Instances

Instances details

HasVariables fn (Binder fn a) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ Binder fn a → FreeVars fn Source # freeVarSet ∷ Binder fn a → Set (Name fn) Source # countOf ∷ Name fn → Binder fn a → Int Source # appearsIn ∷ Name fn → Binder fn a → Bool Source #
HasVariables fn (List (Weighted (Binder fn)) as) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ List (Weighted (Binder fn)) as → FreeVars fn Source # freeVarSet ∷ List (Weighted (Binder fn)) as → Set (Name fn) Source # countOf ∷ Name fn → List (Weighted (Binder fn)) as → Int Source # appearsIn ∷ Name fn → List (Weighted (Binder fn)) as → Bool Source #
Show (Binder fn a) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → Binder fn a → ShowS Source # show ∷ Binder fn a → String Source # showList ∷ [Binder fn a] → ShowS Source #
Rename (Binder fn a) Source #
Instance details Defined in Constrained.Base Methods rename ∷ Typeable x ⇒ Var x → Var x → Binder fn a → Binder fn a Source #
Pretty (Binder fn a) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ Binder fn a → Doc ann Source # prettyList ∷ [Binder fn a] → Doc ann Source #

data Pred (fn ∷ [Type] → Type → Type) where Source #

Constructors

Monitor ∷ ((∀ a. Term fn a → a) → Property → Property) → Pred fn
Block ∷ [Pred fn] → Pred fn
Exists
Fields ∷ ((∀ b. Term fn b → b) → GE a) Constructive recovery function for checking existential quantification → Binder fn a → Pred fn
Subst ∷ HasSpec fn a ⇒ Var a → Term fn a → Pred fn → Pred fn
Let ∷ Term fn a → Binder fn a → Pred fn
Assert ∷ BaseUniverse fn ⇒ Term fn Bool → Pred fn
Reifies
Fields ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn b This depends on the `a` term → Term fn a → (a → b) Recover a useable value from the `a` term. → 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) ⇒ Term fn t → Binder fn a → Pred fn
Case
Fields ∷ HasSpec fn (SumOver as) ⇒ Term fn (SumOver as) → List (Weighted (Binder fn)) as Each branch of the type is bound with only one variable because `as` are types. Constructors with multiple arguments are encoded with `ProdOver` (c.f. `Univ`). → Pred fn
When ∷ HasSpec fn Bool ⇒ Term fn Bool → Pred fn → Pred fn
GenHint ∷ HasGenHint fn a ⇒ Hint a → Term fn a → Pred fn
TruePred ∷ Pred fn
FalsePred ∷ NonEmpty String → Pred fn
Explain ∷ NonEmpty String → Pred fn → Pred fn

Instances

Instances details

HasVariables fn (Pred fn) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ Pred fn → FreeVars fn Source # freeVarSet ∷ Pred fn → Set (Name fn) Source # countOf ∷ Name fn → Pred fn → Int Source # appearsIn ∷ Name fn → Pred fn → Bool Source #
BaseUniverse fn ⇒ Monoid (Pred fn) Source #
Instance details Defined in Constrained.Base Methods mempty ∷ Pred fn Source # mappend ∷ Pred fn → Pred fn → Pred fn Source # mconcat ∷ [Pred fn] → Pred fn Source #
BaseUniverse fn ⇒ Semigroup (Pred fn) Source #
Instance details Defined in Constrained.Base Methods (<>) ∷ Pred fn → Pred fn → Pred fn Source # sconcat ∷ NonEmpty (Pred fn) → Pred fn Source # stimes ∷ Integral b ⇒ b → Pred fn → Pred fn Source #
Show (Pred fn) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → Pred fn → ShowS Source # show ∷ Pred fn → String Source # showList ∷ [Pred fn] → ShowS Source #
PredLike (Pred fn) Source #
Instance details Defined in Constrained.Base Associated Types type UnivConstr (Pred fn) fn Source # Methods toPredExplain ∷ ∀ (fn0 ∷ [Type] → Type → Type). (BaseUniverse fn0, UnivConstr (Pred fn) fn0) ⇒ [String] → Pred fn → Pred fn0 Source #
Rename (Pred fn) Source #
Instance details Defined in Constrained.Base Methods rename ∷ Typeable x ⇒ Var x → Var x → Pred fn → Pred fn Source #
Pretty (Pred fn) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ Pred fn → Doc ann Source # prettyList ∷ [Pred fn] → Doc ann Source #
type UnivConstr (Pred fn) fn' Source #
Instance details Defined in Constrained.Base type UnivConstr (Pred fn) fn' = fn ~ fn'

falsePred1 ∷ String → Pred fn Source #

data Weighted f a Source #

Constructors

Weighted
Fields weight ∷ Maybe Int thing ∷ f a

Instances

Instances details

HasVariables fn (f a) ⇒ HasVariables fn (Weighted f a) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ Weighted f a → FreeVars fn Source # freeVarSet ∷ Weighted f a → Set (Name fn) Source # countOf ∷ Name fn → Weighted f a → Int Source # appearsIn ∷ Name fn → Weighted f a → Bool Source #
HasVariables fn (List (Weighted (Binder fn)) as) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ List (Weighted (Binder fn)) as → FreeVars fn Source # freeVarSet ∷ List (Weighted (Binder fn)) as → Set (Name fn) Source # countOf ∷ Name fn → List (Weighted (Binder fn)) as → Int Source # appearsIn ∷ Name fn → List (Weighted (Binder fn)) as → Bool Source #
Foldable f ⇒ Foldable (Weighted f) Source #
Instance details Defined in Constrained.Base Methods fold ∷ Monoid m ⇒ Weighted f m → m Source # foldMap ∷ Monoid m ⇒ (a → m) → Weighted f a → m Source # foldMap' ∷ Monoid m ⇒ (a → m) → Weighted f a → m Source # foldr ∷ (a → b → b) → b → Weighted f a → b Source # foldr' ∷ (a → b → b) → b → Weighted f a → b Source # foldl ∷ (b → a → b) → b → Weighted f a → b Source # foldl' ∷ (b → a → b) → b → Weighted f a → b Source # foldr1 ∷ (a → a → a) → Weighted f a → a Source # foldl1 ∷ (a → a → a) → Weighted f a → a Source # toList ∷ Weighted f a → [a] Source # null ∷ Weighted f a → Bool Source # length ∷ Weighted f a → Int Source # elem ∷ Eq a ⇒ a → Weighted f a → Bool Source # maximum ∷ Ord a ⇒ Weighted f a → a Source # minimum ∷ Ord a ⇒ Weighted f a → a Source # sum ∷ Num a ⇒ Weighted f a → a Source # product ∷ Num a ⇒ Weighted f a → a Source #
Traversable f ⇒ Traversable (Weighted f) Source #
Instance details Defined in Constrained.Base Methods traverse ∷ Applicative f0 ⇒ (a → f0 b) → Weighted f a → f0 (Weighted f b) Source # sequenceA ∷ Applicative f0 ⇒ Weighted f (f0 a) → f0 (Weighted f a) Source # mapM ∷ Monad m ⇒ (a → m b) → Weighted f a → m (Weighted f b) Source # sequence ∷ Monad m ⇒ Weighted f (m a) → m (Weighted f a) Source #
Functor f ⇒ Functor (Weighted f) Source #
Instance details Defined in Constrained.Base Methods fmap ∷ (a → b) → Weighted f a → Weighted f b Source # (<$) ∷ a → Weighted f b → Weighted f a Source #
Rename (f a) ⇒ Rename (Weighted f a) Source #
Instance details Defined in Constrained.Base Methods rename ∷ Typeable x ⇒ Var x → Var x → Weighted f a → Weighted f a Source #
Pretty (f a) ⇒ Pretty (Weighted f a) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ Weighted f a → Doc ann Source # prettyList ∷ [Weighted f a] → Doc ann Source #

mapWeighted ∷ (f a → g b) → Weighted f a → Weighted g b Source #

traverseWeighted ∷ Applicative m ⇒ (f a → m (g a)) → Weighted f a → m (Weighted g a) Source #

data Ctx (fn ∷ [Type] → Type → Type) v a where Source #

Contexts for Terms, basically a term with a _single_ HOLE instead of a variable. This is used to traverse the defining constraints for a variable and turn them into a spec. Each subterm `f vs Ctx vs'` for lists of values vs and vs` gets given to the propagateSpecFun for f as `f vs HOLE vs'`.

Constructors

CtxHOLE ∷ HasSpec fn v ⇒ Ctx fn v v	A single hole of type `v`
CtxApp ∷ (HasSpec fn b, TypeList as, Typeable as, All (HasSpec fn) as) ⇒ fn as b → ListCtx Value as (Ctx fn v) → Ctx fn v b	The application `f vs Ctx vs'`

data HOLE a b where 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.

Constructors

HOLE ∷ HOLE a a

toCtx ∷ ∀ m fn v a. (BaseUniverse fn, Typeable v, MonadGenError m, HasCallStack, HasSpec fn a, HasSpec fn v) ⇒ Var v → Term fn a → m (Ctx fn v a) Source #

toCtxList ∷ ∀ m fn v as. (BaseUniverse fn, All (HasSpec fn) as, HasSpec fn v, Typeable v, MonadGenError m, HasCallStack) ⇒ Var v → List (Term fn) as → m (ListCtx Value as (Ctx fn v)) Source #

runTerm ∷ MonadGenError m ⇒ Env → Term fn a → m a 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 $ ...

monitorPred ∷ ∀ fn m. (FunctionLike fn, MonadGenError m) ⇒ Env → Pred fn → m (Property → Property) Source #

checkPred ∷ ∀ fn m. (FunctionLike fn, MonadGenError m) ⇒ Env → Pred fn → m Bool Source #

checkPreds ∷ (MonadGenError m, Traversable t, FunctionLike fn) ⇒ Env → t (Pred fn) → m Bool Source #

checkPredPure ∷ FunctionLike fn ⇒ Env → Pred fn → Bool Source #

runCaseOn ∷ SumOver as → List (Binder fn) as → (∀ a. HasSpec fn a ⇒ Var a → a → Pred fn → r) → r Source #

type OrdSet a = [a] Source #

data Specification fn a where Source #

A `Specification fn a` denotes a set of as

Constructors

ExplainSpec ∷ [String] → Specification fn a → Specification fn a	Explain a Specification
MemberSpec	Elements of a known set
Fields ∷ NonEmpty a It must be an element of this OrdSet (List). Try hard not to put duplicates in the List. → Specification fn a
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 `Binder` here
Fields ∷ HasSpec fn a ⇒ Var a This variable ranges over values denoted by the spec → Pred fn And the variable is subject to these constraints → Specification fn a
TypeSpec	A type-specific spec
Fields ∷ HasSpec fn a ⇒ TypeSpec fn a → OrdSet a It can't be any of the elements of this set → Specification fn a
TrueSpec ∷ Specification fn a	Anything

Instances

Instances details

HasSpec fn a ⇒ Pretty (WithPrec (Specification fn a)) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ WithPrec (Specification fn a) → Doc ann Source # prettyList ∷ [WithPrec (Specification fn a)] → Doc ann Source #
(HasSpec fn a, Arbitrary (TypeSpec fn a)) ⇒ Arbitrary (Specification fn a) Source #
Instance details Defined in Constrained.Base Methods arbitrary ∷ Gen (Specification fn a) Source # shrink ∷ Specification fn a → [Specification fn a] Source #
HasSpec fn a ⇒ Monoid (Specification fn a) Source #
Instance details Defined in Constrained.Base Methods mempty ∷ Specification fn a Source # mappend ∷ Specification fn a → Specification fn a → Specification fn a Source # mconcat ∷ [Specification fn a] → Specification fn a Source #
HasSpec fn a ⇒ Semigroup (Specification fn a) Source #
Instance details Defined in Constrained.Base Methods (<>) ∷ Specification fn a → Specification fn a → Specification fn a Source # sconcat ∷ NonEmpty (Specification fn a) → Specification fn a Source # stimes ∷ Integral b ⇒ b → Specification fn a → Specification fn a Source #
HasSpec fn a ⇒ Show (Specification fn a) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → Specification fn a → ShowS Source # show ∷ Specification fn a → String Source # showList ∷ [Specification fn a] → ShowS Source #
HasSpec fn a ⇒ Pretty (Specification fn a) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ Specification fn a → Doc ann Source # prettyList ∷ [Specification fn a] → Doc ann Source #

explainSpecOpt ∷ [String] → Specification fn a → Specification fn a Source #

memberSpecList ∷ [a] → NonEmpty String → Specification fn a Source #

return a MemberSpec or ans ErrorSpec depending on if xs the null list or not

shrinkPred ∷ Pred fn → [Pred fn] Source #

isSuspendedSpec ∷ Specification fn a → Bool Source #

equalSpec ∷ a → Specification fn a Source #

notEqualSpec ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a Source #

notMemberSpec ∷ ∀ fn a f. (HasSpec fn a, Foldable f) ⇒ f a → Specification fn a Source #

typeSpec ∷ HasSpec fn a ⇒ TypeSpec fn a → Specification fn a Source #

data BinaryShow where Source #

Constructors

BinaryShow ∷ ∀ a. String → [Doc a] → BinaryShow
NonBinary ∷ BinaryShow

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).

Minimal complete definition

Nothing

Associated Types

type TypeSpec (fn ∷ [Type] → Type → Type) a Source #

The `TypeSpec fn a` is the type-specific `Specification fn a`.

type TypeSpec fn a = TypeSpec fn (SimpleRep a)

type Prerequisites fn a ∷ Constraint Source #

Prerequisites for the instance that are sometimes necessary when working with e.g. Specifications or functions in the universe.

type Prerequisites fn a = ()

Methods

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)

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

Instances details

BaseUniverse fn ⇒ HasSpec fn Int16 Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn Int16 Source # type Prerequisites fn Int16 Source # Methods emptySpec ∷ TypeSpec fn Int16 Source # combineSpec ∷ TypeSpec fn Int16 → TypeSpec fn Int16 → Specification fn Int16 Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn Int16 → GenT m Int16 Source # conformsTo ∷ Int16 → TypeSpec fn Int16 → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn Int16 → Int16 → [Int16] Source # toPreds ∷ Term fn Int16 → TypeSpec fn Int16 → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn Int16 → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn Int16 → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn Int16 → BinaryShow Source # monadConformsTo ∷ Int16 → TypeSpec fn Int16 → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn Int16 → [Int16] → Specification fn Int16 Source # guardTypeSpec ∷ [String] → TypeSpec fn Int16 → Specification fn Int16 Source # prerequisites ∷ Evidence (Prerequisites fn Int16) Source #
BaseUniverse fn ⇒ HasSpec fn Int32 Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn Int32 Source # type Prerequisites fn Int32 Source # Methods emptySpec ∷ TypeSpec fn Int32 Source # combineSpec ∷ TypeSpec fn Int32 → TypeSpec fn Int32 → Specification fn Int32 Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn Int32 → GenT m Int32 Source # conformsTo ∷ Int32 → TypeSpec fn Int32 → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn Int32 → Int32 → [Int32] Source # toPreds ∷ Term fn Int32 → TypeSpec fn Int32 → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn Int32 → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn Int32 → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn Int32 → BinaryShow Source # monadConformsTo ∷ Int32 → TypeSpec fn Int32 → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn Int32 → [Int32] → Specification fn Int32 Source # guardTypeSpec ∷ [String] → TypeSpec fn Int32 → Specification fn Int32 Source # prerequisites ∷ Evidence (Prerequisites fn Int32) Source #
BaseUniverse fn ⇒ HasSpec fn Int64 Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn Int64 Source # type Prerequisites fn Int64 Source # Methods emptySpec ∷ TypeSpec fn Int64 Source # combineSpec ∷ TypeSpec fn Int64 → TypeSpec fn Int64 → Specification fn Int64 Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn Int64 → GenT m Int64 Source # conformsTo ∷ Int64 → TypeSpec fn Int64 → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn Int64 → Int64 → [Int64] Source # toPreds ∷ Term fn Int64 → TypeSpec fn Int64 → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn Int64 → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn Int64 → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn Int64 → BinaryShow Source # monadConformsTo ∷ Int64 → TypeSpec fn Int64 → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn Int64 → [Int64] → Specification fn Int64 Source # guardTypeSpec ∷ [String] → TypeSpec fn Int64 → Specification fn Int64 Source # prerequisites ∷ Evidence (Prerequisites fn Int64) Source #
BaseUniverse fn ⇒ HasSpec fn Int8 Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn Int8 Source # type Prerequisites fn Int8 Source # Methods emptySpec ∷ TypeSpec fn Int8 Source # combineSpec ∷ TypeSpec fn Int8 → TypeSpec fn Int8 → Specification fn Int8 Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn Int8 → GenT m Int8 Source # conformsTo ∷ Int8 → TypeSpec fn Int8 → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn Int8 → Int8 → [Int8] Source # toPreds ∷ Term fn Int8 → TypeSpec fn Int8 → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn Int8 → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn Int8 → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn Int8 → BinaryShow Source # monadConformsTo ∷ Int8 → TypeSpec fn Int8 → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn Int8 → [Int8] → Specification fn Int8 Source # guardTypeSpec ∷ [String] → TypeSpec fn Int8 → Specification fn Int8 Source # prerequisites ∷ Evidence (Prerequisites fn Int8) Source #
BaseUniverse fn ⇒ HasSpec fn Word16 Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn Word16 Source # type Prerequisites fn Word16 Source # Methods emptySpec ∷ TypeSpec fn Word16 Source # combineSpec ∷ TypeSpec fn Word16 → TypeSpec fn Word16 → Specification fn Word16 Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn Word16 → GenT m Word16 Source # conformsTo ∷ Word16 → TypeSpec fn Word16 → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn Word16 → Word16 → [Word16] Source # toPreds ∷ Term fn Word16 → TypeSpec fn Word16 → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn Word16 → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn Word16 → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn Word16 → BinaryShow Source # monadConformsTo ∷ Word16 → TypeSpec fn Word16 → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn Word16 → [Word16] → Specification fn Word16 Source # guardTypeSpec ∷ [String] → TypeSpec fn Word16 → Specification fn Word16 Source # prerequisites ∷ Evidence (Prerequisites fn Word16) Source #
BaseUniverse fn ⇒ HasSpec fn Word32 Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn Word32 Source # type Prerequisites fn Word32 Source # Methods emptySpec ∷ TypeSpec fn Word32 Source # combineSpec ∷ TypeSpec fn Word32 → TypeSpec fn Word32 → Specification fn Word32 Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn Word32 → GenT m Word32 Source # conformsTo ∷ Word32 → TypeSpec fn Word32 → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn Word32 → Word32 → [Word32] Source # toPreds ∷ Term fn Word32 → TypeSpec fn Word32 → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn Word32 → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn Word32 → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn Word32 → BinaryShow Source # monadConformsTo ∷ Word32 → TypeSpec fn Word32 → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn Word32 → [Word32] → Specification fn Word32 Source # guardTypeSpec ∷ [String] → TypeSpec fn Word32 → Specification fn Word32 Source # prerequisites ∷ Evidence (Prerequisites fn Word32) Source #
BaseUniverse fn ⇒ HasSpec fn Word64 Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn Word64 Source # type Prerequisites fn Word64 Source # Methods emptySpec ∷ TypeSpec fn Word64 Source # combineSpec ∷ TypeSpec fn Word64 → TypeSpec fn Word64 → Specification fn Word64 Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn Word64 → GenT m Word64 Source # conformsTo ∷ Word64 → TypeSpec fn Word64 → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn Word64 → Word64 → [Word64] Source # toPreds ∷ Term fn Word64 → TypeSpec fn Word64 → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn Word64 → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn Word64 → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn Word64 → BinaryShow Source # monadConformsTo ∷ Word64 → TypeSpec fn Word64 → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn Word64 → [Word64] → Specification fn Word64 Source # guardTypeSpec ∷ [String] → TypeSpec fn Word64 → Specification fn Word64 Source # prerequisites ∷ Evidence (Prerequisites fn Word64) Source #
BaseUniverse fn ⇒ HasSpec fn Word8 Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn Word8 Source # type Prerequisites fn Word8 Source # Methods emptySpec ∷ TypeSpec fn Word8 Source # combineSpec ∷ TypeSpec fn Word8 → TypeSpec fn Word8 → Specification fn Word8 Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn Word8 → GenT m Word8 Source # conformsTo ∷ Word8 → TypeSpec fn Word8 → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn Word8 → Word8 → [Word8] Source # toPreds ∷ Term fn Word8 → TypeSpec fn Word8 → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn Word8 → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn Word8 → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn Word8 → BinaryShow Source # monadConformsTo ∷ Word8 → TypeSpec fn Word8 → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn Word8 → [Word8] → Specification fn Word8 Source # guardTypeSpec ∷ [String] → TypeSpec fn Word8 → Specification fn Word8 Source # prerequisites ∷ Evidence (Prerequisites fn Word8) Source #
BaseUniverse fn ⇒ HasSpec fn Foo Source #
Instance details Defined in Constrained.Examples.Basic Associated Types type TypeSpec fn Foo Source # type Prerequisites fn Foo Source # Methods emptySpec ∷ TypeSpec fn Foo Source # combineSpec ∷ TypeSpec fn Foo → TypeSpec fn Foo → Specification fn Foo Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn Foo → GenT m Foo Source # conformsTo ∷ Foo → TypeSpec fn Foo → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn Foo → Foo → [Foo] Source # toPreds ∷ Term fn Foo → TypeSpec fn Foo → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn Foo → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn Foo → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn Foo → BinaryShow Source # monadConformsTo ∷ Foo → TypeSpec fn Foo → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn Foo → [Foo] → Specification fn Foo Source # guardTypeSpec ∷ [String] → TypeSpec fn Foo → Specification fn Foo Source # prerequisites ∷ Evidence (Prerequisites fn Foo) Source #
BaseUniverse fn ⇒ HasSpec fn Three Source #
Instance details Defined in Constrained.Examples.Basic Associated Types type TypeSpec fn Three Source # type Prerequisites fn Three Source # Methods emptySpec ∷ TypeSpec fn Three Source # combineSpec ∷ TypeSpec fn Three → TypeSpec fn Three → Specification fn Three Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn Three → GenT m Three Source # conformsTo ∷ Three → TypeSpec fn Three → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn Three → Three → [Three] Source # toPreds ∷ Term fn Three → TypeSpec fn Three → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn Three → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn Three → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn Three → BinaryShow Source # monadConformsTo ∷ Three → TypeSpec fn Three → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn Three → [Three] → Specification fn Three Source # guardTypeSpec ∷ [String] → TypeSpec fn Three → Specification fn Three Source # prerequisites ∷ Evidence (Prerequisites fn Three) Source #
BaseUniverse fn ⇒ HasSpec fn FooBarBaz Source #
Instance details Defined in Constrained.Examples.CheatSheet Associated Types type TypeSpec fn FooBarBaz Source # type Prerequisites fn FooBarBaz Source # Methods emptySpec ∷ TypeSpec fn FooBarBaz Source # combineSpec ∷ TypeSpec fn FooBarBaz → TypeSpec fn FooBarBaz → Specification fn FooBarBaz Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn FooBarBaz → GenT m FooBarBaz Source # conformsTo ∷ FooBarBaz → TypeSpec fn FooBarBaz → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn FooBarBaz → FooBarBaz → [FooBarBaz] Source # toPreds ∷ Term fn FooBarBaz → TypeSpec fn FooBarBaz → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn FooBarBaz → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn FooBarBaz → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn FooBarBaz → BinaryShow Source # monadConformsTo ∷ FooBarBaz → TypeSpec fn FooBarBaz → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn FooBarBaz → [FooBarBaz] → Specification fn FooBarBaz Source # guardTypeSpec ∷ [String] → TypeSpec fn FooBarBaz → Specification fn FooBarBaz Source # prerequisites ∷ Evidence (Prerequisites fn FooBarBaz) Source #
BaseUniverse fn ⇒ HasSpec fn Integer Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn Integer Source # type Prerequisites fn Integer Source # Methods emptySpec ∷ TypeSpec fn Integer Source # combineSpec ∷ TypeSpec fn Integer → TypeSpec fn Integer → Specification fn Integer Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn Integer → GenT m Integer Source # conformsTo ∷ Integer → TypeSpec fn Integer → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn Integer → Integer → [Integer] Source # toPreds ∷ Term fn Integer → TypeSpec fn Integer → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn Integer → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn Integer → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn Integer → BinaryShow Source # monadConformsTo ∷ Integer → TypeSpec fn Integer → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn Integer → [Integer] → Specification fn Integer Source # guardTypeSpec ∷ [String] → TypeSpec fn Integer → Specification fn Integer Source # prerequisites ∷ Evidence (Prerequisites fn Integer) Source #
BaseUniverse fn ⇒ HasSpec fn Natural Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn Natural Source # type Prerequisites fn Natural Source # Methods emptySpec ∷ TypeSpec fn Natural Source # combineSpec ∷ TypeSpec fn Natural → TypeSpec fn Natural → Specification fn Natural Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn Natural → GenT m Natural Source # conformsTo ∷ Natural → TypeSpec fn Natural → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn Natural → Natural → [Natural] Source # toPreds ∷ Term fn Natural → TypeSpec fn Natural → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn Natural → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn Natural → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn Natural → BinaryShow Source # monadConformsTo ∷ Natural → TypeSpec fn Natural → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn Natural → [Natural] → Specification fn Natural Source # guardTypeSpec ∷ [String] → TypeSpec fn Natural → Specification fn Natural Source # prerequisites ∷ Evidence (Prerequisites fn Natural) Source #
BaseUniverse fn ⇒ HasSpec fn () Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn () Source # type Prerequisites fn () Source # Methods emptySpec ∷ TypeSpec fn () Source # combineSpec ∷ TypeSpec fn () → TypeSpec fn () → Specification fn () Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn () → GenT m () Source # conformsTo ∷ () → TypeSpec fn () → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn () → () → [()] Source # toPreds ∷ Term fn () → TypeSpec fn () → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn () → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn () → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn () → BinaryShow Source # monadConformsTo ∷ () → TypeSpec fn () → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn () → [()] → Specification fn () Source # guardTypeSpec ∷ [String] → TypeSpec fn () → Specification fn () Source # prerequisites ∷ Evidence (Prerequisites fn ()) Source #
(BaseUniverse fn, HasSpec fn ()) ⇒ HasSpec fn Bool Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn Bool Source # type Prerequisites fn Bool Source # Methods emptySpec ∷ TypeSpec fn Bool Source # combineSpec ∷ TypeSpec fn Bool → TypeSpec fn Bool → Specification fn Bool Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn Bool → GenT m Bool Source # conformsTo ∷ Bool → TypeSpec fn Bool → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn Bool → Bool → [Bool] Source # toPreds ∷ Term fn Bool → TypeSpec fn Bool → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn Bool → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn Bool → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn Bool → BinaryShow Source # monadConformsTo ∷ Bool → TypeSpec fn Bool → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn Bool → [Bool] → Specification fn Bool Source # guardTypeSpec ∷ [String] → TypeSpec fn Bool → Specification fn Bool Source # prerequisites ∷ Evidence (Prerequisites fn Bool) Source #
BaseUniverse fn ⇒ HasSpec fn Float Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn Float Source # type Prerequisites fn Float Source # Methods emptySpec ∷ TypeSpec fn Float Source # combineSpec ∷ TypeSpec fn Float → TypeSpec fn Float → Specification fn Float Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn Float → GenT m Float Source # conformsTo ∷ Float → TypeSpec fn Float → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn Float → Float → [Float] Source # toPreds ∷ Term fn Float → TypeSpec fn Float → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn Float → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn Float → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn Float → BinaryShow Source # monadConformsTo ∷ Float → TypeSpec fn Float → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn Float → [Float] → Specification fn Float Source # guardTypeSpec ∷ [String] → TypeSpec fn Float → Specification fn Float Source # prerequisites ∷ Evidence (Prerequisites fn Float) Source #
BaseUniverse fn ⇒ HasSpec fn Int Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn Int Source # type Prerequisites fn Int Source # Methods emptySpec ∷ TypeSpec fn Int Source # combineSpec ∷ TypeSpec fn Int → TypeSpec fn Int → Specification fn Int Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn Int → GenT m Int Source # conformsTo ∷ Int → TypeSpec fn Int → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn Int → Int → [Int] Source # toPreds ∷ Term fn Int → TypeSpec fn Int → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn Int → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn Int → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn Int → BinaryShow Source # monadConformsTo ∷ Int → TypeSpec fn Int → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn Int → [Int] → Specification fn Int Source # guardTypeSpec ∷ [String] → TypeSpec fn Int → Specification fn Int Source # prerequisites ∷ Evidence (Prerequisites fn Int) Source #
BaseUniverse fn ⇒ HasSpec fn (Ratio Integer) Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn (Ratio Integer) Source # type Prerequisites fn (Ratio Integer) Source # Methods emptySpec ∷ TypeSpec fn (Ratio Integer) Source # combineSpec ∷ TypeSpec fn (Ratio Integer) → TypeSpec fn (Ratio Integer) → Specification fn (Ratio Integer) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (Ratio Integer) → GenT m (Ratio Integer) Source # conformsTo ∷ Ratio Integer → TypeSpec fn (Ratio Integer) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (Ratio Integer) → Ratio Integer → [Ratio Integer] Source # toPreds ∷ Term fn (Ratio Integer) → TypeSpec fn (Ratio Integer) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (Ratio Integer) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (Ratio Integer) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (Ratio Integer) → BinaryShow Source # monadConformsTo ∷ Ratio Integer → TypeSpec fn (Ratio Integer) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (Ratio Integer) → [Ratio Integer] → Specification fn (Ratio Integer) Source # guardTypeSpec ∷ [String] → TypeSpec fn (Ratio Integer) → Specification fn (Ratio Integer) Source # prerequisites ∷ Evidence (Prerequisites fn (Ratio Integer)) Source #
(Ord a, HasSpec fn a) ⇒ HasSpec fn (NotASet a) Source #
Instance details Defined in Constrained.Examples.Set Associated Types type TypeSpec fn (NotASet a) Source # type Prerequisites fn (NotASet a) Source # Methods emptySpec ∷ TypeSpec fn (NotASet a) Source # combineSpec ∷ TypeSpec fn (NotASet a) → TypeSpec fn (NotASet a) → Specification fn (NotASet a) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (NotASet a) → GenT m (NotASet a) Source # conformsTo ∷ NotASet a → TypeSpec fn (NotASet a) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (NotASet a) → NotASet a → [NotASet a] Source # toPreds ∷ Term fn (NotASet a) → TypeSpec fn (NotASet a) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (NotASet a) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (NotASet a) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (NotASet a) → BinaryShow Source # monadConformsTo ∷ NotASet a → TypeSpec fn (NotASet a) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (NotASet a) → [NotASet a] → Specification fn (NotASet a) Source # guardTypeSpec ∷ [String] → TypeSpec fn (NotASet a) → Specification fn (NotASet a) Source # prerequisites ∷ Evidence (Prerequisites fn (NotASet a)) Source #
HasSpec fn a ⇒ HasSpec fn (BinTree a) Source #
Instance details Defined in Constrained.Spec.Tree Associated Types type TypeSpec fn (BinTree a) Source # type Prerequisites fn (BinTree a) Source # Methods emptySpec ∷ TypeSpec fn (BinTree a) Source # combineSpec ∷ TypeSpec fn (BinTree a) → TypeSpec fn (BinTree a) → Specification fn (BinTree a) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (BinTree a) → GenT m (BinTree a) Source # conformsTo ∷ BinTree a → TypeSpec fn (BinTree a) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (BinTree a) → BinTree a → [BinTree a] Source # toPreds ∷ Term fn (BinTree a) → TypeSpec fn (BinTree a) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (BinTree a) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (BinTree a) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (BinTree a) → BinaryShow Source # monadConformsTo ∷ BinTree a → TypeSpec fn (BinTree a) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (BinTree a) → [BinTree a] → Specification fn (BinTree a) Source # guardTypeSpec ∷ [String] → TypeSpec fn (BinTree a) → Specification fn (BinTree a) Source # prerequisites ∷ Evidence (Prerequisites fn (BinTree a)) Source #
(Ord a, HasSpec fn a) ⇒ HasSpec fn (Set a) Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn (Set a) Source # type Prerequisites fn (Set a) Source # Methods emptySpec ∷ TypeSpec fn (Set a) Source # combineSpec ∷ TypeSpec fn (Set a) → TypeSpec fn (Set a) → Specification fn (Set a) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (Set a) → GenT m (Set a) Source # conformsTo ∷ Set a → TypeSpec fn (Set a) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (Set a) → Set a → [Set a] Source # toPreds ∷ Term fn (Set a) → TypeSpec fn (Set a) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (Set a) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (Set a) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (Set a) → BinaryShow Source # monadConformsTo ∷ Set a → TypeSpec fn (Set a) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (Set a) → [Set a] → Specification fn (Set a) Source # guardTypeSpec ∷ [String] → TypeSpec fn (Set a) → Specification fn (Set a) Source # prerequisites ∷ Evidence (Prerequisites fn (Set a)) Source #
(HasSpec fn a, Member (TreeFn fn) fn) ⇒ HasSpec fn (Tree a) Source #
Instance details Defined in Constrained.Spec.Tree Associated Types type TypeSpec fn (Tree a) Source # type Prerequisites fn (Tree a) Source # Methods emptySpec ∷ TypeSpec fn (Tree a) Source # combineSpec ∷ TypeSpec fn (Tree a) → TypeSpec fn (Tree a) → Specification fn (Tree a) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (Tree a) → GenT m (Tree a) Source # conformsTo ∷ Tree a → TypeSpec fn (Tree a) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (Tree a) → Tree a → [Tree a] Source # toPreds ∷ Term fn (Tree a) → TypeSpec fn (Tree a) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (Tree a) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (Tree a) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (Tree a) → BinaryShow Source # monadConformsTo ∷ Tree a → TypeSpec fn (Tree a) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (Tree a) → [Tree a] → Specification fn (Tree a) Source # guardTypeSpec ∷ [String] → TypeSpec fn (Tree a) → Specification fn (Tree a) Source # prerequisites ∷ Evidence (Prerequisites fn (Tree a)) Source #
(IsNormalType a, HasSpec fn a) ⇒ HasSpec fn (Maybe a) Source #
Instance details Defined in Constrained.Spec.Generics Associated Types type TypeSpec fn (Maybe a) Source # type Prerequisites fn (Maybe a) Source # Methods emptySpec ∷ TypeSpec fn (Maybe a) Source # combineSpec ∷ TypeSpec fn (Maybe a) → TypeSpec fn (Maybe a) → Specification fn (Maybe a) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (Maybe a) → GenT m (Maybe a) Source # conformsTo ∷ Maybe a → TypeSpec fn (Maybe a) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (Maybe a) → Maybe a → [Maybe a] Source # toPreds ∷ Term fn (Maybe a) → TypeSpec fn (Maybe a) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (Maybe a) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (Maybe a) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (Maybe a) → BinaryShow Source # monadConformsTo ∷ Maybe a → TypeSpec fn (Maybe a) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (Maybe a) → [Maybe a] → Specification fn (Maybe a) Source # guardTypeSpec ∷ [String] → TypeSpec fn (Maybe a) → Specification fn (Maybe a) Source # prerequisites ∷ Evidence (Prerequisites fn (Maybe a)) Source #
HasSpec fn a ⇒ HasSpec fn [a] Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn [a] Source # type Prerequisites fn [a] Source # Methods emptySpec ∷ TypeSpec fn [a] Source # combineSpec ∷ TypeSpec fn [a] → TypeSpec fn [a] → Specification fn [a] Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn [a] → GenT m [a] Source # conformsTo ∷ [a] → TypeSpec fn [a] → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn [a] → [a] → [[a]] Source # toPreds ∷ Term fn [a] → TypeSpec fn [a] → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn [a] → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # 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 # guardTypeSpec ∷ [String] → TypeSpec fn [a] → Specification fn [a] Source # prerequisites ∷ Evidence (Prerequisites fn [a]) Source #
(HasSpec fn a, IsNormalType a, HasSpec fn b, IsNormalType b) ⇒ HasSpec fn (Either a b) Source #
Instance details Defined in Constrained.Spec.Generics Associated Types type TypeSpec fn (Either a b) Source # type Prerequisites fn (Either a b) Source # Methods emptySpec ∷ TypeSpec fn (Either a b) Source # combineSpec ∷ TypeSpec fn (Either a b) → TypeSpec fn (Either a b) → Specification fn (Either a b) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (Either a b) → GenT m (Either a b) Source # conformsTo ∷ Either a b → TypeSpec fn (Either a b) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (Either a b) → Either a b → [Either a b] Source # toPreds ∷ Term fn (Either a b) → TypeSpec fn (Either a b) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (Either a b) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (Either a b) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (Either a b) → BinaryShow Source # monadConformsTo ∷ Either a b → TypeSpec fn (Either a b) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (Either a b) → [Either a b] → Specification fn (Either a b) Source # guardTypeSpec ∷ [String] → TypeSpec fn (Either a b) → Specification fn (Either a b) Source # prerequisites ∷ Evidence (Prerequisites fn (Either a b)) Source #
(HasSpec fn a, HasSpec fn b) ⇒ HasSpec fn (Prod a b) Source #
Instance details Defined in Constrained.Spec.Pairs Associated Types type TypeSpec fn (Prod a b) Source # type Prerequisites fn (Prod a b) Source # Methods emptySpec ∷ TypeSpec fn (Prod a b) Source # combineSpec ∷ TypeSpec fn (Prod a b) → TypeSpec fn (Prod a b) → Specification fn (Prod a b) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (Prod a b) → GenT m (Prod a b) Source # conformsTo ∷ Prod a b → TypeSpec fn (Prod a b) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (Prod a b) → Prod a b → [Prod a b] Source # toPreds ∷ Term fn (Prod a b) → TypeSpec fn (Prod a b) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (Prod a b) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (Prod a b) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (Prod a b) → BinaryShow Source # monadConformsTo ∷ Prod a b → TypeSpec fn (Prod a b) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (Prod a b) → [Prod a b] → Specification fn (Prod a b) Source # guardTypeSpec ∷ [String] → TypeSpec fn (Prod a b) → Specification fn (Prod a b) Source # prerequisites ∷ Evidence (Prerequisites fn (Prod a b)) Source #
(HasSpec fn a, HasSpec fn b, KnownNat (CountCases b)) ⇒ HasSpec fn (Sum a b) Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec fn (Sum a b) Source # type Prerequisites fn (Sum a b) Source # Methods emptySpec ∷ TypeSpec fn (Sum a b) Source # combineSpec ∷ TypeSpec fn (Sum a b) → TypeSpec fn (Sum a b) → Specification fn (Sum a b) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (Sum a b) → GenT m (Sum a b) Source # conformsTo ∷ Sum a b → TypeSpec fn (Sum a b) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (Sum a b) → Sum a b → [Sum a b] Source # toPreds ∷ Term fn (Sum a b) → TypeSpec fn (Sum a b) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (Sum a b) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (Sum a b) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (Sum a b) → BinaryShow Source # monadConformsTo ∷ Sum a b → TypeSpec fn (Sum a b) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (Sum a b) → [Sum a b] → Specification fn (Sum a b) Source # guardTypeSpec ∷ [String] → TypeSpec fn (Sum a b) → Specification fn (Sum a b) Source # prerequisites ∷ Evidence (Prerequisites fn (Sum a b)) Source #
(Ord k, HasSpec fn (Prod k v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) ⇒ HasSpec fn (Map k v) Source #
Instance details Defined in Constrained.Spec.Map Associated Types type TypeSpec fn (Map k v) Source # type Prerequisites fn (Map k v) Source # Methods emptySpec ∷ TypeSpec fn (Map k v) Source # combineSpec ∷ TypeSpec fn (Map k v) → TypeSpec fn (Map k v) → Specification fn (Map k v) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (Map k v) → GenT m (Map k v) Source # conformsTo ∷ Map k v → TypeSpec fn (Map k v) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (Map k v) → Map k v → [Map k v] Source # toPreds ∷ Term fn (Map k v) → TypeSpec fn (Map k v) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (Map k v) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (Map k v) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (Map k v) → BinaryShow Source # monadConformsTo ∷ Map k v → TypeSpec fn (Map k v) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (Map k v) → [Map k v] → Specification fn (Map k v) Source # guardTypeSpec ∷ [String] → TypeSpec fn (Map k v) → Specification fn (Map k v) Source # prerequisites ∷ Evidence (Prerequisites fn (Map k v)) Source #
(HasSpec fn a, HasSpec fn b) ⇒ HasSpec fn (a, b) Source #
Instance details Defined in Constrained.Spec.Generics Associated Types type TypeSpec fn (a, b) Source # type Prerequisites fn (a, b) Source # Methods emptySpec ∷ TypeSpec fn (a, b) Source # combineSpec ∷ TypeSpec fn (a, b) → TypeSpec fn (a, b) → Specification fn (a, b) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (a, b) → GenT m (a, b) Source # conformsTo ∷ (a, b) → TypeSpec fn (a, b) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (a, b) → (a, b) → [(a, b)] Source # toPreds ∷ Term fn (a, b) → TypeSpec fn (a, b) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (a, b) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (a, b) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (a, b) → BinaryShow Source # monadConformsTo ∷ (a, b) → TypeSpec fn (a, b) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (a, b) → [(a, b)] → Specification fn (a, b) Source # guardTypeSpec ∷ [String] → TypeSpec fn (a, b) → Specification fn (a, b) Source # prerequisites ∷ Evidence (Prerequisites fn (a, b)) Source #
(HasSpec fn a, HasSpec fn b, HasSpec fn c) ⇒ HasSpec fn (a, b, c) Source #
Instance details Defined in Constrained.Spec.Generics Associated Types type TypeSpec fn (a, b, c) Source # type Prerequisites fn (a, b, c) Source # Methods emptySpec ∷ TypeSpec fn (a, b, c) Source # combineSpec ∷ TypeSpec fn (a, b, c) → TypeSpec fn (a, b, c) → Specification fn (a, b, c) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (a, b, c) → GenT m (a, b, c) Source # conformsTo ∷ (a, b, c) → TypeSpec fn (a, b, c) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (a, b, c) → (a, b, c) → [(a, b, c)] Source # toPreds ∷ Term fn (a, b, c) → TypeSpec fn (a, b, c) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (a, b, c) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (a, b, c) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (a, b, c) → BinaryShow Source # monadConformsTo ∷ (a, b, c) → TypeSpec fn (a, b, c) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (a, b, c) → [(a, b, c)] → Specification fn (a, b, c) Source # guardTypeSpec ∷ [String] → TypeSpec fn (a, b, c) → Specification fn (a, b, c) Source # prerequisites ∷ Evidence (Prerequisites fn (a, b, c)) Source #
(HasSpec fn a, HasSpec fn b, HasSpec fn c, HasSpec fn d) ⇒ HasSpec fn (a, b, c, d) Source #
Instance details Defined in Constrained.Spec.Generics Associated Types type TypeSpec fn (a, b, c, d) Source # type Prerequisites fn (a, b, c, d) Source # Methods emptySpec ∷ TypeSpec fn (a, b, c, d) Source # combineSpec ∷ TypeSpec fn (a, b, c, d) → TypeSpec fn (a, b, c, d) → Specification fn (a, b, c, d) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (a, b, c, d) → GenT m (a, b, c, d) Source # conformsTo ∷ (a, b, c, d) → TypeSpec fn (a, b, c, d) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (a, b, c, d) → (a, b, c, d) → [(a, b, c, d)] Source # toPreds ∷ Term fn (a, b, c, d) → TypeSpec fn (a, b, c, d) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (a, b, c, d) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (a, b, c, d) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (a, b, c, d) → BinaryShow Source # monadConformsTo ∷ (a, b, c, d) → TypeSpec fn (a, b, c, d) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (a, b, c, d) → [(a, b, c, d)] → Specification fn (a, b, c, d) Source # guardTypeSpec ∷ [String] → TypeSpec fn (a, b, c, d) → Specification fn (a, b, c, d) Source # prerequisites ∷ Evidence (Prerequisites fn (a, b, c, d)) Source #
(HasSpec fn a, HasSpec fn b, HasSpec fn c, HasSpec fn d, HasSpec fn e) ⇒ HasSpec fn (a, b, c, d, e) Source #
Instance details Defined in Constrained.Spec.Generics Associated Types type TypeSpec fn (a, b, c, d, e) Source # type Prerequisites fn (a, b, c, d, e) Source # Methods emptySpec ∷ TypeSpec fn (a, b, c, d, e) Source # combineSpec ∷ TypeSpec fn (a, b, c, d, e) → TypeSpec fn (a, b, c, d, e) → Specification fn (a, b, c, d, e) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (a, b, c, d, e) → GenT m (a, b, c, d, e) Source # conformsTo ∷ (a, b, c, d, e) → TypeSpec fn (a, b, c, d, e) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (a, b, c, d, e) → (a, b, c, d, e) → [(a, b, c, d, e)] Source # toPreds ∷ Term fn (a, b, c, d, e) → TypeSpec fn (a, b, c, d, e) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (a, b, c, d, e) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (a, b, c, d, e) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (a, b, c, d, e) → BinaryShow Source # monadConformsTo ∷ (a, b, c, d, e) → TypeSpec fn (a, b, c, d, e) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (a, b, c, d, e) → [(a, b, c, d, e)] → Specification fn (a, b, c, d, e) Source # guardTypeSpec ∷ [String] → TypeSpec fn (a, b, c, d, e) → Specification fn (a, b, c, d, e) Source # prerequisites ∷ Evidence (Prerequisites fn (a, b, c, d, e)) Source #
(HasSpec fn a, HasSpec fn b, HasSpec fn c, HasSpec fn d, HasSpec fn e, HasSpec fn g) ⇒ HasSpec fn (a, b, c, d, e, g) Source #
Instance details Defined in Constrained.Spec.Generics Associated Types type TypeSpec fn (a, b, c, d, e, g) Source # type Prerequisites fn (a, b, c, d, e, g) Source # Methods emptySpec ∷ TypeSpec fn (a, b, c, d, e, g) Source # combineSpec ∷ TypeSpec fn (a, b, c, d, e, g) → TypeSpec fn (a, b, c, d, e, g) → Specification fn (a, b, c, d, e, g) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (a, b, c, d, e, g) → GenT m (a, b, c, d, e, g) Source # conformsTo ∷ (a, b, c, d, e, g) → TypeSpec fn (a, b, c, d, e, g) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (a, b, c, d, e, g) → (a, b, c, d, e, g) → [(a, b, c, d, e, g)] Source # toPreds ∷ Term fn (a, b, c, d, e, g) → TypeSpec fn (a, b, c, d, e, g) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (a, b, c, d, e, g) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (a, b, c, d, e, g) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (a, b, c, d, e, g) → BinaryShow Source # monadConformsTo ∷ (a, b, c, d, e, g) → TypeSpec fn (a, b, c, d, e, g) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (a, b, c, d, e, g) → [(a, b, c, d, e, g)] → Specification fn (a, b, c, d, e, g) Source # guardTypeSpec ∷ [String] → TypeSpec fn (a, b, c, d, e, g) → Specification fn (a, b, c, d, e, g) Source # prerequisites ∷ Evidence (Prerequisites fn (a, b, c, d, e, g)) Source #
(HasSpec fn a, HasSpec fn b, HasSpec fn c, HasSpec fn d, HasSpec fn e, HasSpec fn g, HasSpec fn h) ⇒ HasSpec fn (a, b, c, d, e, g, h) Source #
Instance details Defined in Constrained.Spec.Generics Associated Types type TypeSpec fn (a, b, c, d, e, g, h) Source # type Prerequisites fn (a, b, c, d, e, g, h) Source # Methods emptySpec ∷ TypeSpec fn (a, b, c, d, e, g, h) Source # combineSpec ∷ TypeSpec fn (a, b, c, d, e, g, h) → TypeSpec fn (a, b, c, d, e, g, h) → Specification fn (a, b, c, d, e, g, h) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (a, b, c, d, e, g, h) → GenT m (a, b, c, d, e, g, h) Source # conformsTo ∷ (a, b, c, d, e, g, h) → TypeSpec fn (a, b, c, d, e, g, h) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (a, b, c, d, e, g, h) → (a, b, c, d, e, g, h) → [(a, b, c, d, e, g, h)] Source # toPreds ∷ Term fn (a, b, c, d, e, g, h) → TypeSpec fn (a, b, c, d, e, g, h) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (a, b, c, d, e, g, h) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (a, b, c, d, e, g, h) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (a, b, c, d, e, g, h) → BinaryShow Source # monadConformsTo ∷ (a, b, c, d, e, g, h) → TypeSpec fn (a, b, c, d, e, g, h) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (a, b, c, d, e, g, h) → [(a, b, c, d, e, g, h)] → Specification fn (a, b, c, d, e, g, h) Source # guardTypeSpec ∷ [String] → TypeSpec fn (a, b, c, d, e, g, h) → Specification fn (a, b, c, d, e, g, h) Source # prerequisites ∷ Evidence (Prerequisites fn (a, b, c, d, e, g, h)) Source #

data WithHasSpec fn f a where Source #

Constructors

WithHasSpec ∷ HasSpec fn a ⇒ f a → WithHasSpec fn f a

Instances

Instances details

HasSpecImpliesEq fn a f ⇒ Eq (WithHasSpec fn f a) Source #
Instance details Defined in Constrained.Base Methods (==) ∷ WithHasSpec fn f a → WithHasSpec fn f a → Bool Source # (/=) ∷ WithHasSpec fn f a → WithHasSpec fn f a → Bool Source #

class Forallable t e | t → e where Source #

Minimal complete definition

Nothing

Methods

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

Instances details

Ord a ⇒ Forallable (NotASet a) a Source #
Instance details Defined in Constrained.Examples.Set Methods fromForAllSpec ∷ ∀ (fn ∷ [Type] → Type → Type). (HasSpec fn (NotASet a), HasSpec fn a, BaseUniverse fn) ⇒ Specification fn a → Specification fn (NotASet a) Source # forAllToList ∷ NotASet a → [a] Source #
Ord a ⇒ Forallable (Set a) a Source #
Instance details Defined in Constrained.Base Methods fromForAllSpec ∷ ∀ (fn ∷ [Type] → Type → Type). (HasSpec fn (Set a), HasSpec fn a, BaseUniverse fn) ⇒ Specification fn a → Specification fn (Set a) Source # forAllToList ∷ Set a → [a] Source #
Forallable [a] a Source #
Instance details Defined in Constrained.Base Methods fromForAllSpec ∷ ∀ (fn ∷ [Type] → Type → Type). (HasSpec fn [a], HasSpec fn a, BaseUniverse fn) ⇒ Specification fn a → Specification fn [a] Source # forAllToList ∷ [a] → [a] Source #
Forallable (Tree a) (a, [Tree a]) Source #
Instance details Defined in Constrained.Spec.Tree Methods fromForAllSpec ∷ ∀ (fn ∷ [Type] → Type → Type). (HasSpec fn (Tree a), HasSpec fn (a, [Tree a]), BaseUniverse fn) ⇒ Specification fn (a, [Tree a]) → Specification fn (Tree a) Source # forAllToList ∷ Tree a → [(a, [Tree a])] Source #
Forallable (BinTree a) (BinTree a, a, BinTree a) Source #
Instance details Defined in Constrained.Spec.Tree Methods fromForAllSpec ∷ ∀ (fn ∷ [Type] → Type → Type). (HasSpec fn (BinTree a), HasSpec fn (BinTree a, a, BinTree a), BaseUniverse fn) ⇒ Specification fn (BinTree a, a, BinTree a) → Specification fn (BinTree a) Source # forAllToList ∷ BinTree a → [(BinTree a, a, BinTree a)] Source #
Ord k ⇒ Forallable (Map k v) (k, v) Source #
Instance details Defined in Constrained.Spec.Map Methods fromForAllSpec ∷ ∀ (fn ∷ [Type] → Type → Type). (HasSpec fn (Map k v), HasSpec fn (k, v), BaseUniverse fn) ⇒ Specification fn (k, v) → Specification fn (Map k v) Source # forAllToList ∷ Map k v → [(k, v)] Source #

class (HasSpec fn a, Show (Hint a)) ⇒ HasGenHint fn a where Source #

Hints are things that only affect generation, and not validation. For instance, parameters to control distribution of generated values.

Associated Types

type Hint a Source #

Methods

giveHint ∷ Hint a → Specification fn a Source #

Instances

Instances details

HasSpec fn a ⇒ HasGenHint fn (BinTree a) Source #
Instance details Defined in Constrained.Spec.Tree Associated Types type Hint (BinTree a) Source # Methods giveHint ∷ Hint (BinTree a) → Specification fn (BinTree a) Source #
(Member (TreeFn fn) fn, HasSpec fn a) ⇒ HasGenHint fn (Tree a) Source #
Instance details Defined in Constrained.Spec.Tree Associated Types type Hint (Tree a) Source # Methods giveHint ∷ Hint (Tree a) → Specification fn (Tree a) Source #
HasSpec fn a ⇒ HasGenHint fn [a] Source #
Instance details Defined in Constrained.Base Associated Types type Hint [a] Source # Methods giveHint ∷ Hint [a] → Specification fn [a] Source #
(Ord k, HasSpec fn (Prod k v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) ⇒ HasGenHint fn (Map k v) Source #
Instance details Defined in Constrained.Spec.Map Associated Types type Hint (Map k v) Source # Methods giveHint ∷ Hint (Map k v) → Specification fn (Map k v) Source #

conformsToSpecM ∷ ∀ fn a m. (HasSpec fn a, MonadGenError m) ⇒ a → Specification fn a → m () Source #

conformsToSpecProp ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a → Property Source #

conformsToSpec ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a → Bool Source #

satisfies ∷ ∀ fn a. HasSpec fn a ⇒ Term fn a → Specification fn a → Pred fn 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.

shrinkWithSpec ∷ ∀ fn a. HasSpec fn a ⇒ Specification fn a → a → [a] Source #

shrinkFromPreds ∷ HasSpec fn a ⇒ Pred fn → Var a → a → [a] Source #

shrinkEnvFromPlan ∷ Env → SolverPlan fn → [Env] Source #

fixupWithSpec ∷ ∀ fn a. HasSpec fn a ⇒ Specification fn a → a → Maybe a Source #

envFromPred ∷ Env → Pred fn → GE Env Source #

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

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

flattenPred ∷ ∀ fn. BaseUniverse fn ⇒ Pred fn → [Pred fn] Source #

Flatten nested Let, Exists, and Block in a `Pred fn`. Let and Exists bound variables become free in the result.

computeDependencies ∷ Pred fn → DependGraph fn Source #

data SolverStage fn where Source #

Constructors

SolverStage
Fields ∷ HasSpec fn a ⇒ { stageVar ∷ Var a , stagePreds ∷ [Pred fn] , stageSpec ∷ Specification fn a } → SolverStage fn

Instances

Instances details

Pretty (SolverStage fn) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ SolverStage fn → Doc ann Source # prettyList ∷ [SolverStage fn] → Doc ann Source #

data SolverPlan fn Source #

Constructors

SolverPlan
Fields solverPlan ∷ [SolverStage fn] solverDependencies ∷ Graph (Name fn)

Instances

Instances details

Pretty (SolverPlan fn) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ SolverPlan fn → Doc ann Source # prettyList ∷ [SolverPlan fn] → Doc ann Source #

isTrueSpec ∷ Specification fn a → Bool Source #

prettyLinear ∷ [SolverStage fn] → Doc ann Source #

prepareLinearization ∷ ∀ fn. BaseUniverse fn ⇒ Pred fn → GE (SolverPlan fn) Source #

Linearize a predicate, turning it into a list of variables to solve and their defining constraints such that each variable can be solved independently.

saturatePred ∷ ∀ fn. Pred fn → [Pred fn] Source #

mergeSolverStage ∷ SolverStage fn → [SolverStage fn] → [SolverStage fn] Source #

Does nothing if the variable is not in the plan already.

backPropagation ∷ ∀ fn. SolverPlan fn → SolverPlan fn Source #

Push as much information we can backwards through the plan.

pattern Eql ∷ ∀ fn. () ⇒ ∀ a. HasSpec fn a ⇒ Term fn a → Term fn a → Term fn Bool Source #

pattern FromG ∷ ∀ fn a. () ⇒ (HasSpec fn a, HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Term fn (SimpleRep a) → Term fn a Source #

pattern SLeft ∷ ∀ fn a. () ⇒ ∀ b c. (HasSpec fn b, a ~ Sum b c) ⇒ Term fn b → Term fn a Source #

pattern SRight ∷ ∀ fn a. () ⇒ ∀ b c. (HasSpec fn c, a ~ Sum b c) ⇒ Term fn c → Term fn a Source #

pattern SubsetPat ∷ ∀ fn a. () ⇒ ∀ b. (Ord b, HasSpec fn (Set b), Show b, Typeable b, a ~ Bool) ⇒ Term fn (Set b) → Term fn (Set b) → Term fn a Source #

pattern DisjointPat ∷ ∀ fn a. () ⇒ ∀ b. (Ord b, HasSpec fn (Set b), Show b, Typeable b, a ~ Bool) ⇒ Term fn (Set b) → Term fn (Set b) → Term fn a Source #

pattern UnionPat ∷ ∀ fn a. () ⇒ ∀ b. (Ord b, HasSpec fn (Set b), Show b, Typeable b, a ~ Set b) ⇒ Term fn (Set b) → Term fn (Set b) → Term fn a Source #

pattern MemberPat ∷ ∀ fn a. () ⇒ ∀ b. (HasSpec fn b, HasSpec fn (Set b), Show b, Typeable b, a ~ Bool) ⇒ Term fn b → Term fn (Set b) → Term fn a Source #

pattern ElemPat ∷ ∀ fn a. () ⇒ ∀ b. (HasSpec fn b, HasSpec fn [b], Show b, Typeable b, a ~ Bool) ⇒ Term fn b → Term fn [b] → Term fn a Source #

pattern AppendPat ∷ ∀ fn a. () ⇒ ∀ b. (HasSpec fn [b], Show b, Typeable b, a ~ [b]) ⇒ Term fn [b] → Term fn [b] → Term fn a Source #

short ∷ ∀ a x. (Show a, Typeable a) ⇒ [a] → Doc x Source #

prettyPlan ∷ HasSpec fn a ⇒ Specification fn a → Doc ann Source #

printPlan ∷ HasSpec fn a ⇒ Specification fn a → IO () Source #

isEmptyPlan ∷ SolverPlan fn → Bool Source #

stepPlan ∷ MonadGenError m ⇒ Env → SolverPlan fn → GenT m (Env, SolverPlan fn) Source #

substStage ∷ Env → SolverStage fn → SolverStage fn Source #

genFromPreds ∷ ∀ fn m. (MonadGenError m, BaseUniverse fn) ⇒ Env → Pred fn → GenT m Env Source #

Generate a satisfying Env for a `p : Pred fn`. The Env contains values for all the free variables in `flattenPred p`.

computeHints ∷ ∀ fn. [Pred fn] → Hints fn Source #

computeBinderDependencies ∷ Binder fn a → DependGraph fn Source #

computeTermDependencies ∷ Term fn a → DependGraph fn Source #

computeTermDependencies' ∷ Term fn a → (DependGraph fn, Set (Name fn)) Source #

linearize ∷ (MonadGenError m, BaseUniverse fn) ⇒ [Pred fn] → DependGraph fn → m [SolverStage fn] Source #

normalizeSolverStage ∷ SolverStage fn → SolverStage fn Source #

fromGESpec ∷ (HasCallStack, HasSpec fn a) ⇒ GE (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

regularize ∷ HasVariables fn t ⇒ Var a → t → Var a Source #

regularizeBinder ∷ Binder fn a → Binder fn a Source #

regularizeNamesPred ∷ Pred fn → Pred fn Source #

regularizeNames ∷ Specification fn a → Specification fn a Source #

simplifySpec ∷ HasSpec fn a ⇒ Specification fn a → Specification fn a Source #

computeSpecSimplified ∷ ∀ fn a. (HasSpec fn a, HasCallStack) ⇒ Var a → Pred fn → GE (Specification fn a) Source #

Precondition: the `Pred fn` defines the `Var a`

Runs in GE in order for us to have detailed context on failure.

computeSpec ∷ ∀ fn a. (HasSpec fn a, HasCallStack) ⇒ Var a → Pred fn → GE (Specification fn a) Source #

Precondition: the `Pred fn` defines the `Var a`.

Runs in GE in order for us to have detailed context on failure.

computeSpecBinder ∷ Binder fn a → GE (Specification fn a) Source #

computeSpecBinderSimplified ∷ Binder fn a → GE (Specification fn a) Source #

caseSpec ∷ ∀ fn as. HasSpec fn (SumOver as) ⇒ Maybe String → List (Weighted (Specification fn)) as → Specification fn (SumOver as) Source #

Turn a list of branches into a SumSpec. If all the branches fail return an ErrorSpec.

totalWeight ∷ List (Weighted f) as → Maybe Int Source #

propagateSpec ∷ ∀ fn v a. HasSpec fn v ⇒ Specification fn a → Ctx fn v a → Specification fn v Source #

ctxHasSpec ∷ Ctx fn v a → Evidence (HasSpec fn a) Source #

class (∀ as b. Show (f as b), ∀ as b. Eq (f as b), Typeable f, FunctionLike f) ⇒ Functions f fn where Source #

Minimal complete definition

propagateSpecFun, mapTypeSpec

Methods

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

Instances details

(BaseUniverse fn, Member (FunFn fn) fn) ⇒ Functions (FunFn fn) fn Source #
Instance details Defined in Constrained.Base Methods 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 #
Instance details Defined in Constrained.Spec.Generics Methods 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 #
Instance details Defined in Constrained.Base Methods 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 #
Instance details Defined in Constrained.Base Methods 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 #
Instance details Defined in Constrained.Base Methods 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 #
Instance details Defined in Constrained.Base Methods 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 #
Instance details Defined in Constrained.Spec.Tree Methods 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 #
Instance details Defined in Constrained.Instances Methods 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 #
Instance details Defined in Constrained.Instances Methods 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 #
Instance details Defined in Constrained.Spec.Map Methods 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 #
Instance details Defined in Constrained.Spec.Pairs Methods 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 #
Instance details Defined in Constrained.Base Methods 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 #
Instance details Defined in Constrained.Spec.Generics Methods 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 #
Instance details Defined in Constrained.Instances Methods 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 #
Instance details Defined in Constrained.Instances Methods 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 #

mapSpec ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ fn '[a] b → Specification fn a → Specification fn b 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.

isErrorLike ∷ ∀ fn a. Specification fn a → Bool Source #

errorLikeMessage ∷ ∀ fn a. Specification fn a → NonEmpty String Source #

type DependGraph fn = Graph (Name fn) Source #

dependency ∷ HasVariables fn t ⇒ Name fn → t → DependGraph fn Source #

irreflexiveDependencyOn ∷ ∀ fn t t'. (HasVariables fn t, HasVariables fn t') ⇒ t → t' → DependGraph fn Source #

noDependencies ∷ HasVariables fn t ⇒ t → DependGraph fn Source #

type Hints fn = DependGraph fn Source #

respecting ∷ Hints f → DependGraph f → DependGraph f Source #

solvableFrom ∷ Name f → Set (Name f) → DependGraph f → Bool Source #

freeVarNames ∷ ∀ fn t. HasVariables fn t ⇒ t → Set Int Source #

data Name fn where Source #

Constructors

Name ∷ HasSpec fn a ⇒ Var a → Name fn

Instances

Instances details

HasVariables f (Name f) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ Name f → FreeVars f Source # freeVarSet ∷ Name f → Set (Name f) Source # countOf ∷ Name f → Name f → Int Source # appearsIn ∷ Name f → Name f → Bool Source #
Show (Name fn) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → Name fn → ShowS Source # show ∷ Name fn → String Source # showList ∷ [Name fn] → ShowS Source #
Rename (Name f) Source #
Instance details Defined in Constrained.Base Methods rename ∷ Typeable x ⇒ Var x → Var x → Name f → Name f Source #
Eq (Name fn) Source #
Instance details Defined in Constrained.Base Methods (==) ∷ Name fn → Name fn → Bool Source # (/=) ∷ Name fn → Name fn → Bool Source #
Ord (Name fn) Source #
Instance details Defined in Constrained.Base Methods compare ∷ Name fn → Name fn → Ordering Source # (<) ∷ Name fn → Name fn → Bool Source # (<=) ∷ Name fn → Name fn → Bool Source # (>) ∷ Name fn → Name fn → Bool Source # (>=) ∷ Name fn → Name fn → Bool Source # max ∷ Name fn → Name fn → Name fn Source # min ∷ Name fn → Name fn → Name fn Source #
Pretty (Name fn) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ Name fn → Doc ann Source # prettyList ∷ [Name fn] → Doc ann Source #

newtype FreeVars fn Source #

Constructors

FreeVars
Fields unFreeVars ∷ Map (Name fn) Int

Instances

Instances details

Monoid (FreeVars fn) Source #
Instance details Defined in Constrained.Base Methods mempty ∷ FreeVars fn Source # mappend ∷ FreeVars fn → FreeVars fn → FreeVars fn Source # mconcat ∷ [FreeVars fn] → FreeVars fn Source #
Semigroup (FreeVars fn) Source #
Instance details Defined in Constrained.Base Methods (<>) ∷ FreeVars fn → FreeVars fn → FreeVars fn Source # sconcat ∷ NonEmpty (FreeVars fn) → FreeVars fn Source # stimes ∷ Integral b ⇒ b → FreeVars fn → FreeVars fn Source #
Show (FreeVars fn) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → FreeVars fn → ShowS Source # show ∷ FreeVars fn → String Source # showList ∷ [FreeVars fn] → ShowS Source #

restrictedTo ∷ FreeVars fn → Set (Name fn) → FreeVars fn Source #

memberOf ∷ Name fn → FreeVars fn → Bool Source #

count ∷ Name fn → FreeVars fn → Int Source #

freeVar ∷ Name fn → FreeVars fn Source #

singleton ∷ Name fn → Int → FreeVars fn Source #

without ∷ Foldable t ⇒ FreeVars fn → t (Name fn) → FreeVars fn Source #

class HasVariables fn a | a → fn where Source #

Minimal complete definition

freeVars

Methods

freeVars ∷ a → FreeVars fn Source #

freeVarSet ∷ a → Set (Name fn) Source #

countOf ∷ Name fn → a → Int Source #

appearsIn ∷ Name fn → a → Bool Source #

Instances

Instances details

HasVariables f (Name f) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ Name f → FreeVars f Source # freeVarSet ∷ Name f → Set (Name f) Source # countOf ∷ Name f → Name f → Int Source # appearsIn ∷ Name f → Name f → Bool Source #
HasVariables f a ⇒ HasVariables f (Set a) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ Set a → FreeVars f Source # freeVarSet ∷ Set a → Set (Name f) Source # countOf ∷ Name f → Set a → Int Source # appearsIn ∷ Name f → Set a → Bool Source #
(Foldable t, HasVariables f a) ⇒ HasVariables f (t a) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ t a → FreeVars f Source # freeVarSet ∷ t a → Set (Name f) Source # countOf ∷ Name f → t a → Int Source # appearsIn ∷ Name f → t a → Bool Source #
HasVariables fn (Pred fn) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ Pred fn → FreeVars fn Source # freeVarSet ∷ Pred fn → Set (Name fn) Source # countOf ∷ Name fn → Pred fn → Int Source # appearsIn ∷ Name fn → Pred fn → Bool Source #
(HasVariables f a, HasVariables f b) ⇒ HasVariables f (a, b) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ (a, b) → FreeVars f Source # freeVarSet ∷ (a, b) → Set (Name f) Source # countOf ∷ Name f → (a, b) → Int Source # appearsIn ∷ Name f → (a, b) → Bool Source #
HasVariables fn (Binder fn a) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ Binder fn a → FreeVars fn Source # freeVarSet ∷ Binder fn a → Set (Name fn) Source # countOf ∷ Name fn → Binder fn a → Int Source # appearsIn ∷ Name fn → Binder fn a → Bool Source #
HasVariables fn (Term fn a) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ Term fn a → FreeVars fn Source # freeVarSet ∷ Term fn a → Set (Name fn) Source # countOf ∷ Name fn → Term fn a → Int Source # appearsIn ∷ Name fn → Term fn a → Bool Source #
HasVariables fn (f a) ⇒ HasVariables fn (Weighted f a) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ Weighted f a → FreeVars fn Source # freeVarSet ∷ Weighted f a → Set (Name fn) Source # countOf ∷ Name fn → Weighted f a → Int Source # appearsIn ∷ Name fn → Weighted f a → Bool Source #
HasVariables fn (List (Term fn) as) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ List (Term fn) as → FreeVars fn Source # freeVarSet ∷ List (Term fn) as → Set (Name fn) Source # countOf ∷ Name fn → List (Term fn) as → Int Source # appearsIn ∷ Name fn → List (Term fn) as → Bool Source #
HasVariables fn (List (Weighted (Binder fn)) as) Source #
Instance details Defined in Constrained.Base Methods freeVars ∷ List (Weighted (Binder fn)) as → FreeVars fn Source # freeVarSet ∷ List (Weighted (Binder fn)) as → Set (Name fn) Source # countOf ∷ Name fn → List (Weighted (Binder fn)) as → Int Source # appearsIn ∷ Name fn → List (Weighted (Binder fn)) as → Bool Source #

type Subst fn = [SubstEntry fn] Source #

data SubstEntry fn where Source #

Constructors

(:=) ∷ HasSpec fn a ⇒ Var a → Term fn a → SubstEntry fn

backwardsSubstitution ∷ ∀ fn a. HasSpec fn a ⇒ Subst fn → Term fn a → Term fn a Source #

fastInequality ∷ Term fn a → Term fn b → Bool Source #

Sound but not complete inequality on terms

substituteTerm ∷ ∀ fn a. Subst fn → Term fn a → Term fn a Source #

substituteTerm' ∷ ∀ fn a. Subst fn → Term fn a → Writer Any (Term fn a) Source #

substituteBinder ∷ HasSpec fn a ⇒ Var a → Term fn a → Binder fn b → Binder fn b Source #

substitutePred ∷ HasSpec fn a ⇒ Var a → Term fn a → Pred fn → Pred fn Source #

substTerm ∷ Env → Term fn a → Term fn a Source #

substBinder ∷ Env → Binder fn a → Binder fn a Source #

substPred ∷ BaseUniverse fn ⇒ Env → Pred fn → Pred fn Source #

unBind ∷ a → Binder fn a → Pred fn Source #

simplifyTerm ∷ ∀ fn a. BaseUniverse fn ⇒ Term fn a → Term fn a Source #

fromLits ∷ List (Term fn) as → Maybe (List Value as) Source #

fromLit ∷ Term fn a → Maybe (Value a) Source #

isLit ∷ Term fn a → Bool Source #

simplifyPred ∷ ∀ fn. BaseUniverse fn ⇒ Pred fn → Pred fn Source #

simplifyPreds ∷ BaseUniverse fn ⇒ [Pred fn] → [Pred fn] Source #

simplifyBinder ∷ Binder fn a → Binder fn a Source #

pinnedBy ∷ ∀ fn a. (BaseUniverse fn, Typeable a) ⇒ Var a → Pred fn → Maybe (Term fn a) Source #

Is the variable x pinned to some free term in p? (free term meaning that all the variables in the term are free in p).

TODO: complete this with more cases!

optimisePred ∷ BaseUniverse fn ⇒ Pred fn → Pred fn Source #

letSubexpressionElimination ∷ BaseUniverse fn ⇒ Pred fn → Pred fn Source #

letFloating ∷ BaseUniverse fn ⇒ Pred fn → Pred fn Source #

aggressiveInlining ∷ BaseUniverse fn ⇒ Pred fn → Pred fn Source #

substituteAndSimplifyTerm ∷ BaseUniverse fn ⇒ Subst fn → Term fn a → Term fn a Source #

Apply a substitution and simplify the resulting term if the substitution changed the term.

class HasSimpleRep a where Source #

Minimal complete definition

Nothing

Associated Types

type SimpleRep a Source #

type SimpleRep a = SOP (TheSop a)

type TheSop a ∷ [Type] Source #

type TheSop a = SOPOf (Rep a)

Methods

toSimpleRep ∷ a → SimpleRep a Source #

default toSimpleRep ∷ (Generic a, SimpleGeneric (Rep a), SimpleRep a ~ SimplifyRep (Rep a)) ⇒ a → SimpleRep a Source #

fromSimpleRep ∷ SimpleRep a → a Source #

default fromSimpleRep ∷ (Generic a, SimpleGeneric (Rep a), SimpleRep a ~ SimplifyRep (Rep a)) ⇒ SimpleRep a → a Source #

Instances

Instances details

HasSimpleRep Foo Source #
Instance details Defined in Constrained.Examples.Basic Associated Types type SimpleRep Foo Source # type TheSop Foo ∷ [Type] Source # Methods toSimpleRep ∷ Foo → SimpleRep Foo Source # fromSimpleRep ∷ SimpleRep Foo → Foo Source #
HasSimpleRep Three Source #
Instance details Defined in Constrained.Examples.Basic Associated Types type SimpleRep Three Source # type TheSop Three ∷ [Type] Source # Methods toSimpleRep ∷ Three → SimpleRep Three Source # fromSimpleRep ∷ SimpleRep Three → Three Source #
HasSimpleRep FooBarBaz Source #
Instance details Defined in Constrained.Examples.CheatSheet Associated Types type SimpleRep FooBarBaz Source # type TheSop FooBarBaz ∷ [Type] Source # Methods toSimpleRep ∷ FooBarBaz → SimpleRep FooBarBaz Source # fromSimpleRep ∷ SimpleRep FooBarBaz → FooBarBaz Source #
HasSimpleRep Bool Source #
Instance details Defined in Constrained.Base Associated Types type SimpleRep Bool Source # type TheSop Bool ∷ [Type] Source # Methods toSimpleRep ∷ Bool → SimpleRep Bool Source # fromSimpleRep ∷ SimpleRep Bool → Bool Source #
Ord a ⇒ HasSimpleRep (NotASet a) Source #
Instance details Defined in Constrained.Examples.Set Associated Types type SimpleRep (NotASet a) Source # type TheSop (NotASet a) ∷ [Type] Source # Methods toSimpleRep ∷ NotASet a → SimpleRep (NotASet a) Source # fromSimpleRep ∷ SimpleRep (NotASet a) → NotASet a Source #
HasSimpleRep (Maybe a) Source #
Instance details Defined in Constrained.Spec.Generics Associated Types type SimpleRep (Maybe a) Source # type TheSop (Maybe a) ∷ [Type] Source # Methods toSimpleRep ∷ Maybe a → SimpleRep (Maybe a) Source # fromSimpleRep ∷ SimpleRep (Maybe a) → Maybe a Source #
HasSimpleRep (Either a b) Source #
Instance details Defined in Constrained.Spec.Generics Associated Types type SimpleRep (Either a b) Source # type TheSop (Either a b) ∷ [Type] Source # Methods toSimpleRep ∷ Either a b → SimpleRep (Either a b) Source # fromSimpleRep ∷ SimpleRep (Either a b) → Either a b Source #
HasSimpleRep (a, b) Source #
Instance details Defined in Constrained.Spec.Generics Associated Types type SimpleRep (a, b) Source # type TheSop (a, b) ∷ [Type] Source # Methods toSimpleRep ∷ (a, b) → SimpleRep (a, b) Source # fromSimpleRep ∷ SimpleRep (a, b) → (a, b) Source #
HasSimpleRep (a, b, c) Source #
Instance details Defined in Constrained.Spec.Generics Associated Types type SimpleRep (a, b, c) Source # type TheSop (a, b, c) ∷ [Type] Source # Methods toSimpleRep ∷ (a, b, c) → SimpleRep (a, b, c) Source # fromSimpleRep ∷ SimpleRep (a, b, c) → (a, b, c) Source #
HasSimpleRep (a, b, c, d) Source #
Instance details Defined in Constrained.Spec.Generics Associated Types type SimpleRep (a, b, c, d) Source # type TheSop (a, b, c, d) ∷ [Type] Source # Methods toSimpleRep ∷ (a, b, c, d) → SimpleRep (a, b, c, d) Source # fromSimpleRep ∷ SimpleRep (a, b, c, d) → (a, b, c, d) Source #
HasSimpleRep (a, b, c, d, e) Source #
Instance details Defined in Constrained.Spec.Generics Associated Types type SimpleRep (a, b, c, d, e) Source # type TheSop (a, b, c, d, e) ∷ [Type] Source # Methods toSimpleRep ∷ (a, b, c, d, e) → SimpleRep (a, b, c, d, e) Source # fromSimpleRep ∷ SimpleRep (a, b, c, d, e) → (a, b, c, d, e) Source #
HasSimpleRep (a, b, c, d, e, g) Source #
Instance details Defined in Constrained.Spec.Generics Associated Types type SimpleRep (a, b, c, d, e, g) Source # type TheSop (a, b, c, d, e, g) ∷ [Type] Source # Methods toSimpleRep ∷ (a, b, c, d, e, g) → SimpleRep (a, b, c, d, e, g) Source # fromSimpleRep ∷ SimpleRep (a, b, c, d, e, g) → (a, b, c, d, e, g) Source #
HasSimpleRep (a, b, c, d, e, g, h) Source #
Instance details Defined in Constrained.Spec.Generics Associated Types type SimpleRep (a, b, c, d, e, g, h) Source # type TheSop (a, b, c, d, e, g, h) ∷ [Type] Source # Methods toSimpleRep ∷ (a, b, c, d, e, g, h) → SimpleRep (a, b, c, d, e, g, h) Source # fromSimpleRep ∷ SimpleRep (a, b, c, d, e, g, h) → (a, b, c, d, e, g, h) Source #

type family SimplifyRep f where ... Source #

Equations

SimplifyRep f = SOP (SOPOf f)

toGenericFn ∷ ∀ fn a. (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ fn '[a] (SimpleRep a) Source #

fromGenericFn ∷ ∀ fn a. (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ fn '[SimpleRep a] a Source #

data GenericsFn fn args res where Source #

Constructors

ToGeneric ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ GenericsFn fn '[a] (SimpleRep a)
FromGeneric ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ GenericsFn fn '[SimpleRep a] a

Instances

Instances details

FunctionLike (GenericsFn fn) Source #
Instance details Defined in Constrained.Spec.Generics Methods sem ∷ ∀ (as ∷ [Type]) b. GenericsFn fn as b → FunTy as b Source #
BaseUniverse fn ⇒ Functions (GenericsFn fn) fn Source #
Instance details Defined in Constrained.Spec.Generics Methods 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 #
Show (GenericsFn fn as b) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → GenericsFn fn as b → ShowS Source # show ∷ GenericsFn fn as b → String Source # showList ∷ [GenericsFn fn as b] → ShowS Source #
Eq (GenericsFn fn args res) Source #
Instance details Defined in Constrained.Base Methods (==) ∷ GenericsFn fn args res → GenericsFn fn args res → Bool Source # (/=) ∷ GenericsFn fn args res → GenericsFn fn args res → Bool Source #

fromSimpleRepSpec ∷ ∀ a fn. (HasSpec fn a, HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Specification fn (SimpleRep a) → Specification fn a Source #

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 #

data (c ∷ Symbol) ::: (ts ∷ [Type]) Source #

A constructor name with the types of its arguments

Instances

Instances details

TypeList prod ⇒ Inject c ((c ::: prod) ': (prod' ': constrs)) r Source #
Instance details Defined in Constrained.Base Methods inject' ∷ (SOP ((c ::: prod) ': (prod' ': constrs)) → r) → FunTy (ConstrOf c ((c ::: prod) ': (prod' ': constrs))) r Source #
TypeList prod ⇒ Inject c '[c ::: prod] r Source #
Instance details Defined in Constrained.Base Methods inject' ∷ (SOP '[c ::: prod] → r) → FunTy (ConstrOf 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 #
Instance details Defined in Constrained.Base Methods inject' ∷ (SOP ((c' ::: prod) ': (con ': constrs)) → r) → FunTy (ConstrOf c ((c' ::: prod) ': (con ': constrs))) r Source #
(TypeList prod, SOPLike (con ': cases) r) ⇒ SOPLike ((c ::: prod) ': (con ': cases)) r Source #
Instance details Defined in Constrained.Base Methods algebra ∷ SOP ((c ::: prod) ': (con ': cases)) → ALG ((c ::: prod) ': (con ': cases)) r Source # consts ∷ r → ALG ((c ::: prod) ': (con ': cases)) r Source #
TypeList prod ⇒ SOPLike '[c ::: prod] r Source #
Instance details Defined in Constrained.Base Methods algebra ∷ SOP '[c ::: prod] → ALG '[c ::: prod] r Source # consts ∷ r → ALG '[c ::: prod] r Source #
SopList (x' ': xs) (y ': ys) ⇒ SopList ((c ::: x) ': (x' ': xs)) (y ': ys) Source #
Instance details Defined in Constrained.Base Methods 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 #
Instance details Defined in Constrained.Base Methods injectSOPLeft ∷ SOP '[c ::: x] → SOP (Append '[c ::: x] (y ': ys)) Source # injectSOPRight ∷ SOP (y ': ys) → SOP (Append '[c ::: x] (y ': ys)) Source # caseSOP ∷ SOP (Append '[c ::: x] (y ': ys)) → Sum (SOP '[c ::: x]) (SOP (y ': ys)) Source #

type family SOPOf f where ... Source #

Turn a Rep into a list that flattens the sum structre and gives the constructors names: Maybe Int -> '[Nothing ::: '[()], Just ::: '[Int]] Either Int Bool -> '[Left ::: '[Int], Right ::: '[Bool]] data Foo = Foo Int Bool | Bar Double -> '[Foo ::: '[Int, Bool], Bar ::: '[Double]]

Equations

SOPOf (D1 _ f) = SOPOf f
SOPOf (f :+: g) = Append (SOPOf f) (SOPOf g)
SOPOf (C1 ('MetaCons constr _ _) f) = '[constr ::: Constr f]

type family Constr f where ... Source #

Flatten a single constructor

Equations

Constr (S1 _ f) = Constr f
Constr (K1 _ k) = '[k]
Constr U1 = '[()]
Constr (f :*: g) = Append (Constr f) (Constr g)

type family SOP constrs where ... Source #

Turn a list from SOPOf into a Sum over Prod representation.

Equations

SOP '[c ::: prod] = ProdOver prod
SOP ((c ::: prod) ': constrs) = Sum (ProdOver prod) (SOP constrs)

type family ConstrOf c sop where ... Source #

Equations

ConstrOf c ((c ::: constr) ': sop) = constr
ConstrOf c (_ ': sop) = ConstrOf c sop

class Inject c constrs r where Source #

Methods

inject' ∷ (SOP constrs → r) → FunTy (ConstrOf c constrs) r Source #

Instances

Instances details

TypeList prod ⇒ Inject c ((c ::: prod) ': (prod' ': constrs)) r Source #
Instance details Defined in Constrained.Base Methods inject' ∷ (SOP ((c ::: prod) ': (prod' ': constrs)) → r) → FunTy (ConstrOf c ((c ::: prod) ': (prod' ': constrs))) r Source #
TypeList prod ⇒ Inject c '[c ::: prod] r Source #
Instance details Defined in Constrained.Base Methods inject' ∷ (SOP '[c ::: prod] → r) → FunTy (ConstrOf 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 #
Instance details Defined in Constrained.Base Methods inject' ∷ (SOP ((c' ::: prod) ': (con ': constrs)) → r) → FunTy (ConstrOf c ((c' ::: prod) ': (con ': constrs))) r Source #

inject ∷ ∀ c constrs. Inject c constrs (SOP constrs) ⇒ FunTy (ConstrOf c constrs) (SOP constrs) Source #

type family ALG constrs r where ... Source #

An `ALG constrs r` is a function that takes a way to turn every constructor into an r: ``` ALG (SOPOf (Rep (Either Int Bool))) r = (Int -> r) -> (Bool -> r) -> r ```

Equations

ALG '[c ::: prod] r = FunTy prod r → r
ALG ((c ::: prod) ': constrs) r = FunTy prod r → ALG constrs r

class SOPLike constrs r where Source #

Methods

algebra ∷ SOP constrs → ALG constrs r Source #

Run a SOP

consts ∷ r → ALG constrs r Source #

Ignore everything in the SOP

Instances

Instances details

(TypeList prod, SOPLike (con ': cases) r) ⇒ SOPLike ((c ::: prod) ': (con ': cases)) r Source #
Instance details Defined in Constrained.Base Methods algebra ∷ SOP ((c ::: prod) ': (con ': cases)) → ALG ((c ::: prod) ': (con ': cases)) r Source # consts ∷ r → ALG ((c ::: prod) ': (con ': cases)) r Source #
TypeList prod ⇒ SOPLike '[c ::: prod] r Source #
Instance details Defined in Constrained.Base Methods algebra ∷ SOP '[c ::: prod] → ALG '[c ::: prod] r Source # consts ∷ r → ALG '[c ::: prod] r Source #

class SimpleConstructor rep where Source #

Methods

toSimpleCon' ∷ rep p → ProdOver (Constr rep) Source #

fromSimpleCon' ∷ ProdOver (Constr rep) → rep p Source #

Instances

Instances details

SimpleConstructor (U1 ∷ Type → Type) Source #
Instance details Defined in Constrained.Base Methods toSimpleCon' ∷ U1 p → ProdOver (Constr U1) Source # fromSimpleCon' ∷ ProdOver (Constr U1) → U1 p Source #
(SimpleConstructor f, SimpleConstructor g, TypeList (Constr f), TypeList (Constr g)) ⇒ SimpleConstructor (f :*: g) Source #
Instance details Defined in Constrained.Base Methods toSimpleCon' ∷ (f :: g) p → ProdOver (Constr (f :: g)) Source # fromSimpleCon' ∷ ProdOver (Constr (f :: g)) → (f :: g) p Source #
SimpleConstructor (K1 i k ∷ Type → Type) Source #
Instance details Defined in Constrained.Base Methods toSimpleCon' ∷ K1 i k p → ProdOver (Constr (K1 i k)) Source # fromSimpleCon' ∷ ProdOver (Constr (K1 i k)) → K1 i k p Source #
SimpleConstructor f ⇒ SimpleConstructor (S1 s f) Source #
Instance details Defined in Constrained.Base Methods toSimpleCon' ∷ S1 s f p → ProdOver (Constr (S1 s f)) Source # fromSimpleCon' ∷ ProdOver (Constr (S1 s f)) → S1 s f p Source #

class SopList xs ys where Source #

Construct and deconstruct cases in a SOP

Methods

injectSOPLeft ∷ SOP xs → SOP (Append xs ys) Source #

injectSOPRight ∷ SOP ys → SOP (Append xs ys) Source #

caseSOP ∷ SOP (Append xs ys) → Sum (SOP xs) (SOP ys) Source #

Instances

Instances details

SopList (x' ': xs) (y ': ys) ⇒ SopList ((c ::: x) ': (x' ': xs)) (y ': ys) Source #
Instance details Defined in Constrained.Base Methods 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 #
Instance details Defined in Constrained.Base Methods injectSOPLeft ∷ SOP '[c ::: x] → SOP (Append '[c ::: x] (y ': ys)) Source # injectSOPRight ∷ SOP (y ': ys) → SOP (Append '[c ::: x] (y ': ys)) Source # caseSOP ∷ SOP (Append '[c ::: x] (y ': ys)) → Sum (SOP '[c ::: x]) (SOP (y ': ys)) Source #

class SimpleGeneric rep where Source #

Methods

toSimpleRep' ∷ rep p → SimplifyRep rep Source #

fromSimpleRep' ∷ SimplifyRep rep → rep p Source #

Instances

Instances details

(SimpleGeneric f, SimpleGeneric g, SopList (SOPOf f) (SOPOf g)) ⇒ SimpleGeneric (f :+: g) Source #
Instance details Defined in Constrained.Base Methods toSimpleRep' ∷ (f :+: g) p → SimplifyRep (f :+: g) Source # fromSimpleRep' ∷ SimplifyRep (f :+: g) → (f :+: g) p Source #
SimpleConstructor f ⇒ SimpleGeneric (C1 ('MetaCons c a b) f) Source #
Instance details Defined in Constrained.Base Methods toSimpleRep' ∷ C1 ('MetaCons c a b) f p → SimplifyRep (C1 ('MetaCons c a b) f) Source # fromSimpleRep' ∷ SimplifyRep (C1 ('MetaCons c a b) f) → C1 ('MetaCons c a b) f p Source #
SimpleGeneric f ⇒ SimpleGeneric (D1 d f) Source #
Instance details Defined in Constrained.Base Methods toSimpleRep' ∷ D1 d f p → SimplifyRep (D1 d f) Source # fromSimpleRep' ∷ SimplifyRep (D1 d f) → D1 d f p Source #

class HasSpec fn a ⇒ Foldy fn a where Source #

Methods

genList ∷ (BaseUniverse fn, MonadGenError m) ⇒ Specification fn a → Specification fn a → GenT m [a] Source #

theAddFn ∷ fn '[a, a] a Source #

theZero ∷ a Source #

Instances

Instances details

BaseUniverse fn ⇒ Foldy fn Int16 Source #
Instance details Defined in Constrained.Base Methods genList ∷ ∀ (m ∷ Type → Type). (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Int16 → Specification fn Int16 → GenT m [Int16] Source # theAddFn ∷ fn '[Int16, Int16] Int16 Source # theZero ∷ Int16 Source #
BaseUniverse fn ⇒ Foldy fn Int32 Source #
Instance details Defined in Constrained.Base Methods genList ∷ ∀ (m ∷ Type → Type). (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Int32 → Specification fn Int32 → GenT m [Int32] Source # theAddFn ∷ fn '[Int32, Int32] Int32 Source # theZero ∷ Int32 Source #
BaseUniverse fn ⇒ Foldy fn Int64 Source #
Instance details Defined in Constrained.Base Methods genList ∷ ∀ (m ∷ Type → Type). (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Int64 → Specification fn Int64 → GenT m [Int64] Source # theAddFn ∷ fn '[Int64, Int64] Int64 Source # theZero ∷ Int64 Source #
BaseUniverse fn ⇒ Foldy fn Int8 Source #
Instance details Defined in Constrained.Base Methods genList ∷ ∀ (m ∷ Type → Type). (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Int8 → Specification fn Int8 → GenT m [Int8] Source # theAddFn ∷ fn '[Int8, Int8] Int8 Source # theZero ∷ Int8 Source #
BaseUniverse fn ⇒ Foldy fn Word16 Source #
Instance details Defined in Constrained.Base Methods genList ∷ ∀ (m ∷ Type → Type). (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Word16 → Specification fn Word16 → GenT m [Word16] Source # theAddFn ∷ fn '[Word16, Word16] Word16 Source # theZero ∷ Word16 Source #
BaseUniverse fn ⇒ Foldy fn Word32 Source #
Instance details Defined in Constrained.Base Methods genList ∷ ∀ (m ∷ Type → Type). (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Word32 → Specification fn Word32 → GenT m [Word32] Source # theAddFn ∷ fn '[Word32, Word32] Word32 Source # theZero ∷ Word32 Source #
BaseUniverse fn ⇒ Foldy fn Word64 Source #
Instance details Defined in Constrained.Base Methods genList ∷ ∀ (m ∷ Type → Type). (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Word64 → Specification fn Word64 → GenT m [Word64] Source # theAddFn ∷ fn '[Word64, Word64] Word64 Source # theZero ∷ Word64 Source #
BaseUniverse fn ⇒ Foldy fn Word8 Source #
Instance details Defined in Constrained.Base Methods genList ∷ ∀ (m ∷ Type → Type). (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Word8 → Specification fn Word8 → GenT m [Word8] Source # theAddFn ∷ fn '[Word8, Word8] Word8 Source # theZero ∷ Word8 Source #
BaseUniverse fn ⇒ Foldy fn Integer Source #
Instance details Defined in Constrained.Base Methods genList ∷ ∀ (m ∷ Type → Type). (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Integer → Specification fn Integer → GenT m [Integer] Source # theAddFn ∷ fn '[Integer, Integer] Integer Source # theZero ∷ Integer Source #
BaseUniverse fn ⇒ Foldy fn Natural Source #
Instance details Defined in Constrained.Base Methods genList ∷ ∀ (m ∷ Type → Type). (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Natural → Specification fn Natural → GenT m [Natural] Source # theAddFn ∷ fn '[Natural, Natural] Natural Source # theZero ∷ Natural Source #
BaseUniverse fn ⇒ Foldy fn Int Source #
Instance details Defined in Constrained.Base Methods genList ∷ ∀ (m ∷ Type → Type). (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Int → Specification fn Int → GenT m [Int] Source # theAddFn ∷ fn '[Int, Int] Int Source # theZero ∷ Int Source #

adds ∷ ∀ fn a. Foldy fn a ⇒ [a] → a Source #

data FoldSpec (fn ∷ [Type] → Type → Type) a where Source #

Constructors

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

Instances details

HasSpec fn a ⇒ Pretty (WithPrec (FoldSpec fn a)) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ WithPrec (FoldSpec fn a) → Doc ann Source # prettyList ∷ [WithPrec (FoldSpec fn a)] → Doc ann Source #
Arbitrary (FoldSpec fn (Map k v)) Source #
Instance details Defined in Constrained.Spec.Map Methods arbitrary ∷ Gen (FoldSpec fn (Map k v)) Source # shrink ∷ FoldSpec fn (Map k v) → [FoldSpec fn (Map k v)] Source #
Arbitrary (FoldSpec fn (Set a)) Source #
Instance details Defined in Constrained.Base Methods arbitrary ∷ Gen (FoldSpec fn (Set a)) Source # shrink ∷ FoldSpec fn (Set a) → [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 #
Instance details Defined in Constrained.Spec.Generics Methods arbitrary ∷ Gen (FoldSpec fn (a, b)) Source # shrink ∷ FoldSpec fn (a, b) → [FoldSpec fn (a, b)] Source #
(Arbitrary a, Arbitrary (TypeSpec fn a), Foldy fn a, BaseUniverse fn) ⇒ Arbitrary (FoldSpec fn a) Source #
Instance details Defined in Constrained.Base Methods arbitrary ∷ Gen (FoldSpec fn a) Source # shrink ∷ FoldSpec fn a → [FoldSpec fn a] Source #
HasSpec fn a ⇒ Show (FoldSpec fn a) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → FoldSpec fn a → ShowS Source # show ∷ FoldSpec fn a → String Source # showList ∷ [FoldSpec fn a] → ShowS Source #
HasSpec fn a ⇒ Pretty (FoldSpec fn a) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ FoldSpec fn a → Doc ann Source # prettyList ∷ [FoldSpec fn a] → Doc ann Source #

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

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

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

toPredsFoldSpec ∷ ∀ fn a. BaseUniverse fn ⇒ Term fn [a] → FoldSpec fn a → Pred fn Source #

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

Note: potentially infinite list

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

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

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

narrowByFuelAndSize Source #

Arguments

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

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

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

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

guardSumSpec ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b, KnownNat (CountCases b)) ⇒ [String] → SumSpec fn a b → Specification fn (Sum a b) Source #

data SumSpec fn a b Source #

Constructors

SumSpecRaw (Maybe String) (Maybe (Int, Int)) (Specification fn a) (Specification fn b)

Instances

Instances details

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

pattern SumSpec ∷ Maybe (Int, Int) → Specification fn a → Specification fn b → SumSpec fn a b Source #

combTypeName ∷ Maybe String → Maybe String → Maybe String Source #

type family CountCases a where ... Source #

Equations

CountCases (Sum a b) = 1 + CountCases b
CountCases _ = 1

countCases ∷ ∀ a. KnownNat (CountCases a) ⇒ Int Source #

sumType ∷ Maybe String → String Source #

sumWeightL ∷ Maybe (Int, Int) → Doc a Source #

sumWeightR ∷ Maybe (Int, Int) → Doc a Source #

data SetSpec fn a Source #

Constructors

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

Instances

Instances details

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

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

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

data ListSpec fn a Source #

Constructors

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

Instances

Instances details

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

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

class MaybeBounded a where Source #

Minimal complete definition

Nothing

Methods

lowerBound ∷ Maybe a Source #

default lowerBound ∷ Bounded a ⇒ Maybe a Source #

upperBound ∷ Maybe a Source #

default upperBound ∷ Bounded a ⇒ Maybe a Source #

Instances

Instances details

MaybeBounded Int16 Source #
Instance details Defined in Constrained.Base Methods lowerBound ∷ Maybe Int16 Source # upperBound ∷ Maybe Int16 Source #
MaybeBounded Int32 Source #
Instance details Defined in Constrained.Base Methods lowerBound ∷ Maybe Int32 Source # upperBound ∷ Maybe Int32 Source #
MaybeBounded Int64 Source #
Instance details Defined in Constrained.Base Methods lowerBound ∷ Maybe Int64 Source # upperBound ∷ Maybe Int64 Source #
MaybeBounded Int8 Source #
Instance details Defined in Constrained.Base Methods lowerBound ∷ Maybe Int8 Source # upperBound ∷ Maybe Int8 Source #
MaybeBounded Word16 Source #
Instance details Defined in Constrained.Base Methods lowerBound ∷ Maybe Word16 Source # upperBound ∷ Maybe Word16 Source #
MaybeBounded Word32 Source #
Instance details Defined in Constrained.Base Methods lowerBound ∷ Maybe Word32 Source # upperBound ∷ Maybe Word32 Source #
MaybeBounded Word64 Source #
Instance details Defined in Constrained.Base Methods lowerBound ∷ Maybe Word64 Source # upperBound ∷ Maybe Word64 Source #
MaybeBounded Word8 Source #
Instance details Defined in Constrained.Base Methods lowerBound ∷ Maybe Word8 Source # upperBound ∷ Maybe Word8 Source #
MaybeBounded Integer Source #
Instance details Defined in Constrained.Base Methods lowerBound ∷ Maybe Integer Source # upperBound ∷ Maybe Integer Source #
MaybeBounded Natural Source #
Instance details Defined in Constrained.Base Methods lowerBound ∷ Maybe Natural Source # upperBound ∷ Maybe Natural Source #
MaybeBounded Float Source #
Instance details Defined in Constrained.Base Methods lowerBound ∷ Maybe Float Source # upperBound ∷ Maybe Float Source #
MaybeBounded Int Source #
Instance details Defined in Constrained.Base Methods lowerBound ∷ Maybe Int Source # upperBound ∷ Maybe Int Source #
MaybeBounded (Ratio Integer) Source #
Instance details Defined in Constrained.Base Methods lowerBound ∷ Maybe (Ratio Integer) Source # upperBound ∷ Maybe (Ratio Integer) Source #

data NumSpec (fn ∷ [Type] → Type → Type) n Source #

Constructors

NumSpecInterval (Maybe n) (Maybe n)

Instances

Instances details

(Arbitrary a, Ord a) ⇒ Arbitrary (NumSpec fn a) Source #
Instance details Defined in Constrained.Base Methods arbitrary ∷ Gen (NumSpec fn a) Source # shrink ∷ NumSpec fn a → [NumSpec fn a] Source #
Ord n ⇒ Monoid (NumSpec fn n) Source #
Instance details Defined in Constrained.Base Methods mempty ∷ NumSpec fn n Source # mappend ∷ NumSpec fn n → NumSpec fn n → NumSpec fn n Source # mconcat ∷ [NumSpec fn n] → NumSpec fn n Source #
Ord n ⇒ Semigroup (NumSpec fn n) Source #
Instance details Defined in Constrained.Base Methods (<>) ∷ NumSpec fn n → NumSpec fn n → NumSpec fn n Source # sconcat ∷ NonEmpty (NumSpec fn n) → NumSpec fn n Source # stimes ∷ Integral b ⇒ b → NumSpec fn n → NumSpec fn n Source #
Num (NumSpec fn Integer) Source #
Instance details Defined in Constrained.Base Methods (+) ∷ 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 # signum ∷ NumSpec fn Integer → NumSpec fn Integer Source # fromInteger ∷ Integer → NumSpec fn Integer Source #
Show n ⇒ Show (NumSpec fn n) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → NumSpec fn n → ShowS Source # show ∷ NumSpec fn n → String Source # showList ∷ [NumSpec fn n] → ShowS Source #
Ord n ⇒ Eq (NumSpec fn n) Source #
Instance details Defined in Constrained.Base Methods (==) ∷ NumSpec fn n → NumSpec fn n → Bool Source # (/=) ∷ NumSpec fn n → NumSpec fn n → Bool Source #

emptyNumSpec ∷ Ord a ⇒ NumSpec fn a Source #

guardNumSpec ∷ (Ord n, HasSpec fn n, TypeSpec fn n ~ NumSpec fn n) ⇒ [String] → NumSpec fn n → Specification fn n 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 #

constrainInterval ∷ (MonadGenError m, Ord a, Num a, Show a) ⇒ Maybe a → Maybe a → Integer → m (a, a) Source #

conformsToNumSpec ∷ Ord n ⇒ n → NumSpec fn n → Bool Source #

toPredsNumSpec ∷ (Ord n, OrdLike fn n) ⇒ Term fn n → NumSpec fn n → Pred fn Source #

type BaseFns = '[EqFn, SetFn, BoolFn, PairFn, IntFn, OrdFn, GenericsFn, ListFn, SumFn, MapFn, FunFn, SizeFn] Source #

type BaseFn = Fix (OneofL BaseFns) Source #

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.

idFn ∷ ∀ fn a. Member (FunFn fn) fn ⇒ fn '[a] a Source #

composeFn ∷ (Member (FunFn fn) fn, HasSpec fn b, Show (fn '[a] b), Show (fn '[b] c), Eq (fn '[a] b), Eq (fn '[b] c)) ⇒ fn '[b] c → fn '[a] b → fn '[a] c 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 #

data FunFn fn args res where Source #

Constructors

Id ∷ FunFn fn '[a] a
Compose ∷ (Typeable b, HasSpec fn b, Show (fn '[a] b), Show (fn '[b] c), Eq (fn '[a] b), Eq (fn '[b] c)) ⇒ fn '[b] c → fn '[a] b → FunFn fn '[a] c
Flip ∷ (Show (fn '[a, b] c), Eq (fn '[a, b] c), HasSpec fn a, HasSpec fn b) ⇒ fn '[a, b] c → FunFn fn '[b, a] c

Instances

Instances details

FunctionLike fn ⇒ FunctionLike (FunFn fn) Source #
Instance details Defined in Constrained.Base Methods sem ∷ ∀ (as ∷ [Type]) b. FunFn fn as b → FunTy as b Source #
(BaseUniverse fn, Member (FunFn fn) fn) ⇒ Functions (FunFn fn) fn Source #
Instance details Defined in Constrained.Base Methods 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 #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → FunFn fn args res → ShowS Source # show ∷ FunFn fn args res → String Source # showList ∷ [FunFn fn args res] → ShowS Source #
Typeable fn ⇒ Eq (FunFn fn args res) Source #
Instance details Defined in Constrained.Base Methods (==) ∷ FunFn fn args res → FunFn fn args res → Bool Source # (/=) ∷ FunFn fn args res → FunFn fn args res → Bool Source #

lessOrEqualFn ∷ ∀ fn a. (Ord a, OrdLike fn a) ⇒ fn '[a, a] Bool Source #

lessFn ∷ ∀ fn a. (Ord a, OrdLike fn a) ⇒ fn '[a, a] Bool Source #

data OrdFn (fn ∷ [Type] → Type → Type) as b where Source #

Constructors

LessOrEqual ∷ (Ord a, OrdLike fn a) ⇒ OrdFn fn '[a, a] Bool
Less ∷ (Ord a, OrdLike fn a) ⇒ OrdFn fn '[a, a] Bool

Instances

Instances details

FunctionLike (OrdFn fn) Source #
Instance details Defined in Constrained.Base Methods sem ∷ ∀ (as ∷ [Type]) b. OrdFn fn as b → FunTy as b Source #
BaseUniverse fn ⇒ Functions (OrdFn fn) fn Source #
Instance details Defined in Constrained.Base Methods 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 #
Show (OrdFn fn as b) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → OrdFn fn as b → ShowS Source # show ∷ OrdFn fn as b → String Source # showList ∷ [OrdFn fn as b] → ShowS Source #
Eq (OrdFn fn as b) Source #
Instance details Defined in Constrained.Base Methods (==) ∷ OrdFn fn as b → OrdFn fn as b → Bool Source # (/=) ∷ OrdFn fn as b → OrdFn fn as b → Bool Source #

class HasSpec fn a ⇒ OrdLike fn a where Source #

Minimal complete definition

Nothing

Methods

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

Instances details

(HasSpec fn a, MaybeBounded a, Num a, TypeSpec fn a ~ NumSpec fn a) ⇒ OrdLike fn a Source #
Instance details Defined in Constrained.Base Methods leqSpec ∷ a → Specification fn a Source # ltSpec ∷ a → Specification fn a Source # geqSpec ∷ a → Specification fn a Source # gtSpec ∷ a → Specification fn a Source #

data ListFn fn args res where Source #

Constructors

FoldMap ∷ (HasSpec fn a, Foldy fn b, Show (fn '[a] b), Eq (fn '[a] b)) ⇒ fn '[a] b → ListFn fn '[[a]] b
SingletonList ∷ ListFn fn '[a] [a]
AppendFn ∷ (Typeable a, Show a) ⇒ ListFn fn '[[a], [a]] [a]

Instances

Instances details

FunctionLike fn ⇒ FunctionLike (ListFn fn) Source #
Instance details Defined in Constrained.Base Methods sem ∷ ∀ (as ∷ [Type]) b. ListFn fn as b → FunTy as b Source #
BaseUniverse fn ⇒ Functions (ListFn fn) fn Source #
Instance details Defined in Constrained.Base Methods 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 #
Show (ListFn fn args res) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → ListFn fn args res → ShowS Source # show ∷ ListFn fn args res → String Source # showList ∷ [ListFn fn args res] → ShowS Source #
Typeable fn ⇒ Eq (ListFn fn args res) Source #
Instance details Defined in Constrained.Base Methods (==) ∷ ListFn fn args res → ListFn fn args res → Bool Source # (/=) ∷ ListFn fn args res → ListFn fn args res → Bool Source #

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

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

appendFn ∷ ∀ fn a. (HasSpec fn a, Show a, Typeable a) ⇒ fn '[[a], [a]] [a] Source #

addFn ∷ ∀ fn a. NumLike fn a ⇒ fn '[a, a] a Source #

negateFn ∷ ∀ fn a. NumLike fn a ⇒ fn '[a] a Source #

data IntFn (fn ∷ [Type] → Type → Type) as b where Source #

Constructors

Add ∷ NumLike fn a ⇒ IntFn fn '[a, a] a
Negate ∷ NumLike fn a ⇒ IntFn fn '[a] a

Instances

Instances details

FunctionLike (IntFn fn) Source #
Instance details Defined in Constrained.Base Methods sem ∷ ∀ (as ∷ [Type]) b. IntFn fn as b → FunTy as b Source #
BaseUniverse fn ⇒ Functions (IntFn fn) fn Source #
Instance details Defined in Constrained.Base Methods 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 #
Show (IntFn fn as b) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → IntFn fn as b → ShowS Source # show ∷ IntFn fn as b → String Source # showList ∷ [IntFn fn as b] → ShowS Source #
Eq (IntFn fn as b) Source #
Instance details Defined in Constrained.Base Methods (==) ∷ IntFn fn as b → IntFn fn as b → Bool Source # (/=) ∷ IntFn fn as b → IntFn fn as b → Bool Source #

class (Num a, HasSpec fn a) ⇒ NumLike fn a where Source #

Minimal complete definition

Nothing

Methods

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

Instances details

(HasSpec fn a, Ord a, Num a, TypeSpec fn a ~ NumSpec fn a, MaybeBounded a) ⇒ NumLike fn a Source #
Instance details Defined in Constrained.Base Methods subtractSpec ∷ a → TypeSpec fn a → Specification fn a Source # negateSpec ∷ TypeSpec fn a → Specification fn a Source # safeSubtract ∷ a → a → Maybe a 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 #

not_ ∷ BaseUniverse fn ⇒ Term fn Bool → Term fn Bool Source #

(||.) ∷ BaseUniverse fn ⇒ Term fn Bool → Term fn Bool → Term fn Bool infixr 2 Source #

elem_ ∷ ∀ a fn. HasSpec fn a ⇒ Term fn a → Term fn [a] → Term fn Bool infix 4 Source #

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

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

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

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

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

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

sizeOf_ ∷ ∀ a fn. (HasSpec fn a, Sized a) ⇒ Term fn a → Term fn Integer 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

length_ ∷ ∀ a fn. HasSpec fn [a] ⇒ Term fn [a] → Term fn Integer Source #

special instance of sizeOf (for Lists) for backward compatibility

null_ ∷ (HasSpec fn a, Sized a) ⇒ Term fn a → Term fn Bool Source #

(<=.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool infix 4 Source #

(>=.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool infix 4 Source #

(<.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool infix 4 Source #

(>.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool infix 4 Source #

(==.) ∷ HasSpec fn a ⇒ Term fn a → Term fn a → Term fn Bool infix 4 Source #

(/=.) ∷ HasSpec fn a ⇒ Term fn a → Term fn a → Term fn Bool infix 4 Source #

sum_ ∷ (BaseUniverse fn, Member (FunFn fn) fn, Foldy fn a) ⇒ Term fn [a] → Term fn a 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 #

(++.) ∷ HasSpec fn a ⇒ Term fn [a] → Term fn [a] → Term fn [a] infixr 5 Source #

singletonList_ ∷ HasSpec fn a ⇒ Term fn a → Term fn [a] Source #

constrained ∷ ∀ a fn p. (IsPred p fn, HasSpec fn a) ⇒ (Term fn a → p) → Specification fn a Source #

assertExplain ∷ (BaseUniverse fn, IsPred p fn) ⇒ NonEmpty String → p → Pred fn Source #

assert ∷ (BaseUniverse fn, IsPred p fn) ⇒ p → Pred fn Source #

forAll ∷ (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) ⇒ Term fn t → (Term fn a → p) → Pred fn Source #

mkForAll ∷ (Forallable t a, HasSpec fn t, HasSpec fn a) ⇒ Term fn t → Binder fn a → Pred fn Source #

exists ∷ ∀ a p fn. (HasSpec fn a, IsPred p fn) ⇒ ((∀ b. Term fn b → b) → GE a) → (Term fn a → p) → Pred fn Source #

unsafeExists ∷ ∀ a p fn. (HasSpec fn a, IsPred p fn) ⇒ (Term fn a → p) → Pred fn Source #

letBind ∷ (HasSpec fn a, IsPred p fn) ⇒ Term fn a → (Term fn a → p) → 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 #

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.

assertReified ∷ HasSpec fn a ⇒ Term fn a → (a → Bool) → Pred fn Source #

reifies ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn b → Term fn a → (a → b) → Pred fn Source #

dependsOn ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn a → Term fn b → Pred fn Source #

lit ∷ Show a ⇒ a → Term fn a Source #

ifElse ∷ (BaseUniverse fn, IsPred p fn, IsPred q fn) ⇒ Term fn Bool → p → q → Pred fn Source #

whenTrue ∷ ∀ fn p. (BaseUniverse fn, IsPred p fn) ⇒ Term fn Bool → p → Pred fn Source #

genHint ∷ ∀ fn t. HasGenHint fn t ⇒ Hint t → Term fn t → Pred fn Source #

app ∷ (HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) ⇒ fn as b → FunTy (MapList (Term fn) as) (Term fn b) Source #

name ∷ String → Term fn a → Term fn a Source #

named ∷ String → Term fn a → Term fn a Source #

Give a Term a nameHint, if its a Var, and doesn't already have one, otherwise return the Term unchanged.

bind ∷ (HasSpec fn a, IsPred p fn) ⇒ (Term fn a → p) → Binder fn a Source #

mkCase ∷ HasSpec fn (SumOver as) ⇒ Term fn (SumOver as) → List (Weighted (Binder fn)) as → Pred fn Source #

type IsPred p fn = (PredLike p, UnivConstr p fn) Source #

class Show p ⇒ PredLike p where Source #

Associated Types

type UnivConstr p (fn ∷ [Type] → Type → Type) ∷ Constraint Source #

Methods

toPredExplain ∷ (BaseUniverse fn, UnivConstr p fn) ⇒ [String] → p → Pred fn Source #

Instances

Instances details

PredLike Bool Source #
Instance details Defined in Constrained.Base Associated Types type UnivConstr Bool fn Source # Methods toPredExplain ∷ ∀ (fn ∷ [Type] → Type → Type). (BaseUniverse fn, UnivConstr Bool fn) ⇒ [String] → Bool → Pred fn Source #
PredLike (Pred fn) Source #
Instance details Defined in Constrained.Base Associated Types type UnivConstr (Pred fn) fn Source # Methods toPredExplain ∷ ∀ (fn0 ∷ [Type] → Type → Type). (BaseUniverse fn0, UnivConstr (Pred fn) fn0) ⇒ [String] → Pred fn → Pred fn0 Source #
(UnivConstr p fn, Show p, PredLike p) ⇒ PredLike [p] Source #
Instance details Defined in Constrained.Base Associated Types type UnivConstr [p] fn Source # Methods toPredExplain ∷ ∀ (fn ∷ [Type] → Type → Type). (BaseUniverse fn, UnivConstr [p] fn) ⇒ [String] → [p] → Pred fn Source #
BaseUniverse fn ⇒ PredLike (Term fn Bool) Source #
Instance details Defined in Constrained.Base Associated Types type UnivConstr (Term fn Bool) fn Source # Methods toPredExplain ∷ ∀ (fn0 ∷ [Type] → Type → Type). (BaseUniverse fn0, UnivConstr (Term fn Bool) fn0) ⇒ [String] → Term fn Bool → Pred fn0 Source #

toPred ∷ ∀ fn p. (BaseUniverse fn, PredLike p, UnivConstr p fn) ⇒ p → Pred fn Source #

data WithPrec a Source #

Constructors

WithPrec Int a

Instances

Instances details

HasSpec fn a ⇒ Pretty (WithPrec (FoldSpec fn a)) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ WithPrec (FoldSpec fn a) → Doc ann Source # prettyList ∷ [WithPrec (FoldSpec fn a)] → Doc ann Source #
HasSpec fn a ⇒ Pretty (WithPrec (ListSpec fn a)) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ WithPrec (ListSpec fn a) → Doc ann Source # prettyList ∷ [WithPrec (ListSpec fn a)] → Doc ann Source #
HasSpec fn a ⇒ Pretty (WithPrec (Specification fn a)) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ WithPrec (Specification fn a) → Doc ann Source # prettyList ∷ [WithPrec (Specification fn a)] → Doc ann Source #
HasSpec fn a ⇒ Pretty (WithPrec (Term fn a)) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ WithPrec (Term fn a) → Doc ann Source # prettyList ∷ [WithPrec (Term fn a)] → Doc ann Source #
(HasSpec fn (k, v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) ⇒ Pretty (WithPrec (MapSpec fn k v)) Source #
Instance details Defined in Constrained.Spec.Map Methods pretty ∷ WithPrec (MapSpec fn k v) → Doc ann Source # prettyList ∷ [WithPrec (MapSpec fn k v)] → Doc ann Source #

parensIf ∷ Bool → Doc ann → Doc ann Source #

prettyPrec ∷ Pretty (WithPrec a) ⇒ Int → a → Doc ann Source #

ppList ∷ ∀ fn f as ann. All (HasSpec fn) as ⇒ (∀ a. HasSpec fn a ⇒ f a → Doc ann) → List f as → [Doc ann] Source #

ppList_ ∷ ∀ f as ann. (∀ a. f a → Doc ann) → List f as → [Doc ann] Source #

vsep' ∷ [Doc ann] → Doc ann Source #

(/>) ∷ Doc ann → Doc ann → Doc ann infixl 5 Source #

genFromSizeSpec ∷ (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Integer → GenT m Integer Source #

Because Sizes should always be >= 0, We provide this alternate generator that can be used to replace (genFromSpecT @Integer), to ensure this important property

data SizeFn (fn ∷ [Type] → Type → Type) as b where Source #

Constructors

SizeOf ∷ ∀ fn a. (Sized a, HasSpec fn a) ⇒ SizeFn fn '[a] Integer

Instances

Instances details

FunctionLike (SizeFn fn) Source #
Instance details Defined in Constrained.Base Methods sem ∷ ∀ (as ∷ [Type]) b. SizeFn fn as b → FunTy as b Source #
(BaseUniverse fn, HasSpec fn Integer) ⇒ Functions (SizeFn fn) fn Source #
Instance details Defined in Constrained.Base Methods 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 #
Show (SizeFn fn as b) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → SizeFn fn as b → ShowS Source # show ∷ SizeFn fn as b → String Source # showList ∷ [SizeFn fn as b] → ShowS Source #
Eq (SizeFn fn as b) Source #
Instance details Defined in Constrained.Base Methods (==) ∷ SizeFn fn as b → SizeFn fn as b → Bool Source # (/=) ∷ SizeFn fn as b → SizeFn fn as b → Bool Source #

sizeOfFn ∷ ∀ fn a. (HasSpec fn a, Member (SizeFn fn) fn, Sized a) ⇒ fn '[a] Integer Source #

mapTypeSpecSize ∷ ∀ fn a b f. f ~ SizeFn fn ⇒ f '[a] b → TypeSpec fn a → Specification fn b Source #

type SizeSpec fn = NumSpec fn Integer Source #

rangeSize ∷ Integer → Integer → SizeSpec fn Source #

maxSpec ∷ BaseUniverse fn ⇒ Specification fn Integer → Specification fn Integer Source #

The widest interval whose largest element is admitted by the original spec

class Sized t where Source #

Methods

sizeOf ∷ t → Integer Source #

liftSizeSpec ∷ HasSpec fn t ⇒ SizeSpec fn → [Integer] → Specification fn t Source #

liftMemberSpec ∷ HasSpec fn t ⇒ OrdSet Integer → Specification fn t Source #

sizeOfTypeSpec ∷ HasSpec fn t ⇒ TypeSpec fn t → Specification fn Integer Source #

Instances

Instances details

Ord a ⇒ Sized (Set a) Source #
Instance details Defined in Constrained.Base Methods sizeOf ∷ Set a → Integer Source # liftSizeSpec ∷ ∀ (fn ∷ [Type] → Type → Type). HasSpec fn (Set a) ⇒ SizeSpec fn → [Integer] → Specification fn (Set a) Source # liftMemberSpec ∷ ∀ (fn ∷ [Type] → Type → Type). HasSpec fn (Set a) ⇒ OrdSet Integer → Specification fn (Set a) Source # sizeOfTypeSpec ∷ ∀ (fn ∷ [Type] → Type → Type). HasSpec fn (Set a) ⇒ TypeSpec fn (Set a) → Specification fn Integer Source #
Sized [a] Source #
Instance details Defined in Constrained.Base Methods sizeOf ∷ [a] → Integer Source # liftSizeSpec ∷ ∀ (fn ∷ [Type] → Type → Type). HasSpec fn [a] ⇒ SizeSpec fn → [Integer] → Specification fn [a] Source # liftMemberSpec ∷ ∀ (fn ∷ [Type] → Type → Type). HasSpec fn [a] ⇒ OrdSet Integer → Specification fn [a] Source # sizeOfTypeSpec ∷ ∀ (fn ∷ [Type] → Type → Type). HasSpec fn [a] ⇒ TypeSpec fn [a] → Specification fn Integer Source #
Ord a ⇒ Sized (Map a b) Source #
Instance details Defined in Constrained.Spec.Map Methods sizeOf ∷ Map a b → Integer Source # liftSizeSpec ∷ ∀ (fn ∷ [Type] → Type → Type). HasSpec fn (Map a b) ⇒ SizeSpec fn → [Integer] → Specification fn (Map a b) Source # liftMemberSpec ∷ ∀ (fn ∷ [Type] → Type → Type). HasSpec fn (Map a b) ⇒ OrdSet Integer → Specification fn (Map a b) Source # sizeOfTypeSpec ∷ ∀ (fn ∷ [Type] → Type → Type). HasSpec fn (Map a b) ⇒ TypeSpec fn (Map a b) → Specification fn Integer Source #

hasSize ∷ (HasSpec fn t, Sized t) ⇒ SizeSpec fn → Specification fn t Source #

guardEmpty ∷ Maybe Integer → Maybe Integer → NumSpec fn Integer → NumSpec fn Integer Source #

addNumSpec ∷ NumSpec fn Integer → NumSpec fn Integer → NumSpec fn Integer Source #

subNumSpec ∷ NumSpec fn Integer → NumSpec fn Integer → NumSpec fn Integer Source #

multNumSpec ∷ NumSpec fn Integer → NumSpec fn Integer → NumSpec fn Integer Source #

negNumSpec ∷ NumSpec fn Integer → NumSpec fn Integer Source #

addSpecInt ∷ BaseUniverse fn ⇒ Specification fn Integer → Specification fn Integer → Specification fn Integer Source #

subSpecInt ∷ BaseUniverse fn ⇒ Specification fn Integer → Specification fn Integer → Specification fn Integer Source #

multSpecInt ∷ BaseUniverse fn ⇒ Specification fn Integer → Specification fn Integer → Specification fn Integer Source #

operateSpec ∷ (TypeSpec fn n ~ NumSpec fn n, Enum n, Ord n, HasSpec fn n) ⇒ String → (n → n → n) → (TypeSpec fn n → TypeSpec fn n → TypeSpec fn n) → Specification fn n → Specification fn n → Specification fn n Source #

let n be some numeric type, and f and ft be operations on n and (TypeSpec fn n) Then lift these operations from (TypeSpec fn n) to (Specification fn n) Normally f will be a (Num n) instance method (+,-,*) on n, and ft will be a a (Num (TypeSpec fn n)) instance method (+,-,*) on (TypeSpec fn n) But this will work for any operations f and ft with the right types

cardinality ∷ ∀ fn a. (Eq a, BaseUniverse fn, HasSpec fn a) ⇒ Specification fn a → Specification fn Integer Source #

Put some (admittedly loose bounds) on the number of solutions that genFromTypeSpec might return. For lots of types, there is no way to be very accurate. Here we lift the HasSpec methods cardinalTrueSpec and cardinalTypeSpec from (TypeSpec fn Integer) to (Specification fn Integer)

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)

lowBound ∷ Bounded n ⇒ Maybe n → n Source #

highBound ∷ Bounded n ⇒ Maybe n → n Source #

countSpec ∷ ∀ n fn. (Bounded n, Integral n) ⇒ NumSpec fn n → Integer Source #

The exact count of the number elements in a Bounded NumSpec

finiteSize ∷ ∀ n. (Integral n, Bounded n) ⇒ Integer Source #

The exact number of elements in a Bounded Integral type.

notInNumSpec ∷ ∀ fn n. (Functions fn fn, BaseUniverse fn, HasSpec fn n, TypeSpec fn n ~ NumSpec fn n, Bounded n, Integral n) ⇒ NumSpec fn n → [n] → Specification fn n Source #

This is an optimizing version of TypeSpec :: TypeSpec fn n -> [n] -> Specification fn n for Bounded NumSpecs. notInNumSpec :: Bounded n => TypeSpec fn n -> [n] -> Specification fn n We use this function to specialize the (HasSpec fn t) method typeSpecOpt for Bounded n. So given (TypeSpec interval badlist) we might want to transform it to (MemberSpec goodlist) There are 2 opportunities where this can payoff big time. 1) Suppose the total count of the elements in the interval is < length badlist we can then return (MemberSpec (filter elements (notElem badlist))) this must be smaller than (TypeSpec interval badlist) because the filtered list must be smaller than badlist 2) Suppose the type t is finite with size N. If the length of the badlist > (N/2), then the number of possible good things must be smaller than (length badlist), because (possible good + bad == N), so regardless of the count of the interval (MemberSpec (filter elements (notElem badlist))) is better. Sometimes much better. Example, let n be the finite set {0,1,2,3,4,5,6,7,8,9} and the bad list be [0,1,3,4,5,6,8,9] (TypeSpec [0..9] [0,1,3,4,5,6,8,9]) = filter {0,1,2,3,4,5,6,7,8,9} (notElem [0,1,3,4,5,6,8,9]) = [2,7] So (MemberSpec [2,7]) is better than (TypeSpec [0..9] [0,1,3,4,5,6,8,9]). This works no matter what the count of interval is. We only need the (length badlist > (N/2)).

data T x Source #

T is a sort of special version of Maybe, with two Nothings. Given:: NumSpecInterval (Maybe n) (Maybe n) -> Numspec We can't distinguish between the two Nothings in (NumSpecInterval Nothing Nothing) But using (NumSpecInterval NegInf PosInf) we can, In fact we can make a total ordering on T So an ascending Sorted [T x] would all the NegInf on the left and all the PosInf on the right, with the Ok's sorted in between. I.e. [NegInf, NegInf, Ok 3, Ok 6, Ok 12, Pos Inf]

Constructors

NegInf
Ok x
PosInf

Instances

Instances details

Show x ⇒ Show (T x) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → T x → ShowS Source # show ∷ T x → String Source # showList ∷ [T x] → ShowS Source #
Ord x ⇒ Eq (T x) Source #
Instance details Defined in Constrained.Base Methods (==) ∷ T x → T x → Bool Source # (/=) ∷ T x → T x → Bool Source #
Ord x ⇒ Ord (T x) Source #
Instance details Defined in Constrained.Base Methods compare ∷ T x → T x → Ordering Source # (<) ∷ T x → T x → Bool Source # (<=) ∷ T x → T x → Bool Source # (>) ∷ T x → T x → Bool Source # (>=) ∷ T x → T x → Bool Source # max ∷ T x → T x → T x Source # min ∷ T x → T x → T x Source #

unT ∷ T x → Maybe x Source #

Conversion between (T x) and (Maybe x)

neg ∷ Maybe x → T x Source #

Use this on the lower bound. I.e. lo from pair (lo,hi)

pos ∷ Maybe x → T x Source #

Use this on the upper bound. I.e. hi from pair (lo,hi)

multT ∷ Num x ⇒ T x → T x → T x Source #

multiply two (T x), correctly handling the infinities NegInf and PosInf

sizeOfSpec ∷ ∀ fn t. (BaseUniverse fn, Sized t, HasSpec fn t) ⇒ Specification fn t → Specification fn Integer Source #

sizeOfSpec generalizes the method sizeOfTypeSpec From (sizeOfTypeSpec :: TypeSpec fn t -> Specification fn Integer) To (sizeOfSpec :: Specification fn t -> Specification fn Integer) It is not unusual for instances (HasSpec fn t) to define sizeOfTypeSpec with calls to sizeOfSpec, Because many (TypeSpec fn t)'s contain (Specification fn s), for types s different from t

checkForNegativeSize ∷ Specification fn Integer → Specification fn Integer Source #

Turn a Size spec into an ErrorSpec if it has negative numbers.

nubOrd ∷ Ord a ⇒ [a] → [a] Source #

Strip out duplicates

nubOrdMemberSpec ∷ Ord a ⇒ String → [a] → Specification fn a Source #

Orphan instances

Arbitrary Natural Source #
Instance details Methods arbitrary ∷ Gen Natural Source # shrink ∷ Natural → [Natural] Source #
Random Natural Source #
Instance details Methods randomR ∷ RandomGen g ⇒ (Natural, Natural) → g → (Natural, g) Source # random ∷ RandomGen g ⇒ g → (Natural, g) Source # randomRs ∷ RandomGen g ⇒ (Natural, Natural) → g → [Natural] Source # randoms ∷ RandomGen g ⇒ g → [Natural] Source #
Uniform Natural Source #
Instance details Methods uniformM ∷ StatefulGen g m ⇒ g → m Natural Source #
Arbitrary a ⇒ Arbitrary (NonEmpty a) Source #
Instance details Methods arbitrary ∷ Gen (NonEmpty a) Source # shrink ∷ NonEmpty a → [NonEmpty a] Source #
Pretty (Var a) Source #
Instance details Methods pretty ∷ Var a → Doc ann Source # prettyList ∷ [Var a] → Doc ann Source #
Random (Ratio Integer) Source #
Instance details Methods randomR ∷ RandomGen g ⇒ (Ratio Integer, Ratio Integer) → g → (Ratio Integer, g) Source # random ∷ RandomGen g ⇒ g → (Ratio Integer, g) Source # randomRs ∷ RandomGen g ⇒ (Ratio Integer, Ratio Integer) → g → [Ratio Integer] Source # randoms ∷ RandomGen g ⇒ g → [Ratio Integer] Source #