constrained-generators-0.2.0.0: Framework for generating constrained random data using a subset of first order logic
Safe HaskellSafe-Inferred
LanguageHaskell2010

Constrained.TheKnot

Description

All the things that are mutually recursive.

Synopsis

Documentation

data SumSpec a b Source #

The Specification for Sums.

Constructors

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

Instances

Instances details
(Arbitrary (Specification a), Arbitrary (Specification b)) ⇒ Arbitrary (SumSpec a b) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

arbitraryGen (SumSpec a b) Source #

shrinkSumSpec a b → [SumSpec a b] Source #

(HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Monoid (SumSpec a b) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

memptySumSpec a b

mappendSumSpec a b → SumSpec a b → SumSpec a b

mconcat ∷ [SumSpec a b] → SumSpec a b

(HasSpec a, HasSpec b) ⇒ Semigroup (SumSpec a b) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

(<>)SumSpec a b → SumSpec a b → SumSpec a b #

sconcatNonEmpty (SumSpec a b) → SumSpec a b

stimes ∷ Integral b0 ⇒ b0 → SumSpec a b → SumSpec a b

(KnownNat (CountCases b), HasSpec a, HasSpec b) ⇒ Show (SumSpec a b) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

showsPrec ∷ Int → SumSpec a b → ShowS

showSumSpec a b → String

showList ∷ [SumSpec a b] → ShowS

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

guardSumSpec ∷ ∀ a b. (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ [String] → SumSpec a b → Specification (Sum 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 #

totalWeightList (Weighted f) as → Maybe Int Source #

sumType ∷ Maybe String → String Source #

data SumW dom rng where Source #

Constructors

InjLeftW ∷ (HasSpec a, HasSpec b) ⇒ SumW '[a] (Sum a b) 
InjRightW ∷ (HasSpec a, HasSpec b) ⇒ SumW '[b] (Sum a b) 

Instances

Instances details
Logic SumW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SumW as b, HasSpec a) ⇒ SumW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source #

propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SumW as b, HasSpec a) ⇒ SumW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source #

propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires SumW as b, HasSpec a) ⇒ SumW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source #

rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ SumW dom rng → List Term dom → Evidence (AppRequires SumW dom rng) → Maybe (Term rng) Source #

mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ SumW '[a] b → TypeSpec a → Specification b Source #

saturate ∷ ∀ (dom ∷ [Type]). SumW dom Bool → List Term dom → [Pred] Source #

Semantics SumW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

semantics ∷ ∀ (d ∷ [Type]) r. SumW d r → FunTy d r Source #

Syntax SumW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

inFix ∷ ∀ (dom ∷ [Type]) rng. SumW dom rng → Bool Source #

prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ SumW dom rng → List Term dom → Int → Maybe (Doc ann) Source #

Show (SumW dom rng) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

showsPrec ∷ Int → SumW dom rng → ShowS

showSumW dom rng → String

showList ∷ [SumW dom rng] → ShowS

Eq (SumW dom rng) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

(==)SumW dom rng → SumW dom rng → Bool

(/=)SumW dom rng → SumW dom rng → Bool

injLeft_ ∷ (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Term a → Term (Sum a b) Source #

injRight_ ∷ (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Term b → Term (Sum a b) Source #

pattern InjRight ∷ ∀ c. () ⇒ ∀ a b. (c ~ Sum a b, AppRequires SumW '[b] c) ⇒ Term b → Term c Source #

pattern InjLeft ∷ ∀ c. () ⇒ ∀ a b. (c ~ Sum a b, AppRequires SumW '[a] c) ⇒ Term a → Term c Source #

caseBoolSpecHasSpec a ⇒ Specification Bool → (Bool → Specification a) → Specification a Source #

data BoolW (dom ∷ [Type]) (rng ∷ Type) where Source #

Operations on Bool

Constructors

NotWBoolW '[Bool] Bool 
OrWBoolW '[Bool, Bool] Bool 

Instances

Instances details
Logic BoolW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires BoolW as b, HasSpec a) ⇒ BoolW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source #

propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires BoolW as b, HasSpec a) ⇒ BoolW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source #

propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires BoolW as b, HasSpec a) ⇒ BoolW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source #

rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ BoolW dom rng → List Term dom → Evidence (AppRequires BoolW dom rng) → Maybe (Term rng) Source #

mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ BoolW '[a] b → TypeSpec a → Specification b Source #

saturate ∷ ∀ (dom ∷ [Type]). BoolW dom Bool → List Term dom → [Pred] Source #

Semantics BoolW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

semantics ∷ ∀ (d ∷ [Type]) r. BoolW d r → FunTy d r Source #

Syntax BoolW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

inFix ∷ ∀ (dom ∷ [Type]) rng. BoolW dom rng → Bool Source #

prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ BoolW dom rng → List Term dom → Int → Maybe (Doc ann) Source #

Show (BoolW dom rng) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

showsPrec ∷ Int → BoolW dom rng → ShowS

showBoolW dom rng → String

showList ∷ [BoolW dom rng] → ShowS

Eq (BoolW dom rng) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

(==)BoolW dom rng → BoolW dom rng → Bool

(/=)BoolW dom rng → BoolW dom rng → Bool

boolSemBoolW dom rng → FunTy dom rng Source #

not_Term Bool → Term Bool Source #

okOr ∷ Bool → Bool → Specification Bool Source #

We have something like (constant ||. HOLE) must evaluate to need. Return a (Specification Bool) for HOLE, that makes that True.

or_Term Bool → Term Bool → Term Bool Source #

data EqW ∷ [Type] → Type → Type where Source #

Constructors

EqualW ∷ (Eq a, HasSpec a) ⇒ EqW '[a, a] Bool 

Instances

Instances details
Logic EqW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires EqW as b, HasSpec a) ⇒ EqW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source #

propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires EqW as b, HasSpec a) ⇒ EqW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source #

propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires EqW as b, HasSpec a) ⇒ EqW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source #

rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ EqW dom rng → List Term dom → Evidence (AppRequires EqW dom rng) → Maybe (Term rng) Source #

mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ EqW '[a] b → TypeSpec a → Specification b Source #

saturate ∷ ∀ (dom ∷ [Type]). EqW dom Bool → List Term dom → [Pred] Source #

Semantics EqW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

semantics ∷ ∀ (d ∷ [Type]) r. EqW d r → FunTy d r Source #

Syntax EqW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

inFix ∷ ∀ (dom ∷ [Type]) rng. EqW dom rng → Bool Source #

prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ EqW dom rng → List Term dom → Int → Maybe (Doc ann) Source #

