Safe Haskell	Safe-Inferred
Language	Haskell2010

Constrained.TheKnot

Contents

Orphan instances

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
caseBoolSpec ∷ HasSpec a ⇒ Specification Bool → (Bool → Specification a) → Specification a
data BoolW (sym ∷ Symbol) (dom ∷ [Type]) (rng ∷ Type) where
- NotW ∷ BoolW "not_" '[Bool] Bool
- OrW ∷ BoolW "or_" '[Bool, Bool] Bool
boolSem ∷ BoolW sym dom rng → FunTy dom rng
not_ ∷ Term Bool → Term Bool
okOr ∷ Bool → Bool → Specification Bool
or_ ∷ Term Bool → Term Bool → Term Bool
(==.) ∷ HasSpec a ⇒ Term a → Term a → Term Bool
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 ∷ ∀ s t a b. (Logic s t '[a] b, HasSpec a, HasSpec b) ⇒ t s '[a] b → Specification a → Specification b
saturatePred ∷ Pred → [Pred]
pairView ∷ ∀ a b. (HasSpec a, HasSpec b) ⇒ 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)
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)

Documentation

data SumSpec a b Source #

The Specification for Sums.

Constructors

SumSpecRaw (Maybe String) (Maybe (Int, Int)) (Specification a) (Specification b)

Instances

Instances details

