| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Constrained.API
Synopsis
- class LogicRequires s t dom rng ⇒ Logic s t dom rng | s → t where
- info ∷ t s dom rng → String
- propagate ∷ Context s t dom rng hole → Specification rng → Specification hole
- rewriteRules ∷ (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ t s dom rng → List Term dom → Evidence (AppRequires s t dom rng) → Maybe (Term rng)
- mapTypeSpec ∷ ∀ a b. (dom ~ '[a], rng ~ b, HasSpec a, HasSpec b) ⇒ t s '[a] b → TypeSpec a → Specification b
- saturate ∷ t s dom Bool → List Term dom → [Pred]
- class Syntax t ⇒ Semantics (t ∷ Symbol → [Type] → Type → Type) where
- class Syntax (t ∷ FSType) where
- class (HasSpec a, NumLike a, Logic "addFn" IntW '[a, a] a) ⇒ Foldy a where
- genList ∷ MonadGenError m ⇒ Specification a → Specification a → GenT m [a]
- theAddFn ∷ IntW "addFn" '[a, a] a
- theZero ∷ a
- genSizedList ∷ MonadGenError m ⇒ Specification Integer → Specification a → Specification a → GenT m [a]
- noNegativeValues ∷ Bool
- data BaseW (sym ∷ Symbol) (dom ∷ [Type]) (rng ∷ Type) where
- InjLeftW ∷ ∀ a b. BaseW "leftFn" '[a] (Sum a b)
- InjRightW ∷ ∀ a b. BaseW "rightFn" '[b] (Sum a b)
- ProdW ∷ ∀ a b. BaseW "prod_" '[a, b] (Prod a b)
- ProdFstW ∷ ∀ a b. BaseW "prodFst_" '[Prod a b] a
- ProdSndW ∷ ∀ a b. BaseW "prodSnd_" '[Prod a b] b
- EqualW ∷ ∀ a. Eq a ⇒ BaseW "==." '[a, a] Bool
- ToGenericW ∷ GenericRequires a ⇒ BaseW "toGenericFn" '[a] (SimpleRep a)
- FromGenericW ∷ GenericRequires a ⇒ BaseW "fromGenericFn" '[SimpleRep a] a
- ElemW ∷ ∀ a. Eq a ⇒ BaseW "elem_" '[a, [a]] Bool
- data BoolW (sym ∷ Symbol) (dom ∷ [Type]) (rng ∷ Type) where
- data NumOrdW (sym ∷ Symbol) (dom ∷ [Type]) (rng ∷ Type) where
- data IntW (s ∷ Symbol) (as ∷ [Type]) b where
- data SizeW (s ∷ Symbol) (dom ∷ [Type]) rng ∷ Type where
- data FunW (sym ∷ Symbol) (dom ∷ [Type]) (rng ∷ Type) where
- data ListW (s ∷ Symbol) (args ∷ [Type]) (res ∷ Type) where
- data MapW (sym ∷ Symbol) (dom ∷ [Type]) (rng ∷ Type) where
- data NumSpec n = NumSpecInterval (Maybe n) (Maybe n)
- class MaybeBounded a where
- lowerBound ∷ Maybe a
- upperBound ∷ Maybe a
- data NonEmpty a = a :| [a]
- data Specification a where
- ExplainSpec ∷ [String] → Specification a → Specification a
- MemberSpec ∷ NonEmpty a → Specification a
- ErrorSpec ∷ NonEmpty String → Specification a
- SuspendedSpec ∷ HasSpec a ⇒ Var a → Pred → Specification a
- TypeSpec ∷ HasSpec a ⇒ TypeSpec a → [a] → Specification a
- TrueSpec ∷ Specification a
- data Term a where
- data Fun dom rng where
- name ∷ String → Term a → Term a
- named ∷ String → Term a → Term a
- data Pred where
- ElemPred ∷ ∀ a. HasSpec a ⇒ Bool → Term a → NonEmpty a → Pred
- Monitor ∷ ((∀ a. Term a → a) → Property → Property) → Pred
- And ∷ [Pred] → Pred
- Exists ∷ ((∀ b. Term b → b) → GE a) → Binder a → Pred
- Subst ∷ HasSpec a ⇒ Var a → Term a → Pred → Pred
- Let ∷ Term a → Binder a → Pred
- Assert ∷ Term Bool → Pred
- Reifies ∷ (HasSpec a, HasSpec b) ⇒ Term b → Term a → (a → b) → Pred
- DependsOn ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Pred
- ForAll ∷ (Forallable t a, HasSpec t, HasSpec a) ⇒ Term t → Binder a → Pred
- Case ∷ HasSpec (SumOver as) ⇒ Term (SumOver as) → List (Weighted Binder) as → Pred
- When ∷ HasSpec Bool ⇒ Term Bool → Pred → Pred
- GenHint ∷ HasGenHint a ⇒ Hint a → Term a → Pred
- TruePred ∷ Pred
- FalsePred ∷ NonEmpty String → Pred
- Explain ∷ NonEmpty String → Pred → Pred
- type Literal a = (Typeable a, Eq a, Show a)
- class (Typeable a, Eq a, Show a, Show (TypeSpec a), Typeable (TypeSpec a)) ⇒ HasSpec a where
- type TypeSpec a
- type Prerequisites a ∷ Constraint
- emptySpec ∷ TypeSpec a
- combineSpec ∷ TypeSpec a → TypeSpec a → Specification a
- genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a
- conformsTo ∷ HasCallStack ⇒ a → TypeSpec a → Bool
- shrinkWithTypeSpec ∷ TypeSpec a → a → [a]
- toPreds ∷ Term a → TypeSpec a → Pred
- cardinalTypeSpec ∷ TypeSpec a → Specification Integer
- cardinalTrueSpec ∷ Specification Integer
- typeSpecHasError ∷ TypeSpec a → Maybe (NonEmpty String)
- alternateShow ∷ TypeSpec a → BinaryShow
- monadConformsTo ∷ a → TypeSpec a → Writer [String] Bool
- typeSpecOpt ∷ TypeSpec a → [a] → Specification a
- guardTypeSpec ∷ [String] → TypeSpec a → Specification a
- prerequisites ∷ Evidence (Prerequisites a)
- class Typeable (SimpleRep a) ⇒ HasSimpleRep a where
- type SimpleRep a
- type TheSop a ∷ [Type]
- toSimpleRep ∷ a → SimpleRep a
- fromSimpleRep ∷ SimpleRep a → a
- class (Ord a, HasSpec a) ⇒ OrdLike a where
- leqSpec ∷ a → Specification a
- ltSpec ∷ a → Specification a
- geqSpec ∷ a → Specification a
- gtSpec ∷ a → Specification a
- conformsToSpecE ∷ ∀ a. HasSpec a ⇒ a → Specification a → NonEmpty String → Maybe (NonEmpty String)
- conformsToSpec ∷ HasSpec a ⇒ a → Specification a → Bool
- satisfies ∷ ∀ a. HasSpec a ⇒ Term a → Specification a → Pred
- genFromSpecT ∷ ∀ a m. (HasCallStack, HasSpec a, MonadGenError m) ⇒ Specification a → GenT m a
- genFromSpec ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Specification a → Gen a
- debugSpec ∷ ∀ a. HasSpec a ⇒ Specification a → IO ()
- genFromSpecWithSeed ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Int → Int → Specification a → a
- simplifySpec ∷ HasSpec a ⇒ Specification a → Specification a
- cardinality ∷ ∀ a. (Number Integer, HasSpec a) ⇒ Specification a → Specification Integer
- ifElse ∷ (IsPred p, IsPred q) ⇒ Term Bool → p → q → Pred
- whenTrue ∷ ∀ p. IsPred p ⇒ Term Bool → p → Pred
- simplifyTerm ∷ ∀ a. Term a → Term a
- constrained ∷ ∀ a p. (IsPred p, HasSpec a) ⇒ (Term a → p) → Specification a
- assertExplain ∷ IsPred p ⇒ NonEmpty String → p → Pred
- assert ∷ IsPred p ⇒ p → Pred
- forAll ∷ (Forallable t a, HasSpec t, HasSpec a, IsPred p) ⇒ Term t → (Term a → p) → Pred
- exists ∷ ∀ a p. (HasSpec a, IsPred p) ⇒ ((∀ b. Term b → b) → GE a) → (Term a → p) → Pred
- unsafeExists ∷ ∀ a p. (HasSpec a, IsPred p) ⇒ (Term a → p) → Pred
- letBind ∷ (HasSpec a, IsPred p) ⇒ Term a → (Term a → p) → Pred
- reify ∷ (HasSpec a, HasSpec b, IsPred p) ⇒ Term a → (a → b) → (Term b → p) → Pred
- assertReified ∷ (HasSpec Bool, HasSpec a) ⇒ Term a → (a → Bool) → Pred
- explanation ∷ NonEmpty String → Pred → Pred
- monitor ∷ ((∀ a. Term a → a) → Property → Property) → Pred
- reifies ∷ (HasSpec a, HasSpec b) ⇒ Term b → Term a → (a → b) → Pred
- dependsOn ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Pred
- lit ∷ HasSpec a ⇒ a → Term a
- genHint ∷ ∀ t. HasGenHint t ⇒ Hint t → Term t → Pred
- giveHint ∷ HasGenHint a ⇒ Hint a → Specification a
- (<.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool
- (<=.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool
- (>=.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool
- (>.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool
- (==.) ∷ HasSpec a ⇒ Term a → Term a → Term Bool
- (/=.) ∷ HasSpec a ⇒ Term a → Term a → Term Bool
- not_ ∷ Term Bool → Term Bool
- or_ ∷ Term Bool → Term Bool → Term Bool
- (||.) ∷ Term Bool → Term Bool → Term Bool
- toGeneric_ ∷ ∀ a. GenericRequires a ⇒ Term a → Term (SimpleRep a)
- fromGeneric_ ∷ ∀ a. (GenericRequires a, AppRequires "fromGenericFn" BaseW '[SimpleRep a] a) ⇒ Term (SimpleRep a) → Term a
- (+.) ∷ NumLike a ⇒ Term a → Term a → Term a
- (-.) ∷ Numeric n ⇒ Term n → Term n → Term n
- negate_ ∷ NumLike a ⇒ Term a → Term a
- addFn ∷ ∀ a. NumLike a ⇒ Term a → Term a → Term a
- negateFn ∷ ∀ a. NumLike a ⇒ Term a → Term a
- type Numeric a = (HasSpec a, Ord a, Num a, TypeSpec a ~ NumSpec a, MaybeBounded a)
- pair_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term b → Term (a, b)
- fst_ ∷ (HasSpec x, HasSpec y) ⇒ Term (x, y) → Term x
- snd_ ∷ (HasSpec x, HasSpec y) ⇒ Term (x, y) → Term y
- prodSnd_ ∷ (HasSpec a, HasSpec b) ⇒ Term (Prod a b) → Term b
- prodFst_ ∷ (HasSpec a, HasSpec b) ⇒ Term (Prod a b) → Term a
- prod_ ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Term (Prod a b)
- type IsNormalType a = (Cases a ~ '[a], Args a ~ '[a], IsProd a, CountCases a ~ 1)
- leftFn ∷ (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Term a → Term (Sum a b)
- rightFn ∷ (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Term b → Term (Sum a b)
- left_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term (Either a b)
- right_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term b → Term (Either a b)
- cJust_ ∷ (HasSpec a, IsNormalType a) ⇒ Term a → Term (Maybe a)
- cNothing_ ∷ (HasSpec a, IsNormalType a) ⇒ Term (Maybe a)
- caseOn ∷ ∀ a. (HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) ⇒ Term a → FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
- branch ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ FunTy (MapList Term (Args a)) p → Weighted Binder a
- branchW ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ Int → FunTy (MapList Term (Args a)) p → Weighted Binder a
- forAll' ∷ ∀ t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t, HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a), HasSpec a) ⇒ Term t → FunTy (MapList Term (Args (SimpleRep a))) p → Pred
- constrained' ∷ ∀ a p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec a, IsPred p) ⇒ FunTy (MapList Term (Args (SimpleRep a))) p → Specification a
- reify' ∷ ∀ a b p. (Cases (SimpleRep b) ~ '[SimpleRep b], TypeSpec b ~ TypeSpec (SimpleRep b), HasSpec (SimpleRep b), HasSimpleRep b, All HasSpec (Args (SimpleRep b)), IsProd (SimpleRep b), HasSpec a, HasSpec b, IsPred p) ⇒ Term a → (a → b) → FunTy (MapList Term (Args (SimpleRep b))) p → Pred
- con ∷ ∀ c a r. (SimpleRep a ~ SOP (TheSop a), TypeSpec a ~ TypeSpec (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), HasSpec a, HasSimpleRep a, r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a), ResultType r ~ Term a, SOPTerm c (TheSop a), ConstrTerm (ConstrOf c (TheSop a))) ⇒ r
- onCon ∷ ∀ c a p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a, HasSpec (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All HasSpec (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term a → FunTy (MapList Term (ConstrOf c (TheSop a))) p → Pred
- isCon ∷ ∀ c a. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a, HasSpec (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term a → Pred
- sel ∷ ∀ n a c as. (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a, HasSpec (ProdOver as), HasSimpleRep a) ⇒ Term a → Term (At n as)
- match ∷ ∀ p a. (HasSpec a, IsProductType a, IsPred p) ⇒ Term a → FunTy (MapList Term (ProductAsList a)) p → Pred
- onJust ∷ ∀ a p. (HasSpec a, IsNormalType a, IsPred p) ⇒ Term (Maybe a) → (Term a → p) → Pred
- isJust ∷ ∀ a. (HasSpec a, IsNormalType a) ⇒ Term (Maybe a) → Pred
- chooseSpec ∷ HasSpec a ⇒ (Int, Specification a) → (Int, Specification a) → Specification a
- equalSpec ∷ a → Specification a
- notEqualSpec ∷ ∀ a. HasSpec a ⇒ a → Specification a
- notMemberSpec ∷ ∀ a f. (HasSpec a, Foldable f) ⇒ f a → Specification a
- id_ ∷ ∀ a. HasSpec a ⇒ Term a → Term a
- flip_ ∷ ∀ (t ∷ FSType) (sym ∷ Symbol) a b r. (HasSpec b, HasSpec a, HasSpec r, ∀ sym1 t1. Logic sym1 t1 '[a, b] r) ⇒ t sym '[a, b] r → Term b → Term a → Term r
- compose_ ∷ ∀ b s1 s2 t1 t2 a r. (AppRequires s1 t1 '[b] r, AppRequires s2 t2 '[a] b) ⇒ t1 s1 '[b] r → t2 s2 '[a] b → Term a → Term r
- foldMap_ ∷ ∀ a b. (Sized [a], Foldy b, HasSpec a) ⇒ (Term a → Term b) → Term [a] → Term b
- sum_ ∷ Foldy a ⇒ Term [a] → Term a
- elem_ ∷ (Sized [a], HasSpec a) ⇒ Term a → Term [a] → Term Bool
- singletonList_ ∷ (Sized [a], HasSpec a) ⇒ Term a → Term [a]
- append_ ∷ (Sized [a], HasSpec a) ⇒ Term [a] → Term [a] → Term [a]
- (++.) ∷ HasSpec a ⇒ Term [a] → Term [a] → Term [a]
- sizeOf ∷ Sized t ⇒ t → Integer
- sizeOf_ ∷ (HasSpec t, Sized t) ⇒ Term t → Term Integer
- null_ ∷ (HasSpec a, Sized a) ⇒ Term a → Term Bool
- hasSize ∷ (HasSpec t, Sized t) ⇒ SizeSpec → Specification t
- rangeSize ∷ Integer → Integer → SizeSpec
- length_ ∷ HasSpec a ⇒ Term [a] → Term Integer
- genFromSizeSpec ∷ MonadGenError m ⇒ Specification Integer → GenT m Integer
- between ∷ (HasSpec a, TypeSpec a ~ NumSpec a) ⇒ a → a → Specification a
- maxSpec ∷ Specification Integer → Specification Integer
- data SetW (s ∷ Symbol) (d ∷ [Type]) (r ∷ Type) where
- SingletonW ∷ Ord a ⇒ SetW "singleton_" '[a] (Set a)
- UnionW ∷ (Literal a, Ord a) ⇒ SetW "union_" '[Set a, Set a] (Set a)
- SubsetW ∷ (Literal a, Ord a) ⇒ SetW "subset_" '[Set a, Set a] Bool
- MemberW ∷ (Literal a, Ord a) ⇒ SetW "member_" '[a, Set a] Bool
- DisjointW ∷ (Literal a, Ord a) ⇒ SetW "disjoint_" '[Set a, Set a] Bool
- FromListW ∷ ∀ a. (HasSpec a, Ord a) ⇒ SetW "fromList_" '[[a]] (Set a)
- data SetSpec a = SetSpec (Set a) (Specification a) (Specification Integer)
- singleton_ ∷ (Ord a, HasSpec a) ⇒ Term a → Term (Set a)
- member_ ∷ (Ord a, HasSpec a) ⇒ Term a → Term (Set a) → Term Bool
- union_ ∷ (Ord a, HasSpec a) ⇒ Term (Set a) → Term (Set a) → Term (Set a)
- subset_ ∷ (Ord a, HasSpec a) ⇒ Term (Set a) → Term (Set a) → Term Bool
- disjoint_ ∷ (Ord a, HasSpec a) ⇒ Term (Set a) → Term (Set a) → Term Bool
- fromList_ ∷ ∀ a. (Ord a, HasSpec a) ⇒ Term [a] → Term (Set a)
- pattern Equal ∷ ∀ b. () ⇒ ∀ a. (b ~ Bool, Eq a, HasSpec a) ⇒ Term a → Term a → Term b
- pattern Elem ∷ ∀ b. () ⇒ ∀ a. (b ~ Bool, Eq a, HasSpec a) ⇒ Term a → Term [a] → Term b
- pattern ToGeneric ∷ ∀ rng. () ⇒ ∀ a. (rng ~ SimpleRep a, GenericRequires a, HasSpec a, AppRequires "toGenericFn" BaseW '[a] rng) ⇒ Term a → Term rng
- pattern FromGeneric ∷ ∀ rng. () ⇒ ∀ a. (rng ~ a, GenericRequires a, HasSpec a, AppRequires "fromGenericFn" BaseW '[SimpleRep a] rng) ⇒ Term (SimpleRep a) → Term rng
- pattern InjLeft ∷ ∀ c. () ⇒ ∀ a b. (c ~ Sum a b, AppRequires "leftFn" BaseW '[a] c) ⇒ Term a → Term c
- pattern InjRight ∷ ∀ c. () ⇒ ∀ a b. (c ~ Sum a b, AppRequires "rightFn" BaseW '[b] c) ⇒ Term b → Term c
- pattern ProdFst ∷ ∀ c. () ⇒ ∀ a b. (c ~ a, Typeable (Prod a b), HasSpec a, AppRequires "prodFst_" BaseW '[Prod a b] a) ⇒ Term (Prod a b) → Term c
- pattern ProdSnd ∷ ∀ c. () ⇒ ∀ a b. (c ~ b, Typeable (Prod a b), HasSpec b, AppRequires "prodSnd_" BaseW '[Prod a b] b) ⇒ Term (Prod a b) → Term c
- pattern Product ∷ ∀ c. () ⇒ ∀ a b. (c ~ Prod a b, AppRequires "prod_" BaseW '[a, b] c) ⇒ Term a → Term b → Term c
- printPlan ∷ HasSpec a ⇒ Specification a → IO ()
- class (Num a, HasSpec a) ⇒ NumLike a
- data PairSpec a b = Cartesian (Specification a) (Specification b)
- data MapSpec k v = MapSpec {
- mapSpecHint ∷ Maybe Integer
- mapSpecMustKeys ∷ Set k
- mapSpecMustValues ∷ [v]
- mapSpecSize ∷ Specification Integer
- mapSpecElem ∷ Specification (k, v)
- mapSpecFold ∷ FoldSpec v
- dom_ ∷ (HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term (Set k)
- rng_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term [v]
- lookup_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term k → Term (Map k v) → Term (Maybe v)
- fstSpec ∷ ∀ k v. (HasSpec k, HasSpec v) ⇒ Specification (k, v) → Specification k
- sndSpec ∷ ∀ k v. (HasSpec k, HasSpec v) ⇒ Specification (k, v) → Specification v
- var ∷ QuasiQuoter
- data Prod a b = Prod {}
Documentation
class LogicRequires s t dom rng ⇒ Logic s t dom rng | s → t where Source #
Logical operations are one that support reasoning about how a function symbol relates to logical properties, that we call Specification's
Minimal complete definition
Methods
info ∷ t s dom rng → String Source #
propagate ∷ Context s t dom rng hole → Specification rng → Specification hole Source #
rewriteRules ∷ (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ t s dom rng → List Term dom → Evidence (AppRequires s t dom rng) → Maybe (Term rng) Source #
mapTypeSpec ∷ ∀ a b. (dom ~ '[a], rng ~ b, HasSpec a, HasSpec b) ⇒ t s '[a] b → TypeSpec a → Specification b Source #
Instances
| OrdLike a ⇒ Logic "<." NumOrdW '[a, a] Bool Source # | |
Defined in Constrained.TheKnot Methods info ∷ NumOrdW "<." '[a, a] Bool → String Source # propagate ∷ Context "<." NumOrdW '[a, a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ NumOrdW "<." '[a, a] Bool → List Term '[a, a] → Evidence (AppRequires "<." NumOrdW '[a, a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ NumOrdW "<." '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ NumOrdW "<." '[a, a] Bool → List Term '[a, a] → [Pred] Source # | |
| OrdLike a ⇒ Logic "<=." NumOrdW '[a, a] Bool Source # | |
Defined in Constrained.TheKnot Methods info ∷ NumOrdW "<=." '[a, a] Bool → String Source # propagate ∷ Context "<=." NumOrdW '[a, a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ NumOrdW "<=." '[a, a] Bool → List Term '[a, a] → Evidence (AppRequires "<=." NumOrdW '[a, a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ NumOrdW "<=." '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ NumOrdW "<=." '[a, a] Bool → List Term '[a, a] → [Pred] Source # | |
| (HasSpec Bool, Eq a, Typeable a) ⇒ Logic "==." BaseW '[a, a] Bool Source # | |
Defined in Constrained.TheKnot Methods info ∷ BaseW "==." '[a, a] Bool → String Source # propagate ∷ Context "==." BaseW '[a, a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ BaseW "==." '[a, a] Bool → List Term '[a, a] → Evidence (AppRequires "==." BaseW '[a, a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ BaseW "==." '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ BaseW "==." '[a, a] Bool → List Term '[a, a] → [Pred] Source # | |
| OrdLike a ⇒ Logic ">." NumOrdW '[a, a] Bool Source # | |
Defined in Constrained.TheKnot Methods info ∷ NumOrdW ">." '[a, a] Bool → String Source # propagate ∷ Context ">." NumOrdW '[a, a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ NumOrdW ">." '[a, a] Bool → List Term '[a, a] → Evidence (AppRequires ">." NumOrdW '[a, a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ NumOrdW ">." '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ NumOrdW ">." '[a, a] Bool → List Term '[a, a] → [Pred] Source # | |
| OrdLike a ⇒ Logic ">=." NumOrdW '[a, a] Bool Source # | |
Defined in Constrained.TheKnot Methods info ∷ NumOrdW ">=." '[a, a] Bool → String Source # propagate ∷ Context ">=." NumOrdW '[a, a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ NumOrdW ">=." '[a, a] Bool → List Term '[a, a] → Evidence (AppRequires ">=." NumOrdW '[a, a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ NumOrdW ">=." '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ NumOrdW ">=." '[a, a] Bool → List Term '[a, a] → [Pred] Source # | |
| NumLike a ⇒ Logic "addFn" IntW '[a, a] a Source # | Just a note that these instances won't work until we are in a context where
there is a HasSpec instance of |
Defined in Constrained.NumSpec Methods info ∷ IntW "addFn" '[a, a] a → String Source # propagate ∷ Context "addFn" IntW '[a, a] a hole → Specification a → Specification hole Source # rewriteRules ∷ IntW "addFn" '[a, a] a → List Term '[a, a] → Evidence (AppRequires "addFn" IntW '[a, a] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], a ~ b, HasSpec a0, HasSpec b) ⇒ IntW "addFn" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ IntW "addFn" '[a, a] Bool → List Term '[a, a] → [Pred] Source # | |
| (All (Typeable ∷ Type → Constraint) '[a, r], HasSpec r) ⇒ Logic "composeFn" FunW '[a] r Source # | |
Defined in Constrained.Spec.ListFoldy Methods info ∷ FunW "composeFn" '[a] r → String Source # propagate ∷ Context "composeFn" FunW '[a] r hole → Specification r → Specification hole Source # rewriteRules ∷ FunW "composeFn" '[a] r → List Term '[a] → Evidence (AppRequires "composeFn" FunW '[a] r) → Maybe (Term r) Source # mapTypeSpec ∷ ('[a] ~ '[a0], r ~ b, HasSpec a0, HasSpec b) ⇒ FunW "composeFn" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ FunW "composeFn" '[a] Bool → List Term '[a] → [Pred] Source # | |
| (HasSpec a, Ord a) ⇒ Logic "disjoint_" SetW '[Set a, Set a] Bool Source # | |
Defined in Constrained.Spec.Set Methods info ∷ SetW "disjoint_" '[Set a, Set a] Bool → String Source # propagate ∷ Context "disjoint_" SetW '[Set a, Set a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ SetW "disjoint_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → Evidence (AppRequires "disjoint_" SetW '[Set a, Set a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[Set a, Set a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ SetW "disjoint_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "disjoint_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → [Pred] Source # | |
| HasSpec a ⇒ Logic "elem_" BaseW '[a, [a]] Bool Source # | |
Defined in Constrained.Spec.ListFoldy Methods info ∷ BaseW "elem_" '[a, [a]] Bool → String Source # propagate ∷ Context "elem_" BaseW '[a, [a]] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ BaseW "elem_" '[a, [a]] Bool → List Term '[a, [a]] → Evidence (AppRequires "elem_" BaseW '[a, [a]] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, [a]] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ BaseW "elem_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ BaseW "elem_" '[a, [a]] Bool → List Term '[a, [a]] → [Pred] Source # | |
| (∀ (sym ∷ Symbol) (t ∷ Symbol → [Type] → Type → Type). Logic sym t '[a, b] r, All (Typeable ∷ Type → Constraint) '[a, b, r]) ⇒ Logic "flip_" FunW '[b, a] r Source # | |
Defined in Constrained.Spec.ListFoldy Methods info ∷ FunW "flip_" '[b, a] r → String Source # propagate ∷ Context "flip_" FunW '[b, a] r hole → Specification r → Specification hole Source # rewriteRules ∷ FunW "flip_" '[b, a] r → List Term '[b, a] → Evidence (AppRequires "flip_" FunW '[b, a] r) → Maybe (Term r) Source # mapTypeSpec ∷ ('[b, a] ~ '[a0], r ~ b0, HasSpec a0, HasSpec b0) ⇒ FunW "flip_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ FunW "flip_" '[b, a] Bool → List Term '[b, a] → [Pred] Source # | |
| (Typeable a, Foldy b) ⇒ Logic "foldMap_" ListW '[[a]] b Source # | |
Defined in Constrained.Spec.ListFoldy Methods info ∷ ListW "foldMap_" '[[a]] b → String Source # propagate ∷ Context "foldMap_" ListW '[[a]] b hole → Specification b → Specification hole Source # rewriteRules ∷ ListW "foldMap_" '[[a]] b → List Term '[[a]] → Evidence (AppRequires "foldMap_" ListW '[[a]] b) → Maybe (Term b) Source # mapTypeSpec ∷ ('[[a]] ~ '[a0], b ~ b0, HasSpec a0, HasSpec b0) ⇒ ListW "foldMap_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ ListW "foldMap_" '[[a]] Bool → List Term '[[a]] → [Pred] Source # | |
| (GenericRequires a, dom ~ SimpleRep a) ⇒ Logic "fromGenericFn" BaseW '[dom] a Source # | |
Defined in Constrained.Base Methods info ∷ BaseW "fromGenericFn" '[dom] a → String Source # propagate ∷ Context "fromGenericFn" BaseW '[dom] a hole → Specification a → Specification hole Source # rewriteRules ∷ BaseW "fromGenericFn" '[dom] a → List Term '[dom] → Evidence (AppRequires "fromGenericFn" BaseW '[dom] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[dom] ~ '[a0], a ~ b, HasSpec a0, HasSpec b) ⇒ BaseW "fromGenericFn" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ BaseW "fromGenericFn" '[dom] Bool → List Term '[dom] → [Pred] Source # | |
| HasSpec a ⇒ Logic "id_" FunW '[a] a Source # | |
Defined in Constrained.Spec.ListFoldy Methods info ∷ FunW "id_" '[a] a → String Source # propagate ∷ Context "id_" FunW '[a] a hole → Specification a → Specification hole Source # rewriteRules ∷ FunW "id_" '[a] a → List Term '[a] → Evidence (AppRequires "id_" FunW '[a] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[a] ~ '[a0], a ~ b, HasSpec a0, HasSpec b) ⇒ FunW "id_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ FunW "id_" '[a] Bool → List Term '[a] → [Pred] Source # | |
| (HasSpec a, Ord a) ⇒ Logic "member_" SetW '[a, Set a] Bool Source # | |
Defined in Constrained.Spec.Set Methods info ∷ SetW "member_" '[a, Set a] Bool → String Source # propagate ∷ Context "member_" SetW '[a, Set a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ SetW "member_" '[a, Set a] Bool → List Term '[a, Set a] → Evidence (AppRequires "member_" SetW '[a, Set a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, Set a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ SetW "member_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "member_" '[a, Set a] Bool → List Term '[a, Set a] → [Pred] Source # | |
| NumLike a ⇒ Logic "negateFn" IntW '[a] a Source # | |
Defined in Constrained.NumSpec Methods info ∷ IntW "negateFn" '[a] a → String Source # propagate ∷ Context "negateFn" IntW '[a] a hole → Specification a → Specification hole Source # rewriteRules ∷ IntW "negateFn" '[a] a → List Term '[a] → Evidence (AppRequires "negateFn" IntW '[a] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[a] ~ '[a0], a ~ b, HasSpec a0, HasSpec b) ⇒ IntW "negateFn" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ IntW "negateFn" '[a] Bool → List Term '[a] → [Pred] Source # | |
| (HasSpec Bool, TypeSpec Bool ~ SumSpec () ()) ⇒ Logic "not_" BoolW '[Bool] Bool Source # | |
Defined in Constrained.TheKnot Methods info ∷ BoolW "not_" '[Bool] Bool → String Source # propagate ∷ Context "not_" BoolW '[Bool] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ BoolW "not_" '[Bool] Bool → List Term '[Bool] → Evidence (AppRequires "not_" BoolW '[Bool] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[Bool] ~ '[a], Bool ~ b, HasSpec a, HasSpec b) ⇒ BoolW "not_" '[a] b → TypeSpec a → Specification b Source # saturate ∷ BoolW "not_" '[Bool] Bool → List Term '[Bool] → [Pred] Source # | |
| HasSpec Bool ⇒ Logic "or_" BoolW '[Bool, Bool] Bool Source # | |
Defined in Constrained.TheKnot Methods info ∷ BoolW "or_" '[Bool, Bool] Bool → String Source # propagate ∷ Context "or_" BoolW '[Bool, Bool] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ BoolW "or_" '[Bool, Bool] Bool → List Term '[Bool, Bool] → Evidence (AppRequires "or_" BoolW '[Bool, Bool] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[Bool, Bool] ~ '[a], Bool ~ b, HasSpec a, HasSpec b) ⇒ BoolW "or_" '[a] b → TypeSpec a → Specification b Source # saturate ∷ BoolW "or_" '[Bool, Bool] Bool → List Term '[Bool, Bool] → [Pred] Source # | |
| (HasSpec a, HasSpec b) ⇒ Logic "prodFst_" BaseW '[Prod a b] a Source # | |
Defined in Constrained.TheKnot Methods info ∷ BaseW "prodFst_" '[Prod a b] a → String Source # propagate ∷ Context "prodFst_" BaseW '[Prod a b] a hole → Specification a → Specification hole Source # rewriteRules ∷ BaseW "prodFst_" '[Prod a b] a → List Term '[Prod a b] → Evidence (AppRequires "prodFst_" BaseW '[Prod a b] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[Prod a b] ~ '[a0], a ~ b0, HasSpec a0, HasSpec b0) ⇒ BaseW "prodFst_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ BaseW "prodFst_" '[Prod a b] Bool → List Term '[Prod a b] → [Pred] Source # | |
| (HasSpec a, HasSpec b) ⇒ Logic "prodSnd_" BaseW '[Prod a b] b Source # | |
Defined in Constrained.TheKnot Methods info ∷ BaseW "prodSnd_" '[Prod a b] b → String Source # propagate ∷ Context "prodSnd_" BaseW '[Prod a b] b hole → Specification b → Specification hole Source # rewriteRules ∷ BaseW "prodSnd_" '[Prod a b] b → List Term '[Prod a b] → Evidence (AppRequires "prodSnd_" BaseW '[Prod a b] b) → Maybe (Term b) Source # mapTypeSpec ∷ ('[Prod a b] ~ '[a0], b ~ b0, HasSpec a0, HasSpec b0) ⇒ BaseW "prodSnd_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ BaseW "prodSnd_" '[Prod a b] Bool → List Term '[Prod a b] → [Pred] Source # | |
| HasSpec a ⇒ Logic "rootLabel_" TreeW '[Tree a] a Source # | |
Defined in Constrained.Spec.Tree Methods info ∷ TreeW "rootLabel_" '[Tree a] a → String Source # propagate ∷ Context "rootLabel_" TreeW '[Tree a] a hole → Specification a → Specification hole Source # rewriteRules ∷ TreeW "rootLabel_" '[Tree a] a → List Term '[Tree a] → Evidence (AppRequires "rootLabel_" TreeW '[Tree a] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[Tree a] ~ '[a0], a ~ b, HasSpec a0, HasSpec b) ⇒ TreeW "rootLabel_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ TreeW "rootLabel_" '[Tree a] Bool → List Term '[Tree a] → [Pred] Source # | |
| (Sized t, HasSpec t) ⇒ Logic "sizeOf_" SizeW '[t] Integer Source # | |
Defined in Constrained.Spec.Size Methods info ∷ SizeW "sizeOf_" '[t] Integer → String Source # propagate ∷ Context "sizeOf_" SizeW '[t] Integer hole → Specification Integer → Specification hole Source # rewriteRules ∷ SizeW "sizeOf_" '[t] Integer → List Term '[t] → Evidence (AppRequires "sizeOf_" SizeW '[t] Integer) → Maybe (Term Integer) Source # mapTypeSpec ∷ ('[t] ~ '[a], Integer ~ b, HasSpec a, HasSpec b) ⇒ SizeW "sizeOf_" '[a] b → TypeSpec a → Specification b Source # saturate ∷ SizeW "sizeOf_" '[t] Bool → List Term '[t] → [Pred] Source # | |
| (HasSpec a, Ord a) ⇒ Logic "subset_" SetW '[Set a, Set a] Bool Source # | |
Defined in Constrained.Spec.Set Methods info ∷ SetW "subset_" '[Set a, Set a] Bool → String Source # propagate ∷ Context "subset_" SetW '[Set a, Set a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ SetW "subset_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → Evidence (AppRequires "subset_" SetW '[Set a, Set a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[Set a, Set a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ SetW "subset_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "subset_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → [Pred] Source # | |
| (GenericRequires a, simplerepA ~ SimpleRep a) ⇒ Logic "toGenericFn" BaseW '[a] simplerepA Source # | |
Defined in Constrained.Base Methods info ∷ BaseW "toGenericFn" '[a] simplerepA → String Source # propagate ∷ Context "toGenericFn" BaseW '[a] simplerepA hole → Specification simplerepA → Specification hole Source # rewriteRules ∷ BaseW "toGenericFn" '[a] simplerepA → List Term '[a] → Evidence (AppRequires "toGenericFn" BaseW '[a] simplerepA) → Maybe (Term simplerepA) Source # mapTypeSpec ∷ ('[a] ~ '[a0], simplerepA ~ b, HasSpec a0, HasSpec b) ⇒ BaseW "toGenericFn" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ BaseW "toGenericFn" '[a] Bool → List Term '[a] → [Pred] Source # | |
| (Sized [a], HasSpec a) ⇒ Logic "append_" ListW '[[a], [a]] [a] Source # | |
Defined in Constrained.Spec.ListFoldy Methods info ∷ ListW "append_" '[[a], [a]] [a] → String Source # propagate ∷ Context "append_" ListW '[[a], [a]] [a] hole → Specification [a] → Specification hole Source # rewriteRules ∷ ListW "append_" '[[a], [a]] [a] → List Term '[[a], [a]] → Evidence (AppRequires "append_" ListW '[[a], [a]] [a]) → Maybe (Term [a]) Source # mapTypeSpec ∷ ('[[a], [a]] ~ '[a0], [a] ~ b, HasSpec a0, HasSpec b) ⇒ ListW "append_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ ListW "append_" '[[a], [a]] Bool → List Term '[[a], [a]] → [Pred] Source # | |
| (HasSpec k, HasSpec v, Ord k, IsNormalType v, IsNormalType k) ⇒ Logic "dom_" MapW '[Map k v] (Set k) Source # | |
Defined in Constrained.Spec.Map Methods info ∷ MapW "dom_" '[Map k v] (Set k) → String Source # propagate ∷ Context "dom_" MapW '[Map k v] (Set k) hole → Specification (Set k) → Specification hole Source # rewriteRules ∷ MapW "dom_" '[Map k v] (Set k) → List Term '[Map k v] → Evidence (AppRequires "dom_" MapW '[Map k v] (Set k)) → Maybe (Term (Set k)) Source # mapTypeSpec ∷ ('[Map k v] ~ '[a], Set k ~ b, HasSpec a, HasSpec b) ⇒ MapW "dom_" '[a] b → TypeSpec a → Specification b Source # saturate ∷ MapW "dom_" '[Map k v] Bool → List Term '[Map k v] → [Pred] Source # | |
| (HasSpec a, Ord a) ⇒ Logic "fromList_" SetW '[[a]] (Set a) Source # | |
Defined in Constrained.Spec.Set Methods info ∷ SetW "fromList_" '[[a]] (Set a) → String Source # propagate ∷ Context "fromList_" SetW '[[a]] (Set a) hole → Specification (Set a) → Specification hole Source # rewriteRules ∷ SetW "fromList_" '[[a]] (Set a) → List Term '[[a]] → Evidence (AppRequires "fromList_" SetW '[[a]] (Set a)) → Maybe (Term (Set a)) Source # mapTypeSpec ∷ ('[[a]] ~ '[a0], Set a ~ b, HasSpec a0, HasSpec b) ⇒ SetW "fromList_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "fromList_" '[[a]] Bool → List Term '[[a]] → [Pred] Source # | |
| (HasSpec k, HasSpec v, IsNormalType v, IsNormalType k) ⇒ Logic "lookup_" MapW '[k, Map k v] (Maybe v) Source # | |
Defined in Constrained.Spec.Map Methods info ∷ MapW "lookup_" '[k, Map k v] (Maybe v) → String Source # propagate ∷ Context "lookup_" MapW '[k, Map k v] (Maybe v) hole → Specification (Maybe v) → Specification hole Source # rewriteRules ∷ MapW "lookup_" '[k, Map k v] (Maybe v) → List Term '[k, Map k v] → Evidence (AppRequires "lookup_" MapW '[k, Map k v] (Maybe v)) → Maybe (Term (Maybe v)) Source # mapTypeSpec ∷ ('[k, Map k v] ~ '[a], Maybe v ~ b, HasSpec a, HasSpec b) ⇒ MapW "lookup_" '[a] b → TypeSpec a → Specification b Source # saturate ∷ MapW "lookup_" '[k, Map k v] Bool → List Term '[k, Map k v] → [Pred] Source # | |
| (HasSpec k, HasSpec v, Ord k, IsNormalType v, IsNormalType k) ⇒ Logic "rng_" MapW '[Map k v] [v] Source # | |
Defined in Constrained.Spec.Map Methods info ∷ MapW "rng_" '[Map k v] [v] → String Source # propagate ∷ Context "rng_" MapW '[Map k v] [v] hole → Specification [v] → Specification hole Source # rewriteRules ∷ MapW "rng_" '[Map k v] [v] → List Term '[Map k v] → Evidence (AppRequires "rng_" MapW '[Map k v] [v]) → Maybe (Term [v]) Source # mapTypeSpec ∷ ('[Map k v] ~ '[a], [v] ~ b, HasSpec a, HasSpec b) ⇒ MapW "rng_" '[a] b → TypeSpec a → Specification b Source # saturate ∷ MapW "rng_" '[Map k v] Bool → List Term '[Map k v] → [Pred] Source # | |
| HasSpec a ⇒ Logic "singeltonList_" ListW '[a] [a] Source # | |
Defined in Constrained.Spec.ListFoldy Methods info ∷ ListW "singeltonList_" '[a] [a] → String Source # propagate ∷ Context "singeltonList_" ListW '[a] [a] hole → Specification [a] → Specification hole Source # rewriteRules ∷ ListW "singeltonList_" '[a] [a] → List Term '[a] → Evidence (AppRequires "singeltonList_" ListW '[a] [a]) → Maybe (Term [a]) Source # mapTypeSpec ∷ ('[a] ~ '[a0], [a] ~ b, HasSpec a0, HasSpec b) ⇒ ListW "singeltonList_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ ListW "singeltonList_" '[a] Bool → List Term '[a] → [Pred] Source # | |
| (HasSpec a, Ord a) ⇒ Logic "singleton_" SetW '[a] (Set a) Source # | |
Defined in Constrained.Spec.Set Methods info ∷ SetW "singleton_" '[a] (Set a) → String Source # propagate ∷ Context "singleton_" SetW '[a] (Set a) hole → Specification (Set a) → Specification hole Source # rewriteRules ∷ SetW "singleton_" '[a] (Set a) → List Term '[a] → Evidence (AppRequires "singleton_" SetW '[a] (Set a)) → Maybe (Term (Set a)) Source # mapTypeSpec ∷ ('[a] ~ '[a0], Set a ~ b, HasSpec a0, HasSpec b) ⇒ SetW "singleton_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "singleton_" '[a] Bool → List Term '[a] → [Pred] Source # | |
| (HasSpec a, Ord a) ⇒ Logic "union_" SetW '[Set a, Set a] (Set a) Source # | |
Defined in Constrained.Spec.Set Methods info ∷ SetW "union_" '[Set a, Set a] (Set a) → String Source # propagate ∷ Context "union_" SetW '[Set a, Set a] (Set a) hole → Specification (Set a) → Specification hole Source # rewriteRules ∷ SetW "union_" '[Set a, Set a] (Set a) → List Term '[Set a, Set a] → Evidence (AppRequires "union_" SetW '[Set a, Set a] (Set a)) → Maybe (Term (Set a)) Source # mapTypeSpec ∷ ('[Set a, Set a] ~ '[a0], Set a ~ b, HasSpec a0, HasSpec b) ⇒ SetW "union_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "union_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → [Pred] Source # | |
| (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Logic "leftFn" BaseW '[a] (Sum a b) Source # | |
Defined in Constrained.Spec.SumProd Methods info ∷ BaseW "leftFn" '[a] (Sum a b) → String Source # propagate ∷ Context "leftFn" BaseW '[a] (Sum a b) hole → Specification (Sum a b) → Specification hole Source # rewriteRules ∷ BaseW "leftFn" '[a] (Sum a b) → List Term '[a] → Evidence (AppRequires "leftFn" BaseW '[a] (Sum a b)) → Maybe (Term (Sum a b)) Source # mapTypeSpec ∷ ('[a] ~ '[a0], Sum a b ~ b0, HasSpec a0, HasSpec b0) ⇒ BaseW "leftFn" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ BaseW "leftFn" '[a] Bool → List Term '[a] → [Pred] Source # | |
| (HasSpec a, HasSpec b) ⇒ Logic "prod_" BaseW '[a, b] (Prod a b) Source # | |
Defined in Constrained.TheKnot Methods info ∷ BaseW "prod_" '[a, b] (Prod a b) → String Source # propagate ∷ Context "prod_" BaseW '[a, b] (Prod a b) hole → Specification (Prod a b) → Specification hole Source # rewriteRules ∷ BaseW "prod_" '[a, b] (Prod a b) → List Term '[a, b] → Evidence (AppRequires "prod_" BaseW '[a, b] (Prod a b)) → Maybe (Term (Prod a b)) Source # mapTypeSpec ∷ ('[a, b] ~ '[a0], Prod a b ~ b0, HasSpec a0, HasSpec b0) ⇒ BaseW "prod_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ BaseW "prod_" '[a, b] Bool → List Term '[a, b] → [Pred] Source # | |
| (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Logic "rightFn" BaseW '[b] (Sum a b) Source # | |
Defined in Constrained.Spec.SumProd Methods info ∷ BaseW "rightFn" '[b] (Sum a b) → String Source # propagate ∷ Context "rightFn" BaseW '[b] (Sum a b) hole → Specification (Sum a b) → Specification hole Source # rewriteRules ∷ BaseW "rightFn" '[b] (Sum a b) → List Term '[b] → Evidence (AppRequires "rightFn" BaseW '[b] (Sum a b)) → Maybe (Term (Sum a b)) Source # mapTypeSpec ∷ ('[b] ~ '[a0], Sum a b ~ b0, HasSpec a0, HasSpec b0) ⇒ BaseW "rightFn" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ BaseW "rightFn" '[b] Bool → List Term '[b] → [Pred] Source # | |
class Syntax t ⇒ Semantics (t ∷ Symbol → [Type] → Type → Type) where Source #
Semantic operations are ones that give the function symbol, meaning as a function. I.e. how to apply the function to a list of arguments and return a value.
class Syntax (t ∷ FSType) where Source #
Syntactic operations are ones that have to do with the structure and appearence of the type.
Minimal complete definition
Nothing
Methods
isInFix ∷ ∀ s dom rng. t s dom rng → Bool Source #
prettyWit ∷ ∀ s dom rng ann. (All HasSpec dom, HasSpec rng) ⇒ t s dom rng → List Term dom → Int → Maybe (Doc ann) Source #
class (HasSpec a, NumLike a, Logic "addFn" IntW '[a, a] a) ⇒ Foldy a where Source #
Minimal complete definition
Methods
genList ∷ MonadGenError m ⇒ Specification a → Specification a → GenT m [a] Source #
theAddFn ∷ IntW "addFn" '[a, a] a Source #
genSizedList ∷ MonadGenError m ⇒ Specification Integer → Specification a → Specification a → GenT m [a] Source #
noNegativeValues ∷ Bool Source #
Instances
data BaseW (sym ∷ Symbol) (dom ∷ [Type]) (rng ∷ Type) where Source #
Constructors
| InjLeftW ∷ ∀ a b. BaseW "leftFn" '[a] (Sum a b) | |
| InjRightW ∷ ∀ a b. BaseW "rightFn" '[b] (Sum a b) | |
| ProdW ∷ ∀ a b. BaseW "prod_" '[a, b] (Prod a b) | |
| ProdFstW ∷ ∀ a b. BaseW "prodFst_" '[Prod a b] a | |
| ProdSndW ∷ ∀ a b. BaseW "prodSnd_" '[Prod a b] b | |
| EqualW ∷ ∀ a. Eq a ⇒ BaseW "==." '[a, a] Bool | |
| ToGenericW ∷ GenericRequires a ⇒ BaseW "toGenericFn" '[a] (SimpleRep a) | |
| FromGenericW ∷ GenericRequires a ⇒ BaseW "fromGenericFn" '[SimpleRep a] a | |
| ElemW ∷ ∀ a. Eq a ⇒ BaseW "elem_" '[a, [a]] Bool |
Instances
| Semantics BaseW Source # | |
| Syntax BaseW Source # | |
| (HasSpec Bool, Eq a, Typeable a) ⇒ Logic "==." BaseW '[a, a] Bool Source # | |
Defined in Constrained.TheKnot Methods info ∷ BaseW "==." '[a, a] Bool → String Source # propagate ∷ Context "==." BaseW '[a, a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ BaseW "==." '[a, a] Bool → List Term '[a, a] → Evidence (AppRequires "==." BaseW '[a, a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ BaseW "==." '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ BaseW "==." '[a, a] Bool → List Term '[a, a] → [Pred] Source # | |
| HasSpec a ⇒ Logic "elem_" BaseW '[a, [a]] Bool Source # | |
Defined in Constrained.Spec.ListFoldy Methods info ∷ BaseW "elem_" '[a, [a]] Bool → String Source # propagate ∷ Context "elem_" BaseW '[a, [a]] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ BaseW "elem_" '[a, [a]] Bool → List Term '[a, [a]] → Evidence (AppRequires "elem_" BaseW '[a, [a]] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, [a]] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ BaseW "elem_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ BaseW "elem_" '[a, [a]] Bool → List Term '[a, [a]] → [Pred] Source # | |
| (GenericRequires a, dom ~ SimpleRep a) ⇒ Logic "fromGenericFn" BaseW '[dom] a Source # | |
Defined in Constrained.Base Methods info ∷ BaseW "fromGenericFn" '[dom] a → String Source # propagate ∷ Context "fromGenericFn" BaseW '[dom] a hole → Specification a → Specification hole Source # rewriteRules ∷ BaseW "fromGenericFn" '[dom] a → List Term '[dom] → Evidence (AppRequires "fromGenericFn" BaseW '[dom] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[dom] ~ '[a0], a ~ b, HasSpec a0, HasSpec b) ⇒ BaseW "fromGenericFn" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ BaseW "fromGenericFn" '[dom] Bool → List Term '[dom] → [Pred] Source # | |
| (HasSpec a, HasSpec b) ⇒ Logic "prodFst_" BaseW '[Prod a b] a Source # | |
Defined in Constrained.TheKnot Methods info ∷ BaseW "prodFst_" '[Prod a b] a → String Source # propagate ∷ Context "prodFst_" BaseW '[Prod a b] a hole → Specification a → Specification hole Source # rewriteRules ∷ BaseW "prodFst_" '[Prod a b] a → List Term '[Prod a b] → Evidence (AppRequires "prodFst_" BaseW '[Prod a b] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[Prod a b] ~ '[a0], a ~ b0, HasSpec a0, HasSpec b0) ⇒ BaseW "prodFst_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ BaseW "prodFst_" '[Prod a b] Bool → List Term '[Prod a b] → [Pred] Source # | |
| (HasSpec a, HasSpec b) ⇒ Logic "prodSnd_" BaseW '[Prod a b] b Source # | |
Defined in Constrained.TheKnot Methods info ∷ BaseW "prodSnd_" '[Prod a b] b → String Source # propagate ∷ Context "prodSnd_" BaseW '[Prod a b] b hole → Specification b → Specification hole Source # rewriteRules ∷ BaseW "prodSnd_" '[Prod a b] b → List Term '[Prod a b] → Evidence (AppRequires "prodSnd_" BaseW '[Prod a b] b) → Maybe (Term b) Source # mapTypeSpec ∷ ('[Prod a b] ~ '[a0], b ~ b0, HasSpec a0, HasSpec b0) ⇒ BaseW "prodSnd_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ BaseW "prodSnd_" '[Prod a b] Bool → List Term '[Prod a b] → [Pred] Source # | |
| (GenericRequires a, simplerepA ~ SimpleRep a) ⇒ Logic "toGenericFn" BaseW '[a] simplerepA Source # | |
Defined in Constrained.Base Methods info ∷ BaseW "toGenericFn" '[a] simplerepA → String Source # propagate ∷ Context "toGenericFn" BaseW '[a] simplerepA hole → Specification simplerepA → Specification hole Source # rewriteRules ∷ BaseW "toGenericFn" '[a] simplerepA → List Term '[a] → Evidence (AppRequires "toGenericFn" BaseW '[a] simplerepA) → Maybe (Term simplerepA) Source # mapTypeSpec ∷ ('[a] ~ '[a0], simplerepA ~ b, HasSpec a0, HasSpec b) ⇒ BaseW "toGenericFn" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ BaseW "toGenericFn" '[a] Bool → List Term '[a] → [Pred] Source # | |
| (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Logic "leftFn" BaseW '[a] (Sum a b) Source # | |
Defined in Constrained.Spec.SumProd Methods info ∷ BaseW "leftFn" '[a] (Sum a b) → String Source # propagate ∷ Context "leftFn" BaseW '[a] (Sum a b) hole → Specification (Sum a b) → Specification hole Source # rewriteRules ∷ BaseW "leftFn" '[a] (Sum a b) → List Term '[a] → Evidence (AppRequires "leftFn" BaseW '[a] (Sum a b)) → Maybe (Term (Sum a b)) Source # mapTypeSpec ∷ ('[a] ~ '[a0], Sum a b ~ b0, HasSpec a0, HasSpec b0) ⇒ BaseW "leftFn" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ BaseW "leftFn" '[a] Bool → List Term '[a] → [Pred] Source # | |
| (HasSpec a, HasSpec b) ⇒ Logic "prod_" BaseW '[a, b] (Prod a b) Source # | |
Defined in Constrained.TheKnot Methods info ∷ BaseW "prod_" '[a, b] (Prod a b) → String Source # propagate ∷ Context "prod_" BaseW '[a, b] (Prod a b) hole → Specification (Prod a b) → Specification hole Source # rewriteRules ∷ BaseW "prod_" '[a, b] (Prod a b) → List Term '[a, b] → Evidence (AppRequires "prod_" BaseW '[a, b] (Prod a b)) → Maybe (Term (Prod a b)) Source # mapTypeSpec ∷ ('[a, b] ~ '[a0], Prod a b ~ b0, HasSpec a0, HasSpec b0) ⇒ BaseW "prod_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ BaseW "prod_" '[a, b] Bool → List Term '[a, b] → [Pred] Source # | |
| (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Logic "rightFn" BaseW '[b] (Sum a b) Source # | |
Defined in Constrained.Spec.SumProd Methods info ∷ BaseW "rightFn" '[b] (Sum a b) → String Source # propagate ∷ Context "rightFn" BaseW '[b] (Sum a b) hole → Specification (Sum a b) → Specification hole Source # rewriteRules ∷ BaseW "rightFn" '[b] (Sum a b) → List Term '[b] → Evidence (AppRequires "rightFn" BaseW '[b] (Sum a b)) → Maybe (Term (Sum a b)) Source # mapTypeSpec ∷ ('[b] ~ '[a0], Sum a b ~ b0, HasSpec a0, HasSpec b0) ⇒ BaseW "rightFn" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ BaseW "rightFn" '[b] Bool → List Term '[b] → [Pred] Source # | |
| Show (BaseW s d r) Source # | |
| Eq (BaseW s dom rng) Source # | |
data BoolW (sym ∷ Symbol) (dom ∷ [Type]) (rng ∷ Type) where Source #
Operations on Bool
Instances
| Semantics BoolW Source # | |
| Syntax BoolW Source # | |
| (HasSpec Bool, TypeSpec Bool ~ SumSpec () ()) ⇒ Logic "not_" BoolW '[Bool] Bool Source # | |
Defined in Constrained.TheKnot Methods info ∷ BoolW "not_" '[Bool] Bool → String Source # propagate ∷ Context "not_" BoolW '[Bool] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ BoolW "not_" '[Bool] Bool → List Term '[Bool] → Evidence (AppRequires "not_" BoolW '[Bool] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[Bool] ~ '[a], Bool ~ b, HasSpec a, HasSpec b) ⇒ BoolW "not_" '[a] b → TypeSpec a → Specification b Source # saturate ∷ BoolW "not_" '[Bool] Bool → List Term '[Bool] → [Pred] Source # | |
| HasSpec Bool ⇒ Logic "or_" BoolW '[Bool, Bool] Bool Source # | |
Defined in Constrained.TheKnot Methods info ∷ BoolW "or_" '[Bool, Bool] Bool → String Source # propagate ∷ Context "or_" BoolW '[Bool, Bool] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ BoolW "or_" '[Bool, Bool] Bool → List Term '[Bool, Bool] → Evidence (AppRequires "or_" BoolW '[Bool, Bool] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[Bool, Bool] ~ '[a], Bool ~ b, HasSpec a, HasSpec b) ⇒ BoolW "or_" '[a] b → TypeSpec a → Specification b Source # saturate ∷ BoolW "or_" '[Bool, Bool] Bool → List Term '[Bool, Bool] → [Pred] Source # | |
| Show (BoolW s dom rng) Source # | |
| Eq (BoolW s dom rng) Source # | |
data NumOrdW (sym ∷ Symbol) (dom ∷ [Type]) (rng ∷ Type) where Source #
Constructors
| LessOrEqualW ∷ OrdLike a ⇒ NumOrdW "<=." '[a, a] Bool | |
| LessW ∷ OrdLike a ⇒ NumOrdW "<." '[a, a] Bool | |
| GreaterOrEqualW ∷ OrdLike a ⇒ NumOrdW ">=." '[a, a] Bool | |
| GreaterW ∷ OrdLike a ⇒ NumOrdW ">." '[a, a] Bool |
Instances
| Semantics NumOrdW Source # | |
| Syntax NumOrdW Source # | |
| OrdLike a ⇒ Logic "<." NumOrdW '[a, a] Bool Source # | |
Defined in Constrained.TheKnot Methods info ∷ NumOrdW "<." '[a, a] Bool → String Source # propagate ∷ Context "<." NumOrdW '[a, a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ NumOrdW "<." '[a, a] Bool → List Term '[a, a] → Evidence (AppRequires "<." NumOrdW '[a, a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ NumOrdW "<." '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ NumOrdW "<." '[a, a] Bool → List Term '[a, a] → [Pred] Source # | |
| OrdLike a ⇒ Logic "<=." NumOrdW '[a, a] Bool Source # | |
Defined in Constrained.TheKnot Methods info ∷ NumOrdW "<=." '[a, a] Bool → String Source # propagate ∷ Context "<=." NumOrdW '[a, a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ NumOrdW "<=." '[a, a] Bool → List Term '[a, a] → Evidence (AppRequires "<=." NumOrdW '[a, a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ NumOrdW "<=." '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ NumOrdW "<=." '[a, a] Bool → List Term '[a, a] → [Pred] Source # | |
| OrdLike a ⇒ Logic ">." NumOrdW '[a, a] Bool Source # | |
Defined in Constrained.TheKnot Methods info ∷ NumOrdW ">." '[a, a] Bool → String Source # propagate ∷ Context ">." NumOrdW '[a, a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ NumOrdW ">." '[a, a] Bool → List Term '[a, a] → Evidence (AppRequires ">." NumOrdW '[a, a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ NumOrdW ">." '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ NumOrdW ">." '[a, a] Bool → List Term '[a, a] → [Pred] Source # | |
| OrdLike a ⇒ Logic ">=." NumOrdW '[a, a] Bool Source # | |
Defined in Constrained.TheKnot Methods info ∷ NumOrdW ">=." '[a, a] Bool → String Source # propagate ∷ Context ">=." NumOrdW '[a, a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ NumOrdW ">=." '[a, a] Bool → List Term '[a, a] → Evidence (AppRequires ">=." NumOrdW '[a, a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ NumOrdW ">=." '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ NumOrdW ">=." '[a, a] Bool → List Term '[a, a] → [Pred] Source # | |
| Show (NumOrdW s ds r) Source # | |
| Eq (NumOrdW s ds r) Source # | |
data IntW (s ∷ Symbol) (as ∷ [Type]) b where Source #
Instances
| Semantics IntW Source # | |
| Syntax IntW Source # | |
| NumLike a ⇒ Logic "addFn" IntW '[a, a] a Source # | Just a note that these instances won't work until we are in a context where
there is a HasSpec instance of |
Defined in Constrained.NumSpec Methods info ∷ IntW "addFn" '[a, a] a → String Source # propagate ∷ Context "addFn" IntW '[a, a] a hole → Specification a → Specification hole Source # rewriteRules ∷ IntW "addFn" '[a, a] a → List Term '[a, a] → Evidence (AppRequires "addFn" IntW '[a, a] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], a ~ b, HasSpec a0, HasSpec b) ⇒ IntW "addFn" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ IntW "addFn" '[a, a] Bool → List Term '[a, a] → [Pred] Source # | |
| NumLike a ⇒ Logic "negateFn" IntW '[a] a Source # | |
Defined in Constrained.NumSpec Methods info ∷ IntW "negateFn" '[a] a → String Source # propagate ∷ Context "negateFn" IntW '[a] a hole → Specification a → Specification hole Source # rewriteRules ∷ IntW "negateFn" '[a] a → List Term '[a] → Evidence (AppRequires "negateFn" IntW '[a] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[a] ~ '[a0], a ~ b, HasSpec a0, HasSpec b) ⇒ IntW "negateFn" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ IntW "negateFn" '[a] Bool → List Term '[a] → [Pred] Source # | |
| Show (IntW s d r) Source # | |
| Eq (IntW s dom rng) Source # | |
data SizeW (s ∷ Symbol) (dom ∷ [Type]) rng ∷ Type where Source #
Instances
| Semantics SizeW Source # | |
| Syntax SizeW Source # | |
| (Sized t, HasSpec t) ⇒ Logic "sizeOf_" SizeW '[t] Integer Source # | |
Defined in Constrained.Spec.Size Methods info ∷ SizeW "sizeOf_" '[t] Integer → String Source # propagate ∷ Context "sizeOf_" SizeW '[t] Integer hole → Specification Integer → Specification hole Source # rewriteRules ∷ SizeW "sizeOf_" '[t] Integer → List Term '[t] → Evidence (AppRequires "sizeOf_" SizeW '[t] Integer) → Maybe (Term Integer) Source # mapTypeSpec ∷ ('[t] ~ '[a], Integer ~ b, HasSpec a, HasSpec b) ⇒ SizeW "sizeOf_" '[a] b → TypeSpec a → Specification b Source # saturate ∷ SizeW "sizeOf_" '[t] Bool → List Term '[t] → [Pred] Source # | |
| Show (SizeW s d r) Source # | |
| Eq (SizeW s ds r) Source # | |
data FunW (sym ∷ Symbol) (dom ∷ [Type]) (rng ∷ Type) where Source #
Constructors
| IdW ∷ ∀ a. FunW "id_" '[a] a | |
| ComposeW ∷ ∀ b s1 s2 t1 t2 a r. (Logic s1 t1 '[b] r, Logic s2 t2 '[a] b, HasSpec b) ⇒ t1 s1 '[b] r → t2 s2 '[a] b → FunW "composeFn" '[a] r | |
| FlipW ∷ ∀ sym t a b r. Logic sym t '[a, b] r ⇒ t sym '[a, b] r → FunW "flip_" '[b, a] r |
Instances
| Semantics FunW Source # | |
| Syntax FunW Source # | |
| (All (Typeable ∷ Type → Constraint) '[a, r], HasSpec r) ⇒ Logic "composeFn" FunW '[a] r Source # | |
Defined in Constrained.Spec.ListFoldy Methods info ∷ FunW "composeFn" '[a] r → String Source # propagate ∷ Context "composeFn" FunW '[a] r hole → Specification r → Specification hole Source # rewriteRules ∷ FunW "composeFn" '[a] r → List Term '[a] → Evidence (AppRequires "composeFn" FunW '[a] r) → Maybe (Term r) Source # mapTypeSpec ∷ ('[a] ~ '[a0], r ~ b, HasSpec a0, HasSpec b) ⇒ FunW "composeFn" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ FunW "composeFn" '[a] Bool → List Term '[a] → [Pred] Source # | |
| (∀ (sym ∷ Symbol) (t ∷ Symbol → [Type] → Type → Type). Logic sym t '[a, b] r, All (Typeable ∷ Type → Constraint) '[a, b, r]) ⇒ Logic "flip_" FunW '[b, a] r Source # | |
Defined in Constrained.Spec.ListFoldy Methods info ∷ FunW "flip_" '[b, a] r → String Source # propagate ∷ Context "flip_" FunW '[b, a] r hole → Specification r → Specification hole Source # rewriteRules ∷ FunW "flip_" '[b, a] r → List Term '[b, a] → Evidence (AppRequires "flip_" FunW '[b, a] r) → Maybe (Term r) Source # mapTypeSpec ∷ ('[b, a] ~ '[a0], r ~ b0, HasSpec a0, HasSpec b0) ⇒ FunW "flip_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ FunW "flip_" '[b, a] Bool → List Term '[b, a] → [Pred] Source # | |
| HasSpec a ⇒ Logic "id_" FunW '[a] a Source # | |
Defined in Constrained.Spec.ListFoldy Methods info ∷ FunW "id_" '[a] a → String Source # propagate ∷ Context "id_" FunW '[a] a hole → Specification a → Specification hole Source # rewriteRules ∷ FunW "id_" '[a] a → List Term '[a] → Evidence (AppRequires "id_" FunW '[a] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[a] ~ '[a0], a ~ b, HasSpec a0, HasSpec b) ⇒ FunW "id_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ FunW "id_" '[a] Bool → List Term '[a] → [Pred] Source # | |
| KnownSymbol s ⇒ Show (FunW s dom rng) Source # | |
| Eq (FunW s dom rng) Source # | |
data ListW (s ∷ Symbol) (args ∷ [Type]) (res ∷ Type) where Source #
Constructors
| FoldMapW ∷ ∀ a b. (Foldy b, HasSpec a) ⇒ Fun '[a] b → ListW "foldMap_" '[[a]] b | |
| SingletonListW ∷ ListW "singeltonList_" '[a] [a] | |
| AppendW ∷ (Typeable a, Show a) ⇒ ListW "append_" '[[a], [a]] [a] |
Instances
| Semantics ListW Source # | |
| Syntax ListW Source # | |
| (Typeable a, Foldy b) ⇒ Logic "foldMap_" ListW '[[a]] b Source # | |
Defined in Constrained.Spec.ListFoldy Methods info ∷ ListW "foldMap_" '[[a]] b → String Source # propagate ∷ Context "foldMap_" ListW '[[a]] b hole → Specification b → Specification hole Source # rewriteRules ∷ ListW "foldMap_" '[[a]] b → List Term '[[a]] → Evidence (AppRequires "foldMap_" ListW '[[a]] b) → Maybe (Term b) Source # mapTypeSpec ∷ ('[[a]] ~ '[a0], b ~ b0, HasSpec a0, HasSpec b0) ⇒ ListW "foldMap_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ ListW "foldMap_" '[[a]] Bool → List Term '[[a]] → [Pred] Source # | |
| (Sized [a], HasSpec a) ⇒ Logic "append_" ListW '[[a], [a]] [a] Source # | |
Defined in Constrained.Spec.ListFoldy Methods info ∷ ListW "append_" '[[a], [a]] [a] → String Source # propagate ∷ Context "append_" ListW '[[a], [a]] [a] hole → Specification [a] → Specification hole Source # rewriteRules ∷ ListW "append_" '[[a], [a]] [a] → List Term '[[a], [a]] → Evidence (AppRequires "append_" ListW '[[a], [a]] [a]) → Maybe (Term [a]) Source # mapTypeSpec ∷ ('[[a], [a]] ~ '[a0], [a] ~ b, HasSpec a0, HasSpec b) ⇒ ListW "append_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ ListW "append_" '[[a], [a]] Bool → List Term '[[a], [a]] → [Pred] Source # | |
| HasSpec a ⇒ Logic "singeltonList_" ListW '[a] [a] Source # | |
Defined in Constrained.Spec.ListFoldy Methods info ∷ ListW "singeltonList_" '[a] [a] → String Source # propagate ∷ Context "singeltonList_" ListW '[a] [a] hole → Specification [a] → Specification hole Source # rewriteRules ∷ ListW "singeltonList_" '[a] [a] → List Term '[a] → Evidence (AppRequires "singeltonList_" ListW '[a] [a]) → Maybe (Term [a]) Source # mapTypeSpec ∷ ('[a] ~ '[a0], [a] ~ b, HasSpec a0, HasSpec b) ⇒ ListW "singeltonList_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ ListW "singeltonList_" '[a] Bool → List Term '[a] → [Pred] Source # | |
| Show (ListW s d r) Source # | |
| Eq (ListW s d r) Source # | |
data MapW (sym ∷ Symbol) (dom ∷ [Type]) (rng ∷ Type) where Source #
Constructors
| DomW ∷ ∀ k v. Ord k ⇒ MapW "dom_" '[Map k v] (Set k) | |
| RngW ∷ ∀ k v. Ord k ⇒ MapW "rng_" '[Map k v] [v] | |
| LookupW ∷ ∀ k v. Ord k ⇒ MapW "lookup_" '[k, Map k v] (Maybe v) |
Instances
| Semantics MapW Source # | |
| Syntax MapW Source # | |
| (HasSpec k, HasSpec v, Ord k, IsNormalType v, IsNormalType k) ⇒ Logic "dom_" MapW '[Map k v] (Set k) Source # | |
Defined in Constrained.Spec.Map Methods info ∷ MapW "dom_" '[Map k v] (Set k) → String Source # propagate ∷ Context "dom_" MapW '[Map k v] (Set k) hole → Specification (Set k) → Specification hole Source # rewriteRules ∷ MapW "dom_" '[Map k v] (Set k) → List Term '[Map k v] → Evidence (AppRequires "dom_" MapW '[Map k v] (Set k)) → Maybe (Term (Set k)) Source # mapTypeSpec ∷ ('[Map k v] ~ '[a], Set k ~ b, HasSpec a, HasSpec b) ⇒ MapW "dom_" '[a] b → TypeSpec a → Specification b Source # saturate ∷ MapW "dom_" '[Map k v] Bool → List Term '[Map k v] → [Pred] Source # | |
| (HasSpec k, HasSpec v, IsNormalType v, IsNormalType k) ⇒ Logic "lookup_" MapW '[k, Map k v] (Maybe v) Source # | |
Defined in Constrained.Spec.Map Methods info ∷ MapW "lookup_" '[k, Map k v] (Maybe v) → String Source # propagate ∷ Context "lookup_" MapW '[k, Map k v] (Maybe v) hole → Specification (Maybe v) → Specification hole Source # rewriteRules ∷ MapW "lookup_" '[k, Map k v] (Maybe v) → List Term '[k, Map k v] → Evidence (AppRequires "lookup_" MapW '[k, Map k v] (Maybe v)) → Maybe (Term (Maybe v)) Source # mapTypeSpec ∷ ('[k, Map k v] ~ '[a], Maybe v ~ b, HasSpec a, HasSpec b) ⇒ MapW "lookup_" '[a] b → TypeSpec a → Specification b Source # saturate ∷ MapW "lookup_" '[k, Map k v] Bool → List Term '[k, Map k v] → [Pred] Source # | |
| (HasSpec k, HasSpec v, Ord k, IsNormalType v, IsNormalType k) ⇒ Logic "rng_" MapW '[Map k v] [v] Source # | |
Defined in Constrained.Spec.Map Methods info ∷ MapW "rng_" '[Map k v] [v] → String Source # propagate ∷ Context "rng_" MapW '[Map k v] [v] hole → Specification [v] → Specification hole Source # rewriteRules ∷ MapW "rng_" '[Map k v] [v] → List Term '[Map k v] → Evidence (AppRequires "rng_" MapW '[Map k v] [v]) → Maybe (Term [v]) Source # mapTypeSpec ∷ ('[Map k v] ~ '[a], [v] ~ b, HasSpec a, HasSpec b) ⇒ MapW "rng_" '[a] b → TypeSpec a → Specification b Source # saturate ∷ MapW "rng_" '[Map k v] Bool → List Term '[Map k v] → [Pred] Source # | |
| Show (MapW s d r) Source # | |
| Eq (MapW s dom rng) Source # | |
Constructors
| NumSpecInterval (Maybe n) (Maybe n) |
Instances
| (Arbitrary a, Ord a) ⇒ Arbitrary (NumSpec a) Source # | |
| Ord n ⇒ Monoid (NumSpec n) Source # | |
| Ord n ⇒ Semigroup (NumSpec n) Source # | |
| Num (NumSpec Integer) Source # | |
Defined in Constrained.NumSpec Methods (+) ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer (-) ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer (*) ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer negate ∷ NumSpec Integer → NumSpec Integer abs ∷ NumSpec Integer → NumSpec Integer signum ∷ NumSpec Integer → NumSpec Integer fromInteger ∷ Integer → NumSpec Integer | |
| Show n ⇒ Show (NumSpec n) Source # | |
| Ord n ⇒ Eq (NumSpec n) Source # | |
class MaybeBounded a where Source #
Minimal complete definition
Nothing
Methods
lowerBound ∷ Maybe a Source #
default lowerBound ∷ Bounded a ⇒ Maybe a Source #
upperBound ∷ Maybe a Source #
default upperBound ∷ Bounded a ⇒ Maybe a Source #
Instances
| MaybeBounded Int16 Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Int32 Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Int64 Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Int8 Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Word16 Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Word32 Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Word64 Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Word8 Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Integer Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Natural Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Float Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Int Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded (Ratio Integer) Source # | |
Defined in Constrained.NumSpec | |
Constructors
| a :| [a] |
Instances
| MonadFix NonEmpty | |
Defined in Control.Monad.Fix | |
| Foldable NonEmpty | |
Defined in Data.Foldable Methods fold ∷ Monoid m ⇒ NonEmpty m → m foldMap ∷ Monoid m ⇒ (a → m) → NonEmpty a → m foldMap' ∷ Monoid m ⇒ (a → m) → NonEmpty a → m foldr ∷ (a → b → b) → b → NonEmpty a → b foldr' ∷ (a → b → b) → b → NonEmpty a → b foldl ∷ (b → a → b) → b → NonEmpty a → b foldl' ∷ (b → a → b) → b → NonEmpty a → b foldr1 ∷ (a → a → a) → NonEmpty a → a foldl1 ∷ (a → a → a) → NonEmpty a → a elem ∷ Eq a ⇒ a → NonEmpty a → Bool maximum ∷ Ord a ⇒ NonEmpty a → a | |
| Eq1 NonEmpty | |
Defined in Data.Functor.Classes | |
| Ord1 NonEmpty | |
Defined in Data.Functor.Classes Methods liftCompare ∷ (a → b → Ordering) → NonEmpty a → NonEmpty b → Ordering | |
| Read1 NonEmpty | |
Defined in Data.Functor.Classes Methods liftReadsPrec ∷ (Int → ReadS a) → ReadS [a] → Int → ReadS (NonEmpty a) liftReadList ∷ (Int → ReadS a) → ReadS [a] → ReadS [NonEmpty a] liftReadPrec ∷ ReadPrec a → ReadPrec [a] → ReadPrec (NonEmpty a) liftReadListPrec ∷ ReadPrec a → ReadPrec [a] → ReadPrec [NonEmpty a] | |
| Show1 NonEmpty | |
Defined in Data.Functor.Classes Methods liftShowsPrec ∷ (Int → a → ShowS) → ([a] → ShowS) → Int → NonEmpty a → ShowS liftShowList ∷ (Int → a → ShowS) → ([a] → ShowS) → [NonEmpty a] → ShowS | |
| Traversable NonEmpty | |
| Applicative NonEmpty | |
| Functor NonEmpty | |
| Monad NonEmpty | |
| Generic1 NonEmpty | |
| Lift a ⇒ Lift (NonEmpty a ∷ Type) | |
| Arbitrary a ⇒ Arbitrary (NonEmpty a) Source # | |
| Semigroup (NonEmpty a) | |
| IsList (NonEmpty a) | |
| Generic (NonEmpty a) | |
| Read a ⇒ Read (NonEmpty a) | |
| Show a ⇒ Show (NonEmpty a) | |
| Eq a ⇒ Eq (NonEmpty a) | |
| Ord a ⇒ Ord (NonEmpty a) | |
Defined in GHC.Base | |
| Pretty a ⇒ Pretty (NonEmpty a) | |
| type Rep1 NonEmpty | |
Defined in GHC.Generics type Rep1 NonEmpty = D1 ('MetaData "NonEmpty" "GHC.Base" "base" 'False) (C1 ('MetaCons ":|" ('InfixI 'LeftAssociative 9) 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1 :*: S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec1 []))) | |
| type Item (NonEmpty a) | |
| type Rep (NonEmpty a) | |
Defined in GHC.Generics type Rep (NonEmpty a) = D1 ('MetaData "NonEmpty" "GHC.Base" "base" 'False) (C1 ('MetaCons ":|" ('InfixI 'LeftAssociative 9) 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [a]))) | |
data Specification a where Source #
A `Specification a` denotes a set of as
Constructors
| ExplainSpec ∷ [String] → Specification a → Specification a | Explain a Specification |
| MemberSpec | Elements of a known set |
Fields
| |
| ErrorSpec ∷ NonEmpty String → Specification a | The empty set |
| SuspendedSpec | The set described by some predicates over the bound variable. |
Fields
| |
| TypeSpec | A type-specific spec |
Fields
| |
| TrueSpec ∷ Specification a | Anything |
Instances
| (HasSpec a, Arbitrary (TypeSpec a)) ⇒ Arbitrary (Specification a) Source # | |
Defined in Constrained.TheKnot Methods arbitrary ∷ Gen (Specification a) Source # shrink ∷ Specification a → [Specification a] Source # | |
| HasSpec a ⇒ Monoid (Specification a) | |
Defined in Constrained.Conformance Methods mempty ∷ Specification a mappend ∷ Specification a → Specification a → Specification a mconcat ∷ [Specification a] → Specification a | |
| HasSpec a ⇒ Semigroup (Specification a) | |
Defined in Constrained.Conformance Methods (<>) ∷ Specification a → Specification a → Specification a # sconcat ∷ NonEmpty (Specification a) → Specification a stimes ∷ Integral b ⇒ b → Specification a → Specification a | |
| Number Integer ⇒ Num (Specification Integer) | This is very liberal, since in lots of cases it returns TrueSpec.
for example all operations on SuspendedSpec, and certain
operations between TypeSpec and MemberSpec. Perhaps we should
remove it. Only the addSpec (+) and multSpec (*) methods are used.
But, it is kind of cool ...
In Fact we can use this to make Num(Specification n) instance for any |
Defined in Constrained.NumSpec Methods (+) ∷ Specification Integer → Specification Integer → Specification Integer (-) ∷ Specification Integer → Specification Integer → Specification Integer (*) ∷ Specification Integer → Specification Integer → Specification Integer negate ∷ Specification Integer → Specification Integer abs ∷ Specification Integer → Specification Integer signum ∷ Specification Integer → Specification Integer fromInteger ∷ Integer → Specification Integer | |
| HasSpec a ⇒ Show (Specification a) Source # | |
Defined in Constrained.Base Methods showsPrec ∷ Int → Specification a → ShowS show ∷ Specification a → String showList ∷ [Specification a] → ShowS | |
| HasSpec a ⇒ Pretty (Specification a) Source # | |
Defined in Constrained.Base | |
| HasSpec a ⇒ Pretty (WithPrec (Specification a)) Source # | |
Defined in Constrained.Base Methods pretty ∷ WithPrec (Specification a) → Doc ann Source # prettyList ∷ [WithPrec (Specification a)] → Doc ann Source # | |
Constructors
| App ∷ ∀ sym t dom rng. AppRequires sym t dom rng ⇒ t sym dom rng → List Term dom → Term rng | |
| Lit ∷ Literal a ⇒ a → Term a | |
| V ∷ HasSpec a ⇒ Var a → Term a |
Instances
| (Ord a, HasSpec a, HasSpec (Set a)) ⇒ Monoid (Term (Set a)) | |
| (Ord a, HasSpec a, HasSpec (Set a)) ⇒ Semigroup (Term (Set a)) | |
| NumLike a ⇒ Num (Term a) | |
| Show a ⇒ Show (Term a) Source # | |
| IsPred (Term Bool) Source # | |
| Rename (Term a) Source # | |
| HasVariables (Term a) Source # | |
| Eq (Term a) Source # | |
| Show a ⇒ Pretty (Term a) Source # | |
| Show a ⇒ Pretty (WithPrec (Term a)) Source # | |
| HasVariables (List Term as) Source # | |
named ∷ String → Term a → Term a Source #
Give a Term a nameHint, if its a Var, and doesn't already have one, otherwise return the Term unchanged.
Constructors
| ElemPred ∷ ∀ a. HasSpec a ⇒ Bool → Term a → NonEmpty a → Pred | |
| Monitor ∷ ((∀ a. Term a → a) → Property → Property) → Pred | |
| And ∷ [Pred] → Pred | |
| Exists | |
| Subst ∷ HasSpec a ⇒ Var a → Term a → Pred → Pred | |
| Let ∷ Term a → Binder a → Pred | |
| Assert ∷ Term Bool → Pred | |
| Reifies | |
| DependsOn ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Pred | |
| ForAll ∷ (Forallable t a, HasSpec t, HasSpec a) ⇒ Term t → Binder a → Pred | |
| Case | |
| When ∷ HasSpec Bool ⇒ Term Bool → Pred → Pred | |
| GenHint ∷ HasGenHint a ⇒ Hint a → Term a → Pred | |
| TruePred ∷ Pred | |
| FalsePred ∷ NonEmpty String → Pred | |
| Explain ∷ NonEmpty String → Pred → Pred | |
type Literal a = (Typeable a, Eq a, Show a) Source #
Properties needed by objects to appear in the system, if they have no semantic or logical requirements. Mostly used for Lit terms, which are self evaluating But such things also occurr in Contexts.
class (Typeable a, Eq a, Show a, Show (TypeSpec a), Typeable (TypeSpec a)) ⇒ HasSpec a where Source #
Minimal complete definition
Nothing
Associated Types
The `TypeSpec a` is the type-specific `Specification a`.
type Prerequisites a ∷ Constraint Source #
Prerequisites for the instance that are sometimes necessary
when working with e.g. Specifications or functions in the universe.
type Prerequisites a = ()
Methods
emptySpec ∷ TypeSpec a Source #
default emptySpec ∷ (HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) ⇒ TypeSpec a Source #
combineSpec ∷ TypeSpec a → TypeSpec a → Specification a Source #
default combineSpec ∷ (HasSimpleRep a, HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) ⇒ TypeSpec a → TypeSpec a → Specification a Source #
genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a Source #
Generate a value that satisfies the Specification.
The key property for this generator is soundness:
∀ a ∈ genFromTypeSpec spec. a conformsTo spec
default genFromTypeSpec ∷ (HasSimpleRep a, HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) ⇒ (HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a Source #
conformsTo ∷ HasCallStack ⇒ a → TypeSpec a → Bool Source #
Check conformance to the spec.
default conformsTo ∷ (HasSimpleRep a, HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) ⇒ HasCallStack ⇒ a → TypeSpec a → Bool Source #
shrinkWithTypeSpec ∷ TypeSpec a → a → [a] Source #
Shrink an a with the aide of a Specification
default shrinkWithTypeSpec ∷ (HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a) ⇒ TypeSpec a → a → [a] Source #
toPreds ∷ Term a → TypeSpec a → Pred Source #
Convert a spec to predicates:
The key property here is:
∀ a. a conformsTo spec == a conformsTo constrained (t -> toPreds t spec)
default toPreds ∷ (HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a) ⇒ Term a → TypeSpec a → Pred Source #
cardinalTypeSpec ∷ TypeSpec a → Specification Integer Source #
Compute an upper and lower bound on the number of solutions genFromTypeSpec might return
default cardinalTypeSpec ∷ (HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) ⇒ TypeSpec a → Specification Integer Source #
cardinalTrueSpec ∷ Specification Integer Source #
A bound on the number of solutions `genFromTypeSpec TrueSpec` can produce. For a type with finite elements, we can get a much more accurate answer than TrueSpec
typeSpecHasError ∷ TypeSpec a → Maybe (NonEmpty String) Source #
alternateShow ∷ TypeSpec a → BinaryShow Source #
monadConformsTo ∷ a → TypeSpec a → Writer [String] Bool Source #
typeSpecOpt ∷ TypeSpec a → [a] → Specification a Source #
For some types (especially finite ones) there may be much better ways to construct
a Specification than the default method of just adding a large bad list to TypSpec. This
function allows each HasSpec instance to decide.
guardTypeSpec ∷ [String] → TypeSpec a → Specification a Source #
This can be used to detect self inconsistencies in a (TypeSpec t)
Note this is similar to typeSpecHasError, and the default
value for typeSpecHasError is written in terms of guardTypeSpec
Both typeSpecHasError and guardTypeSpec can be set individually.
prerequisites ∷ Evidence (Prerequisites a) Source #
Materialize the Prerequisites dictionary. It should not be necessary to
implement this function manually.
default prerequisites ∷ Prerequisites a ⇒ Evidence (Prerequisites a) Source #
Instances
class Typeable (SimpleRep a) ⇒ HasSimpleRep a where Source #
Minimal complete definition
Nothing
Associated Types
Methods
toSimpleRep ∷ a → SimpleRep a Source #
default toSimpleRep ∷ (Generic a, SimpleGeneric (Rep a), SimpleRep a ~ SimplifyRep (Rep a)) ⇒ a → SimpleRep a Source #
fromSimpleRep ∷ SimpleRep a → a Source #
default fromSimpleRep ∷ (Generic a, SimpleGeneric (Rep a), SimpleRep a ~ SimplifyRep (Rep a)) ⇒ SimpleRep a → a Source #
Instances
| HasSimpleRep Foo Source # | |
| HasSimpleRep Three Source # | |
| HasSimpleRep FooBarBaz Source # | |
| HasSimpleRep () Source # | |
Defined in Constrained.Base | |
| HasSimpleRep Bool Source # | |
Defined in Constrained.TheKnot | |
| (Typeable a, Ord a) ⇒ HasSimpleRep (NotASet a) Source # | |
| Typeable a ⇒ HasSimpleRep (Maybe a) Source # | |
Defined in Constrained.Spec.SumProd Methods toSimpleRep ∷ Maybe a → SimpleRep (Maybe a) Source # fromSimpleRep ∷ SimpleRep (Maybe a) → Maybe a Source # | |
| (Typeable a, Typeable b) ⇒ HasSimpleRep (Either a b) Source # | |
Defined in Constrained.Spec.SumProd Methods toSimpleRep ∷ Either a b → SimpleRep (Either a b) Source # fromSimpleRep ∷ SimpleRep (Either a b) → Either a b Source # | |
| (Typeable a, Typeable b) ⇒ HasSimpleRep (a, b) Source # | |
Defined in Constrained.Spec.SumProd Methods toSimpleRep ∷ (a, b) → SimpleRep (a, b) Source # fromSimpleRep ∷ SimpleRep (a, b) → (a, b) Source # | |
| (Typeable a, Typeable b, Typeable c) ⇒ HasSimpleRep (a, b, c) Source # | |
Defined in Constrained.Spec.SumProd Methods toSimpleRep ∷ (a, b, c) → SimpleRep (a, b, c) Source # fromSimpleRep ∷ SimpleRep (a, b, c) → (a, b, c) Source # | |
| (Typeable a, Typeable b, Typeable c, Typeable d) ⇒ HasSimpleRep (a, b, c, d) Source # | |
Defined in Constrained.Spec.SumProd Methods toSimpleRep ∷ (a, b, c, d) → SimpleRep (a, b, c, d) Source # fromSimpleRep ∷ SimpleRep (a, b, c, d) → (a, b, c, d) Source # | |
| (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) ⇒ HasSimpleRep (a, b, c, d, e) Source # | |
Defined in Constrained.Spec.SumProd Methods toSimpleRep ∷ (a, b, c, d, e) → SimpleRep (a, b, c, d, e) Source # fromSimpleRep ∷ SimpleRep (a, b, c, d, e) → (a, b, c, d, e) Source # | |
| (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable g) ⇒ HasSimpleRep (a, b, c, d, e, g) Source # | |
Defined in Constrained.Spec.SumProd Methods toSimpleRep ∷ (a, b, c, d, e, g) → SimpleRep (a, b, c, d, e, g) Source # fromSimpleRep ∷ SimpleRep (a, b, c, d, e, g) → (a, b, c, d, e, g) Source # | |
| (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable g, Typeable h) ⇒ HasSimpleRep (a, b, c, d, e, g, h) Source # | |
Defined in Constrained.Spec.SumProd Methods toSimpleRep ∷ (a, b, c, d, e, g, h) → SimpleRep (a, b, c, d, e, g, h) Source # fromSimpleRep ∷ SimpleRep (a, b, c, d, e, g, h) → (a, b, c, d, e, g, h) Source # | |
class (Ord a, HasSpec a) ⇒ OrdLike a where Source #
Minimal complete definition
Nothing
Methods
leqSpec ∷ a → Specification a Source #
default leqSpec ∷ (TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, OrdLike (SimpleRep a)) ⇒ a → Specification a Source #
ltSpec ∷ a → Specification a Source #
default ltSpec ∷ (TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, OrdLike (SimpleRep a)) ⇒ a → Specification a Source #
geqSpec ∷ a → Specification a Source #
default geqSpec ∷ (TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, OrdLike (SimpleRep a)) ⇒ a → Specification a Source #
gtSpec ∷ a → Specification a Source #
default gtSpec ∷ (TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, OrdLike (SimpleRep a)) ⇒ a → Specification a Source #
Instances
| (Ord a, HasSpec a, MaybeBounded a, Num a, TypeSpec a ~ NumSpec a) ⇒ OrdLike a Source # | This instance should be general enough for every type of Number that has a NumSpec as its TypeSpec |
Defined in Constrained.NumSpec Methods leqSpec ∷ a → Specification a Source # ltSpec ∷ a → Specification a Source # geqSpec ∷ a → Specification a Source # gtSpec ∷ a → Specification a Source # | |
conformsToSpecE ∷ ∀ a. HasSpec a ⇒ a → Specification a → NonEmpty String → Maybe (NonEmpty String) Source #
conformsToSpec with explanation. Nothing if (conformsToSpec a spec), but (Just explanations) if not(conformsToSpec a spec).
conformsToSpec ∷ HasSpec a ⇒ a → Specification a → Bool Source #
genFromSpecT ∷ ∀ a m. (HasCallStack, HasSpec a, MonadGenError m) ⇒ Specification a → GenT m a Source #
Generate a value that satisfies the spec. This function can fail if the spec is inconsistent, there is a dependency error, or if the underlying generators are not flexible enough.
genFromSpec ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Specification a → Gen a Source #
A version of genFromSpecT that simply errors if the generator fails
debugSpec ∷ ∀ a. HasSpec a ⇒ Specification a → IO () Source #
A version of genFromSpecT that runs in the IO monad. Good for debugging.
genFromSpecWithSeed ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Int → Int → Specification a → a Source #
A version of genFromSpecT that takes a seed and a size and gives you a result
simplifySpec ∷ HasSpec a ⇒ Specification a → Specification a Source #
cardinality ∷ ∀ a. (Number Integer, HasSpec a) ⇒ Specification a → Specification Integer Source #
Put some (admittedly loose bounds) on the number of solutions that
genFromTypeSpec might return. For lots of types, there is no way to be very accurate.
Here we lift the HasSpec methods cardinalTrueSpec and cardinalTypeSpec
from (TypeSpec Integer) to (Specification Integer)
ifElse ∷ (IsPred p, IsPred q) ⇒ Term Bool → p → q → Pred Source #
If the `Specification Bool` doesn't constrain the boolean you will get a TrueSpec out.
simplifyTerm ∷ ∀ a. Term a → Term a Source #
Simplify a Term, if the Term is an App, apply the rewrite rules
chosen by the (Logic sym t bs a) instance attached
to the function witness f
constrained ∷ ∀ a p. (IsPred p, HasSpec a) ⇒ (Term a → p) → Specification a Source #
assertReified ∷ (HasSpec Bool, HasSpec a) ⇒ Term a → (a → Bool) → Pred Source #
requires (HasSpec Bool)
explanation ∷ NonEmpty String → Pred → Pred Source #
Wrap an Explain around a Pred, unless there is a simpler form.
monitor ∷ ((∀ a. Term a → a) → Property → Property) → Pred Source #
Add QuickCheck monitoring (e.g. collect or counterexample)
to a predicate. To use the monitoring in a property call monitorSpec on the Specification
containing the monitoring and a value generated from the specification.
giveHint ∷ HasGenHint a ⇒ Hint a → Specification a Source #
toGeneric_ ∷ ∀ a. GenericRequires a ⇒ Term a → Term (SimpleRep a) Source #
fromGeneric_ ∷ ∀ a. (GenericRequires a, AppRequires "fromGenericFn" BaseW '[SimpleRep a] a) ⇒ Term (SimpleRep a) → Term a Source #
pair_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term b → Term (a, b) Source #
type IsNormalType a = (Cases a ~ '[a], Args a ~ '[a], IsProd a, CountCases a ~ 1) Source #
left_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term (Either a b) Source #
right_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term b → Term (Either a b) Source #
caseOn ∷ ∀ a. (HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) ⇒ Term a → FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred Source #
branch ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ FunTy (MapList Term (Args a)) p → Weighted Binder a Source #
branchW ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ Int → FunTy (MapList Term (Args a)) p → Weighted Binder a Source #
forAll' ∷ ∀ t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t, HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a), HasSpec a) ⇒ Term t → FunTy (MapList Term (Args (SimpleRep a))) p → Pred Source #
Like forAll but pattern matches on the `Term a`
constrained' ∷ ∀ a p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec a, IsPred p) ⇒ FunTy (MapList Term (Args (SimpleRep a))) p → Specification a Source #
Like constrained but pattern matches on the bound `Term a`
reify' ∷ ∀ a b p. (Cases (SimpleRep b) ~ '[SimpleRep b], TypeSpec b ~ TypeSpec (SimpleRep b), HasSpec (SimpleRep b), HasSimpleRep b, All HasSpec (Args (SimpleRep b)), IsProd (SimpleRep b), HasSpec a, HasSpec b, IsPred p) ⇒ Term a → (a → b) → FunTy (MapList Term (Args (SimpleRep b))) p → Pred Source #
Like reify but pattern matches on the bound `Term b`
con ∷ ∀ c a r. (SimpleRep a ~ SOP (TheSop a), TypeSpec a ~ TypeSpec (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), HasSpec a, HasSimpleRep a, r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a), ResultType r ~ Term a, SOPTerm c (TheSop a), ConstrTerm (ConstrOf c (TheSop a))) ⇒ r Source #
onCon ∷ ∀ c a p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a, HasSpec (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All HasSpec (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term a → FunTy (MapList Term (ConstrOf c (TheSop a))) p → Pred Source #
isCon ∷ ∀ c a. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a, HasSpec (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term a → Pred Source #
sel ∷ ∀ n a c as. (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a, HasSpec (ProdOver as), HasSimpleRep a) ⇒ Term a → Term (At n as) Source #
match ∷ ∀ p a. (HasSpec a, IsProductType a, IsPred p) ⇒ Term a → FunTy (MapList Term (ProductAsList a)) p → Pred Source #
onJust ∷ ∀ a p. (HasSpec a, IsNormalType a, IsPred p) ⇒ Term (Maybe a) → (Term a → p) → Pred Source #
chooseSpec ∷ HasSpec a ⇒ (Int, Specification a) → (Int, Specification a) → Specification a Source #
ChooseSpec is one of the ways we can Or two Specs together
This works for any kind of type that has a HasSpec instance.
If your type is a Sum type. One can use CaseOn which is much easier.
equalSpec ∷ a → Specification a Source #
notEqualSpec ∷ ∀ a. HasSpec a ⇒ a → Specification a Source #
notMemberSpec ∷ ∀ a f. (HasSpec a, Foldable f) ⇒ f a → Specification a Source #
flip_ ∷ ∀ (t ∷ FSType) (sym ∷ Symbol) a b r. (HasSpec b, HasSpec a, HasSpec r, ∀ sym1 t1. Logic sym1 t1 '[a, b] r) ⇒ t sym '[a, b] r → Term b → Term a → Term r Source #
compose_ ∷ ∀ b s1 s2 t1 t2 a r. (AppRequires s1 t1 '[b] r, AppRequires s2 t2 '[a] b) ⇒ t1 s1 '[b] r → t2 s2 '[a] b → Term a → Term r Source #
genFromSizeSpec ∷ MonadGenError m ⇒ Specification Integer → GenT m Integer Source #
Because Sizes should always be >= 0, We provide this alternate generator that can be used to replace (genFromSpecT @Integer), to ensure this important property
maxSpec ∷ Specification Integer → Specification Integer Source #
The widest interval whose largest element is admitted by the original spec
data SetW (s ∷ Symbol) (d ∷ [Type]) (r ∷ Type) where Source #
Constructors
| SingletonW ∷ Ord a ⇒ SetW "singleton_" '[a] (Set a) | |
| UnionW ∷ (Literal a, Ord a) ⇒ SetW "union_" '[Set a, Set a] (Set a) | |
| SubsetW ∷ (Literal a, Ord a) ⇒ SetW "subset_" '[Set a, Set a] Bool | |
| MemberW ∷ (Literal a, Ord a) ⇒ SetW "member_" '[a, Set a] Bool | |
| DisjointW ∷ (Literal a, Ord a) ⇒ SetW "disjoint_" '[Set a, Set a] Bool | |
| FromListW ∷ ∀ a. (HasSpec a, Ord a) ⇒ SetW "fromList_" '[[a]] (Set a) |
Instances
| Semantics SetW Source # | |
| Syntax SetW Source # | |
| (HasSpec a, Ord a) ⇒ Logic "disjoint_" SetW '[Set a, Set a] Bool Source # | |
Defined in Constrained.Spec.Set Methods info ∷ SetW "disjoint_" '[Set a, Set a] Bool → String Source # propagate ∷ Context "disjoint_" SetW '[Set a, Set a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ SetW "disjoint_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → Evidence (AppRequires "disjoint_" SetW '[Set a, Set a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[Set a, Set a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ SetW "disjoint_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "disjoint_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → [Pred] Source # | |
| (HasSpec a, Ord a) ⇒ Logic "member_" SetW '[a, Set a] Bool Source # | |
Defined in Constrained.Spec.Set Methods info ∷ SetW "member_" '[a, Set a] Bool → String Source # propagate ∷ Context "member_" SetW '[a, Set a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ SetW "member_" '[a, Set a] Bool → List Term '[a, Set a] → Evidence (AppRequires "member_" SetW '[a, Set a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, Set a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ SetW "member_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "member_" '[a, Set a] Bool → List Term '[a, Set a] → [Pred] Source # | |
| (HasSpec a, Ord a) ⇒ Logic "subset_" SetW '[Set a, Set a] Bool Source # | |
Defined in Constrained.Spec.Set Methods info ∷ SetW "subset_" '[Set a, Set a] Bool → String Source # propagate ∷ Context "subset_" SetW '[Set a, Set a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ SetW "subset_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → Evidence (AppRequires "subset_" SetW '[Set a, Set a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[Set a, Set a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ SetW "subset_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "subset_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → [Pred] Source # | |
| (HasSpec a, Ord a) ⇒ Logic "fromList_" SetW '[[a]] (Set a) Source # | |
Defined in Constrained.Spec.Set Methods info ∷ SetW "fromList_" '[[a]] (Set a) → String Source # propagate ∷ Context "fromList_" SetW '[[a]] (Set a) hole → Specification (Set a) → Specification hole Source # rewriteRules ∷ SetW "fromList_" '[[a]] (Set a) → List Term '[[a]] → Evidence (AppRequires "fromList_" SetW '[[a]] (Set a)) → Maybe (Term (Set a)) Source # mapTypeSpec ∷ ('[[a]] ~ '[a0], Set a ~ b, HasSpec a0, HasSpec b) ⇒ SetW "fromList_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "fromList_" '[[a]] Bool → List Term '[[a]] → [Pred] Source # | |
| (HasSpec a, Ord a) ⇒ Logic "singleton_" SetW '[a] (Set a) Source # | |
Defined in Constrained.Spec.Set Methods info ∷ SetW "singleton_" '[a] (Set a) → String Source # propagate ∷ Context "singleton_" SetW '[a] (Set a) hole → Specification (Set a) → Specification hole Source # rewriteRules ∷ SetW "singleton_" '[a] (Set a) → List Term '[a] → Evidence (AppRequires "singleton_" SetW '[a] (Set a)) → Maybe (Term (Set a)) Source # mapTypeSpec ∷ ('[a] ~ '[a0], Set a ~ b, HasSpec a0, HasSpec b) ⇒ SetW "singleton_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "singleton_" '[a] Bool → List Term '[a] → [Pred] Source # | |
| (HasSpec a, Ord a) ⇒ Logic "union_" SetW '[Set a, Set a] (Set a) Source # | |
Defined in Constrained.Spec.Set Methods info ∷ SetW "union_" '[Set a, Set a] (Set a) → String Source # propagate ∷ Context "union_" SetW '[Set a, Set a] (Set a) hole → Specification (Set a) → Specification hole Source # rewriteRules ∷ SetW "union_" '[Set a, Set a] (Set a) → List Term '[Set a, Set a] → Evidence (AppRequires "union_" SetW '[Set a, Set a] (Set a)) → Maybe (Term (Set a)) Source # mapTypeSpec ∷ ('[Set a, Set a] ~ '[a0], Set a ~ b, HasSpec a0, HasSpec b) ⇒ SetW "union_" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ SetW "union_" '[Set a, Set a] Bool → List Term '[Set a, Set a] → [Pred] Source # | |
| Show (SetW s ds r) Source # | |
| Eq (SetW s dom rng) Source # | |
Constructors
| SetSpec (Set a) (Specification a) (Specification Integer) |
pattern ToGeneric ∷ ∀ rng. () ⇒ ∀ a. (rng ~ SimpleRep a, GenericRequires a, HasSpec a, AppRequires "toGenericFn" BaseW '[a] rng) ⇒ Term a → Term rng Source #
pattern FromGeneric ∷ ∀ rng. () ⇒ ∀ a. (rng ~ a, GenericRequires a, HasSpec a, AppRequires "fromGenericFn" BaseW '[SimpleRep a] rng) ⇒ Term (SimpleRep a) → Term rng Source #
pattern InjLeft ∷ ∀ c. () ⇒ ∀ a b. (c ~ Sum a b, AppRequires "leftFn" BaseW '[a] c) ⇒ Term a → Term c Source #
pattern InjRight ∷ ∀ c. () ⇒ ∀ a b. (c ~ Sum a b, AppRequires "rightFn" BaseW '[b] c) ⇒ Term b → Term c Source #
pattern ProdFst ∷ ∀ c. () ⇒ ∀ a b. (c ~ a, Typeable (Prod a b), HasSpec a, AppRequires "prodFst_" BaseW '[Prod a b] a) ⇒ Term (Prod a b) → Term c Source #
pattern ProdSnd ∷ ∀ c. () ⇒ ∀ a b. (c ~ b, Typeable (Prod a b), HasSpec b, AppRequires "prodSnd_" BaseW '[Prod a b] b) ⇒ Term (Prod a b) → Term c Source #
pattern Product ∷ ∀ c. () ⇒ ∀ a b. (c ~ Prod a b, AppRequires "prod_" BaseW '[a, b] c) ⇒ Term a → Term b → Term c Source #
printPlan ∷ HasSpec a ⇒ Specification a → IO () Source #
class (Num a, HasSpec a) ⇒ NumLike a Source #
Instances
| Numeric a ⇒ NumLike a Source # | |
Defined in Constrained.NumSpec Methods subtractSpec ∷ a → TypeSpec a → Specification a Source # negateSpec ∷ TypeSpec a → Specification a Source # safeSubtract ∷ a → a → Maybe a Source # | |
Constructors
| Cartesian (Specification a) (Specification b) |
Constructors
| MapSpec | |
Fields
| |
Instances
| (HasSpec (k, v), HasSpec k, HasSpec v, HasSpec [v]) ⇒ Pretty (WithPrec (MapSpec k v)) Source # | |
| (Arbitrary k, Arbitrary v, Arbitrary (TypeSpec k), Arbitrary (TypeSpec v), Ord k, HasSpec k, Foldy v) ⇒ Arbitrary (MapSpec k v) Source # | |
| Generic (MapSpec k v) Source # | |
| (HasSpec (k, v), HasSpec k, HasSpec v, HasSpec [v]) ⇒ Show (MapSpec k v) Source # | |
| type Rep (MapSpec k v) Source # | |
Defined in Constrained.Spec.Map type Rep (MapSpec k v) = D1 ('MetaData "MapSpec" "Constrained.Spec.Map" "constrained-generators-0.2.0.0-inplace" 'False) (C1 ('MetaCons "MapSpec" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mapSpecHint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Integer)) :*: (S1 ('MetaSel ('Just "mapSpecMustKeys") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set k)) :*: S1 ('MetaSel ('Just "mapSpecMustValues") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [v]))) :*: (S1 ('MetaSel ('Just "mapSpecSize") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Specification Integer)) :*: (S1 ('MetaSel ('Just "mapSpecElem") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Specification (k, v))) :*: S1 ('MetaSel ('Just "mapSpecFold") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FoldSpec v)))))) | |
dom_ ∷ (HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term (Set k) Source #
rng_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term [v] Source #
lookup_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term k → Term (Map k v) → Term (Maybe v) Source #
fstSpec ∷ ∀ k v. (HasSpec k, HasSpec v) ⇒ Specification (k, v) → Specification k Source #
sndSpec ∷ ∀ k v. (HasSpec k, HasSpec v) ⇒ Specification (k, v) → Specification v Source #