Safe Haskell	Safe-Inferred
Language	Haskell2010

Constrained.API

Synopsis

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 LogicRequires 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 Syntax t ⇒ Semantics (t ∷ [Type] → Type → Type) where
- semantics ∷ ∀ d r. t d r → FunTy d r
class Syntax (t ∷ [Type] → Type → Type) where
- inFix ∷ ∀ dom rng. t dom rng → Bool
- prettyWit ∷ ∀ dom rng ann. (All HasSpec dom, HasSpec rng) ⇒ t dom rng → List Term 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]
data Specification a where
- ExplainSpec ∷ [String] → Specification a → Specification a
- MemberSpec ∷ NonEmpty a → Specification a
- ErrorSpec ∷ NonEmpty String → Specification a
- SuspendedSpec ∷ HasSpec a ⇒ Var a → Pred → Specification a
- TypeSpec ∷ HasSpec a ⇒ TypeSpec a → [a] → Specification a
- TrueSpec ∷ Specification a
data Term a where
- App ∷ ∀ t dom rng. AppRequires t dom rng ⇒ t dom rng → List Term dom → Term rng
- Lit ∷ (Typeable a, Eq a, Show a) ⇒ a → Term a
- V ∷ HasSpec a ⇒ Var a → Term a
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
data Pred where
- ElemPred ∷ ∀ a. HasSpec a ⇒ Bool → Term a → NonEmpty a → Pred
- Monitor ∷ ((∀ a. Term a → a) → Property → Property) → Pred
- And ∷ [Pred] → Pred
- Exists ∷ ((∀ b. Term b → b) → GE a) → Binder a → Pred
- Subst ∷ HasSpec a ⇒ Var a → Term a → Pred → Pred
- Let ∷ Term a → Binder a → Pred
- Assert ∷ Term Bool → Pred
- Reifies ∷ (HasSpec a, HasSpec b) ⇒ Term b → Term a → (a → b) → Pred
- DependsOn ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Pred
- ForAll ∷ (Forallable t a, HasSpec t, HasSpec a) ⇒ Term t → Binder a → Pred
- Case ∷ HasSpec (SumOver as) ⇒ Term (SumOver as) → List (Weighted Binder) as → Pred
- When ∷ HasSpec Bool ⇒ Term Bool → Pred → Pred
- GenHint ∷ HasGenHint a ⇒ Hint a → Term a → Pred
- TruePred ∷ Pred
- FalsePred ∷ NonEmpty String → Pred
- Explain ∷ NonEmpty String → Pred → Pred
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 ∷ (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 Bool, 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 = (Cases a ~ '[a], 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. (HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep 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), HasSpec a) ⇒ Term t → FunTy (MapList Term (Args (SimpleRep 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, IsPred p) ⇒ FunTy (MapList Term (Args (SimpleRep 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, IsPred p) ⇒ Term a → (a → b) → FunTy (MapList Term (Args (SimpleRep b))) p → Pred
con ∷ ∀ c a r. (SimpleRep a ~ SOP (TheSop a), TypeSpec a ~ TypeSpec (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), HasSpec a, HasSimpleRep a, r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a), ResultType r ~ Term a, SOPTerm c (TheSop a), ConstrTerm (ConstrOf c (TheSop a))) ⇒ r
onCon ∷ ∀ c a p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a, HasSpec (SimpleRep 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), TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a, HasSpec (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop 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) ⇒ Term a → Term (At n as)
match ∷ ∀ p a. (HasSpec a, IsProductType a, IsPred p) ⇒ 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)
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

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 LogicRequires t ⇒ Logic t where Source #

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 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.NumSpec 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 NumOrdW Source #
Instance details Defined in Constrained.TheKnot Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires NumOrdW as b, HasSpec a) ⇒ NumOrdW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires NumOrdW as b, HasSpec a) ⇒ NumOrdW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires NumOrdW as b, HasSpec a) ⇒ NumOrdW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source # rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ NumOrdW dom rng → List Term dom → Evidence (AppRequires NumOrdW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ NumOrdW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). NumOrdW dom Bool → List Term dom → [Pred] Source #
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 BoolW Source #
Instance details Defined in Constrained.TheKnot Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires BoolW as b, HasSpec a) ⇒ BoolW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires BoolW as b, HasSpec a) ⇒ BoolW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires BoolW as b, HasSpec a) ⇒ BoolW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source # rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ BoolW dom rng → List Term dom → Evidence (AppRequires BoolW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ BoolW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). BoolW dom Bool → List Term dom → [Pred] Source #
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 EqW Source #
Instance details Defined in Constrained.TheKnot Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires EqW as b, HasSpec a) ⇒ EqW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires EqW as b, HasSpec a) ⇒ EqW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires EqW as b, HasSpec a) ⇒ EqW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source # rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ EqW dom rng → List Term dom → Evidence (AppRequires EqW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ EqW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). EqW dom Bool → List Term dom → [Pred] Source #
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 #
Logic SumW Source #
Instance details Defined in Constrained.TheKnot Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SumW as b, HasSpec a) ⇒ SumW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SumW as b, HasSpec a) ⇒ SumW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires SumW as b, HasSpec a) ⇒ SumW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source # rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ SumW dom rng → List Term dom → Evidence (AppRequires SumW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ SumW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). SumW dom Bool → List Term dom → [Pred] Source #

