Safe Haskell	Safe-Inferred
Language	Haskell2010

Constrained.Generic

Description

How can we automatically inject normal Haskell types into the logic, using GHC.Generics

Synopsis

data Prod a b = Prod {
- prodFst ∷ a
- prodSnd ∷ b
}
type family ProdOver as where ...
listToProd ∷ (ProdOver as → r) → List Identity as → r
prodToList ∷ ∀ as. TypeList as ⇒ ProdOver as → List Identity as
appendProd ∷ ∀ xs ys. (TypeList xs, TypeList ys) ⇒ ProdOver xs → ProdOver ys → ProdOver (Append xs ys)
splitProd ∷ ∀ xs ys. (TypeList xs, TypeList ys) ⇒ ProdOver (Append xs ys) → Prod (ProdOver xs) (ProdOver ys)
data Sum a b
- = SumLeft a
- | SumRight b
type family SumOver as where ...
class Typeable (SimpleRep a) ⇒ HasSimpleRep a where
- type SimpleRep a
- type TheSop a ∷ [Type]
- toSimpleRep ∷ a → SimpleRep a
- fromSimpleRep ∷ SimpleRep a → a
type family SimplifyRep f where ...
class SimpleGeneric rep where
- toSimpleRep' ∷ rep p → SimplifyRep rep
- fromSimpleRep' ∷ SimplifyRep rep → rep p
data (c ∷ Symbol) ::: (ts ∷ [Type])
type family SOPOf f where ...
type family Constr f where ...
type family SOP constrs where ...
type family ConstrOf c sop where ...
class Inject c constrs r where
- inject' ∷ (SOP constrs → r) → FunTy (ConstrOf c constrs) r
inject ∷ ∀ c constrs. Inject c constrs (SOP constrs) ⇒ FunTy (ConstrOf c constrs) (SOP constrs)
type family ALG constrs r where ...
class SOPLike constrs r where
- algebra ∷ SOP constrs → ALG constrs r
- consts ∷ r → ALG constrs r
class SimpleConstructor rep where
- toSimpleCon' ∷ rep p → ProdOver (Constr rep)
- fromSimpleCon' ∷ ProdOver (Constr rep) → rep p
class SopList xs ys where
- injectSOPLeft ∷ SOP xs → SOP (Append xs ys)
- injectSOPRight ∷ SOP ys → SOP (Append xs ys)
- caseSOP ∷ SOP (Append xs ys) → Sum (SOP xs) (SOP ys)

Documentation

data Prod a b Source #

Constructors

Prod
Fields prodFst ∷ a prodSnd ∷ b

Instances

Instances details

