Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Constrained.AbstractSyntax
Synopsis
- data TermD deps a where
- type AppRequiresD deps (t ∷ [Type] → Type → Type) dom rng = (LogicD deps t, Syntax t, Semantics t, TypeList dom, Eq (t dom rng), Show (t dom rng), Typeable t, All Typeable dom, Typeable dom, Typeable rng, All (HasSpecD deps) dom, All Show dom, HasSpecD deps rng, Show rng)
- runTermE ∷ ∀ a deps. Env → TermD deps a → Either (NonEmpty String) a
- runTerm ∷ MonadGenError m ⇒ Env → TermD deps a → m a
- fastInequality ∷ TermD deps a → TermD deps b → Bool
- class Syntax (t ∷ [Type] → Type → Type) where
- 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 BinderD deps a where
- 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 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
Documentation
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 # | |
type AppRequiresD deps (t ∷ [Type] → Type → Type) dom rng = (LogicD deps t, Syntax t, Semantics t, TypeList dom, Eq (t dom rng), Show (t dom rng), Typeable t, All Typeable dom, Typeable dom, Typeable rng, All (HasSpecD deps) dom, All Show dom, HasSpecD deps rng, Show rng) Source #
fastInequality ∷ TermD deps a → TermD deps b → Bool Source #
Sound but not complete inequality on terms
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
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 |
Instances
Foldable f ⇒ Foldable (Weighted f) Source # | |
Defined in Constrained.AbstractSyntax 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 # | |
Defined in Constrained.AbstractSyntax | |
Functor f ⇒ Functor (Weighted f) Source # | |
Rename (f a) ⇒ Rename (Weighted f a) Source # | |
HasVariables (f a) ⇒ HasVariables (Weighted f a) Source # | |
Pretty (f a) ⇒ Pretty (Weighted f a) Source # | |
HasVariables (List (Weighted Binder) as) 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 #
data SpecificationD deps a where Source #
A `Specification a` denotes a set of a
s
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 |