Safe Haskell	Safe-Inferred
Language	Haskell2010

Constrained.API

Synopsis

data PredD deps where
- ElemPred ∷ (HasSpecD deps a, Show a) ⇒ Bool → TermD deps a → NonEmpty a → PredD deps
- Monitor ∷ ((∀ a. TermD deps a → a) → Property → Property) → PredD deps
- And ∷ [PredD deps] → PredD deps
- Exists ∷ ((∀ b. TermD deps b → b) → GE a) → BinderD deps a → PredD deps
- Subst ∷ (HasSpecD deps a, Show a) ⇒ Var a → TermD deps a → PredD deps → PredD deps
- Let ∷ TermD deps a → BinderD deps a → PredD deps
- Assert ∷ TermD deps Bool → PredD deps
- Reifies ∷ (HasSpecD deps a, HasSpecD deps b, Show a, Show b) ⇒ TermD deps b → TermD deps a → (a → b) → PredD deps
- DependsOn ∷ (HasSpecD deps a, HasSpecD deps b, Show a, Show b) ⇒ TermD deps a → TermD deps b → PredD deps
- ForAll ∷ (ForallableD deps t e, HasSpecD deps t, HasSpecD deps e, Show t, Show e) ⇒ TermD deps t → BinderD deps e → PredD deps
- Case ∷ (HasSpecD deps (SumOver as), Show (SumOver as)) ⇒ TermD deps (SumOver as) → List (Weighted (BinderD deps)) as → PredD deps
- When ∷ TermD deps Bool → PredD deps → PredD deps
- GenHint ∷ (HasGenHintD deps a, Show a, Show (HintD deps a)) ⇒ HintD deps a → TermD deps a → PredD deps
- TruePred ∷ PredD deps
- FalsePred ∷ NonEmpty String → PredD deps
- Explain ∷ NonEmpty String → PredD deps → PredD deps
data TermD deps a where
- App ∷ AppRequiresD deps t dom rng ⇒ t dom rng → List (TermD deps) dom → TermD deps rng
- Lit ∷ (Typeable a, Eq a, Show a) ⇒ a → TermD deps a
- V ∷ (HasSpecD deps a, Typeable a) ⇒ Var a → TermD deps a
data SpecificationD deps a where
- ExplainSpec ∷ [String] → SpecificationD deps a → SpecificationD deps a
- MemberSpec ∷ NonEmpty a → SpecificationD deps a
- ErrorSpec ∷ NonEmpty String → SpecificationD deps a
- SuspendedSpec ∷ HasSpecD deps a ⇒ Var a → PredD deps → SpecificationD deps a
- TypeSpecD ∷ HasSpecD deps a ⇒ TypeSpecD deps a → [a] → SpecificationD deps a
- TrueSpec ∷ SpecificationD deps a
type GenericallyInstantiated a = (AssertComputes (SimpleRep a) (((Text "Trying to use a generic instantiation of " :<>: ShowType a) :<>: Text ", likely in a HasSpec instance.") :$$: Text "However, the type has no definition of SimpleRep, likely because of a missing instance of HasSimpleRep."), HasSimpleRep a, HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a))
class (Typeable t, Semantics t, Syntax t) ⇒ Logic t where
- propagateTypeSpec ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a
- propagateMemberSpec ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a
- propagate ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → Specification b → Specification a
- rewriteRules ∷ (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ t dom rng → List Term dom → Evidence (AppRequires t dom rng) → Maybe (Term rng)
- mapTypeSpec ∷ ∀ a b. (HasSpec a, HasSpec b) ⇒ t '[a] b → TypeSpec a → Specification b
- saturate ∷ t dom Bool → List Term dom → [Pred]
class Semantics (t ∷ [Type] → Type → Type) where
- semantics ∷ t d r → FunTy d r
class Syntax (t ∷ [Type] → Type → Type) where
- isInfix ∷ t dom rng → Bool
- prettySymbol ∷ ∀ deps dom rng ann. t dom rng → List (TermD deps) dom → Int → Maybe (Doc ann)
class (HasSpec a, NumLike a, Logic IntW) ⇒ Foldy a where
- genList ∷ MonadGenError m ⇒ Specification a → Specification a → GenT m [a]
- theAddFn ∷ IntW '[a, a] a
- theZero ∷ a
- genSizedList ∷ MonadGenError m ⇒ Specification Integer → Specification a → Specification a → GenT m [a]
- noNegativeValues ∷ Bool
data NumSpec n = NumSpecInterval (Maybe n) (Maybe n)
class MaybeBounded a where
- lowerBound ∷ Maybe a
- upperBound ∷ Maybe a
data NonEmpty a = a :| [a]
type Specification = SpecificationD Deps
pattern TypeSpec ∷ () ⇒ HasSpec a ⇒ TypeSpec a → [a] → Specification a
type Term = TermD Deps
data Fun dom rng where
- Fun ∷ ∀ t dom rng. AppRequires t dom rng ⇒ t dom rng → Fun dom rng
name ∷ String → Term a → Term a
named ∷ String → Term a → Term a
type Pred = PredD Deps
class (Typeable a, Eq a, Show a, TypeSpecEqShow a) ⇒ HasSpec a where
- type TypeSpec a
- type Prerequisites a ∷ Constraint
- emptySpec ∷ TypeSpec a
- combineSpec ∷ TypeSpec a → TypeSpec a → Specification a
- genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a
- conformsTo ∷ HasCallStack ⇒ a → TypeSpec a → Bool
- shrinkWithTypeSpec ∷ TypeSpec a → a → [a]
- toPreds ∷ Term a → TypeSpec a → Pred
- cardinalTypeSpec ∷ TypeSpec a → Specification Integer
- cardinalTrueSpec ∷ Specification Integer
- typeSpecHasError ∷ TypeSpec a → Maybe (NonEmpty String)
- alternateShow ∷ TypeSpec a → BinaryShow
- monadConformsTo ∷ a → TypeSpec a → Writer [String] Bool
- typeSpecOpt ∷ TypeSpec a → [a] → Specification a
- guardTypeSpec ∷ [String] → TypeSpec a → Specification a
- prerequisites ∷ Evidence (Prerequisites a)
class Typeable (SimpleRep a) ⇒ HasSimpleRep a where
- type SimpleRep a
- type TheSop a ∷ [Type]
- toSimpleRep ∷ a → SimpleRep a
- fromSimpleRep ∷ SimpleRep a → a
class (Ord a, HasSpec a) ⇒ OrdLike a where
- leqSpec ∷ a → Specification a
- ltSpec ∷ a → Specification a
- geqSpec ∷ a → Specification a
- gtSpec ∷ a → Specification a
conformsToSpecE ∷ ∀ a. HasSpec a ⇒ a → Specification a → NonEmpty String → Maybe (NonEmpty String)
conformsToSpec ∷ HasSpec a ⇒ a → Specification a → Bool
satisfies ∷ ∀ a. HasSpec a ⇒ Term a → Specification a → Pred
genFromSpecT ∷ ∀ a m. (HasCallStack, HasSpec a, MonadGenError m) ⇒ Specification a → GenT m a
genFromSpec ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Specification a → Gen a
debugSpec ∷ ∀ a. HasSpec a ⇒ Specification a → IO ()
genFromSpecWithSeed ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Int → Int → Specification a → a
simplifySpec ∷ HasSpec a ⇒ Specification a → Specification a
cardinality ∷ ∀ a. (Number Integer, HasSpec a) ⇒ Specification a → Specification Integer
ifElse ∷ (IsPred p, IsPred q) ⇒ Term Bool → p → q → Pred
whenTrue ∷ ∀ p. IsPred p ⇒ Term Bool → p → Pred
simplifyTerm ∷ ∀ a. Term a → Term a
constrained ∷ ∀ a p. (IsPred p, HasSpec a) ⇒ (Term a → p) → Specification a
assertExplain ∷ IsPred p ⇒ NonEmpty String → p → Pred
assert ∷ IsPred p ⇒ p → Pred
forAll ∷ ∀ p t a. (Forallable t a, HasSpec t, HasSpec a, IsPred p) ⇒ Term t → (Term a → p) → Pred
exists ∷ ∀ a p. (HasSpec a, IsPred p) ⇒ ((∀ b. Term b → b) → GE a) → (Term a → p) → Pred
unsafeExists ∷ ∀ a p. (HasSpec a, IsPred p) ⇒ (Term a → p) → Pred
letBind ∷ (HasSpec a, IsPred p) ⇒ Term a → (Term a → p) → Pred
reify ∷ (HasSpec a, HasSpec b, IsPred p) ⇒ Term a → (a → b) → (Term b → p) → Pred
assertReified ∷ HasSpec a ⇒ Term a → (a → Bool) → Pred
explanation ∷ NonEmpty String → Pred → Pred
monitor ∷ ((∀ a. Term a → a) → Property → Property) → Pred
reifies ∷ (HasSpec a, HasSpec b) ⇒ Term b → Term a → (a → b) → Pred
dependsOn ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Pred
lit ∷ HasSpec a ⇒ a → Term a
genHint ∷ ∀ t. HasGenHint t ⇒ Hint t → Term t → Pred
giveHint ∷ HasGenHint a ⇒ Hint a → Specification a
(<.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool
(<=.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool
(>=.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool
(>.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool
(==.) ∷ HasSpec a ⇒ Term a → Term a → Term Bool
(/=.) ∷ HasSpec a ⇒ Term a → Term a → Term Bool
not_ ∷ Term Bool → Term Bool
or_ ∷ Term Bool → Term Bool → Term Bool
(||.) ∷ Term Bool → Term Bool → Term Bool
toGeneric_ ∷ ∀ a. GenericRequires a ⇒ Term a → Term (SimpleRep a)
fromGeneric_ ∷ ∀ a. (GenericRequires a, AppRequires BaseW '[SimpleRep a] a) ⇒ Term (SimpleRep a) → Term a
(+.) ∷ NumLike a ⇒ Term a → Term a → Term a
(-.) ∷ Numeric n ⇒ Term n → Term n → Term n
negate_ ∷ NumLike a ⇒ Term a → Term a
addFn ∷ ∀ a. NumLike a ⇒ Term a → Term a → Term a
negateFn ∷ ∀ a. NumLike a ⇒ Term a → Term a
type Numeric a = (HasSpec a, Ord a, Num a, TypeSpec a ~ NumSpec a, MaybeBounded a)
pair_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term b → Term (a, b)
fst_ ∷ (HasSpec x, HasSpec y) ⇒ Term (x, y) → Term x
snd_ ∷ (HasSpec x, HasSpec y) ⇒ Term (x, y) → Term y
prodSnd_ ∷ (HasSpec a, HasSpec b) ⇒ Term (Prod a b) → Term b
prodFst_ ∷ (HasSpec a, HasSpec b) ⇒ Term (Prod a b) → Term a
prod_ ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Term (Prod a b)
type IsNormalType a = (AssertComputes (Cases a) (Text "Failed to compute Cases in a use of IsNormalType for " :$$: (ShowType a :<>: Text ", are you missing an IsNormalType constraint?")), Cases a ~ '[a], AssertComputes (Args a) ((Text "Failed to compute Args in a use of IsNormalType for " :<>: ShowType a) :<>: Text ", are you missing an IsNormalType constraint?"), Args a ~ '[a], IsProd a, CountCases a ~ 1)
injLeft_ ∷ (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Term a → Term (Sum a b)
injRight_ ∷ (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Term b → Term (Sum a b)
left_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term (Either a b)
right_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term b → Term (Either a b)
cJust_ ∷ (HasSpec a, IsNormalType a) ⇒ Term a → Term (Maybe a)
cNothing_ ∷ (HasSpec a, IsNormalType a) ⇒ Term (Maybe a)
caseOn ∷ ∀ a. (GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) ⇒ Term a → FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
branch ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ FunTy (MapList Term (Args a)) p → Weighted Binder a
branchW ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ Int → FunTy (MapList Term (Args a)) p → Weighted Binder a
forAll' ∷ ∀ t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t, HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a), IsProductType a, HasSpec a, GenericRequires a, ProdAsListComputes a) ⇒ Term t → FunTy (MapList Term (ProductAsList a)) p → Pred
constrained' ∷ ∀ a p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p, GenericRequires a, ProdAsListComputes a) ⇒ FunTy (MapList Term (ProductAsList a)) p → Specification a
reify' ∷ ∀ a b p. (Cases (SimpleRep b) ~ '[SimpleRep b], TypeSpec b ~ TypeSpec (SimpleRep b), HasSpec (SimpleRep b), HasSimpleRep b, All HasSpec (Args (SimpleRep b)), IsProd (SimpleRep b), HasSpec a, HasSpec b, IsProductType b, IsProd a, IsPred p, GenericRequires b, ProdAsListComputes b) ⇒ Term a → (a → b) → FunTy (MapList Term (ProductAsList b)) p → Pred
con ∷ ∀ c a r. (SimpleRep a ~ SOP (TheSop a), TypeSpec a ~ TypeSpec (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a), ResultType r ~ Term a, SOPTerm c (TheSop a), ConstrTerm (ConstrOf c (TheSop a)), GenericRequires a) ⇒ r
onCon ∷ ∀ c a p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All HasSpec (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term a → FunTy (MapList Term (ConstrOf c (TheSop a))) p → Pred
isCon ∷ ∀ c a. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), GenericRequires a) ⇒ Term a → Pred
sel ∷ ∀ n a c as. (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a, HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) ⇒ Term a → Term (At n as)
match ∷ ∀ p a. (IsProductType a, IsPred p, GenericRequires a, ProdAsListComputes a) ⇒ Term a → FunTy (MapList Term (ProductAsList a)) p → Pred
onJust ∷ ∀ a p. (HasSpec a, IsNormalType a, IsPred p) ⇒ Term (Maybe a) → (Term a → p) → Pred
isJust ∷ ∀ a. (HasSpec a, IsNormalType a) ⇒ Term (Maybe a) → Pred
chooseSpec ∷ HasSpec a ⇒ (Int, Specification a) → (Int, Specification a) → Specification a
equalSpec ∷ a → Specification a
notEqualSpec ∷ ∀ a. HasSpec a ⇒ a → Specification a
notMemberSpec ∷ ∀ a f. (HasSpec a, Foldable f) ⇒ f a → Specification a
id_ ∷ ∀ a. HasSpec a ⇒ Term a → Term a
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
compose_ ∷ ∀ b t1 t2 a r. (AppRequires t1 '[b] r, AppRequires t2 '[a] b) ⇒ t1 '[b] r → t2 '[a] b → Term a → Term r
foldMap_ ∷ ∀ a b. (Foldy b, HasSpec a) ⇒ (Term a → Term b) → Term [a] → Term b
sum_ ∷ Foldy a ⇒ Term [a] → Term a
elem_ ∷ (Sized [a], HasSpec a) ⇒ Term a → Term [a] → Term Bool
singletonList_ ∷ (Sized [a], HasSpec a) ⇒ Term a → Term [a]
append_ ∷ (Sized [a], HasSpec a) ⇒ Term [a] → Term [a] → Term [a]
(++.) ∷ HasSpec a ⇒ Term [a] → Term [a] → Term [a]
sizeOf ∷ Sized t ⇒ t → Integer
sizeOf_ ∷ (HasSpec a, Sized a) ⇒ Term a → Term Integer
null_ ∷ (HasSpec a, Sized a) ⇒ Term a → Term Bool
hasSize ∷ (HasSpec t, Sized t) ⇒ SizeSpec → Specification t
rangeSize ∷ Integer → Integer → SizeSpec
length_ ∷ HasSpec a ⇒ Term [a] → Term Integer
genFromSizeSpec ∷ MonadGenError m ⇒ Specification Integer → GenT m Integer
between ∷ (HasSpec a, TypeSpec a ~ NumSpec a) ⇒ a → a → Specification a
maxSpec ∷ Specification Integer → Specification Integer
data SetW (d ∷ [Type]) (r ∷ Type) where
- SingletonW ∷ (HasSpec a, Ord a) ⇒ SetW '[a] (Set a)
- UnionW ∷ (HasSpec a, Ord a) ⇒ SetW '[Set a, Set a] (Set a)
- SubsetW ∷ (HasSpec a, Ord a, HasSpec a) ⇒ SetW '[Set a, Set a] Bool
- MemberW ∷ (HasSpec a, Ord a) ⇒ SetW '[a, Set a] Bool
- DisjointW ∷ (HasSpec a, Ord a) ⇒ SetW '[Set a, Set a] Bool
- FromListW ∷ (HasSpec a, Ord a) ⇒ SetW '[[a]] (Set a)
data SetSpec a = SetSpec (Set a) (Specification a) (Specification Integer)
singleton_ ∷ (Ord a, HasSpec a) ⇒ Term a → Term (Set a)
member_ ∷ (Ord a, HasSpec a) ⇒ Term a → Term (Set a) → Term Bool
union_ ∷ (Ord a, HasSpec a) ⇒ Term (Set a) → Term (Set a) → Term (Set a)
subset_ ∷ (Ord a, HasSpec a) ⇒ Term (Set a) → Term (Set a) → Term Bool
disjoint_ ∷ (Ord a, HasSpec a) ⇒ Term (Set a) → Term (Set a) → Term Bool
fromList_ ∷ ∀ a. (Ord a, HasSpec a) ⇒ Term [a] → Term (Set a)
pattern Elem ∷ ∀ b. () ⇒ ∀ a. (b ~ Bool, Eq a, HasSpec a) ⇒ Term a → Term [a] → Term b
pattern ToGeneric ∷ ∀ rng. () ⇒ ∀ a. (rng ~ SimpleRep a, GenericRequires a, HasSpec a, AppRequires BaseW '[a] rng) ⇒ Term a → Term rng
pattern FromGeneric ∷ ∀ rng. () ⇒ ∀ a. (rng ~ a, GenericRequires a, HasSpec a, AppRequires BaseW '[SimpleRep a] rng) ⇒ Term (SimpleRep a) → Term rng
pattern Unary ∷ HOLE a' a → ListCtx f '[a] (HOLE a')
pattern (:<:) ∷ (Typeable b, Show b) ⇒ HOLE c a → b → ListCtx Value '[a, b] (HOLE c)
pattern (:>:) ∷ (Typeable a, Show a) ⇒ a → HOLE c b → ListCtx Value '[a, b] (HOLE c)
printPlan ∷ HasSpec a ⇒ Specification a → IO ()
class (Num a, HasSpec a) ⇒ NumLike a
data PairSpec a b = Cartesian (Specification a) (Specification b)
data MapSpec k v = MapSpec {
- mapSpecHint ∷ Maybe Integer
- mapSpecMustKeys ∷ Set k
- mapSpecMustValues ∷ [v]
- mapSpecSize ∷ Specification Integer
- mapSpecElem ∷ Specification (k, v)
- mapSpecFold ∷ FoldSpec v
}
dom_ ∷ (HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term (Set k)
rng_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term [v]
lookup_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term k → Term (Map k v) → Term (Maybe v)
mapMember_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term k → Term (Map k v) → Term Bool
fstSpec ∷ ∀ k v. (HasSpec k, HasSpec v) ⇒ Specification (k, v) → Specification k
sndSpec ∷ ∀ k v. (HasSpec k, HasSpec v) ⇒ Specification (k, v) → Specification v
var ∷ QuasiQuoter
data Prod a b = Prod {
- prodFst ∷ a
- prodSnd ∷ b
}

Documentation

data PredD deps where Source #

Constructors

ElemPred ∷ (HasSpecD deps a, Show a) ⇒ Bool → TermD deps a → NonEmpty a → PredD deps
Monitor ∷ ((∀ a. TermD deps a → a) → Property → Property) → PredD deps
And ∷ [PredD deps] → PredD deps
Exists
Fields ∷ ((∀ b. TermD deps b → b) → GE a) Constructive recovery function for checking existential quantification → BinderD deps a → PredD deps
Subst ∷ (HasSpecD deps a, Show a) ⇒ Var a → TermD deps a → PredD deps → PredD deps
Let ∷ TermD deps a → BinderD deps a → PredD deps
Assert ∷ TermD deps Bool → PredD deps
Reifies
Fields ∷ (HasSpecD deps a, HasSpecD deps b, Show a, Show b) ⇒ TermD deps b This depends on the `a` term → TermD deps a → (a → b) Recover a useable value from the `a` term. → PredD deps
DependsOn ∷ (HasSpecD deps a, HasSpecD deps b, Show a, Show b) ⇒ TermD deps a → TermD deps b → PredD deps
ForAll ∷ (ForallableD deps t e, HasSpecD deps t, HasSpecD deps e, Show t, Show e) ⇒ TermD deps t → BinderD deps e → PredD deps
Case
Fields ∷ (HasSpecD deps (SumOver as), Show (SumOver as)) ⇒ TermD deps (SumOver as) → List (Weighted (BinderD deps)) as Each branch of the type is bound with only one variable because `as` are types. Constructors with multiple arguments are encoded with `ProdOver` (c.f. `Univ`). → PredD deps
When ∷ TermD deps Bool → PredD deps → PredD deps
GenHint ∷ (HasGenHintD deps a, Show a, Show (HintD deps a)) ⇒ HintD deps a → TermD deps a → PredD deps
TruePred ∷ PredD deps
FalsePred ∷ NonEmpty String → PredD deps
Explain ∷ NonEmpty String → PredD deps → PredD deps

Instances

Instances details

IsPred Pred Source #
Instance details Defined in Constrained.Base Methods toPred ∷ Pred → Pred Source #
Rename Pred Source #
Instance details Defined in Constrained.Syntax Methods rename ∷ Typeable x ⇒ Var x → Var x → Pred → Pred Source #
HasVariables Pred Source #
Instance details Defined in Constrained.Syntax Methods freeVars ∷ Pred → FreeVars Source # freeVarSet ∷ Pred → Set Name Source # countOf ∷ Name → Pred → Int Source # appearsIn ∷ Name → Pred → Bool Source #
Monoid (PredD deps) Source #
Instance details Defined in Constrained.AbstractSyntax Methods mempty ∷ PredD deps # mappend ∷ PredD deps → PredD deps → PredD deps # mconcat ∷ [PredD deps] → PredD deps #
Semigroup (PredD deps) Source #
Instance details Defined in Constrained.AbstractSyntax Methods (<>) ∷ PredD deps → PredD deps → PredD deps # sconcat ∷ NonEmpty (PredD deps) → PredD deps # stimes ∷ Integral b ⇒ b → PredD deps → PredD deps #
Show (PredD deps) Source #
Instance details Defined in Constrained.AbstractSyntax Methods showsPrec ∷ Int → PredD deps → ShowS # show ∷ PredD deps → String # showList ∷ [PredD deps] → ShowS #
Pretty (PredD deps) Source #
Instance details Defined in Constrained.AbstractSyntax Methods pretty ∷ PredD deps → Doc ann Source # prettyList ∷ [PredD deps] → Doc ann Source #

data TermD deps a where Source #

Constructors

App ∷ AppRequiresD deps t dom rng ⇒ t dom rng → List (TermD deps) dom → TermD deps rng
Lit ∷ (Typeable a, Eq a, Show a) ⇒ a → TermD deps a
V ∷ (HasSpecD deps a, Typeable a) ⇒ Var a → TermD deps a

Instances

Instances details

(Ord a, HasSpec a, HasSpec (Set a)) ⇒ Monoid (Term (Set a)) Source #
Instance details Defined in Constrained.Spec.Set Methods mempty ∷ Term (Set a) # mappend ∷ Term (Set a) → Term (Set a) → Term (Set a) # mconcat ∷ [Term (Set a)] → Term (Set a) #
(Ord a, HasSpec a, HasSpec (Set a)) ⇒ Semigroup (Term (Set a)) Source #
Instance details Defined in Constrained.Spec.Set Methods (<>) ∷ Term (Set a) → Term (Set a) → Term (Set a) # sconcat ∷ NonEmpty (Term (Set a)) → Term (Set a) # stimes ∷ Integral b ⇒ b → Term (Set a) → Term (Set a) #
NumLike a ⇒ Num (Term a) Source #
Instance details Defined in Constrained.NumOrd Methods (+) ∷ Term a → Term a → Term a # (-) ∷ Term a → Term a → Term a # (*) ∷ Term a → Term a → Term a # negate ∷ Term a → Term a # abs ∷ Term a → Term a # signum ∷ Term a → Term a # fromInteger ∷ Integer → Term a #
IsPred (Term Bool) Source #
Instance details Defined in Constrained.Base Methods toPred ∷ Term Bool → Pred Source #
Rename (Term a) Source #
Instance details Defined in Constrained.Syntax Methods rename ∷ Typeable x ⇒ Var x → Var x → Term a → Term a Source #
HasVariables (Term a) Source #
Instance details Defined in Constrained.Syntax Methods freeVars ∷ Term a → FreeVars Source # freeVarSet ∷ Term a → Set Name Source # countOf ∷ Name → Term a → Int Source # appearsIn ∷ Name → Term a → Bool Source #
Show a ⇒ Pretty (WithPrec (TermD deps a)) Source #
Instance details Defined in Constrained.AbstractSyntax Methods pretty ∷ WithPrec (TermD deps a) → Doc ann Source # prettyList ∷ [WithPrec (TermD deps a)] → Doc ann Source #
Show a ⇒ Show (TermD deps a) Source #
Instance details Defined in Constrained.AbstractSyntax Methods showsPrec ∷ Int → TermD deps a → ShowS # show ∷ TermD deps a → String # showList ∷ [TermD deps a] → ShowS #
Eq (TermD deps a) Source #
Instance details Defined in Constrained.AbstractSyntax Methods (==) ∷ TermD deps a → TermD deps a → Bool # (/=) ∷ TermD deps a → TermD deps a → Bool #
Show a ⇒ Pretty (TermD deps a) Source #
Instance details Defined in Constrained.AbstractSyntax Methods pretty ∷ TermD deps a → Doc ann Source # prettyList ∷ [TermD deps a] → Doc ann Source #
HasVariables (List Term as) Source #
Instance details Defined in Constrained.Syntax Methods freeVars ∷ List Term as → FreeVars Source # freeVarSet ∷ List Term as → Set Name Source # countOf ∷ Name → List Term as → Int Source # appearsIn ∷ Name → List Term as → Bool Source #

data SpecificationD deps a where Source #

A `Specification a` denotes a set of as

Constructors

ExplainSpec ∷ [String] → SpecificationD deps a → SpecificationD deps a	Explain a Specification
MemberSpec	Elements of a known set
Fields ∷ NonEmpty a It must be an element of this OrdSet (List). Try hard not to put duplicates in the List. → SpecificationD deps a
ErrorSpec ∷ NonEmpty String → SpecificationD deps a	The empty set
SuspendedSpec	The set described by some predicates over the bound variable.
Fields ∷ HasSpecD deps a ⇒ Var a This variable ranges over values denoted by the spec → PredD deps And the variable is subject to these constraints → SpecificationD deps a
TypeSpecD	A type-specific spec
Fields ∷ HasSpecD deps a ⇒ TypeSpecD deps a → [a] It can't be any of the elements of this set → SpecificationD deps a
TrueSpec ∷ SpecificationD deps a	Anything

Instances

Instances details

(HasSpec a, Arbitrary (TypeSpec a)) ⇒ Arbitrary (Specification a) Source #
Instance details Defined in Constrained.Test Methods arbitrary ∷ Gen (Specification a) Source # shrink ∷ Specification a → [Specification a] Source #
HasSpec a ⇒ Monoid (Specification a) Source #
Instance details Defined in Constrained.Conformance Methods mempty ∷ Specification a # mappend ∷ Specification a → Specification a → Specification a # mconcat ∷ [Specification a] → Specification a #
HasSpec a ⇒ Semigroup (Specification a) Source #
Instance details Defined in Constrained.Conformance Methods (<>) ∷ Specification a → Specification a → Specification a # sconcat ∷ NonEmpty (Specification a) → Specification a # stimes ∷ Integral b ⇒ b → Specification a → Specification a #
Number Integer ⇒ Num (Specification Integer) Source #	This is very liberal, since in lots of cases it returns TrueSpec. for example all operations on SuspendedSpec, and certain operations between TypeSpec and MemberSpec. Perhaps we should remove it. Only the addSpec (+) and multSpec (*) methods are used. But, it is kind of cool ... In Fact we can use this to make Num(Specification n) instance for any `n`. But, only Integer is safe, because in all other types (+) and especially (-) can lead to overflow or underflow failures.
Instance details Defined in Constrained.NumOrd Methods (+) ∷ Specification Integer → Specification Integer → Specification Integer # (-) ∷ Specification Integer → Specification Integer → Specification Integer # (*) ∷ Specification Integer → Specification Integer → Specification Integer # negate ∷ Specification Integer → Specification Integer # abs ∷ Specification Integer → Specification Integer # signum ∷ Specification Integer → Specification Integer # fromInteger ∷ Integer → Specification Integer #
(Show a, Typeable a, Show (TypeSpecD deps a)) ⇒ Pretty (WithPrec (SpecificationD deps a)) Source #
Instance details Defined in Constrained.AbstractSyntax Methods pretty ∷ WithPrec (SpecificationD deps a) → Doc ann Source # prettyList ∷ [WithPrec (SpecificationD deps a)] → Doc ann Source #
(Show a, Typeable a, Show (TypeSpecD deps a)) ⇒ Show (SpecificationD deps a) Source #
Instance details Defined in Constrained.AbstractSyntax Methods showsPrec ∷ Int → SpecificationD deps a → ShowS # show ∷ SpecificationD deps a → String # showList ∷ [SpecificationD deps a] → ShowS #
(Show a, Typeable a, Show (TypeSpecD deps a)) ⇒ Pretty (SpecificationD deps a) Source #
Instance details Defined in Constrained.AbstractSyntax Methods pretty ∷ SpecificationD deps a → Doc ann Source # prettyList ∷ [SpecificationD deps a] → Doc ann Source #

type GenericallyInstantiated a = (AssertComputes (SimpleRep a) (((Text "Trying to use a generic instantiation of " :<>: ShowType a) :<>: Text ", likely in a HasSpec instance.") :$$: Text "However, the type has no definition of SimpleRep, likely because of a missing instance of HasSimpleRep."), HasSimpleRep a, HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) Source #

class (Typeable t, Semantics t, Syntax t) ⇒ Logic t where Source #

A First-order typed logic has 4 components 1. Terms (Variables (x), Constants (5), and Applications (F x 5) Applications, apply a function symbol to a list of arguments: (FunctionSymbol term1 .. termN) 2. Predicates (Ordered, Odd, ...) 3. Connectives (And, Or, Not, =>, ...) 4. Quantifiers (Forall, Exists)

The Syntax, Semantics, and Logic classes implement new function symbols in the first order logic. Note that a function symbol is first order data, that uniquely identifies a higher order function. The three classes supply varying levels of functionality, relating to the Syntax, Semantics, and Logical operations of the function symbol.

Logical operations are one that support reasoning about how a function symbol relates to logical properties, that we call Specification's

Minimal complete definition

propagate | propagateTypeSpec, propagateMemberSpec

Methods

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

propagateMemberSpec ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source #

propagate ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source #

rewriteRules ∷ (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ t dom rng → List Term dom → Evidence (AppRequires t dom rng) → Maybe (Term rng) Source #

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

saturate ∷ t dom Bool → List Term dom → [Pred] Source #

Instances

Instances details

Logic BaseW Source #
Instance details Defined in Constrained.Base Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires BaseW as b, HasSpec a) ⇒ BaseW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires BaseW as b, HasSpec a) ⇒ BaseW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires BaseW as b, HasSpec a) ⇒ BaseW 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) ⇒ BaseW dom rng → List Term dom → Evidence (AppRequires BaseW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ BaseW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). BaseW dom Bool → List Term dom → [Pred] Source #
Logic BoolW Source #
Instance details Defined in Constrained.Generation 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 #
Logic EqW Source #
Instance details Defined in Constrained.Generation 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 #
Logic SumW Source #
Instance details Defined in Constrained.Generation 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 #
Logic IntW Source #	Just a note that these instances won't work until we are in a context where there is a HasSpec instance of `a`, which (NumLike a) demands. This happens in Constrained.Experiment.TheKnot
Instance details Defined in Constrained.NumOrd Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires IntW as b, HasSpec a) ⇒ IntW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires IntW as b, HasSpec a) ⇒ IntW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires IntW as b, HasSpec a) ⇒ IntW 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) ⇒ IntW dom rng → List Term dom → Evidence (AppRequires IntW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ IntW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). IntW dom Bool → List Term dom → [Pred] Source #
Logic OrdW Source #
Instance details Defined in Constrained.NumOrd Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires OrdW as b, HasSpec a) ⇒ OrdW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires OrdW as b, HasSpec a) ⇒ OrdW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires OrdW as b, HasSpec a) ⇒ OrdW 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) ⇒ OrdW dom rng → List Term dom → Evidence (AppRequires OrdW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ OrdW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). OrdW dom Bool → List Term dom → [Pred] Source #
Logic MapW Source #
Instance details Defined in Constrained.Spec.Map Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires MapW as b, HasSpec a) ⇒ MapW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires MapW as b, HasSpec a) ⇒ MapW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires MapW as b, HasSpec a) ⇒ MapW 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) ⇒ MapW dom rng → List Term dom → Evidence (AppRequires MapW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ MapW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). MapW dom Bool → List Term dom → [Pred] Source #
Logic SetW Source #
Instance details Defined in Constrained.Spec.Set Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SetW as b, HasSpec a) ⇒ SetW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SetW as b, HasSpec a) ⇒ SetW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires SetW as b, HasSpec a) ⇒ SetW 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) ⇒ SetW dom rng → List Term dom → Evidence (AppRequires SetW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ SetW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). SetW dom Bool → List Term dom → [Pred] Source #
Logic TreeW Source #
Instance details Defined in Constrained.Spec.Tree Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires TreeW as b, HasSpec a) ⇒ TreeW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires TreeW as b, HasSpec a) ⇒ TreeW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires TreeW as b, HasSpec a) ⇒ TreeW 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) ⇒ TreeW dom rng → List Term dom → Evidence (AppRequires TreeW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ TreeW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). TreeW dom Bool → List Term dom → [Pred] Source #
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 #
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 #
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 #
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 #
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 #