(HasSpec a, HasSpec b) ⇒ Logic "prodFst_" BaseW '[Prod a b] a Source #
Instance details Defined in Constrained.TheKnot Methods info ∷ BaseW "prodFst_" '[Prod a b] a → String Source # propagate ∷ Context "prodFst_" BaseW '[Prod a b] a hole → Specification a → Specification hole Source # rewriteRules ∷ BaseW "prodFst_" '[Prod a b] a → List Term '[Prod a b] → Evidence (AppRequires "prodFst_" BaseW '[Prod a b] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[Prod a b] ~ '[a0], a ~ b0, HasSpec a0, HasSpec b0) ⇒ BaseW "prodFst_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ BaseW "prodFst_" '[Prod a b] Bool → List Term '[Prod a b] → [Pred] Source #
(HasSpec a, HasSpec b) ⇒ Logic "prodSnd_" BaseW '[Prod a b] b Source #
Instance details Defined in Constrained.TheKnot Methods info ∷ BaseW "prodSnd_" '[Prod a b] b → String Source # propagate ∷ Context "prodSnd_" BaseW '[Prod a b] b hole → Specification b → Specification hole Source # rewriteRules ∷ BaseW "prodSnd_" '[Prod a b] b → List Term '[Prod a b] → Evidence (AppRequires "prodSnd_" BaseW '[Prod a b] b) → Maybe (Term b) Source # mapTypeSpec ∷ ('[Prod a b] ~ '[a0], b ~ b0, HasSpec a0, HasSpec b0) ⇒ BaseW "prodSnd_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ BaseW "prodSnd_" '[Prod a b] Bool → List Term '[Prod a b] → [Pred] Source #
(HasSpec a, HasSpec b) ⇒ Logic "prod_" BaseW '[a, b] (Prod a b) Source #
Instance details Defined in Constrained.TheKnot Methods info ∷ BaseW "prod_" '[a, b] (Prod a b) → String Source # propagate ∷ Context "prod_" BaseW '[a, b] (Prod a b) hole → Specification (Prod a b) → Specification hole Source # rewriteRules ∷ BaseW "prod_" '[a, b] (Prod a b) → List Term '[a, b] → Evidence (AppRequires "prod_" BaseW '[a, b] (Prod a b)) → Maybe (Term (Prod a b)) Source # mapTypeSpec ∷ ('[a, b] ~ '[a0], Prod a b ~ b0, HasSpec a0, HasSpec b0) ⇒ BaseW "prod_" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ BaseW "prod_" '[a, b] Bool → List Term '[a, b] → [Pred] Source #
(Show a, Show b) ⇒ Show (Prod a b) Source #
Instance details Defined in Constrained.Generic Methods showsPrec ∷ Int → Prod a b → ShowS show ∷ Prod a b → String showList ∷ [Prod a b] → ShowS
(HasSpec a, HasSpec b) ⇒ HasSpec (Prod a b) Source #
Instance details Defined in Constrained.TheKnot Associated Types type TypeSpec (Prod a b) Source # type Prerequisites (Prod a b) Source # Methods emptySpec ∷ TypeSpec (Prod a b) Source # combineSpec ∷ TypeSpec (Prod a b) → TypeSpec (Prod a b) → Specification (Prod a b) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (Prod a b) → GenT m (Prod a b) Source # conformsTo ∷ Prod a b → TypeSpec (Prod a b) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (Prod a b) → Prod a b → [Prod a b] Source # toPreds ∷ Term (Prod a b) → TypeSpec (Prod a b) → Pred Source # cardinalTypeSpec ∷ TypeSpec (Prod a b) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (Prod a b) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (Prod a b) → BinaryShow Source # monadConformsTo ∷ Prod a b → TypeSpec (Prod a b) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (Prod a b) → [Prod a b] → Specification (Prod a b) Source # guardTypeSpec ∷ [String] → TypeSpec (Prod a b) → Specification (Prod a b) Source # prerequisites ∷ Evidence (Prerequisites (Prod a b)) Source #
(Eq a, Eq b) ⇒ Eq (Prod a b) Source #
Instance details Defined in Constrained.Generic Methods (==) ∷ Prod a b → Prod a b → Bool (/=) ∷ Prod a b → Prod a b → Bool
(Ord a, Ord b) ⇒ Ord (Prod a b) Source #
Instance details Defined in Constrained.Generic Methods compare ∷ Prod a b → Prod a b → Ordering (<) ∷ Prod a b → Prod a b → Bool (<=) ∷ Prod a b → Prod a b → Bool (>) ∷ Prod a b → Prod a b → Bool (>=) ∷ Prod a b → Prod a b → Bool max ∷ Prod a b → Prod a b → Prod a b min ∷ Prod a b → Prod a b → Prod a b
type Prerequisites (Prod a b) Source #
Instance details Defined in Constrained.TheKnot type Prerequisites (Prod a b) = (HasSpec a, HasSpec b)
type TypeSpec (Prod a b) Source #
Instance details Defined in Constrained.TheKnot type TypeSpec (Prod a b) = PairSpec a b

type family ProdOver as where ... Source #

Equations

