| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Constrained.Base
Contents
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
- type HasSpecImpliesEq fn a f = HasSpec fn a ⇒ Eq (f a) ∷ Constraint
- data Binder fn a where
- 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 {}
- 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
- data HOLE a b where
- 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
- 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
- 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 ∷ ∀ c constrs. Inject c constrs (SOP constrs) ⇒ FunTy (ConstrOf c constrs) (SOP constrs)
- type family ALG constrs r where ...
- class SOPLike constrs r where
- class SimpleConstructor rep where
- toSimpleCon' ∷ rep p → ProdOver (Constr rep)
- fromSimpleCon' ∷ ProdOver (Constr rep) → rep p
- class SopList xs ys where
- 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
- 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
- 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
- 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
- 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
- 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 fn 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 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
- (>.) ∷ (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
- sizeOfFn ∷ ∀ fn a. (HasSpec fn a, Member (SizeFn fn) fn, Sized fn 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 fn t where
- sizeOf ∷ t → Integer
- liftSizeSpec ∷ HasSpec fn t ⇒ SizeSpec fn → [Integer] → Specification fn t
- liftMemberSpec ∷ HasSpec fn t ⇒ OrdSet Integer → Specification fn t
- sizeOfTypeSpec ∷ HasSpec fn t ⇒ TypeSpec fn t → Specification fn Integer
- hasSize ∷ (HasSpec fn t, Sized fn 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
- 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 fn 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
- runTermE ∷ Env → Term fn a → Either (NonEmpty String) a
- checkPredsE ∷ FunctionLike fn ⇒ NonEmpty String → Env → [Pred fn] → Maybe (NonEmpty String)
- checkPredE ∷ ∀ fn. FunctionLike fn ⇒ Env → NonEmpty String → Pred fn → Maybe (NonEmpty String)
- conformsToSpecE ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a → NonEmpty String → Maybe (NonEmpty String)
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
type HasSpecImpliesEq fn a f = HasSpec fn a ⇒ Eq (f a) ∷ Constraint 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 | |
| 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 | |
| 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 | |
| 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
| HasVariables fn (Pred fn) Source # | |
| BaseUniverse fn ⇒ Monoid (Pred fn) Source # | |
| BaseUniverse fn ⇒ Semigroup (Pred fn) Source # | |
| Show (Pred fn) Source # | |
| PredLike (Pred fn) Source # | |
Defined in Constrained.Base 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 # | |
| Pretty (Pred fn) Source # | |
| type UnivConstr (Pred fn) fn' Source # | |
Defined in Constrained.Base | |
falsePred1 ∷ String → Pred fn Source #
Instances
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'`.
This is used together with ListCtx to form
just the arguments to `f vs Ctx vs'` - replacing
Ctx with HOLE - to provide to propagateSpecFun.
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 #
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 #
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
| |
| 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 |
Fields
| |
| TypeSpec | A type-specific spec |
Fields
| |
| TrueSpec ∷ Specification fn a | Anything |
Instances
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 #
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 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
data WithHasSpec fn f a where Source #
Constructors
| WithHasSpec ∷ HasSpec fn a ⇒ f a → WithHasSpec fn f a |
Instances
| HasSpecImpliesEq fn a f ⇒ Eq (WithHasSpec fn f a) Source # | |
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
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.
Methods
giveHint ∷ Hint a → Specification fn a Source #
Instances
| HasSpec fn a ⇒ HasGenHint fn (BinTree a) Source # | |
| (Member (TreeFn fn) fn, HasSpec fn a) ⇒ HasGenHint fn (Tree a) Source # | |
| HasSpec fn a ⇒ HasGenHint fn [a] Source # | |
Defined in Constrained.Base 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 # | |
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 #
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 #
shrinkEnvFromPlan ∷ Env → SolverPlan fn → [Env] Source #
fixupWithSpec ∷ ∀ fn a. HasSpec fn a ⇒ Specification fn a → a → Maybe a 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 #
computeDependencies ∷ Pred fn → DependGraph fn Source #
data SolverStage fn where Source #
Constructors
| SolverStage | |
Fields
| |
Instances
| Pretty (SolverStage fn) Source # | |
Defined in Constrained.Base | |
data SolverPlan fn Source #
Constructors
| SolverPlan | |
Fields
| |
Instances
| Pretty (SolverPlan fn) Source # | |
Defined in Constrained.Base | |
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 FromG ∷ ∀ fn a. () ⇒ (HasSpec fn a, HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Term fn (SimpleRep a) → 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 #
prettyPlan ∷ HasSpec fn a ⇒ Specification fn a → Doc ann 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 #
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.
propagateSpec ∷ ∀ fn v a. HasSpec fn v ⇒ Specification fn a → Ctx fn v a → Specification fn v 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
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
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 #
Constructors
| FreeVars | |
Fields
| |
class HasVariables fn a | a → fn where Source #
Minimal complete definition
Methods
freeVars ∷ a → FreeVars fn Source #
freeVarSet ∷ a → Set (Name fn) Source #
Instances
| HasVariables f (Name f) Source # | |
| HasVariables f a ⇒ HasVariables f (Set a) Source # | |
| (Foldable t, HasVariables f a) ⇒ HasVariables f (t a) Source # | |
| HasVariables fn (Pred fn) Source # | |
| (HasVariables f a, HasVariables f b) ⇒ HasVariables f (a, b) Source # | |
| HasVariables fn (Binder fn a) Source # | |
| HasVariables fn (Term fn a) Source # | |
| HasVariables fn (f a) ⇒ HasVariables fn (Weighted f a) Source # | |
| HasVariables fn (List (Term fn) as) Source # | |
| HasVariables fn (List (Weighted (Binder fn)) as) Source # | |
Defined in Constrained.Base | |
type Subst fn = [SubstEntry fn] Source #
data SubstEntry fn where Source #
Constructors
| (:=) ∷ HasSpec fn a ⇒ Var a → Term fn a → SubstEntry fn |
simplifyTerm ∷ ∀ fn a. BaseUniverse fn ⇒ Term fn a → Term fn a 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
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
| HasSimpleRep Foo Source # | |
| HasSimpleRep Three Source # | |
| HasSimpleRep FooBarBaz Source # | |
| HasSimpleRep Bool Source # | |
| Ord a ⇒ HasSimpleRep (NotASet a) Source # | |
| HasSimpleRep (Maybe a) Source # | |
| HasSimpleRep (Either a b) Source # | |
| HasSimpleRep (a, b) Source # | |
| HasSimpleRep (a, b, c) Source # | |
| HasSimpleRep (a, b, c, d) Source # | |
| HasSimpleRep (a, b, c, d, e) Source # | |
| HasSimpleRep (a, b, c, d, e, g) Source # | |
| HasSimpleRep (a, b, c, d, e, g, h) Source # | |
Defined in Constrained.Spec.Generics 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
| FunctionLike (GenericsFn fn) Source # | |
Defined in Constrained.Spec.Generics | |
| BaseUniverse fn ⇒ Functions (GenericsFn fn) fn Source # | |
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 # | |
Defined in Constrained.Base | |
| Eq (GenericsFn fn args res) Source # | |
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
| TypeList prod ⇒ Inject c ((c ::: prod) ': (prod' ': constrs)) r Source # | |
| TypeList prod ⇒ Inject c '[c ::: prod] r Source # | |
| (FunTy (ConstrOf c ((c' ::: prod) ': (con ': constrs))) r ~ FunTy (ConstrOf c (con ': constrs)) r, Inject c (con ': constrs) r) ⇒ Inject c ((c' ::: prod) ': (con ': constrs)) r Source # | |
| (TypeList prod, SOPLike (con ': cases) r) ⇒ SOPLike ((c ::: prod) ': (con ': cases)) r Source # | |
| TypeList prod ⇒ SOPLike '[c ::: prod] r Source # | |
| SopList (x' ': xs) (y ': ys) ⇒ SopList ((c ::: x) ': (x' ': xs)) (y ': ys) Source # | |
Defined in Constrained.Base 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 # | |
class Inject c constrs r where Source #
Instances
| TypeList prod ⇒ Inject c ((c ::: prod) ': (prod' ': constrs)) r Source # | |
| TypeList prod ⇒ Inject c '[c ::: prod] r Source # | |
| (FunTy (ConstrOf c ((c' ::: prod) ': (con ': constrs))) r ~ FunTy (ConstrOf c (con ': constrs)) r, Inject c (con ': constrs) r) ⇒ Inject c ((c' ::: prod) ': (con ': constrs)) r Source # | |
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
```
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
class SimpleConstructor rep where Source #
Methods
toSimpleCon' ∷ rep p → ProdOver (Constr rep) Source #
fromSimpleCon' ∷ ProdOver (Constr rep) → rep p Source #
Instances
| SimpleConstructor (U1 ∷ Type → Type) Source # | |
Defined in Constrained.Base | |
| (SimpleConstructor f, SimpleConstructor g, TypeList (Constr f), TypeList (Constr g)) ⇒ SimpleConstructor (f :*: g) Source # | |
Defined in Constrained.Base | |
| SimpleConstructor (K1 i k ∷ Type → Type) Source # | |
Defined in Constrained.Base | |
| SimpleConstructor f ⇒ SimpleConstructor (S1 s f) Source # | |
Defined in Constrained.Base | |
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
| SopList (x' ': xs) (y ': ys) ⇒ SopList ((c ::: x) ': (x' ': xs)) (y ': ys) Source # | |
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 # | |
class SimpleGeneric rep where Source #
Methods
toSimpleRep' ∷ rep p → SimplifyRep rep Source #
fromSimpleRep' ∷ SimplifyRep rep → rep p Source #
Instances
| (SimpleGeneric f, SimpleGeneric g, SopList (SOPOf f) (SOPOf g)) ⇒ SimpleGeneric (f :+: g) Source # | |
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 # | |
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 # | |
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 #
Instances
| BaseUniverse fn ⇒ Foldy fn Int16 Source # | |
Defined in Constrained.Base | |
| BaseUniverse fn ⇒ Foldy fn Int32 Source # | |
Defined in Constrained.Base | |
| BaseUniverse fn ⇒ Foldy fn Int64 Source # | |
Defined in Constrained.Base | |
| BaseUniverse fn ⇒ Foldy fn Int8 Source # | |
Defined in Constrained.Base | |
| BaseUniverse fn ⇒ Foldy fn Word16 Source # | |
Defined in Constrained.Base | |
| BaseUniverse fn ⇒ Foldy fn Word32 Source # | |
Defined in Constrained.Base | |
| BaseUniverse fn ⇒ Foldy fn Word64 Source # | |
Defined in Constrained.Base | |
| BaseUniverse fn ⇒ Foldy fn Word8 Source # | |
Defined in Constrained.Base | |
| BaseUniverse fn ⇒ Foldy fn Integer Source # | |
Defined in Constrained.Base | |
| BaseUniverse fn ⇒ Foldy fn Natural Source # | |
Defined in Constrained.Base | |
| BaseUniverse fn ⇒ Foldy fn Int Source # | |
Defined in Constrained.Base | |
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
| HasSpec fn a ⇒ Pretty (WithPrec (FoldSpec fn a)) Source # | |
| Arbitrary (FoldSpec fn (Map k v)) Source # | |
| Arbitrary (FoldSpec fn (Set a)) Source # | |
| (HasSpec fn a, HasSpec fn b, Arbitrary (FoldSpec fn a), Arbitrary (FoldSpec fn b)) ⇒ Arbitrary (FoldSpec fn (a, b)) Source # | |
| (Arbitrary a, Arbitrary (TypeSpec fn a), Foldy fn a, BaseUniverse fn) ⇒ Arbitrary (FoldSpec fn a) Source # | |
| HasSpec fn a ⇒ Show (FoldSpec fn a) Source # | |
| HasSpec fn a ⇒ Pretty (FoldSpec fn a) Source # | |
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 #
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 #
Constructors
| SumSpecRaw (Maybe String) (Maybe (Int, Int)) (Specification fn a) (Specification fn b) |
Instances
| (Arbitrary (Specification fn a), Arbitrary (Specification fn b)) ⇒ Arbitrary (SumSpec fn a b) Source # | |
| (HasSpec fn a, HasSpec fn b, KnownNat (CountCases b)) ⇒ Monoid (SumSpec fn a b) Source # | |
| (HasSpec fn a, HasSpec fn b) ⇒ Semigroup (SumSpec fn a b) Source # | |
| (KnownNat (CountCases b), HasSpec fn a, HasSpec fn b) ⇒ Show (SumSpec fn a b) Source # | |
pattern SumSpec ∷ Maybe (Int, Int) → Specification fn a → Specification fn b → SumSpec fn a b Source #
type family CountCases a where ... Source #
Equations
| CountCases (Sum a b) = 1 + CountCases b | |
| CountCases _ = 1 |
countCases ∷ ∀ a. KnownNat (CountCases a) ⇒ Int Source #
Constructors
| SetSpec (Set a) (Specification fn a) (Specification fn Integer) |
guardSetSpec ∷ (HasSpec fn a, Ord a) ⇒ [String] → SetSpec fn a → Specification fn (Set a) Source #
Constructors
| ListSpec | |
Fields
| |
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
| MaybeBounded Int16 Source # | |
Defined in Constrained.Base | |
| MaybeBounded Int32 Source # | |
Defined in Constrained.Base | |
| MaybeBounded Int64 Source # | |
Defined in Constrained.Base | |
| MaybeBounded Int8 Source # | |
Defined in Constrained.Base | |
| MaybeBounded Word16 Source # | |
Defined in Constrained.Base | |
| MaybeBounded Word32 Source # | |
Defined in Constrained.Base | |
| MaybeBounded Word64 Source # | |
Defined in Constrained.Base | |
| MaybeBounded Word8 Source # | |
Defined in Constrained.Base | |
| MaybeBounded Integer Source # | |
Defined in Constrained.Base | |
| MaybeBounded Natural Source # | |
Defined in Constrained.Base | |
| MaybeBounded Float Source # | |
Defined in Constrained.Base | |
| MaybeBounded Int Source # | |
Defined in Constrained.Base | |
| MaybeBounded (Ratio Integer) Source # | |
Defined in Constrained.Base | |
data NumSpec (fn ∷ [Type] → Type → Type) n Source #
Constructors
| NumSpecInterval (Maybe n) (Maybe n) |
Instances
| (Arbitrary a, Ord a) ⇒ Arbitrary (NumSpec fn a) Source # | |
| Ord n ⇒ Monoid (NumSpec fn n) Source # | |
| Ord n ⇒ Semigroup (NumSpec fn n) Source # | |
| Num (NumSpec fn Integer) Source # | |
Defined in Constrained.Base 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 # | |
| Show n ⇒ Show (NumSpec fn n) Source # | |
| Ord n ⇒ Eq (NumSpec fn n) 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 #
type BaseFns = '[EqFn, SetFn, BoolFn, PairFn, IntFn, OrdFn, GenericsFn, ListFn, SumFn, MapFn, FunFn, SizeFn] 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.
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
| FunctionLike fn ⇒ FunctionLike (FunFn fn) Source # | |
| (BaseUniverse fn, Member (FunFn fn) fn) ⇒ Functions (FunFn fn) fn Source # | |
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 # | |
| Typeable fn ⇒ Eq (FunFn fn args res) 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
| FunctionLike (OrdFn fn) Source # | |
| BaseUniverse fn ⇒ Functions (OrdFn fn) fn Source # | |
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 # | |
| Eq (OrdFn fn as b) 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
| (HasSpec fn a, MaybeBounded a, Num a, TypeSpec fn a ~ NumSpec fn a) ⇒ OrdLike fn a Source # | |
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
| FunctionLike fn ⇒ FunctionLike (ListFn fn) Source # | |
| BaseUniverse fn ⇒ Functions (ListFn fn) fn Source # | |
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 # | |
| Typeable fn ⇒ Eq (ListFn fn args res) 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 #
data IntFn (fn ∷ [Type] → Type → Type) as b where Source #
Instances
| FunctionLike (IntFn fn) Source # | |
| BaseUniverse fn ⇒ Functions (IntFn fn) fn Source # | |
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 # | |
| Eq (IntFn fn as b) 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
| (HasSpec fn a, Ord a, Num a, TypeSpec fn a ~ NumSpec fn a, MaybeBounded a) ⇒ NumLike fn a Source # | |
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 #
subset_ ∷ (HasSpec fn (Set a), Ord a, Show a, Typeable a) ⇒ Term fn (Set a) → Term fn (Set a) → Term fn Bool Source #
union_ ∷ ∀ a fn. (HasSpec fn a, Ord a) ⇒ Term fn (Set a) → Term fn (Set a) → Term fn (Set a) Source #
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
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 #
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 #
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 #
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.
app ∷ (HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) ⇒ fn as b → FunTy (MapList (Term fn) as) (Term fn b) 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.
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
toPred ∷ ∀ fn p. (BaseUniverse fn, PredLike p, UnivConstr p fn) ⇒ p → Pred fn Source #
Instances
| HasSpec fn a ⇒ Pretty (WithPrec (FoldSpec fn a)) Source # | |
| HasSpec fn a ⇒ Pretty (WithPrec (ListSpec fn a)) Source # | |
| HasSpec fn a ⇒ Pretty (WithPrec (Specification fn a)) Source # | |
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 # | |
| (HasSpec fn (k, v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) ⇒ Pretty (WithPrec (MapSpec fn k v)) Source # | |
ppList ∷ ∀ fn f as ann. All (HasSpec fn) as ⇒ (∀ a. HasSpec fn a ⇒ f a → Doc ann) → List f as → [Doc ann] 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 #
Instances
| FunctionLike (SizeFn fn) Source # | |
| (BaseUniverse fn, HasSpec fn Integer) ⇒ Functions (SizeFn fn) fn Source # | |
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 # | |
| Eq (SizeFn fn as b) Source # | |
mapTypeSpecSize ∷ ∀ fn a b f. f ~ SizeFn fn ⇒ f '[a] b → TypeSpec fn a → Specification fn b 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 fn t where Source #
Minimal complete definition
Nothing
Methods
liftSizeSpec ∷ HasSpec fn t ⇒ SizeSpec fn → [Integer] → Specification fn t Source #
default liftSizeSpec ∷ (HasSpec fn t, HasSimpleRep t, Sized fn (SimpleRep t), HasSpec fn (SimpleRep t), TypeSpec fn t ~ TypeSpec fn (SimpleRep t)) ⇒ SizeSpec fn → [Integer] → Specification fn t Source #
liftMemberSpec ∷ HasSpec fn t ⇒ OrdSet Integer → Specification fn t Source #
default liftMemberSpec ∷ (HasSpec fn t, HasSpec fn (SimpleRep t), HasSimpleRep t, Sized fn (SimpleRep t), TypeSpec fn t ~ TypeSpec fn (SimpleRep t)) ⇒ OrdSet Integer → Specification fn t Source #
sizeOfTypeSpec ∷ HasSpec fn t ⇒ TypeSpec fn t → Specification fn Integer Source #
default sizeOfTypeSpec ∷ (HasSpec fn t, HasSpec fn (SimpleRep t), HasSimpleRep t, Sized fn (SimpleRep t), TypeSpec fn t ~ TypeSpec fn (SimpleRep t)) ⇒ TypeSpec fn t → Specification fn Integer Source #
Instances
| Ord a ⇒ Sized fn (Set a) Source # | |
Defined in Constrained.Base Methods sizeOf ∷ Set a → Integer Source # liftSizeSpec ∷ SizeSpec fn → [Integer] → Specification fn (Set a) Source # liftMemberSpec ∷ OrdSet Integer → Specification fn (Set a) Source # sizeOfTypeSpec ∷ TypeSpec fn (Set a) → Specification fn Integer Source # | |
| Sized fn [a] Source # | |
Defined in Constrained.Base Methods sizeOf ∷ [a] → Integer Source # liftSizeSpec ∷ SizeSpec fn → [Integer] → Specification fn [a] Source # liftMemberSpec ∷ OrdSet Integer → Specification fn [a] Source # sizeOfTypeSpec ∷ TypeSpec fn [a] → Specification fn Integer Source # | |
| Ord a ⇒ Sized fn (Map a b) Source # | |
Defined in Constrained.Spec.Map Methods sizeOf ∷ Map a b → Integer Source # liftSizeSpec ∷ SizeSpec fn → [Integer] → Specification fn (Map a b) Source # liftMemberSpec ∷ OrdSet Integer → Specification fn (Map a b) Source # sizeOfTypeSpec ∷ TypeSpec fn (Map a b) → Specification fn Integer Source # | |
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)
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)).
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]
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 fn 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.
nubOrdMemberSpec ∷ Ord a ⇒ String → [a] → Specification fn a Source #
checkPredsE ∷ FunctionLike fn ⇒ NonEmpty String → Env → [Pred fn] → Maybe (NonEmpty String) Source #
checkPredE ∷ ∀ fn. FunctionLike fn ⇒ Env → NonEmpty String → Pred fn → Maybe (NonEmpty String) Source #
conformsToSpecE ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a → NonEmpty String → Maybe (NonEmpty String) Source #