Show (EqW d r) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

showsPrec ∷ Int → EqW d r → ShowS

showEqW d r → String

showList ∷ [EqW d r] → ShowS

Eq (EqW dom rng) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

(==)EqW dom rng → EqW dom rng → Bool

(/=)EqW dom rng → EqW dom rng → Bool

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

pattern Equal ∷ ∀ b. () ⇒ ∀ a. (b ~ Bool, Eq a, HasSpec a) ⇒ Term a → Term a → Term b Source #

(<=.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool infixr 4 Source #

(<.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool infixr 4 Source #

(>=.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool infixr 4 Source #

(>.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool infixr 4 Source #

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

If the `Specification Bool` doesn't constrain the boolean you will get a TrueSpec out.

whenTrue ∷ ∀ p. IsPred p ⇒ Term Bool → p → Pred Source #

pinnedBy ∷ ∀ a. HasSpec a ⇒ Var a → Pred → Maybe (Term 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!

substituteAndSimplifyTermSubstTerm a → Term a Source #

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

simplifyTerm ∷ ∀ a. Term a → Term a Source #

Simplify a Term, if the Term is an App, apply the rewrite rules chosen by the (Logic sym t bs a) instance attached to the function witness f

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

Precondition: the Pred defines the `Var a` Runs in GE in order for us to have detailed context on failure.

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

Precondition: the `Pred fn` defines the `Var a`. Runs in GE in order for us to have detailed context on failure.

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

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

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

Turn a list of branches into a SumSpec. If all the branches fail return an ErrorSpec. Note the requirement of HasSpec(SumOver).

genFromSpecT ∷ ∀ a m. (HasCallStack, HasSpec a, MonadGenError m) ⇒ Specification a → GenT m a Source #

Generate a value that satisfies the spec. This function can fail if the spec is inconsistent, there is a dependency error, or if the underlying generators are not flexible enough.

genFromSpec ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Specification a → Gen a Source #

A version of genFromSpecT that simply errors if the generator fails

genFromSpecWithSeed ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Int → Int → Specification a → a Source #

A version of genFromSpecT that takes a seed and a size and gives you a result

debugSpec ∷ ∀ a. HasSpec a ⇒ Specification a → IO () Source #

A version of genFromSpecT that runs in the IO monad. Good for debugging.

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

solvableFromName → Set NameDependGraph → Bool Source #

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

shrinkFromPredsHasSpec a ⇒ PredVar a → a → [a] Source #

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

prepareLinearizationPredGE SolverPlan 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.

flattenPredPred → [Pred] Source #

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

mergeSolverStageSolverStage → [SolverStage] → [SolverStage] Source #

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

printPlanHasSpec a ⇒ Specification a → IO () Source #

genFromPreds ∷ ∀ m. MonadGenError m ⇒ EnvPredGenT m Env Source #

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

backPropagationSolverPlanSolverPlan Source #

Push as much information we can backwards through the plan.

mapSpec ∷ ∀ t a b. AppRequires t '[a] b ⇒ t '[a] b → Specification a → Specification b Source #

Functor like property for Specification, but instead of a Haskell function (a -> b), it takes a function symbol (t '[a] b) from a to b. Note, in this context, a function symbol is some constructor of a witnesstype. Eg. ProdFstW, InjRightW, SingletonW, etc. NOT the lifted versions like fst_ singleton_, which construct Terms. We had to wait until here to define this because it depends on Semigroup property of Specification, and Asserting equality

pairView ∷ ∀ a b. (HasSpec a, HasSpec b) ⇒ Term (Prod a b) → Maybe (Term a, Term b) Source #

cartesian ∷ ∀ a b. (HasSpec a, HasSpec b) ⇒ Specification a → Specification b → Specification (Prod a b) Source #

data PairSpec a b Source #

Constructors

Cartesian (Specification a) (Specification b) 

Instances

Instances details
(Arbitrary (Specification a), Arbitrary (Specification b)) ⇒ Arbitrary (PairSpec a b) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

arbitraryGen (PairSpec a b) Source #

shrinkPairSpec a b → [PairSpec a b] Source #

(HasSpec a, HasSpec b) ⇒ Show (PairSpec a b) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

showsPrec ∷ Int → PairSpec a b → ShowS

showPairSpec a b → String

showList ∷ [PairSpec a b] → ShowS

data ProdW ∷ [Type] → Type → Type where Source #

Constructors

ProdW ∷ (HasSpec a, HasSpec b) ⇒ ProdW '[a, b] (Prod a b) 
ProdFstW ∷ (HasSpec a, HasSpec b) ⇒ ProdW '[Prod a b] a 
ProdSndW ∷ (HasSpec a, HasSpec b) ⇒ ProdW '[Prod a b] b 

Instances

Instances details
Logic ProdW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires ProdW as b, HasSpec a) ⇒ ProdW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source #

propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires ProdW as b, HasSpec a) ⇒ ProdW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source #

propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires ProdW as b, HasSpec a) ⇒ ProdW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source #

rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ ProdW dom rng → List Term dom → Evidence (AppRequires ProdW dom rng) → Maybe (Term rng) Source #

mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ ProdW '[a] b → TypeSpec a → Specification b Source #

saturate ∷ ∀ (dom ∷ [Type]). ProdW dom Bool → List Term dom → [Pred] Source #

Semantics ProdW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

semantics ∷ ∀ (d ∷ [Type]) r. ProdW d r → FunTy d r Source #

Syntax ProdW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

inFix ∷ ∀ (dom ∷ [Type]) rng. ProdW dom rng → Bool Source #

prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ ProdW dom rng → List Term dom → Int → Maybe (Doc ann) Source #

Show (ProdW as b) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

showsPrec ∷ Int → ProdW as b → ShowS

showProdW as b → String

showList ∷ [ProdW as b] → ShowS

Eq (ProdW as b) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

(==)ProdW as b → ProdW as b → Bool

(/=)ProdW as b → ProdW as b → Bool

prodFst_ ∷ (HasSpec a, HasSpec b) ⇒ Term (Prod a b) → Term a Source #

prodSnd_ ∷ (HasSpec a, HasSpec b) ⇒ Term (Prod a b) → Term b Source #

sameFst ∷ Eq a1 ⇒ a1 → [Prod a1 a2] → [a2] Source #

sameSnd ∷ Eq a1 ⇒ a1 → [Prod a2 a1] → [a2] Source #

prod_ ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Term (Prod a b) Source #

pattern Product ∷ ∀ c. () ⇒ ∀ a b. (c ~ Prod a b, AppRequires ProdW '[a, b] (Prod a b)) ⇒ Term a → Term b → Term c Source #

data ElemW ∷ [Type] → Type → Type where Source #

Constructors

ElemWHasSpec a ⇒ ElemW '[a, [a]] Bool 

Instances

Instances details
Logic ElemW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires ElemW as b, HasSpec a) ⇒ ElemW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source #

propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires ElemW as b, HasSpec a) ⇒ ElemW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source #

propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires ElemW as b, HasSpec a) ⇒ ElemW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source #

rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ ElemW dom rng → List Term dom → Evidence (AppRequires ElemW dom rng) → Maybe (Term rng) Source #

mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ ElemW '[a] b → TypeSpec a → Specification b Source #

saturate ∷ ∀ (dom ∷ [Type]). ElemW dom Bool → List Term dom → [Pred] Source #

Semantics ElemW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

semantics ∷ ∀ (d ∷ [Type]) r. ElemW d r → FunTy d r Source #

Syntax ElemW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

inFix ∷ ∀ (dom ∷ [Type]) rng. ElemW dom rng → Bool Source #

prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ ElemW dom rng → List Term dom → Int → Maybe (Doc ann) Source #

Show (ElemW dom rng) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

showsPrec ∷ Int → ElemW dom rng → ShowS

showElemW dom rng → String

showList ∷ [ElemW dom rng] → ShowS

Eq (ElemW dom rng) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

(==)ElemW dom rng → ElemW dom rng → Bool

(/=)ElemW dom rng → ElemW dom rng → Bool

elem_ ∷ (Sized [a], HasSpec a) ⇒ Term a → Term [a] → Term Bool infix 4 Source #

elemFnHasSpec a ⇒ Fun '[a, [a]] Bool Source #

pattern Elem ∷ ∀ b. () ⇒ ∀ a. (b ~ Bool, Eq a, HasSpec a) ⇒ Term a → Term [a] → Term b Source #

data ListSpec a Source #

Constructors

ListSpec 

Fields

Instances

Instances details
(Arbitrary a, Arbitrary (FoldSpec a), Arbitrary (TypeSpec a), HasSpec a) ⇒ Arbitrary (ListSpec a) Source # 
Instance details

Defined in Constrained.TheKnot

HasSpec a ⇒ Show (ListSpec a) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

showsPrec ∷ Int → ListSpec a → ShowS

showListSpec a → String

showList ∷ [ListSpec a] → ShowS

HasSpec a ⇒ Pretty (WithPrec (ListSpec a)) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

prettyWithPrec (ListSpec a) → Doc ann Source #

prettyList ∷ [WithPrec (ListSpec a)] → Doc ann Source #

HasSpec a ⇒ Pretty (ListSpec a) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

prettyListSpec a → Doc ann Source #

prettyList ∷ [ListSpec a] → Doc ann Source #

guardListSpecHasSpec a ⇒ [String] → ListSpec a → Specification [a] Source #

sizeOf_ ∷ (HasSpec a, Sized a) ⇒ Term a → Term Integer Source #

genFromSizeSpecMonadGenError m ⇒ Specification Integer → GenT m Integer Source #

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

data ListW (args ∷ [Type]) (res ∷ Type) where Source #

Constructors

FoldMapW ∷ ∀ a b. (Foldy b, HasSpec a) ⇒ Fun '[a] b → ListW '[[a]] b 
SingletonListWHasSpec a ⇒ ListW '[a] [a] 
AppendW ∷ (HasSpec a, Typeable a, Show a) ⇒ ListW '[[a], [a]] [a] 

Instances

Instances details
Logic ListW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires ListW as b, HasSpec a) ⇒ ListW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source #

propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires ListW as b, HasSpec a) ⇒ ListW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source #

propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires ListW as b, HasSpec a) ⇒ ListW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source #

rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ ListW dom rng → List Term dom → Evidence (AppRequires ListW dom rng) → Maybe (Term rng) Source #

mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ ListW '[a] b → TypeSpec a → Specification b Source #

saturate ∷ ∀ (dom ∷ [Type]). ListW dom Bool → List Term dom → [Pred] Source #

Semantics ListW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

semantics ∷ ∀ (d ∷ [Type]) r. ListW d r → FunTy d r Source #

Syntax ListW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

inFix ∷ ∀ (dom ∷ [Type]) rng. ListW dom rng → Bool Source #

prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ ListW dom rng → List Term dom → Int → Maybe (Doc ann) Source #

Show (ListW d r) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

showsPrec ∷ Int → ListW d r → ShowS

showListW d r → String

showList ∷ [ListW d r] → ShowS

Eq (ListW d r) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

(==)ListW d r → ListW d r → Bool

(/=)ListW d r → ListW d r → Bool

listSemListW dom rng → FunTy dom rng Source #

foldMap_ ∷ ∀ a b. (Foldy b, HasSpec a) ⇒ (Term a → Term b) → Term [a] → Term b Source #

sum_Foldy a ⇒ Term [a] → Term a Source #

singletonList_ ∷ (Sized [a], HasSpec a) ⇒ Term a → Term [a] Source #

append_ ∷ (Sized [a], HasSpec a) ⇒ Term [a] → Term [a] → Term [a] Source #

appendFn ∷ ∀ a. (Sized [a], HasSpec a) ⇒ Fun '[[a], [a]] [a] Source #

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

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

prefixedBy ∷ Eq a ⇒ [a] → [[a]] → [[a]] Source #

suffixedBy ∷ Eq a ⇒ [a] → [[a]] → [[a]] Source #

alreadyHave ∷ Eq a ⇒ [a] → ListSpec a → ListSpec a Source #

toPredsFoldSpecHasSpec a ⇒ Term [a] → FoldSpec a → Pred Source #

Used in the HasSpec [a] instance

data FoldSpec a where Source #

Constructors

NoFoldFoldSpec a 
FoldSpec ∷ ∀ b a. (HasSpec a, HasSpec b, Foldy b) ⇒ Fun '[a] b → Specification b → FoldSpec a 

Instances

Instances details
Arbitrary (FoldSpec (Map k v)) Source # 
Instance details

Defined in Constrained.Spec.Map

Methods

arbitraryGen (FoldSpec (Map k v)) Source #

shrinkFoldSpec (Map k v) → [FoldSpec (Map k v)] Source #

Arbitrary (FoldSpec (Set a)) Source # 
Instance details

Defined in Constrained.Spec.Set

Methods

arbitraryGen (FoldSpec (Set a)) Source #

shrinkFoldSpec (Set a) → [FoldSpec (Set a)] Source #

