| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Constrained.TheKnot
Contents
Description
All the things that are mutually recursive.
Synopsis
- ifElse ∷ (IsPred p, IsPred q) ⇒ Term Bool → p → q → Pred
- mapSpec ∷ ∀ t a b. AppRequires t '[a] b ⇒ t '[a] b → Specification a → Specification b
- pairView ∷ Term (Prod a b) → Maybe (Term a, Term b)
- cartesian ∷ ∀ a b. (HasSpec a, HasSpec b) ⇒ Specification a → Specification b → Specification (Prod a b)
- data PairSpec a b = Cartesian (Specification a) (Specification b)
- data ProdW ∷ [Type] → Type → Type where
- prodFst_ ∷ (HasSpec a, HasSpec b) ⇒ Term (Prod a b) → Term a
- prodSnd_ ∷ (HasSpec a, HasSpec b) ⇒ Term (Prod a b) → Term b
- sameFst ∷ Eq a1 ⇒ a1 → [Prod a1 a2] → [a2]
- sameSnd ∷ Eq a1 ⇒ a1 → [Prod a2 a1] → [a2]
- prod_ ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Term (Prod a b)
- pattern Product ∷ ∀ c. () ⇒ ∀ a b. (c ~ Prod a b, AppRequires ProdW '[a, b] (Prod a b)) ⇒ Term a → Term b → Term c
- data ElemW ∷ [Type] → Type → Type where
- elem_ ∷ (Sized [a], HasSpec a) ⇒ Term a → Term [a] → Term Bool
- elemFn ∷ HasSpec a ⇒ Fun '[a, [a]] Bool
- pattern Elem ∷ ∀ b. () ⇒ ∀ a. (b ~ Bool, Eq a, HasSpec a) ⇒ Term a → Term [a] → Term b
- data ListSpec a = ListSpec {}
- guardListSpec ∷ HasSpec a ⇒ [String] → ListSpec a → Specification [a]
- sizeOf_ ∷ (HasSpec a, Sized a) ⇒ Term a → Term Integer
- genFromSizeSpec ∷ MonadGenError m ⇒ Specification Integer → GenT m Integer
- data ListW (args ∷ [Type]) (res ∷ Type) where
- listSem ∷ ListW dom rng → FunTy dom rng
- foldMap_ ∷ ∀ a b. (Foldy b, HasSpec a) ⇒ (Term a → Term b) → Term [a] → Term b
- sum_ ∷ Foldy a ⇒ Term [a] → Term a
- singletonList_ ∷ (Sized [a], HasSpec a) ⇒ Term a → Term [a]
- append_ ∷ (Sized [a], HasSpec a) ⇒ Term [a] → Term [a] → Term [a]
- appendFn ∷ ∀ a. (Sized [a], HasSpec a) ⇒ Fun '[[a], [a]] [a]
- singletonListFn ∷ ∀ a. HasSpec a ⇒ Fun '[a] [a]
- foldMapFn ∷ ∀ a b. (HasSpec a, Foldy b) ⇒ Fun '[a] b → Fun '[[a]] b
- reverseFoldSpec ∷ FoldSpec a → Specification a
- prefixedBy ∷ Eq a ⇒ [a] → [[a]] → [[a]]
- suffixedBy ∷ Eq a ⇒ [a] → [[a]] → [[a]]
- alreadyHave ∷ Eq a ⇒ [a] → ListSpec a → ListSpec a
- alreadyHaveFold ∷ [a] → FoldSpec a → FoldSpec a
- toPredsFoldSpec ∷ HasSpec a ⇒ Term [a] → FoldSpec a → Pred
- data FoldSpec a where
- preMapFoldSpec ∷ HasSpec a ⇒ Fun '[a] b → FoldSpec b → FoldSpec a
- composeFn ∷ (HasSpec b, HasSpec c) ⇒ Fun '[b] c → Fun '[a] b → Fun '[a] c
- idFn ∷ HasSpec a ⇒ Fun '[a] a
- combineFoldSpec ∷ FoldSpec a → FoldSpec a → Either [String] (FoldSpec a)
- conformsToFoldSpec ∷ ∀ a. [a] → FoldSpec a → Bool
- class (HasSpec a, NumLike a, Logic IntW) ⇒ Foldy a where
- genList ∷ MonadGenError m ⇒ Specification a → Specification a → GenT m [a]
- theAddFn ∷ IntW '[a, a] a
- theZero ∷ a
- genSizedList ∷ MonadGenError m ⇒ Specification Integer → Specification a → Specification a → GenT m [a]
- noNegativeValues ∷ Bool
- type SizeSpec = NumSpec Integer
- class Sized t where
- sizeOf ∷ t → Integer
- liftSizeSpec ∷ HasSpec t ⇒ SizeSpec → [Integer] → Specification t
- liftMemberSpec ∷ HasSpec t ⇒ [Integer] → Specification t
- sizeOfTypeSpec ∷ HasSpec t ⇒ TypeSpec t → Specification Integer
- adds ∷ Foldy a ⇒ [a] → a
- data FunW (dom ∷ [Type]) (rng ∷ Type) where
- IdW ∷ ∀ a. FunW '[a] a
- ComposeW ∷ ∀ b t1 t2 a r. (AppRequires t1 '[b] r, AppRequires t2 '[a] b, HasSpec b) ⇒ t1 '[b] r → t2 '[a] b → FunW '[a] r
- FlipW ∷ ∀ t a b r. AppRequires t '[a, b] r ⇒ t '[a, b] r → FunW '[b, a] r
- funSem ∷ FunW dom rng → FunTy dom rng
- compareWit ∷ ∀ t1 bs1 r1 t2 bs2 r2. (AppRequires t1 bs1 r1, AppRequires t2 bs2 r2) ⇒ t1 bs1 r1 → t2 bs2 r2 → Bool
- id_ ∷ ∀ a. HasSpec a ⇒ Term a → Term a
- flip_ ∷ ∀ (t ∷ [Type] → Type → Type) a b r. (HasSpec b, HasSpec a, AppRequires t '[a, b] r) ⇒ t '[a, b] r → Term b → Term a → Term r
- compose_ ∷ ∀ b t1 t2 a r. (AppRequires t1 '[b] r, AppRequires t2 '[a] b) ⇒ t1 '[b] r → t2 '[a] b → Term a → Term r
- genInverse ∷ (MonadGenError m, HasSpec a, HasSpec b) ⇒ Fun '[a] b → Specification a → b → GenT m a
- genFromFold ∷ ∀ m a b. (MonadGenError m, Foldy b, HasSpec a) ⇒ [a] → Specification Integer → Specification a → Fun '[a] b → Specification b → GenT m [a]
- addFun ∷ NumLike n ⇒ Fun '[n, n] n
- data SizeW (dom ∷ [Type]) rng ∷ Type where
- sizeOfFn ∷ ∀ a. (HasSpec a, Sized a) ⇒ Fun '[a] Integer
- rangeSize ∷ Integer → Integer → SizeSpec
- between ∷ (HasSpec a, TypeSpec a ~ NumSpec a) ⇒ a → a → Specification a
- maxSpec ∷ Specification Integer → Specification Integer
- hasSize ∷ (HasSpec t, Sized t) ⇒ SizeSpec → Specification t
Documentation
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.
mapSpec ∷ ∀ t a b. AppRequires t '[a] b ⇒ t '[a] b → Specification a → Specification b Source #
Functor like property for Specification, but instead of a Haskell function (a -> b), it takes a function symbol (t '[a] b) from a to b. Note, in this context, a function symbol is some constructor of a witnesstype. Eg. ProdFstW, InjRightW, SingletonW, etc. NOT the lifted versions like fst_ singleton_, which construct Terms. We had to wait until here to define this because it depends on Semigroup property of Specification, and Asserting equality
cartesian ∷ ∀ a b. (HasSpec a, HasSpec b) ⇒ Specification a → Specification b → Specification (Prod a b) Source #
Constructors
| Cartesian (Specification a) (Specification b) |
data ProdW ∷ [Type] → Type → Type where Source #
Constructors
| ProdW ∷ (HasSpec a, HasSpec b) ⇒ ProdW '[a, b] (Prod a b) | |
| ProdFstW ∷ (HasSpec a, HasSpec b) ⇒ ProdW '[Prod a b] a | |
| ProdSndW ∷ (HasSpec a, HasSpec b) ⇒ ProdW '[Prod a b] b |
Instances
| Syntax ProdW Source # | |
| Logic ProdW Source # | |
Defined in Constrained.TheKnot Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires ProdW as b, HasSpec a) ⇒ ProdW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires ProdW as b, HasSpec a) ⇒ ProdW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires ProdW as b, HasSpec a) ⇒ ProdW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source # rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ ProdW dom rng → List Term dom → Evidence (AppRequires ProdW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ ProdW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). ProdW dom Bool → List Term dom → [Pred] Source # | |
| Semantics ProdW Source # | |
| Show (ProdW as b) Source # | |
| Eq (ProdW as b) Source # | |
pattern Product ∷ ∀ c. () ⇒ ∀ a b. (c ~ Prod a b, AppRequires ProdW '[a, b] (Prod a b)) ⇒ Term a → Term b → Term c Source #
data ElemW ∷ [Type] → Type → Type where Source #
Instances
Constructors
| ListSpec | |
Fields | |
guardListSpec ∷ HasSpec a ⇒ [String] → ListSpec a → Specification [a] 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
data ListW (args ∷ [Type]) (res ∷ Type) where Source #
Constructors
| FoldMapW ∷ ∀ a b. (Foldy b, HasSpec a) ⇒ Fun '[a] b → ListW '[[a]] b | |
| SingletonListW ∷ HasSpec a ⇒ ListW '[a] [a] | |
| AppendW ∷ (HasSpec a, Typeable a, Show a) ⇒ ListW '[[a], [a]] [a] |
Instances
| Syntax ListW Source # | |
| Logic ListW Source # | |
Defined in Constrained.TheKnot Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires ListW as b, HasSpec a) ⇒ ListW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires ListW as b, HasSpec a) ⇒ ListW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires ListW as b, HasSpec a) ⇒ ListW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source # rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ ListW dom rng → List Term dom → Evidence (AppRequires ListW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ ListW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). ListW dom Bool → List Term dom → [Pred] Source # | |
| Semantics ListW Source # | |
| Show (ListW d r) Source # | |
| Eq (ListW d r) Source # | |
singletonListFn ∷ ∀ a. HasSpec a ⇒ Fun '[a] [a] Source #
reverseFoldSpec ∷ FoldSpec a → Specification a Source #
prefixedBy ∷ Eq a ⇒ [a] → [[a]] → [[a]] Source #
suffixedBy ∷ Eq a ⇒ [a] → [[a]] → [[a]] Source #
alreadyHaveFold ∷ [a] → FoldSpec a → FoldSpec a Source #
data FoldSpec a where Source #
Constructors
| NoFold ∷ FoldSpec a | |
| FoldSpec ∷ ∀ b a. (HasSpec a, HasSpec b, Foldy b) ⇒ Fun '[a] b → Specification b → FoldSpec a |
Instances
| Arbitrary (FoldSpec (Map k v)) Source # | |
| Arbitrary (FoldSpec (Set a)) Source # | |
| (HasSpec a, HasSpec b, Arbitrary (FoldSpec a), Arbitrary (FoldSpec b)) ⇒ Arbitrary (FoldSpec (a, b)) Source # | |
| (Arbitrary (Specification a), Foldy a) ⇒ Arbitrary (FoldSpec a) Source # | |
| HasSpec a ⇒ Show (FoldSpec a) Source # | |
| HasSpec a ⇒ Pretty (WithPrec (FoldSpec a)) Source # | |
| HasSpec a ⇒ Pretty (FoldSpec a) Source # | |
conformsToFoldSpec ∷ ∀ a. [a] → FoldSpec a → Bool Source #
class (HasSpec a, NumLike a, Logic IntW) ⇒ Foldy a where Source #
Minimal complete definition
Methods
genList ∷ MonadGenError m ⇒ Specification a → Specification a → GenT m [a] Source #
theAddFn ∷ IntW '[a, a] a Source #
genSizedList ∷ MonadGenError m ⇒ Specification Integer → Specification a → Specification a → GenT m [a] Source #
Instances
Minimal complete definition
Nothing
Methods
liftSizeSpec ∷ HasSpec t ⇒ SizeSpec → [Integer] → Specification t Source #
default liftSizeSpec ∷ (Sized (SimpleRep t), GenericRequires t) ⇒ SizeSpec → [Integer] → Specification t Source #
liftMemberSpec ∷ HasSpec t ⇒ [Integer] → Specification t Source #
default liftMemberSpec ∷ (Sized (SimpleRep t), GenericRequires t) ⇒ [Integer] → Specification t Source #
sizeOfTypeSpec ∷ HasSpec t ⇒ TypeSpec t → Specification Integer Source #
Instances
| Ord a ⇒ Sized (Set a) Source # | |
Defined in Constrained.Spec.Set Methods sizeOf ∷ Set a → Integer Source # liftSizeSpec ∷ SizeSpec → [Integer] → Specification (Set a) Source # liftMemberSpec ∷ [Integer] → Specification (Set a) Source # sizeOfTypeSpec ∷ TypeSpec (Set a) → Specification Integer Source # | |
| Sized [a] Source # | |
Defined in Constrained.TheKnot Methods sizeOf ∷ [a] → Integer Source # liftSizeSpec ∷ SizeSpec → [Integer] → Specification [a] Source # liftMemberSpec ∷ [Integer] → Specification [a] Source # sizeOfTypeSpec ∷ TypeSpec [a] → Specification Integer Source # | |
| Ord a ⇒ Sized (Map a b) Source # | |
Defined in Constrained.Spec.Map Methods sizeOf ∷ Map a b → Integer Source # liftSizeSpec ∷ SizeSpec → [Integer] → Specification (Map a b) Source # liftMemberSpec ∷ [Integer] → Specification (Map a b) Source # sizeOfTypeSpec ∷ TypeSpec (Map a b) → Specification Integer Source # | |
data FunW (dom ∷ [Type]) (rng ∷ Type) where Source #
Constructors
| IdW ∷ ∀ a. FunW '[a] a | |
| ComposeW ∷ ∀ b t1 t2 a r. (AppRequires t1 '[b] r, AppRequires t2 '[a] b, HasSpec b) ⇒ t1 '[b] r → t2 '[a] b → FunW '[a] r | |
| FlipW ∷ ∀ t a b r. AppRequires t '[a, b] r ⇒ t '[a, b] r → FunW '[b, a] r |
Instances
| Syntax FunW Source # | |
| Logic FunW Source # | |
Defined in Constrained.TheKnot Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires FunW as b, HasSpec a) ⇒ FunW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires FunW as b, HasSpec a) ⇒ FunW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires FunW as b, HasSpec a) ⇒ FunW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source # rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ FunW dom rng → List Term dom → Evidence (AppRequires FunW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ FunW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). FunW dom Bool → List Term dom → [Pred] Source # | |
| Semantics FunW Source # | |
| Show (FunW dom rng) Source # | |
| Eq (FunW dom rng) Source # | |
compareWit ∷ ∀ t1 bs1 r1 t2 bs2 r2. (AppRequires t1 bs1 r1, AppRequires t2 bs2 r2) ⇒ t1 bs1 r1 → t2 bs2 r2 → Bool Source #
flip_ ∷ ∀ (t ∷ [Type] → Type → Type) a b r. (HasSpec b, HasSpec a, AppRequires t '[a, b] r) ⇒ t '[a, b] r → Term b → Term a → Term r Source #
compose_ ∷ ∀ b t1 t2 a r. (AppRequires t1 '[b] r, AppRequires t2 '[a] b) ⇒ t1 '[b] r → t2 '[a] b → Term a → Term r Source #
genInverse ∷ (MonadGenError m, HasSpec a, HasSpec b) ⇒ Fun '[a] b → Specification a → b → GenT m a Source #
genFromFold ∷ ∀ m a b. (MonadGenError m, Foldy b, HasSpec a) ⇒ [a] → Specification Integer → Specification a → Fun '[a] b → Specification b → GenT m [a] Source #
data SizeW (dom ∷ [Type]) rng ∷ Type where Source #
Instances
| Syntax SizeW Source # | |
| Logic SizeW Source # | |
Defined in Constrained.TheKnot Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SizeW as b, HasSpec a) ⇒ SizeW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SizeW as b, HasSpec a) ⇒ SizeW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires SizeW as b, HasSpec a) ⇒ SizeW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source # rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ SizeW dom rng → List Term dom → Evidence (AppRequires SizeW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ SizeW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). SizeW dom Bool → List Term dom → [Pred] Source # | |
| Semantics SizeW Source # | |
| Show (SizeW d r) Source # | |
| Eq (SizeW ds r) Source # | |
maxSpec ∷ Specification Integer → Specification Integer Source #
The widest interval whose largest element is admitted by the original spec