| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Constrained.Spec.SumProd
Contents
Synopsis
- type IsNormalType a = (AssertComputes (Cases a) (Text "Failed to compute Cases in a use of IsNormalType for " :$$: (ShowType a :<>: Text ", are you missing an IsNormalType constraint?")), Cases a ~ '[a], AssertComputes (Args a) ((Text "Failed to compute Args in a use of IsNormalType for " :<>: ShowType a) :<>: Text ", are you missing an IsNormalType constraint?"), Args a ~ '[a], IsProd a, CountCases a ~ 1)
- type ProdAsListComputes a = AssertSpineComputes (Text "Have you considered adding an IsNormalType or ProdAsListComputes constraint?") (ProductAsList a)
- caseOn ∷ ∀ a. (GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) ⇒ Term a → FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
- branch ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ FunTy (MapList Term (Args a)) p → Weighted Binder a
- branchW ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ Int → FunTy (MapList Term (Args a)) p → Weighted Binder a
- forAll' ∷ ∀ t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t, HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a), IsProductType a, HasSpec a, GenericRequires a, ProdAsListComputes a) ⇒ Term t → FunTy (MapList Term (ProductAsList a)) p → Pred
- constrained' ∷ ∀ a p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p, GenericRequires a, ProdAsListComputes a) ⇒ FunTy (MapList Term (ProductAsList a)) p → Specification a
- reify' ∷ ∀ a b p. (Cases (SimpleRep b) ~ '[SimpleRep b], TypeSpec b ~ TypeSpec (SimpleRep b), HasSpec (SimpleRep b), HasSimpleRep b, All HasSpec (Args (SimpleRep b)), IsProd (SimpleRep b), HasSpec a, HasSpec b, IsProductType b, IsProd a, IsPred p, GenericRequires b, ProdAsListComputes b) ⇒ Term a → (a → b) → FunTy (MapList Term (ProductAsList b)) p → Pred
- con ∷ ∀ c a r. (SimpleRep a ~ SOP (TheSop a), TypeSpec a ~ TypeSpec (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a), ResultType r ~ Term a, SOPTerm c (TheSop a), ConstrTerm (ConstrOf c (TheSop a)), GenericRequires a) ⇒ r
- onCon ∷ ∀ c a p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All HasSpec (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term a → FunTy (MapList Term (ConstrOf c (TheSop a))) p → Pred
- isCon ∷ ∀ c a. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), GenericRequires a) ⇒ Term a → Pred
- sel ∷ ∀ n a c as. (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a, HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) ⇒ Term a → Term (At n as)
- match ∷ ∀ p a. (IsProductType a, IsPred p, GenericRequires a, ProdAsListComputes a) ⇒ Term a → FunTy (MapList Term (ProductAsList a)) p → Pred
- onJust ∷ ∀ a p. (HasSpec a, IsNormalType a, IsPred p) ⇒ Term (Maybe a) → (Term a → p) → Pred
- isJust ∷ ∀ a. (HasSpec a, IsNormalType a) ⇒ Term (Maybe a) → Pred
- chooseSpec ∷ HasSpec a ⇒ (Int, Specification a) → (Int, Specification a) → Specification a
- left_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term (Either a b)
- right_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term b → Term (Either a b)
- cJust_ ∷ (HasSpec a, IsNormalType a) ⇒ Term a → Term (Maybe a)
- cNothing_ ∷ (HasSpec a, IsNormalType a) ⇒ Term (Maybe a)
- fst_ ∷ (HasSpec x, HasSpec y) ⇒ Term (x, y) → Term x
- snd_ ∷ (HasSpec x, HasSpec y) ⇒ Term (x, y) → Term y
- fstW ∷ (HasSpec a, HasSpec b) ⇒ FunW '[(a, b)] a
- sndW ∷ (HasSpec a, HasSpec b) ⇒ FunW '[(a, b)] b
- pair_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term b → Term (a, b)
- injLeft_ ∷ (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Term a → Term (Sum a b)
- injRight_ ∷ (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Term b → Term (Sum a b)
- prodFst_ ∷ (HasSpec a, HasSpec b) ⇒ Term (Prod a b) → Term a
- prodSnd_ ∷ (HasSpec a, HasSpec b) ⇒ Term (Prod a b) → Term b
- prod_ ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Term (Prod a b)
- data PairSpec a b = Cartesian (Specification a) (Specification b)
- data SumW dom rng where
Documentation
type IsNormalType a = (AssertComputes (Cases a) (Text "Failed to compute Cases in a use of IsNormalType for " :$$: (ShowType a :<>: Text ", are you missing an IsNormalType constraint?")), Cases a ~ '[a], AssertComputes (Args a) ((Text "Failed to compute Args in a use of IsNormalType for " :<>: ShowType a) :<>: Text ", are you missing an IsNormalType constraint?"), Args a ~ '[a], IsProd a, CountCases a ~ 1) Source #
type ProdAsListComputes a = AssertSpineComputes (Text "Have you considered adding an IsNormalType or ProdAsListComputes constraint?") (ProductAsList a) Source #
ProdAsListComputes is here to make sure that in situations like this:
type family Foobar k ex :: HasSpec (Foobar k) => Specification (Int, Foobar k) ex = constrained $ \ p -> match p $ \ i _ -> (i ==. 10)
Where you're trying to work with an unevaluated type family in constraints.
You get reasonable type errors prompting you to add the IsNormalType (Foobar k) constraint
like this:
• Type list computation is stuck on
Args (Foobar k)
Have you considered adding an IsNormalType or ProdAsListComputes constraint?
• In the first argument of ‘($)’, namely ‘match p’
In the expression: match p $ \ i _ -> (i ==. 10)
In the second argument of ‘($)’, namely
‘\ p -> match p $ \ i _ -> (i ==. 10)’
|
503 | ex = constrained $ \ p -> match p $ \ i _ -> (i ==. 10)
| ^^^^^Which should help you come to the conclusion that you need to do something like this for everything to compile:
ex :: (HasSpec (Foobar k), IsNormalType (Foobar k)) => Specification (Int, Foobar k)
caseOn ∷ ∀ a. (GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) ⇒ Term a → FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred Source #
branch ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ FunTy (MapList Term (Args a)) p → Weighted Binder a Source #
branchW ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ Int → FunTy (MapList Term (Args a)) p → Weighted Binder a Source #
forAll' ∷ ∀ t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t, HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a), IsProductType a, HasSpec a, GenericRequires a, ProdAsListComputes a) ⇒ Term t → FunTy (MapList Term (ProductAsList a)) p → Pred Source #
Like forAll but pattern matches on the `Term a`
constrained' ∷ ∀ a p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p, GenericRequires a, ProdAsListComputes a) ⇒ FunTy (MapList Term (ProductAsList a)) p → Specification a Source #
Like constrained but pattern matches on the bound `Term a`
reify' ∷ ∀ a b p. (Cases (SimpleRep b) ~ '[SimpleRep b], TypeSpec b ~ TypeSpec (SimpleRep b), HasSpec (SimpleRep b), HasSimpleRep b, All HasSpec (Args (SimpleRep b)), IsProd (SimpleRep b), HasSpec a, HasSpec b, IsProductType b, IsProd a, IsPred p, GenericRequires b, ProdAsListComputes b) ⇒ Term a → (a → b) → FunTy (MapList Term (ProductAsList b)) p → Pred Source #
Like reify but pattern matches on the bound `Term b`
con ∷ ∀ c a r. (SimpleRep a ~ SOP (TheSop a), TypeSpec a ~ TypeSpec (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a), ResultType r ~ Term a, SOPTerm c (TheSop a), ConstrTerm (ConstrOf c (TheSop a)), GenericRequires a) ⇒ r Source #
onCon ∷ ∀ c a p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All HasSpec (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term a → FunTy (MapList Term (ConstrOf c (TheSop a))) p → Pred Source #
isCon ∷ ∀ c a. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), GenericRequires a) ⇒ Term a → Pred Source #
sel ∷ ∀ n a c as. (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a, HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) ⇒ Term a → Term (At n as) Source #
match ∷ ∀ p a. (IsProductType a, IsPred p, GenericRequires a, ProdAsListComputes a) ⇒ Term a → FunTy (MapList Term (ProductAsList a)) p → Pred Source #
onJust ∷ ∀ a p. (HasSpec a, IsNormalType a, IsPred p) ⇒ Term (Maybe a) → (Term a → p) → Pred Source #
chooseSpec ∷ HasSpec a ⇒ (Int, Specification a) → (Int, Specification a) → Specification a Source #
ChooseSpec is one of the ways we can Or two Specs together
This works for any kind of type that has a HasSpec instance.
If your type is a Sum type. One can use CaseOn which is much easier.
left_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term (Either a b) Source #
right_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term b → Term (Either a b) Source #
pair_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term b → Term (a, b) Source #
Constructors
| Cartesian (Specification a) (Specification b) |
data SumW dom rng where Source #
Instances
| Syntax SumW Source # | |
| Logic SumW Source # | |
Defined in Constrained.TheKnot Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SumW as b, HasSpec a) ⇒ SumW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SumW as b, HasSpec a) ⇒ SumW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires SumW as b, HasSpec a) ⇒ SumW 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) ⇒ SumW dom rng → List Term dom → Evidence (AppRequires SumW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ SumW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). SumW dom Bool → List Term dom → [Pred] Source # | |
| Semantics SumW Source # | |
| Show (SumW dom rng) Source # | |
| Eq (SumW dom rng) Source # | |