(HasSpec a, HasSpec b, Arbitrary (FoldSpec a), Arbitrary (FoldSpec b)) ⇒ Arbitrary (FoldSpec (a, b)) Source # 
Instance details

Defined in Constrained.Spec.SumProd

Methods

arbitraryGen (FoldSpec (a, b)) Source #

shrinkFoldSpec (a, b) → [FoldSpec (a, b)] Source #

(Arbitrary (Specification a), Foldy a) ⇒ Arbitrary (FoldSpec a) Source # 
Instance details

Defined in Constrained.TheKnot

HasSpec a ⇒ Show (FoldSpec a) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

showsPrec ∷ Int → FoldSpec a → ShowS

showFoldSpec a → String

showList ∷ [FoldSpec a] → ShowS

HasSpec a ⇒ Pretty (WithPrec (FoldSpec a)) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

prettyWithPrec (FoldSpec a) → Doc ann Source #

prettyList ∷ [WithPrec (FoldSpec a)] → Doc ann Source #

HasSpec a ⇒ Pretty (FoldSpec a) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

prettyFoldSpec a → Doc ann Source #

prettyList ∷ [FoldSpec a] → Doc ann Source #

preMapFoldSpecHasSpec a ⇒ Fun '[a] b → FoldSpec b → FoldSpec a Source #

composeFn ∷ (HasSpec b, HasSpec c) ⇒ Fun '[b] c → Fun '[a] b → Fun '[a] c Source #

idFnHasSpec a ⇒ Fun '[a] a Source #

combineFoldSpecFoldSpec a → FoldSpec a → Either [String] (FoldSpec a) Source #

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

class (HasSpec a, NumLike a, Logic IntW) ⇒ Foldy a where Source #

Minimal complete definition

genList, genSizedList, noNegativeValues

Instances

Instances details
Foldy Int16 Source # 
Instance details

Defined in Constrained.TheKnot

Methods

genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Int16 → Specification Int16 → GenT m [Int16] Source #

theAddFnIntW '[Int16, Int16] Int16 Source #

theZero ∷ Int16 Source #

genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Int16 → Specification Int16 → GenT m [Int16] Source #

noNegativeValues ∷ Bool Source #

Foldy Int32 Source # 
Instance details

Defined in Constrained.TheKnot

Methods

genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Int32 → Specification Int32 → GenT m [Int32] Source #

theAddFnIntW '[Int32, Int32] Int32 Source #

theZero ∷ Int32 Source #

genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Int32 → Specification Int32 → GenT m [Int32] Source #

noNegativeValues ∷ Bool Source #

Foldy Int64 Source # 
Instance details

Defined in Constrained.TheKnot

Methods

genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Int64 → Specification Int64 → GenT m [Int64] Source #

theAddFnIntW '[Int64, Int64] Int64 Source #

theZero ∷ Int64 Source #

genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Int64 → Specification Int64 → GenT m [Int64] Source #

noNegativeValues ∷ Bool Source #

Foldy Int8 Source # 
Instance details

Defined in Constrained.TheKnot

Methods

genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Int8 → Specification Int8 → GenT m [Int8] Source #

theAddFnIntW '[Int8, Int8] Int8 Source #

theZero ∷ Int8 Source #

genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Int8 → Specification Int8 → GenT m [Int8] Source #

noNegativeValues ∷ Bool Source #

Foldy Word16 Source # 
Instance details

Defined in Constrained.TheKnot

Methods

genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Word16 → Specification Word16 → GenT m [Word16] Source #

theAddFnIntW '[Word16, Word16] Word16 Source #

theZero ∷ Word16 Source #

genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Word16 → Specification Word16 → GenT m [Word16] Source #

noNegativeValues ∷ Bool Source #

Foldy Word32 Source # 
Instance details

Defined in Constrained.TheKnot

Methods

genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Word32 → Specification Word32 → GenT m [Word32] Source #

theAddFnIntW '[Word32, Word32] Word32 Source #

theZero ∷ Word32 Source #

genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Word32 → Specification Word32 → GenT m [Word32] Source #

noNegativeValues ∷ Bool Source #

Foldy Word64 Source # 
Instance details

Defined in Constrained.TheKnot

Methods

genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Word64 → Specification Word64 → GenT m [Word64] Source #

theAddFnIntW '[Word64, Word64] Word64 Source #

theZero ∷ Word64 Source #

genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Word64 → Specification Word64 → GenT m [Word64] Source #

noNegativeValues ∷ Bool Source #

Foldy Word8 Source # 
Instance details

Defined in Constrained.TheKnot

Methods

genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Word8 → Specification Word8 → GenT m [Word8] Source #

theAddFnIntW '[Word8, Word8] Word8 Source #

theZero ∷ Word8 Source #

genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Word8 → Specification Word8 → GenT m [Word8] Source #

noNegativeValues ∷ Bool Source #

Foldy Integer Source # 
Instance details

Defined in Constrained.TheKnot

Methods

genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Integer → GenT m [Integer] Source #

theAddFnIntW '[Integer, Integer] Integer Source #

theZero ∷ Integer Source #

genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Integer → Specification Integer → GenT m [Integer] Source #

noNegativeValues ∷ Bool Source #

Foldy Natural Source # 
Instance details

Defined in Constrained.TheKnot

Methods

genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Natural → Specification Natural → GenT m [Natural] Source #

theAddFnIntW '[Natural, Natural] Natural Source #

theZero ∷ Natural Source #

genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Natural → Specification Natural → GenT m [Natural] Source #

noNegativeValues ∷ Bool Source #

Foldy Int Source # 
Instance details

Defined in Constrained.TheKnot

Methods

genList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Int → Specification Int → GenT m [Int] Source #

theAddFnIntW '[Int, Int] Int Source #

theZero ∷ Int Source #

genSizedList ∷ ∀ (m ∷ Type → Type). MonadGenError m ⇒ Specification Integer → Specification Int → Specification Int → GenT m [Int] Source #

noNegativeValues ∷ Bool Source #

type SizeSpec = NumSpec Integer Source #

class Sized t where Source #

Minimal complete definition

Nothing

Methods

sizeOf ∷ t → Integer Source #

default sizeOf ∷ (HasSimpleRep t, Sized (SimpleRep t)) ⇒ t → Integer Source #

liftSizeSpecHasSpec t ⇒ SizeSpec → [Integer] → Specification t Source #

liftMemberSpecHasSpec t ⇒ [Integer] → Specification t Source #

