Safe Haskell  SafeInferred 

Language  Haskell2010 
This module contains most of the implementation of the framework.
NOTE: This is a very big module. Splitting it up would
be a nice thing to do but it's not very easy. The problem
is that a lot of the things in here depend on each other
via a cycle like Pred
depends on Term
which depend on
HasSpec
which depends on Specification
and Generic
and Specification
depends in turn on Pred
and so on.
Synopsis
 data Term (fn ∷ [Type] → Type → Type) a where
 type HasSpecImpliesEq fn a f = HasSpec fn a ⇒ Eq (f a) ∷ Constraint
 data Binder fn a where
 data Pred (fn ∷ [Type] → Type → Type) where
 Monitor ∷ ((∀ a. Term fn a → a) → Property → Property) → Pred fn
 Block ∷ [Pred fn] → Pred fn
 Exists ∷ ((∀ b. Term fn b → b) → GE a) → Binder fn a → Pred fn
 Subst ∷ HasSpec fn a ⇒ Var a → Term fn a → Pred fn → Pred fn
 Let ∷ Term fn a → Binder fn a → Pred fn
 Assert ∷ BaseUniverse fn ⇒ NonEmpty String → Term fn Bool → Pred fn
 Reifies ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn b → Term fn a → (a → b) → Pred fn
 DependsOn ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn a → Term fn b → Pred fn
 ForAll ∷ (Forallable t a, HasSpec fn t, HasSpec fn a) ⇒ Term fn t → Binder fn a → Pred fn
 Case ∷ HasSpec fn (SumOver as) ⇒ Term fn (SumOver as) → List (Weighted (Binder fn)) as → Pred fn
 When ∷ HasSpec fn Bool ⇒ Term fn Bool → Pred fn → Pred fn
 GenHint ∷ HasGenHint fn a ⇒ Hint a → Term fn a → Pred fn
 TruePred ∷ Pred fn
 FalsePred ∷ NonEmpty String → Pred fn
 Explain ∷ NonEmpty String → Pred fn → Pred fn
 falsePred1 ∷ String → Pred fn
 data Weighted f a = Weighted {}
 mapWeighted ∷ (f a → g b) → Weighted f a → Weighted g b
 traverseWeighted ∷ Applicative m ⇒ (f a → m (g a)) → Weighted f a → m (Weighted g a)
 data Ctx (fn ∷ [Type] → Type → Type) v a where
 data HOLE a b where
 toCtx ∷ ∀ m fn v a. (BaseUniverse fn, Typeable v, MonadGenError m, HasCallStack) ⇒ Var v → Term fn a → m (Ctx fn v a)
 toCtxList ∷ ∀ m fn v as. (BaseUniverse fn, Typeable v, MonadGenError m, HasCallStack) ⇒ Var v → List (Term fn) as → m (ListCtx Value as (Ctx fn v))
 runTerm ∷ MonadGenError m ⇒ Env → Term fn a → m a
 monitorSpec ∷ (FunctionLike fn, Testable p) ⇒ Specification fn a → a → p → Property
 monitorPred ∷ ∀ fn m. (FunctionLike fn, MonadGenError m) ⇒ Env → Pred fn → m (Property → Property)
 checkPred ∷ ∀ fn m. (FunctionLike fn, MonadGenError m) ⇒ Env → Pred fn → m Bool
 checkPreds ∷ (MonadGenError m, Traversable t, FunctionLike fn) ⇒ Env → t (Pred fn) → m Bool
 checkPredPure ∷ FunctionLike fn ⇒ Env → Pred fn → Bool
 runCaseOn ∷ SumOver as → List (Binder fn) as → (∀ a. HasSpec fn a ⇒ Var a → a → Pred fn → r) → r
 type OrdSet a = [a]
 data Specification fn a where
 MemberSpec ∷ OrdSet a → Specification fn a
 ErrorSpec ∷ NonEmpty String → Specification fn a
 SuspendedSpec ∷ HasSpec fn a ⇒ Var a → Pred fn → Specification fn a
 TypeSpec ∷ HasSpec fn a ⇒ TypeSpec fn a → OrdSet a → Specification fn a
 TrueSpec ∷ Specification fn a
 shrinkPred ∷ Pred fn → [Pred fn]
 isSuspendedSpec ∷ Specification fn a → Bool
 equalSpec ∷ a → Specification fn a
 notEqualSpec ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a
 notMemberSpec ∷ ∀ fn a f. (HasSpec fn a, Foldable f) ⇒ f a → Specification fn a
 typeSpec ∷ HasSpec fn a ⇒ TypeSpec fn a → Specification fn a
 class (Typeable a, Eq a, Show a, Show (TypeSpec fn a), BaseUniverse fn) ⇒ HasSpec fn a where
 type TypeSpec (fn ∷ [Type] → Type → Type) a
 type Prerequisites fn a ∷ Constraint
 emptySpec ∷ TypeSpec fn a
 combineSpec ∷ TypeSpec fn a → TypeSpec fn a → Specification fn a
 genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec fn a → GenT m a
 conformsTo ∷ HasCallStack ⇒ a → TypeSpec fn a → Bool
 shrinkWithTypeSpec ∷ TypeSpec fn a → a → [a]
 toPreds ∷ Term fn a → TypeSpec fn a → Pred fn
 cardinalTypeSpec ∷ TypeSpec fn a → Specification fn Integer
 cardinalTrueSpec ∷ Specification fn Integer
 typeSpecOpt ∷ TypeSpec fn a → [a] → Specification fn a
 prerequisites ∷ Evidence (Prerequisites fn a)
 data WithHasSpec fn f a where
 WithHasSpec ∷ HasSpec fn a ⇒ f a → WithHasSpec fn f a
 class Forallable t e  t → e where
 fromForAllSpec ∷ (HasSpec fn t, HasSpec fn e, BaseUniverse fn) ⇒ Specification fn e → Specification fn t
 forAllToList ∷ t → [e]
 class (HasSpec fn a, Show (Hint a)) ⇒ HasGenHint fn a where
 type Hint a
 giveHint ∷ Hint a → Specification fn a
 conformsToSpecM ∷ ∀ fn a m. (HasSpec fn a, MonadGenError m, Alternative m) ⇒ a → Specification fn a → m ()
 conformsToSpecProp ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a → Property
 conformsToSpec ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a → Bool
 satisfies ∷ ∀ fn a. HasSpec fn a ⇒ Term fn a → Specification fn a → Pred fn
 genFromSpecT ∷ ∀ fn a m. (HasCallStack, HasSpec fn a, MonadGenError m) ⇒ Specification fn a → GenT m a
 shrinkWithSpec ∷ ∀ fn a. HasSpec fn a ⇒ Specification fn a → a → [a]
 genFromSpec ∷ ∀ fn a. (HasCallStack, HasSpec fn a) ⇒ Specification fn a → Gen a
 genFromSpecWithSeed ∷ ∀ fn a. (HasCallStack, HasSpec fn a) ⇒ Int → Int → Specification fn a → a
 genInverse ∷ (MonadGenError m, HasSpec fn a, Show b, Functions fn fn, HasSpec fn b) ⇒ fn '[a] b → Specification fn a → b → GenT m a
 flattenPred ∷ ∀ fn. BaseUniverse fn ⇒ Pred fn → [Pred fn]
 computeDependencies ∷ Pred fn → DependGraph fn
 data SolverStage fn where
 SolverStage ∷ HasSpec fn a ⇒ {..} → SolverStage fn
 data SolverPlan fn = SolverPlan {
 solverPlan ∷ [SolverStage fn]
 solverDependencies ∷ Graph (Name fn)
 isTrueSpec ∷ Specification fn a → Bool
 prettyLinear ∷ [SolverStage fn] → Doc ann
 prepareLinearization ∷ ∀ fn. BaseUniverse fn ⇒ Pred fn → GE (SolverPlan fn)
 mergeSolverStage ∷ SolverStage fn → [SolverStage fn] → [SolverStage fn]
 backPropagation ∷ ∀ fn. SolverPlan fn → SolverPlan fn
 pattern Eql ∷ ∀ fn. () ⇒ ∀ a. HasSpec fn a ⇒ Term fn a → Term fn a → Term fn Bool
 prettyPlan ∷ HasSpec fn a ⇒ Specification fn a → Doc ann
 printPlan ∷ HasSpec fn a ⇒ Specification fn a → IO ()
 isEmptyPlan ∷ SolverPlan fn → Bool
 stepPlan ∷ MonadGenError m ⇒ SolverPlan fn → GenT m (Env, SolverPlan fn)
 substStage ∷ Env → SolverStage fn → SolverStage fn
 genFromPreds ∷ (MonadGenError m, BaseUniverse fn) ⇒ Pred fn → GenT m Env
 computeHints ∷ ∀ fn. [Pred fn] → Hints fn
 computeBinderDependencies ∷ Binder fn a → DependGraph fn
 computeTermDependencies ∷ Term fn a → DependGraph fn
 computeTermDependencies' ∷ Term fn a → (DependGraph fn, Set (Name fn))
 linearize ∷ (MonadGenError m, BaseUniverse fn) ⇒ [Pred fn] → DependGraph fn → m [SolverStage fn]
 normalizeSolverStage ∷ SolverStage fn → SolverStage fn
 fromGESpec ∷ HasCallStack ⇒ GE (Specification fn a) → Specification fn a
 explainSpec ∷ NonEmpty String → Specification fn a → Specification fn a
 regularize ∷ HasVariables fn t ⇒ Var a → t → Var a
 regularizeBinder ∷ Binder fn a → Binder fn a
 regularizeNamesPred ∷ Pred fn → Pred fn
 regularizeNames ∷ Specification fn a → Specification fn a
 simplifySpec ∷ HasSpec fn a ⇒ Specification fn a → Specification fn a
 computeSpecSimplified ∷ ∀ fn a. (HasSpec fn a, HasCallStack) ⇒ Var a → Pred fn → GE (Specification fn a)
 computeSpec ∷ ∀ fn a. (HasSpec fn a, HasCallStack) ⇒ Var a → Pred fn → GE (Specification fn a)
 computeSpecBinder ∷ Binder fn a → GE (Specification fn a)
 computeSpecBinderSimplified ∷ Binder fn a → GE (Specification fn a)
 caseSpec ∷ ∀ fn as. HasSpec fn (SumOver as) ⇒ List (Weighted (Specification fn)) as → Specification fn (SumOver as)
 totalWeight ∷ List (Weighted f) as → Maybe Int
 propagateSpec ∷ ∀ fn v a. HasSpec fn v ⇒ Specification fn a → Ctx fn v a → Specification fn v
 ctxHasSpec ∷ Ctx fn v a → Evidence (HasSpec fn a)
 class (∀ as b. Show (f as b), ∀ as b. Eq (f as b), Typeable f, FunctionLike f) ⇒ Functions f fn where
 propagateSpecFun ∷ (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ f as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a
 rewriteRules ∷ (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ f as b → List (Term fn) as → Maybe (Term fn b)
 mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ f '[a] b → TypeSpec fn a → Specification fn b
 mapSpec ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ fn '[a] b → Specification fn a → Specification fn b
 caseBoolSpec ∷ HasSpec fn a ⇒ Specification fn Bool → (Bool → Specification fn a) → Specification fn a
 isErrorLike ∷ Specification fn a → Bool
 errorLikeMessage ∷ Specification fn a → NonEmpty String
 type DependGraph fn = Graph (Name fn)
 dependency ∷ HasVariables fn t ⇒ Name fn → t → DependGraph fn
 irreflexiveDependencyOn ∷ ∀ fn t t'. (HasVariables fn t, HasVariables fn t') ⇒ t → t' → DependGraph fn
 noDependencies ∷ HasVariables fn t ⇒ t → DependGraph fn
 type Hints fn = DependGraph fn
 respecting ∷ Hints f → DependGraph f → DependGraph f
 solvableFrom ∷ Name f → Set (Name f) → DependGraph f → Bool
 freeVarNames ∷ ∀ fn t. HasVariables fn t ⇒ t → Set Int
 data Name fn where
 newtype FreeVars fn = FreeVars {
 unFreeVars ∷ Map (Name fn) Int
 restrictedTo ∷ FreeVars fn → Set (Name fn) → FreeVars fn
 memberOf ∷ Name fn → FreeVars fn → Bool
 count ∷ Name fn → FreeVars fn → Int
 freeVar ∷ Name fn → FreeVars fn
 singleton ∷ Name fn → Int → FreeVars fn
 without ∷ Foldable t ⇒ FreeVars fn → t (Name fn) → FreeVars fn
 class HasVariables fn a  a → fn where
 type Subst fn = [SubstEntry fn]
 data SubstEntry fn where
 (:=) ∷ HasSpec fn a ⇒ Var a → Term fn a → SubstEntry fn
 backwardsSubstitution ∷ ∀ fn a. HasSpec fn a ⇒ Subst fn → Term fn a → Term fn a
 fastInequality ∷ Term fn a → Term fn b → Bool
 substituteTerm ∷ ∀ fn a. Subst fn → Term fn a → Term fn a
 substituteTerm' ∷ ∀ fn a. Subst fn → Term fn a → Writer Any (Term fn a)
 substituteBinder ∷ HasSpec fn a ⇒ Var a → Term fn a → Binder fn b → Binder fn b
 substitutePred ∷ HasSpec fn a ⇒ Var a → Term fn a → Pred fn → Pred fn
 substTerm ∷ Env → Term fn a → Term fn a
 substBinder ∷ Env → Binder fn a → Binder fn a
 substPred ∷ BaseUniverse fn ⇒ Env → Pred fn → Pred fn
 unBind ∷ a → Binder fn a → Pred fn
 simplifyTerm ∷ ∀ fn a. BaseUniverse fn ⇒ Term fn a → Term fn a
 fromLits ∷ List (Term fn) as → Maybe (List Value as)
 fromLit ∷ Term fn a → Maybe (Value a)
 isLit ∷ Term fn a → Bool
 simplifyPred ∷ ∀ fn. BaseUniverse fn ⇒ Pred fn → Pred fn
 simplifyPreds ∷ BaseUniverse fn ⇒ [Pred fn] → [Pred fn]
 simplifyBinder ∷ Binder fn a → Binder fn a
 pinnedBy ∷ ∀ fn a. (BaseUniverse fn, Typeable a) ⇒ Var a → Pred fn → Maybe (Term fn a)
 optimisePred ∷ BaseUniverse fn ⇒ Pred fn → Pred fn
 letSubexpressionElimination ∷ BaseUniverse fn ⇒ Pred fn → Pred fn
 letFloating ∷ BaseUniverse fn ⇒ Pred fn → Pred fn
 aggressiveInlining ∷ BaseUniverse fn ⇒ Pred fn → Pred fn
 substituteAndSimplifyTerm ∷ BaseUniverse fn ⇒ Subst fn → Term fn a → Term fn a
 class HasSimpleRep a where
 type SimpleRep a
 type TheSop a ∷ [Type]
 toSimpleRep ∷ a → SimpleRep a
 fromSimpleRep ∷ SimpleRep a → a
 type family SimplifyRep f where ...
 toGenericFn ∷ ∀ fn a. (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ fn '[a] (SimpleRep a)
 fromGenericFn ∷ ∀ fn a. (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ fn '[SimpleRep a] a
 data GenericsFn fn args res where
 ToGeneric ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ GenericsFn fn '[a] (SimpleRep a)
 FromGeneric ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ GenericsFn fn '[SimpleRep a] a
 fromSimpleRepSpec ∷ ∀ a fn. (HasSpec fn a, HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Specification fn (SimpleRep a) → Specification fn a
 toSimpleRepSpec ∷ ∀ a fn. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Specification fn a → Specification fn (SimpleRep a)
 data (c ∷ Symbol) ::: (ts ∷ [Type])
 type family SOPOf f where ...
 type family Constr f where ...
 type family SOP constrs where ...
 type family ConstrOf c sop where ...
 class Inject c constrs r where
 inject ∷ ∀ c constrs. Inject c constrs (SOP constrs) ⇒ FunTy (ConstrOf c constrs) (SOP constrs)
 type family ALG constrs r where ...
 class SOPLike constrs r where
 class SimpleConstructor rep where
 toSimpleCon' ∷ rep p → ProdOver (Constr rep)
 fromSimpleCon' ∷ ProdOver (Constr rep) → rep p
 class SopList xs ys where
 class SimpleGeneric rep where
 toSimpleRep' ∷ rep p → SimplifyRep rep
 fromSimpleRep' ∷ SimplifyRep rep → rep p
 class HasSpec fn a ⇒ Foldy fn a where
 genList ∷ (BaseUniverse fn, MonadGenError m) ⇒ Specification fn a → Specification fn a → GenT m [a]
 theAddFn ∷ fn '[a, a] a
 theZero ∷ a
 adds ∷ ∀ fn a. Foldy fn a ⇒ [a] → a
 data FoldSpec (fn ∷ [Type] → Type → Type) a where
 preMapFoldSpec ∷ HasSpec fn a ⇒ fn '[a] b → FoldSpec fn b → FoldSpec fn a
 combineFoldSpec ∷ MonadGenError m ⇒ FoldSpec fn a → FoldSpec fn a → m (FoldSpec fn a)
 conformsToFoldSpec ∷ ∀ fn a. [a] → FoldSpec fn a → Bool
 toPredsFoldSpec ∷ ∀ fn a. BaseUniverse fn ⇒ Term fn [a] → FoldSpec fn a → Pred fn
 enumerateInterval ∷ (Enum a, Num a, Ord a, MaybeBounded a) ⇒ NumSpec a → [a]
 isEmptyNumSpec ∷ (TypeSpec fn a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) ⇒ Specification fn a → Bool
 knownUpperBound ∷ (TypeSpec fn a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) ⇒ Specification fn a → Maybe a
 knownLowerBound ∷ (TypeSpec fn a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) ⇒ Specification fn a → Maybe a
 narrowByFuelAndSize ∷ ∀ a fn. (BaseUniverse fn, TypeSpec fn a ~ NumSpec a, HasSpec fn a, Arbitrary a, Integral a, Ord a, Random a, MaybeBounded a) ⇒ a → Int → (Specification fn a, Specification fn a) → (Specification fn a, Specification fn a)
 narrowFoldSpecs ∷ ∀ a fn. (BaseUniverse fn, TypeSpec fn a ~ NumSpec a, HasSpec fn a, Arbitrary a, Integral a, Ord a, Random a, MaybeBounded a) ⇒ (Specification fn a, Specification fn a) → (Specification fn a, Specification fn a)
 genNumList ∷ ∀ a fn m. (BaseUniverse fn, MonadGenError m, TypeSpec fn a ~ NumSpec a, HasSpec fn a, Arbitrary a, Integral a, Ord a, Random a, MaybeBounded a, Foldy fn a) ⇒ Specification fn a → Specification fn a → GenT m [a]
 genFromFold ∷ ∀ m fn a b. (MonadGenError m, Foldy fn b, HasSpec fn a) ⇒ [a] → Specification fn Integer → Specification fn a → fn '[a] b → Specification fn b → GenT m [a]
 guardSumSpec ∷ (HasSpec fn a, HasSpec fn b, KnownNat (CountCases b)) ⇒ SumSpec fn a b → Specification fn (Sum a b)
 data SumSpec fn a b = SumSpec (Maybe (Int, Int)) (Specification fn a) (Specification fn b)
 type family CountCases a where ...
 countCases ∷ ∀ a. KnownNat (CountCases a) ⇒ Int
 data SetSpec fn a = SetSpec (Set a) (Specification fn a) (Specification fn Integer)
 guardSetSpec ∷ (HasSpec fn a, Ord a) ⇒ SetSpec fn a → Specification fn (Set a)
 data ListSpec fn a = ListSpec {
 listSpecHint ∷ Maybe Integer
 listSpecMust ∷ [a]
 listSpecSize ∷ Specification fn Integer
 listSpecElem ∷ Specification fn a
 listSpecFold ∷ FoldSpec fn a
 class MaybeBounded a where
 lowerBound ∷ Maybe a
 upperBound ∷ Maybe a
 data NumSpec n = NumSpecInterval (Maybe n) (Maybe n)
 emptyNumSpec ∷ Ord a ⇒ NumSpec a
 combineNumSpec ∷ (HasSpec fn n, Ord n, TypeSpec fn n ~ NumSpec n) ⇒ NumSpec n → NumSpec n → Specification fn n
 genFromNumSpec ∷ (MonadGenError m, Show n, Random n, Ord n, Num n, MaybeBounded n) ⇒ NumSpec n → GenT m n
 shrinkWithNumSpec ∷ Arbitrary n ⇒ NumSpec n → n → [n]
 constrainInterval ∷ (MonadGenError m, Ord a, Num a, Show a) ⇒ Maybe a → Maybe a → Integer → m (a, a)
 conformsToNumSpec ∷ Ord n ⇒ n → NumSpec n → Bool
 toPredsNumSpec ∷ (Ord n, OrdLike fn n) ⇒ Term fn n → NumSpec n → Pred fn
 type BaseFns = '[EqFn, SetFn, BoolFn, PairFn, IntFn, OrdFn, GenericsFn, ListFn, SumFn, MapFn, FunFn, SizeFn]
 type BaseFn = Fix (OneofL BaseFns)
 type BaseUniverse fn = (Functions fn fn, Member (EqFn fn) fn, Member (SetFn fn) fn, Member (BoolFn fn) fn, Member (PairFn fn) fn, Member (IntFn fn) fn, Member (OrdFn fn) fn, Member (GenericsFn fn) fn, Member (ListFn fn) fn, Member (SumFn fn) fn, Member (MapFn fn) fn, Member (FunFn fn) fn, Member (SizeFn fn) fn)
 idFn ∷ ∀ fn a. Member (FunFn fn) fn ⇒ fn '[a] a
 composeFn ∷ (Member (FunFn fn) fn, HasSpec fn b, Show (fn '[a] b), Show (fn '[b] c), Eq (fn '[a] b), Eq (fn '[b] c)) ⇒ fn '[b] c → fn '[a] b → fn '[a] c
 flip_ ∷ ∀ fn a b c. (Member (FunFn fn) fn, Typeable a, Typeable b, HasSpec fn a, HasSpec fn b, HasSpec fn c) ⇒ (Term fn a → Term fn b → Term fn c) → Term fn b → Term fn a → Term fn c
 data FunFn fn args res where
 lessOrEqualFn ∷ ∀ fn a. (Ord a, OrdLike fn a) ⇒ fn '[a, a] Bool
 lessFn ∷ ∀ fn a. (Ord a, OrdLike fn a) ⇒ fn '[a, a] Bool
 data OrdFn (fn ∷ [Type] → Type → Type) as b where
 class HasSpec fn a ⇒ OrdLike fn a where
 leqSpec ∷ a → Specification fn a
 ltSpec ∷ a → Specification fn a
 geqSpec ∷ a → Specification fn a
 gtSpec ∷ a → Specification fn a
 data ListFn fn args res where
 foldMapFn ∷ ∀ fn a b. (HasSpec fn a, Foldy fn b, Show (fn '[a] b), Eq (fn '[a] b)) ⇒ fn '[a] b → fn '[[a]] b
 addFn ∷ ∀ fn a. NumLike fn a ⇒ fn '[a, a] a
 negateFn ∷ ∀ fn a. NumLike fn a ⇒ fn '[a] a
 data IntFn (fn ∷ [Type] → Type → Type) as b where
 class (Num a, HasSpec fn a) ⇒ NumLike fn a where
 subtractSpec ∷ a → TypeSpec fn a → Specification fn a
 negateSpec ∷ TypeSpec fn a → Specification fn a
 safeSubtract ∷ a → a → Maybe a
 toGeneric_ ∷ ∀ a fn. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Term fn a → Term fn (SimpleRep a)
 fromGeneric_ ∷ ∀ a fn. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Term fn (SimpleRep a) → Term fn a
 not_ ∷ BaseUniverse fn ⇒ Term fn Bool → Term fn Bool
 (.) ∷ BaseUniverse fn ⇒ Term fn Bool → Term fn Bool → Term fn Bool
 elem_ ∷ ∀ a fn. HasSpec fn a ⇒ Term fn a → Term fn [a] → Term fn Bool
 member_ ∷ ∀ a fn. (HasSpec fn a, Ord a) ⇒ Term fn a → Term fn (Set a) → Term fn Bool
 subset_ ∷ (HasSpec fn a, Ord a) ⇒ Term fn (Set a) → Term fn (Set a) → Term fn Bool
 disjoint_ ∷ (HasSpec fn a, Ord a) ⇒ Term fn (Set a) → Term fn (Set a) → Term fn Bool
 singleton_ ∷ (HasSpec fn a, Ord a) ⇒ Term fn a → Term fn (Set a)
 union_ ∷ ∀ a fn. (HasSpec fn a, Ord a) ⇒ Term fn (Set a) → Term fn (Set a) → Term fn (Set a)
 fromList_ ∷ ∀ a fn. (HasSpec fn a, Ord a) ⇒ Term fn [a] → Term fn (Set a)
 sizeOf_ ∷ ∀ a fn. (HasSpec fn a, Sized a) ⇒ Term fn a → Term fn Integer
 size_ ∷ ∀ a fn. (HasSpec fn (Set a), Ord a) ⇒ Term fn (Set a) → Term fn Integer
 length_ ∷ ∀ a fn. HasSpec fn [a] ⇒ Term fn [a] → Term fn Integer
 null_ ∷ (HasSpec fn a, Sized a) ⇒ Term fn a → Term fn Bool
 (<=.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool
 (>=.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool
 (<.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool
 (>.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool
 (==.) ∷ HasSpec fn a ⇒ Term fn a → Term fn a → Term fn Bool
 (/=.) ∷ HasSpec fn a ⇒ Term fn a → Term fn a → Term fn Bool
 sum_ ∷ (BaseUniverse fn, Member (FunFn fn) fn, Foldy fn a) ⇒ Term fn [a] → Term fn a
 foldMap_ ∷ ∀ fn a b. (BaseUniverse fn, Foldy fn b, HasSpec fn a) ⇒ (Term fn a → Term fn b) → Term fn [a] → Term fn b
 constrained ∷ ∀ a fn p. (IsPred p fn, HasSpec fn a) ⇒ (Term fn a → p) → Specification fn a
 assertExplain ∷ (BaseUniverse fn, IsPred p fn) ⇒ NonEmpty String → p → Pred fn
 assert ∷ (BaseUniverse fn, IsPred p fn) ⇒ p → Pred fn
 forAll ∷ (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) ⇒ Term fn t → (Term fn a → p) → Pred fn
 mkForAll ∷ (Forallable t a, HasSpec fn t, HasSpec fn a) ⇒ Term fn t → Binder fn a → Pred fn
 exists ∷ ∀ a p fn. (HasSpec fn a, IsPred p fn) ⇒ ((∀ b. Term fn b → b) → GE a) → (Term fn a → p) → Pred fn
 unsafeExists ∷ ∀ a p fn. (HasSpec fn a, IsPred p fn) ⇒ (Term fn a → p) → Pred fn
 letBind ∷ (HasSpec fn a, IsPred p fn) ⇒ Term fn a → (Term fn a → p) → Pred fn
 reify ∷ (HasSpec fn a, HasSpec fn b, IsPred p fn) ⇒ Term fn a → (a → b) → (Term fn b → p) → Pred fn
 explanation ∷ NonEmpty String → Pred fn → Pred fn
 monitor ∷ ((∀ a. Term fn a → a) → Property → Property) → Pred fn
 assertReified ∷ HasSpec fn a ⇒ Term fn a → (a → Bool) → Pred fn
 reifies ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn b → Term fn a → (a → b) → Pred fn
 dependsOn ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn a → Term fn b → Pred fn
 lit ∷ Show a ⇒ a → Term fn a
 ifElse ∷ (BaseUniverse fn, IsPred p fn, IsPred q fn) ⇒ Term fn Bool → p → q → Pred fn
 whenTrue ∷ ∀ fn p. (BaseUniverse fn, IsPred p fn) ⇒ Term fn Bool → p → Pred fn
 genHint ∷ ∀ fn t. HasGenHint fn t ⇒ Hint t → Term fn t → Pred fn
 app ∷ (HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) ⇒ fn as b → FunTy (MapList (Term fn) as) (Term fn b)
 name ∷ String → Term fn a → Term fn a
 bind ∷ (HasSpec fn a, IsPred p fn) ⇒ (Term fn a → p) → Binder fn a
 mkCase ∷ HasSpec fn (SumOver as) ⇒ Term fn (SumOver as) → List (Weighted (Binder fn)) as → Pred fn
 type IsPred p fn = (PredLike p, UnivConstr p fn)
 class Show p ⇒ PredLike p where
 type UnivConstr p (fn ∷ [Type] → Type → Type) ∷ Constraint
 toPredExplain ∷ (BaseUniverse fn, UnivConstr p fn) ⇒ [String] → p → Pred fn
 toPred ∷ ∀ fn p. (BaseUniverse fn, PredLike p, UnivConstr p fn) ⇒ p → Pred fn
 data WithPrec a = WithPrec Int a
 parensIf ∷ Bool → Doc ann → Doc ann
 prettyPrec ∷ Pretty (WithPrec a) ⇒ Int → a → Doc ann
 ppList ∷ ∀ fn f as ann. All (HasSpec fn) as ⇒ (∀ a. HasSpec fn a ⇒ f a → Doc ann) → List f as → [Doc ann]
 ppList_ ∷ ∀ f as ann. (∀ a. f a → Doc ann) → List f as → [Doc ann]
 vsep' ∷ [Doc ann] → Doc ann
 (/>) ∷ Doc ann → Doc ann → Doc ann
 genFromSizeSpec ∷ (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Integer → GenT m Integer
 data SizeFn (fn ∷ [Type] → Type → Type) as b where
 sizeOfFn ∷ ∀ fn a. (HasSpec fn a, Member (SizeFn fn) fn, Sized a) ⇒ fn '[a] Integer
 mapTypeSpecSize ∷ ∀ fn a b f. f ~ SizeFn fn ⇒ f '[a] b → TypeSpec fn a → Specification fn b
 type SizeSpec = NumSpec Integer
 rangeSize ∷ Integer → Integer → SizeSpec
 maxSpec ∷ BaseUniverse fn ⇒ Specification fn Integer → Specification fn Integer
 class Sized t where
 sizeOf ∷ t → Integer
 liftSizeSpec ∷ HasSpec fn t ⇒ SizeSpec → [Integer] → Specification fn t
 liftMemberSpec ∷ HasSpec fn t ⇒ OrdSet Integer → Specification fn t
 sizeOfTypeSpec ∷ HasSpec fn t ⇒ TypeSpec fn t → Specification fn Integer
 hasSize ∷ (HasSpec fn t, Sized t) ⇒ SizeSpec → Specification fn t
 guardEmpty ∷ Maybe Integer → Maybe Integer → NumSpec Integer → NumSpec Integer
 addNumSpec ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer
 subNumSpec ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer
 multNumSpec ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer
 negNumSpec ∷ NumSpec Integer → NumSpec Integer
 addSpecInt ∷ BaseUniverse fn ⇒ Specification fn Integer → Specification fn Integer → Specification fn Integer
 subSpecInt ∷ BaseUniverse fn ⇒ Specification fn Integer → Specification fn Integer → Specification fn Integer
 multSpecInt ∷ BaseUniverse fn ⇒ Specification fn Integer → Specification fn Integer → Specification fn Integer
 operateSpec ∷ (TypeSpec fn n ~ NumSpec n, Enum n, Ord n) ⇒ (n → n → n) → (TypeSpec fn n → TypeSpec fn n → TypeSpec fn n) → Specification fn n → Specification fn n → Specification fn n
 cardinality ∷ ∀ fn a. (Eq a, BaseUniverse fn, HasSpec fn a) ⇒ Specification fn a → Specification fn Integer
 cardinalNumSpec ∷ ∀ n fn. (Integral n, Num n, MaybeBounded n) ⇒ NumSpec n → Specification fn Integer
 lowBound ∷ Bounded n ⇒ Maybe n → n
 highBound ∷ Bounded n ⇒ Maybe n → n
 countSpec ∷ ∀ n. (Bounded n, Integral n) ⇒ NumSpec n → Integer
 finiteSize ∷ ∀ n. (Integral n, Bounded n) ⇒ Integer
 notInNumSpec ∷ ∀ fn n. (Functions fn fn, BaseUniverse fn, HasSpec fn n, TypeSpec fn n ~ NumSpec n, Bounded n, Integral n) ⇒ NumSpec n → [n] → Specification fn n
 data T x
 unT ∷ T x → Maybe x
 neg ∷ Maybe x → T x
 pos ∷ Maybe x → T x
 multT ∷ Num x ⇒ T x → T x → T x
 sizeOfSpec ∷ ∀ fn t. (BaseUniverse fn, Sized t) ⇒ Specification fn t → Specification fn Integer
 checkForNegativeSize ∷ Specification fn Integer → Specification fn Integer
Documentation
data Term (fn ∷ [Type] → Type → Type) a where Source #
Typed first order terms with function symbols from fn
.
App ∷ (Typeable as, TypeList as, All (HasSpec fn) as, HasSpec fn b, BaseUniverse fn) ⇒ fn as b → List (Term fn) as → Term fn b  
Lit ∷ Show a ⇒ a → Term fn a  
V ∷ HasSpec fn a ⇒ Var a → Term fn a 
Instances
type HasSpecImpliesEq fn a f = HasSpec fn a ⇒ Eq (f a) ∷ Constraint Source #
data Pred (fn ∷ [Type] → Type → Type) where Source #
Monitor ∷ ((∀ a. Term fn a → a) → Property → Property) → Pred fn  
Block ∷ [Pred fn] → Pred fn  
Exists  
Subst ∷ HasSpec fn a ⇒ Var a → Term fn a → Pred fn → Pred fn  
Let ∷ Term fn a → Binder fn a → Pred fn  
Assert ∷ BaseUniverse fn ⇒ NonEmpty String → Term fn Bool → Pred fn  
Reifies  
DependsOn ∷ (HasSpec fn a, HasSpec fn b) ⇒ Term fn a → Term fn b → Pred fn  
ForAll ∷ (Forallable t a, HasSpec fn t, HasSpec fn a) ⇒ Term fn t → Binder fn a → Pred fn  
Case  
When ∷ HasSpec fn Bool ⇒ Term fn Bool → Pred fn → Pred fn  
GenHint ∷ HasGenHint fn a ⇒ Hint a → Term fn a → Pred fn  
TruePred ∷ Pred fn  
FalsePred ∷ NonEmpty String → Pred fn  
Explain ∷ NonEmpty String → Pred fn → Pred fn 
Instances
HasVariables fn (Pred fn) Source #  
BaseUniverse fn ⇒ Monoid (Pred fn) Source #  
BaseUniverse fn ⇒ Semigroup (Pred fn) Source #  
Show (Pred fn) Source #  
PredLike (Pred fn) Source #  
Defined in Constrained.Base type UnivConstr (Pred fn) fn Source # toPredExplain ∷ ∀ (fn0 ∷ [Type] → Type → Type). (BaseUniverse fn0, UnivConstr (Pred fn) fn0) ⇒ [String] → Pred fn → Pred fn0 Source #  
Rename (Pred fn) Source #  
Pretty (Pred fn) Source #  
type UnivConstr (Pred fn) fn' Source #  
Defined in Constrained.Base 
falsePred1 ∷ String → Pred fn Source #
Instances
mapWeighted ∷ (f a → g b) → Weighted f a → Weighted g b Source #
traverseWeighted ∷ Applicative m ⇒ (f a → m (g a)) → Weighted f a → m (Weighted g a) Source #
data Ctx (fn ∷ [Type] → Type → Type) v a where Source #
Contexts for Terms, basically a term with a _single_ HOLE
instead of a variable. This is used to traverse the defining
constraints for a variable and turn them into a spec. Each
subterm `f vs Ctx vs'` for lists of values vs
and vs
`
gets given to the propagateSpecFun
for f
as
`f vs HOLE vs'`.
This is used together with ListCtx
to form
just the arguments to `f vs Ctx vs'`  replacing
Ctx
with HOLE
 to provide to propagateSpecFun
.
toCtx ∷ ∀ m fn v a. (BaseUniverse fn, Typeable v, MonadGenError m, HasCallStack) ⇒ Var v → Term fn a → m (Ctx fn v a) Source #
toCtxList ∷ ∀ m fn v as. (BaseUniverse fn, Typeable v, MonadGenError m, HasCallStack) ⇒ Var v → List (Term fn) as → m (ListCtx Value as (Ctx fn v)) Source #
monitorSpec ∷ (FunctionLike fn, Testable p) ⇒ Specification fn a → a → p → Property Source #
Collect the monitor
calls from a specification instantiated to the given value. Typically,
>>>
quickCheck $ forAll (genFromSpec spec) $ \ x > monitorSpec spec x $ ...
monitorPred ∷ ∀ fn m. (FunctionLike fn, MonadGenError m) ⇒ Env → Pred fn → m (Property → Property) Source #
checkPred ∷ ∀ fn m. (FunctionLike fn, MonadGenError m) ⇒ Env → Pred fn → m Bool Source #
checkPreds ∷ (MonadGenError m, Traversable t, FunctionLike fn) ⇒ Env → t (Pred fn) → m Bool Source #
checkPredPure ∷ FunctionLike fn ⇒ Env → Pred fn → Bool Source #
runCaseOn ∷ SumOver as → List (Binder fn) as → (∀ a. HasSpec fn a ⇒ Var a → a → Pred fn → r) → r Source #
data Specification fn a where Source #
A `Specification fn a` denotes a set of a
s
MemberSpec  Elements of a known set 
 
ErrorSpec ∷ NonEmpty String → Specification fn a  The empty set 
SuspendedSpec  The set described by some predicates over the bound variable. TODO: possibly we want to use a 
 
TypeSpec  A typespecific spec 
 
TrueSpec ∷ Specification fn a  Anything 
Instances
shrinkPred ∷ Pred fn → [Pred fn] Source #
isSuspendedSpec ∷ Specification fn a → Bool Source #
equalSpec ∷ a → Specification fn a Source #
notEqualSpec ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a Source #
notMemberSpec ∷ ∀ fn a f. (HasSpec fn a, Foldable f) ⇒ f a → Specification fn a Source #
class (Typeable a, Eq a, Show a, Show (TypeSpec fn a), BaseUniverse fn) ⇒ HasSpec fn a where Source #
This class provides the interface that allows you to extend the language
to handle a new type. In the case of types that have a generic representation
(via HasSimpleRep
) that already has an instance of HasSpec
it is sufficient
to provide an empty instance. However, for types that are used together with
specific functions in the function universe fn
it may be necessary to provide
a specific implementation of HasSpec
. This is typically necessary when the Specification
for the generic representation does not permit an implementation of propagateSpecFun
for some function.
The basic types provided in the language, Set
, `[]`, Map
, Int
, Word64
,
(,)
, Either
, etc. have instances of this class (technically (,)
and Either
have
instances derived from the instances for their generic Prod
and Sum
implementations).
Nothing
type TypeSpec (fn ∷ [Type] → Type → Type) a Source #
The `TypeSpec fn a` is the typespecific `Specification fn a`.
type Prerequisites fn a ∷ Constraint Source #
Prerequisites for the instance that are sometimes necessary
when working with e.g. Specification
s or functions in the universe.
type Prerequisites fn a = ()
emptySpec ∷ TypeSpec fn a Source #
default emptySpec ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ TypeSpec fn a Source #
combineSpec ∷ TypeSpec fn a → TypeSpec fn a → Specification fn a Source #
default combineSpec ∷ (HasSimpleRep a, HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ TypeSpec fn a → TypeSpec fn a → Specification fn a Source #
genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec fn a → GenT m a Source #
Generate a value that satisfies the Specification
.
The key property for this generator is soundness:
∀ a ∈ genFromTypeSpec spec. a conformsTo
spec
default genFromTypeSpec ∷ (HasSimpleRep a, HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ (HasCallStack, MonadGenError m) ⇒ TypeSpec fn a → GenT m a Source #
conformsTo ∷ HasCallStack ⇒ a → TypeSpec fn a → Bool Source #
Check conformance to the spec.
default conformsTo ∷ (HasSimpleRep a, HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ HasCallStack ⇒ a → TypeSpec fn a → Bool Source #
shrinkWithTypeSpec ∷ TypeSpec fn a → a → [a] Source #
Shrink an a
with the aide of a Specification
default shrinkWithTypeSpec ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ TypeSpec fn a → a → [a] Source #
toPreds ∷ Term fn a → TypeSpec fn a → Pred fn Source #
Convert a spec to predicates:
The key property here is:
∀ a. a conformsTo
spec == a conformsTo
constrained (t > toPreds t spec)
default toPreds ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ Term fn a → TypeSpec fn a → Pred fn Source #
cardinalTypeSpec ∷ TypeSpec fn a → Specification fn Integer Source #
Compute an upper and lower bound on the number of solutions genFromTypeSpec might return
default cardinalTypeSpec ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ TypeSpec fn a → Specification fn Integer Source #
cardinalTrueSpec ∷ Specification fn Integer Source #
A bound on the number of solutions `genFromTypeSpec TrueSpec` can produce. For a type with finite elements, we can get a much more accurate answer than TrueSpec
typeSpecOpt ∷ TypeSpec fn a → [a] → Specification fn a Source #
For some types (especially finite ones) there may be much better ways to construct
a Specification than the default method of just adding a large bad
list to TypSpec. This
function allows each HasSpec instance to decide.
prerequisites ∷ Evidence (Prerequisites fn a) Source #
Materialize the Prerequisites
dictionary. It should not be necessary to
implement this function manually.
default prerequisites ∷ Prerequisites fn a ⇒ Evidence (Prerequisites fn a) Source #
Instances
data WithHasSpec fn f a where Source #
WithHasSpec ∷ HasSpec fn a ⇒ f a → WithHasSpec fn f a 
Instances
HasSpecImpliesEq fn a f ⇒ Eq (WithHasSpec fn f a) Source #  
Defined in Constrained.Base (==) ∷ WithHasSpec fn f a → WithHasSpec fn f a → Bool Source # (/=) ∷ WithHasSpec fn f a → WithHasSpec fn f a → Bool Source # 
class Forallable t e  t → e where Source #
Nothing
fromForAllSpec ∷ (HasSpec fn t, HasSpec fn e, BaseUniverse fn) ⇒ Specification fn e → Specification fn t Source #
default fromForAllSpec ∷ (HasSpec fn t, HasSpec fn e, HasSimpleRep t, TypeSpec fn t ~ TypeSpec fn (SimpleRep t), Forallable (SimpleRep t) e, HasSpec fn (SimpleRep t)) ⇒ Specification fn e → Specification fn t Source #
forAllToList ∷ t → [e] Source #
default forAllToList ∷ (HasSimpleRep t, Forallable (SimpleRep t) e) ⇒ t → [e] Source #
Instances
class (HasSpec fn a, Show (Hint a)) ⇒ HasGenHint fn a where Source #
Hints are things that only affect generation, and not validation. For instance, parameters to control distribution of generated values.
giveHint ∷ Hint a → Specification fn a Source #
Instances
HasSpec fn a ⇒ HasGenHint fn (BinTree a) Source #  
(Member (TreeFn fn) fn, HasSpec fn a) ⇒ HasGenHint fn (Tree a) Source #  
HasSpec fn a ⇒ HasGenHint fn [a] Source #  
Defined in Constrained.Base giveHint ∷ Hint [a] → Specification fn [a] Source #  
(Ord k, HasSpec fn (Prod k v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) ⇒ HasGenHint fn (Map k v) Source #  
conformsToSpecM ∷ ∀ fn a m. (HasSpec fn a, MonadGenError m, Alternative m) ⇒ a → Specification fn a → m () Source #
conformsToSpecProp ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a → Property Source #
conformsToSpec ∷ ∀ fn a. HasSpec fn a ⇒ a → Specification fn a → Bool Source #
genFromSpecT ∷ ∀ fn a m. (HasCallStack, HasSpec fn a, MonadGenError m) ⇒ Specification fn 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.
shrinkWithSpec ∷ ∀ fn a. HasSpec fn a ⇒ Specification fn a → a → [a] Source #
genFromSpec ∷ ∀ fn a. (HasCallStack, HasSpec fn a) ⇒ Specification fn a → Gen a Source #
A version of genFromSpecT
that simply errors if the generator fails
genFromSpecWithSeed ∷ ∀ fn a. (HasCallStack, HasSpec fn a) ⇒ Int → Int → Specification fn a → a Source #
A version of genFromSpecT
that takes a seed and a size and gives you a result
genInverse ∷ (MonadGenError m, HasSpec fn a, Show b, Functions fn fn, HasSpec fn b) ⇒ fn '[a] b → Specification fn a → b → GenT m a Source #
flattenPred ∷ ∀ fn. BaseUniverse fn ⇒ Pred fn → [Pred fn] Source #
computeDependencies ∷ Pred fn → DependGraph fn Source #
data SolverStage fn where Source #
SolverStage  

Instances
Pretty (SolverStage fn) Source #  
Defined in Constrained.Base pretty ∷ SolverStage fn → Doc ann Source # prettyList ∷ [SolverStage fn] → Doc ann Source # 
data SolverPlan fn Source #
SolverPlan  

Instances
Pretty (SolverPlan fn) Source #  
Defined in Constrained.Base pretty ∷ SolverPlan fn → Doc ann Source # prettyList ∷ [SolverPlan fn] → Doc ann Source # 
isTrueSpec ∷ Specification fn a → Bool Source #
prettyLinear ∷ [SolverStage fn] → Doc ann Source #
prepareLinearization ∷ ∀ fn. BaseUniverse fn ⇒ Pred fn → GE (SolverPlan fn) 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.
mergeSolverStage ∷ SolverStage fn → [SolverStage fn] → [SolverStage fn] Source #
Does nothing if the variable is not in the plan already.
backPropagation ∷ ∀ fn. SolverPlan fn → SolverPlan fn Source #
Push as much information we can backwards through the plan.
prettyPlan ∷ HasSpec fn a ⇒ Specification fn a → Doc ann Source #
isEmptyPlan ∷ SolverPlan fn → Bool Source #
stepPlan ∷ MonadGenError m ⇒ SolverPlan fn → GenT m (Env, SolverPlan fn) Source #
substStage ∷ Env → SolverStage fn → SolverStage fn Source #
genFromPreds ∷ (MonadGenError m, BaseUniverse fn) ⇒ Pred fn → GenT m Env Source #
computeHints ∷ ∀ fn. [Pred fn] → Hints fn Source #
computeBinderDependencies ∷ Binder fn a → DependGraph fn Source #
computeTermDependencies ∷ Term fn a → DependGraph fn Source #
computeTermDependencies' ∷ Term fn a → (DependGraph fn, Set (Name fn)) Source #
linearize ∷ (MonadGenError m, BaseUniverse fn) ⇒ [Pred fn] → DependGraph fn → m [SolverStage fn] Source #
normalizeSolverStage ∷ SolverStage fn → SolverStage fn Source #
fromGESpec ∷ HasCallStack ⇒ GE (Specification fn a) → Specification fn a Source #
explainSpec ∷ NonEmpty String → Specification fn a → Specification fn a Source #
regularize ∷ HasVariables fn t ⇒ Var a → t → Var a Source #
regularizeBinder ∷ Binder fn a → Binder fn a Source #
regularizeNamesPred ∷ Pred fn → Pred fn Source #
regularizeNames ∷ Specification fn a → Specification fn a Source #
simplifySpec ∷ HasSpec fn a ⇒ Specification fn a → Specification fn a Source #
computeSpecSimplified ∷ ∀ fn a. (HasSpec fn a, HasCallStack) ⇒ Var a → Pred fn → GE (Specification fn a) Source #
Precondition: the `Pred fn` defines the `Var a`
Runs in GE
in order for us to have detailed context on failure.
computeSpec ∷ ∀ fn a. (HasSpec fn a, HasCallStack) ⇒ Var a → Pred fn → GE (Specification fn 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 fn a → GE (Specification fn a) Source #
computeSpecBinderSimplified ∷ Binder fn a → GE (Specification fn a) Source #
caseSpec ∷ ∀ fn as. HasSpec fn (SumOver as) ⇒ List (Weighted (Specification fn)) as → Specification fn (SumOver as) Source #
propagateSpec ∷ ∀ fn v a. HasSpec fn v ⇒ Specification fn a → Ctx fn v a → Specification fn v Source #
class (∀ as b. Show (f as b), ∀ as b. Eq (f as b), Typeable f, FunctionLike f) ⇒ Functions f fn where Source #
propagateSpecFun ∷ (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ f as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source #
rewriteRules ∷ (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ f as b → List (Term fn) as → Maybe (Term fn b) Source #
mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ f '[a] b → TypeSpec fn a → Specification fn b Source #
Instances
mapSpec ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ fn '[a] b → Specification fn a → Specification fn b Source #
caseBoolSpec ∷ HasSpec fn a ⇒ Specification fn Bool → (Bool → Specification fn a) → Specification fn a Source #
If the `Specification fn Bool` doesn't constrain the boolean you will get a TrueSpec
out.
isErrorLike ∷ Specification fn a → Bool Source #
errorLikeMessage ∷ Specification fn a → NonEmpty String Source #
type DependGraph fn = Graph (Name fn) Source #
dependency ∷ HasVariables fn t ⇒ Name fn → t → DependGraph fn Source #
irreflexiveDependencyOn ∷ ∀ fn t t'. (HasVariables fn t, HasVariables fn t') ⇒ t → t' → DependGraph fn Source #
noDependencies ∷ HasVariables fn t ⇒ t → DependGraph fn Source #
type Hints fn = DependGraph fn Source #
respecting ∷ Hints f → DependGraph f → DependGraph f Source #
solvableFrom ∷ Name f → Set (Name f) → DependGraph f → Bool Source #
freeVarNames ∷ ∀ fn t. HasVariables fn t ⇒ t → Set Int Source #
FreeVars  

class HasVariables fn a  a → fn where Source #
freeVars ∷ a → FreeVars fn Source #
freeVarSet ∷ a → Set (Name fn) Source #
Instances
HasVariables f (Name f) Source #  
HasVariables f a ⇒ HasVariables f (Set a) Source #  
(Foldable t, HasVariables f a) ⇒ HasVariables f (t a) Source #  
HasVariables fn (Pred fn) Source #  
(HasVariables f a, HasVariables f b) ⇒ HasVariables f (a, b) Source #  
HasVariables fn (Binder fn a) Source #  
HasVariables fn (Term fn a) Source #  
HasVariables fn (f a) ⇒ HasVariables fn (Weighted f a) Source #  
HasVariables fn (List (Term fn) as) Source #  
HasVariables fn (List (Weighted (Binder fn)) as) Source #  
type Subst fn = [SubstEntry fn] Source #
data SubstEntry fn where Source #
(:=) ∷ HasSpec fn a ⇒ Var a → Term fn a → SubstEntry fn 
simplifyTerm ∷ ∀ fn a. BaseUniverse fn ⇒ Term fn a → Term fn a Source #
simplifyPred ∷ ∀ fn. BaseUniverse fn ⇒ Pred fn → Pred fn Source #
simplifyPreds ∷ BaseUniverse fn ⇒ [Pred fn] → [Pred fn] Source #
simplifyBinder ∷ Binder fn a → Binder fn a Source #
pinnedBy ∷ ∀ fn a. (BaseUniverse fn, Typeable a) ⇒ Var a → Pred fn → Maybe (Term fn 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 ∷ BaseUniverse fn ⇒ Pred fn → Pred fn Source #
letSubexpressionElimination ∷ BaseUniverse fn ⇒ Pred fn → Pred fn Source #
letFloating ∷ BaseUniverse fn ⇒ Pred fn → Pred fn Source #
aggressiveInlining ∷ BaseUniverse fn ⇒ Pred fn → Pred fn Source #
substituteAndSimplifyTerm ∷ BaseUniverse fn ⇒ Subst fn → Term fn a → Term fn a Source #
Apply a substitution and simplify the resulting term if the substitution changed the term.
class HasSimpleRep a where Source #
Nothing
toSimpleRep ∷ a → SimpleRep a Source #
default toSimpleRep ∷ (Generic a, SimpleGeneric (Rep a), SimpleRep a ~ SimplifyRep (Rep a)) ⇒ a → SimpleRep a Source #
fromSimpleRep ∷ SimpleRep a → a Source #
default fromSimpleRep ∷ (Generic a, SimpleGeneric (Rep a), SimpleRep a ~ SimplifyRep (Rep a)) ⇒ SimpleRep a → a Source #
Instances
HasSimpleRep Foo Source #  
HasSimpleRep Three Source #  
HasSimpleRep Bool Source #  
Ord a ⇒ HasSimpleRep (NotASet a) Source #  
HasSimpleRep (Maybe a) Source #  
HasSimpleRep (Either a b) Source #  
HasSimpleRep (a, b) Source #  
HasSimpleRep (a, b, c) Source #  
HasSimpleRep (a, b, c, d) Source #  
HasSimpleRep (a, b, c, d, e) Source #  
HasSimpleRep (a, b, c, d, e, g) Source #  
HasSimpleRep (a, b, c, d, e, g, h) Source #  
type family SimplifyRep f where ... Source #
SimplifyRep f = SOP (SOPOf f) 
toGenericFn ∷ ∀ fn a. (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ fn '[a] (SimpleRep a) Source #
fromGenericFn ∷ ∀ fn a. (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ fn '[SimpleRep a] a Source #
data GenericsFn fn args res where Source #
ToGeneric ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ GenericsFn fn '[a] (SimpleRep a)  
FromGeneric ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) ⇒ GenericsFn fn '[SimpleRep a] a 
Instances
FunctionLike (GenericsFn fn) Source #  
Defined in Constrained.Spec.Generics  
BaseUniverse fn ⇒ Functions (GenericsFn fn) fn Source #  
Defined in Constrained.Spec.Generics propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ GenericsFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ GenericsFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ GenericsFn fn '[a] b → TypeSpec fn a → Specification fn b Source #  
Show (GenericsFn fn as b) Source #  
Defined in Constrained.Base  
Eq (GenericsFn fn args res) Source #  
Defined in Constrained.Base (==) ∷ GenericsFn fn args res → GenericsFn fn args res → Bool Source # (/=) ∷ GenericsFn fn args res → GenericsFn fn args res → Bool Source # 
fromSimpleRepSpec ∷ ∀ a fn. (HasSpec fn a, HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Specification fn (SimpleRep a) → Specification fn a Source #
toSimpleRepSpec ∷ ∀ a fn. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Specification fn a → Specification fn (SimpleRep a) Source #
data (c ∷ Symbol) ::: (ts ∷ [Type]) Source #
A constructor name with the types of its arguments
Instances
TypeList prod ⇒ Inject c ((c ::: prod) ': (prod' ': constrs)) r Source #  
TypeList prod ⇒ Inject c '[c ::: prod] r Source #  
(FunTy (ConstrOf c ((c' ::: prod) ': (con ': constrs))) r ~ FunTy (ConstrOf c (con ': constrs)) r, Inject c (con ': constrs) r) ⇒ Inject c ((c' ::: prod) ': (con ': constrs)) r Source #  
(TypeList prod, SOPLike (con ': cases) r) ⇒ SOPLike ((c ::: prod) ': (con ': cases)) r Source #  
TypeList prod ⇒ SOPLike '[c ::: prod] r Source #  
SopList (x' ': xs) (y ': ys) ⇒ SopList ((c ::: x) ': (x' ': xs)) (y ': ys) Source #  
Defined in Constrained.Base injectSOPLeft ∷ SOP ((c ::: x) ': (x' ': xs)) → SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) Source # injectSOPRight ∷ SOP (y ': ys) → SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) Source # caseSOP ∷ SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) → Sum (SOP ((c ::: x) ': (x' ': xs))) (SOP (y ': ys)) Source #  
SopList '[c ::: x] (y ': ys) Source #  
class Inject c constrs r where Source #
Instances
TypeList prod ⇒ Inject c ((c ::: prod) ': (prod' ': constrs)) r Source #  
TypeList prod ⇒ Inject c '[c ::: prod] r Source #  
(FunTy (ConstrOf c ((c' ::: prod) ': (con ': constrs))) r ~ FunTy (ConstrOf c (con ': constrs)) r, Inject c (con ': constrs) r) ⇒ Inject c ((c' ::: prod) ': (con ': constrs)) r Source #  
inject ∷ ∀ c constrs. Inject c constrs (SOP constrs) ⇒ FunTy (ConstrOf c constrs) (SOP constrs) Source #
type family ALG constrs r where ... Source #
An `ALG constrs r` is a function that takes a way to turn every
constructor into an r
:
```
ALG (SOPOf (Rep (Either Int Bool))) r = (Int > r) > (Bool > r) > r
```
class SOPLike constrs r where Source #
algebra ∷ SOP constrs → ALG constrs r Source #
Run a SOP
consts ∷ r → ALG constrs r Source #
Ignore everything in the SOP
class SimpleConstructor rep where Source #
toSimpleCon' ∷ rep p → ProdOver (Constr rep) Source #
fromSimpleCon' ∷ ProdOver (Constr rep) → rep p Source #
Instances
SimpleConstructor (U1 ∷ Type → Type) Source #  
Defined in Constrained.Base  
(SimpleConstructor f, SimpleConstructor g, TypeList (Constr f), TypeList (Constr g)) ⇒ SimpleConstructor (f :*: g) Source #  
Defined in Constrained.Base  
SimpleConstructor (K1 i k ∷ Type → Type) Source #  
Defined in Constrained.Base  
SimpleConstructor f ⇒ SimpleConstructor (S1 s f) Source #  
Defined in Constrained.Base 
class SopList xs ys where Source #
Construct and deconstruct cases in a SOP
injectSOPLeft ∷ SOP xs → SOP (Append xs ys) Source #
injectSOPRight ∷ SOP ys → SOP (Append xs ys) Source #
caseSOP ∷ SOP (Append xs ys) → Sum (SOP xs) (SOP ys) Source #
Instances
SopList (x' ': xs) (y ': ys) ⇒ SopList ((c ::: x) ': (x' ': xs)) (y ': ys) Source #  
Defined in Constrained.Base injectSOPLeft ∷ SOP ((c ::: x) ': (x' ': xs)) → SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) Source # injectSOPRight ∷ SOP (y ': ys) → SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) Source # caseSOP ∷ SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) → Sum (SOP ((c ::: x) ': (x' ': xs))) (SOP (y ': ys)) Source #  
SopList '[c ::: x] (y ': ys) Source #  
class SimpleGeneric rep where Source #
toSimpleRep' ∷ rep p → SimplifyRep rep Source #
fromSimpleRep' ∷ SimplifyRep rep → rep p Source #
Instances
(SimpleGeneric f, SimpleGeneric g, SopList (SOPOf f) (SOPOf g)) ⇒ SimpleGeneric (f :+: g) Source #  
Defined in Constrained.Base toSimpleRep' ∷ (f :+: g) p → SimplifyRep (f :+: g) Source # fromSimpleRep' ∷ SimplifyRep (f :+: g) → (f :+: g) p Source #  
SimpleConstructor f ⇒ SimpleGeneric (C1 ('MetaCons c a b) f) Source #  
Defined in Constrained.Base toSimpleRep' ∷ C1 ('MetaCons c a b) f p → SimplifyRep (C1 ('MetaCons c a b) f) Source # fromSimpleRep' ∷ SimplifyRep (C1 ('MetaCons c a b) f) → C1 ('MetaCons c a b) f p Source #  
SimpleGeneric f ⇒ SimpleGeneric (D1 d f) Source #  
Defined in Constrained.Base toSimpleRep' ∷ D1 d f p → SimplifyRep (D1 d f) Source # fromSimpleRep' ∷ SimplifyRep (D1 d f) → D1 d f p Source # 
class HasSpec fn a ⇒ Foldy fn a where Source #
genList ∷ (BaseUniverse fn, MonadGenError m) ⇒ Specification fn a → Specification fn a → GenT m [a] Source #
Instances
BaseUniverse fn ⇒ Foldy fn Int16 Source #  
Defined in Constrained.Base  
BaseUniverse fn ⇒ Foldy fn Int32 Source #  
Defined in Constrained.Base  
BaseUniverse fn ⇒ Foldy fn Int64 Source #  
Defined in Constrained.Base  
BaseUniverse fn ⇒ Foldy fn Int8 Source #  
Defined in Constrained.Base  
BaseUniverse fn ⇒ Foldy fn Word16 Source #  
Defined in Constrained.Base  
BaseUniverse fn ⇒ Foldy fn Word32 Source #  
Defined in Constrained.Base  
BaseUniverse fn ⇒ Foldy fn Word64 Source #  
Defined in Constrained.Base  
BaseUniverse fn ⇒ Foldy fn Word8 Source #  
Defined in Constrained.Base  
BaseUniverse fn ⇒ Foldy fn Integer Source #  
Defined in Constrained.Base  
BaseUniverse fn ⇒ Foldy fn Natural Source #  
Defined in Constrained.Base  
BaseUniverse fn ⇒ Foldy fn Int Source #  
Defined in Constrained.Base 
data FoldSpec (fn ∷ [Type] → Type → Type) a where Source #
NoFold ∷ FoldSpec fn a  
FoldSpec ∷ ∀ b fn a. (HasSpec fn a, HasSpec fn b, Foldy fn b, Member (ListFn fn) fn, BaseUniverse fn) ⇒ fn '[a] b → Specification fn b → FoldSpec fn a 
Instances
HasSpec fn a ⇒ Pretty (WithPrec (FoldSpec fn a)) Source #  
Arbitrary (FoldSpec fn (Map k v)) Source #  
Arbitrary (FoldSpec fn (Set a)) Source #  
(HasSpec fn a, HasSpec fn b, Arbitrary (FoldSpec fn a), Arbitrary (FoldSpec fn b)) ⇒ Arbitrary (FoldSpec fn (a, b)) Source #  
(Arbitrary a, Arbitrary (TypeSpec fn a), Foldy fn a, BaseUniverse fn) ⇒ Arbitrary (FoldSpec fn a) Source #  
HasSpec fn a ⇒ Show (FoldSpec fn a) Source #  
HasSpec fn a ⇒ Pretty (FoldSpec fn a) Source #  
combineFoldSpec ∷ MonadGenError m ⇒ FoldSpec fn a → FoldSpec fn a → m (FoldSpec fn a) Source #
conformsToFoldSpec ∷ ∀ fn a. [a] → FoldSpec fn a → Bool Source #
toPredsFoldSpec ∷ ∀ fn a. BaseUniverse fn ⇒ Term fn [a] → FoldSpec fn a → Pred fn Source #
enumerateInterval ∷ (Enum a, Num a, Ord a, MaybeBounded a) ⇒ NumSpec a → [a] Source #
Note: potentially infinite list
isEmptyNumSpec ∷ (TypeSpec fn a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) ⇒ Specification fn a → Bool Source #
knownUpperBound ∷ (TypeSpec fn a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) ⇒ Specification fn a → Maybe a Source #
knownLowerBound ∷ (TypeSpec fn a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) ⇒ Specification fn a → Maybe a Source #
∷ ∀ a fn. (BaseUniverse fn, TypeSpec fn a ~ NumSpec a, HasSpec fn a, Arbitrary a, Integral a, Ord a, Random a, MaybeBounded a)  
⇒ a  Fuel 
→ Int  Integer 
→ (Specification fn a, Specification fn a)  
→ (Specification fn a, Specification fn a) 
narrowFoldSpecs ∷ ∀ a fn. (BaseUniverse fn, TypeSpec fn a ~ NumSpec a, HasSpec fn a, Arbitrary a, Integral a, Ord a, Random a, MaybeBounded a) ⇒ (Specification fn a, Specification fn a) → (Specification fn a, Specification fn a) Source #
genNumList ∷ ∀ a fn m. (BaseUniverse fn, MonadGenError m, TypeSpec fn a ~ NumSpec a, HasSpec fn a, Arbitrary a, Integral a, Ord a, Random a, MaybeBounded a, Foldy fn a) ⇒ Specification fn a → Specification fn a → GenT m [a] Source #
genFromFold ∷ ∀ m fn a b. (MonadGenError m, Foldy fn b, HasSpec fn a) ⇒ [a] → Specification fn Integer → Specification fn a → fn '[a] b → Specification fn b → GenT m [a] Source #
guardSumSpec ∷ (HasSpec fn a, HasSpec fn b, KnownNat (CountCases b)) ⇒ SumSpec fn a b → Specification fn (Sum a b) Source #
SumSpec (Maybe (Int, Int)) (Specification fn a) (Specification fn b) 
Instances
(Arbitrary (Specification fn a), Arbitrary (Specification fn b)) ⇒ Arbitrary (SumSpec fn a b) Source #  
(HasSpec fn a, HasSpec fn b, KnownNat (CountCases b)) ⇒ Monoid (SumSpec fn a b) Source #  
(HasSpec fn a, HasSpec fn b) ⇒ Semigroup (SumSpec fn a b) Source #  
(HasSpec fn a, HasSpec fn b) ⇒ Show (SumSpec fn a b) Source #  
type family CountCases a where ... Source #
CountCases (Sum a b) = 1 + CountCases b  
CountCases _ = 1 
countCases ∷ ∀ a. KnownNat (CountCases a) ⇒ Int Source #
SetSpec (Set a) (Specification fn a) (Specification fn Integer) 
guardSetSpec ∷ (HasSpec fn a, Ord a) ⇒ SetSpec fn a → Specification fn (Set a) Source #
ListSpec  

class MaybeBounded a where Source #
Nothing
lowerBound ∷ Maybe a Source #
default lowerBound ∷ Bounded a ⇒ Maybe a Source #
upperBound ∷ Maybe a Source #
default upperBound ∷ Bounded a ⇒ Maybe a Source #
Instances
MaybeBounded Int16 Source #  
Defined in Constrained.Base  
MaybeBounded Int32 Source #  
Defined in Constrained.Base  
MaybeBounded Int64 Source #  
Defined in Constrained.Base  
MaybeBounded Int8 Source #  
Defined in Constrained.Base  
MaybeBounded Word16 Source #  
Defined in Constrained.Base  
MaybeBounded Word32 Source #  
Defined in Constrained.Base  
MaybeBounded Word64 Source #  
Defined in Constrained.Base  
MaybeBounded Word8 Source #  
Defined in Constrained.Base  
MaybeBounded Integer Source #  
Defined in Constrained.Base  
MaybeBounded Natural Source #  
Defined in Constrained.Base  
MaybeBounded Float Source #  
Defined in Constrained.Base  
MaybeBounded Int Source #  
Defined in Constrained.Base  
MaybeBounded (Ratio Integer) Source #  
Defined in Constrained.Base 
NumSpecInterval (Maybe n) (Maybe n) 
Instances
(Arbitrary a, Ord a) ⇒ Arbitrary (NumSpec a) Source #  
Ord n ⇒ Monoid (NumSpec n) Source #  
Ord n ⇒ Semigroup (NumSpec n) Source #  
Num (NumSpec Integer) Source #  
Defined in Constrained.Base (+) ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer Source # () ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer Source # (*) ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer Source # negate ∷ NumSpec Integer → NumSpec Integer Source # abs ∷ NumSpec Integer → NumSpec Integer Source #  
Show n ⇒ Show (NumSpec n) Source #  
Ord n ⇒ Eq (NumSpec n) Source #  
emptyNumSpec ∷ Ord a ⇒ NumSpec a Source #
combineNumSpec ∷ (HasSpec fn n, Ord n, TypeSpec fn n ~ NumSpec n) ⇒ NumSpec n → NumSpec n → Specification fn n Source #
genFromNumSpec ∷ (MonadGenError m, Show n, Random n, Ord n, Num n, MaybeBounded n) ⇒ NumSpec n → GenT m n Source #
shrinkWithNumSpec ∷ Arbitrary n ⇒ NumSpec n → n → [n] Source #
constrainInterval ∷ (MonadGenError m, Ord a, Num a, Show a) ⇒ Maybe a → Maybe a → Integer → m (a, a) Source #
type BaseFns = '[EqFn, SetFn, BoolFn, PairFn, IntFn, OrdFn, GenericsFn, ListFn, SumFn, MapFn, FunFn, SizeFn] Source #
type BaseUniverse fn = (Functions fn fn, Member (EqFn fn) fn, Member (SetFn fn) fn, Member (BoolFn fn) fn, Member (PairFn fn) fn, Member (IntFn fn) fn, Member (OrdFn fn) fn, Member (GenericsFn fn) fn, Member (ListFn fn) fn, Member (SumFn fn) fn, Member (MapFn fn) fn, Member (FunFn fn) fn, Member (SizeFn fn) fn) Source #
A minimal Universe contains functions for a bunch of different things.
composeFn ∷ (Member (FunFn fn) fn, HasSpec fn b, Show (fn '[a] b), Show (fn '[b] c), Eq (fn '[a] b), Eq (fn '[b] c)) ⇒ fn '[b] c → fn '[a] b → fn '[a] c Source #
flip_ ∷ ∀ fn a b c. (Member (FunFn fn) fn, Typeable a, Typeable b, HasSpec fn a, HasSpec fn b, HasSpec fn c) ⇒ (Term fn a → Term fn b → Term fn c) → Term fn b → Term fn a → Term fn c Source #
data FunFn fn args res where Source #
Id ∷ FunFn fn '[a] a  
Compose ∷ (Typeable b, HasSpec fn b, Show (fn '[a] b), Show (fn '[b] c), Eq (fn '[a] b), Eq (fn '[b] c)) ⇒ fn '[b] c → fn '[a] b → FunFn fn '[a] c  
Flip ∷ (Show (fn '[a, b] c), Eq (fn '[a, b] c), HasSpec fn a, HasSpec fn b) ⇒ fn '[a, b] c → FunFn fn '[b, a] c 
Instances
FunctionLike fn ⇒ FunctionLike (FunFn fn) Source #  
(BaseUniverse fn, Member (FunFn fn) fn) ⇒ Functions (FunFn fn) fn Source #  
Defined in Constrained.Base propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ FunFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ FunFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ FunFn fn '[a] b → TypeSpec fn a → Specification fn b Source #  
Show (FunFn fn args res) Source #  
Typeable fn ⇒ Eq (FunFn fn args res) Source #  
data OrdFn (fn ∷ [Type] → Type → Type) as b where Source #
LessOrEqual ∷ (Ord a, OrdLike fn a) ⇒ OrdFn fn '[a, a] Bool  
Less ∷ (Ord a, OrdLike fn a) ⇒ OrdFn fn '[a, a] Bool 
Instances
FunctionLike (OrdFn fn) Source #  
BaseUniverse fn ⇒ Functions (OrdFn fn) fn Source #  
Defined in Constrained.Base propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ OrdFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ OrdFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ OrdFn fn '[a] b → TypeSpec fn a → Specification fn b Source #  
Show (OrdFn fn as b) Source #  
Eq (OrdFn fn as b) Source #  
class HasSpec fn a ⇒ OrdLike fn a where Source #
Nothing
leqSpec ∷ a → Specification fn a Source #
default leqSpec ∷ (TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, OrdLike fn (SimpleRep a)) ⇒ a → Specification fn a Source #
ltSpec ∷ a → Specification fn a Source #
default ltSpec ∷ (TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, OrdLike fn (SimpleRep a)) ⇒ a → Specification fn a Source #
geqSpec ∷ a → Specification fn a Source #
default geqSpec ∷ (TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, OrdLike fn (SimpleRep a)) ⇒ a → Specification fn a Source #
gtSpec ∷ a → Specification fn a Source #
default gtSpec ∷ (TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, OrdLike fn (SimpleRep a)) ⇒ a → Specification fn a Source #
Instances
(HasSpec fn a, MaybeBounded a, Num a, TypeSpec fn a ~ NumSpec a) ⇒ OrdLike fn a Source #  
Defined in Constrained.Base leqSpec ∷ a → Specification fn a Source # ltSpec ∷ a → Specification fn a Source # geqSpec ∷ a → Specification fn a Source # gtSpec ∷ a → Specification fn a Source # 
data ListFn fn args res where Source #
FoldMap ∷ (HasSpec fn a, Foldy fn b, Show (fn '[a] b), Eq (fn '[a] b)) ⇒ fn '[a] b → ListFn fn '[[a]] b 
Instances
FunctionLike fn ⇒ FunctionLike (ListFn fn) Source #  
BaseUniverse fn ⇒ Functions (ListFn fn) fn Source #  
Defined in Constrained.Base propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ ListFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ ListFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ ListFn fn '[a] b → TypeSpec fn a → Specification fn b Source #  
Show (ListFn fn args res) Source #  
Typeable fn ⇒ Eq (ListFn fn args res) Source #  
foldMapFn ∷ ∀ fn a b. (HasSpec fn a, Foldy fn b, Show (fn '[a] b), Eq (fn '[a] b)) ⇒ fn '[a] b → fn '[[a]] b Source #
data IntFn (fn ∷ [Type] → Type → Type) as b where Source #
Instances
FunctionLike (IntFn fn) Source #  
BaseUniverse fn ⇒ Functions (IntFn fn) fn Source #  
Defined in Constrained.Base propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ IntFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ IntFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ IntFn fn '[a] b → TypeSpec fn a → Specification fn b Source #  
Show (IntFn fn as b) Source #  
Eq (IntFn fn as b) Source #  
class (Num a, HasSpec fn a) ⇒ NumLike fn a where Source #
Nothing
subtractSpec ∷ a → TypeSpec fn a → Specification fn a Source #
default subtractSpec ∷ (TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, NumLike fn (SimpleRep a)) ⇒ a → TypeSpec fn a → Specification fn a Source #
negateSpec ∷ TypeSpec fn a → Specification fn a Source #
default negateSpec ∷ (TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, NumLike fn (SimpleRep a)) ⇒ TypeSpec fn a → Specification fn a Source #
safeSubtract ∷ a → a → Maybe a Source #
default safeSubtract ∷ (HasSimpleRep a, NumLike fn (SimpleRep a)) ⇒ a → a → Maybe a Source #
Instances
(HasSpec fn a, Ord a, Num a, TypeSpec fn a ~ NumSpec a, MaybeBounded a) ⇒ NumLike fn a Source #  
Defined in Constrained.Base subtractSpec ∷ a → TypeSpec fn a → Specification fn a Source # negateSpec ∷ TypeSpec fn a → Specification fn a Source # safeSubtract ∷ a → a → Maybe a Source # 
toGeneric_ ∷ ∀ a fn. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Term fn a → Term fn (SimpleRep a) Source #
fromGeneric_ ∷ ∀ a fn. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ Term fn (SimpleRep a) → Term fn a Source #
union_ ∷ ∀ a fn. (HasSpec fn a, Ord a) ⇒ Term fn (Set a) → Term fn (Set a) → Term fn (Set a) Source #
size_ ∷ ∀ a fn. (HasSpec fn (Set a), Ord a) ⇒ Term fn (Set a) → Term fn Integer Source #
special instance of sizeOf (for Sets) for backward compatibility
length_ ∷ ∀ a fn. HasSpec fn [a] ⇒ Term fn [a] → Term fn Integer Source #
special instance of sizeOf (for Lists) for backward compatibility
foldMap_ ∷ ∀ fn a b. (BaseUniverse fn, Foldy fn b, HasSpec fn a) ⇒ (Term fn a → Term fn b) → Term fn [a] → Term fn b Source #
constrained ∷ ∀ a fn p. (IsPred p fn, HasSpec fn a) ⇒ (Term fn a → p) → Specification fn a Source #
assertExplain ∷ (BaseUniverse fn, IsPred p fn) ⇒ NonEmpty String → p → Pred fn Source #
forAll ∷ (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) ⇒ Term fn t → (Term fn a → p) → Pred fn Source #
mkForAll ∷ (Forallable t a, HasSpec fn t, HasSpec fn a) ⇒ Term fn t → Binder fn a → Pred fn Source #