{-# LANGUAGE UndecidableInstances #-}
module Composite.CoRecord where
import Prelude
import Composite.Record (AllHave, HasInstances, (:->)(getVal, Val), reifyDicts, val, zipRecsWith)
import Control.Lens (Prism', prism')
import Data.Functor.Identity (Identity(Identity), runIdentity)
import Data.Kind (Constraint)
import Data.Maybe (fromMaybe)
import Data.Profunctor (dimap)
import Data.Proxy (Proxy(Proxy))
import Data.Vinyl.Core (Dict(Dict), Rec((:&), RNil), RecApplicative, recordToList, reifyConstraint, rmap, rpure)
import Data.Vinyl.Functor (Compose(Compose, getCompose), Const(Const), (:.))
import Data.Vinyl.Lens (RElem, type (∈), type (⊆), rget, rput, rreplace)
import Data.Vinyl.TypeLevel (RecAll, RIndex)
data CoRec :: (u -> *) -> [u] -> * where
CoVal :: r ∈ rs => !(f r) -> CoRec f rs
instance forall rs. (AllHave '[Show] rs, RecApplicative rs) => Show (CoRec Identity rs) where
show (CoVal (Identity x)) = "(CoVal " ++ show' x ++ ")"
where
shower :: Rec (Op String) rs
shower = reifyDicts (Proxy @'[Show]) (\ _ -> Op show)
show' = runOp (rget Proxy shower)
instance forall rs. (RecAll Maybe rs Eq, RecApplicative rs) => Eq (CoRec Identity rs) where
crA == crB = and . recordToList $ zipRecsWith f (toRec crA) (fieldToRec crB)
where
f :: forall a. (Dict Eq :. Maybe) a -> Maybe a -> Const Bool a
f (Compose (Dict a)) b = Const $ a == b
toRec = reifyConstraint (Proxy @Eq) . fieldToRec
type Field = CoRec Identity
coRec :: r ∈ rs => f r -> CoRec f rs
coRec = CoVal
coRecPrism :: (RecApplicative rs, r ∈ rs) => proxy r -> Prism' (CoRec f rs) (f r)
coRecPrism proxy = prism' CoVal (getCompose . rget proxy . coRecToRec)
field :: r ∈ rs => r -> Field rs
field = CoVal . Identity
fieldVal :: forall s a rs proxy. s :-> a ∈ rs => proxy (s :-> a) -> a -> Field rs
fieldVal _ = CoVal . val @s
fieldPrism :: (RecApplicative rs, r ∈ rs) => proxy r -> Prism' (Field rs) r
fieldPrism proxy = coRecPrism proxy . dimap runIdentity (fmap Identity)
fieldValPrism :: (RecApplicative rs, s :-> a ∈ rs) => proxy (s :-> a) -> Prism' (Field rs) a
fieldValPrism proxy = coRecPrism proxy . dimap (getVal . runIdentity) (fmap (Identity . Val))
foldCoVal :: (forall (r :: u). RElem r rs (RIndex r rs) => f r -> b) -> CoRec f rs -> b
foldCoVal f (CoVal x) = f x
{-# INLINE foldCoVal #-}
mapCoRec :: (forall x. f x -> g x) -> CoRec f rs -> CoRec g rs
mapCoRec f (CoVal x) = CoVal (f x)
{-# INLINE mapCoRec #-}
traverseCoRec :: Functor h => (forall x. f x -> h (g x)) -> CoRec f rs -> h (CoRec g rs)
traverseCoRec f (CoVal x) = CoVal <$> f x
{-# INLINE traverseCoRec #-}
coRecToRec :: RecApplicative rs => CoRec f rs -> Rec (Maybe :. f) rs
coRecToRec (CoVal a) = rput (Compose (Just a)) (rpure (Compose Nothing))
{-# INLINE coRecToRec #-}
fieldToRec :: RecApplicative rs => Field rs -> Rec Maybe rs
fieldToRec = rmap (fmap runIdentity . getCompose) . coRecToRec
{-# INLINE fieldToRec #-}
class FoldRec ss ts where
foldRec
:: (CoRec f ss -> CoRec f ss -> CoRec f ss)
-> CoRec f ss
-> Rec f ts
-> CoRec f ss
instance FoldRec ss '[] where
foldRec _ z _ = z
{-# INLINE foldRec #-}
instance (t ∈ ss, FoldRec ss ts) => FoldRec ss (t ': ts) where
foldRec f z (x :& xs) = foldRec f (z `f` CoVal x) xs
{-# INLINE foldRec #-}
foldRec1
:: FoldRec (r ': rs) rs
=> (CoRec f (r ': rs) -> CoRec f (r ': rs) -> CoRec f (r ': rs))
-> Rec f (r ': rs)
-> CoRec f (r ': rs)
foldRec1 f (x :& xs) = foldRec f (CoVal x) xs
{-# INLINE foldRec1 #-}
firstCoRec :: FoldRec rs rs => Rec (Maybe :. f) rs -> Maybe (CoRec f rs)
firstCoRec RNil = Nothing
firstCoRec v@(x :& _) = traverseCoRec getCompose $ foldRec f (CoVal x) v
where
f c@(CoVal (Compose (Just _))) _ = c
f _ c = c
{-# INLINE firstCoRec #-}
firstField :: FoldRec rs rs => Rec Maybe rs -> Maybe (Field rs)
firstField = firstCoRec . rmap (Compose . fmap Identity)
{-# INLINE firstField #-}
lastCoRec :: FoldRec rs rs => Rec (Maybe :. f) rs -> Maybe (CoRec f rs)
lastCoRec RNil = Nothing
lastCoRec v@(x :& _) = traverseCoRec getCompose $ foldRec f (CoVal x) v
where
f _ c@(CoVal (Compose (Just _))) = c
f c _ = c
{-# INLINE lastCoRec #-}
lastField :: FoldRec rs rs => Rec Maybe rs -> Maybe (Field rs)
lastField = lastCoRec . rmap (Compose . fmap Identity)
{-# INLINE lastField #-}
newtype Op b a = Op { runOp :: a -> b }
onCoRec
:: forall (cs :: [* -> Constraint]) (f :: * -> *) (rs :: [*]) (b :: *) (proxy :: [* -> Constraint] -> *).
(AllHave cs rs, Functor f, RecApplicative rs)
=> proxy cs
-> (forall (a :: *). HasInstances a cs => a -> b)
-> CoRec f rs
-> f b
onCoRec p f (CoVal x) = go <$> x
where
go = runOp $ rget Proxy (reifyDicts p (\ _ -> Op f) :: Rec (Op b) rs)
{-# INLINE onCoRec #-}
onField
:: forall (cs :: [* -> Constraint]) (rs :: [*]) (b :: *) (proxy :: [* -> Constraint] -> *).
(AllHave cs rs, RecApplicative rs)
=> proxy cs
-> (forall (a :: *). HasInstances a cs => a -> b)
-> Field rs
-> b
onField p f x = runIdentity (onCoRec p f x)
{-# INLINE onField #-}
asA :: (r ∈ rs, RecApplicative rs) => proxy r -> Field rs -> Maybe r
asA p = rget p . fieldToRec
{-# INLINE asA #-}
newtype Case' f b a = Case' { unCase' :: f a -> b }
type Cases' f rs b = Rec (Case' f b) rs
foldCoRec :: RecApplicative (r ': rs) => Cases' f (r ': rs) b -> CoRec f (r ': rs) -> b
foldCoRec hs = go hs . coRecToRec
where
go :: Cases' f rs b -> Rec (Maybe :. f) rs -> b
go (Case' f :& _) (Compose (Just x) :& _) = f x
go (Case' _ :& fs) (Compose Nothing :& t) = go fs t
go RNil RNil = error "foldCoRec should be provably total, isn't"
{-# INLINE go #-}
{-# INLINE foldCoRec #-}
matchCoRec :: RecApplicative (r ': rs) => CoRec f (r ': rs) -> Cases' f (r ': rs) b -> b
matchCoRec = flip foldCoRec
{-# INLINE matchCoRec #-}
newtype Case b a = Case { unCase :: a -> b }
type Cases rs b = Rec (Case b) rs
foldField :: RecApplicative (r ': rs) => Cases (r ': rs) b -> Field (r ': rs) -> b
foldField hs = foldCoRec (rmap (Case' . (. runIdentity) . unCase) hs)
{-# INLINE foldField #-}
matchField :: RecApplicative (r ': rs) => Field (r ': rs) -> Cases (r ': rs) b -> b
matchField = flip foldField
{-# INLINE matchField #-}
widenCoRec :: (FoldRec ss ss, RecApplicative rs, RecApplicative ss, rs ⊆ ss) => CoRec f rs -> CoRec f ss
widenCoRec r =
fromMaybe (error "widenCoRec should be provably total, isn't") $
firstCoRec (rreplace (coRecToRec r) (rpure $ Compose Nothing))
widenField :: (FoldRec ss ss, RecApplicative rs, RecApplicative ss, rs ⊆ ss) => Field rs -> Field ss
widenField r =
fromMaybe (error "widenField should be provably total, isn't") $
firstField (rreplace (fieldToRec r) (rpure Nothing))