(Arbitrary (Specification a), Arbitrary (Specification b)) ⇒ Arbitrary (SumSpec a b) Source #
Instance details Defined in Constrained.TheKnot Methods arbitrary ∷ Gen (SumSpec a b) Source # shrink ∷ SumSpec a b → [SumSpec a b] Source #
(HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Monoid (SumSpec a b) Source #
Instance details Defined in Constrained.TheKnot Methods mempty ∷ SumSpec a b mappend ∷ SumSpec a b → SumSpec a b → SumSpec a b mconcat ∷ [SumSpec a b] → SumSpec a b
(HasSpec a, HasSpec b) ⇒ Semigroup (SumSpec a b) Source #
Instance details Defined in Constrained.TheKnot Methods (<>) ∷ SumSpec a b → SumSpec a b → SumSpec a b # sconcat ∷ NonEmpty (SumSpec a b) → SumSpec a b stimes ∷ Integral b0 ⇒ b0 → SumSpec a b → SumSpec a b
(KnownNat (CountCases b), HasSpec a, HasSpec b) ⇒ Show (SumSpec a b) Source #
Instance details Defined in Constrained.TheKnot Methods showsPrec ∷ Int → SumSpec a b → ShowS show ∷ SumSpec a b → String showList ∷ [SumSpec a b] → ShowS

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 #

combTypeName ∷ Maybe String → Maybe String → Maybe String Source #

type family CountCases a where ... Source #

Equations

CountCases (Sum a b) = 1 + CountCases b
CountCases _ = 1

countCases ∷ ∀ a. KnownNat (CountCases a) ⇒ Int Source #

totalWeight ∷ List (Weighted f) as → Maybe Int Source #

sumType ∷ Maybe String → String Source #

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

data BoolW (sym ∷ Symbol) (dom ∷ [Type]) (rng ∷ Type) where Source #

Operations on Bool

Constructors

NotW ∷ BoolW "not_" '[Bool] Bool
OrW ∷ BoolW "or_" '[Bool, Bool] Bool

Instances

Instances details

Semantics BoolW Source #
Instance details Defined in Constrained.TheKnot Methods semantics ∷ ∀ (s ∷ Symbol) (d ∷ [Type]) r. BoolW s d r → FunTy d r Source #
Syntax BoolW Source #
Instance details Defined in Constrained.TheKnot Methods isInFix ∷ ∀ (s ∷ Symbol) (dom ∷ [Type]) rng. BoolW s dom rng → Bool Source # prettyWit ∷ ∀ (s ∷ Symbol) (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ BoolW s dom rng → List Term dom → Int → Maybe (Doc ann) Source #
(HasSpec Bool, TypeSpec Bool ~ SumSpec () ()) ⇒ Logic "not_" BoolW '[Bool] Bool Source #
Instance details 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 #
Instance details 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 #
Instance details Defined in Constrained.TheKnot Methods showsPrec ∷ Int → BoolW s dom rng → ShowS show ∷ BoolW s dom rng → String showList ∷ [BoolW s dom rng] → ShowS
Eq (BoolW s dom rng) Source #
Instance details Defined in Constrained.TheKnot Methods (==) ∷ BoolW s dom rng → BoolW s dom rng → Bool (/=) ∷ BoolW s dom rng → BoolW s dom rng → Bool

boolSem ∷ BoolW sym dom rng → FunTy dom rng Source #

not_ ∷ Term Bool → Term Bool Source #

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.

or_ ∷ Term Bool → Term Bool → Term Bool Source #

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

toPredsNumSpec ∷ OrdLike n ⇒ Term n → NumSpec n → Pred Source #

(<=.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool infixr 4 Source #

(<.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool infixr 4 Source #

(>=.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool infixr 4 Source #

(>.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool infixr 4 Source #

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.

whenTrue ∷ ∀ p. IsPred p ⇒ Term Bool → p → Pred Source #

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 #

aggressiveInlining ∷ 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 #

Precondition: the Pred defines the `Var a` Runs in GE in order for us to have detailed context on failure.

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 #

sumWeightL ∷ Maybe (Int, Int) → Doc a Source #

sumWeightR ∷ Maybe (Int, Int) → Doc 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 #

computeDependencies ∷ Pred → DependGraph Source #

computeBinderDependencies ∷ Binder a → DependGraph Source #

computeTermDependencies ∷ Term a → DependGraph Source #

computeTermDependencies' ∷ Term a → (DependGraph, Set Name) Source #

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

shrinkFromPreds ∷ HasSpec a ⇒ Pred → Var a → a → [a] Source #

shrinkEnvFromPlan ∷ Env → SolverPlan → [Env] Source #

substStage ∷ Env → SolverStage → SolverStage Source #

normalizeSolverStage ∷ 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 #

Flatten nested Let, Exists, and And in a `Pred fn`. Let and Exists bound variables become free in the result.

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 #

printPlan ∷ HasSpec a ⇒ Specification a → IO () 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 #

Generate a satisfying Env for a `p : Pred fn`. The Env contains values for all the free variables in `flattenPred p`.

backPropagation ∷ SolverPlan → SolverPlan Source #

Push as much information we can backwards through the plan.

mapSpec ∷ ∀ s t a b. (Logic s t '[a] b, HasSpec a, HasSpec b) ⇒ t s '[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 c s '[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 #

pairView ∷ ∀ a b. (HasSpec a, HasSpec b) ⇒ Term (Prod a b) → Maybe (Term a, Term b) Source #

cartesian ∷ ∀ a b. (HasSpec a, HasSpec b) ⇒ Specification a → Specification b → Specification (Prod a b) Source #

data PairSpec a b Source #

Constructors

Cartesian (Specification a) (Specification b)

Instances

Instances details

(Arbitrary (Specification a), Arbitrary (Specification b)) ⇒ Arbitrary (PairSpec a b) Source #
Instance details Defined in Constrained.TheKnot Methods arbitrary ∷ Gen (PairSpec a b) Source # shrink ∷ PairSpec a b → [PairSpec a b] Source #
(HasSpec a, HasSpec b) ⇒ Show (PairSpec a b) Source #
Instance details Defined in Constrained.TheKnot Methods showsPrec ∷ Int → PairSpec a b → ShowS show ∷ PairSpec a b → String showList ∷ [PairSpec a b] → ShowS

prodFst_ ∷ (HasSpec a, HasSpec b) ⇒ Term (Prod a b) → Term a Source #

prodSnd_ ∷ (HasSpec a, HasSpec b) ⇒ Term (Prod a b) → Term b Source #

sameFst ∷ Eq a1 ⇒ a1 → [Prod a1 a2] → [a2] Source #

sameSnd ∷ Eq a1 ⇒ a1 → [Prod a2 a1] → [a2] Source #

prod_ ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Term (Prod a b) Source #

Orphan instances

HasSpec Integer Source #
Instance details Associated Types type TypeSpec Integer Source # type Prerequisites Integer Source # Methods emptySpec ∷ TypeSpec Integer Source # combineSpec ∷ TypeSpec Integer → TypeSpec Integer → Specification Integer Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Integer → GenT m Integer Source # conformsTo ∷ Integer → TypeSpec Integer → Bool Source # shrinkWithTypeSpec ∷ TypeSpec Integer → Integer → [Integer] Source # toPreds ∷ Term Integer → TypeSpec Integer → Pred Source # cardinalTypeSpec ∷ TypeSpec Integer → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Integer → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Integer → BinaryShow Source # monadConformsTo ∷ Integer → TypeSpec Integer → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Integer → [Integer] → Specification Integer Source # guardTypeSpec ∷ [String] → TypeSpec Integer → Specification Integer Source # prerequisites ∷ Evidence (Prerequisites Integer) Source #
HasSpec Bool Source #
Instance details Associated Types type TypeSpec Bool Source # type Prerequisites Bool Source # Methods emptySpec ∷ TypeSpec Bool Source # combineSpec ∷ TypeSpec Bool → TypeSpec Bool → Specification Bool Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec Bool → GenT m Bool Source # conformsTo ∷ Bool → TypeSpec Bool → Bool Source # shrinkWithTypeSpec ∷ TypeSpec Bool → Bool → [Bool] Source # toPreds ∷ Term Bool → TypeSpec Bool → Pred Source # cardinalTypeSpec ∷ TypeSpec Bool → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec Bool → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec Bool → BinaryShow Source # monadConformsTo ∷ Bool → TypeSpec Bool → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec Bool → [Bool] → Specification Bool Source # guardTypeSpec ∷ [String] → TypeSpec Bool → Specification Bool Source # prerequisites ∷ Evidence (Prerequisites Bool) Source #
HasSimpleRep Bool Source #
Instance details Associated Types type SimpleRep Bool Source # type TheSop Bool ∷ [Type] Source # Methods toSimpleRep ∷ Bool → SimpleRep Bool Source # fromSimpleRep ∷ SimpleRep Bool → Bool Source #
OrdLike a ⇒ Logic "<." NumOrdW '[a, a] Bool Source #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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, TypeSpec Bool ~ SumSpec () ()) ⇒ Logic "not_" BoolW '[Bool] Bool Source #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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, HasSpec b) ⇒ Logic "prod_" BaseW '[a, b] (Prod a b) Source #
Instance details 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, Arbitrary (TypeSpec a)) ⇒ Arbitrary (Specification a) Source #
Instance details Methods arbitrary ∷ Gen (Specification a) Source # shrink ∷ Specification a → [Specification a] Source #
(HasSpec a, HasSpec b) ⇒ HasSpec (Prod a b) Source #
Instance details Associated Types type TypeSpec (Prod a b) Source # type Prerequisites (Prod a b) Source # Methods emptySpec ∷ TypeSpec (Prod a b) Source # combineSpec ∷ TypeSpec (Prod a b) → TypeSpec (Prod a b) → Specification (Prod a b) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (Prod a b) → GenT m (Prod a b) Source # conformsTo ∷ Prod a b → TypeSpec (Prod a b) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (Prod a b) → Prod a b → [Prod a b] Source # toPreds ∷ Term (Prod a b) → TypeSpec (Prod a b) → Pred Source # cardinalTypeSpec ∷ TypeSpec (Prod a b) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (Prod a b) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (Prod a b) → BinaryShow Source # monadConformsTo ∷ Prod a b → TypeSpec (Prod a b) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (Prod a b) → [Prod a b] → Specification (Prod a b) Source # guardTypeSpec ∷ [String] → TypeSpec (Prod a b) → Specification (Prod a b) Source # prerequisites ∷ Evidence (Prerequisites (Prod a b)) Source #
(HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ HasSpec (Sum a b) Source #	The HasSpec Sum instance
Instance details Associated Types type TypeSpec (Sum a b) Source # type Prerequisites (Sum a b) Source # Methods emptySpec ∷ TypeSpec (Sum a b) Source # combineSpec ∷ TypeSpec (Sum a b) → TypeSpec (Sum a b) → Specification (Sum a b) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (Sum a b) → GenT m (Sum a b) Source # conformsTo ∷ Sum a b → TypeSpec (Sum a b) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (Sum a b) → Sum a b → [Sum a b] Source # toPreds ∷ Term (Sum a b) → TypeSpec (Sum a b) → Pred Source # cardinalTypeSpec ∷ TypeSpec (Sum a b) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (Sum a b) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (Sum a b) → BinaryShow Source # monadConformsTo ∷ Sum a b → TypeSpec (Sum a b) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (Sum a b) → [Sum a b] → Specification (Sum a b) Source # guardTypeSpec ∷ [String] → TypeSpec (Sum a b) → Specification (Sum a b) Source # prerequisites ∷ Evidence (Prerequisites (Sum a b)) Source #