constrained-generators-0.2.0.0: Framework for generating constrained random data using a subset of first order logic
Safe HaskellSafe-Inferred
LanguageHaskell2010

Constrained.Base

Description

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

Documentation

data Term (fn ∷ [Type] → TypeType) a where Source #

Typed first order terms with function symbols from fn.

Constructors

App ∷ (Typeable as, TypeList as, All (HasSpec fn) as, HasSpec fn b, BaseUniverse fn) ⇒ fn as b → List (Term fn) as → Term fn b 
LitShow a ⇒ a → Term fn a 
VHasSpec fn a ⇒ Var a → Term fn a 

Instances

Instances details
HasVariables fn (Term fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsTerm fn a → FreeVars fn Source #

freeVarSetTerm fn a → Set (Name fn) Source #

countOfName fn → Term fn a → Int Source #

appearsInName fn → Term fn a → Bool Source #

HasVariables fn (List (Term fn) as) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsList (Term fn) as → FreeVars fn Source #

freeVarSetList (Term fn) as → Set (Name fn) Source #

countOfName fn → List (Term fn) as → Int Source #

appearsInName fn → List (Term fn) as → Bool Source #

HasSpec fn a ⇒ Pretty (WithPrec (Term fn a)) Source # 
Instance details

Defined in Constrained.Base

Methods

prettyWithPrec (Term fn a) → Doc ann Source #

prettyList ∷ [WithPrec (Term fn a)] → Doc ann Source #

(Ord a, HasSpec fn (Set a)) ⇒ Monoid (Term fn (Set a)) Source # 
Instance details

Defined in Constrained.Base

Methods

memptyTerm fn (Set a) Source #

mappendTerm fn (Set a) → Term fn (Set a) → Term fn (Set a) Source #

mconcat ∷ [Term fn (Set a)] → Term fn (Set a) Source #

(Ord a, HasSpec fn (Set a)) ⇒ Semigroup (Term fn (Set a)) Source # 
Instance details

Defined in Constrained.Base

Methods

(<>)Term fn (Set a) → Term fn (Set a) → Term fn (Set a) Source #

sconcatNonEmpty (Term fn (Set a)) → Term fn (Set a) Source #

stimesIntegral b ⇒ b → Term fn (Set a) → Term fn (Set a) Source #

NumLike fn a ⇒ Num (Term fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

(+)Term fn a → Term fn a → Term fn a Source #

(-)Term fn a → Term fn a → Term fn a Source #

(*)Term fn a → Term fn a → Term fn a Source #

negateTerm fn a → Term fn a Source #

absTerm fn a → Term fn a Source #

signumTerm fn a → Term fn a Source #

fromIntegerIntegerTerm fn a Source #

HasSpec fn a ⇒ Show (Term fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

showsPrecIntTerm fn a → ShowS Source #

showTerm fn a → String Source #

showList ∷ [Term fn a] → ShowS Source #

BaseUniverse fn ⇒ PredLike (Term fn Bool) Source # 
Instance details

Defined in Constrained.Base

Associated Types

type UnivConstr (Term fn Bool) fn Source #

Methods

toPredExplain ∷ ∀ (fn0 ∷ [Type] → TypeType). (BaseUniverse fn0, UnivConstr (Term fn Bool) fn0) ⇒ [String] → Term fn BoolPred fn0 Source #

Rename (Term fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

renameTypeable x ⇒ Var x → Var x → Term fn a → Term fn a Source #

HasSpec fn a ⇒ Eq (Term fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

(==)Term fn a → Term fn a → Bool Source #

(/=)Term fn a → Term fn a → Bool Source #

HasSpec fn a ⇒ Pretty (Term fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

prettyTerm fn a → Doc ann Source #

prettyList ∷ [Term fn a] → Doc ann Source #

type UnivConstr (Term fn Bool) fn' Source # 
Instance details

Defined in Constrained.Base

type UnivConstr (Term fn Bool) fn' = fn ~ fn'

type HasSpecImpliesEq fn a f = HasSpec fn a ⇒ Eq (f a) ∷ Constraint Source #

data Binder fn a where Source #

Constructors

(:->)HasSpec fn a ⇒ Var a → Pred fn → Binder fn a 

Instances

Instances details
HasVariables fn (Binder fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsBinder fn a → FreeVars fn Source #

freeVarSetBinder fn a → Set (Name fn) Source #

countOfName fn → Binder fn a → Int Source #

appearsInName fn → Binder fn a → Bool Source #

HasVariables fn (List (Weighted (Binder fn)) as) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsList (Weighted (Binder fn)) as → FreeVars fn Source #

freeVarSetList (Weighted (Binder fn)) as → Set (Name fn) Source #

countOfName fn → List (Weighted (Binder fn)) as → Int Source #

appearsInName fn → List (Weighted (Binder fn)) as → Bool Source #

Show (Binder fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

showsPrecIntBinder fn a → ShowS Source #

showBinder fn a → String Source #

showList ∷ [Binder fn a] → ShowS Source #

Rename (Binder fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

renameTypeable x ⇒ Var x → Var x → Binder fn a → Binder fn a Source #

Pretty (Binder fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

prettyBinder fn a → Doc ann Source #

prettyList ∷ [Binder fn a] → Doc ann Source #

data Pred (fn ∷ [Type] → TypeType) where Source #

Constructors

Monitor ∷ ((∀ a. Term fn a → a) → PropertyProperty) → Pred fn 
Block ∷ [Pred fn] → Pred fn 
Exists 

Fields

  • ∷ ((∀ b. Term fn b → b) → GE a)

    Constructive recovery function for checking existential quantification

  • Binder fn a
     
  • Pred fn
     
SubstHasSpec fn a ⇒ Var a → Term fn a → Pred fn → Pred fn 
LetTerm fn a → Binder fn a → Pred fn 
AssertBaseUniverse fn ⇒ NonEmpty StringTerm fn BoolPred fn 
Reifies 

Fields

  • ∷ (HasSpec fn a, HasSpec fn b)
     
  • Term fn b

    This depends on the a term

  • Term fn a
     
  • → (a → b)

    Recover a useable value from the a term.

  • 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 

Fields

WhenHasSpec fn BoolTerm fn BoolPred fn → Pred fn 
GenHintHasGenHint fn a ⇒ Hint a → Term fn a → Pred fn 
TruePredPred fn 
FalsePredNonEmpty StringPred fn 
ExplainNonEmpty StringPred fn → Pred fn 

Instances

Instances details
HasVariables fn (Pred fn) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsPred fn → FreeVars fn Source #

freeVarSetPred fn → Set (Name fn) Source #

countOfName fn → Pred fn → Int Source #

appearsInName fn → Pred fn → Bool Source #

BaseUniverse fn ⇒ Monoid (Pred fn) Source # 
Instance details

Defined in Constrained.Base

Methods

memptyPred fn Source #

mappendPred fn → Pred fn → Pred fn Source #

mconcat ∷ [Pred fn] → Pred fn Source #

BaseUniverse fn ⇒ Semigroup (Pred fn) Source # 
Instance details

Defined in Constrained.Base

Methods

(<>)Pred fn → Pred fn → Pred fn Source #

sconcatNonEmpty (Pred fn) → Pred fn Source #

stimesIntegral b ⇒ b → Pred fn → Pred fn Source #

Show (Pred fn) Source # 
Instance details

Defined in Constrained.Base

Methods

showsPrecIntPred fn → ShowS Source #

showPred fn → String Source #

showList ∷ [Pred fn] → ShowS Source #

PredLike (Pred fn) Source # 
Instance details

Defined in Constrained.Base

Associated Types

type UnivConstr (Pred fn) fn Source #

Methods

toPredExplain ∷ ∀ (fn0 ∷ [Type] → TypeType). (BaseUniverse fn0, UnivConstr (Pred fn) fn0) ⇒ [String] → Pred fn → Pred fn0 Source #

Rename (Pred fn) Source # 
Instance details

Defined in Constrained.Base

Methods

renameTypeable x ⇒ Var x → Var x → Pred fn → Pred fn Source #

Pretty (Pred fn) Source # 
Instance details

Defined in Constrained.Base

Methods

prettyPred fn → Doc ann Source #

prettyList ∷ [Pred fn] → Doc ann Source #

type UnivConstr (Pred fn) fn' Source # 
Instance details

Defined in Constrained.Base

type UnivConstr (Pred fn) fn' = fn ~ fn'

data Weighted f a Source #

Constructors

Weighted 

Fields

Instances

Instances details
HasVariables fn (f a) ⇒ HasVariables fn (Weighted f a) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsWeighted f a → FreeVars fn Source #

freeVarSetWeighted f a → Set (Name fn) Source #

countOfName fn → Weighted f a → Int Source #

appearsInName fn → Weighted f a → Bool Source #

HasVariables fn (List (Weighted (Binder fn)) as) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsList (Weighted (Binder fn)) as → FreeVars fn Source #

freeVarSetList (Weighted (Binder fn)) as → Set (Name fn) Source #

countOfName fn → List (Weighted (Binder fn)) as → Int Source #

appearsInName fn → List (Weighted (Binder fn)) as → Bool Source #

Foldable f ⇒ Foldable (Weighted f) Source # 
Instance details

Defined in Constrained.Base

Methods

foldMonoid m ⇒ Weighted f m → m Source #

foldMapMonoid m ⇒ (a → m) → Weighted f a → m Source #

foldMap'Monoid m ⇒ (a → m) → Weighted f a → m Source #

foldr ∷ (a → b → b) → b → Weighted f a → b Source #

foldr' ∷ (a → b → b) → b → Weighted f a → b Source #

foldl ∷ (b → a → b) → b → Weighted f a → b Source #

foldl' ∷ (b → a → b) → b → Weighted f a → b Source #

foldr1 ∷ (a → a → a) → Weighted f a → a Source #

foldl1 ∷ (a → a → a) → Weighted f a → a Source #

toListWeighted f a → [a] Source #

nullWeighted f a → Bool Source #

lengthWeighted f a → Int Source #

elemEq a ⇒ a → Weighted f a → Bool Source #

maximumOrd a ⇒ Weighted f a → a Source #

minimumOrd a ⇒ Weighted f a → a Source #

sumNum a ⇒ Weighted f a → a Source #

productNum a ⇒ Weighted f a → a Source #

Traversable f ⇒ Traversable (Weighted f) Source # 
Instance details

Defined in Constrained.Base

Methods

traverseApplicative f0 ⇒ (a → f0 b) → Weighted f a → f0 (Weighted f b) Source #

sequenceAApplicative f0 ⇒ Weighted f (f0 a) → f0 (Weighted f a) Source #

mapMMonad m ⇒ (a → m b) → Weighted f a → m (Weighted f b) Source #

sequenceMonad m ⇒ Weighted f (m a) → m (Weighted f a) Source #

Functor f ⇒ Functor (Weighted f) Source # 
Instance details

Defined in Constrained.Base

Methods

fmap ∷ (a → b) → Weighted f a → Weighted f b Source #

(<$) ∷ a → Weighted f b → Weighted f a Source #

Rename (f a) ⇒ Rename (Weighted f a) Source # 
Instance details

Defined in Constrained.Base

Methods

renameTypeable x ⇒ Var x → Var x → Weighted f a → Weighted f a Source #

Pretty (f a) ⇒ Pretty (Weighted f a) Source # 
Instance details

Defined in Constrained.Base

Methods

prettyWeighted f a → Doc ann Source #

prettyList ∷ [Weighted f a] → Doc ann Source #

mapWeighted ∷ (f a → g b) → Weighted f a → Weighted g b Source #

traverseWeightedApplicative m ⇒ (f a → m (g a)) → Weighted f a → m (Weighted g a) Source #

data Ctx (fn ∷ [Type] → TypeType) 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'`.

Constructors

CtxHOLEHasSpec fn v ⇒ Ctx fn v v

A single hole of type v

CtxApp ∷ (HasSpec fn b, TypeList as, Typeable as, All (HasSpec fn) as) ⇒ fn as b → ListCtx Value as (Ctx fn v) → Ctx fn v b

The application `f vs Ctx vs'`

data HOLE a b where Source #

This is used together with ListCtx to form just the arguments to `f vs Ctx vs'` - replacing Ctx with HOLE - to provide to propagateSpecFun.

Constructors

HOLEHOLE a a 

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 #

runTermMonadGenError m ⇒ EnvTerm fn a → m a 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) ⇒ EnvPred fn → m (PropertyProperty) Source #

checkPred ∷ ∀ fn m. (FunctionLike fn, MonadGenError m) ⇒ EnvPred fn → m Bool Source #

checkPreds ∷ (MonadGenError m, Traversable t, FunctionLike fn) ⇒ Env → t (Pred fn) → m Bool Source #

runCaseOnSumOver as → List (Binder fn) as → (∀ a. HasSpec fn a ⇒ Var a → a → Pred fn → r) → r Source #

type OrdSet a = [a] Source #

data Specification fn a where Source #

A `Specification fn a` denotes a set of as

Constructors

MemberSpec

Elements of a known set

Fields

ErrorSpecNonEmpty StringSpecification fn a

The empty set

SuspendedSpec

The set described by some predicates over the bound variable.

TODO: possibly we want to use a Binder here

Fields

  • HasSpec fn a
     
  • Var a

    This variable ranges over values denoted by the spec

  • Pred fn

    And the variable is subject to these constraints

  • Specification fn a
     
TypeSpec

A type-specific spec

Fields

TrueSpecSpecification fn a

Anything

Instances

Instances details
HasSpec fn a ⇒ Pretty (WithPrec (Specification fn a)) Source # 
Instance details

Defined in Constrained.Base

Methods

prettyWithPrec (Specification fn a) → Doc ann Source #

prettyList ∷ [WithPrec (Specification fn a)] → Doc ann Source #

(HasSpec fn a, Arbitrary (TypeSpec fn a)) ⇒ Arbitrary (Specification fn a) Source # 
Instance details

Defined in Constrained.Base

HasSpec fn a ⇒ Monoid (Specification fn a) Source # 
Instance details

Defined in Constrained.Base

HasSpec fn a ⇒ Semigroup (Specification fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

(<>)Specification fn a → Specification fn a → Specification fn a Source #

sconcatNonEmpty (Specification fn a) → Specification fn a Source #

stimesIntegral b ⇒ b → Specification fn a → Specification fn a Source #

HasSpec fn a ⇒ Show (Specification fn a) Source # 
Instance details

Defined in Constrained.Base

HasSpec fn a ⇒ Pretty (Specification fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

prettySpecification fn a → Doc ann Source #

prettyList ∷ [Specification fn a] → Doc ann Source #

shrinkPredPred fn → [Pred fn] 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 #

typeSpecHasSpec fn a ⇒ TypeSpec fn 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).

Minimal complete definition

Nothing

Associated Types

type TypeSpec (fn ∷ [Type] → TypeType) a Source #

The `TypeSpec fn a` is the type-specific `Specification fn a`.

type TypeSpec fn a = TypeSpec fn (SimpleRep a)

type Prerequisites fn a ∷ Constraint Source #

Prerequisites for the instance that are sometimes necessary when working with e.g. Specifications or functions in the universe.

type Prerequisites fn a = ()

Methods

emptySpecTypeSpec fn a Source #

default emptySpec ∷ (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) ⇒ TypeSpec fn a Source #

combineSpecTypeSpec 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 #

conformsToHasCallStack ⇒ 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 #

shrinkWithTypeSpecTypeSpec 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 #

toPredsTerm 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 #

cardinalTypeSpecTypeSpec 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 #

cardinalTrueSpecSpecification 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

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

prerequisitesEvidence (Prerequisites fn a) Source #

Materialize the Prerequisites dictionary. It should not be necessary to implement this function manually.

Instances

Instances details
BaseUniverse fn ⇒ HasSpec fn Int16 Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn Int16 Source #

type Prerequisites fn Int16 Source #

BaseUniverse fn ⇒ HasSpec fn Int32 Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn Int32 Source #

type Prerequisites fn Int32 Source #

BaseUniverse fn ⇒ HasSpec fn Int64 Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn Int64 Source #

type Prerequisites fn Int64 Source #

BaseUniverse fn ⇒ HasSpec fn Int8 Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn Int8 Source #

type Prerequisites fn Int8 Source #

BaseUniverse fn ⇒ HasSpec fn Word16 Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn Word16 Source #

type Prerequisites fn Word16 Source #

BaseUniverse fn ⇒ HasSpec fn Word32 Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn Word32 Source #

type Prerequisites fn Word32 Source #

BaseUniverse fn ⇒ HasSpec fn Word64 Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn Word64 Source #

type Prerequisites fn Word64 Source #

BaseUniverse fn ⇒ HasSpec fn Word8 Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn Word8 Source #

type Prerequisites fn Word8 Source #

BaseUniverse fn ⇒ HasSpec fn Foo Source # 
Instance details

Defined in Constrained.Examples.Basic

Associated Types

type TypeSpec fn Foo Source #

type Prerequisites fn Foo Source #

BaseUniverse fn ⇒ HasSpec fn Three Source # 
Instance details

Defined in Constrained.Examples.Basic

Associated Types

type TypeSpec fn Three Source #

type Prerequisites fn Three Source #

BaseUniverse fn ⇒ HasSpec fn Integer Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn Integer Source #

type Prerequisites fn Integer Source #

BaseUniverse fn ⇒ HasSpec fn Natural Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn Natural Source #

type Prerequisites fn Natural Source #

BaseUniverse fn ⇒ HasSpec fn () Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn () Source #

type Prerequisites fn () Source #

Methods

emptySpecTypeSpec fn () Source #

combineSpecTypeSpec fn () → TypeSpec fn () → Specification fn () Source #

genFromTypeSpec ∷ ∀ (m ∷ TypeType). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn () → GenT m () Source #

conformsTo ∷ () → TypeSpec fn () → Bool Source #

shrinkWithTypeSpecTypeSpec fn () → () → [()] Source #

toPredsTerm fn () → TypeSpec fn () → Pred fn Source #

cardinalTypeSpecTypeSpec fn () → Specification fn Integer Source #

cardinalTrueSpecSpecification fn Integer Source #

typeSpecOptTypeSpec fn () → [()] → Specification fn () Source #

prerequisitesEvidence (Prerequisites fn ()) Source #

(BaseUniverse fn, HasSpec fn ()) ⇒ HasSpec fn Bool Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn Bool Source #

type Prerequisites fn Bool Source #

BaseUniverse fn ⇒ HasSpec fn Float Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn Float Source #

type Prerequisites fn Float Source #

BaseUniverse fn ⇒ HasSpec fn Int Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn Int Source #

type Prerequisites fn Int Source #

BaseUniverse fn ⇒ HasSpec fn (Ratio Integer) Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn (Ratio Integer) Source #

type Prerequisites fn (Ratio Integer) Source #

(Ord a, HasSpec fn a) ⇒ HasSpec fn (NotASet a) Source # 
Instance details

Defined in Constrained.Examples.Set

Associated Types

type TypeSpec fn (NotASet a) Source #

type Prerequisites fn (NotASet a) Source #

HasSpec fn a ⇒ HasSpec fn (BinTree a) Source # 
Instance details

Defined in Constrained.Spec.Tree

Associated Types

type TypeSpec fn (BinTree a) Source #

type Prerequisites fn (BinTree a) Source #

(Ord a, HasSpec fn a) ⇒ HasSpec fn (Set a) Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn (Set a) Source #

type Prerequisites fn (Set a) Source #

(HasSpec fn a, Member (TreeFn fn) fn) ⇒ HasSpec fn (Tree a) Source # 
Instance details

Defined in Constrained.Spec.Tree

Associated Types

type TypeSpec fn (Tree a) Source #

type Prerequisites fn (Tree a) Source #

(IsNormalType a, HasSpec fn a) ⇒ HasSpec fn (Maybe a) Source # 
Instance details

Defined in Constrained.Spec.Generics

Associated Types

type TypeSpec fn (Maybe a) Source #

type Prerequisites fn (Maybe a) Source #

HasSpec fn a ⇒ HasSpec fn [a] Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn [a] Source #

type Prerequisites fn [a] Source #

Methods

emptySpecTypeSpec fn [a] Source #

combineSpecTypeSpec fn [a] → TypeSpec fn [a] → Specification fn [a] Source #

genFromTypeSpec ∷ ∀ (m ∷ TypeType). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn [a] → GenT m [a] Source #

conformsTo ∷ [a] → TypeSpec fn [a] → Bool Source #

shrinkWithTypeSpecTypeSpec fn [a] → [a] → [[a]] Source #

toPredsTerm fn [a] → TypeSpec fn [a] → Pred fn Source #

cardinalTypeSpecTypeSpec fn [a] → Specification fn Integer Source #

cardinalTrueSpecSpecification fn Integer Source #

typeSpecOptTypeSpec fn [a] → [[a]] → Specification fn [a] Source #

prerequisitesEvidence (Prerequisites fn [a]) Source #

(HasSpec fn a, IsNormalType a, HasSpec fn b, IsNormalType b) ⇒ HasSpec fn (Either a b) Source # 
Instance details

Defined in Constrained.Spec.Generics

Associated Types

type TypeSpec fn (Either a b) Source #

type Prerequisites fn (Either a b) Source #

(HasSpec fn a, HasSpec fn b) ⇒ HasSpec fn (Prod a b) Source # 
Instance details

Defined in Constrained.Spec.Pairs

Associated Types

type TypeSpec fn (Prod a b) Source #

type Prerequisites fn (Prod a b) Source #

Methods

emptySpecTypeSpec fn (Prod a b) Source #

combineSpecTypeSpec fn (Prod a b) → TypeSpec fn (Prod a b) → Specification fn (Prod a b) Source #

genFromTypeSpec ∷ ∀ (m ∷ TypeType). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (Prod a b) → GenT m (Prod a b) Source #

conformsToProd a b → TypeSpec fn (Prod a b) → Bool Source #

shrinkWithTypeSpecTypeSpec fn (Prod a b) → Prod a b → [Prod a b] Source #

toPredsTerm fn (Prod a b) → TypeSpec fn (Prod a b) → Pred fn Source #

cardinalTypeSpecTypeSpec fn (Prod a b) → Specification fn Integer Source #

cardinalTrueSpecSpecification fn Integer Source #

typeSpecOptTypeSpec fn (Prod a b) → [Prod a b] → Specification fn (Prod a b) Source #

prerequisitesEvidence (Prerequisites fn (Prod a b)) Source #

(HasSpec fn a, HasSpec fn b, KnownNat (CountCases b)) ⇒ HasSpec fn (Sum a b) Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn (Sum a b) Source #

type Prerequisites fn (Sum a b) Source #

Methods

emptySpecTypeSpec fn (Sum a b) Source #

combineSpecTypeSpec fn (Sum a b) → TypeSpec fn (Sum a b) → Specification fn (Sum a b) Source #

genFromTypeSpec ∷ ∀ (m ∷ TypeType). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (Sum a b) → GenT m (Sum a b) Source #

conformsToSum a b → TypeSpec fn (Sum a b) → Bool Source #

shrinkWithTypeSpecTypeSpec fn (Sum a b) → Sum a b → [Sum a b] Source #

toPredsTerm fn (Sum a b) → TypeSpec fn (Sum a b) → Pred fn Source #

cardinalTypeSpecTypeSpec fn (Sum a b) → Specification fn Integer Source #

cardinalTrueSpecSpecification fn Integer Source #

typeSpecOptTypeSpec fn (Sum a b) → [Sum a b] → Specification fn (Sum a b) Source #

prerequisitesEvidence (Prerequisites fn (Sum a b)) Source #

(Ord k, HasSpec fn (Prod k v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) ⇒ HasSpec fn (Map k v) Source # 
Instance details

Defined in Constrained.Spec.Map

Associated Types

type TypeSpec fn (Map k v) Source #

type Prerequisites fn (Map k v) Source #

Methods

emptySpecTypeSpec fn (Map k v) Source #

combineSpecTypeSpec fn (Map k v) → TypeSpec fn (Map k v) → Specification fn (Map k v) Source #

genFromTypeSpec ∷ ∀ (m ∷ TypeType). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (Map k v) → GenT m (Map k v) Source #

conformsToMap k v → TypeSpec fn (Map k v) → Bool Source #

shrinkWithTypeSpecTypeSpec fn (Map k v) → Map k v → [Map k v] Source #

toPredsTerm fn (Map k v) → TypeSpec fn (Map k v) → Pred fn Source #

cardinalTypeSpecTypeSpec fn (Map k v) → Specification fn Integer Source #

cardinalTrueSpecSpecification fn Integer Source #

typeSpecOptTypeSpec fn (Map k v) → [Map k v] → Specification fn (Map k v) Source #

prerequisitesEvidence (Prerequisites fn (Map k v)) Source #

(HasSpec fn a, HasSpec fn b) ⇒ HasSpec fn (a, b) Source # 
Instance details

Defined in Constrained.Spec.Generics

Associated Types

type TypeSpec fn (a, b) Source #

type Prerequisites fn (a, b) Source #

Methods

emptySpecTypeSpec fn (a, b) Source #

combineSpecTypeSpec fn (a, b) → TypeSpec fn (a, b) → Specification fn (a, b) Source #

genFromTypeSpec ∷ ∀ (m ∷ TypeType). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (a, b) → GenT m (a, b) Source #

conformsTo ∷ (a, b) → TypeSpec fn (a, b) → Bool Source #

shrinkWithTypeSpecTypeSpec fn (a, b) → (a, b) → [(a, b)] Source #

toPredsTerm fn (a, b) → TypeSpec fn (a, b) → Pred fn Source #

cardinalTypeSpecTypeSpec fn (a, b) → Specification fn Integer Source #

cardinalTrueSpecSpecification fn Integer Source #

typeSpecOptTypeSpec fn (a, b) → [(a, b)] → Specification fn (a, b) Source #

prerequisitesEvidence (Prerequisites fn (a, b)) Source #

(HasSpec fn a, HasSpec fn b, HasSpec fn c) ⇒ HasSpec fn (a, b, c) Source # 
Instance details

Defined in Constrained.Spec.Generics

Associated Types

type TypeSpec fn (a, b, c) Source #

type Prerequisites fn (a, b, c) Source #

Methods

emptySpecTypeSpec fn (a, b, c) Source #

combineSpecTypeSpec fn (a, b, c) → TypeSpec fn (a, b, c) → Specification fn (a, b, c) Source #

genFromTypeSpec ∷ ∀ (m ∷ TypeType). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (a, b, c) → GenT m (a, b, c) Source #

conformsTo ∷ (a, b, c) → TypeSpec fn (a, b, c) → Bool Source #

shrinkWithTypeSpecTypeSpec fn (a, b, c) → (a, b, c) → [(a, b, c)] Source #

toPredsTerm fn (a, b, c) → TypeSpec fn (a, b, c) → Pred fn Source #

cardinalTypeSpecTypeSpec fn (a, b, c) → Specification fn Integer Source #

cardinalTrueSpecSpecification fn Integer Source #

typeSpecOptTypeSpec fn (a, b, c) → [(a, b, c)] → Specification fn (a, b, c) Source #

prerequisitesEvidence (Prerequisites fn (a, b, c)) Source #

(HasSpec fn a, HasSpec fn b, HasSpec fn c, HasSpec fn d) ⇒ HasSpec fn (a, b, c, d) Source # 
Instance details

Defined in Constrained.Spec.Generics

Associated Types

type TypeSpec fn (a, b, c, d) Source #

type Prerequisites fn (a, b, c, d) Source #

Methods

emptySpecTypeSpec fn (a, b, c, d) Source #

combineSpecTypeSpec fn (a, b, c, d) → TypeSpec fn (a, b, c, d) → Specification fn (a, b, c, d) Source #

genFromTypeSpec ∷ ∀ (m ∷ TypeType). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (a, b, c, d) → GenT m (a, b, c, d) Source #

conformsTo ∷ (a, b, c, d) → TypeSpec fn (a, b, c, d) → Bool Source #

shrinkWithTypeSpecTypeSpec fn (a, b, c, d) → (a, b, c, d) → [(a, b, c, d)] Source #

toPredsTerm fn (a, b, c, d) → TypeSpec fn (a, b, c, d) → Pred fn Source #

cardinalTypeSpecTypeSpec fn (a, b, c, d) → Specification fn Integer Source #

cardinalTrueSpecSpecification fn Integer Source #

typeSpecOptTypeSpec fn (a, b, c, d) → [(a, b, c, d)] → Specification fn (a, b, c, d) Source #

prerequisitesEvidence (Prerequisites fn (a, b, c, d)) Source #

(HasSpec fn a, HasSpec fn b, HasSpec fn c, HasSpec fn d, HasSpec fn e) ⇒ HasSpec fn (a, b, c, d, e) Source # 
Instance details

Defined in Constrained.Spec.Generics

Associated Types

type TypeSpec fn (a, b, c, d, e) Source #

type Prerequisites fn (a, b, c, d, e) Source #

Methods

emptySpecTypeSpec fn (a, b, c, d, e) Source #

combineSpecTypeSpec fn (a, b, c, d, e) → TypeSpec fn (a, b, c, d, e) → Specification fn (a, b, c, d, e) Source #

genFromTypeSpec ∷ ∀ (m ∷ TypeType). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (a, b, c, d, e) → GenT m (a, b, c, d, e) Source #

conformsTo ∷ (a, b, c, d, e) → TypeSpec fn (a, b, c, d, e) → Bool Source #

shrinkWithTypeSpecTypeSpec fn (a, b, c, d, e) → (a, b, c, d, e) → [(a, b, c, d, e)] Source #

toPredsTerm fn (a, b, c, d, e) → TypeSpec fn (a, b, c, d, e) → Pred fn Source #

cardinalTypeSpecTypeSpec fn (a, b, c, d, e) → Specification fn Integer Source #

cardinalTrueSpecSpecification fn Integer Source #

typeSpecOptTypeSpec fn (a, b, c, d, e) → [(a, b, c, d, e)] → Specification fn (a, b, c, d, e) Source #

prerequisitesEvidence (Prerequisites fn (a, b, c, d, e)) Source #

(HasSpec fn a, HasSpec fn b, HasSpec fn c, HasSpec fn d, HasSpec fn e, HasSpec fn g) ⇒ HasSpec fn (a, b, c, d, e, g) Source # 
Instance details

Defined in Constrained.Spec.Generics

Associated Types

type TypeSpec fn (a, b, c, d, e, g) Source #

type Prerequisites fn (a, b, c, d, e, g) Source #

Methods

emptySpecTypeSpec fn (a, b, c, d, e, g) Source #

combineSpecTypeSpec fn (a, b, c, d, e, g) → TypeSpec fn (a, b, c, d, e, g) → Specification fn (a, b, c, d, e, g) Source #

genFromTypeSpec ∷ ∀ (m ∷ TypeType). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (a, b, c, d, e, g) → GenT m (a, b, c, d, e, g) Source #

conformsTo ∷ (a, b, c, d, e, g) → TypeSpec fn (a, b, c, d, e, g) → Bool Source #

shrinkWithTypeSpecTypeSpec fn (a, b, c, d, e, g) → (a, b, c, d, e, g) → [(a, b, c, d, e, g)] Source #

toPredsTerm fn (a, b, c, d, e, g) → TypeSpec fn (a, b, c, d, e, g) → Pred fn Source #

cardinalTypeSpecTypeSpec fn (a, b, c, d, e, g) → Specification fn Integer Source #

cardinalTrueSpecSpecification fn Integer Source #

typeSpecOptTypeSpec fn (a, b, c, d, e, g) → [(a, b, c, d, e, g)] → Specification fn (a, b, c, d, e, g) Source #

prerequisitesEvidence (Prerequisites fn (a, b, c, d, e, g)) Source #

(HasSpec fn a, HasSpec fn b, HasSpec fn c, HasSpec fn d, HasSpec fn e, HasSpec fn g, HasSpec fn h) ⇒ HasSpec fn (a, b, c, d, e, g, h) Source # 
Instance details

Defined in Constrained.Spec.Generics

Associated Types

type TypeSpec fn (a, b, c, d, e, g, h) Source #

type Prerequisites fn (a, b, c, d, e, g, h) Source #

Methods

emptySpecTypeSpec fn (a, b, c, d, e, g, h) Source #

combineSpecTypeSpec fn (a, b, c, d, e, g, h) → TypeSpec fn (a, b, c, d, e, g, h) → Specification fn (a, b, c, d, e, g, h) Source #

genFromTypeSpec ∷ ∀ (m ∷ TypeType). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (a, b, c, d, e, g, h) → GenT m (a, b, c, d, e, g, h) Source #

conformsTo ∷ (a, b, c, d, e, g, h) → TypeSpec fn (a, b, c, d, e, g, h) → Bool Source #

shrinkWithTypeSpecTypeSpec fn (a, b, c, d, e, g, h) → (a, b, c, d, e, g, h) → [(a, b, c, d, e, g, h)] Source #

toPredsTerm fn (a, b, c, d, e, g, h) → TypeSpec fn (a, b, c, d, e, g, h) → Pred fn Source #

cardinalTypeSpecTypeSpec fn (a, b, c, d, e, g, h) → Specification fn Integer Source #

cardinalTrueSpecSpecification fn Integer Source #

typeSpecOptTypeSpec fn (a, b, c, d, e, g, h) → [(a, b, c, d, e, g, h)] → Specification fn (a, b, c, d, e, g, h) Source #

prerequisitesEvidence (Prerequisites fn (a, b, c, d, e, g, h)) Source #

data WithHasSpec fn f a where Source #

Constructors

WithHasSpecHasSpec fn a ⇒ f a → WithHasSpec fn f a 

Instances

Instances details
HasSpecImpliesEq fn a f ⇒ Eq (WithHasSpec fn f a) Source # 
Instance details

Defined in Constrained.Base

Methods

(==)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 #

Minimal complete definition

Nothing

Methods

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

Instances details
Ord a ⇒ Forallable (NotASet a) a Source # 
Instance details

Defined in Constrained.Examples.Set

Methods

fromForAllSpec ∷ ∀ (fn ∷ [Type] → TypeType). (HasSpec fn (NotASet a), HasSpec fn a, BaseUniverse fn) ⇒ Specification fn a → Specification fn (NotASet a) Source #

forAllToListNotASet a → [a] Source #

Ord a ⇒ Forallable (Set a) a Source # 
Instance details

Defined in Constrained.Base

Methods

fromForAllSpec ∷ ∀ (fn ∷ [Type] → TypeType). (HasSpec fn (Set a), HasSpec fn a, BaseUniverse fn) ⇒ Specification fn a → Specification fn (Set a) Source #

forAllToListSet a → [a] Source #

Forallable [a] a Source # 
Instance details

Defined in Constrained.Base

Methods

fromForAllSpec ∷ ∀ (fn ∷ [Type] → TypeType). (HasSpec fn [a], HasSpec fn a, BaseUniverse fn) ⇒ Specification fn a → Specification fn [a] Source #

forAllToList ∷ [a] → [a] Source #

Forallable (Tree a) (a, [Tree a]) Source # 
Instance details

Defined in Constrained.Spec.Tree

Methods

fromForAllSpec ∷ ∀ (fn ∷ [Type] → TypeType). (HasSpec fn (Tree a), HasSpec fn (a, [Tree a]), BaseUniverse fn) ⇒ Specification fn (a, [Tree a]) → Specification fn (Tree a) Source #

forAllToListTree a → [(a, [Tree a])] Source #

Forallable (BinTree a) (BinTree a, a, BinTree a) Source # 
Instance details

Defined in Constrained.Spec.Tree

Methods

fromForAllSpec ∷ ∀ (fn ∷ [Type] → TypeType). (HasSpec fn (BinTree a), HasSpec fn (BinTree a, a, BinTree a), BaseUniverse fn) ⇒ Specification fn (BinTree a, a, BinTree a) → Specification fn (BinTree a) Source #

forAllToListBinTree a → [(BinTree a, a, BinTree a)] Source #

Ord k ⇒ Forallable (Map k v) (k, v) Source # 
Instance details

Defined in Constrained.Spec.Map

Methods

fromForAllSpec ∷ ∀ (fn ∷ [Type] → TypeType). (HasSpec fn (Map k v), HasSpec fn (k, v), BaseUniverse fn) ⇒ Specification fn (k, v) → Specification fn (Map k v) Source #

forAllToListMap k v → [(k, v)] Source #

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.

Associated Types

type Hint a Source #

Methods

giveHintHint a → Specification fn a Source #

Instances

Instances details
HasSpec fn a ⇒ HasGenHint fn (BinTree a) Source # 
Instance details

Defined in Constrained.Spec.Tree

Associated Types

type Hint (BinTree a) Source #

Methods

giveHintHint (BinTree a) → Specification fn (BinTree a) Source #

(Member (TreeFn fn) fn, HasSpec fn a) ⇒ HasGenHint fn (Tree a) Source # 
Instance details

Defined in Constrained.Spec.Tree

Associated Types

type Hint (Tree a) Source #

Methods

giveHintHint (Tree a) → Specification fn (Tree a) Source #

HasSpec fn a ⇒ HasGenHint fn [a] Source # 
Instance details

Defined in Constrained.Base

Associated Types

type Hint [a] Source #

Methods

giveHintHint [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 # 
Instance details

Defined in Constrained.Spec.Map

Associated Types

type Hint (Map k v) Source #

Methods

giveHintHint (Map k v) → Specification 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 #

satisfies ∷ ∀ fn a. HasSpec fn a ⇒ Term fn a → Specification fn a → Pred fn 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) ⇒ IntIntSpecification 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 #

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

data SolverStage fn where Source #

Constructors

SolverStage 

Fields

Instances

Instances details
Pretty (SolverStage fn) Source # 
Instance details

Defined in Constrained.Base

Methods

prettySolverStage fn → Doc ann Source #

prettyList ∷ [SolverStage fn] → Doc ann Source #

data SolverPlan fn Source #

Constructors

SolverPlan 

Instances

Instances details
Pretty (SolverPlan fn) Source # 
Instance details

Defined in Constrained.Base

Methods

prettySolverPlan fn → Doc ann Source #

prettyList ∷ [SolverPlan 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.

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

pattern Eql ∷ ∀ fn. () ⇒ ∀ a. HasSpec fn a ⇒ Term fn a → Term fn a → Term fn Bool Source #

prettyPlanHasSpec fn a ⇒ Specification fn a → Doc ann Source #

printPlanHasSpec fn a ⇒ Specification fn a → IO () Source #

genFromPreds ∷ (MonadGenError m, BaseUniverse fn) ⇒ Pred fn → 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`.

computeHints ∷ ∀ fn. [Pred fn] → Hints fn Source #

linearize ∷ (MonadGenError m, BaseUniverse fn) ⇒ [Pred fn] → DependGraph fn → m [SolverStage fn] Source #

regularizeHasVariables fn t ⇒ Var a → t → Var 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.

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 #

ctxHasSpecCtx fn v a → Evidence (HasSpec fn a) Source #

class (∀ as b. Show (f as b), ∀ as b. Eq (f as b), Typeable f, FunctionLike f) ⇒ Functions f fn where Source #

Minimal complete definition

propagateSpecFun, mapTypeSpec

Methods

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

Instances details
(BaseUniverse fn, Member (FunFn fn) fn) ⇒ Functions (FunFn fn) fn Source # 
Instance details

Defined in Constrained.Base

Methods

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 #

BaseUniverse fn ⇒ Functions (GenericsFn fn) fn Source # 
Instance details

Defined in Constrained.Spec.Generics

Methods

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 #

BaseUniverse fn ⇒ Functions (IntFn fn) fn Source # 
Instance details

Defined in Constrained.Base

Methods

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 #

BaseUniverse fn ⇒ Functions (ListFn fn) fn Source # 
Instance details

Defined in Constrained.Base

Methods

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 #

BaseUniverse fn ⇒ Functions (OrdFn fn) fn Source # 
Instance details

Defined in Constrained.Base

Methods

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 #

(BaseUniverse fn, HasSpec fn Integer) ⇒ Functions (SizeFn fn) fn Source # 
Instance details

Defined in Constrained.Base

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ SizeFn 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) ⇒ SizeFn fn as b → List (Term fn) as → Maybe (Term fn b) Source #

mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ SizeFn fn '[a] b → TypeSpec fn a → Specification fn b Source #

(Member (TreeFn fn) fn, BaseUniverse fn) ⇒ Functions (TreeFn fn) fn Source # 
Instance details

Defined in Constrained.Spec.Tree

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ TreeFn 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) ⇒ TreeFn fn as b → List (Term fn) as → Maybe (Term fn b) Source #

mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ TreeFn fn '[a] b → TypeSpec fn a → Specification fn b Source #

BaseUniverse fn ⇒ Functions (BoolFn fn) fn Source # 
Instance details

Defined in Constrained.Instances

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ BoolFn 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) ⇒ BoolFn fn as b → List (Term fn) as → Maybe (Term fn b) Source #

mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ BoolFn fn '[a] b → TypeSpec fn a → Specification fn b Source #

BaseUniverse fn ⇒ Functions (EqFn fn) fn Source # 
Instance details

Defined in Constrained.Instances

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ EqFn 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) ⇒ EqFn fn as b → List (Term fn) as → Maybe (Term fn b) Source #

mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ EqFn fn '[a] b → TypeSpec fn a → Specification fn b Source #

BaseUniverse fn ⇒ Functions (MapFn fn) fn Source # 
Instance details

Defined in Constrained.Spec.Map

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ MapFn 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) ⇒ MapFn fn as b → List (Term fn) as → Maybe (Term fn b) Source #

mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ MapFn fn '[a] b → TypeSpec fn a → Specification fn b Source #

BaseUniverse fn ⇒ Functions (PairFn fn) fn Source # 
Instance details

Defined in Constrained.Spec.Pairs

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ PairFn 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) ⇒ PairFn fn as b → List (Term fn) as → Maybe (Term fn b) Source #

mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ PairFn fn '[a] b → TypeSpec fn a → Specification fn b Source #

BaseUniverse fn ⇒ Functions (SetFn fn) fn Source # 
Instance details

Defined in Constrained.Base

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ SetFn 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) ⇒ SetFn fn as b → List (Term fn) as → Maybe (Term fn b) Source #

mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ SetFn fn '[a] b → TypeSpec fn a → Specification fn b Source #

BaseUniverse fn ⇒ Functions (SumFn fn) fn Source # 
Instance details

Defined in Constrained.Spec.Generics

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ SumFn 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) ⇒ SumFn fn as b → List (Term fn) as → Maybe (Term fn b) Source #

mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ SumFn fn '[a] b → TypeSpec fn a → Specification fn b Source #

(Typeable fn, Functions (fn (Fix fn)) (Fix fn)) ⇒ Functions (Fix fn) (Fix fn) Source # 
Instance details

Defined in Constrained.Instances

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec (Fix fn) a, HasSpec (Fix fn) b, All (HasSpec (Fix fn)) as) ⇒ Fix fn as b → ListCtx Value as (HOLE a) → Specification (Fix fn) b → Specification (Fix fn) a Source #

rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec (Fix fn) b, All (HasSpec (Fix fn)) as) ⇒ Fix fn as b → List (Term (Fix fn)) as → Maybe (Term (Fix fn) b) Source #

mapTypeSpec ∷ (HasSpec (Fix fn) a, HasSpec (Fix fn) b) ⇒ Fix fn '[a] b → TypeSpec (Fix fn) a → Specification (Fix fn) b Source #

(Typeable fn, Typeable fn', Typeable fnU, Functions (fn fnU) fnU, Functions (fn' fnU) fnU) ⇒ Functions (Oneof fn fn' fnU) fnU Source # 
Instance details

Defined in Constrained.Instances

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fnU a, HasSpec fnU b, All (HasSpec fnU) as) ⇒ Oneof fn fn' fnU as b → ListCtx Value as (HOLE a) → Specification fnU b → Specification fnU a Source #

rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fnU b, All (HasSpec fnU) as) ⇒ Oneof fn fn' fnU as b → List (Term fnU) as → Maybe (Term fnU b) Source #

mapTypeSpec ∷ (HasSpec fnU a, HasSpec fnU b) ⇒ Oneof fn fn' fnU '[a] b → TypeSpec fnU a → Specification fnU b Source #

mapSpec ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ fn '[a] b → Specification fn a → Specification fn b Source #

caseBoolSpecHasSpec fn a ⇒ Specification fn Bool → (BoolSpecification fn a) → Specification fn a Source #

If the `Specification fn Bool` doesn't constrain the boolean you will get a TrueSpec out.

type DependGraph fn = Graph (Name fn) Source #

dependencyHasVariables fn t ⇒ Name fn → t → DependGraph fn Source #

irreflexiveDependencyOn ∷ ∀ fn t t'. (HasVariables fn t, HasVariables fn t') ⇒ t → t' → DependGraph fn Source #

type Hints fn = DependGraph fn Source #

solvableFromName f → Set (Name f) → DependGraph f → Bool Source #

freeVarNames ∷ ∀ fn t. HasVariables fn t ⇒ t → Set Int Source #

data Name fn where Source #

Constructors

NameHasSpec fn a ⇒ Var a → Name fn 

Instances

Instances details
HasVariables f (Name f) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsName f → FreeVars f Source #

freeVarSetName f → Set (Name f) Source #

countOfName f → Name f → Int Source #

appearsInName f → Name f → Bool Source #

Show (Name fn) Source # 
Instance details

Defined in Constrained.Base

Methods

showsPrecIntName fn → ShowS Source #

showName fn → String Source #

showList ∷ [Name fn] → ShowS Source #

Rename (Name f) Source # 
Instance details

Defined in Constrained.Base

Methods

renameTypeable x ⇒ Var x → Var x → Name f → Name f Source #

Eq (Name fn) Source # 
Instance details

Defined in Constrained.Base

Methods

(==)Name fn → Name fn → Bool Source #

(/=)Name fn → Name fn → Bool Source #

Ord (Name fn) Source # 
Instance details

Defined in Constrained.Base

Methods

compareName fn → Name fn → Ordering Source #

(<)Name fn → Name fn → Bool Source #

(<=)Name fn → Name fn → Bool Source #

(>)Name fn → Name fn → Bool Source #

(>=)Name fn → Name fn → Bool Source #

maxName fn → Name fn → Name fn Source #

minName fn → Name fn → Name fn Source #

Pretty (Name fn) Source # 
Instance details

Defined in Constrained.Base

Methods

prettyName fn → Doc ann Source #

prettyList ∷ [Name fn] → Doc ann Source #

newtype FreeVars fn Source #

Constructors

FreeVars 

Fields

Instances

Instances details
Monoid (FreeVars fn) Source # 
Instance details

Defined in Constrained.Base

Methods

memptyFreeVars fn Source #

mappendFreeVars fn → FreeVars fn → FreeVars fn Source #

mconcat ∷ [FreeVars fn] → FreeVars fn Source #

Semigroup (FreeVars fn) Source # 
Instance details

Defined in Constrained.Base

Methods

(<>)FreeVars fn → FreeVars fn → FreeVars fn Source #

sconcatNonEmpty (FreeVars fn) → FreeVars fn Source #

stimesIntegral b ⇒ b → FreeVars fn → FreeVars fn Source #

Show (FreeVars fn) Source # 
Instance details

Defined in Constrained.Base

Methods

showsPrecIntFreeVars fn → ShowS Source #

showFreeVars fn → String Source #

showList ∷ [FreeVars fn] → ShowS Source #

restrictedToFreeVars fn → Set (Name fn) → FreeVars fn Source #

memberOfName fn → FreeVars fn → Bool Source #

countName fn → FreeVars fn → Int Source #

freeVarName fn → FreeVars fn Source #

singletonName fn → IntFreeVars fn Source #

withoutFoldable t ⇒ FreeVars fn → t (Name fn) → FreeVars fn Source #

class HasVariables fn a | a → fn where Source #

Minimal complete definition

freeVars

Methods

freeVars ∷ a → FreeVars fn Source #

freeVarSet ∷ a → Set (Name fn) Source #

countOfName fn → a → Int Source #

appearsInName fn → a → Bool Source #

Instances

Instances details
HasVariables f (Name f) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsName f → FreeVars f Source #

freeVarSetName f → Set (Name f) Source #

countOfName f → Name f → Int Source #

appearsInName f → Name f → Bool Source #

HasVariables f a ⇒ HasVariables f (Set a) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsSet a → FreeVars f Source #

freeVarSetSet a → Set (Name f) Source #

countOfName f → Set a → Int Source #

appearsInName f → Set a → Bool Source #

(Foldable t, HasVariables f a) ⇒ HasVariables f (t a) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVars ∷ t a → FreeVars f Source #

freeVarSet ∷ t a → Set (Name f) Source #

countOfName f → t a → Int Source #

appearsInName f → t a → Bool Source #

HasVariables fn (Pred fn) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsPred fn → FreeVars fn Source #

freeVarSetPred fn → Set (Name fn) Source #

countOfName fn → Pred fn → Int Source #

appearsInName fn → Pred fn → Bool Source #

(HasVariables f a, HasVariables f b) ⇒ HasVariables f (a, b) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVars ∷ (a, b) → FreeVars f Source #

freeVarSet ∷ (a, b) → Set (Name f) Source #

countOfName f → (a, b) → Int Source #

appearsInName f → (a, b) → Bool Source #

HasVariables fn (Binder fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsBinder fn a → FreeVars fn Source #

freeVarSetBinder fn a → Set (Name fn) Source #

countOfName fn → Binder fn a → Int Source #

appearsInName fn → Binder fn a → Bool Source #

HasVariables fn (Term fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsTerm fn a → FreeVars fn Source #

freeVarSetTerm fn a → Set (Name fn) Source #

countOfName fn → Term fn a → Int Source #

appearsInName fn → Term fn a → Bool Source #

HasVariables fn (f a) ⇒ HasVariables fn (Weighted f a) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsWeighted f a → FreeVars fn Source #

freeVarSetWeighted f a → Set (Name fn) Source #

countOfName fn → Weighted f a → Int Source #

appearsInName fn → Weighted f a → Bool Source #

HasVariables fn (List (Term fn) as) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsList (Term fn) as → FreeVars fn Source #

freeVarSetList (Term fn) as → Set (Name fn) Source #

countOfName fn → List (Term fn) as → Int Source #

appearsInName fn → List (Term fn) as → Bool Source #

HasVariables fn (List (Weighted (Binder fn)) as) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsList (Weighted (Binder fn)) as → FreeVars fn Source #

freeVarSetList (Weighted (Binder fn)) as → Set (Name fn) Source #

countOfName fn → List (Weighted (Binder fn)) as → Int Source #

appearsInName fn → List (Weighted (Binder fn)) as → Bool Source #

type Subst fn = [SubstEntry fn] Source #

data SubstEntry fn where Source #

Constructors

(:=)HasSpec fn a ⇒ Var a → Term fn a → SubstEntry fn 

backwardsSubstitution ∷ ∀ fn a. HasSpec fn a ⇒ Subst fn → Term fn a → Term fn a Source #

fastInequalityTerm fn a → Term fn b → Bool Source #

Sound but not complete inequality on terms

substituteTerm ∷ ∀ fn a. Subst fn → Term fn a → Term fn a Source #

substituteTerm' ∷ ∀ fn a. Subst fn → Term fn a → Writer Any (Term fn a) Source #

substituteBinderHasSpec fn a ⇒ Var a → Term fn a → Binder fn b → Binder fn b Source #

substitutePredHasSpec fn a ⇒ Var a → Term fn a → Pred fn → Pred fn Source #

substTermEnvTerm fn a → Term fn a Source #

substBinderEnvBinder fn a → Binder fn a Source #

substPredBaseUniverse fn ⇒ EnvPred fn → Pred fn Source #

unBind ∷ a → Binder fn a → Pred fn Source #

simplifyTerm ∷ ∀ fn a. BaseUniverse fn ⇒ Term fn a → Term fn a Source #

fromLitsList (Term fn) as → Maybe (List Value as) Source #

fromLitTerm fn a → Maybe (Value a) Source #

isLitTerm fn a → Bool Source #

simplifyPred ∷ ∀ fn. BaseUniverse fn ⇒ Pred fn → Pred fn Source #

simplifyPredsBaseUniverse fn ⇒ [Pred fn] → [Pred fn] Source #

simplifyBinderBinder 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!

optimisePredBaseUniverse fn ⇒ Pred fn → Pred fn Source #

letFloatingBaseUniverse fn ⇒ Pred fn → Pred fn Source #

substituteAndSimplifyTermBaseUniverse 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 #

Minimal complete definition

Nothing

Associated Types

type SimpleRep a Source #

type SimpleRep a = SOP (TheSop a)

type TheSop a ∷ [Type] Source #

type TheSop a = SOPOf (Rep a)

Methods

toSimpleRep ∷ a → SimpleRep a Source #

default toSimpleRep ∷ (Generic a, SimpleGeneric (Rep a), SimpleRep a ~ SimplifyRep (Rep a)) ⇒ a → SimpleRep a Source #

fromSimpleRepSimpleRep a → a Source #

default fromSimpleRep ∷ (Generic a, SimpleGeneric (Rep a), SimpleRep a ~ SimplifyRep (Rep a)) ⇒ SimpleRep a → a Source #

Instances

Instances details
HasSimpleRep Foo Source # 
Instance details

Defined in Constrained.Examples.Basic

Associated Types

type SimpleRep Foo Source #

type TheSop Foo ∷ [Type] Source #

HasSimpleRep Three Source # 
Instance details

Defined in Constrained.Examples.Basic

Associated Types

type SimpleRep Three Source #

type TheSop Three ∷ [Type] Source #

HasSimpleRep Bool Source # 
Instance details

Defined in Constrained.Base

Associated Types

type SimpleRep Bool Source #

type TheSop Bool ∷ [Type] Source #

Ord a ⇒ HasSimpleRep (NotASet a) Source # 
Instance details

Defined in Constrained.Examples.Set

Associated Types

type SimpleRep (NotASet a) Source #

type TheSop (NotASet a) ∷ [Type] Source #

HasSimpleRep (Maybe a) Source # 
Instance details

Defined in Constrained.Spec.Generics

Associated Types

type SimpleRep (Maybe a) Source #

type TheSop (Maybe a) ∷ [Type] Source #

HasSimpleRep (Either a b) Source # 
Instance details

Defined in Constrained.Spec.Generics

Associated Types

type SimpleRep (Either a b) Source #

type TheSop (Either a b) ∷ [Type] Source #

HasSimpleRep (a, b) Source # 
Instance details

Defined in Constrained.Spec.Generics

Associated Types

type SimpleRep (a, b) Source #

type TheSop (a, b) ∷ [Type] Source #

Methods

toSimpleRep ∷ (a, b) → SimpleRep (a, b) Source #

fromSimpleRepSimpleRep (a, b) → (a, b) Source #

HasSimpleRep (a, b, c) Source # 
Instance details

Defined in Constrained.Spec.Generics

Associated Types

type SimpleRep (a, b, c) Source #

type TheSop (a, b, c) ∷ [Type] Source #

Methods

toSimpleRep ∷ (a, b, c) → SimpleRep (a, b, c) Source #

fromSimpleRepSimpleRep (a, b, c) → (a, b, c) Source #

HasSimpleRep (a, b, c, d) Source # 
Instance details

Defined in Constrained.Spec.Generics

Associated Types

type SimpleRep (a, b, c, d) Source #

type TheSop (a, b, c, d) ∷ [Type] Source #

Methods

toSimpleRep ∷ (a, b, c, d) → SimpleRep (a, b, c, d) Source #

fromSimpleRepSimpleRep (a, b, c, d) → (a, b, c, d) Source #

HasSimpleRep (a, b, c, d, e) Source # 
Instance details

Defined in Constrained.Spec.Generics

Associated Types

type SimpleRep (a, b, c, d, e) Source #

type TheSop (a, b, c, d, e) ∷ [Type] Source #

Methods

toSimpleRep ∷ (a, b, c, d, e) → SimpleRep (a, b, c, d, e) Source #

fromSimpleRepSimpleRep (a, b, c, d, e) → (a, b, c, d, e) Source #

HasSimpleRep (a, b, c, d, e, g) Source # 
Instance details

Defined in Constrained.Spec.Generics

Associated Types

type SimpleRep (a, b, c, d, e, g) Source #

type TheSop (a, b, c, d, e, g) ∷ [Type] Source #

Methods

toSimpleRep ∷ (a, b, c, d, e, g) → SimpleRep (a, b, c, d, e, g) Source #

fromSimpleRepSimpleRep (a, b, c, d, e, g) → (a, b, c, d, e, g) Source #

HasSimpleRep (a, b, c, d, e, g, h) Source # 
Instance details

Defined in Constrained.Spec.Generics

Associated Types

type SimpleRep (a, b, c, d, e, g, h) Source #

type TheSop (a, b, c, d, e, g, h) ∷ [Type] Source #

Methods

toSimpleRep ∷ (a, b, c, d, e, g, h) → SimpleRep (a, b, c, d, e, g, h) Source #

fromSimpleRepSimpleRep (a, b, c, d, e, g, h) → (a, b, c, d, e, g, h) Source #

type family SimplifyRep f where ... Source #

Equations

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 #

Constructors

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

Instances details
FunctionLike (GenericsFn fn) Source # 
Instance details

Defined in Constrained.Spec.Generics

Methods

sem ∷ ∀ (as ∷ [Type]) b. GenericsFn fn as b → FunTy as b Source #

BaseUniverse fn ⇒ Functions (GenericsFn fn) fn Source # 
Instance details

Defined in Constrained.Spec.Generics

Methods

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 # 
Instance details

Defined in Constrained.Base

Methods

showsPrecIntGenericsFn fn as b → ShowS Source #

showGenericsFn fn as b → String Source #

showList ∷ [GenericsFn fn as b] → ShowS Source #

Eq (GenericsFn fn args res) Source # 
Instance details

Defined in Constrained.Base

Methods

(==)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

Instances details
TypeList prod ⇒ Inject c ((c ::: prod) ': (prod' ': constrs)) r Source # 
Instance details

Defined in Constrained.Base

Methods

inject' ∷ (SOP ((c ::: prod) ': (prod' ': constrs)) → r) → FunTy (ConstrOf c ((c ::: prod) ': (prod' ': constrs))) r Source #

TypeList prod ⇒ Inject c '[c ::: prod] r Source # 
Instance details

Defined in Constrained.Base

Methods

inject' ∷ (SOP '[c ::: prod] → r) → FunTy (ConstrOf 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 # 
Instance details

Defined in Constrained.Base

Methods

inject' ∷ (SOP ((c' ::: prod) ': (con ': constrs)) → r) → FunTy (ConstrOf c ((c' ::: prod) ': (con ': constrs))) r Source #

(TypeList prod, SOPLike (con ': cases) r) ⇒ SOPLike ((c ::: prod) ': (con ': cases)) r Source # 
Instance details

Defined in Constrained.Base

Methods

algebraSOP ((c ::: prod) ': (con ': cases)) → ALG ((c ::: prod) ': (con ': cases)) r Source #

consts ∷ r → ALG ((c ::: prod) ': (con ': cases)) r Source #

TypeList prod ⇒ SOPLike '[c ::: prod] r Source # 
Instance details

Defined in Constrained.Base

Methods

algebraSOP '[c ::: prod] → ALG '[c ::: prod] r Source #

consts ∷ r → ALG '[c ::: prod] r Source #

SopList (x' ': xs) (y ': ys) ⇒ SopList ((c ::: x) ': (x' ': xs)) (y ': ys) Source # 
Instance details

Defined in Constrained.Base

Methods

injectSOPLeftSOP ((c ::: x) ': (x' ': xs)) → SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) Source #

injectSOPRightSOP (y ': ys) → SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) Source #

caseSOPSOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) → Sum (SOP ((c ::: x) ': (x' ': xs))) (SOP (y ': ys)) Source #

SopList '[c ::: x] (y ': ys) Source # 
Instance details

Defined in Constrained.Base

Methods

injectSOPLeftSOP '[c ::: x] → SOP (Append '[c ::: x] (y ': ys)) Source #

injectSOPRightSOP (y ': ys) → SOP (Append '[c ::: x] (y ': ys)) Source #

caseSOPSOP (Append '[c ::: x] (y ': ys)) → Sum (SOP '[c ::: x]) (SOP (y ': ys)) Source #

type family SOPOf f where ... Source #

Turn a Rep into a list that flattens the sum structre and gives the constructors names: Maybe Int -> '[Nothing ::: '[()], Just ::: '[Int]] Either Int Bool -> '[Left ::: '[Int], Right ::: '[Bool]] data Foo = Foo Int Bool | Bar Double -> '[Foo ::: '[Int, Bool], Bar ::: '[Double]]

Equations

SOPOf (D1 _ f) = SOPOf f 
SOPOf (f :+: g) = Append (SOPOf f) (SOPOf g) 
SOPOf (C1 ('MetaCons constr _ _) f) = '[constr ::: Constr f] 

type family Constr f where ... Source #

Flatten a single constructor

Equations

Constr (S1 _ f) = Constr f 
Constr (K1 _ k) = '[k] 
Constr U1 = '[()] 
Constr (f :*: g) = Append (Constr f) (Constr g) 

type family SOP constrs where ... Source #

Turn a list from SOPOf into a Sum over Prod representation.

Equations

SOP '[c ::: prod] = ProdOver prod 
SOP ((c ::: prod) ': constrs) = Sum (ProdOver prod) (SOP constrs) 

type family ConstrOf c sop where ... Source #

Equations

ConstrOf c ((c ::: constr) ': sop) = constr 
ConstrOf c (_ ': sop) = ConstrOf c sop 

class Inject c constrs r where Source #

Methods

inject' ∷ (SOP constrs → r) → FunTy (ConstrOf c constrs) r Source #

Instances

Instances details
TypeList prod ⇒ Inject c ((c ::: prod) ': (prod' ': constrs)) r Source # 
Instance details

Defined in Constrained.Base

Methods

inject' ∷ (SOP ((c ::: prod) ': (prod' ': constrs)) → r) → FunTy (ConstrOf c ((c ::: prod) ': (prod' ': constrs))) r Source #

TypeList prod ⇒ Inject c '[c ::: prod] r Source # 
Instance details

Defined in Constrained.Base

Methods

inject' ∷ (SOP '[c ::: prod] → r) → FunTy (ConstrOf 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 # 
Instance details

Defined in Constrained.Base

Methods

inject' ∷ (SOP ((c' ::: prod) ': (con ': constrs)) → r) → FunTy (ConstrOf 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 ```

Equations

ALG '[c ::: prod] r = FunTy prod r → r 
ALG ((c ::: prod) ': constrs) r = FunTy prod r → ALG constrs r 

class SOPLike constrs r where Source #

Methods

algebraSOP constrs → ALG constrs r Source #

Run a SOP

consts ∷ r → ALG constrs r Source #

Ignore everything in the SOP

Instances

Instances details
(TypeList prod, SOPLike (con ': cases) r) ⇒ SOPLike ((c ::: prod) ': (con ': cases)) r Source # 
Instance details

Defined in Constrained.Base

Methods

algebraSOP ((c ::: prod) ': (con ': cases)) → ALG ((c ::: prod) ': (con ': cases)) r Source #

consts ∷ r → ALG ((c ::: prod) ': (con ': cases)) r Source #

TypeList prod ⇒ SOPLike '[c ::: prod] r Source # 
Instance details

Defined in Constrained.Base

Methods

algebraSOP '[c ::: prod] → ALG '[c ::: prod] r Source #

consts ∷ r → ALG '[c ::: prod] r Source #

class SimpleConstructor rep where Source #

Methods

toSimpleCon' ∷ rep p → ProdOver (Constr rep) Source #

fromSimpleCon'ProdOver (Constr rep) → rep p Source #

Instances

Instances details
SimpleConstructor (U1TypeType) Source # 
Instance details

Defined in Constrained.Base

(SimpleConstructor f, SimpleConstructor g, TypeList (Constr f), TypeList (Constr g)) ⇒ SimpleConstructor (f :*: g) Source # 
Instance details

Defined in Constrained.Base

Methods

toSimpleCon' ∷ (f :*: g) p → ProdOver (Constr (f :*: g)) Source #

fromSimpleCon'ProdOver (Constr (f :*: g)) → (f :*: g) p Source #

SimpleConstructor (K1 i k ∷ TypeType) Source # 
Instance details

Defined in Constrained.Base

Methods

toSimpleCon'K1 i k p → ProdOver (Constr (K1 i k)) Source #

fromSimpleCon'ProdOver (Constr (K1 i k)) → K1 i k p Source #

SimpleConstructor f ⇒ SimpleConstructor (S1 s f) Source # 
Instance details

Defined in Constrained.Base

Methods

toSimpleCon'S1 s f p → ProdOver (Constr (S1 s f)) Source #

fromSimpleCon'ProdOver (Constr (S1 s f)) → S1 s f p Source #

class SopList xs ys where Source #

Construct and deconstruct cases in a SOP

Methods

injectSOPLeftSOP xs → SOP (Append xs ys) Source #

injectSOPRightSOP ys → SOP (Append xs ys) Source #

caseSOPSOP (Append xs ys) → Sum (SOP xs) (SOP ys) Source #

Instances

Instances details
SopList (x' ': xs) (y ': ys) ⇒ SopList ((c ::: x) ': (x' ': xs)) (y ': ys) Source # 
Instance details

Defined in Constrained.Base

Methods

injectSOPLeftSOP ((c ::: x) ': (x' ': xs)) → SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) Source #

injectSOPRightSOP (y ': ys) → SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) Source #

caseSOPSOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) → Sum (SOP ((c ::: x) ': (x' ': xs))) (SOP (y ': ys)) Source #

SopList '[c ::: x] (y ': ys) Source # 
Instance details

Defined in Constrained.Base

Methods

injectSOPLeftSOP '[c ::: x] → SOP (Append '[c ::: x] (y ': ys)) Source #

injectSOPRightSOP (y ': ys) → SOP (Append '[c ::: x] (y ': ys)) Source #

caseSOPSOP (Append '[c ::: x] (y ': ys)) → Sum (SOP '[c ::: x]) (SOP (y ': ys)) Source #

class SimpleGeneric rep where Source #

Methods

toSimpleRep' ∷ rep p → SimplifyRep rep Source #

fromSimpleRep'SimplifyRep rep → rep p Source #

Instances

Instances details
(SimpleGeneric f, SimpleGeneric g, SopList (SOPOf f) (SOPOf g)) ⇒ SimpleGeneric (f :+: g) Source # 
Instance details

Defined in Constrained.Base

Methods

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 # 
Instance details

Defined in Constrained.Base

Methods

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 # 
Instance details

Defined in Constrained.Base

Methods

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 #

Methods

genList ∷ (BaseUniverse fn, MonadGenError m) ⇒ Specification fn a → Specification fn a → GenT m [a] Source #

theAddFn ∷ fn '[a, a] a Source #

theZero ∷ a Source #

Instances

Instances details
BaseUniverse fn ⇒ Foldy fn Int16 Source # 
Instance details

Defined in Constrained.Base

BaseUniverse fn ⇒ Foldy fn Int32 Source # 
Instance details

Defined in Constrained.Base

BaseUniverse fn ⇒ Foldy fn Int64 Source # 
Instance details

Defined in Constrained.Base

BaseUniverse fn ⇒ Foldy fn Int8 Source # 
Instance details

Defined in Constrained.Base

Methods

genList ∷ ∀ (m ∷ TypeType). (BaseUniverse fn, MonadGenError m) ⇒ Specification fn Int8Specification fn Int8GenT m [Int8] Source #

theAddFn ∷ fn '[Int8, Int8] Int8 Source #

theZeroInt8 Source #

BaseUniverse fn ⇒ Foldy fn Word16 Source # 
Instance details

Defined in Constrained.Base

BaseUniverse fn ⇒ Foldy fn Word32 Source # 
Instance details

Defined in Constrained.Base

BaseUniverse fn ⇒ Foldy fn Word64 Source # 
Instance details

Defined in Constrained.Base

BaseUniverse fn ⇒ Foldy fn Word8 Source # 
Instance details

Defined in Constrained.Base

BaseUniverse fn ⇒ Foldy fn Integer Source # 
Instance details

Defined in Constrained.Base

BaseUniverse fn ⇒ Foldy fn Natural Source # 
Instance details

Defined in Constrained.Base

BaseUniverse fn ⇒ Foldy fn Int Source # 
Instance details

Defined in Constrained.Base

Methods

genList ∷ ∀ (m ∷ TypeType). (BaseUniverse fn, MonadGenError m) ⇒ Specification fn IntSpecification fn IntGenT m [Int] Source #

theAddFn ∷ fn '[Int, Int] Int Source #

theZeroInt Source #

adds ∷ ∀ fn a. Foldy fn a ⇒ [a] → a Source #

data FoldSpec (fn ∷ [Type] → TypeType) a where Source #

Constructors

NoFoldFoldSpec 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

Instances details
HasSpec fn a ⇒ Pretty (WithPrec (FoldSpec fn a)) Source # 
Instance details

Defined in Constrained.Base

Methods

prettyWithPrec (FoldSpec fn a) → Doc ann Source #

prettyList ∷ [WithPrec (FoldSpec fn a)] → Doc ann Source #

Arbitrary (FoldSpec fn (Map k v)) Source # 
Instance details

Defined in Constrained.Spec.Map

Methods

arbitraryGen (FoldSpec fn (Map k v)) Source #

shrinkFoldSpec fn (Map k v) → [FoldSpec fn (Map k v)] Source #

Arbitrary (FoldSpec fn (Set a)) Source # 
Instance details

Defined in Constrained.Base

Methods

arbitraryGen (FoldSpec fn (Set a)) Source #

shrinkFoldSpec fn (Set a) → [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 # 
Instance details

Defined in Constrained.Spec.Generics

Methods

arbitraryGen (FoldSpec fn (a, b)) Source #

shrinkFoldSpec fn (a, b) → [FoldSpec fn (a, b)] Source #

(Arbitrary a, Arbitrary (TypeSpec fn a), Foldy fn a, BaseUniverse fn) ⇒ Arbitrary (FoldSpec fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

arbitraryGen (FoldSpec fn a) Source #

shrinkFoldSpec fn a → [FoldSpec fn a] Source #

HasSpec fn a ⇒ Show (FoldSpec fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

showsPrecIntFoldSpec fn a → ShowS Source #

showFoldSpec fn a → String Source #

showList ∷ [FoldSpec fn a] → ShowS Source #

HasSpec fn a ⇒ Pretty (FoldSpec fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

prettyFoldSpec fn a → Doc ann Source #

prettyList ∷ [FoldSpec fn a] → Doc ann Source #

preMapFoldSpecHasSpec fn a ⇒ fn '[a] b → FoldSpec fn b → FoldSpec fn a Source #

combineFoldSpecMonadGenError 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 #

narrowByFuelAndSize Source #

Arguments

∷ ∀ 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 IntegerSpecification 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 #

data SumSpec fn a b Source #

Constructors

SumSpec (Maybe (Int, Int)) (Specification fn a) (Specification fn b) 

Instances

Instances details
(Arbitrary (Specification fn a), Arbitrary (Specification fn b)) ⇒ Arbitrary (SumSpec fn a b) Source # 
Instance details

Defined in Constrained.Base

Methods

arbitraryGen (SumSpec fn a b) Source #

shrinkSumSpec fn a b → [SumSpec fn a b] Source #

(HasSpec fn a, HasSpec fn b, KnownNat (CountCases b)) ⇒ Monoid (SumSpec fn a b) Source # 
Instance details

Defined in Constrained.Base

Methods

memptySumSpec fn a b Source #

mappendSumSpec fn a b → SumSpec fn a b → SumSpec fn a b Source #

mconcat ∷ [SumSpec fn a b] → SumSpec fn a b Source #

(HasSpec fn a, HasSpec fn b) ⇒ Semigroup (SumSpec fn a b) Source # 
Instance details

Defined in Constrained.Base

Methods

(<>)SumSpec fn a b → SumSpec fn a b → SumSpec fn a b Source #

sconcatNonEmpty (SumSpec fn a b) → SumSpec fn a b Source #

stimesIntegral b0 ⇒ b0 → SumSpec fn a b → SumSpec fn a b Source #

(HasSpec fn a, HasSpec fn b) ⇒ Show (SumSpec fn a b) Source # 
Instance details

Defined in Constrained.Base

Methods

showsPrecIntSumSpec fn a b → ShowS Source #

showSumSpec fn a b → String Source #

showList ∷ [SumSpec fn a b] → ShowS Source #

type family CountCases a where ... Source #

Equations

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

data SetSpec fn a Source #

Constructors

SetSpec (Set a) (Specification fn a) (Specification fn Integer) 

Instances

Instances details
(BaseUniverse fn, Ord a, Arbitrary (Specification fn a), Arbitrary a) ⇒ Arbitrary (SetSpec fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

arbitraryGen (SetSpec fn a) Source #

shrinkSetSpec fn a → [SetSpec fn a] Source #

(Ord a, HasSpec fn a) ⇒ Monoid (SetSpec fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

memptySetSpec fn a Source #

mappendSetSpec fn a → SetSpec fn a → SetSpec fn a Source #

mconcat ∷ [SetSpec fn a] → SetSpec fn a Source #

(Ord a, HasSpec fn a) ⇒ Semigroup (SetSpec fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

(<>)SetSpec fn a → SetSpec fn a → SetSpec fn a Source #

sconcatNonEmpty (SetSpec fn a) → SetSpec fn a Source #

stimesIntegral b ⇒ b → SetSpec fn a → SetSpec fn a Source #

HasSpec fn a ⇒ Show (SetSpec fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

showsPrecIntSetSpec fn a → ShowS Source #

showSetSpec fn a → String Source #

showList ∷ [SetSpec fn a] → ShowS Source #

guardSetSpec ∷ (HasSpec fn a, Ord a) ⇒ SetSpec fn a → Specification fn (Set a) Source #

data ListSpec fn a Source #

Instances

Instances details
HasSpec fn a ⇒ Pretty (WithPrec (ListSpec fn a)) Source # 
Instance details

Defined in Constrained.Base

Methods

prettyWithPrec (ListSpec fn a) → Doc ann Source #

prettyList ∷ [WithPrec (ListSpec fn a)] → Doc ann Source #

(Arbitrary a, Arbitrary (FoldSpec fn a), Arbitrary (TypeSpec fn a), HasSpec fn a) ⇒ Arbitrary (ListSpec fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

arbitraryGen (ListSpec fn a) Source #

shrinkListSpec fn a → [ListSpec fn a] Source #

HasSpec fn a ⇒ Show (ListSpec fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

showsPrecIntListSpec fn a → ShowS Source #

showListSpec fn a → String Source #

showList ∷ [ListSpec fn a] → ShowS Source #

HasSpec fn a ⇒ Pretty (ListSpec fn a) Source # 
Instance details

Defined in Constrained.Base

Methods

prettyListSpec fn a → Doc ann Source #

prettyList ∷ [ListSpec fn a] → Doc ann Source #

class MaybeBounded a where Source #

Minimal complete definition

Nothing

Methods

lowerBoundMaybe a Source #

default lowerBoundBounded a ⇒ Maybe a Source #

upperBoundMaybe a Source #

default upperBoundBounded a ⇒ Maybe a Source #

Instances

Instances details
MaybeBounded Int16 Source # 
Instance details

Defined in Constrained.Base

MaybeBounded Int32 Source # 
Instance details

Defined in Constrained.Base

MaybeBounded Int64 Source # 
Instance details

Defined in Constrained.Base

MaybeBounded Int8 Source # 
Instance details

Defined in Constrained.Base

MaybeBounded Word16 Source # 
Instance details

Defined in Constrained.Base

MaybeBounded Word32 Source # 
Instance details

Defined in Constrained.Base

MaybeBounded Word64 Source # 
Instance details

Defined in Constrained.Base

MaybeBounded Word8 Source # 
Instance details

Defined in Constrained.Base

MaybeBounded Integer Source # 
Instance details

Defined in Constrained.Base

MaybeBounded Natural Source # 
Instance details

Defined in Constrained.Base

MaybeBounded Float Source # 
Instance details

Defined in Constrained.Base

MaybeBounded Int Source # 
Instance details

Defined in Constrained.Base

MaybeBounded (Ratio Integer) Source # 
Instance details

Defined in Constrained.Base

data NumSpec n Source #

Constructors

NumSpecInterval (Maybe n) (Maybe n) 

Instances

Instances details
(Arbitrary a, Ord a) ⇒ Arbitrary (NumSpec a) Source # 
Instance details

Defined in Constrained.Base

Methods

arbitraryGen (NumSpec a) Source #

shrinkNumSpec a → [NumSpec a] Source #

Ord n ⇒ Monoid (NumSpec n) Source # 
Instance details

Defined in Constrained.Base

Methods

memptyNumSpec n Source #

mappendNumSpec n → NumSpec n → NumSpec n Source #

mconcat ∷ [NumSpec n] → NumSpec n Source #

Ord n ⇒ Semigroup (NumSpec n) Source # 
Instance details

Defined in Constrained.Base

Methods

(<>)NumSpec n → NumSpec n → NumSpec n Source #

sconcatNonEmpty (NumSpec n) → NumSpec n Source #

stimesIntegral b ⇒ b → NumSpec n → NumSpec n Source #

Num (NumSpec Integer) Source # 
Instance details

Defined in Constrained.Base

Show n ⇒ Show (NumSpec n) Source # 
Instance details

Defined in Constrained.Base

Methods

showsPrecIntNumSpec n → ShowS Source #

showNumSpec n → String Source #

showList ∷ [NumSpec n] → ShowS Source #

Ord n ⇒ Eq (NumSpec n) Source # 
Instance details

Defined in Constrained.Base

Methods

(==)NumSpec n → NumSpec n → Bool Source #

(/=)NumSpec n → NumSpec n → Bool Source #

combineNumSpec ∷ (HasSpec fn n, Ord n, TypeSpec fn n ~ NumSpec n) ⇒ NumSpec n → NumSpec n → Specification fn n Source #

shrinkWithNumSpecArbitrary n ⇒ NumSpec n → n → [n] Source #

constrainInterval ∷ (MonadGenError m, Ord a, Num a, Show a) ⇒ Maybe a → Maybe a → Integer → m (a, a) Source #

conformsToNumSpecOrd n ⇒ n → NumSpec n → Bool Source #

toPredsNumSpec ∷ (Ord n, OrdLike fn n) ⇒ Term fn n → NumSpec n → Pred fn 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.

idFn ∷ ∀ fn a. Member (FunFn fn) fn ⇒ fn '[a] a Source #

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 #

Constructors

IdFunFn 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

Instances details
FunctionLike fn ⇒ FunctionLike (FunFn fn) Source # 
Instance details

Defined in Constrained.Base

Methods

sem ∷ ∀ (as ∷ [Type]) b. FunFn fn as b → FunTy as b Source #

(BaseUniverse fn, Member (FunFn fn) fn) ⇒ Functions (FunFn fn) fn Source # 
Instance details

Defined in Constrained.Base

Methods

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 # 
Instance details

Defined in Constrained.Base

Methods

showsPrecIntFunFn fn args res → ShowS Source #

showFunFn fn args res → String Source #

showList ∷ [FunFn fn args res] → ShowS Source #

Typeable fn ⇒ Eq (FunFn fn args res) Source # 
Instance details

Defined in Constrained.Base

Methods

(==)FunFn fn args res → FunFn fn args res → Bool Source #

(/=)FunFn fn args res → FunFn fn args res → Bool Source #

lessOrEqualFn ∷ ∀ fn a. (Ord a, OrdLike fn a) ⇒ fn '[a, a] Bool Source #

lessFn ∷ ∀ fn a. (Ord a, OrdLike fn a) ⇒ fn '[a, a] Bool Source #

data OrdFn (fn ∷ [Type] → TypeType) as b where Source #

Constructors

LessOrEqual ∷ (Ord a, OrdLike fn a) ⇒ OrdFn fn '[a, a] Bool 
Less ∷ (Ord a, OrdLike fn a) ⇒ OrdFn fn '[a, a] Bool 

Instances

Instances details
FunctionLike (OrdFn fn) Source # 
Instance details

Defined in Constrained.Base

Methods

sem ∷ ∀ (as ∷ [Type]) b. OrdFn fn as b → FunTy as b Source #

BaseUniverse fn ⇒ Functions (OrdFn fn) fn Source # 
Instance details

Defined in Constrained.Base

Methods

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 # 
Instance details

Defined in Constrained.Base

Methods

showsPrecIntOrdFn fn as b → ShowS Source #

showOrdFn fn as b → String Source #

showList ∷ [OrdFn fn as b] → ShowS Source #

Eq (OrdFn fn as b) Source # 
Instance details

Defined in Constrained.Base

Methods

(==)OrdFn fn as b → OrdFn fn as b → Bool Source #

(/=)OrdFn fn as b → OrdFn fn as b → Bool Source #

class HasSpec fn a ⇒ OrdLike fn a where Source #

Minimal complete definition

Nothing

Methods

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

Instances details
(HasSpec fn a, MaybeBounded a, Num a, TypeSpec fn a ~ NumSpec a) ⇒ OrdLike fn a Source # 
Instance details

Defined in Constrained.Base

Methods

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 #

Constructors

FoldMap ∷ (HasSpec fn a, Foldy fn b, Show (fn '[a] b), Eq (fn '[a] b)) ⇒ fn '[a] b → ListFn fn '[[a]] b 

Instances

Instances details
FunctionLike fn ⇒ FunctionLike (ListFn fn) Source # 
Instance details

Defined in Constrained.Base

Methods

sem ∷ ∀ (as ∷ [Type]) b. ListFn fn as b → FunTy as b Source #

BaseUniverse fn ⇒ Functions (ListFn fn) fn Source # 
Instance details

Defined in Constrained.Base

Methods

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 # 
Instance details

Defined in Constrained.Base

Methods

showsPrecIntListFn fn args res → ShowS Source #

showListFn fn args res → String Source #

showList ∷ [ListFn fn args res] → ShowS Source #

Typeable fn ⇒ Eq (ListFn fn args res) Source # 
Instance details

Defined in Constrained.Base

Methods

(==)ListFn fn args res → ListFn fn args res → Bool Source #

(/=)ListFn fn args res → ListFn fn args res → Bool 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 #

addFn ∷ ∀ fn a. NumLike fn a ⇒ fn '[a, a] a Source #

negateFn ∷ ∀ fn a. NumLike fn a ⇒ fn '[a] a Source #

data IntFn (fn ∷ [Type] → TypeType) as b where Source #

Constructors

AddNumLike fn a ⇒ IntFn fn '[a, a] a 
NegateNumLike fn a ⇒ IntFn fn '[a] a 

Instances

Instances details
FunctionLike (IntFn fn) Source # 
Instance details

Defined in Constrained.Base

Methods

sem ∷ ∀ (as ∷ [Type]) b. IntFn fn as b → FunTy as b Source #

BaseUniverse fn ⇒ Functions (IntFn fn) fn Source # 
Instance details

Defined in Constrained.Base

Methods

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 # 
Instance details

Defined in Constrained.Base

Methods

showsPrecIntIntFn fn as b → ShowS Source #

showIntFn fn as b → String Source #

showList ∷ [IntFn fn as b] → ShowS Source #

Eq (IntFn fn as b) Source # 
Instance details

Defined in Constrained.Base

Methods

(==)IntFn fn as b → IntFn fn as b → Bool Source #

(/=)IntFn fn as b → IntFn fn as b → Bool Source #

class (Num a, HasSpec fn a) ⇒ NumLike fn a where Source #

Minimal complete definition

Nothing

Methods

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 #

negateSpecTypeSpec 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

Instances details
(HasSpec fn a, Ord a, Num a, TypeSpec fn a ~ NumSpec a, MaybeBounded a) ⇒ NumLike fn a Source # 
Instance details

Defined in Constrained.Base

Methods

subtractSpec ∷ a → TypeSpec fn a → Specification fn a Source #

negateSpecTypeSpec 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 #

not_BaseUniverse fn ⇒ Term fn BoolTerm fn Bool Source #

(||.)BaseUniverse fn ⇒ Term fn BoolTerm fn BoolTerm fn Bool infixr 2 Source #

elem_ ∷ ∀ a fn. HasSpec fn a ⇒ Term fn a → Term fn [a] → Term fn Bool Source #

member_ ∷ ∀ a fn. (HasSpec fn a, Ord a) ⇒ Term fn a → Term fn (Set a) → Term fn Bool Source #

subset_ ∷ (HasSpec fn a, Ord a) ⇒ Term fn (Set a) → Term fn (Set a) → Term fn Bool Source #

disjoint_ ∷ (HasSpec fn a, Ord a) ⇒ Term fn (Set a) → Term fn (Set a) → Term fn Bool Source #

singleton_ ∷ (HasSpec fn a, Ord a) ⇒ Term fn a → Term fn (Set a) Source #

union_ ∷ ∀ a fn. (HasSpec fn a, Ord a) ⇒ Term fn (Set a) → Term fn (Set a) → Term fn (Set a) Source #

fromList_ ∷ ∀ a fn. (HasSpec fn a, Ord a) ⇒ Term fn [a] → Term fn (Set a) Source #

sizeOf_ ∷ ∀ a fn. (HasSpec fn a, Sized a) ⇒ Term fn a → Term fn Integer 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

null_ ∷ (HasSpec fn a, Sized a) ⇒ Term fn a → Term fn Bool Source #

(<=.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool infix 4 Source #

(>=.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool infix 4 Source #

(<.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool infix 4 Source #

(>.) ∷ (Ord a, OrdLike fn a) ⇒ Term fn a → Term fn a → Term fn Bool infix 4 Source #

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

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

sum_ ∷ (BaseUniverse fn, Member (FunFn fn) fn, Foldy fn a) ⇒ Term fn [a] → Term fn a Source #

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 #

assert ∷ (BaseUniverse fn, IsPred p fn) ⇒ 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 #

exists ∷ ∀ a p fn. (HasSpec fn a, IsPred p fn) ⇒ ((∀ b. Term fn b → b) → GE a) → (Term fn a → p) → Pred fn Source #

unsafeExists ∷ ∀ a p fn. (HasSpec fn a, IsPred p fn) ⇒ (Term fn a → p) → Pred fn Source #

letBind ∷ (HasSpec fn a, IsPred p fn) ⇒