module Data.YokoRaw
(module Data.Yoko.Representation,
module Data.Yoko.View,
module Data.Yoko.TypeBasics,
module Data.Yoko.W,
one, (|||), (||.), (.||), (.|.),
disbanded, AreDCsOf, band, precise_case0,
(:-:), Embed, Partition,
embed, inject, partition, project,
reps, EachGeneric, EachRep, ig_from) where
import Data.Yoko.W
import Data.Yoko.TypeBasics
import Data.Yoko.Representation
import Data.Yoko.View
import Data.Yoko.TypeSums (Embed, Partition, (:-:))
import qualified Data.Yoko.TypeSums as TypeSums
one :: (dc -> a) -> N dc p1 p0 -> a
one = foldN0
infixl 6 |||
(|||) :: (Codomain0 sumL ~ Codomain0 sumR) => (sumL p1 p0 -> a) -> (sumR p1 p0 -> a) -> (sumL :+: sumR) p1 p0 -> a
(|||) = foldPlus
infixl 9 .|.
infixr 8 .||, ||.
f .|. g = one f ||| one g
f .|| g = one f ||| g
f ||. g = f ||| one g
disbanded :: Embed (N dc) (DCs (Codomain dc)) => dc -> DCs (Codomain dc) p1 p0
disbanded = TypeSums.inject0
class AreDCsOf (t :: k) (dcs :: * -> * -> *) where band_ :: W' t dcs p1 p0
instance (WN dc, Codomain dc ~ t, DC dc) => AreDCsOf t (N dc) where
band_ = composeSymW' rejoin unN
instance (FoldPlusW' t, AreDCsOf t l, AreDCsOf t r) => AreDCsOf t (l :+: r) where band_ = foldPlusW' band_ band_
band :: (AreDCsOf (t :: k) (DCs t)) => W' t (DCs t) p1 p0
band = band_
embed :: (Codomain0 sub ~ Codomain0 sup, Embed sub sup) => sub p1 p0 -> sup p1 p0
embed = TypeSums.embed
inject :: Embed (N dc) sum => dc -> sum p1 p0
inject = TypeSums.inject0
partition :: (Codomain0 sum ~ Codomain0 sub, Partition sum sub (sum :-: sub)) =>
sum p1 p0 -> Either (sub p1 p0) ((sum :-: sub) p1 p0)
partition = TypeSums.partition
project :: (Codomain0 sum ~ Codomain dc, Partition sum (N dc) (sum :-: N dc)) =>
sum p1 p0 -> Either dc ((sum :-: N dc) p1 p0)
project = TypeSums.project0
reps :: EachGeneric sum => sum p1 p0 -> EachRep sum p1 p0
reps = repEach
type family EachRep (sum :: * -> * -> *) :: * -> * -> *
type instance EachRep (N a) = Rep a
type instance EachRep (a :+: b) = EachRep a :+: EachRep b
class EachGeneric sum where repEach :: sum p1 p0 -> EachRep sum p1 p0
instance (WN dc, Generic dc) => EachGeneric (N dc) where repEach = unSym rep unN
instance (EachGeneric a, EachGeneric b) => EachGeneric (a :+: b) where repEach = mapPlus repEach repEach
precise_case0 :: (Codomain0 dcs ~ t, Codomain0 (DCs t) ~ t, DT t,
Partition (DCs t) dcs (DCs t :-: dcs)) =>
((DCs t :-: dcs) p1 p0 -> a) -> t -> (dcs p1 p0 -> a) -> a
precise_case0 g x f = either f g $ partition $ unW0 disband x
ig_from :: (ComposeW t, DT t, EachGeneric (DCs t)) => W t (EachRep (DCs t)) p1 p0
ig_from = reps `composeW` disband