module Data.Extensible.Product (
(:*)(..)
, (<:)
, (<:*)
, (*++*)
, hhead
, htail
, huncons
, hmap
, htrans
, hzipWith
, hzipWith3
, hfoldMap
, htraverse
, htabulate
, hlookup
, sector
, sectorAt
, Generate(..)
, generate
, Forall(..)
, generateFor
, fromHList
, toHList) where
import Data.Extensible.Internal
import Data.Extensible.Internal.Rig
import Data.Extensible.Internal.HList
import Unsafe.Coerce
import Data.Typeable
import Control.Applicative
import Data.Monoid
data (h :: k -> *) :* (s :: [k]) where
Nil :: h :* '[]
Tree :: !(h x)
-> h :* Half xs
-> h :* Half (Tail xs)
-> h :* (x ': xs)
deriving instance Typeable (:*)
hhead :: h :* (x ': xs) -> h x
hhead (Tree a _ _) = a
htail :: h :* (x ': xs) -> h :* xs
htail (Tree _ a@(Tree h _ _) b) = unsafeCoerce (Tree h) b (htail a)
htail (Tree _ Nil _) = unsafeCoerce Nil
huncons :: forall h x xs. h :* (x ': xs) -> (h x, h :* xs)
huncons t@(Tree a _ _) = (a, htail t)
(<:*) :: forall h x xs. h x -> h :* xs -> h :* (x ': xs)
a <:* Tree b c d = Tree a (lemmaHalfTail (Proxy :: Proxy (Tail xs)) $ b <: d) c
a <:* Nil = Tree a Nil Nil
infixr 0 <:*
(<:) :: h x -> h :* xs -> h :* (x ': xs)
(<:) = (<:*)
infixr 0 <:
hmap :: (forall x. g x -> h x) -> g :* xs -> h :* xs
hmap t (Tree h a b) = Tree (t h) (hmap t a) (hmap t b)
hmap _ Nil = Nil
htrans :: (forall x. g x -> h (t x)) -> g :* xs -> h :* Map t xs
htrans t (Tree h a b) = unsafeCoerce (Tree (t h)) (htrans t a) (htrans t b)
htrans _ Nil = Nil
(*++*) :: h :* xs -> h :* ys -> h :* (xs ++ ys)
(*++*) Nil ys = ys
(*++*) xs'@(Tree x _ _) ys = let xs = htail xs' in x <:* (xs *++* ys)
infixr 0 *++*
hzipWith :: (forall x. f x -> g x -> h x) -> f :* xs -> g :* xs -> h :* xs
hzipWith t (Tree f a b) (Tree g c d) = Tree (t f g) (hzipWith t a c) (hzipWith t b d)
hzipWith _ Nil _ = Nil
hzipWith _ _ Nil = Nil
hzipWith3 :: (forall x. f x -> g x -> h x -> i x) -> f :* xs -> g :* xs -> h :* xs -> i :* xs
hzipWith3 t (Tree f a b) (Tree g c d) (Tree h e f') = Tree (t f g h) (hzipWith3 t a c e) (hzipWith3 t b d f')
hzipWith3 _ Nil _ _ = Nil
hzipWith3 _ _ Nil _ = Nil
hzipWith3 _ _ _ Nil = Nil
hfoldMap :: Monoid a => (forall x. h x -> a) -> h :* xs -> a
hfoldMap f (Tree h a b) = f h <> hfoldMap f a <> hfoldMap f b
hfoldMap _ Nil = mempty
htraverse :: Applicative f => (forall x. h x -> f (h x)) -> h :* xs -> f (h :* xs)
htraverse f (Tree h a b) = Tree <$> f h <*> htraverse f a <*> htraverse f b
htraverse _ Nil = pure Nil
hlookup :: Membership xs x -> h :* xs -> h x
hlookup = view . sectorAt
htabulate :: forall g h xs. (forall x. Membership xs x -> g x -> h x) -> g :* xs -> h :* xs
htabulate f = go id where
go :: (forall x. Membership t x -> Membership xs x) -> g :* t -> h :* t
go k (Tree g a b) = Tree (f (k here) g) (go (k . navL) a) (go (k . navR) b)
go _ Nil = Nil
sector :: (x ∈ xs) => Lens' (h :* xs) (h x)
sector = sectorAt membership
sectorAt :: forall f h x xs. Functor f => Membership xs x -> (h x -> f (h x)) -> h :* xs -> f (h :* xs)
sectorAt pos f = flip go pos where
go :: forall t. h :* t -> Membership t x -> f (h :* t)
go (Tree h a b) = navigate
(\Here -> fmap (\h' -> Tree h' a b) (f h))
(fmap (\a' -> Tree h a' b) . go a)
(fmap (\b' -> Tree h a b') . go b)
go Nil = error "Impossible"
class Generate (xs :: [k]) where
generateA :: Applicative f => (forall x. Membership xs x -> f (h x)) -> f (h :* xs)
instance Generate '[] where
generateA _ = pure Nil
instance (Generate (Half xs), Generate (Half (Tail xs))) => Generate (x ': xs) where
generateA f = Tree <$> f here <*> generateA (f . navL) <*> generateA (f . navR)
generate :: Generate xs => (forall x. Membership xs x -> h x) -> h :* xs
generate f = getK0 (generateA (K0 . f))
class Forall c (xs :: [k]) where
generateForA :: Applicative f => proxy c -> (forall x. c x => Membership xs x -> f (h x)) -> f (h :* xs)
instance Forall c '[] where
generateForA _ _ = pure Nil
instance (c x, Forall c (Half xs), Forall c (Half (Tail xs))) => Forall c (x ': xs) where
generateForA proxy f = Tree
<$> f here
<*> generateForA proxy (f . navL)
<*> generateForA proxy (f . navR)
generateFor :: Forall c xs => proxy c -> (forall x. c x => Membership xs x -> h x) -> h :* xs
generateFor p f = getK0 (generateForA p (K0 . f))
toHList :: h :* xs -> HList h xs
toHList (Tree h a b) = HCons h $ lemmaMerging $ toHList a `merge` toHList b
toHList Nil = HNil
fromHList :: HList h xs -> h :* xs
fromHList (HCons x xs) = let (a, b) = split xs in Tree x (fromHList a) (fromHList b)
fromHList HNil = Nil