sizeOfTypeSpecHasSpec t ⇒ TypeSpec t → Specification Integer Source #

Instances

Instances details
Ord a ⇒ Sized (Set a) Source # 
Instance details

Defined in Constrained.Spec.Set

Methods

sizeOf ∷ Set a → Integer Source #

liftSizeSpecSizeSpec → [Integer] → Specification (Set a) Source #

liftMemberSpec ∷ [Integer] → Specification (Set a) Source #

sizeOfTypeSpecTypeSpec (Set a) → Specification Integer Source #

Sized [a] Source # 
Instance details

Defined in Constrained.TheKnot

Methods

sizeOf ∷ [a] → Integer Source #

liftSizeSpecSizeSpec → [Integer] → Specification [a] Source #

liftMemberSpec ∷ [Integer] → Specification [a] Source #

sizeOfTypeSpecTypeSpec [a] → Specification Integer Source #

Ord a ⇒ Sized (Map a b) Source # 
Instance details

Defined in Constrained.Spec.Map

Methods

sizeOf ∷ Map a b → Integer Source #

liftSizeSpecSizeSpec → [Integer] → Specification (Map a b) Source #

liftMemberSpec ∷ [Integer] → Specification (Map a b) Source #

sizeOfTypeSpecTypeSpec (Map a b) → Specification Integer Source #

addsFoldy a ⇒ [a] → a Source #

data FunW (dom ∷ [Type]) (rng ∷ Type) where Source #

Constructors

IdW ∷ ∀ a. FunW '[a] a 
ComposeW ∷ ∀ b t1 t2 a r. (AppRequires t1 '[b] r, AppRequires t2 '[a] b, HasSpec b) ⇒ t1 '[b] r → t2 '[a] b → FunW '[a] r 
FlipW ∷ ∀ t a b r. AppRequires t '[a, b] r ⇒ t '[a, b] r → FunW '[b, a] r 

Instances

Instances details
Logic FunW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires FunW as b, HasSpec a) ⇒ FunW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source #

propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires FunW as b, HasSpec a) ⇒ FunW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source #

propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires FunW as b, HasSpec a) ⇒ FunW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source #

rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ FunW dom rng → List Term dom → Evidence (AppRequires FunW dom rng) → Maybe (Term rng) Source #

mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ FunW '[a] b → TypeSpec a → Specification b Source #

saturate ∷ ∀ (dom ∷ [Type]). FunW dom Bool → List Term dom → [Pred] Source #

Semantics FunW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

semantics ∷ ∀ (d ∷ [Type]) r. FunW d r → FunTy d r Source #

Syntax FunW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

inFix ∷ ∀ (dom ∷ [Type]) rng. FunW dom rng → Bool Source #

prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ FunW dom rng → List Term dom → Int → Maybe (Doc ann) Source #

Show (FunW dom rng) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

showsPrec ∷ Int → FunW dom rng → ShowS

showFunW dom rng → String

showList ∷ [FunW dom rng] → ShowS

Eq (FunW dom rng) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

(==)FunW dom rng → FunW dom rng → Bool

(/=)FunW dom rng → FunW dom rng → Bool

funSemFunW dom rng → FunTy dom rng Source #

compareWit ∷ ∀ t1 bs1 r1 t2 bs2 r2. (AppRequires t1 bs1 r1, AppRequires t2 bs2 r2) ⇒ t1 bs1 r1 → t2 bs2 r2 → Bool Source #

id_ ∷ ∀ a. HasSpec a ⇒ Term a → Term a Source #

flip_ ∷ ∀ (t ∷ [Type] → Type → Type) a b r. (HasSpec b, HasSpec a, AppRequires t '[a, b] r) ⇒ t '[a, b] r → Term b → Term a → Term r Source #

compose_ ∷ ∀ b t1 t2 a r. (AppRequires t1 '[b] r, AppRequires t2 '[a] b) ⇒ t1 '[b] r → t2 '[a] b → Term a → Term r Source #

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

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

addFunNumLike n ⇒ Fun '[n, n] n Source #

data SizeW (dom ∷ [Type]) rng ∷ Type where Source #

Constructors

SizeOfW ∷ (Sized n, HasSpec n) ⇒ SizeW '[n] Integer 

Instances

Instances details
Logic SizeW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SizeW as b, HasSpec a) ⇒ SizeW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source #

propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SizeW as b, HasSpec a) ⇒ SizeW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source #

propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires SizeW as b, HasSpec a) ⇒ SizeW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source #

rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ SizeW dom rng → List Term dom → Evidence (AppRequires SizeW dom rng) → Maybe (Term rng) Source #

mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ SizeW '[a] b → TypeSpec a → Specification b Source #

saturate ∷ ∀ (dom ∷ [Type]). SizeW dom Bool → List Term dom → [Pred] Source #

Semantics SizeW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

semantics ∷ ∀ (d ∷ [Type]) r. SizeW d r → FunTy d r Source #

Syntax SizeW Source # 
Instance details

Defined in Constrained.TheKnot

Methods

inFix ∷ ∀ (dom ∷ [Type]) rng. SizeW dom rng → Bool Source #

prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ SizeW dom rng → List Term dom → Int → Maybe (Doc ann) Source #

Show (SizeW d r) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

showsPrec ∷ Int → SizeW d r → ShowS

showSizeW d r → String

showList ∷ [SizeW d r] → ShowS

Eq (SizeW ds r) Source # 
Instance details

Defined in Constrained.TheKnot

Methods

(==)SizeW ds r → SizeW ds r → Bool

(/=)SizeW ds r → SizeW ds r → Bool

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

rangeSize ∷ Integer → Integer → SizeSpec Source #

between ∷ (HasSpec a, TypeSpec a ~ NumSpec a) ⇒ a → a → Specification a Source #

maxSpecSpecification Integer → Specification Integer Source #

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

(+.)NumLike a ⇒ Term a → Term a → Term a infix 4 Source #

negate_NumLike a ⇒ Term a → Term a Source #

(-.)Numeric n ⇒ Term n → Term n → Term n infix 4 Source #

Orphan instances

HasSpec Int16 Source # 
Instance details

Associated Types

type TypeSpec Int16 Source #

type Prerequisites Int16 Source #

Methods

emptySpecTypeSpec Int16 Source #

combineSpecTypeSpec Int16 → TypeSpec Int16 → Specification Int16 Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Int16 → GenT m Int16 Source #

conformsTo ∷ Int16 → TypeSpec Int16 → Bool Source #

shrinkWithTypeSpecTypeSpec Int16 → Int16 → [Int16] Source #

toPredsTerm Int16 → TypeSpec Int16 → Pred Source #