ProdOver '[] = ()
ProdOver '[a] = a
ProdOver (a ': as) = Prod a (ProdOver as)

listToProd ∷ (ProdOver as → r) → List Identity as → r Source #

prodToList ∷ ∀ as. TypeList as ⇒ ProdOver as → List Identity as Source #

appendProd ∷ ∀ xs ys. (TypeList xs, TypeList ys) ⇒ ProdOver xs → ProdOver ys → ProdOver (Append xs ys) Source #

splitProd ∷ ∀ xs ys. (TypeList xs, TypeList ys) ⇒ ProdOver (Append xs ys) → Prod (ProdOver xs) (ProdOver ys) Source #

data Sum a b Source #

Generic way to represent Sums

Constructors

SumLeft a
SumRight b

Instances

Instances details

(HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Logic "leftFn" BaseW '[a] (Sum a b) Source #
Instance details Defined in Constrained.Spec.SumProd Methods info ∷ BaseW "leftFn" '[a] (Sum a b) → String Source # propagate ∷ Context "leftFn" BaseW '[a] (Sum a b) hole → Specification (Sum a b) → Specification hole Source # rewriteRules ∷ BaseW "leftFn" '[a] (Sum a b) → List Term '[a] → Evidence (AppRequires "leftFn" BaseW '[a] (Sum a b)) → Maybe (Term (Sum a b)) Source # mapTypeSpec ∷ ('[a] ~ '[a0], Sum a b ~ b0, HasSpec a0, HasSpec b0) ⇒ BaseW "leftFn" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ BaseW "leftFn" '[a] Bool → List Term '[a] → [Pred] Source #
(HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Logic "rightFn" BaseW '[b] (Sum a b) Source #
Instance details Defined in Constrained.Spec.SumProd Methods info ∷ BaseW "rightFn" '[b] (Sum a b) → String Source # propagate ∷ Context "rightFn" BaseW '[b] (Sum a b) hole → Specification (Sum a b) → Specification hole Source # rewriteRules ∷ BaseW "rightFn" '[b] (Sum a b) → List Term '[b] → Evidence (AppRequires "rightFn" BaseW '[b] (Sum a b)) → Maybe (Term (Sum a b)) Source # mapTypeSpec ∷ ('[b] ~ '[a0], Sum a b ~ b0, HasSpec a0, HasSpec b0) ⇒ BaseW "rightFn" '[a0] b0 → TypeSpec a0 → Specification b0 Source # saturate ∷ BaseW "rightFn" '[b] Bool → List Term '[b] → [Pred] Source #
(Show a, Show b) ⇒ Show (Sum a b) Source #
Instance details Defined in Constrained.Generic Methods showsPrec ∷ Int → Sum a b → ShowS show ∷ Sum a b → String showList ∷ [Sum a b] → ShowS
(HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ HasSpec (Sum a b) Source #	The HasSpec Sum instance
Instance details Defined in Constrained.TheKnot Associated Types type TypeSpec (Sum a b) Source # type Prerequisites (Sum a b) Source # Methods emptySpec ∷ TypeSpec (Sum a b) Source # combineSpec ∷ TypeSpec (Sum a b) → TypeSpec (Sum a b) → Specification (Sum a b) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec (Sum a b) → GenT m (Sum a b) Source # conformsTo ∷ Sum a b → TypeSpec (Sum a b) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec (Sum a b) → Sum a b → [Sum a b] Source # toPreds ∷ Term (Sum a b) → TypeSpec (Sum a b) → Pred Source # cardinalTypeSpec ∷ TypeSpec (Sum a b) → Specification Integer Source # cardinalTrueSpec ∷ Specification Integer Source # typeSpecHasError ∷ TypeSpec (Sum a b) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec (Sum a b) → BinaryShow Source # monadConformsTo ∷ Sum a b → TypeSpec (Sum a b) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec (Sum a b) → [Sum a b] → Specification (Sum a b) Source # guardTypeSpec ∷ [String] → TypeSpec (Sum a b) → Specification (Sum a b) Source # prerequisites ∷ Evidence (Prerequisites (Sum a b)) Source #
(Eq a, Eq b) ⇒ Eq (Sum a b) Source #
Instance details Defined in Constrained.Generic Methods (==) ∷ Sum a b → Sum a b → Bool (/=) ∷ Sum a b → Sum a b → Bool
(Ord a, Ord b) ⇒ Ord (Sum a b) Source #
Instance details Defined in Constrained.Generic Methods compare ∷ Sum a b → Sum a b → Ordering (<) ∷ Sum a b → Sum a b → Bool (<=) ∷ Sum a b → Sum a b → Bool (>) ∷ Sum a b → Sum a b → Bool (>=) ∷ Sum a b → Sum a b → Bool max ∷ Sum a b → Sum a b → Sum a b min ∷ Sum a b → Sum a b → Sum a b
type Prerequisites (Sum a b) Source #
Instance details Defined in Constrained.TheKnot type Prerequisites (Sum a b) = (HasSpec a, HasSpec b)
type TypeSpec (Sum a b) Source #
Instance details Defined in Constrained.TheKnot type TypeSpec (Sum a b) = SumSpec a b

type family SumOver as where ... Source #

Equations

SumOver '[a] = a
SumOver (a ': as) = Sum a (SumOver as)

class Typeable (SimpleRep a) ⇒ HasSimpleRep a where Source #

Minimal complete definition

Nothing

Associated Types

type SimpleRep a Source #

type SimpleRep a = SOP (TheSop a)

type TheSop a ∷ [Type] Source #

type TheSop a = SOPOf (Rep a)

Methods

toSimpleRep ∷ a → SimpleRep a Source #

default toSimpleRep ∷ (Generic a, SimpleGeneric (Rep a), SimpleRep a ~ SimplifyRep (Rep a)) ⇒ a → SimpleRep a Source #

fromSimpleRep ∷ SimpleRep a → a Source #

default fromSimpleRep ∷ (Generic a, SimpleGeneric (Rep a), SimpleRep a ~ SimplifyRep (Rep a)) ⇒ SimpleRep a → a Source #

Instances

Instances details

HasSimpleRep Foo Source #
Instance details Defined in Constrained.Examples.Basic Associated Types type SimpleRep Foo Source # type TheSop Foo ∷ [Type] Source # Methods toSimpleRep ∷ Foo → SimpleRep Foo Source # fromSimpleRep ∷ SimpleRep Foo → Foo Source #
HasSimpleRep Three Source #
Instance details Defined in Constrained.Examples.Basic Associated Types type SimpleRep Three Source # type TheSop Three ∷ [Type] Source # Methods toSimpleRep ∷ Three → SimpleRep Three Source # fromSimpleRep ∷ SimpleRep Three → Three Source #
HasSimpleRep FooBarBaz Source #
Instance details Defined in Constrained.Examples.CheatSheet Associated Types type SimpleRep FooBarBaz Source # type TheSop FooBarBaz ∷ [Type] Source # Methods toSimpleRep ∷ FooBarBaz → SimpleRep FooBarBaz Source # fromSimpleRep ∷ SimpleRep FooBarBaz → FooBarBaz Source #
HasSimpleRep () Source #
Instance details Defined in Constrained.Base Associated Types type SimpleRep () Source # type TheSop () ∷ [Type] Source # Methods toSimpleRep ∷ () → SimpleRep () Source # fromSimpleRep ∷ SimpleRep () → () Source #
HasSimpleRep Bool Source #
Instance details Defined in Constrained.TheKnot Associated Types type SimpleRep Bool Source # type TheSop Bool ∷ [Type] Source # Methods toSimpleRep ∷ Bool → SimpleRep Bool Source # fromSimpleRep ∷ SimpleRep Bool → Bool Source #
(Typeable a, Ord a) ⇒ HasSimpleRep (NotASet a) Source #
Instance details Defined in Constrained.Examples.Set Associated Types type SimpleRep (NotASet a) Source # type TheSop (NotASet a) ∷ [Type] Source # Methods toSimpleRep ∷ NotASet a → SimpleRep (NotASet a) Source # fromSimpleRep ∷ SimpleRep (NotASet a) → NotASet a Source #
Typeable a ⇒ HasSimpleRep (Maybe a) Source #
Instance details Defined in Constrained.Spec.SumProd Associated Types type SimpleRep (Maybe a) Source # type TheSop (Maybe a) ∷ [Type] Source # Methods toSimpleRep ∷ Maybe a → SimpleRep (Maybe a) Source # fromSimpleRep ∷ SimpleRep (Maybe a) → Maybe a Source #
(Typeable a, Typeable b) ⇒ HasSimpleRep (Either a b) Source #
Instance details Defined in Constrained.Spec.SumProd Associated Types type SimpleRep (Either a b) Source # type TheSop (Either a b) ∷ [Type] Source # Methods toSimpleRep ∷ Either a b → SimpleRep (Either a b) Source # fromSimpleRep ∷ SimpleRep (Either a b) → Either a b Source #
(Typeable a, Typeable b) ⇒ HasSimpleRep (a, b) Source #
Instance details Defined in Constrained.Spec.SumProd Associated Types type SimpleRep (a, b) Source # type TheSop (a, b) ∷ [Type] Source # Methods toSimpleRep ∷ (a, b) → SimpleRep (a, b) Source # fromSimpleRep ∷ SimpleRep (a, b) → (a, b) Source #
(Typeable a, Typeable b, Typeable c) ⇒ HasSimpleRep (a, b, c) Source #
Instance details Defined in Constrained.Spec.SumProd Associated Types type SimpleRep (a, b, c) Source # type TheSop (a, b, c) ∷ [Type] Source # Methods toSimpleRep ∷ (a, b, c) → SimpleRep (a, b, c) Source # fromSimpleRep ∷ SimpleRep (a, b, c) → (a, b, c) Source #
(Typeable a, Typeable b, Typeable c, Typeable d) ⇒ HasSimpleRep (a, b, c, d) Source #
Instance details Defined in Constrained.Spec.SumProd Associated Types type SimpleRep (a, b, c, d) Source # type TheSop (a, b, c, d) ∷ [Type] Source # Methods toSimpleRep ∷ (a, b, c, d) → SimpleRep (a, b, c, d) Source # fromSimpleRep ∷ SimpleRep (a, b, c, d) → (a, b, c, d) Source #
(Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) ⇒ HasSimpleRep (a, b, c, d, e) Source #
Instance details Defined in Constrained.Spec.SumProd Associated Types type SimpleRep (a, b, c, d, e) Source # type TheSop (a, b, c, d, e) ∷ [Type] Source # Methods toSimpleRep ∷ (a, b, c, d, e) → SimpleRep (a, b, c, d, e) Source # fromSimpleRep ∷ SimpleRep (a, b, c, d, e) → (a, b, c, d, e) Source #
(Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable g) ⇒ HasSimpleRep (a, b, c, d, e, g) Source #
Instance details Defined in Constrained.Spec.SumProd Associated Types type SimpleRep (a, b, c, d, e, g) Source # type TheSop (a, b, c, d, e, g) ∷ [Type] Source # Methods toSimpleRep ∷ (a, b, c, d, e, g) → SimpleRep (a, b, c, d, e, g) Source # fromSimpleRep ∷ SimpleRep (a, b, c, d, e, g) → (a, b, c, d, e, g) Source #
(Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable g, Typeable h) ⇒ HasSimpleRep (a, b, c, d, e, g, h) Source #
Instance details Defined in Constrained.Spec.SumProd Associated Types type SimpleRep (a, b, c, d, e, g, h) Source # type TheSop (a, b, c, d, e, g, h) ∷ [Type] Source # Methods toSimpleRep ∷ (a, b, c, d, e, g, h) → SimpleRep (a, b, c, d, e, g, h) Source # fromSimpleRep ∷ SimpleRep (a, b, c, d, e, g, h) → (a, b, c, d, e, g, h) Source #

type family SimplifyRep f where ... Source #

Equations

SimplifyRep f = SOP (SOPOf f)

class SimpleGeneric rep where Source #

Methods

toSimpleRep' ∷ rep p → SimplifyRep rep Source #

fromSimpleRep' ∷ SimplifyRep rep → rep p Source #

Instances

Instances details

(SimpleGeneric f, SimpleGeneric g, SopList (SOPOf f) (SOPOf g)) ⇒ SimpleGeneric (f :+: g) Source #
Instance details Defined in Constrained.Generic Methods toSimpleRep' ∷ (f :+: g) p → SimplifyRep (f :+: g) Source # fromSimpleRep' ∷ SimplifyRep (f :+: g) → (f :+: g) p Source #
SimpleConstructor f ⇒ SimpleGeneric (C1 ('MetaCons c a b) f) Source #
Instance details Defined in Constrained.Generic Methods toSimpleRep' ∷ C1 ('MetaCons c a b) f p → SimplifyRep (C1 ('MetaCons c a b) f) Source # fromSimpleRep' ∷ SimplifyRep (C1 ('MetaCons c a b) f) → C1 ('MetaCons c a b) f p Source #
SimpleGeneric f ⇒ SimpleGeneric (D1 d f) Source #
Instance details Defined in Constrained.Generic Methods toSimpleRep' ∷ D1 d f p → SimplifyRep (D1 d f) Source # fromSimpleRep' ∷ SimplifyRep (D1 d f) → D1 d f p Source #

data (c ∷ Symbol) ::: (ts ∷ [Type]) Source #

A constructor name with the types of its arguments

Instances

Instances details

TypeList prod ⇒ Inject c ((c ::: prod) ': (prod' ': constrs)) r Source #
Instance details Defined in Constrained.Generic Methods inject' ∷ (SOP ((c ::: prod) ': (prod' ': constrs)) → r) → FunTy (ConstrOf c ((c ::: prod) ': (prod' ': constrs))) r Source #
TypeList prod ⇒ Inject c '[c ::: prod] r Source #
Instance details Defined in Constrained.Generic Methods inject' ∷ (SOP '[c ::: prod] → r) → FunTy (ConstrOf c '[c ::: prod]) r Source #
(FunTy (ConstrOf c ((c' ::: prod) ': (con ': constrs))) r ~ FunTy (ConstrOf c (con ': constrs)) r, Inject c (con ': constrs) r) ⇒ Inject c ((c' ::: prod) ': (con ': constrs)) r Source #
Instance details Defined in Constrained.Generic Methods inject' ∷ (SOP ((c' ::: prod) ': (con ': constrs)) → r) → FunTy (ConstrOf c ((c' ::: prod) ': (con ': constrs))) r Source #
(TypeList prod, SOPLike (con ': cases) r) ⇒ SOPLike ((c ::: prod) ': (con ': cases)) r Source #
Instance details Defined in Constrained.Generic Methods algebra ∷ SOP ((c ::: prod) ': (con ': cases)) → ALG ((c ::: prod) ': (con ': cases)) r Source # consts ∷ r → ALG ((c ::: prod) ': (con ': cases)) r Source #
TypeList prod ⇒ SOPLike '[c ::: prod] r Source #
Instance details Defined in Constrained.Generic Methods algebra ∷ SOP '[c ::: prod] → ALG '[c ::: prod] r Source # consts ∷ r → ALG '[c ::: prod] r Source #
SopList (x' ': xs) (y ': ys) ⇒ SopList ((c ::: x) ': (x' ': xs)) (y ': ys) Source #
Instance details Defined in Constrained.Generic Methods injectSOPLeft ∷ SOP ((c ::: x) ': (x' ': xs)) → SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) Source # injectSOPRight ∷ SOP (y ': ys) → SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) Source # caseSOP ∷ SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) → Sum (SOP ((c ::: x) ': (x' ': xs))) (SOP (y ': ys)) Source #
SopList '[c ::: x] (y ': ys) Source #
Instance details Defined in Constrained.Generic Methods injectSOPLeft ∷ SOP '[c ::: x] → SOP (Append '[c ::: x] (y ': ys)) Source # injectSOPRight ∷ SOP (y ': ys) → SOP (Append '[c ::: x] (y ': ys)) Source # caseSOP ∷ SOP (Append '[c ::: x] (y ': ys)) → Sum (SOP '[c ::: x]) (SOP (y ': ys)) Source #

type family SOPOf f where ... Source #

Turn a Rep into a list that flattens the sum structre and gives the constructors names: Maybe Int -> '[Nothing ::: '[()], Just ::: '[Int]] Either Int Bool -> '[Left ::: '[Int], Right ::: '[Bool]] data Foo = Foo Int Bool | Bar Double -> '[Foo ::: '[Int, Bool], Bar ::: '[Double]]

Equations

SOPOf (D1 _ f) = SOPOf f
SOPOf (f :+: g) = Append (SOPOf f) (SOPOf g)
SOPOf (C1 ('MetaCons constr _ _) f) = '[constr ::: Constr f]

type family Constr f where ... Source #

Flatten a single constructor

Equations

Constr (S1 _ f) = Constr f
Constr (K1 _ k) = '[k]
Constr U1 = '[()]
Constr (f :*: g) = Append (Constr f) (Constr g)

type family SOP constrs where ... Source #

Turn a list from SOPOf into a Sum over Prod representation.

Equations

SOP '[c ::: prod] = ProdOver prod
SOP ((c ::: prod) ': constrs) = Sum (ProdOver prod) (SOP constrs)

type family ConstrOf c sop where ... Source #

Equations

ConstrOf c ((c ::: constr) ': sop) = constr
ConstrOf c (_ ': sop) = ConstrOf c sop

class Inject c constrs r where Source #

Methods

inject' ∷ (SOP constrs → r) → FunTy (ConstrOf c constrs) r Source #

Instances

Instances details

TypeList prod ⇒ Inject c ((c ::: prod) ': (prod' ': constrs)) r Source #
Instance details Defined in Constrained.Generic Methods inject' ∷ (SOP ((c ::: prod) ': (prod' ': constrs)) → r) → FunTy (ConstrOf c ((c ::: prod) ': (prod' ': constrs))) r Source #
TypeList prod ⇒ Inject c '[c ::: prod] r Source #
Instance details Defined in Constrained.Generic Methods inject' ∷ (SOP '[c ::: prod] → r) → FunTy (ConstrOf c '[c ::: prod]) r Source #
(FunTy (ConstrOf c ((c' ::: prod) ': (con ': constrs))) r ~ FunTy (ConstrOf c (con ': constrs)) r, Inject c (con ': constrs) r) ⇒ Inject c ((c' ::: prod) ': (con ': constrs)) r Source #
Instance details Defined in Constrained.Generic Methods inject' ∷ (SOP ((c' ::: prod) ': (con ': constrs)) → r) → FunTy (ConstrOf c ((c' ::: prod) ': (con ': constrs))) r Source #

inject ∷ ∀ c constrs. Inject c constrs (SOP constrs) ⇒ FunTy (ConstrOf c constrs) (SOP constrs) Source #

type family ALG constrs r where ... Source #

An `ALG constrs r` is a function that takes a way to turn every constructor into an r: ``` ALG (SOPOf (Rep (Either Int Bool))) r = (Int -> r) -> (Bool -> r) -> r ```

Equations

ALG '[c ::: prod] r = FunTy prod r → r
ALG ((c ::: prod) ': constrs) r = FunTy prod r → ALG constrs r

class SOPLike constrs r where Source #

Methods

algebra ∷ SOP constrs → ALG constrs r Source #

Run a SOP

consts ∷ r → ALG constrs r Source #

Ignore everything in the SOP

Instances

Instances details

(TypeList prod, SOPLike (con ': cases) r) ⇒ SOPLike ((c ::: prod) ': (con ': cases)) r Source #
Instance details Defined in Constrained.Generic Methods algebra ∷ SOP ((c ::: prod) ': (con ': cases)) → ALG ((c ::: prod) ': (con ': cases)) r Source # consts ∷ r → ALG ((c ::: prod) ': (con ': cases)) r Source #
TypeList prod ⇒ SOPLike '[c ::: prod] r Source #
Instance details Defined in Constrained.Generic Methods algebra ∷ SOP '[c ::: prod] → ALG '[c ::: prod] r Source # consts ∷ r → ALG '[c ::: prod] r Source #

class SimpleConstructor rep where Source #

Methods

toSimpleCon' ∷ rep p → ProdOver (Constr rep) Source #

fromSimpleCon' ∷ ProdOver (Constr rep) → rep p Source #

Instances

Instances details

SimpleConstructor (U1 ∷ Type → Type) Source #
Instance details Defined in Constrained.Generic Methods toSimpleCon' ∷ U1 p → ProdOver (Constr U1) Source # fromSimpleCon' ∷ ProdOver (Constr U1) → U1 p Source #
(SimpleConstructor f, SimpleConstructor g, TypeList (Constr f), TypeList (Constr g)) ⇒ SimpleConstructor (f :*: g) Source #
Instance details Defined in Constrained.Generic Methods toSimpleCon' ∷ (f :: g) p → ProdOver (Constr (f :: g)) Source # fromSimpleCon' ∷ ProdOver (Constr (f :: g)) → (f :: g) p Source #
SimpleConstructor (K1 i k ∷ Type → Type) Source #
Instance details Defined in Constrained.Generic Methods toSimpleCon' ∷ K1 i k p → ProdOver (Constr (K1 i k)) Source # fromSimpleCon' ∷ ProdOver (Constr (K1 i k)) → K1 i k p Source #
SimpleConstructor f ⇒ SimpleConstructor (S1 s f) Source #
Instance details Defined in Constrained.Generic Methods toSimpleCon' ∷ S1 s f p → ProdOver (Constr (S1 s f)) Source # fromSimpleCon' ∷ ProdOver (Constr (S1 s f)) → S1 s f p Source #

class SopList xs ys where Source #

Construct and deconstruct cases in a SOP

Methods

injectSOPLeft ∷ SOP xs → SOP (Append xs ys) Source #

injectSOPRight ∷ SOP ys → SOP (Append xs ys) Source #

caseSOP ∷ SOP (Append xs ys) → Sum (SOP xs) (SOP ys) Source #

Instances

Instances details

SopList (x' ': xs) (y ': ys) ⇒ SopList ((c ::: x) ': (x' ': xs)) (y ': ys) Source #
Instance details Defined in Constrained.Generic Methods injectSOPLeft ∷ SOP ((c ::: x) ': (x' ': xs)) → SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) Source # injectSOPRight ∷ SOP (y ': ys) → SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) Source # caseSOP ∷ SOP (Append ((c ::: x) ': (x' ': xs)) (y ': ys)) → Sum (SOP ((c ::: x) ': (x' ': xs))) (SOP (y ': ys)) Source #
SopList '[c ::: x] (y ': ys) Source #
Instance details Defined in Constrained.Generic Methods injectSOPLeft ∷ SOP '[c ::: x] → SOP (Append '[c ::: x] (y ': ys)) Source # injectSOPRight ∷ SOP (y ': ys) → SOP (Append '[c ::: x] (y ': ys)) Source # caseSOP ∷ SOP (Append '[c ::: x] (y ': ys)) → Sum (SOP '[c ::: x]) (SOP (y ': ys)) Source #