| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Constrained.API.Extend
Synopsis
- data SpecificationD deps a where
- ExplainSpec ∷ [String] → SpecificationD deps a → SpecificationD deps a
- MemberSpec ∷ NonEmpty a → SpecificationD deps a
- ErrorSpec ∷ NonEmpty String → SpecificationD deps a
- SuspendedSpec ∷ HasSpecD deps a ⇒ Var a → PredD deps → SpecificationD deps a
- TypeSpecD ∷ HasSpecD deps a ⇒ TypeSpecD deps a → [a] → SpecificationD deps a
- TrueSpec ∷ SpecificationD deps a
- pattern TypeSpec ∷ () ⇒ HasSpec a ⇒ TypeSpec a → [a] → Specification a
- data PredD deps where
- ElemPred ∷ (HasSpecD deps a, Show a) ⇒ Bool → TermD deps a → NonEmpty a → PredD deps
- Monitor ∷ ((∀ a. TermD deps a → a) → Property → Property) → PredD deps
- And ∷ [PredD deps] → PredD deps
- Exists ∷ ((∀ b. TermD deps b → b) → GE a) → BinderD deps a → PredD deps
- Subst ∷ (HasSpecD deps a, Show a) ⇒ Var a → TermD deps a → PredD deps → PredD deps
- Let ∷ TermD deps a → BinderD deps a → PredD deps
- Assert ∷ TermD deps Bool → PredD deps
- Reifies ∷ (HasSpecD deps a, HasSpecD deps b, Show a, Show b) ⇒ TermD deps b → TermD deps a → (a → b) → PredD deps
- DependsOn ∷ (HasSpecD deps a, HasSpecD deps b, Show a, Show b) ⇒ TermD deps a → TermD deps b → PredD deps
- ForAll ∷ (ForallableD deps t e, HasSpecD deps t, HasSpecD deps e, Show t, Show e) ⇒ TermD deps t → BinderD deps e → PredD deps
- Case ∷ (HasSpecD deps (SumOver as), Show (SumOver as)) ⇒ TermD deps (SumOver as) → List (Weighted (BinderD deps)) as → PredD deps
- When ∷ TermD deps Bool → PredD deps → PredD deps
- GenHint ∷ (HasGenHintD deps a, Show a, Show (HintD deps a)) ⇒ HintD deps a → TermD deps a → PredD deps
- TruePred ∷ PredD deps
- FalsePred ∷ NonEmpty String → PredD deps
- Explain ∷ NonEmpty String → PredD deps → PredD deps
- data TermD deps a where
- data BinderD deps a where
- appTerm ∷ ∀ t ds r. AppRequires t ds r ⇒ t ds r → FunTy (MapList Term ds) (Term r)
- class Semantics (t ∷ [Type] → Type → Type) where
- class Syntax (t ∷ [Type] → Type → Type) where
- 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]
- data HOLE a b where
- 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)
- data PairSpec a b = Cartesian (Specification a) (Specification b)
- data MapSpec k v = MapSpec {
- mapSpecHint ∷ Maybe Integer
- mapSpecMustKeys ∷ Set k
- mapSpecMustValues ∷ [v]
- mapSpecSize ∷ Specification Integer
- mapSpecElem ∷ Specification (k, v)
- mapSpecFold ∷ FoldSpec v
- data SetSpec a = SetSpec (Set a) (Specification a) (Specification Integer)
- data NumSpec n = NumSpecInterval (Maybe n) (Maybe n)
- data TreeSpec a = TreeSpec {}
- module Constrained.API
Abstract syntax
data SpecificationD deps a where Source #
A `Specification a` denotes a set of as
Constructors
| ExplainSpec ∷ [String] → SpecificationD deps a → SpecificationD deps a | Explain a Specification |
| MemberSpec | Elements of a known set |
Fields
| |
| ErrorSpec ∷ NonEmpty String → SpecificationD deps a | The empty set |
| SuspendedSpec | The set described by some predicates over the bound variable. |
Fields
| |
| TypeSpecD | A type-specific spec |
Fields
| |
| TrueSpec ∷ SpecificationD deps a | Anything |
Instances
data PredD deps where Source #
Constructors
| ElemPred ∷ (HasSpecD deps a, Show a) ⇒ Bool → TermD deps a → NonEmpty a → PredD deps | |
| Monitor ∷ ((∀ a. TermD deps a → a) → Property → Property) → PredD deps | |
| And ∷ [PredD deps] → PredD deps | |
| Exists | |
| Subst ∷ (HasSpecD deps a, Show a) ⇒ Var a → TermD deps a → PredD deps → PredD deps | |
| Let ∷ TermD deps a → BinderD deps a → PredD deps | |
| Assert ∷ TermD deps Bool → PredD deps | |
| Reifies | |
| DependsOn ∷ (HasSpecD deps a, HasSpecD deps b, Show a, Show b) ⇒ TermD deps a → TermD deps b → PredD deps | |
| ForAll ∷ (ForallableD deps t e, HasSpecD deps t, HasSpecD deps e, Show t, Show e) ⇒ TermD deps t → BinderD deps e → PredD deps | |
| Case | |
| When ∷ TermD deps Bool → PredD deps → PredD deps | |
| GenHint ∷ (HasGenHintD deps a, Show a, Show (HintD deps a)) ⇒ HintD deps a → TermD deps a → PredD deps | |
| TruePred ∷ PredD deps | |
| FalsePred ∷ NonEmpty String → PredD deps | |
| Explain ∷ NonEmpty String → PredD deps → PredD deps | |
data TermD deps a where Source #
Constructors
| App ∷ AppRequiresD deps t dom rng ⇒ t dom rng → List (TermD deps) dom → TermD deps rng | |
| Lit ∷ (Typeable a, Eq a, Show a) ⇒ a → TermD deps a | |
| V ∷ (HasSpecD deps a, Typeable a) ⇒ Var a → TermD deps a |
Instances
| (Ord a, HasSpec a, HasSpec (Set a)) ⇒ Monoid (Term (Set a)) Source # | |
| (Ord a, HasSpec a, HasSpec (Set a)) ⇒ Semigroup (Term (Set a)) Source # | |
| NumLike a ⇒ Num (Term a) Source # | |
| IsPred (Term Bool) Source # | |
| Rename (Term a) Source # | |
| HasVariables (Term a) Source # | |
| Show a ⇒ Pretty (WithPrec (TermD deps a)) Source # | |
| Show a ⇒ Show (TermD deps a) Source # | |
| Eq (TermD deps a) Source # | |
| Show a ⇒ Pretty (TermD deps a) Source # | |
| HasVariables (List Term as) Source # | |
Implementing new functions
class 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
class Syntax (t ∷ [Type] → Type → Type) where Source #
Syntactic operations are ones that have to do with the structure and appearence of the type.
See DependencyInjection to better understand deps - it's a
pointer to postpone having to define HasSpec and friends here.
Minimal complete definition
Nothing
Methods
isInfix ∷ t dom rng → Bool Source #
prettySymbol ∷ ∀ deps dom rng ann. t dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Instances
The Logic instance
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
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)
Built-in HasSpecs
Constructors
| Cartesian (Specification a) (Specification b) |
Constructors
| MapSpec | |
Fields
| |
Instances
Constructors
| SetSpec (Set a) (Specification a) (Specification Integer) |
Constructors
| NumSpecInterval (Maybe n) (Maybe n) |
Instances
| (Arbitrary a, Ord a) ⇒ Arbitrary (NumSpec a) Source # | |
| Ord n ⇒ Monoid (NumSpec n) Source # | |
| Ord n ⇒ Semigroup (NumSpec n) Source # | |
| Num (NumSpec Integer) Source # | |
Defined in Constrained.NumOrd Methods (+) ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer # (-) ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer # (*) ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer # negate ∷ NumSpec Integer → NumSpec Integer # abs ∷ NumSpec Integer → NumSpec Integer # | |
| Show n ⇒ Show (NumSpec n) Source # | |
| Ord n ⇒ Eq (NumSpec n) Source # | |
Constructors
| TreeSpec | |
Fields | |
Re-export of API
module Constrained.API