cardinalTypeSpecTypeSpec Int16 → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec Int16 → Maybe (NonEmpty String) Source #

alternateShowTypeSpec Int16 → BinaryShow Source #

monadConformsTo ∷ Int16 → TypeSpec Int16 → Writer [String] Bool Source #

typeSpecOptTypeSpec Int16 → [Int16] → Specification Int16 Source #

guardTypeSpec ∷ [String] → TypeSpec Int16 → Specification Int16 Source #

prerequisitesEvidence (Prerequisites Int16) Source #

HasSpec Int32 Source # 
Instance details

Associated Types

type TypeSpec Int32 Source #

type Prerequisites Int32 Source #

Methods

emptySpecTypeSpec Int32 Source #

combineSpecTypeSpec Int32 → TypeSpec Int32 → Specification Int32 Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Int32 → GenT m Int32 Source #

conformsTo ∷ Int32 → TypeSpec Int32 → Bool Source #

shrinkWithTypeSpecTypeSpec Int32 → Int32 → [Int32] Source #

toPredsTerm Int32 → TypeSpec Int32 → Pred Source #

cardinalTypeSpecTypeSpec Int32 → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec Int32 → Maybe (NonEmpty String) Source #

alternateShowTypeSpec Int32 → BinaryShow Source #

monadConformsTo ∷ Int32 → TypeSpec Int32 → Writer [String] Bool Source #

typeSpecOptTypeSpec Int32 → [Int32] → Specification Int32 Source #

guardTypeSpec ∷ [String] → TypeSpec Int32 → Specification Int32 Source #

prerequisitesEvidence (Prerequisites Int32) Source #

HasSpec Int64 Source # 
Instance details

Associated Types

type TypeSpec Int64 Source #

type Prerequisites Int64 Source #

Methods

emptySpecTypeSpec Int64 Source #

combineSpecTypeSpec Int64 → TypeSpec Int64 → Specification Int64 Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Int64 → GenT m Int64 Source #

conformsTo ∷ Int64 → TypeSpec Int64 → Bool Source #

shrinkWithTypeSpecTypeSpec Int64 → Int64 → [Int64] Source #

toPredsTerm Int64 → TypeSpec Int64 → Pred Source #

cardinalTypeSpecTypeSpec Int64 → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec Int64 → Maybe (NonEmpty String) Source #

alternateShowTypeSpec Int64 → BinaryShow Source #

monadConformsTo ∷ Int64 → TypeSpec Int64 → Writer [String] Bool Source #

typeSpecOptTypeSpec Int64 → [Int64] → Specification Int64 Source #

guardTypeSpec ∷ [String] → TypeSpec Int64 → Specification Int64 Source #

prerequisitesEvidence (Prerequisites Int64) Source #

HasSpec Int8 Source # 
Instance details

Associated Types

type TypeSpec Int8 Source #

type Prerequisites Int8 Source #

Methods

emptySpecTypeSpec Int8 Source #

combineSpecTypeSpec Int8 → TypeSpec Int8 → Specification Int8 Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Int8 → GenT m Int8 Source #

conformsTo ∷ Int8 → TypeSpec Int8 → Bool Source #

shrinkWithTypeSpecTypeSpec Int8 → Int8 → [Int8] Source #

toPredsTerm Int8 → TypeSpec Int8 → Pred Source #

cardinalTypeSpecTypeSpec Int8 → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec Int8 → Maybe (NonEmpty String) Source #

alternateShowTypeSpec Int8 → BinaryShow Source #

monadConformsTo ∷ Int8 → TypeSpec Int8 → Writer [String] Bool Source #

typeSpecOptTypeSpec Int8 → [Int8] → Specification Int8 Source #

guardTypeSpec ∷ [String] → TypeSpec Int8 → Specification Int8 Source #

prerequisitesEvidence (Prerequisites Int8) Source #

HasSpec Word16 Source # 
Instance details

Associated Types

type TypeSpec Word16 Source #

type Prerequisites Word16 Source #

Methods

emptySpecTypeSpec Word16 Source #

combineSpecTypeSpec Word16 → TypeSpec Word16 → Specification Word16 Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Word16 → GenT m Word16 Source #

conformsTo ∷ Word16 → TypeSpec Word16 → Bool Source #

shrinkWithTypeSpecTypeSpec Word16 → Word16 → [Word16] Source #

toPredsTerm Word16 → TypeSpec Word16 → Pred Source #

cardinalTypeSpecTypeSpec Word16 → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec Word16 → Maybe (NonEmpty String) Source #

alternateShowTypeSpec Word16 → BinaryShow Source #

monadConformsTo ∷ Word16 → TypeSpec Word16 → Writer [String] Bool Source #

typeSpecOptTypeSpec Word16 → [Word16] → Specification Word16 Source #

guardTypeSpec ∷ [String] → TypeSpec Word16 → Specification Word16 Source #

prerequisitesEvidence (Prerequisites Word16) Source #

HasSpec Word32 Source # 
Instance details

Associated Types

type TypeSpec Word32 Source #

type Prerequisites Word32 Source #

Methods

emptySpecTypeSpec Word32 Source #

combineSpecTypeSpec Word32 → TypeSpec Word32 → Specification Word32 Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Word32 → GenT m Word32 Source #

conformsTo ∷ Word32 → TypeSpec Word32 → Bool Source #

shrinkWithTypeSpecTypeSpec Word32 → Word32 → [Word32] Source #

toPredsTerm Word32 → TypeSpec Word32 → Pred Source #

cardinalTypeSpecTypeSpec Word32 → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec Word32 → Maybe (NonEmpty String) Source #

alternateShowTypeSpec Word32 → BinaryShow Source #

monadConformsTo ∷ Word32 → TypeSpec Word32 → Writer [String] Bool Source #

typeSpecOptTypeSpec Word32 → [Word32] → Specification Word32 Source #

guardTypeSpec ∷ [String] → TypeSpec Word32 → Specification Word32 Source #

prerequisitesEvidence (Prerequisites Word32) Source #

HasSpec Word64 Source # 
Instance details

Associated Types

type TypeSpec Word64 Source #

type Prerequisites Word64 Source #

Methods

emptySpecTypeSpec Word64 Source #

combineSpecTypeSpec Word64 → TypeSpec Word64 → Specification Word64 Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Word64 → GenT m Word64 Source #

conformsTo ∷ Word64 → TypeSpec Word64 → Bool Source #

shrinkWithTypeSpecTypeSpec Word64 → Word64 → [Word64] Source #

toPredsTerm Word64 → TypeSpec Word64 → Pred Source #

