| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Minimal.Base
Synopsis
- 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
- applyFunSym ∷ ∀ t ds rng. (Typeable rng, Eq rng, Show rng, Semantics t) ⇒ FunTy ds rng → List Term ds → Maybe rng
- reducesToLit ∷ Term a → Maybe a
- sameTerms ∷ All HasSpec as ⇒ List Term as → List Term as → Bool
- class Syntax (t ∷ [Type] → Type → Type) where
- class Syntax t ⇒ Semantics (t ∷ [Type] → Type → Type) where
- class (Typeable t, Syntax t, Semantics t) ⇒ Logic (t ∷ [Type] → Type → Type) where
- propagateTypeSpec ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx as (HOLE a) → TypeSpec b → [b] → Spec a
- propagateMemberSpec ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx as (HOLE a) → NonEmpty b → Spec a
- propagate ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx as (HOLE a) → Spec b → Spec a
- data Pred where
- ElemPred ∷ ∀ a. HasSpec a ⇒ Bool → Term a → NonEmpty a → Pred
- And ∷ [Pred] → Pred
- Exists ∷ ((∀ b. Term b → b) → GE a) → Binder a → Pred
- ForAll ∷ (Container t a, HasSpec t, HasSpec a) ⇒ Term t → Binder a → Pred
- DependsOn ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Pred
- Assert ∷ Term Bool → Pred
- TruePred ∷ Pred
- FalsePred ∷ NonEmpty String → Pred
- Case ∷ HasSpec (Either a b) ⇒ Term (Either a b) → Binder a → Binder b → Pred
- Let ∷ Term a → Binder a → Pred
- Subst ∷ HasSpec a ⇒ Var a → Term a → Pred → Pred
- data Binder a where
- class Container t e | t → e where
- fromForAllSpec ∷ (HasSpec t, HasSpec e) ⇒ Spec e → Spec t
- forAllToList ∷ t → [e]
- data Binders as where
- data Bind a where
- toBind ∷ All HasSpec as ⇒ List Term as → List Var as → List Bind as
- data Spec a where
- typeSpec ∷ HasSpec a ⇒ TypeSpec a → Spec a
- constrained ∷ ∀ a. HasSpec a ⇒ (Term a → Pred) → Spec a
- bind ∷ HasSpec a ⇒ (Term a → Pred) → Binder a
- class (Typeable a, Eq a, Show a, Show (TypeSpec a), Typeable (TypeSpec a)) ⇒ HasSpec a where
- type TypeSpec a
- anySpec ∷ TypeSpec a
- combineSpec ∷ TypeSpec a → TypeSpec a → Spec a
- genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a
- conformsTo ∷ HasCallStack ⇒ a → TypeSpec a → Bool
- toPreds ∷ Term a → TypeSpec a → Pred
- guardTypeSpec ∷ TypeSpec a → Spec a
- data HOLE a b where
- data ListCtx (as ∷ [Type]) (c ∷ Type → Type) where
- data Ctx v (a ∷ Type) where
- ctxHasSpec ∷ Ctx v a → Evidence (HasSpec a)
- fromListCtx ∷ All HasSpec as ⇒ ListCtx as (HOLE a) → Term a → List Term as
- propagateSpec ∷ ∀ v a. HasSpec v ⇒ Ctx v a → Spec a → Spec v
- 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) ⇒ String → Var v → List Term as → m (ListCtx as (Ctx v))
- 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
Documentation
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 #
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 |
applyFunSym ∷ ∀ t ds rng. (Typeable rng, Eq rng, Show rng, Semantics t) ⇒ FunTy ds rng → List Term ds → Maybe rng Source #
If the list is composed solely of literals, apply the function to get a value
reducesToLit ∷ Term a → Maybe a Source #
class Syntax (t ∷ [Type] → Type → Type) where Source #
Syntactic operations are ones that have to do with the structure and appearence of the type.
Minimal complete definition
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, or to apply meaning preserving rewrite rules.
Minimal complete definition
Methods
semantics ∷ ∀ d r. t d r → FunTy d r Source #
rewriteRules ∷ ∀ ds rng. (TypeList ds, Typeable ds, HasSpec rng, All HasSpec ds) ⇒ t ds rng → List Term ds → Evidence (Typeable rng, Eq rng, Show rng) → Maybe (Term rng) Source #
class (Typeable t, Syntax t, Semantics t) ⇒ Logic (t ∷ [Type] → Type → Type) where Source #
Logical operations are one that support reasoning about how a function symbol relates to logical properties, that we call Spec's
Minimal complete definition
Methods
propagateTypeSpec ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx as (HOLE a) → TypeSpec b → [b] → Spec a Source #
propagateMemberSpec ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx as (HOLE a) → NonEmpty b → Spec a Source #
propagate ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx as (HOLE a) → Spec b → Spec a Source #
Instances
Constructors
| ElemPred ∷ ∀ a. HasSpec a ⇒ Bool → Term a → NonEmpty a → Pred | |
| And ∷ [Pred] → Pred | |
| Exists ∷ ((∀ b. Term b → b) → GE a) → Binder a → Pred | |
| ForAll ∷ (Container t a, HasSpec t, HasSpec a) ⇒ Term t → Binder a → Pred | |
| DependsOn ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Pred | |
| Assert ∷ Term Bool → Pred | |
| TruePred ∷ Pred | |
| FalsePred ∷ NonEmpty String → Pred | |
| Case ∷ HasSpec (Either a b) ⇒ Term (Either a b) → Binder a → Binder b → Pred | |
| Let ∷ Term a → Binder a → Pred | |
| Subst ∷ HasSpec a ⇒ Var a → Term a → Pred → Pred |
class Container t e | t → e where Source #
Methods
fromForAllSpec ∷ (HasSpec t, HasSpec e) ⇒ Spec e → Spec t Source #
forAllToList ∷ t → [e] Source #
Constructors
| TrueSpec ∷ Spec a | |
| ErrorSpec ∷ NonEmpty String → Spec a | |
| SuspendedSpec ∷ HasSpec a ⇒ Var a → Pred → Spec a | |
| MemberSpec ∷ NonEmpty a → Spec a | |
| TypeSpec ∷ HasSpec a ⇒ TypeSpec a → [a] → Spec a |
class (Typeable a, Eq a, Show a, Show (TypeSpec a), Typeable (TypeSpec a)) ⇒ HasSpec a where Source #
Minimal complete definition
Methods
combineSpec ∷ TypeSpec a → TypeSpec a → Spec a Source #
genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a Source #
Generate a value that satisfies the Spec.
The key property for this generator is soundness:
∀ a ∈ genFromTypeSpec spec. a conformsTo spec
conformsTo ∷ HasCallStack ⇒ a → TypeSpec a → Bool Source #
Check conformance to the spec.
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)
guardTypeSpec ∷ TypeSpec a → Spec a Source #
This is used to detect self inconsistencies in a (TypeSpec t) guardTypeSpec message ty --> ErrorSpec message, if ty is inconsistent
Instances
data ListCtx (as ∷ [Type]) (c ∷ Type → Type) where Source #
Note the arrows (n :|> hole) and (hole :<| n) always point towards the term with
type `(c x)`, (i.e. hole in the picture above) where the target variable must occur.
fromListCtx ∷ All HasSpec as ⇒ ListCtx 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.
Hole becomes t, values become Lit .
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) ⇒ String → Var v → List Term as → m (ListCtx as (Ctx v)) 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 #