class Semantics (t ∷ [Type] → Type → Type) where Source #

Semantic operations are ones that give the function symbol, meaning as a function. I.e. how to apply the function to a list of arguments and return a value.

Methods

semantics ∷ t d r → FunTy d r Source #

Instances

Instances details

Semantics BaseW Source #
Instance details Defined in Constrained.Base Methods semantics ∷ ∀ (d ∷ [Type]) r. BaseW d r → FunTy d r Source #
Semantics BoolW Source #
Instance details Defined in Constrained.Generation Methods semantics ∷ ∀ (d ∷ [Type]) r. BoolW d r → FunTy d r Source #
Semantics EqW Source #
Instance details Defined in Constrained.Generation Methods semantics ∷ ∀ (d ∷ [Type]) r. EqW d r → FunTy d r Source #
Semantics SumW Source #
Instance details Defined in Constrained.Generation Methods semantics ∷ ∀ (d ∷ [Type]) r. SumW d r → FunTy d r Source #
Semantics IntW Source #
Instance details Defined in Constrained.NumOrd Methods semantics ∷ ∀ (d ∷ [Type]) r. IntW d r → FunTy d r Source #
Semantics OrdW Source #
Instance details Defined in Constrained.NumOrd Methods semantics ∷ ∀ (d ∷ [Type]) r. OrdW d r → FunTy d r Source #
Semantics MapW Source #
Instance details Defined in Constrained.Spec.Map Methods semantics ∷ ∀ (d ∷ [Type]) r. MapW d r → FunTy d r Source #
Semantics SetW Source #
Instance details Defined in Constrained.Spec.Set Methods semantics ∷ ∀ (d ∷ [Type]) r. SetW d r → FunTy d r Source #
Semantics TreeW Source #
Instance details Defined in Constrained.Spec.Tree Methods semantics ∷ ∀ (d ∷ [Type]) r. TreeW d r → FunTy d r Source #
Semantics ElemW Source #
Instance details Defined in Constrained.TheKnot Methods semantics ∷ ∀ (d ∷ [Type]) r. ElemW d r → FunTy d r Source #
Semantics FunW Source #
Instance details Defined in Constrained.TheKnot Methods semantics ∷ ∀ (d ∷ [Type]) r. FunW d r → FunTy d r Source #
Semantics ListW Source #
Instance details Defined in Constrained.TheKnot Methods semantics ∷ ∀ (d ∷ [Type]) r. ListW d r → FunTy d r Source #
Semantics ProdW Source #
Instance details Defined in Constrained.TheKnot Methods semantics ∷ ∀ (d ∷ [Type]) r. ProdW d r → FunTy d r Source #
Semantics SizeW Source #
Instance details Defined in Constrained.TheKnot Methods semantics ∷ ∀ (d ∷ [Type]) r. SizeW d r → FunTy d r Source #