cardinalTypeSpecTypeSpec Word64 → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec Word64 → Maybe (NonEmpty String) Source #

alternateShowTypeSpec Word64 → BinaryShow Source #

monadConformsTo ∷ Word64 → TypeSpec Word64 → Writer [String] Bool Source #

typeSpecOptTypeSpec Word64 → [Word64] → Specification Word64 Source #

guardTypeSpec ∷ [String] → TypeSpec Word64 → Specification Word64 Source #

prerequisitesEvidence (Prerequisites Word64) Source #

HasSpec Word8 Source # 
Instance details

Associated Types

type TypeSpec Word8 Source #

type Prerequisites Word8 Source #

Methods

emptySpecTypeSpec Word8 Source #

combineSpecTypeSpec Word8 → TypeSpec Word8 → Specification Word8 Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Word8 → GenT m Word8 Source #

conformsTo ∷ Word8 → TypeSpec Word8 → Bool Source #

shrinkWithTypeSpecTypeSpec Word8 → Word8 → [Word8] Source #

toPredsTerm Word8 → TypeSpec Word8 → Pred Source #

cardinalTypeSpecTypeSpec Word8 → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec Word8 → Maybe (NonEmpty String) Source #

alternateShowTypeSpec Word8 → BinaryShow Source #

monadConformsTo ∷ Word8 → TypeSpec Word8 → Writer [String] Bool Source #

typeSpecOptTypeSpec Word8 → [Word8] → Specification Word8 Source #

guardTypeSpec ∷ [String] → TypeSpec Word8 → Specification Word8 Source #

prerequisitesEvidence (Prerequisites Word8) Source #

HasSpec Integer Source # 
Instance details

Associated Types

type TypeSpec Integer Source #

type Prerequisites Integer Source #

Methods

emptySpecTypeSpec Integer Source #

combineSpecTypeSpec Integer → TypeSpec Integer → Specification Integer Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Integer → GenT m Integer Source #

conformsTo ∷ Integer → TypeSpec Integer → Bool Source #

shrinkWithTypeSpecTypeSpec Integer → Integer → [Integer] Source #

toPredsTerm Integer → TypeSpec Integer → Pred Source #

cardinalTypeSpecTypeSpec Integer → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec Integer → Maybe (NonEmpty String) Source #

alternateShowTypeSpec Integer → BinaryShow Source #

monadConformsTo ∷ Integer → TypeSpec Integer → Writer [String] Bool Source #

typeSpecOptTypeSpec Integer → [Integer] → Specification Integer Source #

guardTypeSpec ∷ [String] → TypeSpec Integer → Specification Integer Source #

prerequisitesEvidence (Prerequisites Integer) Source #

HasSpec Natural Source # 
Instance details

Associated Types

type TypeSpec Natural Source #

type Prerequisites Natural Source #

Methods

emptySpecTypeSpec Natural Source #

combineSpecTypeSpec Natural → TypeSpec Natural → Specification Natural Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Natural → GenT m Natural Source #

conformsTo ∷ Natural → TypeSpec Natural → Bool Source #

shrinkWithTypeSpecTypeSpec Natural → Natural → [Natural] Source #

toPredsTerm Natural → TypeSpec Natural → Pred Source #

cardinalTypeSpecTypeSpec Natural → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec Natural → Maybe (NonEmpty String) Source #

alternateShowTypeSpec Natural → BinaryShow Source #

monadConformsTo ∷ Natural → TypeSpec Natural → Writer [String] Bool Source #

typeSpecOptTypeSpec Natural → [Natural] → Specification Natural Source #

guardTypeSpec ∷ [String] → TypeSpec Natural → Specification Natural Source #

prerequisitesEvidence (Prerequisites Natural) Source #

HasSpec Bool Source # 
Instance details

Associated Types

type TypeSpec Bool Source #

type Prerequisites Bool Source #

Methods

emptySpecTypeSpec Bool Source #

combineSpecTypeSpec Bool → TypeSpec Bool → Specification Bool Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Bool → GenT m Bool Source #

conformsTo ∷ Bool → TypeSpec Bool → Bool Source #

shrinkWithTypeSpecTypeSpec Bool → Bool → [Bool] Source #

toPredsTerm Bool → TypeSpec Bool → Pred Source #

cardinalTypeSpecTypeSpec Bool → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec Bool → Maybe (NonEmpty String) Source #

alternateShowTypeSpec Bool → BinaryShow Source #

monadConformsTo ∷ Bool → TypeSpec Bool → Writer [String] Bool Source #

typeSpecOptTypeSpec Bool → [Bool] → Specification Bool Source #

guardTypeSpec ∷ [String] → TypeSpec Bool → Specification Bool Source #

prerequisitesEvidence (Prerequisites Bool) Source #

HasSpec Float Source # 
Instance details

Associated Types

type TypeSpec Float Source #

type Prerequisites Float Source #

Methods

emptySpecTypeSpec Float Source #

combineSpecTypeSpec Float → TypeSpec Float → Specification Float Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Float → GenT m Float Source #

conformsTo ∷ Float → TypeSpec Float → Bool Source #

shrinkWithTypeSpecTypeSpec Float → Float → [Float] Source #

toPredsTerm Float → TypeSpec Float → Pred Source #

cardinalTypeSpecTypeSpec Float → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec Float → Maybe (NonEmpty String) Source #

alternateShowTypeSpec Float → BinaryShow Source #

monadConformsTo ∷ Float → TypeSpec Float → Writer [String] Bool Source #

typeSpecOptTypeSpec Float → [Float] → Specification Float Source #

guardTypeSpec ∷ [String] → TypeSpec Float → Specification Float Source #

prerequisitesEvidence (Prerequisites Float) Source #

HasSpec Int Source # 
Instance details

Associated Types

type TypeSpec Int Source #

type Prerequisites Int Source #

Methods

emptySpecTypeSpec Int Source #

combineSpecTypeSpec Int → TypeSpec Int → Specification Int Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Int → GenT m Int Source #

conformsTo ∷ Int → TypeSpec Int → Bool Source #

shrinkWithTypeSpecTypeSpec Int → Int → [Int] Source #

toPredsTerm Int → TypeSpec Int → Pred Source #

cardinalTypeSpecTypeSpec Int → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec Int → Maybe (NonEmpty String) Source #

alternateShowTypeSpec Int → BinaryShow Source #

monadConformsTo ∷ Int → TypeSpec Int → Writer [String] Bool Source #

typeSpecOptTypeSpec Int → [Int] → Specification Int Source #