class Syntax t ⇒ 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 ∷ ∀ d r. 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 IntW Source #
Instance details Defined in Constrained.NumSpec Methods semantics ∷ ∀ (d ∷ [Type]) r. IntW d r → FunTy d r Source #
Semantics NumOrdW Source #
Instance details Defined in Constrained.NumSpec Methods semantics ∷ ∀ (d ∷ [Type]) r. NumOrdW 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 BoolW Source #
Instance details Defined in Constrained.TheKnot Methods semantics ∷ ∀ (d ∷ [Type]) r. BoolW 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 EqW Source #
Instance details Defined in Constrained.TheKnot Methods semantics ∷ ∀ (d ∷ [Type]) r. EqW 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 #
Semantics SumW Source #
Instance details Defined in Constrained.TheKnot Methods semantics ∷ ∀ (d ∷ [Type]) r. SumW d r → FunTy d r Source #

class Syntax (t ∷ [Type] → Type → Type) 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.

Syntactic operations are ones that have to do with the structure and appearence of the type.

Minimal complete definition

Nothing

Methods

inFix ∷ ∀ dom rng. t dom rng → Bool Source #

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

Instances

Instances details

Syntax BaseW Source #
Instance details Defined in Constrained.Base Methods inFix ∷ ∀ (dom ∷ [Type]) rng. BaseW dom rng → Bool Source # prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ BaseW dom rng → List Term dom → Int → Maybe (Doc ann) Source #
Syntax IntW Source #
Instance details Defined in Constrained.NumSpec Methods inFix ∷ ∀ (dom ∷ [Type]) rng. IntW dom rng → Bool Source # prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ IntW dom rng → List Term dom → Int → Maybe (Doc ann) Source #
Syntax NumOrdW Source #
Instance details Defined in Constrained.NumSpec Methods inFix ∷ ∀ (dom ∷ [Type]) rng. NumOrdW dom rng → Bool Source # prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ NumOrdW dom rng → List Term dom → Int → Maybe (Doc ann) Source #
Syntax MapW Source #
Instance details Defined in Constrained.Spec.Map Methods inFix ∷ ∀ (dom ∷ [Type]) rng. MapW dom rng → Bool Source # prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ MapW dom rng → List Term dom → Int → Maybe (Doc ann) Source #
Syntax SetW Source #
Instance details Defined in Constrained.Spec.Set Methods inFix ∷ ∀ (dom ∷ [Type]) rng. SetW dom rng → Bool Source # prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ SetW dom rng → List Term dom → Int → Maybe (Doc ann) Source #
Syntax TreeW Source #
Instance details Defined in Constrained.Spec.Tree Methods inFix ∷ ∀ (dom ∷ [Type]) rng. TreeW dom rng → Bool Source # prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ TreeW dom rng → List Term dom → Int → Maybe (Doc ann) Source #
Syntax BoolW Source #
Instance details Defined in Constrained.TheKnot Methods inFix ∷ ∀ (dom ∷ [Type]) rng. BoolW dom rng → Bool Source # prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ BoolW dom rng → List Term dom → Int → Maybe (Doc ann) Source #
Syntax ElemW Source #
Instance details Defined in Constrained.TheKnot Methods inFix ∷ ∀ (dom ∷ [Type]) rng. ElemW dom rng → Bool Source # prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ ElemW dom rng → List Term dom → Int → Maybe (Doc ann) Source #
Syntax EqW Source #
Instance details Defined in Constrained.TheKnot Methods inFix ∷ ∀ (dom ∷ [Type]) rng. EqW dom rng → Bool Source # prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ EqW dom rng → List Term dom → Int → Maybe (Doc ann) Source #
Syntax FunW Source #
Instance details Defined in Constrained.TheKnot Methods inFix ∷ ∀ (dom ∷ [Type]) rng. FunW dom rng → Bool Source # prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ FunW dom rng → List Term dom → Int → Maybe (Doc ann) Source #
Syntax ListW Source #
Instance details Defined in Constrained.TheKnot Methods inFix ∷ ∀ (dom ∷ [Type]) rng. ListW dom rng → Bool Source # prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ ListW dom rng → List Term dom → Int → Maybe (Doc ann) Source #
Syntax ProdW Source #
Instance details Defined in Constrained.TheKnot Methods inFix ∷ ∀ (dom ∷ [Type]) rng. ProdW dom rng → Bool Source # prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ ProdW dom rng → List Term dom → Int → Maybe (Doc ann) Source #
Syntax SizeW Source #
Instance details Defined in Constrained.TheKnot Methods inFix ∷ ∀ (dom ∷ [Type]) rng. SizeW dom rng → Bool Source # prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ SizeW dom rng → List Term dom → Int → Maybe (Doc ann) Source #
Syntax SumW Source #
Instance details Defined in Constrained.TheKnot Methods inFix ∷ ∀ (dom ∷ [Type]) rng. SumW dom rng → Bool Source # prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ SumW dom rng → List Term dom → Int → Maybe (Doc ann) Source #

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.NumSpec Methods arbitrary ∷ Gen (NumSpec a) Source # shrink ∷ NumSpec a → [NumSpec a] Source #
Ord n ⇒ Monoid (NumSpec n) Source #
Instance details Defined in Constrained.NumSpec 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.NumSpec 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.NumSpec 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.NumSpec 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.NumSpec 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.NumSpec Methods lowerBound ∷ Maybe Int16 Source # upperBound ∷ Maybe Int16 Source #
MaybeBounded Int32 Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Int32 Source # upperBound ∷ Maybe Int32 Source #
MaybeBounded Int64 Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Int64 Source # upperBound ∷ Maybe Int64 Source #
MaybeBounded Int8 Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Int8 Source # upperBound ∷ Maybe Int8 Source #
MaybeBounded Word16 Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Word16 Source # upperBound ∷ Maybe Word16 Source #
MaybeBounded Word32 Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Word32 Source # upperBound ∷ Maybe Word32 Source #
MaybeBounded Word64 Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Word64 Source # upperBound ∷ Maybe Word64 Source #
MaybeBounded Word8 Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Word8 Source # upperBound ∷ Maybe Word8 Source #
MaybeBounded Integer Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Integer Source # upperBound ∷ Maybe Integer Source #
MaybeBounded Natural Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Natural Source # upperBound ∷ Maybe Natural Source #
MaybeBounded Float Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Float Source # upperBound ∷ Maybe Float Source #
MaybeBounded Int Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Int Source # upperBound ∷ Maybe Int Source #
MaybeBounded (Ratio Integer) Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe (Ratio Integer) Source # upperBound ∷ Maybe (Ratio Integer) Source #
MaybeBounded (Unbounded a) Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe (Unbounded a) Source # upperBound ∷ Maybe (Unbounded a) Source #

