{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Ten.Update
( Update10(..), updateRep10, ixRep10, FieldSetter10(..)
, EqualityTable(..), equalityTable
, GUpdate10(..)
) where
import Data.Functor ((<&>))
import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..))
import GHC.Generics
( Generic1(..)
, (:*:)(..), (:.:)(..)
, M1(..), Rec1(..), U1(..)
)
import Data.Wrapped (Wrapped1(..))
import Data.Functor.Rep (Representable(..))
import Data.Functor.Update (Update(..))
import Data.Ten.Ap (Ap10(..))
import Data.Ten.Applicative (Applicative10(..))
import Data.Ten.Field (Field10(..))
import Data.Ten.Internal (mapStarFst, mapStarSnd)
import Data.Ten.Representable (Representable10(..), GTabulate10(..))
class Representable10 f => Update10 (f :: (k -> Type) -> Type) where
overRep10 :: Rep10 f a -> (m a -> m a) -> f m -> f m
updateRep10 :: Update10 f => Rep10 f a -> m a -> f m -> f m
updateRep10 :: Rep10 f a -> m a -> f m -> f m
updateRep10 Rep10 f a
i = Rep10 f a -> (m a -> m a) -> f m -> f m
forall k (f :: (k -> *) -> *) (a :: k) (m :: k -> *).
Update10 f =>
Rep10 f a -> (m a -> m a) -> f m -> f m
overRep10 Rep10 f a
i ((m a -> m a) -> f m -> f m)
-> (m a -> m a -> m a) -> m a -> f m -> f m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> m a -> m a
forall a b. a -> b -> a
const
ixRep10
:: (Update10 f, Functor g)
=> Rep10 f a -> (m a -> g (m a)) -> f m -> g (f m)
ixRep10 :: Rep10 f a -> (m a -> g (m a)) -> f m -> g (f m)
ixRep10 Rep10 f a
i m a -> g (m a)
f = \f m
fm -> m a -> g (m a)
f (f m -> Rep10 f a -> m a
forall k (f :: (k -> *) -> *) (m :: k -> *) (a :: k).
Representable10 f =>
f m -> Rep10 f a -> m a
index10 f m
fm Rep10 f a
i) g (m a) -> (m a -> f m) -> g (f m)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \m a
fma -> Rep10 f a -> m a -> f m -> f m
forall k (f :: (k -> *) -> *) (a :: k) (m :: k -> *).
Update10 f =>
Rep10 f a -> m a -> f m -> f m
updateRep10 Rep10 f a
i m a
fma f m
fm
newtype EqualityTable f a = EqualityTable (f (Maybe :.: ((:~:) a)))
equalityTable :: Update10 f => f (EqualityTable f)
equalityTable :: f (EqualityTable f)
equalityTable = (forall (a :: k1). Rep10 f a -> EqualityTable f a)
-> f (EqualityTable f)
forall k (f :: (k -> *) -> *) (m :: k -> *).
Representable10 f =>
(forall (a :: k). Rep10 f a -> m a) -> f m
tabulate10 ((forall (a :: k1). Rep10 f a -> EqualityTable f a)
-> f (EqualityTable f))
-> (forall (a :: k1). Rep10 f a -> EqualityTable f a)
-> f (EqualityTable f)
forall a b. (a -> b) -> a -> b
$ \Rep10 f a
i -> f (Maybe :.: (:~:) a) -> EqualityTable f a
forall k1 (f :: (k1 -> *) -> *) (a :: k1).
f (Maybe :.: (:~:) a) -> EqualityTable f a
EqualityTable (f (Maybe :.: (:~:) a) -> EqualityTable f a)
-> f (Maybe :.: (:~:) a) -> EqualityTable f a
forall a b. (a -> b) -> a -> b
$
Rep10 f a
-> (:.:) Maybe ((:~:) a) a
-> f (Maybe :.: (:~:) a)
-> f (Maybe :.: (:~:) a)
forall k (f :: (k -> *) -> *) (a :: k) (m :: k -> *).
Update10 f =>
Rep10 f a -> m a -> f m -> f m
updateRep10 Rep10 f a
i (Maybe (a :~: a) -> (:.:) Maybe ((:~:) a) a
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 ((a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl)) ((forall (a :: k1). (:.:) Maybe ((:~:) a) a)
-> f (Maybe :.: (:~:) a)
forall k (f :: (k -> *) -> *) (m :: k -> *).
Applicative10 f =>
(forall (a :: k). m a) -> f m
pure10 (Maybe (a :~: a) -> (:.:) Maybe ((:~:) a) a
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 Maybe (a :~: a)
forall a. Maybe a
Nothing))
instance ( Generic1 f
, Applicative10 (Rep1 f), GTabulate10 (Rep1 f), GUpdate10 (Rep1 f)
)
=> Update10 (Wrapped1 Generic1 f) where
overRep10 :: Rep10 (Wrapped1 Generic1 f) a
-> (m a -> m a) -> Wrapped1 Generic1 f m -> Wrapped1 Generic1 f m
overRep10 =
\Rep10 (Wrapped1 Generic1 f) a
i m a -> m a
f (Wrapped1 f m
fm) -> f m -> Wrapped1 Generic1 f m
forall k (c :: (k -> *) -> Constraint) (f :: k -> *) (a :: k).
f a -> Wrapped1 c f a
Wrapped1 (f m -> Wrapped1 Generic1 f m) -> f m -> Wrapped1 Generic1 f m
forall a b. (a -> b) -> a -> b
$ FieldSetter10 f a -> (m a -> m a) -> f m -> f m
forall k (f :: (k -> *) -> *) (a :: k).
FieldSetter10 f a
-> forall (m :: k -> *). (m a -> m a) -> f m -> f m
runFS10 (Field10 f a -> f (FieldSetter10 f) -> FieldSetter10 f a
forall k (f :: (k -> *) -> *) (a :: k).
Field10 f a -> forall (m :: k -> *). f m -> m a
getField10 Field10 f a
Rep10 (Wrapped1 Generic1 f) a
i f (FieldSetter10 f)
setters) m a -> m a
f f m
fm
where
setters :: f (FieldSetter10 f)
setters :: f (FieldSetter10 f)
setters = f (FieldSetter10 f)
forall k (f :: (k -> *) -> *).
(Generic1 f, GUpdate10 (Rep1 f)) =>
f (FieldSetter10 f)
setters10
class GUpdate10 (rec :: (k -> Type) -> Type) where
gsetters10
:: (forall a. (forall m. (m a -> m a) -> rec m -> rec m) -> r a)
-> rec r
instance Update10 (Ap10 a) where
overRep10 :: Rep10 (Ap10 a) a -> (m a -> m a) -> Ap10 a m -> Ap10 a m
overRep10 Rep10 (Ap10 a) a
Refl m a -> m a
f (Ap10 m a
x) = m a -> Ap10 a m
forall k (a :: k) (f :: k -> *). f a -> Ap10 a f
Ap10 (m a -> m a
f m a
m a
x)
{-# INLINE overRep10 #-}
instance GUpdate10 U1 where
gsetters10 :: (forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> U1 m -> U1 m) -> r a)
-> U1 r
gsetters10 forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> U1 m -> U1 m) -> r a
_ = U1 r
forall k (p :: k). U1 p
U1
{-# INLINE gsetters10 #-}
instance Update10 rec => GUpdate10 (Rec1 rec) where
gsetters10 :: (forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> Rec1 rec m -> Rec1 rec m)
-> r a)
-> Rec1 rec r
gsetters10 forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> Rec1 rec m -> Rec1 rec m)
-> r a
r = rec r -> Rec1 rec r
forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1 (rec r -> Rec1 rec r) -> rec r -> Rec1 rec r
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Rep10 rec a -> r a) -> rec r
forall k (f :: (k -> *) -> *) (m :: k -> *).
Representable10 f =>
(forall (a :: k). Rep10 f a -> m a) -> f m
tabulate10 ((forall (a :: k). Rep10 rec a -> r a) -> rec r)
-> (forall (a :: k). Rep10 rec a -> r a) -> rec r
forall a b. (a -> b) -> a -> b
$
\Rep10 rec a
i -> (forall (m :: k -> *). (m a -> m a) -> Rec1 rec m -> Rec1 rec m)
-> r a
forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> Rec1 rec m -> Rec1 rec m)
-> r a
r (\m a -> m a
f -> rec m -> Rec1 rec m
forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1 (rec m -> Rec1 rec m)
-> (Rec1 rec m -> rec m) -> Rec1 rec m -> Rec1 rec m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep10 rec a -> (m a -> m a) -> rec m -> rec m
forall k (f :: (k -> *) -> *) (a :: k) (m :: k -> *).
Update10 f =>
Rep10 f a -> (m a -> m a) -> f m -> f m
overRep10 Rep10 rec a
i m a -> m a
f (rec m -> rec m) -> (Rec1 rec m -> rec m) -> Rec1 rec m -> rec m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec1 rec m -> rec m
forall k (f :: k -> *) (p :: k). Rec1 f p -> f p
unRec1)
{-# INLINE gsetters10 #-}
instance GUpdate10 rec => GUpdate10 (M1 k i rec) where
gsetters10 :: (forall (a :: k).
(forall (m :: k -> *).
(m a -> m a) -> M1 k i rec m -> M1 k i rec m)
-> r a)
-> M1 k i rec r
gsetters10 forall (a :: k).
(forall (m :: k -> *).
(m a -> m a) -> M1 k i rec m -> M1 k i rec m)
-> r a
r = rec r -> M1 k i rec r
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (rec r -> M1 k i rec r) -> rec r -> M1 k i rec r
forall a b. (a -> b) -> a -> b
$ (forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> rec m -> rec m) -> r a)
-> rec r
forall k (rec :: (k -> *) -> *) (r :: k -> *).
GUpdate10 rec =>
(forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> rec m -> rec m) -> r a)
-> rec r
gsetters10 (\forall (m :: k -> *). (m a -> m a) -> rec m -> rec m
s -> (forall (m :: k -> *).
(m a -> m a) -> M1 k i rec m -> M1 k i rec m)
-> r a
forall (a :: k).
(forall (m :: k -> *).
(m a -> m a) -> M1 k i rec m -> M1 k i rec m)
-> r a
r ((forall (m :: k -> *).
(m a -> m a) -> M1 k i rec m -> M1 k i rec m)
-> r a)
-> (forall (m :: k -> *).
(m a -> m a) -> M1 k i rec m -> M1 k i rec m)
-> r a
forall a b. (a -> b) -> a -> b
$ \m a -> m a
f -> rec m -> M1 k i rec m
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (rec m -> M1 k i rec m)
-> (M1 k i rec m -> rec m) -> M1 k i rec m -> M1 k i rec m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m a -> m a) -> rec m -> rec m
forall (m :: k -> *). (m a -> m a) -> rec m -> rec m
s m a -> m a
f (rec m -> rec m)
-> (M1 k i rec m -> rec m) -> M1 k i rec m -> rec m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 k i rec m -> rec m
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1 )
{-# INLINE gsetters10 #-}
instance (GUpdate10 f, GUpdate10 g) => GUpdate10 (f :*: g) where
gsetters10 :: (forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> (:*:) f g m -> (:*:) f g m)
-> r a)
-> (:*:) f g r
gsetters10 forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> (:*:) f g m -> (:*:) f g m)
-> r a
r = f r
fs f r -> g r -> (:*:) f g r
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g r
gs
where
fs :: f r
fs = (forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> f m -> f m) -> r a)
-> f r
forall k (rec :: (k -> *) -> *) (r :: k -> *).
GUpdate10 rec =>
(forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> rec m -> rec m) -> r a)
-> rec r
gsetters10 ((forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> f m -> f m) -> r a)
-> f r)
-> (forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> f m -> f m) -> r a)
-> f r
forall a b. (a -> b) -> a -> b
$ \forall (m :: k -> *). (m a -> m a) -> f m -> f m
s -> (forall (m :: k -> *). (m a -> m a) -> (:*:) f g m -> (:*:) f g m)
-> r a
forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> (:*:) f g m -> (:*:) f g m)
-> r a
r ((forall (m :: k -> *). (m a -> m a) -> (:*:) f g m -> (:*:) f g m)
-> r a)
-> (forall (m :: k -> *).
(m a -> m a) -> (:*:) f g m -> (:*:) f g m)
-> r a
forall a b. (a -> b) -> a -> b
$ (f m -> f m) -> (:*:) f g m -> (:*:) f g m
forall k (f :: k -> *) (m :: k) (g :: k -> *).
(f m -> f m) -> (:*:) f g m -> (:*:) f g m
mapStarFst ((f m -> f m) -> (:*:) f g m -> (:*:) f g m)
-> ((m a -> m a) -> f m -> f m)
-> (m a -> m a)
-> (:*:) f g m
-> (:*:) f g m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m a -> m a) -> f m -> f m
forall (m :: k -> *). (m a -> m a) -> f m -> f m
s
gs :: g r
gs = (forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> g m -> g m) -> r a)
-> g r
forall k (rec :: (k -> *) -> *) (r :: k -> *).
GUpdate10 rec =>
(forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> rec m -> rec m) -> r a)
-> rec r
gsetters10 ((forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> g m -> g m) -> r a)
-> g r)
-> (forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> g m -> g m) -> r a)
-> g r
forall a b. (a -> b) -> a -> b
$ \forall (m :: k -> *). (m a -> m a) -> g m -> g m
s -> (forall (m :: k -> *). (m a -> m a) -> (:*:) f g m -> (:*:) f g m)
-> r a
forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> (:*:) f g m -> (:*:) f g m)
-> r a
r ((forall (m :: k -> *). (m a -> m a) -> (:*:) f g m -> (:*:) f g m)
-> r a)
-> (forall (m :: k -> *).
(m a -> m a) -> (:*:) f g m -> (:*:) f g m)
-> r a
forall a b. (a -> b) -> a -> b
$ (g m -> g m) -> (:*:) f g m -> (:*:) f g m
forall k (g :: k -> *) (m :: k) (f :: k -> *).
(g m -> g m) -> (:*:) f g m -> (:*:) f g m
mapStarSnd ((g m -> g m) -> (:*:) f g m -> (:*:) f g m)
-> ((m a -> m a) -> g m -> g m)
-> (m a -> m a)
-> (:*:) f g m
-> (:*:) f g m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m a -> m a) -> g m -> g m
forall (m :: k -> *). (m a -> m a) -> g m -> g m
s
{-# INLINE gsetters10 #-}
instance (Update f, GUpdate10 g) => GUpdate10 (f :.: g) where
gsetters10 :: (forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> (:.:) f g m -> (:.:) f g m)
-> r a)
-> (:.:) f g r
gsetters10 forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> (:.:) f g m -> (:.:) f g m)
-> r a
r = f (g r) -> (:.:) f g r
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (f (g r) -> (:.:) f g r) -> f (g r) -> (:.:) f g r
forall a b. (a -> b) -> a -> b
$
(Rep f -> g r) -> f (g r)
forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
tabulate ((Rep f -> g r) -> f (g r)) -> (Rep f -> g r) -> f (g r)
forall a b. (a -> b) -> a -> b
$ \ Rep f
i ->
(forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> g m -> g m) -> r a)
-> g r
forall k (rec :: (k -> *) -> *) (r :: k -> *).
GUpdate10 rec =>
(forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> rec m -> rec m) -> r a)
-> rec r
gsetters10 ((forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> g m -> g m) -> r a)
-> g r)
-> (forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> g m -> g m) -> r a)
-> g r
forall a b. (a -> b) -> a -> b
$ \ forall (m :: k -> *). (m a -> m a) -> g m -> g m
s ->
(forall (m :: k -> *). (m a -> m a) -> (:.:) f g m -> (:.:) f g m)
-> r a
forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> (:.:) f g m -> (:.:) f g m)
-> r a
r ((forall (m :: k -> *). (m a -> m a) -> (:.:) f g m -> (:.:) f g m)
-> r a)
-> (forall (m :: k -> *).
(m a -> m a) -> (:.:) f g m -> (:.:) f g m)
-> r a
forall a b. (a -> b) -> a -> b
$ \m a -> m a
f -> f (g m) -> (:.:) f g m
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (f (g m) -> (:.:) f g m)
-> ((:.:) f g m -> f (g m)) -> (:.:) f g m -> (:.:) f g m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep f -> (g m -> g m) -> f (g m) -> f (g m)
forall (f :: * -> *) a. Update f => Rep f -> (a -> a) -> f a -> f a
overRep Rep f
i ((m a -> m a) -> g m -> g m
forall (m :: k -> *). (m a -> m a) -> g m -> g m
s m a -> m a
f) (f (g m) -> f (g m))
-> ((:.:) f g m -> f (g m)) -> (:.:) f g m -> f (g m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:.:) f g m -> f (g m)
forall k2 (f :: k2 -> *) k1 (g :: k1 -> k2) (p :: k1).
(:.:) f g p -> f (g p)
unComp1
{-# INLINE gsetters10 #-}
newtype FieldSetter10 f a = FS10
{ FieldSetter10 f a
-> forall (m :: k -> *). (m a -> m a) -> f m -> f m
runFS10 :: forall m. (m a -> m a) -> f m -> f m }
setters10 :: (Generic1 f, GUpdate10 (Rep1 f)) => f (FieldSetter10 f)
setters10 :: f (FieldSetter10 f)
setters10 = Rep1 f (FieldSetter10 f) -> f (FieldSetter10 f)
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
to1 (Rep1 f (FieldSetter10 f) -> f (FieldSetter10 f))
-> Rep1 f (FieldSetter10 f) -> f (FieldSetter10 f)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> Rep1 f m -> Rep1 f m)
-> FieldSetter10 f a)
-> Rep1 f (FieldSetter10 f)
forall k (rec :: (k -> *) -> *) (r :: k -> *).
GUpdate10 rec =>
(forall (a :: k).
(forall (m :: k -> *). (m a -> m a) -> rec m -> rec m) -> r a)
-> rec r
gsetters10 (\forall (m :: k -> *). (m a -> m a) -> Rep1 f m -> Rep1 f m
overI -> (forall (m :: k -> *). (m a -> m a) -> f m -> f m)
-> FieldSetter10 f a
forall k (f :: (k -> *) -> *) (a :: k).
(forall (m :: k -> *). (m a -> m a) -> f m -> f m)
-> FieldSetter10 f a
FS10 ((forall (m :: k -> *). (m a -> m a) -> f m -> f m)
-> FieldSetter10 f a)
-> (forall (m :: k -> *). (m a -> m a) -> f m -> f m)
-> FieldSetter10 f a
forall a b. (a -> b) -> a -> b
$ \m a -> m a
f -> Rep1 f m -> f m
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
to1 (Rep1 f m -> f m) -> (f m -> Rep1 f m) -> f m -> f m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m a -> m a) -> Rep1 f m -> Rep1 f m
forall (m :: k -> *). (m a -> m a) -> Rep1 f m -> Rep1 f m
overI m a -> m a
f (Rep1 f m -> Rep1 f m) -> (f m -> Rep1 f m) -> f m -> Rep1 f m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f m -> Rep1 f m
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1)