class Syntax (t ∷ [Type] → Type → Type) where Source #

Syntactic operations are ones that have to do with the structure and appearence of the type. See DependencyInjection to better understand deps - it's a pointer to postpone having to define HasSpec and friends here.

Minimal complete definition

Nothing

Methods

isInfix ∷ t dom rng → Bool Source #

prettySymbol ∷ ∀ deps dom rng ann. t dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #

Instances

Instances details

Syntax BaseW Source #
Instance details Defined in Constrained.Base Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. BaseW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. BaseW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Syntax BoolW Source #
Instance details Defined in Constrained.Generation Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. BoolW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. BoolW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Syntax EqW Source #
Instance details Defined in Constrained.Generation Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. EqW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. EqW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Syntax SumW Source #
Instance details Defined in Constrained.Generation Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. SumW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. SumW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Syntax IntW Source #
Instance details Defined in Constrained.NumOrd Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. IntW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. IntW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Syntax OrdW Source #
Instance details Defined in Constrained.NumOrd Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. OrdW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. OrdW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Syntax MapW Source #
Instance details Defined in Constrained.Spec.Map Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. MapW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. MapW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Syntax SetW Source #
Instance details Defined in Constrained.Spec.Set Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. SetW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. SetW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Syntax TreeW Source #
Instance details Defined in Constrained.Spec.Tree Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. TreeW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. TreeW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Syntax ElemW Source #
Instance details Defined in Constrained.TheKnot Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. ElemW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. ElemW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Syntax FunW Source #
Instance details Defined in Constrained.TheKnot Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. FunW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. FunW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Syntax ListW Source #
Instance details Defined in Constrained.TheKnot Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. ListW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. ListW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Syntax ProdW Source #
Instance details Defined in Constrained.TheKnot Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. ProdW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. ProdW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Syntax SizeW Source #
Instance details Defined in Constrained.TheKnot Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. SizeW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. SizeW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #

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

Minimal complete definition

genList, genSizedList, noNegativeValues

Methods

genList ∷ MonadGenError m ⇒ Specification a → Specification a → GenT m [a] Source #

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

theZero ∷ a Source #

genSizedList ∷ MonadGenError m ⇒ Specification Integer → Specification a → Specification a → GenT m [a] Source #

noNegativeValues ∷ Bool Source #

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 # theAddFn ∷ IntW '[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 # theAddFn ∷ IntW '[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 # theAddFn ∷ IntW '[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 # theAddFn ∷ IntW '[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 # theAddFn ∷ IntW '[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 # theAddFn ∷ IntW '[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 # theAddFn ∷ IntW '[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 # theAddFn ∷ IntW '[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 # theAddFn ∷ IntW '[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 # theAddFn ∷ IntW '[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 # theAddFn ∷ IntW '[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 #

data NumSpec n Source #

Constructors

NumSpecInterval (Maybe n) (Maybe n)

Instances

Instances details

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

class MaybeBounded a where Source #

Minimal complete definition

Nothing

Methods

lowerBound ∷ Maybe a Source #

default lowerBound ∷ Bounded a ⇒ Maybe a Source #

upperBound ∷ Maybe a Source #

default upperBound ∷ Bounded a ⇒ Maybe a Source #

Instances

Instances details

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

data NonEmpty a #

Non-empty (and non-strict) list type.

Since: base-4.9.0.0

Constructors

a :| [a] infixr 5

Instances

Instances details

