| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Minimal.Model
Contents
Synopsis
- data IntegerSym (dom ∷ [Type]) rng where
- PlusW ∷ IntegerSym '[Integer, Integer] Integer
- MinusW ∷ IntegerSym '[Integer, Integer] Integer
- NegateW ∷ IntegerSym '[Integer] Integer
- LessOrEqW ∷ IntegerSym '[Integer, Integer] Bool
- GreaterOrEqW ∷ IntegerSym '[Integer, Integer] Bool
- negateRange ∷ Range → Range
- minus ∷ Integer → Integer → Integer
- geqSpec ∷ Integer → Spec Integer
- leqSpec ∷ Integer → Spec Integer
- gtSpec ∷ Integer → Spec Integer
- ltSpec ∷ Integer → Spec Integer
- (<=.) ∷ Term Integer → Term Integer → Term Bool
- (>=.) ∷ Term Integer → Term Integer → Term Bool
- (+.) ∷ Term Integer → Term Integer → Term Integer
- (-.) ∷ Term Integer → Term Integer → Term Integer
- negate_ ∷ Term Integer → Term Integer
- data Range = Interval (Maybe Integer) (Maybe Integer)
- constrainInterval ∷ MonadGenError m ⇒ Maybe Integer → Maybe Integer → Integer → m (Integer, Integer)
- data BoolSym (dom ∷ [Type]) rng where
- not_ ∷ Term Bool → Term Bool
- data SetSym (dom ∷ [Type]) rng where
- setSize ∷ Set a → Integer
- size_ ∷ (HasSpec s, Ord s) ⇒ Term (Set s) → Term Integer
- subset_ ∷ (HasSpec s, Ord s) ⇒ Term (Set s) → Term (Set s) → Term Bool
- member_ ∷ (Ord a, HasSpec a) ⇒ Term a → Term (Set a) → Term Bool
- data SetSpec a = SetSpec {}
- guardSetSpec ∷ (HasSpec a, Ord a) ⇒ SetSpec a → Spec (Set a)
- knownUpperBound ∷ Spec Integer → Maybe Integer
- pattern Pair ∷ ∀ c. () ⇒ ∀ a b. (c ~ (a, b), HasSpec a, HasSpec b) ⇒ Term a → Term b → Term c
- data PairSym (dom ∷ [Type]) rng where
- sameFst ∷ Eq a1 ⇒ a1 → [(a1, a2)] → [a2]
- sameSnd ∷ Eq a1 ⇒ a1 → [(a2, a1)] → [a2]
- fst_ ∷ (HasSpec a, HasSpec b) ⇒ Term (a, b) → Term a
- snd_ ∷ (HasSpec a, HasSpec b) ⇒ Term (a, b) → Term b
- pair_ ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Term (a, b)
- data PairSpec a b = Cartesian (Spec a) (Spec b)
- guardPair ∷ ∀ a b. (HasSpec a, HasSpec b) ⇒ Spec a → Spec b → Spec (a, b)
- data EitherSym (dom ∷ [Type]) rng where
- left_ ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term (Either a b)
- right_ ∷ (HasSpec a, HasSpec b) ⇒ Term b → Term (Either a b)
- data SumSpec a b = SumSpec a b
- guardSum ∷ ∀ a b. (HasSpec a, HasSpec b) ⇒ Spec a → Spec b → Spec (Either a b)
- data ListSym (dom ∷ [Type]) rng where
- genFromSpecT ∷ ∀ a m. (HasCallStack, HasSpec a, MonadGenError m) ⇒ Spec a → GenT m a
- genFromSpec ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Spec a → Gen a
- debugSpec ∷ ∀ a. HasSpec a ⇒ Spec a → IO ()
- genFromPreds ∷ ∀ m. MonadGenError m ⇒ Env → Pred → GenT m Env
- simplifySpec ∷ HasSpec a ⇒ Spec a → Spec a
- fromGESpec ∷ HasCallStack ⇒ GE (Spec a) → Spec a
- optimisePred ∷ Pred → Pred
- aggressiveInlining ∷ Pred → Pred
- propagateSpecM ∷ ∀ v a m. (Monad m, HasSpec v) ⇒ Spec a → m (Ctx v a) → m (Spec v)
- computeSpecSimplified ∷ ∀ a. (HasSpec a, HasCallStack) ⇒ Var a → Pred → GE (Spec a)
- computeSpec ∷ ∀ a. (HasSpec a, HasCallStack) ⇒ Var a → Pred → GE (Spec a)
- computeSpecBinder ∷ Binder a → GE (Spec a)
- computeSpecBinderSimplified ∷ Binder a → GE (Spec a)
- substStage ∷ Env → SolverStage → SolverStage
- normalizeSolverStage ∷ SolverStage → SolverStage
- type Hints = DependGraph
- 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
- respecting ∷ Hints → DependGraph → DependGraph
- solvableFrom ∷ Name → Set Name → DependGraph → Bool
- computeHints ∷ [Pred] → Hints
- saturatePred ∷ Pred → [Pred]
- prepareLinearization ∷ Pred → GE SolverPlan
- flattenPred ∷ Pred → [Pred]
- linearize ∷ MonadGenError m ⇒ [Pred] → DependGraph → m [SolverStage]
- mergeSolverStage ∷ SolverStage → [SolverStage] → [SolverStage]
- prettyPlan ∷ HasSpec a ⇒ Spec a → Doc ann
- printPlan ∷ HasSpec a ⇒ Spec a → IO ()
- isEmptyPlan ∷ SolverPlan → Bool
- stepPlan ∷ MonadGenError m ⇒ Env → SolverPlan → GenT m (Env, SolverPlan)
- computeDependencies ∷ Pred → DependGraph
- computeBinderDependencies ∷ Binder a → DependGraph
- computeTermDependencies ∷ Term a → DependGraph
- computeTermDependencies' ∷ Term a → (DependGraph, Set Name)
- backPropagation ∷ SolverPlan → SolverPlan
- spec9 ∷ Spec (Set Integer)
Documentation
data IntegerSym (dom ∷ [Type]) rng where Source #
Constructors
| PlusW ∷ IntegerSym '[Integer, Integer] Integer | |
| MinusW ∷ IntegerSym '[Integer, Integer] Integer | |
| NegateW ∷ IntegerSym '[Integer] Integer | |
| LessOrEqW ∷ IntegerSym '[Integer, Integer] Bool | |
| GreaterOrEqW ∷ IntegerSym '[Integer, Integer] Bool |
Instances
negateRange ∷ Range → Range Source #
constrainInterval ∷ MonadGenError m ⇒ Maybe Integer → Maybe Integer → Integer → m (Integer, Integer) Source #
data BoolSym (dom ∷ [Type]) rng where Source #
Instances
| Logic BoolSym Source # | |
Defined in Test.Minimal.Model Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires BoolSym as b, HasSpec a) ⇒ BoolSym as b → ListCtx as (HOLE a) → TypeSpec b → [b] → Spec a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires BoolSym as b, HasSpec a) ⇒ BoolSym as b → ListCtx as (HOLE a) → NonEmpty b → Spec a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires BoolSym as b, HasSpec a) ⇒ BoolSym as b → ListCtx as (HOLE a) → Spec b → Spec a Source # | |
| Semantics BoolSym Source # | |
| Syntax BoolSym Source # | |
| Show (BoolSym dom rng) Source # | |
| Eq (BoolSym dom rng) Source # | |
data SetSym (dom ∷ [Type]) rng where Source #
Constructors
| MemberW ∷ (HasSpec a, Ord a) ⇒ SetSym [a, Set a] Bool | |
| SizeW ∷ (HasSpec a, Ord a) ⇒ SetSym '[Set a] Integer | |
| SubsetW ∷ (HasSpec a, Ord a) ⇒ SetSym [Set a, Set a] Bool |
Instances
| Logic SetSym Source # | |
Defined in Test.Minimal.Model Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SetSym as b, HasSpec a) ⇒ SetSym as b → ListCtx as (HOLE a) → TypeSpec b → [b] → Spec a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SetSym as b, HasSpec a) ⇒ SetSym as b → ListCtx as (HOLE a) → NonEmpty b → Spec a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires SetSym as b, HasSpec a) ⇒ SetSym as b → ListCtx as (HOLE a) → Spec b → Spec a Source # | |
| Semantics SetSym Source # | |
| Syntax SetSym Source # | |
| Show (SetSym dom rng) Source # | |
| Eq (SetSym dom rng) Source # | |
pattern Pair ∷ ∀ c. () ⇒ ∀ a b. (c ~ (a, b), HasSpec a, HasSpec b) ⇒ Term a → Term b → Term c Source #
data PairSym (dom ∷ [Type]) rng where Source #
Instances
| Logic PairSym Source # | |
Defined in Test.Minimal.Model Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires PairSym as b, HasSpec a) ⇒ PairSym as b → ListCtx as (HOLE a) → TypeSpec b → [b] → Spec a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires PairSym as b, HasSpec a) ⇒ PairSym as b → ListCtx as (HOLE a) → NonEmpty b → Spec a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires PairSym as b, HasSpec a) ⇒ PairSym as b → ListCtx as (HOLE a) → Spec b → Spec a Source # | |
| Semantics PairSym Source # | |
| Syntax PairSym Source # | |
| Show (PairSym dom rng) Source # | |
| Eq (PairSym dom rng) Source # | |
data EitherSym (dom ∷ [Type]) rng where Source #
Instances
| Logic EitherSym Source # | |
Defined in Test.Minimal.Model Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires EitherSym as b, HasSpec a) ⇒ EitherSym as b → ListCtx as (HOLE a) → TypeSpec b → [b] → Spec a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires EitherSym as b, HasSpec a) ⇒ EitherSym as b → ListCtx as (HOLE a) → NonEmpty b → Spec a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires EitherSym as b, HasSpec a) ⇒ EitherSym as b → ListCtx as (HOLE a) → Spec b → Spec a Source # | |
| Semantics EitherSym Source # | |
| Syntax EitherSym Source # | |
| Show (EitherSym dom rng) Source # | |
| Eq (EitherSym dom rng) Source # | |
Constructors
| SumSpec a b |
genFromSpecT ∷ ∀ a m. (HasCallStack, HasSpec a, MonadGenError m) ⇒ Spec a → GenT m a Source #
Generalize genFromTypeSpec from `TypeSpec t` to `Spec t`
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) ⇒ Spec a → Gen a Source #
A version of genFromSpecT that simply errors if the generator fails
debugSpec ∷ ∀ a. HasSpec a ⇒ Spec a → IO () Source #
A version of genFromSpecT that runs in the IO monad. Good for debugging.
genFromPreds ∷ ∀ m. MonadGenError m ⇒ Env → Pred → GenT m Env Source #
fromGESpec ∷ HasCallStack ⇒ GE (Spec a) → Spec a Source #
optimisePred ∷ Pred → Pred Source #
propagateSpecM ∷ ∀ v a m. (Monad m, HasSpec v) ⇒ Spec a → m (Ctx v a) → m (Spec v) Source #
Lifts propagateSpec to take a Monadic Ctx
computeSpecSimplified ∷ ∀ a. (HasSpec a, HasCallStack) ⇒ Var a → Pred → GE (Spec a) Source #
computeSpec ∷ ∀ a. (HasSpec a, HasCallStack) ⇒ Var a → Pred → GE (Spec a) Source #
Precondition: the `Pred fn` defines the `Var a`.
Runs in GE in order for us to have detailed context on failure.
substStage ∷ Env → SolverStage → SolverStage Source #
type Hints = DependGraph Source #
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 #
respecting ∷ Hints → DependGraph → DependGraph Source #
solvableFrom ∷ Name → Set Name → DependGraph → Bool Source #
computeHints ∷ [Pred] → Hints Source #
saturatePred ∷ Pred → [Pred] 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.
isEmptyPlan ∷ SolverPlan → Bool Source #
stepPlan ∷ MonadGenError m ⇒ Env → SolverPlan → GenT m (Env, SolverPlan) Source #
computeTermDependencies' ∷ Term a → (DependGraph, Set Name) Source #
backPropagation ∷ SolverPlan → SolverPlan Source #
Push as much information we can backwards through the plan.