| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Constrained.Base
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
- newtype TypeSpecF a = TypeSpecF (TypeSpec a)
- newtype HintF a = HintF (Hint a)
- data Deps
- type Binder = BinderD Deps
- type AppRequires t as b = AppRequiresD Deps t as b
- type Pred = PredD Deps
- type Term = TermD Deps
- type Specification = SpecificationD Deps
- pattern TypeSpec ∷ () ⇒ HasSpec a ⇒ TypeSpec a → [a] → Specification a
- typeSpec ∷ HasSpec a ⇒ TypeSpec a → Specification a
- class (Typeable t, Semantics t, Syntax 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
- type GenericallyInstantiated a = (AssertComputes (SimpleRep a) (((Text "Trying to use a generic instantiation of " :<>: ShowType a) :<>: Text ", likely in a HasSpec instance.") :$$: Text "However, the type has no definition of SimpleRep, likely because of a missing instance of HasSimpleRep."), HasSimpleRep a, HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a))
- type TypeSpecEqShow a = (AssertComputes (TypeSpec a) ((Text "Can't compute " :<>: ShowType (TypeSpec a)) :$$: Text "Either because of a missing definition of TypeSpec or a missing instance of HasSimpleRep."), Show (TypeSpec a), Typeable (TypeSpec a))
- class (Typeable a, Eq a, Show a, TypeSpecEqShow 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, GenericallyInstantiated 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 ∷ GenericRequires a ⇒ Specification (SimpleRep a) → Specification a
- toSimpleRepSpec ∷ ∀ a. GenericRequires a ⇒ Specification a → Specification (SimpleRep a)
- data BinaryShow where
- BinaryShow ∷ ∀ a. String → [Doc a] → BinaryShow
- NonBinary ∷ BinaryShow
- 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
- bind ∷ (HasSpec a, IsPred p) ⇒ (Term a → p) → Binder a
- class Forallable t e | t → e where
- fromForAllSpec ∷ (HasSpec t, HasSpec e) ⇒ Specification e → Specification t
- forAllToList ∷ t → [e]
- 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 Fun dom rng where
- Fun ∷ ∀ t dom rng. AppRequires t dom rng ⇒ t dom rng → Fun dom rng
- extractf ∷ Typeable 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
- class (HasSpec a, Show (Hint a)) ⇒ HasGenHint a where
- type Hint a
- giveHint ∷ Hint a → Specification a
Documentation
Instances
type AppRequires t as b = AppRequiresD Deps t as b Source #
type Specification = SpecificationD Deps Source #
class (Typeable t, Semantics t, Syntax t) ⇒ Logic t 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.
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.
type GenericallyInstantiated a = (AssertComputes (SimpleRep a) (((Text "Trying to use a generic instantiation of " :<>: ShowType a) :<>: Text ", likely in a HasSpec instance.") :$$: Text "However, the type has no definition of SimpleRep, likely because of a missing instance of HasSimpleRep."), HasSimpleRep a, HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) Source #
type TypeSpecEqShow a = (AssertComputes (TypeSpec a) ((Text "Can't compute " :<>: ShowType (TypeSpec a)) :$$: Text "Either because of a missing definition of TypeSpec or a missing instance of HasSimpleRep."), Show (TypeSpec a), Typeable (TypeSpec a)) Source #
class (Typeable a, Eq a, Show a, TypeSpecEqShow 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 ∷ GenericallyInstantiated a ⇒ TypeSpec a Source #
combineSpec ∷ TypeSpec a → TypeSpec a → Specification a Source #
default combineSpec ∷ GenericallyInstantiated a ⇒ TypeSpec a → TypeSpec a → Specification a Source #
genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a Source #
Generate a value that satisfies the HasSpec.
The key property for this generator is soundness:
∀ a ∈ genFromTypeSpec spec. a conformsTo spec
default genFromTypeSpec ∷ (GenericallyInstantiated a, HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a Source #
conformsTo ∷ HasCallStack ⇒ a → TypeSpec a → Bool Source #
Check conformance to the spec.
default conformsTo ∷ (GenericallyInstantiated a, HasCallStack) ⇒ a → TypeSpec a → Bool Source #
shrinkWithTypeSpec ∷ TypeSpec a → a → [a] Source #
Shrink an a with the aide of a HasSpec
default shrinkWithTypeSpec ∷ GenericallyInstantiated 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)
cardinalTypeSpec ∷ TypeSpec a → Specification Integer Source #
Compute an upper and lower bound on the number of solutions genFromTypeSpec might return
default cardinalTypeSpec ∷ GenericallyInstantiated 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, GenericallyInstantiated 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
| Syntax BaseW Source # | |
| 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 # | |
| 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 ∷ GenericRequires a ⇒ Specification (SimpleRep a) → Specification a Source #
toSimpleRepSpec ∷ ∀ a. GenericRequires a ⇒ Specification a → Specification (SimpleRep a) Source #
data BinaryShow where Source #
Constructors
| BinaryShow ∷ ∀ a. String → [Doc a] → BinaryShow | |
| NonBinary ∷ BinaryShow |
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.
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 e, Forallable (SimpleRep t) e, GenericRequires t) ⇒ Specification e → Specification t Source #
forAllToList ∷ t → [e] Source #
default forAllToList ∷ (HasSimpleRep t, Forallable (SimpleRep t) e) ⇒ t → [e] Source #
Instances
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
data Fun dom rng where Source #
Constructors
| Fun ∷ ∀ t dom rng. AppRequires t dom rng ⇒ t dom rng → Fun dom rng |
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 #
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 # | |
| (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 # | |