Foldable NonEmpty	Since: base-4.9.0.0
Instance details Defined in Data.Foldable Methods fold ∷ Monoid m ⇒ NonEmpty m → m # foldMap ∷ Monoid m ⇒ (a → m) → NonEmpty a → m # foldMap' ∷ Monoid m ⇒ (a → m) → NonEmpty a → m # foldr ∷ (a → b → b) → b → NonEmpty a → b # foldr' ∷ (a → b → b) → b → NonEmpty a → b # foldl ∷ (b → a → b) → b → NonEmpty a → b # foldl' ∷ (b → a → b) → b → NonEmpty a → b # foldr1 ∷ (a → a → a) → NonEmpty a → a # foldl1 ∷ (a → a → a) → NonEmpty a → a # toList ∷ NonEmpty a → [a] # null ∷ NonEmpty a → Bool # length ∷ NonEmpty a → Int # elem ∷ Eq a ⇒ a → NonEmpty a → Bool # maximum ∷ Ord a ⇒ NonEmpty a → a # minimum ∷ Ord a ⇒ NonEmpty a → a # sum ∷ Num a ⇒ NonEmpty a → a # product ∷ Num a ⇒ NonEmpty a → a #
Eq1 NonEmpty	Since: base-4.10.0.0
Instance details Defined in Data.Functor.Classes Methods liftEq ∷ (a → b → Bool) → NonEmpty a → NonEmpty b → Bool #
Ord1 NonEmpty	Since: base-4.10.0.0
Instance details Defined in Data.Functor.Classes Methods liftCompare ∷ (a → b → Ordering) → NonEmpty a → NonEmpty b → Ordering #
Read1 NonEmpty	Since: base-4.10.0.0
Instance details Defined in Data.Functor.Classes Methods liftReadsPrec ∷ (Int → ReadS a) → ReadS [a] → Int → ReadS (NonEmpty a) # liftReadList ∷ (Int → ReadS a) → ReadS [a] → ReadS [NonEmpty a] # liftReadPrec ∷ ReadPrec a → ReadPrec [a] → ReadPrec (NonEmpty a) # liftReadListPrec ∷ ReadPrec a → ReadPrec [a] → ReadPrec [NonEmpty a] #
Show1 NonEmpty	Since: base-4.10.0.0
Instance details Defined in Data.Functor.Classes Methods liftShowsPrec ∷ (Int → a → ShowS) → ([a] → ShowS) → Int → NonEmpty a → ShowS # liftShowList ∷ (Int → a → ShowS) → ([a] → ShowS) → [NonEmpty a] → ShowS #
Traversable NonEmpty	Since: base-4.9.0.0
Instance details Defined in Data.Traversable Methods traverse ∷ Applicative f ⇒ (a → f b) → NonEmpty a → f (NonEmpty b) # sequenceA ∷ Applicative f ⇒ NonEmpty (f a) → f (NonEmpty a) # mapM ∷ Monad m ⇒ (a → m b) → NonEmpty a → m (NonEmpty b) # sequence ∷ Monad m ⇒ NonEmpty (m a) → m (NonEmpty a) #
Applicative NonEmpty	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods pure ∷ a → NonEmpty a # (<>) ∷ NonEmpty (a → b) → NonEmpty a → NonEmpty b # liftA2 ∷ (a → b → c) → NonEmpty a → NonEmpty b → NonEmpty c # (>) ∷ NonEmpty a → NonEmpty b → NonEmpty b # (<*) ∷ NonEmpty a → NonEmpty b → NonEmpty a #
Functor NonEmpty	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods fmap ∷ (a → b) → NonEmpty a → NonEmpty b # (<$) ∷ a → NonEmpty b → NonEmpty a #
Monad NonEmpty	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (>>=) ∷ NonEmpty a → (a → NonEmpty b) → NonEmpty b # (>>) ∷ NonEmpty a → NonEmpty b → NonEmpty b # return ∷ a → NonEmpty a #
NFData1 NonEmpty	Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf ∷ (a → ()) → NonEmpty a → () #
Generic1 NonEmpty
Instance details Defined in GHC.Generics Associated Types type Rep1 NonEmpty ∷ k → Type # Methods from1 ∷ ∀ (a ∷ k). NonEmpty a → Rep1 NonEmpty a # to1 ∷ ∀ (a ∷ k). Rep1 NonEmpty a → NonEmpty a #
Lift a ⇒ Lift (NonEmpty a ∷ Type)	Since: template-haskell-2.15.0.0
Instance details Defined in Language.Haskell.TH.Syntax Methods lift ∷ Quote m ⇒ NonEmpty a → m Exp # liftTyped ∷ ∀ (m ∷ Type → Type). Quote m ⇒ NonEmpty a → Code m (NonEmpty a) #
Arbitrary a ⇒ Arbitrary (NonEmpty a) Source #
Instance details Defined in Constrained.Core Methods arbitrary ∷ Gen (NonEmpty a) Source # shrink ∷ NonEmpty a → [NonEmpty a] Source #
Semigroup (NonEmpty a)	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) ∷ NonEmpty a → NonEmpty a → NonEmpty a # sconcat ∷ NonEmpty (NonEmpty a) → NonEmpty a # stimes ∷ Integral b ⇒ b → NonEmpty a → NonEmpty a #
Generic (NonEmpty a)
Instance details Defined in GHC.Generics Associated Types type Rep (NonEmpty a) ∷ Type → Type # Methods from ∷ NonEmpty a → Rep (NonEmpty a) x # to ∷ Rep (NonEmpty a) x → NonEmpty a #
IsList (NonEmpty a)	Since: base-4.9.0.0
Instance details Defined in GHC.IsList Associated Types type Item (NonEmpty a) # Methods fromList ∷ [Item (NonEmpty a)] → NonEmpty a # fromListN ∷ Int → [Item (NonEmpty a)] → NonEmpty a # toList ∷ NonEmpty a → [Item (NonEmpty a)] #
Read a ⇒ Read (NonEmpty a)	Since: base-4.11.0.0
Instance details Defined in GHC.Read Methods readsPrec ∷ Int → ReadS (NonEmpty a) # readList ∷ ReadS [NonEmpty a] # readPrec ∷ ReadPrec (NonEmpty a) # readListPrec ∷ ReadPrec [NonEmpty a] #
Show a ⇒ Show (NonEmpty a)	Since: base-4.11.0.0
Instance details Defined in GHC.Show Methods showsPrec ∷ Int → NonEmpty a → ShowS # show ∷ NonEmpty a → String # showList ∷ [NonEmpty a] → ShowS #
NFData a ⇒ NFData (NonEmpty a)	Since: deepseq-1.4.2.0
Instance details Defined in Control.DeepSeq Methods rnf ∷ NonEmpty a → () #
Eq a ⇒ Eq (NonEmpty a)	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (==) ∷ NonEmpty a → NonEmpty a → Bool # (/=) ∷ NonEmpty a → NonEmpty a → Bool #
Ord a ⇒ Ord (NonEmpty a)	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods compare ∷ NonEmpty a → NonEmpty a → Ordering # (<) ∷ NonEmpty a → NonEmpty a → Bool # (<=) ∷ NonEmpty a → NonEmpty a → Bool # (>) ∷ NonEmpty a → NonEmpty a → Bool # (>=) ∷ NonEmpty a → NonEmpty a → Bool # max ∷ NonEmpty a → NonEmpty a → NonEmpty a # min ∷ NonEmpty a → NonEmpty a → NonEmpty a #
Pretty a ⇒ Pretty (NonEmpty a)
Instance details Defined in Prettyprinter.Internal Methods pretty ∷ NonEmpty a → Doc ann Source # prettyList ∷ [NonEmpty a] → Doc ann Source #
type Rep1 NonEmpty	Since: base-4.6.0.0
Instance details Defined in GHC.Generics type Rep1 NonEmpty = D1 ('MetaData "NonEmpty" "GHC.Base" "base" 'False) (C1 ('MetaCons ":\|" ('InfixI 'RightAssociative 5) 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1 :*: S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec1 List)))
type Rep (NonEmpty a)	Since: base-4.6.0.0
Instance details Defined in GHC.Generics type Rep (NonEmpty a) = D1 ('MetaData "NonEmpty" "GHC.Base" "base" 'False) (C1 ('MetaCons ":\|" ('InfixI 'RightAssociative 5) 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [a])))
type Item (NonEmpty a)
Instance details Defined in GHC.IsList type Item (NonEmpty a) = a

type Specification = SpecificationD Deps Source #

pattern TypeSpec ∷ () ⇒ HasSpec a ⇒ TypeSpec a → [a] → Specification a Source #

type Term = TermD Deps Source #

data Fun dom rng where Source #

Constructors

Fun ∷ ∀ t dom rng. AppRequires t dom rng ⇒ t dom rng → Fun dom rng

Instances

Instances details

Show (Fun dom r) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → Fun dom r → ShowS # show ∷ Fun dom r → String # showList ∷ [Fun dom r] → ShowS #
Eq (Fun d r) Source #
Instance details Defined in Constrained.Base Methods (==) ∷ Fun d r → Fun d r → Bool # (/=) ∷ Fun d r → Fun d r → Bool #

name ∷ String → Term a → Term a Source #

named ∷ String → Term a → Term a Source #

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

type Pred = PredD Deps Source #

class (Typeable a, Eq a, Show a, TypeSpecEqShow a) ⇒ HasSpec a where Source #

Minimal complete definition

Nothing

Associated Types

type TypeSpec a Source #

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

type TypeSpec a = TypeSpec (SimpleRep a)

type Prerequisites a ∷ Constraint Source #

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

type Prerequisites a = ()

Methods

emptySpec ∷ TypeSpec a Source #

default emptySpec ∷ GenericallyInstantiated a ⇒ TypeSpec a Source #

combineSpec ∷ TypeSpec a → TypeSpec a → Specification a Source #

default combineSpec ∷ GenericallyInstantiated a ⇒ TypeSpec a → TypeSpec a → Specification a Source #

genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a Source #

Generate a value that satisfies the HasSpec. The key property for this generator is soundness: ∀ a ∈ genFromTypeSpec spec. a conformsTo spec

default genFromTypeSpec ∷ (GenericallyInstantiated a, HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a Source #

conformsTo ∷ HasCallStack ⇒ a → TypeSpec a → Bool Source #

Check conformance to the spec.

default conformsTo ∷ (GenericallyInstantiated a, HasCallStack) ⇒ a → TypeSpec a → Bool Source #

shrinkWithTypeSpec ∷ TypeSpec a → a → [a] Source #

Shrink an a with the aide of a HasSpec

default shrinkWithTypeSpec ∷ GenericallyInstantiated a ⇒ TypeSpec a → a → [a] Source #

toPreds ∷ Term a → TypeSpec a → Pred Source #

Convert a spec to predicates: The key property here is: ∀ a. a conformsTo spec == a conformsTo constrained (t -> toPreds t spec)

default toPreds ∷ GenericallyInstantiated a ⇒ Term a → TypeSpec a → Pred Source #

cardinalTypeSpec ∷ TypeSpec a → Specification Integer Source #

Compute an upper and lower bound on the number of solutions genFromTypeSpec might return

default cardinalTypeSpec ∷ GenericallyInstantiated a ⇒ TypeSpec a → Specification Integer Source #

cardinalTrueSpec ∷ Specification 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 a → Maybe (NonEmpty String) Source #

alternateShow ∷ TypeSpec a → BinaryShow Source #

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

typeSpecOpt ∷ TypeSpec a → [a] → Specification 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 a → Specification a Source #

This can be used to detect self inconsistencies in a (TypeSpec t) Note this is similar to typeSpecHasError, and the default value for typeSpecHasError is written in terms of guardTypeSpec Both typeSpecHasError and guardTypeSpec can be set individually.

prerequisites ∷ Evidence (Prerequisites a) Source #

Materialize the Prerequisites dictionary. It should not be necessary to implement this function manually.

default prerequisites ∷ Prerequisites a ⇒ Evidence (Prerequisites a) Source #

Instances

Instances details

HasSpec Int16 Source #
Instance details Defined in Constrained.NumOrd Associated Types type TypeSpec Int16 Source # type Prerequisites Int16 Source # Methods emptySpec ∷ TypeSpec Int16 Source # combineSpec ∷ TypeSpec 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 # shrinkWithTypeSpec ∷ TypeSpec Int16 → Int16 → [Int16] Source # toPreds ∷ Term Int16 → TypeSpec Int16 → Pred Source # cardinalTypeSpec ∷ TypeSpec Int16 → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Int16 → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Int16 → BinaryShow Source # monadConformsTo ∷ Int16 → TypeSpec Int16 → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Int16 → [Int16] → Specification Int16 Source # guardTypeSpec ∷ [String] → TypeSpec Int16 → Specification Int16 Source # prerequisites ∷ Evidence (Prerequisites Int16) Source #
HasSpec Int32 Source #
Instance details Defined in Constrained.NumOrd Associated Types type TypeSpec Int32 Source # type Prerequisites Int32 Source # Methods emptySpec ∷ TypeSpec Int32 Source # combineSpec ∷ TypeSpec 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 # shrinkWithTypeSpec ∷ TypeSpec Int32 → Int32 → [Int32] Source # toPreds ∷ Term Int32 → TypeSpec Int32 → Pred Source # cardinalTypeSpec ∷ TypeSpec Int32 → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Int32 → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Int32 → BinaryShow Source # monadConformsTo ∷ Int32 → TypeSpec Int32 → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Int32 → [Int32] → Specification Int32 Source # guardTypeSpec ∷ [String] → TypeSpec Int32 → Specification Int32 Source # prerequisites ∷ Evidence (Prerequisites Int32) Source #
HasSpec Int64 Source #
Instance details Defined in Constrained.NumOrd Associated Types type TypeSpec Int64 Source # type Prerequisites Int64 Source # Methods emptySpec ∷ TypeSpec Int64 Source # combineSpec ∷ TypeSpec 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 # shrinkWithTypeSpec ∷ TypeSpec Int64 → Int64 → [Int64] Source # toPreds ∷ Term Int64 → TypeSpec Int64 → Pred Source # cardinalTypeSpec ∷ TypeSpec Int64 → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Int64 → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Int64 → BinaryShow Source # monadConformsTo ∷ Int64 → TypeSpec Int64 → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Int64 → [Int64] → Specification Int64 Source # guardTypeSpec ∷ [String] → TypeSpec Int64 → Specification Int64 Source # prerequisites ∷ Evidence (Prerequisites Int64) Source #
HasSpec Int8 Source #
Instance details Defined in Constrained.NumOrd Associated Types type TypeSpec Int8 Source # type Prerequisites Int8 Source # Methods emptySpec ∷ TypeSpec Int8 Source # combineSpec ∷ TypeSpec 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 # shrinkWithTypeSpec ∷ TypeSpec Int8 → Int8 → [Int8] Source # toPreds ∷ Term Int8 → TypeSpec Int8 → Pred Source # cardinalTypeSpec ∷ TypeSpec Int8 → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Int8 → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Int8 → BinaryShow Source # monadConformsTo ∷ Int8 → TypeSpec Int8 → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Int8 → [Int8] → Specification Int8 Source # guardTypeSpec ∷ [String] → TypeSpec Int8 → Specification Int8 Source # prerequisites ∷ Evidence (Prerequisites Int8) Source #
HasSpec Word16 Source #
Instance details Defined in Constrained.NumOrd Associated Types type TypeSpec Word16 Source # type Prerequisites Word16 Source # Methods emptySpec ∷ TypeSpec Word16 Source # combineSpec ∷ TypeSpec 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 # shrinkWithTypeSpec ∷ TypeSpec Word16 → Word16 → [Word16] Source # toPreds ∷ Term Word16 → TypeSpec Word16 → Pred Source # cardinalTypeSpec ∷ TypeSpec Word16 → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Word16 → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Word16 → BinaryShow Source # monadConformsTo ∷ Word16 → TypeSpec Word16 → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Word16 → [Word16] → Specification Word16 Source # guardTypeSpec ∷ [String] → TypeSpec Word16 → Specification Word16 Source # prerequisites ∷ Evidence (Prerequisites Word16) Source #
HasSpec Word32 Source #
Instance details Defined in Constrained.NumOrd Associated Types type TypeSpec Word32 Source # type Prerequisites Word32 Source # Methods emptySpec ∷ TypeSpec Word32 Source # combineSpec ∷ TypeSpec 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 # shrinkWithTypeSpec ∷ TypeSpec Word32 → Word32 → [Word32] Source # toPreds ∷ Term Word32 → TypeSpec Word32 → Pred Source # cardinalTypeSpec ∷ TypeSpec Word32 → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Word32 → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Word32 → BinaryShow Source # monadConformsTo ∷ Word32 → TypeSpec Word32 → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Word32 → [Word32] → Specification Word32 Source # guardTypeSpec ∷ [String] → TypeSpec Word32 → Specification Word32 Source # prerequisites ∷ Evidence (Prerequisites Word32) Source #
HasSpec Word64 Source #
Instance details Defined in Constrained.NumOrd Associated Types type TypeSpec Word64 Source # type Prerequisites Word64 Source # Methods emptySpec ∷ TypeSpec Word64 Source # combineSpec ∷ TypeSpec 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 # shrinkWithTypeSpec ∷ TypeSpec Word64 → Word64 → [Word64] Source # toPreds ∷ Term Word64 → TypeSpec Word64 → Pred Source # cardinalTypeSpec ∷ TypeSpec Word64 → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Word64 → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Word64 → BinaryShow Source # monadConformsTo ∷ Word64 → TypeSpec Word64 → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Word64 → [Word64] → Specification Word64 Source # guardTypeSpec ∷ [String] → TypeSpec Word64 → Specification Word64 Source # prerequisites ∷ Evidence (Prerequisites Word64) Source #
HasSpec Word8 Source #
Instance details Defined in Constrained.NumOrd Associated Types type TypeSpec Word8 Source # type Prerequisites Word8 Source # Methods emptySpec ∷ TypeSpec Word8 Source # combineSpec ∷ TypeSpec 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 # shrinkWithTypeSpec ∷ TypeSpec Word8 → Word8 → [Word8] Source # toPreds ∷ Term Word8 → TypeSpec Word8 → Pred Source # cardinalTypeSpec ∷ TypeSpec Word8 → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Word8 → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Word8 → BinaryShow Source # monadConformsTo ∷ Word8 → TypeSpec Word8 → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Word8 → [Word8] → Specification Word8 Source # guardTypeSpec ∷ [String] → TypeSpec Word8 → Specification Word8 Source # prerequisites ∷ Evidence (Prerequisites Word8) Source #
HasSpec Foo Source #
Instance details Defined in Constrained.Examples.Basic Associated Types type TypeSpec Foo Source # type Prerequisites Foo Source # Methods emptySpec ∷ TypeSpec Foo Source # combineSpec ∷ TypeSpec Foo → TypeSpec Foo → Specification Foo Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Foo → GenT m Foo Source # conformsTo ∷ Foo → TypeSpec Foo → Bool Source # shrinkWithTypeSpec ∷ TypeSpec Foo → Foo → [Foo] Source # toPreds ∷ Term Foo → TypeSpec Foo → Pred Source # cardinalTypeSpec ∷ TypeSpec Foo → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Foo → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Foo → BinaryShow Source # monadConformsTo ∷ Foo → TypeSpec Foo → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Foo → [Foo] → Specification Foo Source # guardTypeSpec ∷ [String] → TypeSpec Foo → Specification Foo Source # prerequisites ∷ Evidence (Prerequisites Foo) Source #
HasSpec Three Source #
Instance details Defined in Constrained.Examples.Basic Associated Types type TypeSpec Three Source # type Prerequisites Three Source # Methods emptySpec ∷ TypeSpec Three Source # combineSpec ∷ TypeSpec Three → TypeSpec Three → Specification Three Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Three → GenT m Three Source # conformsTo ∷ Three → TypeSpec Three → Bool Source # shrinkWithTypeSpec ∷ TypeSpec Three → Three → [Three] Source # toPreds ∷ Term Three → TypeSpec Three → Pred Source # cardinalTypeSpec ∷ TypeSpec Three → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Three → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Three → BinaryShow Source # monadConformsTo ∷ Three → TypeSpec Three → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Three → [Three] → Specification Three Source # guardTypeSpec ∷ [String] → TypeSpec Three → Specification Three Source # prerequisites ∷ Evidence (Prerequisites Three) Source #
HasSpec FooBarBaz Source #
Instance details Defined in Constrained.Examples.CheatSheet Associated Types type TypeSpec FooBarBaz Source # type Prerequisites FooBarBaz Source # Methods emptySpec ∷ TypeSpec FooBarBaz Source # combineSpec ∷ TypeSpec FooBarBaz → TypeSpec FooBarBaz → Specification FooBarBaz Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec FooBarBaz → GenT m FooBarBaz Source # conformsTo ∷ FooBarBaz → TypeSpec FooBarBaz → Bool Source # shrinkWithTypeSpec ∷ TypeSpec FooBarBaz → FooBarBaz → [FooBarBaz] Source # toPreds ∷ Term FooBarBaz → TypeSpec FooBarBaz → Pred Source # cardinalTypeSpec ∷ TypeSpec FooBarBaz → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec FooBarBaz → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec FooBarBaz → BinaryShow Source # monadConformsTo ∷ FooBarBaz → TypeSpec FooBarBaz → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec FooBarBaz → [FooBarBaz] → Specification FooBarBaz Source # guardTypeSpec ∷ [String] → TypeSpec FooBarBaz → Specification FooBarBaz Source # prerequisites ∷ Evidence (Prerequisites FooBarBaz) Source #
HasSpec Coin Source #
Instance details Defined in Constrained.Examples.ManualExamples Associated Types type TypeSpec Coin Source # type Prerequisites Coin Source # Methods emptySpec ∷ TypeSpec Coin Source # combineSpec ∷ TypeSpec Coin → TypeSpec Coin → Specification Coin Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Coin → GenT m Coin Source # conformsTo ∷ Coin → TypeSpec Coin → Bool Source # shrinkWithTypeSpec ∷ TypeSpec Coin → Coin → [Coin] Source # toPreds ∷ Term Coin → TypeSpec Coin → Pred Source # cardinalTypeSpec ∷ TypeSpec Coin → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Coin → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Coin → BinaryShow Source # monadConformsTo ∷ Coin → TypeSpec Coin → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Coin → [Coin] → Specification Coin Source # guardTypeSpec ∷ [String] → TypeSpec Coin → Specification Coin Source # prerequisites ∷ Evidence (Prerequisites Coin) Source #
HasSpec Dimensions Source #
Instance details Defined in Constrained.Examples.ManualExamples Associated Types type TypeSpec Dimensions Source # type Prerequisites Dimensions Source # Methods emptySpec ∷ TypeSpec Dimensions Source # combineSpec ∷ TypeSpec Dimensions → TypeSpec Dimensions → Specification Dimensions Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Dimensions → GenT m Dimensions Source # conformsTo ∷ Dimensions → TypeSpec Dimensions → Bool Source # shrinkWithTypeSpec ∷ TypeSpec Dimensions → Dimensions → [Dimensions] Source # toPreds ∷ Term Dimensions → TypeSpec Dimensions → Pred Source # cardinalTypeSpec ∷ TypeSpec Dimensions → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Dimensions → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Dimensions → BinaryShow Source # monadConformsTo ∷ Dimensions → TypeSpec Dimensions → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Dimensions → [Dimensions] → Specification Dimensions Source # guardTypeSpec ∷ [String] → TypeSpec Dimensions → Specification Dimensions Source # prerequisites ∷ Evidence (Prerequisites Dimensions) Source #
HasSpec Nested Source #
Instance details Defined in Constrained.Examples.ManualExamples Associated Types type TypeSpec Nested Source # type Prerequisites Nested Source # Methods emptySpec ∷ TypeSpec Nested Source # combineSpec ∷ TypeSpec Nested → TypeSpec Nested → Specification Nested Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Nested → GenT m Nested Source # conformsTo ∷ Nested → TypeSpec Nested → Bool Source # shrinkWithTypeSpec ∷ TypeSpec Nested → Nested → [Nested] Source # toPreds ∷ Term Nested → TypeSpec Nested → Pred Source # cardinalTypeSpec ∷ TypeSpec Nested → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Nested → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Nested → BinaryShow Source # monadConformsTo ∷ Nested → TypeSpec Nested → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Nested → [Nested] → Specification Nested Source # guardTypeSpec ∷ [String] → TypeSpec Nested → Specification Nested Source # prerequisites ∷ Evidence (Prerequisites Nested) Source #
HasSpec Rectangle Source #
Instance details Defined in Constrained.Examples.ManualExamples Associated Types type TypeSpec Rectangle Source # type Prerequisites Rectangle Source # Methods emptySpec ∷ TypeSpec Rectangle Source # combineSpec ∷ TypeSpec Rectangle → TypeSpec Rectangle → Specification Rectangle Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Rectangle → GenT m Rectangle Source # conformsTo ∷ Rectangle → TypeSpec Rectangle → Bool Source # shrinkWithTypeSpec ∷ TypeSpec Rectangle → Rectangle → [Rectangle] Source # toPreds ∷ Term Rectangle → TypeSpec Rectangle → Pred Source # cardinalTypeSpec ∷ TypeSpec Rectangle → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Rectangle → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Rectangle → BinaryShow Source # monadConformsTo ∷ Rectangle → TypeSpec Rectangle → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Rectangle → [Rectangle] → Specification Rectangle Source # guardTypeSpec ∷ [String] → TypeSpec Rectangle → Specification Rectangle Source # prerequisites ∷ Evidence (Prerequisites Rectangle) Source #
HasSpec Three Source #
Instance details Defined in Constrained.Examples.ManualExamples Associated Types type TypeSpec Three Source # type Prerequisites Three Source # Methods emptySpec ∷ TypeSpec Three Source # combineSpec ∷ TypeSpec Three → TypeSpec Three → Specification Three Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Three → GenT m Three Source # conformsTo ∷ Three → TypeSpec Three → Bool Source # shrinkWithTypeSpec ∷ TypeSpec Three → Three → [Three] Source # toPreds ∷ Term Three → TypeSpec Three → Pred Source # cardinalTypeSpec ∷ TypeSpec Three → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Three → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Three → BinaryShow Source # monadConformsTo ∷ Three → TypeSpec Three → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Three → [Three] → Specification Three Source # guardTypeSpec ∷ [String] → TypeSpec Three → Specification Three Source # prerequisites ∷ Evidence (Prerequisites Three) Source #
HasSpec Integer Source #
Instance details Defined in Constrained.NumOrd Associated Types type TypeSpec Integer Source # type Prerequisites Integer Source # Methods emptySpec ∷ TypeSpec Integer Source # combineSpec ∷ TypeSpec 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 # shrinkWithTypeSpec ∷ TypeSpec Integer → Integer → [Integer] Source # toPreds ∷ Term Integer → TypeSpec Integer → Pred Source # cardinalTypeSpec ∷ TypeSpec Integer → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Integer → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Integer → BinaryShow Source # monadConformsTo ∷ Integer → TypeSpec Integer → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Integer → [Integer] → Specification Integer Source # guardTypeSpec ∷ [String] → TypeSpec Integer → Specification Integer Source # prerequisites ∷ Evidence (Prerequisites Integer) Source #
HasSpec Natural Source #
Instance details Defined in Constrained.NumOrd Associated Types type TypeSpec Natural Source # type Prerequisites Natural Source # Methods emptySpec ∷ TypeSpec Natural Source # combineSpec ∷ TypeSpec 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 # shrinkWithTypeSpec ∷ TypeSpec Natural → Natural → [Natural] Source # toPreds ∷ Term Natural → TypeSpec Natural → Pred Source # cardinalTypeSpec ∷ TypeSpec Natural → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Natural → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Natural → BinaryShow Source # monadConformsTo ∷ Natural → TypeSpec Natural → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Natural → [Natural] → Specification Natural Source # guardTypeSpec ∷ [String] → TypeSpec Natural → Specification Natural Source # prerequisites ∷ Evidence (Prerequisites Natural) Source #
HasSpec () Source #
Instance details Defined in Constrained.Base Associated Types type TypeSpec () Source # type Prerequisites () Source # Methods emptySpec ∷ TypeSpec () Source # combineSpec ∷ TypeSpec () → TypeSpec () → Specification () Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec () → GenT m () Source # conformsTo ∷ () → TypeSpec () → Bool Source # shrinkWithTypeSpec ∷ TypeSpec () → () → [()] Source # toPreds ∷ Term () → TypeSpec () → Pred Source # cardinalTypeSpec ∷ TypeSpec () → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec () → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec () → BinaryShow Source # monadConformsTo ∷ () → TypeSpec () → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec () → [()] → Specification () Source # guardTypeSpec ∷ [String] → TypeSpec () → Specification () Source # prerequisites ∷ Evidence (Prerequisites ()) Source #
HasSpec Bool Source #	NOTE: this instance means we have to use `ifElse`, `whenTrue`, and `whenFalse` instead of `caseOn` for `Bool`
Instance details Defined in Constrained.Base Associated Types type TypeSpec Bool Source # type Prerequisites Bool Source # Methods emptySpec ∷ TypeSpec Bool Source # combineSpec ∷ TypeSpec 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 # shrinkWithTypeSpec ∷ TypeSpec Bool → Bool → [Bool] Source # toPreds ∷ Term Bool → TypeSpec Bool → Pred Source # cardinalTypeSpec ∷ TypeSpec Bool → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Bool → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Bool → BinaryShow Source # monadConformsTo ∷ Bool → TypeSpec Bool → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Bool → [Bool] → Specification Bool Source # guardTypeSpec ∷ [String] → TypeSpec Bool → Specification Bool Source # prerequisites ∷ Evidence (Prerequisites Bool) Source #
HasSpec Float Source #
Instance details Defined in Constrained.NumOrd Associated Types type TypeSpec Float Source # type Prerequisites Float Source # Methods emptySpec ∷ TypeSpec Float Source # combineSpec ∷ TypeSpec 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 # shrinkWithTypeSpec ∷ TypeSpec Float → Float → [Float] Source # toPreds ∷ Term Float → TypeSpec Float → Pred Source # cardinalTypeSpec ∷ TypeSpec Float → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Float → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Float → BinaryShow Source # monadConformsTo ∷ Float → TypeSpec Float → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Float → [Float] → Specification Float Source # guardTypeSpec ∷ [String] → TypeSpec Float → Specification Float Source # prerequisites ∷ Evidence (Prerequisites Float) Source #
HasSpec Int Source #
Instance details Defined in Constrained.NumOrd Associated Types type TypeSpec Int Source # type Prerequisites Int Source # Methods emptySpec ∷ TypeSpec Int Source # combineSpec ∷ TypeSpec 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 # shrinkWithTypeSpec ∷ TypeSpec Int → Int → [Int] Source # toPreds ∷ Term Int → TypeSpec Int → Pred Source # cardinalTypeSpec ∷ TypeSpec Int → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Int → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Int → BinaryShow Source # monadConformsTo ∷ Int → TypeSpec Int → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Int → [Int] → Specification Int Source # guardTypeSpec ∷ [String] → TypeSpec Int → Specification Int Source # prerequisites ∷ Evidence (Prerequisites Int) Source #
HasSpec (Ratio Integer) Source #
Instance details Defined in Constrained.NumOrd Associated Types type TypeSpec (Ratio Integer) Source # type Prerequisites (Ratio Integer) Source # Methods emptySpec ∷ TypeSpec (Ratio Integer) Source # combineSpec ∷ TypeSpec (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 # shrinkWithTypeSpec ∷ TypeSpec (Ratio Integer) → Ratio Integer → [Ratio Integer] Source # toPreds ∷ Term (Ratio Integer) → TypeSpec (Ratio Integer) → Pred Source # cardinalTypeSpec ∷ TypeSpec (Ratio Integer) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (Ratio Integer) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (Ratio Integer) → BinaryShow Source # monadConformsTo ∷ Ratio Integer → TypeSpec (Ratio Integer) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (Ratio Integer) → [Ratio Integer] → Specification (Ratio Integer) Source # guardTypeSpec ∷ [String] → TypeSpec (Ratio Integer) → Specification (Ratio Integer) Source # prerequisites ∷ Evidence (Prerequisites (Ratio Integer)) Source #
(Ord a, HasSpec a) ⇒ HasSpec (NotASet a) Source #
Instance details Defined in Constrained.Examples.Set Associated Types type TypeSpec (NotASet a) Source # type Prerequisites (NotASet a) Source # Methods emptySpec ∷ TypeSpec (NotASet a) Source # combineSpec ∷ TypeSpec (NotASet a) → TypeSpec (NotASet a) → Specification (NotASet a) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (NotASet a) → GenT m (NotASet a) Source # conformsTo ∷ NotASet a → TypeSpec (NotASet a) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (NotASet a) → NotASet a → [NotASet a] Source # toPreds ∷ Term (NotASet a) → TypeSpec (NotASet a) → Pred Source # cardinalTypeSpec ∷ TypeSpec (NotASet a) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (NotASet a) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (NotASet a) → BinaryShow Source # monadConformsTo ∷ NotASet a → TypeSpec (NotASet a) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (NotASet a) → [NotASet a] → Specification (NotASet a) Source # guardTypeSpec ∷ [String] → TypeSpec (NotASet a) → Specification (NotASet a) Source # prerequisites ∷ Evidence (Prerequisites (NotASet a)) Source #
HasSpec a ⇒ HasSpec (BinTree a) Source #
Instance details Defined in Constrained.Spec.Tree Associated Types type TypeSpec (BinTree a) Source # type Prerequisites (BinTree a) Source # Methods emptySpec ∷ TypeSpec (BinTree a) Source # combineSpec ∷ TypeSpec (BinTree a) → TypeSpec (BinTree a) → Specification (BinTree a) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (BinTree a) → GenT m (BinTree a) Source # conformsTo ∷ BinTree a → TypeSpec (BinTree a) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (BinTree a) → BinTree a → [BinTree a] Source # toPreds ∷ Term (BinTree a) → TypeSpec (BinTree a) → Pred Source # cardinalTypeSpec ∷ TypeSpec (BinTree a) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (BinTree a) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (BinTree a) → BinaryShow Source # monadConformsTo ∷ BinTree a → TypeSpec (BinTree a) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (BinTree a) → [BinTree a] → Specification (BinTree a) Source # guardTypeSpec ∷ [String] → TypeSpec (BinTree a) → Specification (BinTree a) Source # prerequisites ∷ Evidence (Prerequisites (BinTree a)) Source #
(Ord a, HasSpec a) ⇒ HasSpec (Set a) Source #
Instance details Defined in Constrained.Spec.Set Associated Types type TypeSpec (Set a) Source # type Prerequisites (Set a) Source # Methods emptySpec ∷ TypeSpec (Set a) Source # combineSpec ∷ TypeSpec (Set a) → TypeSpec (Set a) → Specification (Set a) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (Set a) → GenT m (Set a) Source # conformsTo ∷ Set a → TypeSpec (Set a) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (Set a) → Set a → [Set a] Source # toPreds ∷ Term (Set a) → TypeSpec (Set a) → Pred Source # cardinalTypeSpec ∷ TypeSpec (Set a) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (Set a) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (Set a) → BinaryShow Source # monadConformsTo ∷ Set a → TypeSpec (Set a) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (Set a) → [Set a] → Specification (Set a) Source # guardTypeSpec ∷ [String] → TypeSpec (Set a) → Specification (Set a) Source # prerequisites ∷ Evidence (Prerequisites (Set a)) Source #
HasSpec a ⇒ HasSpec (Tree a) Source #
Instance details Defined in Constrained.Spec.Tree Associated Types type TypeSpec (Tree a) Source # type Prerequisites (Tree a) Source # Methods emptySpec ∷ TypeSpec (Tree a) Source # combineSpec ∷ TypeSpec (Tree a) → TypeSpec (Tree a) → Specification (Tree a) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (Tree a) → GenT m (Tree a) Source # conformsTo ∷ Tree a → TypeSpec (Tree a) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (Tree a) → Tree a → [Tree a] Source # toPreds ∷ Term (Tree a) → TypeSpec (Tree a) → Pred Source # cardinalTypeSpec ∷ TypeSpec (Tree a) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (Tree a) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (Tree a) → BinaryShow Source # monadConformsTo ∷ Tree a → TypeSpec (Tree a) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (Tree a) → [Tree a] → Specification (Tree a) Source # guardTypeSpec ∷ [String] → TypeSpec (Tree a) → Specification (Tree a) Source # prerequisites ∷ Evidence (Prerequisites (Tree a)) Source #
(IsNormalType a, HasSpec a) ⇒ HasSpec (Maybe a) Source #
Instance details Defined in Constrained.Spec.SumProd Associated Types type TypeSpec (Maybe a) Source # type Prerequisites (Maybe a) Source # Methods emptySpec ∷ TypeSpec (Maybe a) Source # combineSpec ∷ TypeSpec (Maybe a) → TypeSpec (Maybe a) → Specification (Maybe a) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (Maybe a) → GenT m (Maybe a) Source # conformsTo ∷ Maybe a → TypeSpec (Maybe a) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (Maybe a) → Maybe a → [Maybe a] Source # toPreds ∷ Term (Maybe a) → TypeSpec (Maybe a) → Pred Source # cardinalTypeSpec ∷ TypeSpec (Maybe a) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (Maybe a) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (Maybe a) → BinaryShow Source # monadConformsTo ∷ Maybe a → TypeSpec (Maybe a) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (Maybe a) → [Maybe a] → Specification (Maybe a) Source # guardTypeSpec ∷ [String] → TypeSpec (Maybe a) → Specification (Maybe a) Source # prerequisites ∷ Evidence (Prerequisites (Maybe a)) Source #
(Sized [a], HasSpec a) ⇒ HasSpec [a] Source #
Instance details Defined in Constrained.TheKnot Associated Types type TypeSpec [a] Source # type Prerequisites [a] Source # Methods emptySpec ∷ TypeSpec [a] Source # combineSpec ∷ TypeSpec [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 # shrinkWithTypeSpec ∷ TypeSpec [a] → [a] → [[a]] Source # toPreds ∷ Term [a] → TypeSpec [a] → Pred Source # cardinalTypeSpec ∷ TypeSpec [a] → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec [a] → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec [a] → BinaryShow Source # monadConformsTo ∷ [a] → TypeSpec [a] → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec [a] → [[a]] → Specification [a] Source # guardTypeSpec ∷ [String] → TypeSpec [a] → Specification [a] Source # prerequisites ∷ Evidence (Prerequisites [a]) Source #
(HasSpec a, IsNormalType a, HasSpec b, IsNormalType b) ⇒ HasSpec (Either a b) Source #
Instance details Defined in Constrained.Spec.SumProd Associated Types type TypeSpec (Either a b) Source # type Prerequisites (Either a b) Source # Methods emptySpec ∷ TypeSpec (Either a b) Source # combineSpec ∷ TypeSpec (Either a b) → TypeSpec (Either a b) → Specification (Either a b) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (Either a b) → GenT m (Either a b) Source # conformsTo ∷ Either a b → TypeSpec (Either a b) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (Either a b) → Either a b → [Either a b] Source # toPreds ∷ Term (Either a b) → TypeSpec (Either a b) → Pred Source # cardinalTypeSpec ∷ TypeSpec (Either a b) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (Either a b) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (Either a b) → BinaryShow Source # monadConformsTo ∷ Either a b → TypeSpec (Either a b) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (Either a b) → [Either a b] → Specification (Either a b) Source # guardTypeSpec ∷ [String] → TypeSpec (Either a b) → Specification (Either a b) Source # prerequisites ∷ Evidence (Prerequisites (Either a b)) Source #
(HasSpec a, HasSpec b) ⇒ HasSpec (Prod a b) Source #
Instance details Defined in Constrained.TheKnot Associated Types type TypeSpec (Prod a b) Source # type Prerequisites (Prod a b) Source # Methods emptySpec ∷ TypeSpec (Prod a b) Source # combineSpec ∷ TypeSpec (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 # conformsTo ∷ Prod a b → TypeSpec (Prod a b) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (Prod a b) → Prod a b → [Prod a b] Source # toPreds ∷ Term (Prod a b) → TypeSpec (Prod a b) → Pred Source # cardinalTypeSpec ∷ TypeSpec (Prod a b) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (Prod a b) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (Prod a b) → BinaryShow Source # monadConformsTo ∷ Prod a b → TypeSpec (Prod a b) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (Prod a b) → [Prod a b] → Specification (Prod a b) Source # guardTypeSpec ∷ [String] → TypeSpec (Prod a b) → Specification (Prod a b) Source # prerequisites ∷ Evidence (Prerequisites (Prod a b)) Source #
(HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ HasSpec (Sum a b) Source #	The HasSpec Sum instance
Instance details Defined in Constrained.Generation Associated Types type TypeSpec (Sum a b) Source # type Prerequisites (Sum a b) Source # Methods emptySpec ∷ TypeSpec (Sum a b) Source # combineSpec ∷ TypeSpec (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 # conformsTo ∷ Sum a b → TypeSpec (Sum a b) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (Sum a b) → Sum a b → [Sum a b] Source # toPreds ∷ Term (Sum a b) → TypeSpec (Sum a b) → Pred Source # cardinalTypeSpec ∷ TypeSpec (Sum a b) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (Sum a b) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (Sum a b) → BinaryShow Source # monadConformsTo ∷ Sum a b → TypeSpec (Sum a b) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (Sum a b) → [Sum a b] → Specification (Sum a b) Source # guardTypeSpec ∷ [String] → TypeSpec (Sum a b) → Specification (Sum a b) Source # prerequisites ∷ Evidence (Prerequisites (Sum a b)) Source #
(Ord k, HasSpec (Prod k v), HasSpec k, HasSpec v, HasSpec [v], IsNormalType k, IsNormalType v) ⇒ HasSpec (Map k v) Source #
Instance details Defined in Constrained.Spec.Map Associated Types type TypeSpec (Map k v) Source # type Prerequisites (Map k v) Source # Methods emptySpec ∷ TypeSpec (Map k v) Source # combineSpec ∷ TypeSpec (Map k v) → TypeSpec (Map k v) → Specification (Map k v) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (Map k v) → GenT m (Map k v) Source # conformsTo ∷ Map k v → TypeSpec (Map k v) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (Map k v) → Map k v → [Map k v] Source # toPreds ∷ Term (Map k v) → TypeSpec (Map k v) → Pred Source # cardinalTypeSpec ∷ TypeSpec (Map k v) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (Map k v) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (Map k v) → BinaryShow Source # monadConformsTo ∷ Map k v → TypeSpec (Map k v) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (Map k v) → [Map k v] → Specification (Map k v) Source # guardTypeSpec ∷ [String] → TypeSpec (Map k v) → Specification (Map k v) Source # prerequisites ∷ Evidence (Prerequisites (Map k v)) Source #
(HasSpec a, HasSpec b) ⇒ HasSpec (a, b) Source #
Instance details Defined in Constrained.Spec.SumProd Associated Types type TypeSpec (a, b) Source # type Prerequisites (a, b) Source # Methods emptySpec ∷ TypeSpec (a, b) Source # combineSpec ∷ TypeSpec (a, b) → TypeSpec (a, b) → Specification (a, b) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (a, b) → GenT m (a, b) Source # conformsTo ∷ (a, b) → TypeSpec (a, b) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (a, b) → (a, b) → [(a, b)] Source # toPreds ∷ Term (a, b) → TypeSpec (a, b) → Pred Source # cardinalTypeSpec ∷ TypeSpec (a, b) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (a, b) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (a, b) → BinaryShow Source # monadConformsTo ∷ (a, b) → TypeSpec (a, b) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (a, b) → [(a, b)] → Specification (a, b) Source # guardTypeSpec ∷ [String] → TypeSpec (a, b) → Specification (a, b) Source # prerequisites ∷ Evidence (Prerequisites (a, b)) Source #
(HasSpec a, HasSpec b, HasSpec c) ⇒ HasSpec (a, b, c) Source #
Instance details Defined in Constrained.Spec.SumProd Associated Types type TypeSpec (a, b, c) Source # type Prerequisites (a, b, c) Source # Methods emptySpec ∷ TypeSpec (a, b, c) Source # combineSpec ∷ TypeSpec (a, b, c) → TypeSpec (a, b, c) → Specification (a, b, c) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (a, b, c) → GenT m (a, b, c) Source # conformsTo ∷ (a, b, c) → TypeSpec (a, b, c) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (a, b, c) → (a, b, c) → [(a, b, c)] Source # toPreds ∷ Term (a, b, c) → TypeSpec (a, b, c) → Pred Source # cardinalTypeSpec ∷ TypeSpec (a, b, c) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (a, b, c) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (a, b, c) → BinaryShow Source # monadConformsTo ∷ (a, b, c) → TypeSpec (a, b, c) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (a, b, c) → [(a, b, c)] → Specification (a, b, c) Source # guardTypeSpec ∷ [String] → TypeSpec (a, b, c) → Specification (a, b, c) Source # prerequisites ∷ Evidence (Prerequisites (a, b, c)) Source #
(HasSpec a, HasSpec b, HasSpec c, HasSpec d) ⇒ HasSpec (a, b, c, d) Source #
Instance details Defined in Constrained.Spec.SumProd Associated Types type TypeSpec (a, b, c, d) Source # type Prerequisites (a, b, c, d) Source # Methods emptySpec ∷ TypeSpec (a, b, c, d) Source # combineSpec ∷ TypeSpec (a, b, c, d) → TypeSpec (a, b, c, d) → Specification (a, b, c, d) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (a, b, c, d) → GenT m (a, b, c, d) Source # conformsTo ∷ (a, b, c, d) → TypeSpec (a, b, c, d) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (a, b, c, d) → (a, b, c, d) → [(a, b, c, d)] Source # toPreds ∷ Term (a, b, c, d) → TypeSpec (a, b, c, d) → Pred Source # cardinalTypeSpec ∷ TypeSpec (a, b, c, d) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (a, b, c, d) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (a, b, c, d) → BinaryShow Source # monadConformsTo ∷ (a, b, c, d) → TypeSpec (a, b, c, d) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (a, b, c, d) → [(a, b, c, d)] → Specification (a, b, c, d) Source # guardTypeSpec ∷ [String] → TypeSpec (a, b, c, d) → Specification (a, b, c, d) Source # prerequisites ∷ Evidence (Prerequisites (a, b, c, d)) Source #
(HasSpec a, HasSpec b, HasSpec c, HasSpec d, HasSpec e) ⇒ HasSpec (a, b, c, d, e) Source #
Instance details Defined in Constrained.Spec.SumProd Associated Types type TypeSpec (a, b, c, d, e) Source # type Prerequisites (a, b, c, d, e) Source # Methods emptySpec ∷ TypeSpec (a, b, c, d, e) Source # combineSpec ∷ TypeSpec (a, b, c, d, e) → TypeSpec (a, b, c, d, e) → Specification (a, b, c, d, e) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (a, b, c, d, e) → GenT m (a, b, c, d, e) Source # conformsTo ∷ (a, b, c, d, e) → TypeSpec (a, b, c, d, e) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (a, b, c, d, e) → (a, b, c, d, e) → [(a, b, c, d, e)] Source # toPreds ∷ Term (a, b, c, d, e) → TypeSpec (a, b, c, d, e) → Pred Source # cardinalTypeSpec ∷ TypeSpec (a, b, c, d, e) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (a, b, c, d, e) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (a, b, c, d, e) → BinaryShow Source # monadConformsTo ∷ (a, b, c, d, e) → TypeSpec (a, b, c, d, e) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (a, b, c, d, e) → [(a, b, c, d, e)] → Specification (a, b, c, d, e) Source # guardTypeSpec ∷ [String] → TypeSpec (a, b, c, d, e) → Specification (a, b, c, d, e) Source # prerequisites ∷ Evidence (Prerequisites (a, b, c, d, e)) Source #
(HasSpec a, HasSpec b, HasSpec c, HasSpec d, HasSpec e, HasSpec g) ⇒ HasSpec (a, b, c, d, e, g) Source #
Instance details Defined in Constrained.Spec.SumProd Associated Types type TypeSpec (a, b, c, d, e, g) Source # type Prerequisites (a, b, c, d, e, g) Source # Methods emptySpec ∷ TypeSpec (a, b, c, d, e, g) Source # combineSpec ∷ TypeSpec (a, b, c, d, e, g) → TypeSpec (a, b, c, d, e, g) → Specification (a, b, c, d, e, g) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (a, b, c, d, e, g) → GenT m (a, b, c, d, e, g) Source # conformsTo ∷ (a, b, c, d, e, g) → TypeSpec (a, b, c, d, e, g) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (a, b, c, d, e, g) → (a, b, c, d, e, g) → [(a, b, c, d, e, g)] Source # toPreds ∷ Term (a, b, c, d, e, g) → TypeSpec (a, b, c, d, e, g) → Pred Source # cardinalTypeSpec ∷ TypeSpec (a, b, c, d, e, g) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (a, b, c, d, e, g) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (a, b, c, d, e, g) → BinaryShow Source # monadConformsTo ∷ (a, b, c, d, e, g) → TypeSpec (a, b, c, d, e, g) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (a, b, c, d, e, g) → [(a, b, c, d, e, g)] → Specification (a, b, c, d, e, g) Source # guardTypeSpec ∷ [String] → TypeSpec (a, b, c, d, e, g) → Specification (a, b, c, d, e, g) Source # prerequisites ∷ Evidence (Prerequisites (a, b, c, d, e, g)) Source #
(HasSpec a, HasSpec b, HasSpec c, HasSpec d, HasSpec e, HasSpec g, HasSpec h) ⇒ HasSpec (a, b, c, d, e, g, h) Source #
Instance details Defined in Constrained.Spec.SumProd Associated Types type TypeSpec (a, b, c, d, e, g, h) Source # type Prerequisites (a, b, c, d, e, g, h) Source # Methods emptySpec ∷ TypeSpec (a, b, c, d, e, g, h) Source # combineSpec ∷ TypeSpec (a, b, c, d, e, g, h) → TypeSpec (a, b, c, d, e, g, h) → Specification (a, b, c, d, e, g, h) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (a, b, c, d, e, g, h) → GenT m (a, b, c, d, e, g, h) Source # conformsTo ∷ (a, b, c, d, e, g, h) → TypeSpec (a, b, c, d, e, g, h) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (a, b, c, d, e, g, h) → (a, b, c, d, e, g, h) → [(a, b, c, d, e, g, h)] Source # toPreds ∷ Term (a, b, c, d, e, g, h) → TypeSpec (a, b, c, d, e, g, h) → Pred Source # cardinalTypeSpec ∷ TypeSpec (a, b, c, d, e, g, h) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (a, b, c, d, e, g, h) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (a, b, c, d, e, g, h) → BinaryShow Source # monadConformsTo ∷ (a, b, c, d, e, g, h) → TypeSpec (a, b, c, d, e, g, h) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (a, b, c, d, e, g, h) → [(a, b, c, d, e, g, h)] → Specification (a, b, c, d, e, g, h) Source # guardTypeSpec ∷ [String] → TypeSpec (a, b, c, d, e, g, h) → Specification (a, b, c, d, e, g, h) Source # prerequisites ∷ Evidence (Prerequisites (a, b, c, d, e, g, h)) Source #

class Typeable (SimpleRep a) ⇒ HasSimpleRep a where Source #

Minimal complete definition

Nothing

Associated Types

type SimpleRep a Source #

type SimpleRep a = SOP (TheSop a)

type TheSop a ∷ [Type] Source #

type TheSop a = SOPOf (Rep a)

Methods

toSimpleRep ∷ a → SimpleRep a Source #

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

fromSimpleRep ∷ SimpleRep a → a Source #

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

Instances

Instances details

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

class (Ord a, HasSpec a) ⇒ OrdLike a where Source #

Minimal complete definition

Nothing

Methods

leqSpec ∷ a → Specification a Source #

default leqSpec ∷ (GenericRequires a, OrdLike (SimpleRep a)) ⇒ a → Specification a Source #

ltSpec ∷ a → Specification a Source #

default ltSpec ∷ (OrdLike (SimpleRep a), GenericRequires a) ⇒ a → Specification a Source #

geqSpec ∷ a → Specification a Source #

default geqSpec ∷ (OrdLike (SimpleRep a), GenericRequires a) ⇒ a → Specification a Source #

gtSpec ∷ a → Specification a Source #

default gtSpec ∷ (OrdLike (SimpleRep a), GenericRequires a) ⇒ a → Specification a Source #

Instances

Instances details

(Ord a, HasSpec a, MaybeBounded a, Num a, TypeSpec a ~ NumSpec a) ⇒ OrdLike a Source #	This instance should be general enough for every type of Number that has a NumSpec as its TypeSpec
Instance details Defined in Constrained.NumOrd Methods leqSpec ∷ a → Specification a Source # ltSpec ∷ a → Specification a Source # geqSpec ∷ a → Specification a Source # gtSpec ∷ a → Specification a Source #

conformsToSpecE ∷ ∀ a. HasSpec a ⇒ a → Specification a → NonEmpty String → Maybe (NonEmpty String) Source #

conformsToSpec with explanation. Nothing if (conformsToSpec a spec), but (Just explanations) if not(conformsToSpec a spec).

conformsToSpec ∷ HasSpec a ⇒ a → Specification a → Bool Source #

satisfies ∷ ∀ a. HasSpec a ⇒ Term a → Specification a → Pred Source #

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

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

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

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

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

cardinality ∷ ∀ a. (Number Integer, HasSpec a) ⇒ Specification a → Specification 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 Integer) to (Specification Integer)

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 #

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

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

assertExplain ∷ IsPred p ⇒ NonEmpty String → p → Pred Source #

assert ∷ IsPred p ⇒ p → Pred Source #

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

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

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

letBind ∷ (HasSpec a, IsPred p) ⇒ Term a → (Term a → p) → Pred Source #

reify ∷ (HasSpec a, HasSpec b, IsPred p) ⇒ Term a → (a → b) → (Term b → p) → Pred Source #

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

explanation ∷ NonEmpty String → Pred → Pred Source #

Wrap an Explain around a Pred, unless there is a simpler form.

monitor ∷ ((∀ a. Term a → a) → Property → Property) → Pred 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.

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

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

lit ∷ HasSpec a ⇒ a → Term a Source #

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

giveHint ∷ HasGenHint a ⇒ Hint a → Specification a 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 #

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

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

not_ ∷ Term Bool → Term Bool Source #

or_ ∷ Term Bool → Term Bool → Term Bool Source #

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

toGeneric_ ∷ ∀ a. GenericRequires a ⇒ Term a → Term (SimpleRep a) Source #

fromGeneric_ ∷ ∀ a. (GenericRequires a, AppRequires BaseW '[SimpleRep a] a) ⇒ Term (SimpleRep a) → Term a Source #

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

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

negate_ ∷ NumLike a ⇒ Term a → Term a Source #

addFn ∷ ∀ a. NumLike a ⇒ Term a → Term a → Term a Source #

negateFn ∷ ∀ a. NumLike a ⇒ Term a → Term a Source #

type Numeric a = (HasSpec a, Ord a, Num a, TypeSpec a ~ NumSpec a, MaybeBounded a) Source #

pair_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term b → Term (a, b) Source #

fst_ ∷ (HasSpec x, HasSpec y) ⇒ Term (x, y) → Term x Source #

snd_ ∷ (HasSpec x, HasSpec y) ⇒ Term (x, y) → Term y Source #

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

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

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

type IsNormalType a = (AssertComputes (Cases a) (Text "Failed to compute Cases in a use of IsNormalType for " :$$: (ShowType a :<>: Text ", are you missing an IsNormalType constraint?")), Cases a ~ '[a], AssertComputes (Args a) ((Text "Failed to compute Args in a use of IsNormalType for " :<>: ShowType a) :<>: Text ", are you missing an IsNormalType constraint?"), Args a ~ '[a], IsProd a, CountCases a ~ 1) Source #

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 #

left_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term (Either a b) Source #

right_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term b → Term (Either a b) Source #

cJust_ ∷ (HasSpec a, IsNormalType a) ⇒ Term a → Term (Maybe a) Source #

cNothing_ ∷ (HasSpec a, IsNormalType a) ⇒ Term (Maybe a) Source #

caseOn ∷ ∀ a. (GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) ⇒ Term a → FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred Source #

branch ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ FunTy (MapList Term (Args a)) p → Weighted Binder a Source #

branchW ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ Int → FunTy (MapList Term (Args a)) p → Weighted Binder a Source #

forAll' ∷ ∀ t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t, HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a), IsProductType a, HasSpec a, GenericRequires a, ProdAsListComputes a) ⇒ Term t → FunTy (MapList Term (ProductAsList a)) p → Pred Source #

Like forAll but pattern matches on the `Term a`

constrained' ∷ ∀ a p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p, GenericRequires a, ProdAsListComputes a) ⇒ FunTy (MapList Term (ProductAsList a)) p → Specification a Source #

Like constrained but pattern matches on the bound `Term a`

reify' ∷ ∀ a b p. (Cases (SimpleRep b) ~ '[SimpleRep b], TypeSpec b ~ TypeSpec (SimpleRep b), HasSpec (SimpleRep b), HasSimpleRep b, All HasSpec (Args (SimpleRep b)), IsProd (SimpleRep b), HasSpec a, HasSpec b, IsProductType b, IsProd a, IsPred p, GenericRequires b, ProdAsListComputes b) ⇒ Term a → (a → b) → FunTy (MapList Term (ProductAsList b)) p → Pred Source #

Like reify but pattern matches on the bound `Term b`

con ∷ ∀ c a r. (SimpleRep a ~ SOP (TheSop a), TypeSpec a ~ TypeSpec (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a), ResultType r ~ Term a, SOPTerm c (TheSop a), ConstrTerm (ConstrOf c (TheSop a)), GenericRequires a) ⇒ r Source #

onCon ∷ ∀ c a p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All HasSpec (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term a → FunTy (MapList Term (ConstrOf c (TheSop a))) p → Pred Source #

isCon ∷ ∀ c a. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), GenericRequires a) ⇒ Term a → Pred Source #

sel ∷ ∀ n a c as. (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a, HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) ⇒ Term a → Term (At n as) Source #

match ∷ ∀ p a. (IsProductType a, IsPred p, GenericRequires a, ProdAsListComputes a) ⇒ Term a → FunTy (MapList Term (ProductAsList a)) p → Pred Source #

onJust ∷ ∀ a p. (HasSpec a, IsNormalType a, IsPred p) ⇒ Term (Maybe a) → (Term a → p) → Pred Source #

isJust ∷ ∀ a. (HasSpec a, IsNormalType a) ⇒ Term (Maybe a) → Pred Source #

chooseSpec ∷ HasSpec a ⇒ (Int, Specification a) → (Int, Specification a) → Specification a Source #

ChooseSpec is one of the ways we can Or two Specs together This works for any kind of type that has a HasSpec instance. If your type is a Sum type. One can use CaseOn which is much easier.

equalSpec ∷ a → Specification a Source #

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

notMemberSpec ∷ ∀ a f. (HasSpec a, Foldable f) ⇒ f a → Specification a 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 #

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

sum_ ∷ Foldy a ⇒ Term [a] → Term a Source #

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

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

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

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

sizeOf ∷ Sized t ⇒ t → Integer Source #

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

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

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

rangeSize ∷ Integer → Integer → SizeSpec Source #

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

genFromSizeSpec ∷ MonadGenError 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

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

maxSpec ∷ Specification Integer → Specification Integer Source #

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

data SetW (d ∷ [Type]) (r ∷ Type) where Source #

Constructors

SingletonW ∷ (HasSpec a, Ord a) ⇒ SetW '[a] (Set a)
UnionW ∷ (HasSpec a, Ord a) ⇒ SetW '[Set a, Set a] (Set a)
SubsetW ∷ (HasSpec a, Ord a, HasSpec a) ⇒ SetW '[Set a, Set a] Bool
MemberW ∷ (HasSpec a, Ord a) ⇒ SetW '[a, Set a] Bool
DisjointW ∷ (HasSpec a, Ord a) ⇒ SetW '[Set a, Set a] Bool
FromListW ∷ (HasSpec a, Ord a) ⇒ SetW '[[a]] (Set a)

Instances

Instances details

Syntax SetW Source #
Instance details Defined in Constrained.Spec.Set Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. SetW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. SetW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Logic SetW Source #
Instance details Defined in Constrained.Spec.Set Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SetW as b, HasSpec a) ⇒ SetW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SetW as b, HasSpec a) ⇒ SetW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires SetW as b, HasSpec a) ⇒ SetW 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) ⇒ SetW dom rng → List Term dom → Evidence (AppRequires SetW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ SetW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). SetW dom Bool → List Term dom → [Pred] Source #
Semantics SetW Source #
Instance details Defined in Constrained.Spec.Set Methods semantics ∷ ∀ (d ∷ [Type]) r. SetW d r → FunTy d r Source #
Show (SetW ds r) Source #
Instance details Defined in Constrained.Spec.Set Methods showsPrec ∷ Int → SetW ds r → ShowS # show ∷ SetW ds r → String # showList ∷ [SetW ds r] → ShowS #
Eq (SetW dom rng) Source #
Instance details Defined in Constrained.Spec.Set Methods (==) ∷ SetW dom rng → SetW dom rng → Bool # (/=) ∷ SetW dom rng → SetW dom rng → Bool #

