module Data.YokoRaw
(module Data.Yoko.Representation,
module Data.Yoko.View,
one, (|||), (||.), (.||), (.|.),
disbanded, band, ConDCOf, precise_case,
(:-:), Embed, Partition,
embed, inject, partition, project,
reps, EachGeneric, EachRep, ig_from,
Equal,
module Data.Yoko.TH) where
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
import Data.Yoko.Each
import Data.Yoko.TH
one :: (dc -> a) -> N dc -> a
one = foldN
infixl 6 |||
(|||) :: (Codomain sumL ~ Codomain sumR) => (sumL -> a) -> (sumR -> a) -> sumL :+: sumR -> 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)
disbanded = TypeSums.inject
band :: forall t. Each (ConDCOf t) (DCs t) => DCs t -> t
band = each (Proxy :: Proxy (ConDCOf t)) rejoin
class (Codomain dc ~ t, DC dc) => ConDCOf t dc
instance (Codomain dc ~ t, DC dc) => ConDCOf t dc
embed :: (Codomain sub ~ Codomain sup, Embed sub sup) => sub -> sup
embed = TypeSums.embed
inject :: Embed (N dc) sum => dc -> sum
inject = TypeSums.inject
partition :: (Codomain sum ~ Codomain sub, Partition sum sub (sum :-: sub)) =>
sum -> Either sub (sum :-: sub)
partition = TypeSums.partition
project :: (Codomain sum ~ Codomain dc, Partition sum (N dc) (sum :-: N dc)) =>
sum -> Either dc (sum :-: N dc)
project = TypeSums.project
reps :: EachGeneric sum => sum -> EachRep sum
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 -> EachRep sum ; objEach :: EachRep sum -> sum
instance Generic a => EachGeneric (N a) where
repEach (N x) = rep x ; objEach = N . obj
instance (EachGeneric a, EachGeneric b) => EachGeneric (a :+: b) where
repEach = mapPlus repEach repEach
objEach = mapPlus objEach objEach
precise_case :: (Codomain dcs ~ t, Codomain (DCs t) ~ t, DT t,
Partition (DCs t) dcs (DCs t :-: dcs)) =>
(DCs t :-: dcs -> a) -> t -> (dcs -> a) -> a
precise_case g x f = either f g $ partition $ disband x
ig_from :: (DT t, EachGeneric (DCs t)) => t -> EachRep (DCs t)
ig_from x = reps $ disband x