data NonEmpty a #

Constructors

a :| [a]

Instances

Instances details

MonadFix NonEmpty
Instance details Defined in Control.Monad.Fix Methods mfix ∷ (a → NonEmpty a) → NonEmpty a
Foldable NonEmpty
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
Instance details Defined in Data.Functor.Classes Methods liftEq ∷ (a → b → Bool) → NonEmpty a → NonEmpty b → Bool
Ord1 NonEmpty
Instance details Defined in Data.Functor.Classes Methods liftCompare ∷ (a → b → Ordering) → NonEmpty a → NonEmpty b → Ordering
Read1 NonEmpty
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
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
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
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
Instance details Defined in GHC.Base Methods fmap ∷ (a → b) → NonEmpty a → NonEmpty b (<$) ∷ a → NonEmpty b → NonEmpty a
Monad NonEmpty
Instance details Defined in GHC.Base Methods (>>=) ∷ NonEmpty a → (a → NonEmpty b) → NonEmpty b (>>) ∷ NonEmpty a → NonEmpty b → NonEmpty b return ∷ 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)
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)
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
IsList (NonEmpty a)
Instance details Defined in GHC.Exts 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)]
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
Read a ⇒ Read (NonEmpty a)
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)
Instance details Defined in GHC.Show Methods showsPrec ∷ Int → NonEmpty a → ShowS show ∷ NonEmpty a → String showList ∷ [NonEmpty a] → ShowS
Eq a ⇒ Eq (NonEmpty a)
Instance details Defined in GHC.Base Methods (==) ∷ NonEmpty a → NonEmpty a → Bool (/=) ∷ NonEmpty a → NonEmpty a → Bool
Ord a ⇒ Ord (NonEmpty a)
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
Instance details Defined in GHC.Generics type Rep1 NonEmpty = D1 ('MetaData "NonEmpty" "GHC.Base" "base" 'False) (C1 ('MetaCons ":\|" ('InfixI 'LeftAssociative 9) 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1 :*: S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec1 [])))
type Item (NonEmpty a)
Instance details Defined in GHC.Exts type Item (NonEmpty a) = a
type Rep (NonEmpty a)
Instance details Defined in GHC.Generics type Rep (NonEmpty a) = D1 ('MetaData "NonEmpty" "GHC.Base" "base" 'False) (C1 ('MetaCons ":\|" ('InfixI 'LeftAssociative 9) 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [a])))

data Specification a where Source #

A `Specification a` denotes a set of as

Constructors

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

Instances

Instances details

(HasSpec a, Arbitrary (TypeSpec a)) ⇒ Arbitrary (Specification a) Source #
Instance details Defined in Constrained.TheKnot Methods arbitrary ∷ Gen (Specification a) Source # shrink ∷ Specification a → [Specification a] Source #
HasSpec a ⇒ Monoid (Specification a)
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)
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)	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.NumSpec 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
HasSpec a ⇒ Show (Specification a) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → Specification a → ShowS show ∷ Specification a → String showList ∷ [Specification a] → ShowS
HasSpec a ⇒ Pretty (Specification a) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ Specification a → Doc ann Source # prettyList ∷ [Specification a] → Doc ann Source #
HasSpec a ⇒ Pretty (WithPrec (Specification a)) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ WithPrec (Specification a) → Doc ann Source # prettyList ∷ [WithPrec (Specification a)] → Doc ann Source #

data Term a where Source #

Constructors

App ∷ ∀ t dom rng. AppRequires t dom rng ⇒ t dom rng → List Term dom → Term rng
Lit ∷ (Typeable a, Eq a, Show a) ⇒ a → Term a
V ∷ HasSpec a ⇒ Var a → Term a

Instances

Instances details

(Ord a, HasSpec a, HasSpec (Set a)) ⇒ Monoid (Term (Set a))
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))
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)
Instance details Defined in Constrained.NumSpec 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
Show a ⇒ Show (Term a) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → Term a → ShowS show ∷ Term a → String showList ∷ [Term a] → ShowS
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 #
Eq (Term a) Source #
Instance details Defined in Constrained.Base Methods (==) ∷ Term a → Term a → Bool (/=) ∷ Term a → Term a → Bool
Show a ⇒ Pretty (Term a) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ Term a → Doc ann Source # prettyList ∷ [Term a] → Doc ann Source #
Show a ⇒ Pretty (WithPrec (Term a)) Source #
Instance details Defined in Constrained.Base Methods pretty ∷ WithPrec (Term a) → Doc ann Source # prettyList ∷ [WithPrec (Term 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 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.