data SetSpec a Source #

Constructors

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

Instances

Instances details

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

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

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

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

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

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

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

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

pattern ToGeneric ∷ ∀ rng. () ⇒ ∀ a. (rng ~ SimpleRep a, GenericRequires a, HasSpec a, AppRequires BaseW '[a] rng) ⇒ Term a → Term rng Source #

pattern FromGeneric ∷ ∀ rng. () ⇒ ∀ a. (rng ~ a, GenericRequires a, HasSpec a, AppRequires BaseW '[SimpleRep a] rng) ⇒ Term (SimpleRep a) → Term rng Source #

pattern Unary ∷ HOLE a' a → ListCtx f '[a] (HOLE a') Source #

A Convenient pattern for singleton contexts

pattern (:<:) ∷ (Typeable b, Show b) ⇒ HOLE c a → b → ListCtx Value '[a, b] (HOLE c) Source #

Convenient patterns for binary contexts (the arrow :<: points towards the hole)

pattern (:>:) ∷ (Typeable a, Show a) ⇒ a → HOLE c b → ListCtx Value '[a, b] (HOLE c) Source #

Convenient patterns for binary contexts (the arrow :>: points towards the hole)

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

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

Instances

Instances details

Numeric a ⇒ NumLike a Source #
Instance details Defined in Constrained.NumOrd Methods subtractSpec ∷ a → TypeSpec a → Specification a Source # negateSpec ∷ TypeSpec a → Specification a Source # safeSubtract ∷ a → a → Maybe a 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.Test Methods arbitrary ∷ Gen (PairSpec a b) Source # shrink ∷ PairSpec 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 # show ∷ PairSpec a b → String # showList ∷ [PairSpec a b] → ShowS #

data MapSpec k v Source #

Constructors

MapSpec
Fields mapSpecHint ∷ Maybe Integer mapSpecMustKeys ∷ Set k mapSpecMustValues ∷ [v] mapSpecSize ∷ Specification Integer mapSpecElem ∷ Specification (k, v) mapSpecFold ∷ FoldSpec v

Instances

Instances details

(HasSpec (k, v), HasSpec k, HasSpec v, HasSpec [v]) ⇒ Pretty (WithPrec (MapSpec k v)) Source #
Instance details Defined in Constrained.Spec.Map Methods pretty ∷ WithPrec (MapSpec k v) → Doc ann Source # prettyList ∷ [WithPrec (MapSpec k v)] → Doc ann Source #
(Arbitrary k, Arbitrary v, Arbitrary (TypeSpec k), Arbitrary (TypeSpec v), Ord k, HasSpec k, Foldy v) ⇒ Arbitrary (MapSpec k v) Source #
Instance details Defined in Constrained.Test Methods arbitrary ∷ Gen (MapSpec k v) Source # shrink ∷ MapSpec k v → [MapSpec k v] Source #
Generic (MapSpec k v) Source #
Instance details Defined in Constrained.Spec.Map Associated Types type Rep (MapSpec k v) ∷ Type → Type # Methods from ∷ MapSpec k v → Rep (MapSpec k v) x # to ∷ Rep (MapSpec k v) x → MapSpec k v #
(HasSpec (k, v), HasSpec k, HasSpec v, HasSpec [v]) ⇒ Show (MapSpec k v) Source #
Instance details Defined in Constrained.Spec.Map Methods showsPrec ∷ Int → MapSpec k v → ShowS # show ∷ MapSpec k v → String # showList ∷ [MapSpec k v] → ShowS #
type Rep (MapSpec k v) Source #
Instance details Defined in Constrained.Spec.Map type Rep (MapSpec k v) = D1 ('MetaData "MapSpec" "Constrained.Spec.Map" "constrained-generators-0.2.0.0-inplace" 'False) (C1 ('MetaCons "MapSpec" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mapSpecHint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Integer)) :: (S1 ('MetaSel ('Just "mapSpecMustKeys") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set k)) :: S1 ('MetaSel ('Just "mapSpecMustValues") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [v]))) :: (S1 ('MetaSel ('Just "mapSpecSize") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Specification Integer)) :: (S1 ('MetaSel ('Just "mapSpecElem") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Specification (k, v))) :*: S1 ('MetaSel ('Just "mapSpecFold") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FoldSpec v))))))

dom_ ∷ (HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term (Set k) Source #

rng_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term [v] Source #

lookup_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term k → Term (Map k v) → Term (Maybe v) Source #

mapMember_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term k → Term (Map k v) → Term Bool Source #

fstSpec ∷ ∀ k v. (HasSpec k, HasSpec v) ⇒ Specification (k, v) → Specification k Source #

sndSpec ∷ ∀ k v. (HasSpec k, HasSpec v) ⇒ Specification (k, v) → Specification v Source #

var ∷ QuasiQuoter Source #

data Prod a b Source #

Constructors

Prod
Fields prodFst ∷ a prodSnd ∷ b

Instances

Instances details

(Show a, Show b) ⇒ Show (Prod a b) Source #
Instance details Defined in Constrained.Generic Methods showsPrec ∷ Int → Prod a b → ShowS # show ∷ Prod a b → String # showList ∷ [Prod a b] → ShowS #
(HasSpec a, HasSpec b) ⇒ HasSpec (Prod a b) Source #
Instance details Defined in Constrained.TheKnot Associated Types type TypeSpec (Prod a b) Source # type Prerequisites (Prod a b) Source # Methods emptySpec ∷ TypeSpec (Prod a b) Source # combineSpec ∷ TypeSpec (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 # conformsTo ∷ Prod a b → TypeSpec (Prod a b) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (Prod a b) → Prod a b → [Prod a b] Source # toPreds ∷ Term (Prod a b) → TypeSpec (Prod a b) → Pred Source # cardinalTypeSpec ∷ TypeSpec (Prod a b) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (Prod a b) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (Prod a b) → BinaryShow Source # monadConformsTo ∷ Prod a b → TypeSpec (Prod a b) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (Prod a b) → [Prod a b] → Specification (Prod a b) Source # guardTypeSpec ∷ [String] → TypeSpec (Prod a b) → Specification (Prod a b) Source # prerequisites ∷ Evidence (Prerequisites (Prod a b)) Source #
(Eq a, Eq b) ⇒ Eq (Prod a b) Source #
Instance details Defined in Constrained.Generic Methods (==) ∷ Prod a b → Prod a b → Bool # (/=) ∷ Prod a b → Prod a b → Bool #
(Ord a, Ord b) ⇒ Ord (Prod a b) Source #
Instance details Defined in Constrained.Generic Methods compare ∷ Prod a b → Prod a b → Ordering # (<) ∷ Prod a b → Prod a b → Bool # (<=) ∷ Prod a b → Prod a b → Bool # (>) ∷ Prod a b → Prod a b → Bool # (>=) ∷ Prod a b → Prod a b → Bool # max ∷ Prod a b → Prod a b → Prod a b # min ∷ Prod a b → Prod a b → Prod a b #
type Prerequisites (Prod a b) Source #
Instance details Defined in Constrained.TheKnot type Prerequisites (Prod a b) = (HasSpec a, HasSpec b)
type TypeSpec (Prod a b) Source #
Instance details Defined in Constrained.TheKnot type TypeSpec (Prod a b) = PairSpec a b