guardTypeSpec ∷ [String] → TypeSpec Int → Specification Int Source #

prerequisitesEvidence (Prerequisites Int) Source #

Logic NumOrdW Source # 
Instance details

Methods

propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires NumOrdW as b, HasSpec a) ⇒ NumOrdW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source #

propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires NumOrdW as b, HasSpec a) ⇒ NumOrdW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source #

propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires NumOrdW as b, HasSpec a) ⇒ NumOrdW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source #

rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ NumOrdW dom rng → List Term dom → Evidence (AppRequires NumOrdW dom rng) → Maybe (Term rng) Source #

mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ NumOrdW '[a] b → TypeSpec a → Specification b Source #

saturate ∷ ∀ (dom ∷ [Type]). NumOrdW dom Bool → List Term dom → [Pred] Source #

Numeric a ⇒ Complete a Source # 
Instance details

Methods

simplifyASpecification a → Specification a Source #

genFromSpecA ∷ ∀ (m ∷ Type → Type). (HasCallStack, HasSpec a, MonadGenError m) ⇒ Specification a → GenT m a Source #

theAddAIntW '[a, a] a Source #

(HasSpec a, Arbitrary (TypeSpec a)) ⇒ Arbitrary (Specification a) Source # 
Instance details

(Sized [a], HasSpec a) ⇒ HasGenHint [a] Source # 
Instance details

Associated Types

type Hint [a] Source #

Methods

giveHintHint [a] → Specification [a] Source #

HasSpec (Ratio Integer) Source # 
Instance details

Associated Types

type TypeSpec (Ratio Integer) Source #

type Prerequisites (Ratio Integer) Source #

Methods

emptySpecTypeSpec (Ratio Integer) Source #

combineSpecTypeSpec (Ratio Integer) → TypeSpec (Ratio Integer) → Specification (Ratio Integer) Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (Ratio Integer) → GenT m (Ratio Integer) Source #

conformsTo ∷ Ratio Integer → TypeSpec (Ratio Integer) → Bool Source #

shrinkWithTypeSpecTypeSpec (Ratio Integer) → Ratio Integer → [Ratio Integer] Source #

toPredsTerm (Ratio Integer) → TypeSpec (Ratio Integer) → Pred Source #

cardinalTypeSpecTypeSpec (Ratio Integer) → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec (Ratio Integer) → Maybe (NonEmpty String) Source #

alternateShowTypeSpec (Ratio Integer) → BinaryShow Source #

monadConformsTo ∷ Ratio Integer → TypeSpec (Ratio Integer) → Writer [String] Bool Source #

typeSpecOptTypeSpec (Ratio Integer) → [Ratio Integer] → Specification (Ratio Integer) Source #

guardTypeSpec ∷ [String] → TypeSpec (Ratio Integer) → Specification (Ratio Integer) Source #

prerequisitesEvidence (Prerequisites (Ratio Integer)) Source #

(Sized [a], HasSpec a) ⇒ HasSpec [a] Source # 
Instance details

Associated Types

type TypeSpec [a] Source #

type Prerequisites [a] Source #

Methods

emptySpecTypeSpec [a] Source #

combineSpecTypeSpec [a] → TypeSpec [a] → Specification [a] Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec [a] → GenT m [a] Source #

conformsTo ∷ [a] → TypeSpec [a] → Bool Source #

shrinkWithTypeSpecTypeSpec [a] → [a] → [[a]] Source #

toPredsTerm [a] → TypeSpec [a] → Pred Source #

cardinalTypeSpecTypeSpec [a] → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec [a] → Maybe (NonEmpty String) Source #

alternateShowTypeSpec [a] → BinaryShow Source #

monadConformsTo ∷ [a] → TypeSpec [a] → Writer [String] Bool Source #

typeSpecOptTypeSpec [a] → [[a]] → Specification [a] Source #

guardTypeSpec ∷ [String] → TypeSpec [a] → Specification [a] Source #

prerequisitesEvidence (Prerequisites [a]) Source #

Forallable [a] a Source # 
Instance details

(HasSpec a, HasSpec b) ⇒ HasSpec (Prod a b) Source # 
Instance details

Associated Types

type TypeSpec (Prod a b) Source #

type Prerequisites (Prod a b) Source #

Methods

emptySpecTypeSpec (Prod a b) Source #

combineSpecTypeSpec (Prod a b) → TypeSpec (Prod a b) → Specification (Prod a b) Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (Prod a b) → GenT m (Prod a b) Source #

conformsToProd a b → TypeSpec (Prod a b) → Bool Source #

shrinkWithTypeSpecTypeSpec (Prod a b) → Prod a b → [Prod a b] Source #

toPredsTerm (Prod a b) → TypeSpec (Prod a b) → Pred Source #

cardinalTypeSpecTypeSpec (Prod a b) → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec (Prod a b) → Maybe (NonEmpty String) Source #

alternateShowTypeSpec (Prod a b) → BinaryShow Source #

monadConformsToProd a b → TypeSpec (Prod a b) → Writer [String] Bool Source #

typeSpecOptTypeSpec (Prod a b) → [Prod a b] → Specification (Prod a b) Source #

guardTypeSpec ∷ [String] → TypeSpec (Prod a b) → Specification (Prod a b) Source #

prerequisitesEvidence (Prerequisites (Prod a b)) Source #

(HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ HasSpec (Sum a b) Source #

The HasSpec Sum instance

Instance details

Associated Types

type TypeSpec (Sum a b) Source #

type Prerequisites (Sum a b) Source #

Methods

emptySpecTypeSpec (Sum a b) Source #

combineSpecTypeSpec (Sum a b) → TypeSpec (Sum a b) → Specification (Sum a b) Source #

genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (Sum a b) → GenT m (Sum a b) Source #

conformsToSum a b → TypeSpec (Sum a b) → Bool Source #

shrinkWithTypeSpecTypeSpec (Sum a b) → Sum a b → [Sum a b] Source #

toPredsTerm (Sum a b) → TypeSpec (Sum a b) → Pred Source #

cardinalTypeSpecTypeSpec (Sum a b) → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec (Sum a b) → Maybe (NonEmpty String) Source #

alternateShowTypeSpec (Sum a b) → BinaryShow Source #

monadConformsToSum a b → TypeSpec (Sum a b) → Writer [String] Bool Source #

typeSpecOptTypeSpec (Sum a b) → [Sum a b] → Specification (Sum a b) Source #

guardTypeSpec ∷ [String] → TypeSpec (Sum a b) → Specification (Sum a b) Source #

prerequisitesEvidence (Prerequisites (Sum a b)) Source #