data Pred where Source #

Constructors

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

Instances

Instances details

Monoid Pred Source #
Instance details Defined in Constrained.Base Methods mempty ∷ Pred mappend ∷ Pred → Pred → Pred mconcat ∷ [Pred] → Pred
Semigroup Pred Source #
Instance details Defined in Constrained.Base Methods (<>) ∷ Pred → Pred → Pred # sconcat ∷ NonEmpty Pred → Pred stimes ∷ Integral b ⇒ b → Pred → Pred
Show Pred Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → Pred → ShowS show ∷ Pred → String showList ∷ [Pred] → ShowS
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 #
Pretty Pred Source #
Instance details Defined in Constrained.Base Methods pretty ∷ Pred → Doc ann Source # prettyList ∷ [Pred] → Doc ann 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 Specification. 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 Specification

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.TheKnot 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.TheKnot 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.TheKnot 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.TheKnot 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.TheKnot 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.TheKnot 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.TheKnot 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.TheKnot 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 Integer Source #
Instance details Defined in Constrained.TheKnot 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.TheKnot 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 #
Instance details Defined in Constrained.TheKnot 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.TheKnot 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.TheKnot 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.TheKnot 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.TheKnot 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 () Source #
Instance details Defined in Constrained.Base Associated Types type SimpleRep () Source # type TheSop () ∷ [Type] Source # Methods toSimpleRep ∷ () → SimpleRep () Source # fromSimpleRep ∷ SimpleRep () → () Source #
HasSimpleRep Bool Source #
Instance details Defined in Constrained.Generic Associated Types type SimpleRep Bool Source # type TheSop Bool ∷ [Type] Source # Methods toSimpleRep ∷ Bool → SimpleRep Bool Source # fromSimpleRep ∷ SimpleRep Bool → Bool 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 ∷ (TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, OrdLike (SimpleRep a)) ⇒ a → Specification a Source #

