Safe Haskell	Safe-Inferred
Language	Haskell2010

Constrained.Generation

Contents

Orphan instances

Description

All the things that are necessary for generation and shrinking.

Synopsis

genFromSpecT ∷ ∀ a m. (HasCallStack, HasSpec a, MonadGenError m) ⇒ Specification a → GenT m a
simplifySpec ∷ HasSpec a ⇒ Specification a → Specification 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)
caseSpec ∷ ∀ as. HasSpec (SumOver as) ⇒ Maybe String → List (Weighted Specification) as → Specification (SumOver as)
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
sumType ∷ Maybe String → String
totalWeight ∷ List (Weighted f) as → Maybe Int
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 ()
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
data EqW ∷ [Type] → Type → Type where
- EqualW ∷ (Eq a, HasSpec a) ⇒ EqW '[a, a] Bool
(==.) ∷ HasSpec a ⇒ Term a → Term a → Term Bool
pattern Equal ∷ ∀ b. () ⇒ ∀ a. (b ~ Bool, Eq a, HasSpec a) ⇒ Term a → Term a → Term b
whenTrue ∷ ∀ p. IsPred p ⇒ Term Bool → p → Pred
pinnedBy ∷ ∀ a. HasSpec a ⇒ Var a → Pred → Maybe (Term a)
saturatePred ∷ Pred → [Pred]
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
data SumW dom rng where
- InjLeftW ∷ SumW '[a] (Sum a b)
- InjRightW ∷ SumW '[b] (Sum a b)
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
sumWeightL ∷ Maybe (Int, Int) → Doc a
sumWeightR ∷ Maybe (Int, Int) → Doc a
data BoolW (dom ∷ [Type]) (rng ∷ Type) where
- NotW ∷ BoolW '[Bool] Bool
- OrW ∷ BoolW '[Bool, Bool] Bool
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 SolverStage where
- SolverStage ∷ HasSpec a ⇒ {..} → SolverStage
data SolverPlan = SolverPlan {
- solverPlan ∷ [SolverStage]
- solverDependencies ∷ Graph Name
}
isTrueSpec ∷ Specification a → Bool
prettyLinear ∷ [SolverStage] → Doc ann

Documentation

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.

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

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 #

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).

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.Test 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.Generation 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.Generation 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.Generation 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 #

sumType ∷ Maybe String → String Source #

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

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.

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.

data EqW ∷ [Type] → Type → Type where Source #

Constructors

EqualW ∷ (Eq a, HasSpec a) ⇒ EqW '[a, a] Bool

Instances

Instances details

Syntax EqW Source #
Instance details Defined in Constrained.Generation Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. EqW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. EqW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Logic EqW Source #
Instance details Defined in Constrained.Generation 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 #
Instance details Defined in Constrained.Generation Methods semantics ∷ ∀ (d ∷ [Type]) r. EqW d r → FunTy d r Source #
Show (EqW d r) Source #
Instance details Defined in Constrained.Generation Methods showsPrec ∷ Int → EqW d r → ShowS # show ∷ EqW d r → String # showList ∷ [EqW d r] → ShowS #
Eq (EqW dom rng) Source #
Instance details Defined in Constrained.Generation Methods (==) ∷ EqW dom rng → EqW dom rng → Bool # (/=) ∷ EqW dom rng → EqW dom rng → Bool #

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

pattern Equal ∷ ∀ b. () ⇒ ∀ a. (b ~ Bool, Eq a, HasSpec a) ⇒ Term a → Term a → Term b Source #

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!

saturatePred ∷ Pred → [Pred] 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 #

data SumW dom rng where Source #

Constructors

InjLeftW ∷ SumW '[a] (Sum a b)
InjRightW ∷ SumW '[b] (Sum a b)

Instances

Instances details

Syntax SumW Source #
Instance details Defined in Constrained.Generation Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. SumW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. SumW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Logic SumW Source #
Instance details Defined in Constrained.Generation 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 #
Instance details Defined in Constrained.Generation Methods semantics ∷ ∀ (d ∷ [Type]) r. SumW d r → FunTy d r Source #
Show (SumW dom rng) Source #
Instance details Defined in Constrained.Generation Methods showsPrec ∷ Int → SumW dom rng → ShowS # show ∷ SumW dom rng → String # showList ∷ [SumW dom rng] → ShowS #
Eq (SumW dom rng) Source #
Instance details Defined in Constrained.Generation Methods (==) ∷ SumW dom rng → SumW dom rng → Bool # (/=) ∷ SumW dom rng → SumW dom rng → Bool #

injLeft_ ∷ (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Term a → Term (Sum a b) Source #

injRight_ ∷ (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Term b → Term (Sum a b) 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 #

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

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

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

Operations on Bool

Constructors

NotW ∷ BoolW '[Bool] Bool
OrW ∷ BoolW '[Bool, Bool] Bool

Instances

Instances details

Syntax BoolW Source #
Instance details Defined in Constrained.Generation Methods isInfix ∷ ∀ (dom ∷ [Type]) rng. BoolW dom rng → Bool Source # prettySymbol ∷ ∀ deps (dom ∷ [Type]) rng ann. BoolW dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Logic BoolW Source #
Instance details Defined in Constrained.Generation Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires BoolW as b, HasSpec a) ⇒ BoolW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires BoolW as b, HasSpec a) ⇒ BoolW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires BoolW as b, HasSpec a) ⇒ BoolW 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) ⇒ BoolW dom rng → List Term dom → Evidence (AppRequires BoolW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ BoolW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). BoolW dom Bool → List Term dom → [Pred] Source #
Semantics BoolW Source #
Instance details Defined in Constrained.Generation Methods semantics ∷ ∀ (d ∷ [Type]) r. BoolW d r → FunTy d r Source #
Show (BoolW dom rng) Source #
Instance details Defined in Constrained.Generation Methods showsPrec ∷ Int → BoolW dom rng → ShowS # show ∷ BoolW dom rng → String # showList ∷ [BoolW dom rng] → ShowS #
Eq (BoolW dom rng) Source #
Instance details Defined in Constrained.Generation Methods (==) ∷ BoolW dom rng → BoolW dom rng → Bool # (/=) ∷ BoolW dom rng → BoolW dom rng → Bool #

boolSem ∷ BoolW 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 #

data SolverStage where Source #

Constructors

SolverStage
Fields ∷ HasSpec a ⇒ { stageVar ∷ Var a , stagePreds ∷ [Pred] , stageSpec ∷ Specification a } → SolverStage

Instances

Instances details

Pretty SolverStage Source #
Instance details Defined in Constrained.Generation Methods pretty ∷ SolverStage → Doc ann Source # prettyList ∷ [SolverStage] → Doc ann Source #

data SolverPlan Source #

Constructors

SolverPlan
Fields solverPlan ∷ [SolverStage] solverDependencies ∷ Graph Name

Instances

Instances details

Pretty SolverPlan Source #
Instance details Defined in Constrained.Generation Methods pretty ∷ SolverPlan → Doc ann Source # prettyList ∷ [SolverPlan] → Doc ann Source #