| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Constrained.Base
Contents
Description
This module contains the most basic parts the implementation. Essentially everything to define Specification, HasSpec, HasSimpleRep, Term, Pred, and the Syntax, Semantics, and Logic class. It also has a few HasSpec, HasSimpleRep, and Logic instances for basic types needed to define the default types and methods of HasSpec. It also supplies Eq, Pretty, and Show instances on the syntax (Term, Pred, Binder etc.) because many functions require these instances. It exports functions that define the user interface to the domain embedded language (constrained, forall, exists etc.). And, by design, nothing more.
Synopsis
- class Syntax (t ∷ [Type] → Type → Type) where
- class Syntax t ⇒ Semantics (t ∷ [Type] → Type → Type) where
- type LogicRequires t = (Typeable t, Syntax t, Semantics t)
- class LogicRequires t ⇒ Logic t where
- propagateTypeSpec ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a
- propagateMemberSpec ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a
- propagate ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → Specification b → Specification a
- rewriteRules ∷ (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ t dom rng → List Term dom → Evidence (AppRequires t dom rng) → Maybe (Term rng)
- mapTypeSpec ∷ ∀ a b. (HasSpec a, HasSpec b) ⇒ t '[a] b → TypeSpec a → Specification b
- saturate ∷ t dom Bool → List Term dom → [Pred]
- propagateSpec ∷ ∀ v a. HasSpec v ⇒ Specification a → Ctx v a → Specification v
- ctxHasSpec ∷ Ctx v a → Evidence (HasSpec a)
- data Ctx v a where
- data HOLE a b where
- toCtx ∷ ∀ m v a. (Typeable v, Show v, MonadGenError m, HasCallStack) ⇒ Var v → Term a → m (Ctx v a)
- toCtxList ∷ ∀ m v as. (Show v, Typeable v, MonadGenError m, HasCallStack) ⇒ Var v → List Term as → m (ListCtx Value as (Ctx v))
- pattern Unary ∷ HOLE a' a → ListCtx f '[a] (HOLE a')
- pattern (:<:) ∷ (Typeable b, Show b) ⇒ HOLE c a → b → ListCtx Value '[a, b] (HOLE c)
- pattern (:>:) ∷ (Typeable a, Show a) ⇒ a → HOLE c b → ListCtx Value '[a, b] (HOLE c)
- flipCtx ∷ (Typeable a, Show a, Typeable b, Show b) ⇒ ListCtx Value '[a, b] (HOLE c) → ListCtx Value '[b, a] (HOLE c)
- fromListCtx ∷ All HasSpec as ⇒ ListCtx Value as (HOLE a) → Term a → List Term as
- sameFunSym ∷ ∀ (t1 ∷ [Type] → Type → Type) d1 r1 (t2 ∷ [Type] → Type → Type) d2 r2. (AppRequires t1 d1 r1, AppRequires t2 d2 r2) ⇒ t1 d1 r1 → t2 d2 r2 → Maybe (t1 d1 r1, t1 :~: t2, d1 :~: d2, r1 :~: r2)
- getWitness ∷ ∀ t t' d r. (AppRequires t d r, Typeable t') ⇒ t d r → Maybe (t' d r)
- data Specification a where
- ExplainSpec ∷ [String] → Specification a → Specification a
- MemberSpec ∷ NonEmpty a → Specification a
- ErrorSpec ∷ NonEmpty String → Specification a
- SuspendedSpec ∷ HasSpec a ⇒ Var a → Pred → Specification a
- TypeSpec ∷ HasSpec a ⇒ TypeSpec a → [a] → Specification a
- TrueSpec ∷ Specification a
- typeSpec ∷ HasSpec a ⇒ TypeSpec a → Specification a
- class (Typeable a, Eq a, Show a, Show (TypeSpec a), Typeable (TypeSpec a)) ⇒ HasSpec a where
- type TypeSpec a
- type Prerequisites a ∷ Constraint
- emptySpec ∷ TypeSpec a
- combineSpec ∷ TypeSpec a → TypeSpec a → Specification a
- genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a
- conformsTo ∷ HasCallStack ⇒ a → TypeSpec a → Bool
- shrinkWithTypeSpec ∷ TypeSpec a → a → [a]
- toPreds ∷ Term a → TypeSpec a → Pred
- cardinalTypeSpec ∷ TypeSpec a → Specification Integer
- cardinalTrueSpec ∷ Specification Integer
- typeSpecHasError ∷ TypeSpec a → Maybe (NonEmpty String)
- alternateShow ∷ TypeSpec a → BinaryShow
- monadConformsTo ∷ a → TypeSpec a → Writer [String] Bool
- typeSpecOpt ∷ TypeSpec a → [a] → Specification a
- guardTypeSpec ∷ [String] → TypeSpec a → Specification a
- prerequisites ∷ Evidence (Prerequisites a)
- type GenericRequires a = (HasSpec a, HasSimpleRep a, HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a))
- data BaseW (dom ∷ [Type]) (rng ∷ Type) where
- ToGenericW ∷ GenericRequires a ⇒ BaseW '[a] (SimpleRep a)
- FromGenericW ∷ GenericRequires a ⇒ BaseW '[SimpleRep a] a
- toGeneric_ ∷ ∀ a. GenericRequires a ⇒ Term a → Term (SimpleRep a)
- fromGeneric_ ∷ ∀ a. (GenericRequires a, AppRequires BaseW '[SimpleRep a] a) ⇒ Term (SimpleRep a) → Term a
- fromSimpleRepSpec ∷ ∀ a. (HasSpec a, HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep a)) ⇒ Specification (SimpleRep a) → Specification a
- toSimpleRepSpec ∷ ∀ a. (HasSpec (SimpleRep a), HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep a)) ⇒ Specification a → Specification (SimpleRep a)
- data BinaryShow where
- BinaryShow ∷ ∀ a. String → [Doc a] → BinaryShow
- NonBinary ∷ BinaryShow
- type AppRequires t dom rng = (Logic t, TypeList dom, Eq (t dom rng), Show (t dom rng), Typeable dom, Typeable rng, All HasSpec dom, HasSpec rng)
- data Term a where
- sameTerms ∷ All HasSpec as ⇒ List Term as → List Term as → Bool
- appSym ∷ ∀ t as b. AppRequires t as b ⇒ t as b → List Term as → Term b
- appTerm ∷ ∀ t ds r. AppRequires t ds r ⇒ t ds r → FunTy (MapList Term ds) (Term r)
- name ∷ String → Term a → Term a
- named ∷ String → Term a → Term a
- data Binder a where
- bind ∷ (HasSpec a, IsPred p) ⇒ (Term a → p) → Binder a
- data Weighted f a = Weighted {}
- mapWeighted ∷ (f a → g b) → Weighted f a → Weighted g b
- traverseWeighted ∷ Applicative m ⇒ (f a → m (g a)) → Weighted f a → m (Weighted g a)
- data Pred where
- ElemPred ∷ ∀ a. HasSpec a ⇒ Bool → Term a → NonEmpty a → Pred
- Monitor ∷ ((∀ a. Term a → a) → Property → Property) → Pred
- And ∷ [Pred] → Pred
- Exists ∷ ((∀ b. Term b → b) → GE a) → Binder a → Pred
- Subst ∷ HasSpec a ⇒ Var a → Term a → Pred → Pred
- Let ∷ Term a → Binder a → Pred
- Assert ∷ Term Bool → Pred
- Reifies ∷ (HasSpec a, HasSpec b) ⇒ Term b → Term a → (a → b) → Pred
- DependsOn ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Pred
- ForAll ∷ (Forallable t a, HasSpec t, HasSpec a) ⇒ Term t → Binder a → Pred
- Case ∷ HasSpec (SumOver as) ⇒ Term (SumOver as) → List (Weighted Binder) as → Pred
- When ∷ HasSpec Bool ⇒ Term Bool → Pred → Pred
- GenHint ∷ HasGenHint a ⇒ Hint a → Term a → Pred
- TruePred ∷ Pred
- FalsePred ∷ NonEmpty String → Pred
- Explain ∷ NonEmpty String → Pred → Pred
- class Forallable t e | t → e where
- fromForAllSpec ∷ (HasSpec t, HasSpec e) ⇒ Specification e → Specification t
- forAllToList ∷ t → [e]
- class (HasSpec a, Show (Hint a)) ⇒ HasGenHint a where
- type Hint a
- giveHint ∷ Hint a → Specification a
- class Show p ⇒ IsPred p where
- memberSpecList ∷ [a] → NonEmpty String → Specification a
- explainSpec ∷ [String] → Specification a → Specification a
- explainSpecOpt ∷ [String] → Specification a → Specification a
- equalSpec ∷ a → Specification a
- notEqualSpec ∷ ∀ a. HasSpec a ⇒ a → Specification a
- notMemberSpec ∷ ∀ a f. (HasSpec a, Foldable f) ⇒ f a → Specification a
- constrained ∷ ∀ a p. (IsPred p, HasSpec a) ⇒ (Term a → p) → Specification a
- isErrorLike ∷ ∀ a. Specification a → Bool
- errorLikeMessage ∷ ∀ a. Specification a → NonEmpty String
- fromGESpec ∷ HasCallStack ⇒ GE (Specification a) → Specification a
- addToErrorSpec ∷ NonEmpty String → Specification a → Specification a
- data WithPrec a = WithPrec Int a
- parensIf ∷ Bool → Doc ann → Doc ann
- prettyPrec ∷ Pretty (WithPrec a) ⇒ Int → a → Doc ann
- ppList ∷ ∀ f as ann. All HasSpec as ⇒ (∀ a. HasSpec a ⇒ f a → Doc ann) → List f as → [Doc ann]
- ppList_ ∷ ∀ f as ann. (∀ a. f a → Doc ann) → List f as → [Doc ann]
- prettyType ∷ ∀ t x. Typeable t ⇒ Doc x
- vsep' ∷ [Doc ann] → Doc ann
- (/>) ∷ Doc ann → Doc ann → Doc ann
- short ∷ ∀ a x. (Show a, Typeable a) ⇒ [a] → Doc x
- showType ∷ ∀ t. Typeable t ⇒ String
- data Fun dom rng where
- Fun ∷ ∀ t dom rng. AppRequires t dom rng ⇒ t dom rng → Fun dom rng
- extractf ∷ ∀ t d r. LogicRequires t ⇒ Fun d r → Maybe (t d r)
- appFun ∷ Fun '[x] b → Term x → Term b
- sameFun ∷ Fun d1 r1 → Fun d2 r2 → Bool
- pattern FromGeneric ∷ ∀ rng. () ⇒ ∀ a. (rng ~ a, GenericRequires a, HasSpec a, AppRequires BaseW '[SimpleRep a] rng) ⇒ Term (SimpleRep a) → Term rng
- pattern ToGeneric ∷ ∀ rng. () ⇒ ∀ a. (rng ~ SimpleRep a, GenericRequires a, HasSpec a, AppRequires BaseW '[a] rng) ⇒ Term a → Term rng
Documentation
class Syntax (t ∷ [Type] → Type → Type) where Source #
A First-order typed logic has 4 components 1. Terms (Variables (x), Constants (5), and Applications (F x 5) Applications, apply a function symbol to a list of arguments: (FunctionSymbol term1 .. termN) 2. Predicates (Ordered, Odd, ...) 3. Connectives (And, Or, Not, =>, ...) 4. Quantifiers (Forall, Exists)
The Syntax, Semantics, and Logic classes implement new function symbols in the first order logic. Note that a function symbol is first order data, that uniquely identifies a higher order function. The three classes supply varying levels of functionality, relating to the Syntax, Semantics, and Logical operations of the function symbol.
Syntactic operations are ones that have to do with the structure and appearence of the type.
Minimal complete definition
Nothing
Methods
inFix ∷ ∀ dom rng. t dom rng → Bool Source #
prettyWit ∷ ∀ dom rng ann. (All HasSpec dom, HasSpec rng) ⇒ t dom rng → List Term dom → Int → Maybe (Doc ann) Source #
Instances
class Syntax t ⇒ Semantics (t ∷ [Type] → Type → Type) where Source #
Semantic operations are ones that give the function symbol, meaning as a function. I.e. how to apply the function to a list of arguments and return a value.
Instances
type LogicRequires t = (Typeable t, Syntax t, Semantics t) Source #
class LogicRequires t ⇒ Logic t where Source #
Logical operations are one that support reasoning about how a function symbol relates to logical properties, that we call Specification's
Minimal complete definition
Methods
propagateTypeSpec ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source #
propagateMemberSpec ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source #
propagate ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source #
rewriteRules ∷ (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ t dom rng → List Term dom → Evidence (AppRequires t dom rng) → Maybe (Term rng) Source #
mapTypeSpec ∷ ∀ a b. (HasSpec a, HasSpec b) ⇒ t '[a] b → TypeSpec a → Specification b Source #
Instances
propagateSpec ∷ ∀ v a. HasSpec v ⇒ Specification a → Ctx v a → Specification v 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
| CtxHOLE ∷ HasSpec v ⇒ Ctx v v | A single hole of type |
| CtxApp ∷ (AppRequires fn as b, HasSpec b, TypeList as, Typeable as, All HasSpec as, Logic fn) ⇒ fn as b → ListCtx Value as (Ctx v) → Ctx v b | The application `f vs Ctx vs'` |
toCtx ∷ ∀ m v a. (Typeable v, Show v, MonadGenError m, HasCallStack) ⇒ Var v → Term a → m (Ctx v a) Source #
toCtxList ∷ ∀ m v as. (Show v, Typeable v, MonadGenError m, HasCallStack) ⇒ Var v → List Term as → m (ListCtx Value as (Ctx v)) Source #
pattern Unary ∷ HOLE a' a → ListCtx f '[a] (HOLE a') Source #
A Convenient pattern for singleton contexts
pattern (:<:) ∷ (Typeable b, Show b) ⇒ HOLE c a → b → ListCtx Value '[a, b] (HOLE c) Source #
Convenient patterns for binary contexts (the arrow :<: points towards the hole)
pattern (:>:) ∷ (Typeable a, Show a) ⇒ a → HOLE c b → ListCtx Value '[a, b] (HOLE c) Source #
Convenient patterns for binary contexts (the arrow :>: points towards the hole)
flipCtx ∷ (Typeable a, Show a, Typeable b, Show b) ⇒ ListCtx Value '[a, b] (HOLE c) → ListCtx Value '[b, a] (HOLE c) Source #
fromListCtx ∷ All HasSpec as ⇒ ListCtx Value as (HOLE a) → Term a → List Term as Source #
From a ListCtx, build a (List Term as), to which the function symbol can be applied.
sameFunSym ∷ ∀ (t1 ∷ [Type] → Type → Type) d1 r1 (t2 ∷ [Type] → Type → Type) d2 r2. (AppRequires t1 d1 r1, AppRequires t2 d2 r2) ⇒ t1 d1 r1 → t2 d2 r2 → Maybe (t1 d1 r1, t1 :~: t2, d1 :~: d2, r1 :~: r2) Source #
getWitness ∷ ∀ t t' d r. (AppRequires t d r, Typeable t') ⇒ t d r → Maybe (t' d r) Source #
Here we only care about the Type t and the Symbol s
the dom, and the rng can be anything. Useful for defining patterns.
data Specification a where Source #
A `Specification a` denotes a set of as
Constructors
| ExplainSpec ∷ [String] → Specification a → Specification a | Explain a Specification |
| MemberSpec | Elements of a known set |
Fields
| |
| ErrorSpec ∷ NonEmpty String → Specification a | The empty set |
| SuspendedSpec | The set described by some predicates over the bound variable. |
Fields
| |
| TypeSpec | A type-specific spec |
Fields
| |
| TrueSpec ∷ Specification a | Anything |
Instances
| (HasSpec a, Arbitrary (TypeSpec a)) ⇒ Arbitrary (Specification a) Source # | |
Defined in Constrained.TheKnot Methods arbitrary ∷ Gen (Specification a) Source # shrink ∷ Specification a → [Specification a] Source # | |
| HasSpec a ⇒ Monoid (Specification a) | |
Defined in Constrained.Conformance Methods mempty ∷ Specification a mappend ∷ Specification a → Specification a → Specification a mconcat ∷ [Specification a] → Specification a | |
| HasSpec a ⇒ Semigroup (Specification a) | |
Defined in Constrained.Conformance Methods (<>) ∷ Specification a → Specification a → Specification a # sconcat ∷ NonEmpty (Specification a) → Specification a stimes ∷ Integral b ⇒ b → Specification a → Specification a | |
| Number Integer ⇒ Num (Specification Integer) | This is very liberal, since in lots of cases it returns TrueSpec.
for example all operations on SuspendedSpec, and certain
operations between TypeSpec and MemberSpec. Perhaps we should
remove it. Only the addSpec (+) and multSpec (*) methods are used.
But, it is kind of cool ...
In Fact we can use this to make Num(Specification n) instance for any |
Defined in Constrained.NumSpec Methods (+) ∷ Specification Integer → Specification Integer → Specification Integer (-) ∷ Specification Integer → Specification Integer → Specification Integer (*) ∷ Specification Integer → Specification Integer → Specification Integer negate ∷ Specification Integer → Specification Integer abs ∷ Specification Integer → Specification Integer signum ∷ Specification Integer → Specification Integer fromInteger ∷ Integer → Specification Integer | |
| HasSpec a ⇒ Show (Specification a) Source # | |
Defined in Constrained.Base Methods showsPrec ∷ Int → Specification a → ShowS show ∷ Specification a → String showList ∷ [Specification a] → ShowS | |
| HasSpec a ⇒ Pretty (Specification a) Source # | |
Defined in Constrained.Base | |
| HasSpec a ⇒ Pretty (WithPrec (Specification a)) Source # | |
Defined in Constrained.Base Methods pretty ∷ WithPrec (Specification a) → Doc ann Source # prettyList ∷ [WithPrec (Specification a)] → Doc ann Source # | |
class (Typeable a, Eq a, Show a, Show (TypeSpec a), Typeable (TypeSpec a)) ⇒ HasSpec a where Source #
Minimal complete definition
Nothing
Associated Types
The `TypeSpec a` is the type-specific `Specification a`.
type Prerequisites a ∷ Constraint Source #
Prerequisites for the instance that are sometimes necessary
when working with e.g. Specifications or functions in the universe.
type Prerequisites a = ()
Methods
emptySpec ∷ TypeSpec a Source #
default emptySpec ∷ (HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) ⇒ TypeSpec a Source #
combineSpec ∷ TypeSpec a → TypeSpec a → Specification a Source #
default combineSpec ∷ (HasSimpleRep a, HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) ⇒ TypeSpec a → TypeSpec a → Specification a Source #
genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec 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 (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) ⇒ (HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a Source #
conformsTo ∷ HasCallStack ⇒ a → TypeSpec a → Bool Source #
Check conformance to the spec.
default conformsTo ∷ (HasSimpleRep a, HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) ⇒ HasCallStack ⇒ a → TypeSpec a → Bool Source #
shrinkWithTypeSpec ∷ TypeSpec a → a → [a] Source #
Shrink an a with the aide of a Specification
default shrinkWithTypeSpec ∷ (HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a) ⇒ TypeSpec a → a → [a] Source #
toPreds ∷ Term a → TypeSpec a → Pred 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 (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a) ⇒ Term a → TypeSpec a → Pred Source #
cardinalTypeSpec ∷ TypeSpec a → Specification Integer Source #
Compute an upper and lower bound on the number of solutions genFromTypeSpec might return
default cardinalTypeSpec ∷ (HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) ⇒ TypeSpec a → Specification Integer Source #
cardinalTrueSpec ∷ Specification 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
typeSpecHasError ∷ TypeSpec a → Maybe (NonEmpty String) Source #
alternateShow ∷ TypeSpec a → BinaryShow Source #
monadConformsTo ∷ a → TypeSpec a → Writer [String] Bool Source #
typeSpecOpt ∷ TypeSpec a → [a] → Specification 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.
guardTypeSpec ∷ [String] → TypeSpec a → Specification a Source #
This can be used to detect self inconsistencies in a (TypeSpec t)
Note this is similar to typeSpecHasError, and the default
value for typeSpecHasError is written in terms of guardTypeSpec
Both typeSpecHasError and guardTypeSpec can be set individually.
prerequisites ∷ Evidence (Prerequisites a) Source #
Materialize the Prerequisites dictionary. It should not be necessary to
implement this function manually.
default prerequisites ∷ Prerequisites a ⇒ Evidence (Prerequisites a) Source #
Instances
type GenericRequires a = (HasSpec a, HasSimpleRep a, HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) Source #
data BaseW (dom ∷ [Type]) (rng ∷ Type) where Source #
Constructors
| ToGenericW ∷ GenericRequires a ⇒ BaseW '[a] (SimpleRep a) | |
| FromGenericW ∷ GenericRequires a ⇒ BaseW '[SimpleRep a] a |
Instances
| Logic BaseW Source # | |
Defined in Constrained.Base Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires BaseW as b, HasSpec a) ⇒ BaseW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires BaseW as b, HasSpec a) ⇒ BaseW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires BaseW as b, HasSpec a) ⇒ BaseW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source # rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ BaseW dom rng → List Term dom → Evidence (AppRequires BaseW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ BaseW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). BaseW dom Bool → List Term dom → [Pred] Source # | |
| Semantics BaseW Source # | |
| Syntax BaseW Source # | |
| Show (BaseW d r) Source # | |
| Eq (BaseW dom rng) Source # | |
toGeneric_ ∷ ∀ a. GenericRequires a ⇒ Term a → Term (SimpleRep a) Source #
fromGeneric_ ∷ ∀ a. (GenericRequires a, AppRequires BaseW '[SimpleRep a] a) ⇒ Term (SimpleRep a) → Term a Source #
fromSimpleRepSpec ∷ ∀ a. (HasSpec a, HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep a)) ⇒ Specification (SimpleRep a) → Specification a Source #
toSimpleRepSpec ∷ ∀ a. (HasSpec (SimpleRep a), HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep a)) ⇒ Specification a → Specification (SimpleRep a) Source #
data BinaryShow where Source #
Constructors
| BinaryShow ∷ ∀ a. String → [Doc a] → BinaryShow | |
| NonBinary ∷ BinaryShow |
type AppRequires t dom rng = (Logic t, TypeList dom, Eq (t dom rng), Show (t dom rng), Typeable dom, Typeable rng, All HasSpec dom, HasSpec rng) Source #
What constraints does the Term constructor App require? (Logic sym t dom rng) supplies the Logic of propagating contexts (All HasSpec dom) the argument types are part of the system (HasSpec rng) the return type is part of the system.
Constructors
| App ∷ ∀ t dom rng. AppRequires t dom rng ⇒ t dom rng → List Term dom → Term rng | |
| Lit ∷ (Typeable a, Eq a, Show a) ⇒ a → Term a | |
| V ∷ HasSpec a ⇒ Var a → Term a |
Instances
| (Ord a, HasSpec a, HasSpec (Set a)) ⇒ Monoid (Term (Set a)) | |
| (Ord a, HasSpec a, HasSpec (Set a)) ⇒ Semigroup (Term (Set a)) | |
| NumLike a ⇒ Num (Term a) | |
| Show a ⇒ Show (Term a) Source # | |
| IsPred (Term Bool) Source # | |
| Rename (Term a) Source # | |
| HasVariables (Term a) Source # | |
| Eq (Term a) Source # | |
| Show a ⇒ Pretty (Term a) Source # | |
| Show a ⇒ Pretty (WithPrec (Term a)) Source # | |
| HasVariables (List Term as) Source # | |
appSym ∷ ∀ t as b. AppRequires t as b ⇒ t as b → List Term as → Term b Source #
Recall function symbols are objects that you can use to build applications
They carry information about both its semantic and logical properties.
Usually the Haskel name ends in '_', for example consider: not_, subset_ ,lookup_, toGeneric_
Infix function symbols names end in ., for example: ==. , <=.
E.g appTerm ToGenericW :: Term a -> Term(SimpleRep a)
(appTerm ToGenericW (lit True)) builds the Term (toGeneric_ True)
Note the witness (ToGenericW ) must have a Logic instance like:
instance Logic BaseW '[a] (SimpleRep a) where ...
type of ToGenericW ^ arg types^ result type^
The Logic instance does not demand any of these things have any properties at all.
It is here, where we actually build the App node, that we demand the properties App terms require.
App :: AppRequires s t ds r => t s ds r -> List Term dom -> Term rng
named ∷ String → Term a → Term a Source #
Give a Term a nameHint, if its a Var, and doesn't already have one, otherwise return the Term unchanged.
Instances
| Foldable f ⇒ Foldable (Weighted f) Source # | |
Defined in Constrained.Base Methods fold ∷ Monoid m ⇒ Weighted f m → m foldMap ∷ Monoid m ⇒ (a → m) → Weighted f a → m foldMap' ∷ Monoid m ⇒ (a → m) → Weighted f a → m foldr ∷ (a → b → b) → b → Weighted f a → b foldr' ∷ (a → b → b) → b → Weighted f a → b foldl ∷ (b → a → b) → b → Weighted f a → b foldl' ∷ (b → a → b) → b → Weighted f a → b foldr1 ∷ (a → a → a) → Weighted f a → a foldl1 ∷ (a → a → a) → Weighted f a → a elem ∷ Eq a ⇒ a → Weighted f a → Bool maximum ∷ Ord a ⇒ Weighted f a → a minimum ∷ Ord a ⇒ Weighted f a → a | |
| Traversable f ⇒ Traversable (Weighted f) Source # | |
| Functor f ⇒ Functor (Weighted f) Source # | |
| Rename (f a) ⇒ Rename (Weighted f a) Source # | |
| HasVariables (f a) ⇒ HasVariables (Weighted f a) Source # | |
| HasVariables (List (Weighted Binder) as) Source # | |
| Pretty (f a) ⇒ Pretty (Weighted f a) Source # | |
mapWeighted ∷ (f a → g b) → Weighted f a → Weighted g b Source #
traverseWeighted ∷ Applicative m ⇒ (f a → m (g a)) → Weighted f a → m (Weighted g a) Source #
Constructors
| ElemPred ∷ ∀ a. HasSpec a ⇒ Bool → Term a → NonEmpty a → Pred | |
| Monitor ∷ ((∀ a. Term a → a) → Property → Property) → Pred | |
| And ∷ [Pred] → Pred | |
| Exists | |
| Subst ∷ HasSpec a ⇒ Var a → Term a → Pred → Pred | |
| Let ∷ Term a → Binder a → Pred | |
| Assert ∷ Term Bool → Pred | |
| Reifies | |
| DependsOn ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Pred | |
| ForAll ∷ (Forallable t a, HasSpec t, HasSpec a) ⇒ Term t → Binder a → Pred | |
| Case | |
| When ∷ HasSpec Bool ⇒ Term Bool → Pred → Pred | |
| GenHint ∷ HasGenHint a ⇒ Hint a → Term a → Pred | |
| TruePred ∷ Pred | |
| FalsePred ∷ NonEmpty String → Pred | |
| Explain ∷ NonEmpty String → Pred → Pred | |
class Forallable t e | t → e where Source #
Minimal complete definition
Nothing
Methods
fromForAllSpec ∷ (HasSpec t, HasSpec e) ⇒ Specification e → Specification t Source #
default fromForAllSpec ∷ (HasSpec t, HasSpec e, HasSimpleRep t, TypeSpec t ~ TypeSpec (SimpleRep t), Forallable (SimpleRep t) e, HasSpec (SimpleRep t)) ⇒ Specification e → Specification t Source #
forAllToList ∷ t → [e] Source #
default forAllToList ∷ (HasSimpleRep t, Forallable (SimpleRep t) e) ⇒ t → [e] Source #
Instances
class (HasSpec a, Show (Hint a)) ⇒ HasGenHint a where Source #
Hints are things that only affect generation, and not validation. For instance, parameters to control distribution of generated values.
Methods
giveHint ∷ Hint a → Specification a Source #
Instances
| HasSpec a ⇒ HasGenHint (BinTree a) Source # | |
| HasSpec a ⇒ HasGenHint (Tree a) Source # | |
Defined in Constrained.Spec.Tree Methods giveHint ∷ Hint (Tree a) → Specification (Tree a) Source # | |
| (Sized [a], HasSpec a) ⇒ HasGenHint [a] Source # | |
Defined in Constrained.TheKnot Methods giveHint ∷ Hint [a] → Specification [a] Source # | |
| (Ord k, HasSpec k, HasSpec v, HasSpec [v], IsNormalType k, IsNormalType v) ⇒ HasGenHint (Map k v) Source # | |
Defined in Constrained.Spec.Map Methods giveHint ∷ Hint (Map k v) → Specification (Map k v) Source # | |
memberSpecList ∷ [a] → NonEmpty String → Specification a Source #
return a MemberSpec or ans ErrorSpec depending on if xs the null list or not
explainSpec ∷ [String] → Specification a → Specification a Source #
explainSpecOpt ∷ [String] → Specification a → Specification a Source #
equalSpec ∷ a → Specification a Source #
notEqualSpec ∷ ∀ a. HasSpec a ⇒ a → Specification a Source #
notMemberSpec ∷ ∀ a f. (HasSpec a, Foldable f) ⇒ f a → Specification a Source #
constrained ∷ ∀ a p. (IsPred p, HasSpec a) ⇒ (Term a → p) → Specification a Source #
isErrorLike ∷ ∀ a. Specification a → Bool Source #
errorLikeMessage ∷ ∀ a. Specification a → NonEmpty String Source #
fromGESpec ∷ HasCallStack ⇒ GE (Specification a) → Specification a Source #
addToErrorSpec ∷ NonEmpty String → Specification a → Specification a Source #
Add the explanations, if it's an ErrorSpec, else drop them
Constructors
| WithPrec Int a |
Instances
| HasSpec a ⇒ Pretty (WithPrec (Specification a)) Source # | |
Defined in Constrained.Base Methods pretty ∷ WithPrec (Specification a) → Doc ann Source # prettyList ∷ [WithPrec (Specification a)] → Doc ann Source # | |
| Show a ⇒ Pretty (WithPrec (Term a)) Source # | |
| (HasSpec (k, v), HasSpec k, HasSpec v, HasSpec [v]) ⇒ Pretty (WithPrec (MapSpec k v)) Source # | |
| HasSpec a ⇒ Pretty (WithPrec (FoldSpec a)) Source # | |
| HasSpec a ⇒ Pretty (WithPrec (ListSpec a)) Source # | |
ppList ∷ ∀ f as ann. All HasSpec as ⇒ (∀ a. HasSpec a ⇒ f a → Doc ann) → List f as → [Doc ann] Source #
prettyType ∷ ∀ t x. Typeable t ⇒ Doc x Source #
data Fun dom rng where Source #
Constructors
| Fun ∷ ∀ t dom rng. AppRequires t dom rng ⇒ t dom rng → Fun dom rng |
extractf ∷ ∀ t d r. LogicRequires t ⇒ Fun d r → Maybe (t d r) Source #
pattern FromGeneric ∷ ∀ rng. () ⇒ ∀ a. (rng ~ a, GenericRequires a, HasSpec a, AppRequires BaseW '[SimpleRep a] rng) ⇒ Term (SimpleRep a) → Term rng Source #
pattern ToGeneric ∷ ∀ rng. () ⇒ ∀ a. (rng ~ SimpleRep a, GenericRequires a, HasSpec a, AppRequires BaseW '[a] rng) ⇒ Term a → Term rng Source #