ltSpec ∷ a → Specification a Source #

default ltSpec ∷ (TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, OrdLike (SimpleRep a)) ⇒ a → Specification a Source #

geqSpec ∷ a → Specification a Source #

default geqSpec ∷ (TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, OrdLike (SimpleRep a)) ⇒ a → Specification a Source #

gtSpec ∷ a → Specification a Source #

default gtSpec ∷ (TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, OrdLike (SimpleRep 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.NumSpec 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 ∷ (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 Bool, HasSpec a) ⇒ Term a → (a → Bool) → Pred Source #

requires (HasSpec Bool)

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 = (Cases a ~ '[a], 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. (HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep 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), HasSpec a) ⇒ Term t → FunTy (MapList Term (Args (SimpleRep 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, IsPred p) ⇒ FunTy (MapList Term (Args (SimpleRep 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, IsPred p) ⇒ Term a → (a → b) → FunTy (MapList Term (Args (SimpleRep 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)), HasSpec a, HasSimpleRep a, r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a), ResultType r ~ Term a, SOPTerm c (TheSop a), ConstrTerm (ConstrOf c (TheSop a))) ⇒ r Source #

onCon ∷ ∀ c a p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a, HasSpec (SimpleRep 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), TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a, HasSpec (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop 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) ⇒ Term a → Term (At n as) Source #

match ∷ ∀ p a. (HasSpec a, IsProductType a, IsPred p) ⇒ 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

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 #
Syntax SetW Source #
Instance details Defined in Constrained.Spec.Set Methods inFix ∷ ∀ (dom ∷ [Type]) rng. SetW dom rng → Bool Source # prettyWit ∷ ∀ (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ SetW dom rng → List Term dom → Int → Maybe (Doc ann) 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.Spec.Set 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.NumSpec 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.TheKnot 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.Spec.Map 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 #

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