Safe Haskell	Safe-Inferred
Language	Haskell2010

Constrained

Description

This module exports the user-facing interface for the library. It is supposed to contain everything you need to write constraints and implement HasSpec and HasSimpleRep instances.

Synopsis

data Specification fn a where
- MemberSpec ∷ OrdSet a → Specification fn a
- ErrorSpec ∷ [String] → Specification fn a
- SuspendedSpec ∷ HasSpec fn a ⇒ Var a → Pred fn → Specification fn a
- TypeSpec ∷ HasSpec fn a ⇒ TypeSpec fn a → OrdSet a → Specification fn a
- TrueSpec ∷ Specification fn a
data Pred (fn ∷ [Type] → Type → Type)
data Term (fn ∷ [Type] → Type → Type) a
class (Typeable a, Eq a, Show a, Show (TypeSpec fn a), BaseUniverse fn) ⇒ HasSpec fn a where
- type TypeSpec (fn ∷ [Type] → Type → Type) a
- type Prerequisites fn a ∷ Constraint
- emptySpec ∷ TypeSpec fn a
- combineSpec ∷ TypeSpec fn a → TypeSpec fn a → Specification fn a
- genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec fn a → GenT m a
- conformsTo ∷ HasCallStack ⇒ a → TypeSpec fn a → Bool
- shrinkWithTypeSpec ∷ TypeSpec fn a → a → [a]
- toPreds ∷ Term fn a → TypeSpec fn a → Pred fn
- cardinalTypeSpec ∷ TypeSpec fn a → Specification fn Integer
- cardinalTrueSpec ∷ Specification fn Integer
- typeSpecOpt ∷ TypeSpec fn a → [a] → Specification fn a
- prerequisites ∷ Evidence (Prerequisites fn a)
class HasSimpleRep a where
- type SimpleRep a
- type TheSop a ∷ [Type]
- toSimpleRep ∷ a → SimpleRep a
- fromSimpleRep ∷ SimpleRep a → a
class (Num a, HasSpec fn a) ⇒ NumLike fn a where
- subtractSpec ∷ a → TypeSpec fn a → Specification fn a
- negateSpec ∷ TypeSpec fn a → Specification fn a
- safeSubtract ∷ a → a → Maybe a
class HasSpec fn a ⇒ OrdLike fn a where
- leqSpec ∷ a → Specification fn a
- ltSpec ∷ a → Specification fn a
- geqSpec ∷ a → Specification fn a
- gtSpec ∷ a → Specification fn a
class Forallable t e | t → e where
- fromForAllSpec ∷ (HasSpec fn t, HasSpec fn e, BaseUniverse fn) ⇒ Specification fn e → Specification fn t
- forAllToList ∷ t → [e]
class HasSpec fn a ⇒ Foldy fn a where
- genList ∷ (BaseUniverse fn, MonadGenError m) ⇒ Specification fn a → Specification fn a → GenT m [a]
- theAddFn ∷ fn '[a, a] a
- theZero ∷ a
class MaybeBounded a where
- lowerBound ∷ Maybe a
- upperBound ∷ Maybe a
class FunctionLike fn where
- sem ∷ fn as b → FunTy as b
class (∀ as b. Show (f as b), ∀ as b. Eq (f as b), Typeable f, FunctionLike f) ⇒ Functions f fn where
- propagateSpecFun ∷ (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ f as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a
- rewriteRules ∷ (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ f as b → List (Term fn) as → Maybe (Term fn b)
- mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ f '[a] b → TypeSpec fn a → Specification fn b
data HOLE a b where
- HOLE ∷ HOLE a a
type BaseUniverse fn = (Functions fn fn, Member (EqFn fn) fn, Member (SetFn fn) fn, Member (BoolFn fn) fn, Member (PairFn fn) fn, Member (IntFn fn) fn, Member (OrdFn fn) fn, Member (GenericsFn fn) fn, Member (ListFn fn) fn, Member (SumFn fn) fn, Member (MapFn fn) fn, Member (FunFn fn) fn, Member (SizeFn fn) fn)
type Member fn univ = IsMember fn univ (Path fn univ)
type BaseFn = Fix (OneofL BaseFns)
type BaseFns = '[EqFn, SetFn, BoolFn, PairFn, IntFn, OrdFn, GenericsFn, ListFn, SumFn, MapFn, FunFn, SizeFn]
data Fix (fn ∷ Univ → Univ) (as ∷ [Type]) b
type family OneofL as where ...
type IsPred p fn = (PredLike p, UnivConstr p fn)
type IsNormalType a = (Cases a ~ '[a], Args a ~ '[a], IsProd a)
data Value a where
- Value ∷ Show a ⇒ !a → Value a
type family SOP constrs where ...
data (c ∷ Symbol) ::: (ts ∷ [Type])
data MapFn (fn ∷ [Type] → Type → Type) args res
data FunFn fn args res
data PairSpec fn a b = Cartesian (Specification fn a) (Specification fn b)
data NumSpec n = NumSpecInterval (Maybe n) (Maybe n)
data MapSpec fn k v = MapSpec {
- mapSpecHint ∷ Maybe Integer
- mapSpecMustKeys ∷ Set k
- mapSpecMustValues ∷ [v]
- mapSpecSize ∷ Specification fn Integer
- mapSpecElem ∷ Specification fn (k, v)
- mapSpecFold ∷ FoldSpec fn v
}
data FoldSpec (fn ∷ [Type] → Type → Type) a where
- NoFold ∷ FoldSpec fn a
- FoldSpec ∷ ∀ b fn a. (HasSpec fn a, HasSpec fn b, Foldy fn b, Member (ListFn fn) fn, BaseUniverse fn) ⇒ fn '[a] b → Specification fn b → FoldSpec fn a
simplifySpec ∷ HasSpec fn a ⇒ Specification fn a → Specification fn a
genFromSpec ∷ ∀ fn a m. (HasCallStack, HasSpec fn a, MonadGenError m) ⇒ Specification fn a → GenT m a
genFromSpec_ ∷ ∀ fn a. (HasCallStack, HasSpec fn a) ⇒ Specification fn a → Gen a
genFromSpecWithSeed ∷ ∀ fn a. (HasCallStack, HasSpec fn a) ⇒ Int → Int → Specification fn a → a
shrinkWithSpec ∷ ∀ fn a. HasSpec fn a ⇒ Specification fn a → a → [a]
conformsToSpec ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a → Bool
conformsToSpecProp ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a → Property
monitorSpec ∷ (FunctionLike fn, Testable p) ⇒ Specification fn a → a → p → Property
forAllSpec ∷ (HasSpec fn a, Testable p) ⇒ Specification fn a → (a → p) → Property
forAllSpecShow ∷ (HasSpec fn a, Testable p) ⇒ Specification fn a → (a → String) → (a → p) → Property
giveHint ∷ HasGenHint fn a ⇒ Hint a → Specification fn a
typeSpec ∷ HasSpec fn a ⇒ TypeSpec fn a → Specification fn a
con ∷ ∀ c a r fn. (SimpleRep a ~ SOP (TheSop a), TypeSpec fn a ~ TypeSpec fn (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), HasSpec fn a, HasSimpleRep a, r ~ FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) (Term fn a), ResultType r ~ Term fn a, SOPTerm c fn (TheSop a), ConstrTerm fn (ConstrOf c (TheSop a))) ⇒ r
isCon ∷ ∀ c a fn. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, HasSpec fn a, HasSpec fn (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All (HasSpec fn) (Cases (SOP (TheSop a))), HasSpec fn (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term fn a → Pred fn
onCon ∷ ∀ c a fn p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, HasSpec fn a, HasSpec fn (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All (HasSpec fn) (Cases (SOP (TheSop a))), HasSpec fn (ProdOver (ConstrOf c (TheSop a))), IsPred p fn, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All (HasSpec fn) (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term fn a → FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) p → Pred fn
sel ∷ ∀ n fn a c as. (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as, HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) ⇒ Term fn a → Term fn (At n as)
caseBoolSpec ∷ HasSpec fn a ⇒ Specification fn Bool → (Bool → Specification fn a) → Specification fn a
constrained ∷ ∀ a fn p. (IsPred p fn, HasSpec fn a) ⇒ (Term fn a → p) → Specification fn a
constrained' ∷ ∀ a fn p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec fn a, IsPred p fn) ⇒ FunTy (MapList (Term fn) (Args (SimpleRep a))) p → Specification fn a
satisfies ∷ ∀ fn a. HasSpec fn a ⇒ Term fn a → Specification fn a → Pred fn
letBind ∷ (HasSpec fn a, IsPred p fn) ⇒ Term fn a → (Term fn a → p) → Pred fn
match ∷ ∀ fn p a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, Cases (SimpleRep a) ~ '[SimpleRep a], SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), IsProd (SimpleRep a), All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn) ⇒ Term fn a → FunTy (MapList (Term fn) (Args (SimpleRep a))) p → Pred fn
assert ∷ (BaseUniverse fn, IsPred p fn) ⇒ p → Pred fn
assertExplain ∷ (BaseUniverse fn, IsPred p fn) ⇒ [String] → p → Pred fn
caseOn ∷ ∀ fn a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) ⇒ Term fn a → FunTy (MapList (Binder fn) (Cases (SimpleRep a))) (Pred fn)
branch ∷ ∀ fn p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) ⇒ FunTy (MapList (Term fn) (Args a)) p → Binder fn a
ifElse ∷ (BaseUniverse fn, IsPred p fn, IsPred q fn) ⇒ Term fn Bool → p → q → Pred fn
onJust ∷ ∀ fn a p. (BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) ⇒ Term fn (Maybe a) → (Term fn a → p) → Pred fn
isJust ∷ ∀ fn a. (BaseUniverse fn, HasSpec fn a, IsNormalType a) ⇒ Term fn (Maybe a) → Pred fn
reify ∷ (HasSpec fn a, HasSpec fn b, IsPred p fn) ⇒ Term fn a → (a → b) → (Term fn b → p) → Pred fn
reify' ∷ ∀ fn a b p. (Cases (SimpleRep b) ~ '[SimpleRep b], TypeSpec fn b ~ TypeSpec fn (SimpleRep b), HasSpec fn (SimpleRep b), HasSimpleRep b, All (HasSpec fn) (Args (SimpleRep b)), IsProd (SimpleRep b), HasSpec fn a, HasSpec fn b, IsPred p fn) ⇒ Term fn a → (a → b) → FunTy (MapList (Term fn) (Args (SimpleRep b))) p → Pred fn
reifies ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn b → Term fn a → (a → b) → Pred fn
assertReified ∷ HasSpec fn a ⇒ Term fn a → (a → Bool) → Pred fn
monitor ∷ ((∀ a. Term fn a → a) → Property → Property) → Pred fn
genHint ∷ ∀ fn t. HasGenHint fn t ⇒ Hint t → Term fn t → Pred fn
dependsOn ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn a → Term fn b → Pred fn
forAll ∷ (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) ⇒ Term fn t → (Term fn a → p) → Pred fn
forAll' ∷ ∀ fn t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t, HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn, IsProd (SimpleRep a), HasSpec fn a) ⇒ Term fn t → FunTy (MapList (Term fn) (Args (SimpleRep a))) p → Pred fn
exists ∷ ∀ a p fn. (HasSpec fn a, IsPred p fn) ⇒ ((∀ b. Term fn b → b) → GE a) → (Term fn a → p) → Pred fn
unsafeExists ∷ ∀ a p fn. (HasSpec fn a, IsPred p fn) ⇒ (Term fn a → p) → Pred fn
fst_ ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ Term fn (a, b) → Term fn a
snd_ ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ Term fn (a, b) → Term fn b
pair_ ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ Term fn a → Term fn b → Term fn (a, b)
(<=.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool
(<.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool
(==.) ∷ HasSpec fn a ⇒ Term fn a → Term fn a → Term fn Bool
(/=.) ∷ HasSpec fn a ⇒ Term fn a → Term fn a → Term fn Bool
(||.) ∷ BaseUniverse fn ⇒ Term fn Bool → Term fn Bool → Term fn Bool
member_ ∷ ∀ a fn. (HasSpec fn a, Ord a) ⇒ Term fn a → Term fn (Set a) → Term fn Bool
subset_ ∷ (HasSpec fn a, Ord a) ⇒ Term fn (Set a) → Term fn (Set a) → Term fn Bool
disjoint_ ∷ (HasSpec fn a, Ord a) ⇒ Term fn (Set a) → Term fn (Set a) → Term fn Bool
singleton_ ∷ (HasSpec fn a, Ord a) ⇒ Term fn a → Term fn (Set a)
elem_ ∷ ∀ a fn. HasSpec fn a ⇒ Term fn a → Term fn [a] → Term fn Bool
not_ ∷ BaseUniverse fn ⇒ Term fn Bool → Term fn Bool
foldMap_ ∷ ∀ fn a b. (BaseUniverse fn, Foldy fn b, HasSpec fn a) ⇒ (Term fn a → Term fn b) → Term fn [a] → Term fn b
sum_ ∷ (BaseUniverse fn, Member (FunFn fn) fn, Foldy fn a) ⇒ Term fn [a] → Term fn a
size_ ∷ ∀ a fn. (HasSpec fn (Set a), Ord a) ⇒ Term fn (Set a) → Term fn Integer
rng_ ∷ (HasSpec fn k, HasSpec fn v, Ord k) ⇒ Term fn (Map k v) → Term fn [v]
dom_ ∷ (HasSpec fn (Map k v), HasSpec fn k, Ord k) ⇒ Term fn (Map k v) → Term fn (Set k)
left_ ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn a → Term fn (Either a b)
right_ ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn b → Term fn (Either a b)
toGeneric_ ∷ ∀ a fn. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Term fn a → Term fn (SimpleRep a)
fromGeneric_ ∷ ∀ a fn. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Term fn (SimpleRep a) → Term fn a
sizeOf_ ∷ ∀ a fn. (HasSpec fn a, Sized a) ⇒ Term fn a → Term fn Integer
length_ ∷ ∀ a fn. HasSpec fn [a] ⇒ Term fn [a] → Term fn Integer
injectFn ∷ ∀ fn fnU as b. Member fn fnU ⇒ fn as b → fnU as b
app ∷ (HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) ⇒ fn as b → FunTy (MapList (Term fn) as) (Term fn b)
lit ∷ Show a ⇒ a → Term fn a
emptyNumSpec ∷ Ord a ⇒ NumSpec a
combineNumSpec ∷ (HasSpec fn n, Ord n, TypeSpec fn n ~ NumSpec n) ⇒ NumSpec n → NumSpec n → Specification fn n
genFromNumSpec ∷ (MonadGenError m, Show n, Random n, Ord n, Num n, MaybeBounded n) ⇒ NumSpec n → GenT m n
shrinkWithNumSpec ∷ Arbitrary n ⇒ NumSpec n → n → [n]
conformsToNumSpec ∷ Ord n ⇒ n → NumSpec n → Bool
toPredsNumSpec ∷ (Ord n, OrdLike fn n) ⇒ Term fn n → NumSpec n → Pred fn
addFn ∷ ∀ fn a. NumLike fn a ⇒ fn '[a, a] a
toSimpleRepSpec ∷ ∀ a fn. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Specification fn a → Specification fn (SimpleRep a)
fromSimpleRepSpec ∷ ∀ a fn. (HasSpec fn a, HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Specification fn (SimpleRep a) → Specification fn a
algebra ∷ SOPLike constrs r ⇒ SOP constrs → ALG constrs r
inject ∷ ∀ c constrs. Inject c constrs (SOP constrs) ⇒ FunTy (ConstrOf c constrs) (SOP constrs)
toPred ∷ (BaseUniverse fn, IsPred p fn) ⇒ p → Pred fn
module Constrained.Spec.Tree
module Constrained.List
module Constrained.GenT

Documentation

data Specification fn a where Source #

A `Specification fn a` denotes a set of as

Constructors

MemberSpec	Elements of a known set
Fields ∷ OrdSet a It must be an element of this set → Specification fn a
ErrorSpec ∷ [String] → Specification fn a	The empty set
SuspendedSpec	The set described by some predicates over the bound variable. TODO: possibly we want to use a `Binder` here
Fields ∷ HasSpec fn a ⇒ Var a This variable ranges over values denoted by the spec → Pred fn And the variable is subject to these constraints → Specification fn a
TypeSpec	A type-specific spec
Fields ∷ HasSpec fn a ⇒ TypeSpec fn a → OrdSet a It can't be any of the elements of this set → Specification fn a
TrueSpec ∷ Specification fn a	Anything

Instances

Instances details

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

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

Instances

Instances details

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

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

Typed first order terms with function symbols from fn.

Instances

Instances details

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

class (Typeable a, Eq a, Show a, Show (TypeSpec fn a), BaseUniverse fn) ⇒ HasSpec fn a where Source #

This class provides the interface that allows you to extend the language to handle a new type. In the case of types that have a generic representation (via HasSimpleRep) that already has an instance of HasSpec it is sufficient to provide an empty instance. However, for types that are used together with specific functions in the function universe fn it may be necessary to provide a specific implementation of HasSpec. This is typically necessary when the Specification for the generic representation does not permit an implementation of propagateSpecFun for some function.

The basic types provided in the language, Set, `[]`, Map, Int, Word64, (,), Either, etc. have instances of this class (technically (,) and Either have instances derived from the instances for their generic Prod and Sum implementations).

Minimal complete definition

Nothing

Associated Types

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

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

type TypeSpec fn a = TypeSpec fn (SimpleRep a)

type Prerequisites fn a ∷ Constraint Source #

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

type Prerequisites fn a = ()

Methods

emptySpec ∷ TypeSpec fn a Source #

default emptySpec ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ TypeSpec fn a Source #

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

default combineSpec ∷ (HasSimpleRep a, HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ TypeSpec fn a → TypeSpec fn a → Specification fn a Source #

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

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

default genFromTypeSpec ∷ (HasSimpleRep a, HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ (HasCallStack, MonadGenError m) ⇒ TypeSpec fn a → GenT m a Source #

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

Check conformance to the spec.

default conformsTo ∷ (HasSimpleRep a, HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ HasCallStack ⇒ a → TypeSpec fn a → Bool Source #

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

Shrink an a with the aide of a Specification

default shrinkWithTypeSpec ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ TypeSpec fn a → a → [a] Source #

toPreds ∷ Term fn a → TypeSpec fn a → Pred fn Source #

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

default toPreds ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ Term fn a → TypeSpec fn a → Pred fn Source #

cardinalTypeSpec ∷ TypeSpec fn a → Specification fn Integer Source #

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

cardinalTrueSpec ∷ Specification fn Integer Source #

A bound on the number of solutions `genFromTypeSpec TrueSpec` can produce. For a type with finite elements, we can get a much more accurate answer than TrueSpec

typeSpecOpt ∷ TypeSpec fn a → [a] → Specification fn a Source #

For some types (especially finite ones) there may be much better ways to construct a Specification than the default method of just adding a large bad list to TypSpec. This function allows each HasSpec instance to decide.

prerequisites ∷ Evidence (Prerequisites fn a) Source #

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

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

Instances

Instances details

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

class HasSimpleRep a where Source #

Minimal complete definition

Nothing

Associated Types

type SimpleRep a Source #

type SimpleRep a = SOP (TheSop a)

type TheSop a ∷ [Type] Source #

type TheSop a = SOPOf (Rep a)

Methods

toSimpleRep ∷ a → SimpleRep a Source #

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

fromSimpleRep ∷ SimpleRep a → a Source #

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

Instances

Instances details

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

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

Minimal complete definition

Nothing

Methods

subtractSpec ∷ a → TypeSpec fn a → Specification fn a Source #

default subtractSpec ∷ (TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, NumLike fn (SimpleRep a)) ⇒ a → TypeSpec fn a → Specification fn a Source #

negateSpec ∷ TypeSpec fn a → Specification fn a Source #

default negateSpec ∷ (TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, NumLike fn (SimpleRep a)) ⇒ TypeSpec fn a → Specification fn a Source #

safeSubtract ∷ a → a → Maybe a Source #

default safeSubtract ∷ (HasSimpleRep a, NumLike fn (SimpleRep a)) ⇒ a → a → Maybe a Source #

Instances

Instances details

(HasSpec fn a, Ord a, Num a, TypeSpec fn a ~ NumSpec a, MaybeBounded a) ⇒ NumLike fn a Source #
Instance details Defined in Constrained.Base Methods subtractSpec ∷ a → TypeSpec fn a → Specification fn a Source # negateSpec ∷ TypeSpec fn a → Specification fn a Source # safeSubtract ∷ a → a → Maybe a Source #

class HasSpec fn a ⇒ OrdLike fn a where Source #

Minimal complete definition

Nothing

Methods

leqSpec ∷ a → Specification fn a Source #

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

ltSpec ∷ a → Specification fn a Source #

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

geqSpec ∷ a → Specification fn a Source #

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

gtSpec ∷ a → Specification fn a Source #

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

Instances

Instances details

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

class Forallable t e | t → e where Source #

Minimal complete definition

Nothing

Methods

fromForAllSpec ∷ (HasSpec fn t, HasSpec fn e, BaseUniverse fn) ⇒ Specification fn e → Specification fn t Source #

default fromForAllSpec ∷ (HasSpec fn t, HasSpec fn e, HasSimpleRep t, TypeSpec fn t ~ TypeSpec fn (SimpleRep t), Forallable (SimpleRep t) e, HasSpec fn (SimpleRep t)) ⇒ Specification fn e → Specification fn t Source #

forAllToList ∷ t → [e] Source #

default forAllToList ∷ (HasSimpleRep t, Forallable (SimpleRep t) e) ⇒ t → [e] Source #

Instances

Instances details

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

class HasSpec fn a ⇒ Foldy fn a where Source #

Methods

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

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

theZero ∷ a Source #

Instances

Instances details

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

class MaybeBounded a where Source #

Minimal complete definition

Nothing

Methods

lowerBound ∷ Maybe a Source #

default lowerBound ∷ Bounded a ⇒ Maybe a Source #

upperBound ∷ Maybe a Source #

default upperBound ∷ Bounded a ⇒ Maybe a Source #

Instances

Instances details

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

class FunctionLike fn where Source #

Methods

sem ∷ fn as b → FunTy as b Source #

The semantics of a function is given by sem

Instances

Instances details

FunctionLike fn ⇒ FunctionLike (FunFn fn) Source #
Instance details Defined in Constrained.Base Methods sem ∷ ∀ (as ∷ [Type]) b. FunFn fn as b → FunTy as b Source #
FunctionLike (GenericsFn fn) Source #
Instance details Defined in Constrained.Spec.Generics Methods sem ∷ ∀ (as ∷ [Type]) b. GenericsFn fn as b → FunTy as b Source #
FunctionLike (IntFn fn) Source #
Instance details Defined in Constrained.Base Methods sem ∷ ∀ (as ∷ [Type]) b. IntFn fn as b → FunTy as b Source #
FunctionLike fn ⇒ FunctionLike (ListFn fn) Source #
Instance details Defined in Constrained.Base Methods sem ∷ ∀ (as ∷ [Type]) b. ListFn fn as b → FunTy as b Source #
FunctionLike (OrdFn fn) Source #
Instance details Defined in Constrained.Base Methods sem ∷ ∀ (as ∷ [Type]) b. OrdFn fn as b → FunTy as b Source #
FunctionLike (SizeFn fn) Source #
Instance details Defined in Constrained.Base Methods sem ∷ ∀ (as ∷ [Type]) b. SizeFn fn as b → FunTy as b Source #
FunctionLike (TreeFn fn) Source #
Instance details Defined in Constrained.Spec.Tree Methods sem ∷ ∀ (as ∷ [Type]) b. TreeFn fn as b → FunTy as b Source #
FunctionLike (BoolFn fn) Source #
Instance details Defined in Constrained.Univ Methods sem ∷ ∀ (as ∷ [Type]) b. BoolFn fn as b → FunTy as b Source #
FunctionLike (EqFn fn) Source #
Instance details Defined in Constrained.Univ Methods sem ∷ ∀ (as ∷ [Type]) b. EqFn fn as b → FunTy as b Source #
FunctionLike (fn (Fix fn)) ⇒ FunctionLike (Fix fn) Source #
Instance details Defined in Constrained.Univ Methods sem ∷ ∀ (as ∷ [Type]) b. Fix fn as b → FunTy as b Source #
FunctionLike (MapFn fn) Source #
Instance details Defined in Constrained.Univ Methods sem ∷ ∀ (as ∷ [Type]) b. MapFn fn as b → FunTy as b Source #
FunctionLike (PairFn fn) Source #
Instance details Defined in Constrained.Univ Methods sem ∷ ∀ (as ∷ [Type]) b. PairFn fn as b → FunTy as b Source #
FunctionLike (SetFn fn) Source #
Instance details Defined in Constrained.Univ Methods sem ∷ ∀ (as ∷ [Type]) b. SetFn fn as b → FunTy as b Source #
FunctionLike (SumFn fn) Source #
Instance details Defined in Constrained.Univ Methods sem ∷ ∀ (as ∷ [Type]) b. SumFn fn as b → FunTy as b Source #
(FunctionLike (fn fnU), FunctionLike (fn' fnU)) ⇒ FunctionLike (Oneof fn fn' fnU) Source #
Instance details Defined in Constrained.Univ Methods sem ∷ ∀ (as ∷ [Type]) b. Oneof fn fn' fnU as b → FunTy as b Source #

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

Minimal complete definition

propagateSpecFun, mapTypeSpec

Methods

propagateSpecFun ∷ (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ f as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source #

rewriteRules ∷ (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ f as b → List (Term fn) as → Maybe (Term fn b) Source #

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

Instances

Instances details

(BaseUniverse fn, Member (FunFn fn) fn) ⇒ Functions (FunFn fn) fn Source #
Instance details Defined in Constrained.Base Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ FunFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ FunFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ FunFn fn '[a] b → TypeSpec fn a → Specification fn b Source #
BaseUniverse fn ⇒ Functions (GenericsFn fn) fn Source #
Instance details Defined in Constrained.Spec.Generics Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ GenericsFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ GenericsFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ GenericsFn fn '[a] b → TypeSpec fn a → Specification fn b Source #
BaseUniverse fn ⇒ Functions (IntFn fn) fn Source #
Instance details Defined in Constrained.Base Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ IntFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ IntFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ IntFn fn '[a] b → TypeSpec fn a → Specification fn b Source #
BaseUniverse fn ⇒ Functions (ListFn fn) fn Source #
Instance details Defined in Constrained.Base Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ ListFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ ListFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ ListFn fn '[a] b → TypeSpec fn a → Specification fn b Source #
BaseUniverse fn ⇒ Functions (OrdFn fn) fn Source #
Instance details Defined in Constrained.Base Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ OrdFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ OrdFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ OrdFn fn '[a] b → TypeSpec fn a → Specification fn b Source #
(BaseUniverse fn, HasSpec fn Integer) ⇒ Functions (SizeFn fn) fn Source #
Instance details Defined in Constrained.Base Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ SizeFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ SizeFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ SizeFn fn '[a] b → TypeSpec fn a → Specification fn b Source #
(Member (TreeFn fn) fn, BaseUniverse fn) ⇒ Functions (TreeFn fn) fn Source #
Instance details Defined in Constrained.Spec.Tree Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ TreeFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ TreeFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ TreeFn fn '[a] b → TypeSpec fn a → Specification fn b Source #
BaseUniverse fn ⇒ Functions (BoolFn fn) fn Source #
Instance details Defined in Constrained.Instances Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ BoolFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ BoolFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ BoolFn fn '[a] b → TypeSpec fn a → Specification fn b Source #
BaseUniverse fn ⇒ Functions (EqFn fn) fn Source #
Instance details Defined in Constrained.Instances Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ EqFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ EqFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ EqFn fn '[a] b → TypeSpec fn a → Specification fn b Source #
BaseUniverse fn ⇒ Functions (MapFn fn) fn Source #
Instance details Defined in Constrained.Spec.Map Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ MapFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ MapFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ MapFn fn '[a] b → TypeSpec fn a → Specification fn b Source #
BaseUniverse fn ⇒ Functions (PairFn fn) fn Source #
Instance details Defined in Constrained.Spec.Pairs Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ PairFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ PairFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ PairFn fn '[a] b → TypeSpec fn a → Specification fn b Source #
BaseUniverse fn ⇒ Functions (SetFn fn) fn Source #
Instance details Defined in Constrained.Base Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ SetFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ SetFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ SetFn fn '[a] b → TypeSpec fn a → Specification fn b Source #
BaseUniverse fn ⇒ Functions (SumFn fn) fn Source #
Instance details Defined in Constrained.Spec.Generics Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ SumFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ SumFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ SumFn fn '[a] b → TypeSpec fn a → Specification fn b Source #
(Typeable fn, Functions (fn (Fix fn)) (Fix fn)) ⇒ Functions (Fix fn) (Fix fn) Source #
Instance details Defined in Constrained.Instances Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec (Fix fn) a, All (HasSpec (Fix fn)) as) ⇒ Fix fn as b → ListCtx Value as (HOLE a) → Specification (Fix fn) b → Specification (Fix fn) a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec (Fix fn) b, All (HasSpec (Fix fn)) as) ⇒ Fix fn as b → List (Term (Fix fn)) as → Maybe (Term (Fix fn) b) Source # mapTypeSpec ∷ (HasSpec (Fix fn) a, HasSpec (Fix fn) b) ⇒ Fix fn '[a] b → TypeSpec (Fix fn) a → Specification (Fix fn) b Source #
(Typeable fn, Typeable fn', Typeable fnU, Functions (fn fnU) fnU, Functions (fn' fnU) fnU) ⇒ Functions (Oneof fn fn' fnU) fnU Source #
Instance details Defined in Constrained.Instances Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fnU a, All (HasSpec fnU) as) ⇒ Oneof fn fn' fnU as b → ListCtx Value as (HOLE a) → Specification fnU b → Specification fnU a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fnU b, All (HasSpec fnU) as) ⇒ Oneof fn fn' fnU as b → List (Term fnU) as → Maybe (Term fnU b) Source # mapTypeSpec ∷ (HasSpec fnU a, HasSpec fnU b) ⇒ Oneof fn fn' fnU '[a] b → TypeSpec fnU a → Specification fnU b Source #

data HOLE a b where Source #

This is used together with ListCtx to form just the arguments to `f vs Ctx vs'` - replacing Ctx with HOLE - to provide to propagateSpecFun.

Constructors

HOLE ∷ HOLE a a

type BaseUniverse fn = (Functions fn fn, Member (EqFn fn) fn, Member (SetFn fn) fn, Member (BoolFn fn) fn, Member (PairFn fn) fn, Member (IntFn fn) fn, Member (OrdFn fn) fn, Member (GenericsFn fn) fn, Member (ListFn fn) fn, Member (SumFn fn) fn, Member (MapFn fn) fn, Member (FunFn fn) fn, Member (SizeFn fn) fn) Source #

A minimal Universe contains functions for a bunch of different things.

type Member fn univ = IsMember fn univ (Path fn univ) Source #

type BaseFn = Fix (OneofL BaseFns) Source #

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

data Fix (fn ∷ Univ → Univ) (as ∷ [Type]) b Source #

Instances

Instances details

IsMember fn (fn' (Fix fn')) path ⇒ IsMember fn (Fix fn') ('PFix ': path) Source #
Instance details Defined in Constrained.Univ Methods injectFn0 ∷ ∀ (as ∷ [Type]) b. fn as b → Fix fn' as b Source # extractFn0 ∷ ∀ (as ∷ [Type]) b. Fix fn' as b → Maybe (fn as b) Source #
FunctionLike (fn (Fix fn)) ⇒ FunctionLike (Fix fn) Source #
Instance details Defined in Constrained.Univ Methods sem ∷ ∀ (as ∷ [Type]) b. Fix fn as b → FunTy as b Source #
(Typeable fn, Functions (fn (Fix fn)) (Fix fn)) ⇒ Functions (Fix fn) (Fix fn) Source #
Instance details Defined in Constrained.Instances Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec (Fix fn) a, All (HasSpec (Fix fn)) as) ⇒ Fix fn as b → ListCtx Value as (HOLE a) → Specification (Fix fn) b → Specification (Fix fn) a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec (Fix fn) b, All (HasSpec (Fix fn)) as) ⇒ Fix fn as b → List (Term (Fix fn)) as → Maybe (Term (Fix fn) b) Source # mapTypeSpec ∷ (HasSpec (Fix fn) a, HasSpec (Fix fn) b) ⇒ Fix fn '[a] b → TypeSpec (Fix fn) a → Specification (Fix fn) b Source #
Show (fn (Fix fn) as b) ⇒ Show (Fix fn as b) Source #
Instance details Defined in Constrained.Univ Methods showsPrec ∷ Int → Fix fn as b → ShowS Source # show ∷ Fix fn as b → String Source # showList ∷ [Fix fn as b] → ShowS Source #
Eq (fn (Fix fn) as b) ⇒ Eq (Fix fn as b) Source #
Instance details Defined in Constrained.Univ Methods (==) ∷ Fix fn as b → Fix fn as b → Bool Source # (/=) ∷ Fix fn as b → Fix fn as b → Bool Source #

type family OneofL as where ... Source #

Build a balanced tree of Oneof from a list of function universes. NOTE: it is important that this is a balanced tree as that reduces the amount of overhead in injectFn and extractFn from `O(n)` to `O(log(n))`. Surprisingly, we've observed this making more than 10% difference in runtime on some generation tasks even though the list as is typically small (< 20 elements).

Equations

OneofL '[t] = t
OneofL (t ': ts) = Insert t (OneofL ts)

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

type IsNormalType a = (Cases a ~ '[a], Args a ~ '[a], IsProd a) Source #

data Value a where Source #

Constructors

Value ∷ Show a ⇒ !a → Value a

Instances

Instances details

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

type family SOP constrs where ... Source #

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

Equations

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

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

A constructor name with the types of its arguments

Instances

Instances details

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

data MapFn (fn ∷ [Type] → Type → Type) args res Source #

Instances

Instances details

FunctionLike (MapFn fn) Source #
Instance details Defined in Constrained.Univ Methods sem ∷ ∀ (as ∷ [Type]) b. MapFn fn as b → FunTy as b Source #
BaseUniverse fn ⇒ Functions (MapFn fn) fn Source #
Instance details Defined in Constrained.Spec.Map Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ MapFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ MapFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ MapFn fn '[a] b → TypeSpec fn a → Specification fn b Source #
Show (MapFn fn args res) Source #
Instance details Defined in Constrained.Univ Methods showsPrec ∷ Int → MapFn fn args res → ShowS Source # show ∷ MapFn fn args res → String Source # showList ∷ [MapFn fn args res] → ShowS Source #
Eq (MapFn fn args res) Source #
Instance details Defined in Constrained.Univ Methods (==) ∷ MapFn fn args res → MapFn fn args res → Bool Source # (/=) ∷ MapFn fn args res → MapFn fn args res → Bool Source #

data FunFn fn args res Source #

Instances

Instances details

FunctionLike fn ⇒ FunctionLike (FunFn fn) Source #
Instance details Defined in Constrained.Base Methods sem ∷ ∀ (as ∷ [Type]) b. FunFn fn as b → FunTy as b Source #
(BaseUniverse fn, Member (FunFn fn) fn) ⇒ Functions (FunFn fn) fn Source #
Instance details Defined in Constrained.Base Methods propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, All (HasSpec fn) as) ⇒ FunFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ FunFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ FunFn fn '[a] b → TypeSpec fn a → Specification fn b Source #
Show (FunFn fn args res) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → FunFn fn args res → ShowS Source # show ∷ FunFn fn args res → String Source # showList ∷ [FunFn fn args res] → ShowS Source #
Typeable fn ⇒ Eq (FunFn fn args res) Source #
Instance details Defined in Constrained.Base Methods (==) ∷ FunFn fn args res → FunFn fn args res → Bool Source # (/=) ∷ FunFn fn args res → FunFn fn args res → Bool Source #

data PairSpec fn a b Source #

Constructors

Cartesian (Specification fn a) (Specification fn b)

Instances

Instances details

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

data MapSpec fn k v Source #

Constructors

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

Instances

Instances details

(HasSpec fn (k, v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) ⇒ Pretty (WithPrec (MapSpec fn k v)) Source #
Instance details Defined in Constrained.Spec.Map Methods pretty ∷ WithPrec (MapSpec fn k v) → Doc ann Source # prettyList ∷ [WithPrec (MapSpec fn k v)] → Doc ann Source #
(Arbitrary k, Arbitrary v, Arbitrary (TypeSpec fn k), Arbitrary (TypeSpec fn v), Ord k, HasSpec fn k, Foldy fn v) ⇒ Arbitrary (MapSpec fn k v) Source #
Instance details Defined in Constrained.Spec.Map Methods arbitrary ∷ Gen (MapSpec fn k v) Source # shrink ∷ MapSpec fn k v → [MapSpec fn k v] Source #
(HasSpec fn (k, v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) ⇒ Show (MapSpec fn k v) Source #
Instance details Defined in Constrained.Spec.Map Methods showsPrec ∷ Int → MapSpec fn k v → ShowS Source # show ∷ MapSpec fn k v → String Source # showList ∷ [MapSpec fn k v] → ShowS Source #

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

Constructors

NoFold ∷ FoldSpec fn a
FoldSpec ∷ ∀ b fn a. (HasSpec fn a, HasSpec fn b, Foldy fn b, Member (ListFn fn) fn, BaseUniverse fn) ⇒ fn '[a] b → Specification fn b → FoldSpec fn a

Instances

Instances details

Arbitrary (FoldSpec fn (Map k v)) Source #
Instance details Defined in Constrained.Spec.Map Methods arbitrary ∷ Gen (FoldSpec fn (Map k v)) Source # shrink ∷ FoldSpec fn (Map k v) → [FoldSpec fn (Map k v)] Source #
Arbitrary (FoldSpec fn (Set a)) Source #
Instance details Defined in Constrained.Base Methods arbitrary ∷ Gen (FoldSpec fn (Set a)) Source # shrink ∷ FoldSpec fn (Set a) → [FoldSpec fn (Set a)] Source #
(HasSpec fn a, HasSpec fn b, Arbitrary (FoldSpec fn a), Arbitrary (FoldSpec fn b)) ⇒ Arbitrary (FoldSpec fn (a, b)) Source #
Instance details Defined in Constrained.Spec.Generics Methods arbitrary ∷ Gen (FoldSpec fn (a, b)) Source # shrink ∷ FoldSpec fn (a, b) → [FoldSpec fn (a, b)] Source #
(Arbitrary a, Arbitrary (TypeSpec fn a), Foldy fn a, BaseUniverse fn) ⇒ Arbitrary (FoldSpec fn a) Source #
Instance details Defined in Constrained.Base Methods arbitrary ∷ Gen (FoldSpec fn a) Source # shrink ∷ FoldSpec fn a → [FoldSpec fn a] Source #
Show (FoldSpec fn a) Source #
Instance details Defined in Constrained.Base Methods showsPrec ∷ Int → FoldSpec fn a → ShowS Source # show ∷ FoldSpec fn a → String Source # showList ∷ [FoldSpec fn a] → ShowS Source #

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

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

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

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

A version of genFromSpec that simply errors if the generator fails

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

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

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

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

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

monitorSpec ∷ (FunctionLike fn, Testable p) ⇒ Specification fn a → a → p → Property Source #

Collect the monitor calls from a specification instantiated to the given value. Typically,

>>> quickCheck $ forAll (genFromSpec_ spec) $ \ x -> monitorSpec spec x $ ...

forAllSpec ∷ (HasSpec fn a, Testable p) ⇒ Specification fn a → (a → p) → Property Source #

forAllSpecShow ∷ (HasSpec fn a, Testable p) ⇒ Specification fn a → (a → String) → (a → p) → Property Source #

giveHint ∷ HasGenHint fn a ⇒ Hint a → Specification fn a Source #

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

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

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

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

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

caseBoolSpec ∷ HasSpec fn a ⇒ Specification fn Bool → (Bool → Specification fn a) → Specification fn a Source #

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

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

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

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

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

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

match ∷ ∀ fn p a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, Cases (SimpleRep a) ~ '[SimpleRep a], SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), IsProd (SimpleRep a), All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn) ⇒ Term fn a → FunTy (MapList (Term fn) (Args (SimpleRep a))) p → Pred fn Source #

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

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

caseOn ∷ ∀ fn a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) ⇒ Term fn a → FunTy (MapList (Binder fn) (Cases (SimpleRep a))) (Pred fn) Source #

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

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

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

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

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

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

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

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

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

monitor ∷ ((∀ a. Term fn a → a) → Property → Property) → Pred fn Source #

Add QuickCheck monitoring (e.g. collect or counterexample) to a predicate. To use the monitoring in a property call monitorSpec on the Specification containing the monitoring and a value generated from the specification.

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

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

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

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

Like forAll but pattern matches on the `Term fn a`

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

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

fst_ ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ Term fn (a, b) → Term fn a Source #

snd_ ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ Term fn (a, b) → Term fn b Source #

pair_ ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ Term fn a → Term fn b → Term fn (a, b) Source #

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

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

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

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

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

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

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

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

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

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

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

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

sum_ ∷ (BaseUniverse fn, Member (FunFn fn) fn, Foldy fn a) ⇒ Term fn [a] → Term fn a Source #

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

special instance of sizeOf (for Sets) for backward compatibility

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

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

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

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

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

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

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

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

special instance of sizeOf (for Lists) for backward compatibility

injectFn ∷ ∀ fn fnU as b. Member fn fnU ⇒ fn as b → fnU as b Source #

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

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

emptyNumSpec ∷ Ord a ⇒ NumSpec a Source #

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

genFromNumSpec ∷ (MonadGenError m, Show n, Random n, Ord n, Num n, MaybeBounded n) ⇒ NumSpec n → GenT m n Source #

shrinkWithNumSpec ∷ Arbitrary n ⇒ NumSpec n → n → [n] Source #

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

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

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

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

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

algebra ∷ SOPLike constrs r ⇒ SOP constrs → ALG constrs r Source #

Run a SOP

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

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

module Constrained.Spec.Tree

module Constrained.List

module Constrained.GenT