{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Vinyl.XRec where
import Data.Vinyl.Core (Rec(..))
import Data.Vinyl.Functor
import Data.Vinyl.Lens (RecElem, RecElemFCtx, rgetC)
import Data.Vinyl.TypeLevel (RIndex)
import Data.Monoid
import GHC.TypeLits (KnownSymbol)
type XRec f = Rec (XData f)
pattern (::&) :: HKD f r -> XRec f rs -> XRec f (r ': rs)
pattern x $b::& :: HKD f r -> XRec f rs -> XRec f (r : rs)
$m::& :: forall r a (f :: a -> *) (r :: a) (rs :: [a]).
XRec f (r : rs) -> (HKD f r -> XRec f rs -> r) -> (Void# -> r) -> r
::& xs = XData x :& xs
{-# COMPLETE (::&) #-}
infixr 7 ::&
pattern XRNil :: XRec f '[]
pattern $bXRNil :: XRec f '[]
$mXRNil :: forall r u (f :: u -> *).
XRec f '[] -> (Void# -> r) -> (Void# -> r) -> r
XRNil = RNil
{-# COMPLETE XRNil #-}
rmapX :: forall f g rs. (XRMap f g rs, IsoXRec f rs, IsoXRec g rs)
=> (forall a. HKD f a -> HKD g a) -> Rec f rs -> Rec g rs
rmapX :: (forall (a :: u). HKD f a -> HKD g a) -> Rec f rs -> Rec g rs
rmapX forall (a :: u). HKD f a -> HKD g a
f = XRec g rs -> Rec g rs
forall u (f :: u -> *) (ts :: [u]).
IsoXRec f ts =>
XRec f ts -> Rec f ts
fromXRec (XRec g rs -> Rec g rs)
-> (Rec f rs -> XRec g rs) -> Rec f rs -> Rec g rs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: u). XData f a -> XData g a) -> XRec f rs -> XRec g rs
forall u (f :: u -> *) (g :: u -> *) (rs :: [u]).
XRMap f g rs =>
(forall (a :: u). XData f a -> XData g a) -> XRec f rs -> XRec g rs
xrmapAux forall (a :: u). XData f a -> XData g a
aux (XRec f rs -> XRec g rs)
-> (Rec f rs -> XRec f rs) -> Rec f rs -> XRec g rs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec f rs -> XRec f rs
forall u (f :: u -> *) (ts :: [u]).
IsoXRec f ts =>
Rec f ts -> XRec f ts
toXRec
where aux :: forall a. XData f a -> XData g a
aux :: XData f a -> XData g a
aux = HKD g a -> XData g a
forall k (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD g a -> XData g a)
-> (XData f a -> HKD g a) -> XData f a -> XData g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HKD f a -> HKD g a
forall (a :: u). HKD f a -> HKD g a
f @a (HKD f a -> HKD g a)
-> (XData f a -> HKD f a) -> XData f a -> HKD g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XData f a -> HKD f a
forall k (t :: k -> *) (a :: k). XData t a -> HKD t a
unX
rmapXEndo :: forall f rs. (XRMap f f rs, IsoXRec f rs)
=> (forall a. HKD f a -> HKD f a) -> Rec f rs -> Rec f rs
rmapXEndo :: (forall (a :: u). HKD f a -> HKD f a) -> Rec f rs -> Rec f rs
rmapXEndo forall (a :: u). HKD f a -> HKD f a
f = XRec f rs -> Rec f rs
forall u (f :: u -> *) (ts :: [u]).
IsoXRec f ts =>
XRec f ts -> Rec f ts
fromXRec (XRec f rs -> Rec f rs)
-> (Rec f rs -> XRec f rs) -> Rec f rs -> Rec f rs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: u). XData f a -> XData f a) -> XRec f rs -> XRec f rs
forall u (f :: u -> *) (g :: u -> *) (rs :: [u]).
XRMap f g rs =>
(forall (a :: u). XData f a -> XData g a) -> XRec f rs -> XRec g rs
xrmapAux forall (a :: u). XData f a -> XData f a
aux (XRec f rs -> XRec f rs)
-> (Rec f rs -> XRec f rs) -> Rec f rs -> XRec f rs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec f rs -> XRec f rs
forall u (f :: u -> *) (ts :: [u]).
IsoXRec f ts =>
Rec f ts -> XRec f ts
toXRec
where aux :: forall a. XData f a -> XData f a
aux :: XData f a -> XData f a
aux = HKD f a -> XData f a
forall k (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD f a -> XData f a)
-> (XData f a -> HKD f a) -> XData f a -> XData f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HKD f a -> HKD f a
forall (a :: u). HKD f a -> HKD f a
f @a (HKD f a -> HKD f a)
-> (XData f a -> HKD f a) -> XData f a -> HKD f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XData f a -> HKD f a
forall k (t :: k -> *) (a :: k). XData t a -> HKD t a
unX
xrmap :: forall f g rs. XRMap f g rs
=> (forall a. HKD f a -> HKD g a) -> XRec f rs -> XRec g rs
xrmap :: (forall (a :: u). HKD f a -> HKD g a) -> XRec f rs -> XRec g rs
xrmap forall (a :: u). HKD f a -> HKD g a
f = (forall (a :: u). XData f a -> XData g a) -> XRec f rs -> XRec g rs
forall u (f :: u -> *) (g :: u -> *) (rs :: [u]).
XRMap f g rs =>
(forall (a :: u). XData f a -> XData g a) -> XRec f rs -> XRec g rs
xrmapAux forall (a :: u). XData f a -> XData g a
aux
where aux :: forall a. XData f a -> XData g a
aux :: XData f a -> XData g a
aux = HKD g a -> XData g a
forall k (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD g a -> XData g a)
-> (XData f a -> HKD g a) -> XData f a -> XData g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HKD f a -> HKD g a
forall (a :: u). HKD f a -> HKD g a
f @a (HKD f a -> HKD g a)
-> (XData f a -> HKD f a) -> XData f a -> HKD g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XData f a -> HKD f a
forall k (t :: k -> *) (a :: k). XData t a -> HKD t a
unX
newtype XData t a = XData { XData t a -> HKD t a
unX :: HKD t a }
class XRMap f g rs where
xrmapAux :: (forall a . XData f a -> XData g a) -> XRec f rs -> XRec g rs
instance XRMap f g '[] where
xrmapAux :: (forall (a :: u). XData f a -> XData g a)
-> XRec f '[] -> XRec g '[]
xrmapAux forall (a :: u). XData f a -> XData g a
_ XRec f '[]
RNil = XRec g '[]
forall u (f :: u -> *). Rec f '[]
RNil
instance forall f g r rs. (XRMap f g rs, IsoHKD f r, IsoHKD g r)
=> XRMap f g (r ': rs) where
xrmapAux :: (forall (a :: a). XData f a -> XData g a)
-> XRec f (r : rs) -> XRec g (r : rs)
xrmapAux forall (a :: a). XData f a -> XData g a
f (XData f r
x :& Rec (XData f) rs
xs) = XData f r -> XData g r
forall (a :: a). XData f a -> XData g a
f XData f r
x XData g r -> Rec (XData g) rs -> Rec (XData g) (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& (forall (a :: a). XData f a -> XData g a)
-> Rec (XData f) rs -> Rec (XData g) rs
forall u (f :: u -> *) (g :: u -> *) (rs :: [u]).
XRMap f g rs =>
(forall (a :: u). XData f a -> XData g a) -> XRec f rs -> XRec g rs
xrmapAux forall (a :: a). XData f a -> XData g a
f Rec (XData f) rs
xs
class XRApply f g rs where
xrapply :: XRec (Lift (->) f g) rs -> XRec f rs -> XRec g rs
instance XRApply f g '[] where
xrapply :: XRec (Lift (->) f g) '[] -> XRec f '[] -> XRec g '[]
xrapply XRec (Lift (->) f g) '[]
RNil XRec f '[]
RNil = XRec g '[]
forall u (f :: u -> *). Rec f '[]
RNil
instance XRApply f g rs => XRApply f g (r ': rs) where
xrapply :: XRec (Lift (->) f g) (r : rs) -> XRec f (r : rs) -> XRec g (r : rs)
xrapply (XData HKD (Lift (->) f g) r
f :& Rec (XData (Lift (->) f g)) rs
fs) (XData HKD f r
x :& Rec (XData f) rs
xs) = HKD g r -> XData g r
forall k (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD (Lift (->) f g) r
HKD f r -> HKD g r
f HKD f r
HKD f r
x) XData g r -> Rec (XData g) rs -> Rec (XData g) (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& Rec (XData (Lift (->) f g)) rs -> XRec f rs -> Rec (XData g) rs
forall u (f :: u -> *) (g :: u -> *) (rs :: [u]).
XRApply f g rs =>
XRec (Lift (->) f g) rs -> XRec f rs -> XRec g rs
xrapply Rec (XData (Lift (->) f g)) rs
fs XRec f rs
Rec (XData f) rs
xs
class IsoXRec f ts where
fromXRec :: XRec f ts -> Rec f ts
toXRec :: Rec f ts -> XRec f ts
instance IsoXRec f '[] where
fromXRec :: XRec f '[] -> Rec f '[]
fromXRec XRec f '[]
RNil = Rec f '[]
forall u (f :: u -> *). Rec f '[]
RNil
toXRec :: Rec f '[] -> XRec f '[]
toXRec Rec f '[]
RNil = XRec f '[]
forall u (f :: u -> *). XRec f '[]
XRNil
instance (IsoXRec f ts, IsoHKD f t) => IsoXRec f (t ': ts) where
fromXRec :: XRec f (t : ts) -> Rec f (t : ts)
fromXRec (HKD f t
x ::& XRec f ts
xs) = HKD f t -> f t
forall k (f :: k -> *) (a :: k). IsoHKD f a => HKD f a -> f a
unHKD HKD f t
x f t -> Rec f ts -> Rec f (t : ts)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& XRec f ts -> Rec f ts
forall u (f :: u -> *) (ts :: [u]).
IsoXRec f ts =>
XRec f ts -> Rec f ts
fromXRec XRec f ts
xs
toXRec :: Rec f (t : ts) -> XRec f (t : ts)
toXRec (f r
x :& Rec f rs
xs) = f r -> HKD f r
forall k (f :: k -> *) (a :: k). IsoHKD f a => f a -> HKD f a
toHKD f r
x HKD f t -> XRec f rs -> XRec f (t : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
HKD f r -> XRec f rs -> XRec f (r : rs)
::& Rec f rs -> XRec f rs
forall u (f :: u -> *) (ts :: [u]).
IsoXRec f ts =>
Rec f ts -> XRec f ts
toXRec Rec f rs
xs
class IsoHKD f a where
type HKD f a
type HKD f a = f a
unHKD :: HKD f a -> f a
default unHKD :: HKD f a ~ f a => HKD f a -> f a
unHKD = HKD f a -> f a
forall a. a -> a
id
toHKD :: f a -> HKD f a
default toHKD :: (HKD f a ~ f a) => f a -> HKD f a
toHKD = f a -> HKD f a
forall a. a -> a
id
instance IsoHKD Identity a where
type HKD Identity a = a
unHKD :: HKD Identity a -> Identity a
unHKD = HKD Identity a -> Identity a
forall a. a -> Identity a
Identity
toHKD :: Identity a -> HKD Identity a
toHKD (Identity a
x) = a
HKD Identity a
x
instance KnownSymbol s => IsoHKD ElField '(s,a) where
type HKD ElField '(s,a) = a
unHKD :: HKD ElField '(s, a) -> ElField '(s, a)
unHKD = HKD ElField '(s, a) -> ElField '(s, a)
forall (t :: (Symbol, *)). Snd t -> ElField t
Field
toHKD :: ElField '(s, a) -> HKD ElField '(s, a)
toHKD (Field Snd '(s, a)
x) = Snd '(s, a)
HKD ElField '(s, a)
x
instance (IsoHKD f (HKD g a), IsoHKD g a, Functor f) => IsoHKD (Compose f g) a where
type HKD (Compose f g) a = HKD f (HKD g a)
unHKD :: HKD (Compose f g) a -> Compose f g a
unHKD HKD (Compose f g) a
x = f (g a) -> Compose f g a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose (HKD g a -> g a
forall k (f :: k -> *) (a :: k). IsoHKD f a => HKD f a -> f a
unHKD (HKD g a -> g a) -> f (HKD g a) -> f (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HKD f (HKD g a) -> f (HKD g a)
forall k (f :: k -> *) (a :: k). IsoHKD f a => HKD f a -> f a
unHKD HKD (Compose f g) a
HKD f (HKD g a)
x)
toHKD :: Compose f g a -> HKD (Compose f g) a
toHKD (Compose f (g a)
fgx) = f (HKD g a) -> HKD f (HKD g a)
forall k (f :: k -> *) (a :: k). IsoHKD f a => f a -> HKD f a
toHKD (g a -> HKD g a
forall k (f :: k -> *) (a :: k). IsoHKD f a => f a -> HKD f a
toHKD (g a -> HKD g a) -> f (g a) -> f (HKD g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (g a)
fgx)
instance (IsoHKD f a, IsoHKD g a) => IsoHKD (Lift (->) f g) a where
type HKD (Lift (->) f g) a = HKD f a -> HKD g a
unHKD :: HKD (Lift (->) f g) a -> Lift (->) f g a
unHKD HKD (Lift (->) f g) a
x = (f a -> g a) -> Lift (->) f g a
forall l l' k (op :: l -> l' -> *) (f :: k -> l) (g :: k -> l')
(x :: k).
op (f x) (g x) -> Lift op f g x
Lift (HKD g a -> g a
forall k (f :: k -> *) (a :: k). IsoHKD f a => HKD f a -> f a
unHKD (HKD g a -> g a) -> (f a -> HKD g a) -> f a -> g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HKD (Lift (->) f g) a
HKD f a -> HKD g a
x (HKD f a -> HKD g a) -> (f a -> HKD f a) -> f a -> HKD g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> HKD f a
forall k (f :: k -> *) (a :: k). IsoHKD f a => f a -> HKD f a
toHKD)
toHKD :: Lift (->) f g a -> HKD (Lift (->) f g) a
toHKD (Lift f a -> g a
x) = g a -> HKD g a
forall k (f :: k -> *) (a :: k). IsoHKD f a => f a -> HKD f a
toHKD (g a -> HKD g a) -> (HKD f a -> g a) -> HKD f a -> HKD g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> g a
x (f a -> g a) -> (HKD f a -> f a) -> HKD f a -> g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HKD f a -> f a
forall k (f :: k -> *) (a :: k). IsoHKD f a => HKD f a -> f a
unHKD
instance IsoHKD IO a where
instance IsoHKD (Either a) b where
instance IsoHKD Maybe a where
instance IsoHKD First a where
instance IsoHKD Last a where
instance IsoHKD ((,) a) b where
instance IsoHKD Sum a where
type HKD Sum a = a
unHKD :: HKD Sum a -> Sum a
unHKD = HKD Sum a -> Sum a
forall a. a -> Sum a
Sum
toHKD :: Sum a -> HKD Sum a
toHKD (Sum a
x) = a
HKD Sum a
x
instance IsoHKD Product a where
type HKD Product a = a
unHKD :: HKD Product a -> Product a
unHKD = HKD Product a -> Product a
forall a. a -> Product a
Product
toHKD :: Product a -> HKD Product a
toHKD (Product a
x) = a
HKD Product a
x
rgetX :: forall a record f rs.
(RecElem record a a rs rs (RIndex a rs),
RecElemFCtx record f,
IsoHKD f a)
=> record f rs -> HKD f a
rgetX :: record f rs -> HKD f a
rgetX = f a -> HKD f a
forall k (f :: k -> *) (a :: k). IsoHKD f a => f a -> HKD f a
toHKD (f a -> HKD f a) -> (record f rs -> f a) -> record f rs -> HKD f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RecElem record a a rs rs (RIndex a rs), RecElemFCtx record f) =>
record f rs -> f a
forall (r :: k).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
record f rs -> f r
rgetAux @a
where rgetAux :: forall r.
(RecElem record r r rs rs (RIndex r rs),
RecElemFCtx record f)
=> record f rs -> f r
rgetAux :: record f rs -> f r
rgetAux = record f rs -> f r
forall k (record :: (k -> *) -> [k] -> *) (r :: k) (r' :: k)
(rs :: [k]) (rs' :: [k]) (i :: Nat) (f :: k -> *).
(RecElem record r r' rs rs' i, RecElemFCtx record f, r ~ r') =>
record f rs -> f r
rgetC