| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Constrained.TheKnot
Contents
Description
All the things that are mutually recursive.
Synopsis
- data SumSpec a b = SumSpecRaw (Maybe String) (Maybe (Int, Int)) (Specification a) (Specification b)
- pattern SumSpec ∷ Maybe (Int, Int) → Specification a → Specification b → SumSpec a b
- guardSumSpec ∷ ∀ a b. (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ [String] → SumSpec a b → Specification (Sum a b)
- combTypeName ∷ Maybe String → Maybe String → Maybe String
- type family CountCases a where ...
- countCases ∷ ∀ a. KnownNat (CountCases a) ⇒ Int
- totalWeight ∷ List (Weighted f) as → Maybe Int
- sumType ∷ Maybe String → String
- data SumW dom rng where
- injLeft_ ∷ (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Term a → Term (Sum a b)
- injRight_ ∷ (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Term b → Term (Sum a b)
- pattern InjRight ∷ ∀ c. () ⇒ ∀ a b. (c ~ Sum a b, AppRequires SumW '[b] c) ⇒ Term b → Term c
- pattern InjLeft ∷ ∀ c. () ⇒ ∀ a b. (c ~ Sum a b, AppRequires SumW '[a] c) ⇒ Term a → Term c
- caseBoolSpec ∷ HasSpec a ⇒ Specification Bool → (Bool → Specification a) → Specification a
- data BoolW (dom ∷ [Type]) (rng ∷ Type) where
- boolSem ∷ BoolW dom rng → FunTy dom rng
- not_ ∷ Term Bool → Term Bool
- okOr ∷ Bool → Bool → Specification Bool
- or_ ∷ Term Bool → Term Bool → Term Bool
- data EqW ∷ [Type] → Type → Type where
- (==.) ∷ HasSpec a ⇒ Term a → Term a → Term Bool
- pattern Equal ∷ ∀ b. () ⇒ ∀ a. (b ~ Bool, Eq a, HasSpec a) ⇒ Term a → Term a → Term b
- toPredsNumSpec ∷ OrdLike n ⇒ Term n → NumSpec n → Pred
- (<=.) ∷ ∀ 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
- simplifySpec ∷ HasSpec a ⇒ Specification a → Specification a
- ifElse ∷ (IsPred p, IsPred q) ⇒ Term Bool → p → q → Pred
- whenTrue ∷ ∀ p. IsPred p ⇒ Term Bool → p → Pred
- pinnedBy ∷ ∀ a. HasSpec a ⇒ Var a → Pred → Maybe (Term a)
- optimisePred ∷ Pred → Pred
- aggressiveInlining ∷ Pred → Pred
- substituteAndSimplifyTerm ∷ Subst → Term a → Term a
- simplifyTerm ∷ ∀ a. Term a → Term a
- simplifyPred ∷ Pred → Pred
- simplifyPreds ∷ [Pred] → [Pred]
- simplifyBinder ∷ Binder a → Binder a
- computeSpecSimplified ∷ ∀ a. (HasSpec a, HasCallStack) ⇒ Var a → Pred → GE (Specification a)
- computeSpec ∷ ∀ a. (HasSpec a, HasCallStack) ⇒ Var a → Pred → GE (Specification a)
- computeSpecBinder ∷ Binder a → GE (Specification a)
- computeSpecBinderSimplified ∷ Binder a → GE (Specification a)
- sumWeightL ∷ Maybe (Int, Int) → Doc a
- sumWeightR ∷ Maybe (Int, Int) → Doc a
- caseSpec ∷ ∀ as. HasSpec (SumOver as) ⇒ Maybe String → List (Weighted Specification) as → Specification (SumOver as)
- genFromSpecT ∷ ∀ a m. (HasCallStack, HasSpec a, MonadGenError m) ⇒ Specification a → GenT m a
- genFromSpec ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Specification a → Gen a
- genFromSpecWithSeed ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Int → Int → Specification a → a
- debugSpec ∷ ∀ a. HasSpec a ⇒ Specification a → IO ()
- type DependGraph = Graph Name
- dependency ∷ HasVariables t ⇒ Name → t → DependGraph
- irreflexiveDependencyOn ∷ ∀ t t'. (HasVariables t, HasVariables t') ⇒ t → t' → DependGraph
- noDependencies ∷ HasVariables t ⇒ t → DependGraph
- type Hints = DependGraph
- respecting ∷ Hints → DependGraph → DependGraph
- solvableFrom ∷ Name → Set Name → DependGraph → Bool
- computeDependencies ∷ Pred → DependGraph
- computeBinderDependencies ∷ Binder a → DependGraph
- computeTermDependencies ∷ Term a → DependGraph
- computeTermDependencies' ∷ Term a → (DependGraph, Set Name)
- shrinkWithSpec ∷ ∀ a. HasSpec a ⇒ Specification a → a → [a]
- shrinkFromPreds ∷ HasSpec a ⇒ Pred → Var a → a → [a]
- shrinkEnvFromPlan ∷ Env → SolverPlan → [Env]
- substStage ∷ Env → SolverStage → SolverStage
- normalizeSolverStage ∷ SolverStage → SolverStage
- fixupWithSpec ∷ ∀ a. HasSpec a ⇒ Specification a → a → Maybe a
- computeHints ∷ [Pred] → Hints
- prepareLinearization ∷ Pred → GE SolverPlan
- flattenPred ∷ Pred → [Pred]
- linearize ∷ MonadGenError m ⇒ [Pred] → DependGraph → m [SolverStage]
- mergeSolverStage ∷ SolverStage → [SolverStage] → [SolverStage]
- prettyPlan ∷ HasSpec a ⇒ Specification a → Doc ann
- printPlan ∷ HasSpec a ⇒ Specification a → IO ()
- isEmptyPlan ∷ SolverPlan → Bool
- stepPlan ∷ MonadGenError m ⇒ Env → SolverPlan → GenT m (Env, SolverPlan)
- genFromPreds ∷ ∀ m. MonadGenError m ⇒ Env → Pred → GenT m Env
- backPropagation ∷ SolverPlan → SolverPlan
- mapSpec ∷ ∀ t a b. AppRequires t '[a] b ⇒ t '[a] b → Specification a → Specification b
- saturatePred ∷ Pred → [Pred]
- 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
- (+.) ∷ NumLike a ⇒ Term a → Term a → Term a
- negate_ ∷ NumLike a ⇒ Term a → Term a
- (-.) ∷ Numeric n ⇒ Term n → Term n → Term n
Documentation
The Specification for Sums.
Constructors
| SumSpecRaw (Maybe String) (Maybe (Int, Int)) (Specification a) (Specification b) |
Instances
| (Arbitrary (Specification a), Arbitrary (Specification b)) ⇒ Arbitrary (SumSpec a b) Source # | |
| (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Monoid (SumSpec a b) Source # | |
| (HasSpec a, HasSpec b) ⇒ Semigroup (SumSpec a b) Source # | |
| (KnownNat (CountCases b), HasSpec a, HasSpec b) ⇒ Show (SumSpec a b) Source # | |
pattern SumSpec ∷ Maybe (Int, Int) → Specification a → Specification b → SumSpec a b Source #
guardSumSpec ∷ ∀ a b. (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ [String] → SumSpec a b → Specification (Sum a b) Source #
type family CountCases a where ... Source #
Equations
| CountCases (Sum a b) = 1 + CountCases b | |
| CountCases _ = 1 |
countCases ∷ ∀ a. KnownNat (CountCases a) ⇒ Int Source #
data SumW dom rng where Source #
Constructors
| InjLeftW ∷ (HasSpec a, HasSpec b) ⇒ SumW '[a] (Sum a b) | |
| InjRightW ∷ (HasSpec a, HasSpec b) ⇒ SumW '[b] (Sum a b) |
Instances
| Syntax SumW Source # | |
| Logic SumW Source # | |
Defined in Constrained.TheKnot Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SumW as b, HasSpec a) ⇒ SumW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SumW as b, HasSpec a) ⇒ SumW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires SumW as b, HasSpec a) ⇒ SumW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source # rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ SumW dom rng → List Term dom → Evidence (AppRequires SumW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ SumW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). SumW dom Bool → List Term dom → [Pred] Source # | |
| Semantics SumW Source # | |
| Show (SumW dom rng) Source # | |
| Eq (SumW dom rng) Source # | |
pattern InjRight ∷ ∀ c. () ⇒ ∀ a b. (c ~ Sum a b, AppRequires SumW '[b] c) ⇒ Term b → Term c Source #
pattern InjLeft ∷ ∀ c. () ⇒ ∀ a b. (c ~ Sum a b, AppRequires SumW '[a] c) ⇒ Term a → Term c Source #
caseBoolSpec ∷ HasSpec a ⇒ Specification Bool → (Bool → Specification a) → Specification a Source #
data BoolW (dom ∷ [Type]) (rng ∷ Type) where Source #
Operations on Bool
Instances
okOr ∷ Bool → Bool → Specification Bool Source #
We have something like (constant ||. HOLE) must evaluate to need.
Return a (Specification Bool) for HOLE, that makes that True.
data EqW ∷ [Type] → Type → Type where Source #
Instances
| Syntax EqW Source # | |
| Logic EqW Source # | |
Defined in Constrained.TheKnot Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires EqW as b, HasSpec a) ⇒ EqW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires EqW as b, HasSpec a) ⇒ EqW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires EqW as b, HasSpec a) ⇒ EqW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source # rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ EqW dom rng → List Term dom → Evidence (AppRequires EqW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ EqW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). EqW dom Bool → List Term dom → [Pred] Source # | |
| Semantics EqW Source # | |
| Show (EqW d r) Source # | |
| Eq (EqW dom rng) Source # | |
simplifySpec ∷ HasSpec a ⇒ Specification a → Specification a Source #
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.
pinnedBy ∷ ∀ a. HasSpec a ⇒ Var a → Pred → Maybe (Term a) Source #
Is the variable x pinned to some free term in p? (free term meaning that all the variables in the term are free in p).
TODO: complete this with more cases!
optimisePred ∷ Pred → Pred Source #
substituteAndSimplifyTerm ∷ Subst → Term a → Term a Source #
Apply a substitution and simplify the resulting term if the substitution changed the term.
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
simplifyPred ∷ Pred → Pred Source #
simplifyPreds ∷ [Pred] → [Pred] Source #
simplifyBinder ∷ Binder a → Binder a Source #
computeSpecSimplified ∷ ∀ a. (HasSpec a, HasCallStack) ⇒ Var a → Pred → GE (Specification a) Source #
computeSpec ∷ ∀ a. (HasSpec a, HasCallStack) ⇒ Var a → Pred → GE (Specification a) Source #
Precondition: the `Pred fn` defines the `Var a`.
Runs in GE in order for us to have detailed context on failure.
computeSpecBinder ∷ Binder a → GE (Specification a) Source #
computeSpecBinderSimplified ∷ Binder a → GE (Specification a) Source #
caseSpec ∷ ∀ as. HasSpec (SumOver as) ⇒ Maybe String → List (Weighted Specification) as → Specification (SumOver as) Source #
Turn a list of branches into a SumSpec. If all the branches fail return an ErrorSpec. Note the requirement of HasSpec(SumOver).
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
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
debugSpec ∷ ∀ a. HasSpec a ⇒ Specification a → IO () Source #
A version of genFromSpecT that runs in the IO monad. Good for debugging.
type DependGraph = Graph Name Source #
dependency ∷ HasVariables t ⇒ Name → t → DependGraph Source #
irreflexiveDependencyOn ∷ ∀ t t'. (HasVariables t, HasVariables t') ⇒ t → t' → DependGraph Source #
noDependencies ∷ HasVariables t ⇒ t → DependGraph Source #
type Hints = DependGraph Source #
respecting ∷ Hints → DependGraph → DependGraph Source #
solvableFrom ∷ Name → Set Name → DependGraph → Bool Source #
computeTermDependencies' ∷ Term a → (DependGraph, Set Name) Source #
shrinkWithSpec ∷ ∀ a. HasSpec a ⇒ Specification a → a → [a] Source #
shrinkEnvFromPlan ∷ Env → SolverPlan → [Env] Source #
substStage ∷ Env → SolverStage → SolverStage Source #
fixupWithSpec ∷ ∀ a. HasSpec a ⇒ Specification a → a → Maybe a Source #
computeHints ∷ [Pred] → Hints Source #
prepareLinearization ∷ Pred → GE SolverPlan Source #
Linearize a predicate, turning it into a list of variables to solve and their defining constraints such that each variable can be solved independently.
flattenPred ∷ Pred → [Pred] Source #
linearize ∷ MonadGenError m ⇒ [Pred] → DependGraph → m [SolverStage] Source #
mergeSolverStage ∷ SolverStage → [SolverStage] → [SolverStage] Source #
Does nothing if the variable is not in the plan already.
prettyPlan ∷ HasSpec a ⇒ Specification a → Doc ann Source #
isEmptyPlan ∷ SolverPlan → Bool Source #
stepPlan ∷ MonadGenError m ⇒ Env → SolverPlan → GenT m (Env, SolverPlan) Source #
genFromPreds ∷ ∀ m. MonadGenError m ⇒ Env → Pred → GenT m Env Source #
backPropagation ∷ SolverPlan → SolverPlan Source #
Push as much information we can backwards through the plan.
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
saturatePred ∷ Pred → [Pred] Source #
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