{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Generic.Data.Surgery.Internal where
import Control.Monad ((<=<))
import Data.Bifunctor (bimap, first)
import Data.Coerce
import Data.Functor.Identity (Identity)
import Data.Kind (Constraint, Type)
import Data.Type.Equality (type (==))
import GHC.Generics
import GHC.TypeLits
import Fcf
( Eval, If, _If, IsBool, Pure, Pure2, Bimap, Uncurry
, type (=<<), type (<=<), type (<$>)
)
import Generic.Data.Internal.Compat (Div)
import Generic.Data.Internal.Data (Data(Data,unData))
import Generic.Data.Internal.Meta (MetaOf, MetaConsName, UnM1)
import Generic.Data.Internal.Utils (coerce', absurd1)
newtype OR (l :: k -> Type) (x :: k) = OR { unOR :: l x }
toOR :: forall a l x. (Generic a, ToORRep a l) => a -> OR l x
toOR = OR . gLinearize . from
fromOR' :: forall f l x. FromOR f l => OR l x -> Data f x
fromOR' = Data . gArborify . unOR
toOR' :: forall f l x. ToOR f l => Data f x -> OR l x
toOR' = OR . gLinearize . unData
fromOR :: forall a l x. (Generic a, FromORRep a l) => OR l x -> a
fromOR = to . gArborify . unOR
type OROf a = OR (Linearize (Rep a)) ()
type ToORRep a l = ToOR (Rep a) l
type FromORRep a l = FromOR (Rep a) l
type ToOR f l = (GLinearize f, Linearize f ~ l, f ~ Arborify l)
type FromOR f l = (GArborify f, Linearize f ~ l, f ~ Arborify l)
removeCField
:: forall n t lt l x
. RmvCField n t lt l
=> OR lt x -> (t, OR l x)
removeCField (OR a) = OR <$> gRemoveField @n a
removeRField
:: forall fd n t lt l x
. RmvRField fd n t lt l
=> OR lt x -> (t, OR l x)
removeRField (OR a) = OR <$> gRemoveField @n a
insertCField
:: forall n t lt l x
. InsCField n t lt l
=> (t, OR l x) -> OR lt x
insertCField = uncurry (insertCField' @n)
insertCField'
:: forall n t lt l x
. InsCField n t lt l
=> t -> OR l x -> OR lt x
insertCField' z (OR a) = OR (gInsertField @n z a)
insertRField
:: forall fd n t lt l x
. InsRField fd n t lt l
=> (t, OR l x) -> OR lt x
insertRField = uncurry (insertRField' @fd)
insertRField'
:: forall fd n t lt l x
. InsRField fd n t lt l
=> t -> OR l x -> OR lt x
insertRField' z (OR a) = OR (gInsertField @n z a)
modifyCField
:: forall n t t' lt lt' l x
. ModCField n t t' lt lt' l
=> (t -> t') -> OR lt x -> OR lt' x
modifyCField f = insertCField @n @t' . first f . removeCField @n @t
modifyRField
:: forall fd n t t' lt lt' l x
. ModRField fd n t t' lt lt' l
=> (t -> t') -> OR lt x -> OR lt' x
modifyRField f = insertRField @fd @n @t' . first f . removeRField @fd @n @t
removeConstr
:: forall c n t lc l l_t x
. RmvConstr c n t lc l l_t
=> OR lc x -> Either t (OR l x)
removeConstr (OR a) = bimap
(to . coerce' . gArborify @(Arborify l_t)) OR (gRemoveConstr @n a)
removeConstrT
:: forall c n t lc l l_t x
. RmvConstrT c n t lc l l_t
=> OR lc x -> Either t (OR l x)
removeConstrT = removeConstr @c @n @t
insertConstr
:: forall c n t lc l l_t x
. InsConstr c n t lc l l_t
=> Either t (OR l x) -> OR lc x
insertConstr z =
OR (gInsertConstr @n
(bimap (gLinearize @(Arborify l_t) . coerce' . from) unOR z))
insertConstrT
:: forall c n t lc l l_t x
. InsConstrT c n t lc l l_t
=> Either t (OR l x) -> OR lc x
insertConstrT = insertConstr @c @n @t
modifyConstr
:: forall c n t t' lc lc' l l_t l_t' x
. ModConstr c n t t' lc lc' l l_t l_t'
=> (t -> t') -> OR lc x -> OR lc' x
modifyConstr f = insertConstr @c @n @t' . first f . removeConstr @c @n @t
modifyConstrT
:: forall c n t t' lc lc' l l_t l_t' x
. ModConstrT c n t t' lc lc' l l_t l_t'
=> (t -> t') -> OR lc x -> OR lc' x
modifyConstrT = modifyConstr @c @n @t @t'
type RmvCField n t lt l =
( GRemoveField n lt
, CFieldSurgery n t lt l
)
type RmvRField fd n t lt l =
( GRemoveField n lt
, RFieldSurgery fd n t lt l
)
type InsCField n t lt l =
( GInsertField n lt
, CFieldSurgery n t lt l
)
type InsRField fd n t lt l =
( GInsertField n lt
, RFieldSurgery fd n t lt l
)
type ModCField n t t' lt lt' l =
( RmvCField n t lt l
, InsCField n t' lt' l
)
type ModRField fd n t t' lt lt' l =
( RmvRField fd n t lt l
, InsRField fd n t' lt' l
)
type RmvConstr c n t lc l l_t =
( GRemoveConstr n lc
, GArborify (Arborify l_t)
, ConstrSurgery c n t lc l l_t
)
type RmvConstrT c n t lc l l_t =
( RmvConstr c n t lc l l_t
, IsTuple (Arity l_t) t
)
type InsConstr c n t lc l l_t =
( GInsertConstr n lc
, GLinearize (Arborify l_t)
, ConstrSurgery c n t lc l l_t
)
type InsConstrT c n t lc l l_t =
( InsConstr c n t lc l l_t
, IsTuple (Arity l_t) t
)
type ModConstr c n t t' lc lc' l l_t l_t' =
( RmvConstr c n t lc l l_t
, InsConstr c n t' lc' l l_t'
)
type ModConstrT c n t t' lc lc' l l_t l_t' =
( ModConstr c n t t' lc lc' l l_t l_t'
, IsTuple (Arity l_t) t
, IsTuple (Arity l_t') t'
)
type FieldSurgery n t lt l =
( t ~ Eval (FieldTypeAt n lt)
, l ~ Eval (RemoveField n lt)
)
type CFieldSurgery n t lt l =
( lt ~ Eval (InsertField n 'Nothing t l)
, FieldSurgery n t lt l
)
type RFieldSurgery fd n t lt l =
( n ~ Eval (FieldIndex fd lt)
, lt ~ Eval (InsertField n ('Just fd) t l)
, FieldSurgery n t lt l
)
type ConstrSurgery c n t lc l l_t =
( Generic t
, MatchFields (UnM1 (Rep t)) (Arborify l_t)
, Coercible (Arborify l_t) (Rep t)
, n ~ Eval (ConstrIndex c lc)
, c ~ MetaConsName (MetaOf l_t)
, l_t ~ Linearize (Arborify l_t)
, l_t ~ Eval (ConstrAt n lc)
, lc ~ Eval (InsertConstr n l_t l)
, l ~ Eval (RemoveConstr n lc)
)
type family Linearize (f :: k -> *) :: k -> *
type instance Linearize (M1 D m f) = M1 D m (LinearizeSum f V1)
type instance Linearize (M1 C m f) = M1 C m (LinearizeProduct f U1)
type family LinearizeSum (f :: k -> *) (tl :: k -> *) :: k -> *
type instance LinearizeSum V1 tl = tl
type instance LinearizeSum (f :+: g) tl = LinearizeSum f (LinearizeSum g tl)
type instance LinearizeSum (M1 c m f) tl = M1 c m (LinearizeProduct f U1) :+: tl
type family LinearizeProduct (f :: k -> *) (tl :: k -> *) :: k -> *
type instance LinearizeProduct U1 tl = tl
type instance LinearizeProduct (f :*: g) tl = LinearizeProduct f (LinearizeProduct g tl)
type instance LinearizeProduct (M1 s m f) tl = M1 s m f :*: tl
class GLinearize f where
gLinearize :: f x -> Linearize f x
instance GLinearizeSum f V1 => GLinearize (M1 D m f) where
gLinearize (M1 a) = M1 (gLinearizeSum @_ @V1 (Left a))
instance GLinearizeProduct f U1 => GLinearize (M1 C m f) where
gLinearize (M1 a) = M1 (gLinearizeProduct a U1)
class GLinearizeSum f tl where
gLinearizeSum :: Either (f x) (tl x) -> LinearizeSum f tl x
instance GLinearizeSum V1 tl where
gLinearizeSum (Left v) = absurd1 v
gLinearizeSum (Right c) = c
instance (GLinearizeSum g tl, GLinearizeSum f (LinearizeSum g tl))
=> GLinearizeSum (f :+: g) tl where
gLinearizeSum (Left (L1 a)) = gLinearizeSum @_ @(LinearizeSum g tl) (Left a)
gLinearizeSum (Left (R1 b)) = gLinearizeSum @f (Right (gLinearizeSum @g @tl (Left b)))
gLinearizeSum (Right c) = gLinearizeSum @f (Right (gLinearizeSum @g (Right c)))
instance GLinearizeProduct f U1 => GLinearizeSum (M1 c m f) tl where
gLinearizeSum (Left (M1 a)) = L1 (M1 (gLinearizeProduct a U1))
gLinearizeSum (Right c) = R1 c
class GLinearizeProduct f tl where
gLinearizeProduct :: f x -> tl x -> LinearizeProduct f tl x
instance GLinearizeProduct U1 tl where
gLinearizeProduct _ = id
instance (GLinearizeProduct g tl, GLinearizeProduct f (LinearizeProduct g tl))
=> GLinearizeProduct (f :*: g) tl where
gLinearizeProduct (a :*: b) = gLinearizeProduct a . gLinearizeProduct b
instance GLinearizeProduct (M1 s m f) tl where
gLinearizeProduct = (:*:)
class GArborify f where
gArborify :: Linearize f x -> f x
instance GArborifySum f V1 => GArborify (M1 D m f) where
gArborify (M1 a) = case gArborifySum @_ @V1 a of
Left a' -> M1 a'
Right v -> absurd1 v
instance GArborifyProduct f U1 => GArborify (M1 C m f) where
gArborify (M1 a) = M1 (fst (gArborifyProduct @_ @U1 a))
class GArborifySum f tl where
gArborifySum :: LinearizeSum f tl x -> Either (f x) (tl x)
instance GArborifySum V1 tl where
gArborifySum = Right
instance (GArborifySum g tl, GArborifySum f (LinearizeSum g tl))
=> GArborifySum (f :+: g) tl where
gArborifySum = first R1 . gArborifySum <=< first L1 . gArborifySum
instance GArborifyProduct f U1 => GArborifySum (M1 c m f) tl where
gArborifySum (L1 (M1 a)) = Left (M1 (fst (gArborifyProduct @_ @U1 a)))
gArborifySum (R1 c) = Right c
class GArborifyProduct f tl where
gArborifyProduct :: LinearizeProduct f tl x -> (f x, tl x)
instance GArborifyProduct U1 tl where
gArborifyProduct c = (U1, c)
instance (GArborifyProduct g tl, GArborifyProduct f (LinearizeProduct g tl))
=> GArborifyProduct (f :*: g) tl where
gArborifyProduct abc = (a :*: b, c) where
(a, bc) = gArborifyProduct abc
(b, c) = gArborifyProduct bc
instance GArborifyProduct (M1 s m f) tl where
gArborifyProduct (a :*: c) = (a, c)
type family Arborify (f :: k -> *) :: k -> *
type instance Arborify (M1 D m f) = M1 D m (Eval (ArborifySum (CoArity f) f))
type instance Arborify (M1 C m f) = M1 C m (Eval (ArborifyProduct (Arity f) f))
data ArborifySum (n :: Nat) (f :: k -> *) :: (k -> *) -> *
type instance Eval (ArborifySum n V1) = V1
type instance Eval (ArborifySum n (f :+: g)) =
Eval (If (n == 1)
(ArborifyProduct (Arity f) f)
(Arborify' ArborifySum (:+:) n (Div n 2) f g))
data ArborifyProduct (n :: Nat) (f :: k -> *) :: (k -> *) -> *
type instance Eval (ArborifyProduct n (M1 C s f)) = M1 C s (Eval (ArborifyProduct n f))
type instance Eval (ArborifyProduct n U1) = U1
type instance Eval (ArborifyProduct n (f :*: g)) =
Eval (If (n == 1)
(Pure f)
(Arborify' ArborifyProduct (:*:) n (Div n 2) f g))
type Arborify' arb op n nDiv2 f g =
( Uncurry (Pure2 op)
<=< Bimap (arb nDiv2) (arb (n-nDiv2))
<=< SplitAt nDiv2
) (op f g)
data SplitAt :: Nat -> (k -> *) -> (k -> *, k -> *) -> *
type instance Eval (SplitAt n (f :+: g)) =
Eval (If (n == 0)
(Pure '(V1, f :+: g))
(Bimap (Pure2 (:+:) f) Pure =<< SplitAt (n-1) g))
type instance Eval (SplitAt n (f :*: g)) =
Eval (If (n == 0)
(Pure '(U1, f :*: g))
(Bimap (Pure2 (:*:) f) Pure =<< SplitAt (n-1) g))
data FieldTypeAt (n :: Nat) (f :: k -> *) :: * -> *
type instance Eval (FieldTypeAt n (M1 i c f)) = Eval (FieldTypeAt n f)
type instance Eval (FieldTypeAt n (f :+: V1)) = Eval (FieldTypeAt n f)
type instance Eval (FieldTypeAt n (f :*: g)) =
Eval (If (n == 0) (Pure (FieldTypeOf f)) (FieldTypeAt (n-1) g))
type family FieldTypeOf (f :: k -> *) :: *
type instance FieldTypeOf (M1 s m (K1 i a)) = a
data RemoveField (n :: Nat) (f :: k -> *) :: (k -> *) -> *
type instance Eval (RemoveField n (M1 i m f)) = M1 i m (Eval (RemoveField n f))
type instance Eval (RemoveField n (f :+: V1)) = Eval (RemoveField n f) :+: V1
type instance Eval (RemoveField n (f :*: g)) =
Eval (If (n == 0) (Pure g) ((:*:) f <$> RemoveField (n-1) g))
type DefaultMetaSel field
= 'MetaSel field 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy
data InsertField (n :: Nat) (fd :: Maybe Symbol) (t :: *) (f :: k -> *) :: (k -> *) -> *
type instance Eval (InsertField n fd t (M1 D m f)) = M1 D m (Eval (InsertField n fd t f))
type instance Eval (InsertField n fd t (M1 C m f)) = M1 C m (Eval (InsertField n fd t f))
type instance Eval (InsertField n fd t (f :+: V1)) = Eval (InsertField n fd t f) :+: V1
type instance Eval (InsertField n fd t (f :*: g)) =
Eval (If (n == 0)
(Pure (M1 S (DefaultMetaSel fd) (K1 R t) :*: (f :*: g)))
((:*:) f <$> InsertField (n-1) fd t g))
type instance Eval (InsertField 0 fd t U1) = M1 S (DefaultMetaSel fd) (K1 R t) :*: U1
data Succ :: Nat -> Nat -> *
type instance Eval (Succ n) = 1 + n
data FieldIndex (field :: Symbol) (f :: k -> *) :: Nat -> *
type instance Eval (FieldIndex field (M1 D m f)) = Eval (FieldIndex field f)
type instance Eval (FieldIndex field (M1 C m f)) = Eval (FieldIndex field f)
type instance Eval (FieldIndex field (f :+: V1)) = Eval (FieldIndex field f)
type instance Eval (FieldIndex field (M1 S ('MetaSel ('Just field') su ss ds) f :*: g))
= Eval (If (field == field') (Pure 0) (Succ =<< FieldIndex field g))
type family Arity (f :: k -> *) :: Nat
type instance Arity (M1 d m f) = Arity f
type instance Arity (f :+: V1) = Arity f
type instance Arity (f :*: g) = Arity f + Arity g
type instance Arity (K1 i c) = 1
type instance Arity U1 = 0
type family CoArity (f :: k -> *) :: Nat
type instance CoArity (M1 D m f) = CoArity f
type instance CoArity (M1 C m f) = 1
type instance CoArity V1 = 0
type instance CoArity (f :+: g) = CoArity f + CoArity g
class GRemoveField (n :: Nat) f where
gRemoveField :: f x -> (Eval (FieldTypeAt n f), Eval (RemoveField n f) x)
instance GRemoveField n f => GRemoveField n (M1 i c f) where
gRemoveField (M1 a) = M1 <$> gRemoveField @n a
instance GRemoveField n f => GRemoveField n (f :+: V1) where
gRemoveField (L1 a) = L1 <$> gRemoveField @n a
gRemoveField (R1 v) = absurd1 v
instance (If (n == 0) (() :: Constraint) (GRemoveField (n-1) g), IsBool (n == 0))
=> GRemoveField n (M1 s m (K1 i t) :*: g) where
gRemoveField (a@(M1 (K1 t)) :*: b) = _If @(n == 0)
(t, b)
((a :*:) <$> gRemoveField @(n-1) b)
class GInsertField (n :: Nat) f where
gInsertField :: Eval (FieldTypeAt n f) -> Eval (RemoveField n f) x -> f x
instance GInsertField n f => GInsertField n (M1 i c f) where
gInsertField t (M1 a) = M1 (gInsertField @n t a)
instance GInsertField n f => GInsertField n (f :+: V1) where
gInsertField t (L1 a) = L1 (gInsertField @n t a)
gInsertField _ (R1 v) = absurd1 v
instance (If (n == 0) (() :: Constraint) (GInsertField (n-1) g), IsBool (n == 0))
=> GInsertField n (M1 s m (K1 i t) :*: g) where
gInsertField t ab = _If @(n == 0)
(M1 (K1 t) :*: ab)
(let a :*: b = ab in a :*: gInsertField @(n-1) t b)
data ConstrAt (n :: Nat) (f :: k -> *) :: (k -> *) -> *
type instance Eval (ConstrAt n (M1 i m f)) = Eval (ConstrAt n f)
type instance Eval (ConstrAt n (f :+: g)) =
Eval (If (n == 0) (Pure f) (ConstrAt (n-1) g))
data RemoveConstr (n :: Nat) (f :: k -> *) :: (k -> *) -> *
type instance Eval (RemoveConstr n (M1 i m f)) = M1 i m (Eval (RemoveConstr n f))
type instance Eval (RemoveConstr n (f :+: g)) =
Eval (If (n == 0) (Pure g) ((:+:) f <$> RemoveConstr (n-1) g))
data InsertConstr (n :: Nat) (t :: k -> *) (f :: k -> *) :: (k -> *) -> *
type instance Eval (InsertConstr n t (M1 i m f)) = M1 i m (Eval (InsertConstr n t f))
type instance Eval (InsertConstr n t (f :+: g)) =
Eval (If (n == 0) (Pure (t :+: (f :+: g))) ((:+:) f <$> InsertConstr (n-1) t g))
type instance Eval (InsertConstr 0 t V1) = t :+: V1
data ConstrIndex (con :: Symbol) (f :: k -> *) :: Nat -> *
type instance Eval (ConstrIndex con (M1 D m f)) = Eval (ConstrIndex con f)
type instance Eval (ConstrIndex con (M1 C ('MetaCons con' fx s) f :+: g)) =
Eval (If (con == con') (Pure 0) (Succ =<< ConstrIndex con g))
class GRemoveConstr (n :: Nat) f where
gRemoveConstr :: f x -> Either (Eval (ConstrAt n f) x) (Eval (RemoveConstr n f) x)
instance GRemoveConstr n f => GRemoveConstr n (M1 i c f) where
gRemoveConstr (M1 a) = M1 <$> gRemoveConstr @n a
instance (If (n == 0) (() :: Constraint) (GRemoveConstr (n-1) g), IsBool (n == 0))
=> GRemoveConstr n (f :+: g) where
gRemoveConstr = _If @(n == 0)
(\case
L1 a -> Left a
R1 b -> Right b)
(\case
L1 a -> Right (L1 a)
R1 b -> R1 <$> gRemoveConstr @(n-1) b)
class GInsertConstr (n :: Nat) f where
gInsertConstr :: Either (Eval (ConstrAt n f) x) (Eval (RemoveConstr n f) x) -> f x
instance GInsertConstr n f => GInsertConstr n (M1 i c f) where
gInsertConstr = M1 . gInsertConstr @n . fmap unM1
instance (If (n == 0) (() :: Constraint) (GInsertConstr (n-1) g), IsBool (n == 0))
=> GInsertConstr n (f :+: g) where
gInsertConstr = _If @(n == 0)
(\case
Left a -> L1 a
Right b -> R1 b)
(\case
Left a -> R1 (gInsertConstr @(n-1) (Left a))
Right (L1 a) -> L1 a
Right (R1 b) -> R1 (gInsertConstr @(n-1) (Right b)))
class MatchFields (f :: k -> *) (g :: k -> *)
instance (g' ~ M1 D d g, MatchFields f g) => MatchFields (M1 D c f) g'
instance (g' ~ M1 C ('MetaCons _cn _s _t) g, MatchFields f g)
=> MatchFields (M1 C c f) g'
instance (g' ~ M1 S d g, MatchFields f g) => MatchFields (M1 S c f) g'
instance (g' ~ (g1 :+: g2), MatchFields f1 g1, MatchFields f2 g2)
=> MatchFields (f1 :+: f2) g'
instance (g' ~ (g1 :*: g2), MatchFields f1 g1, MatchFields f2 g2)
=> MatchFields (f1 :*: f2) g'
instance (g' ~ K1 j a) => MatchFields (K1 i a) g'
instance (g' ~ U1) => MatchFields U1 g'
instance (g' ~ V1) => MatchFields V1 g'
class IsTuple (n :: Nat) (t :: k)
instance (t ~ ()) => IsTuple 0 t
instance (t ~ Identity a) => IsTuple 1 t
instance (t ~ (a, b)) => IsTuple 2 t
instance (t ~ (a, b, c)) => IsTuple 3 t
instance (t ~ (a, b, c, d)) => IsTuple 4 t
instance (t ~ (a, b, c, d, e)) => IsTuple 5 t
instance (t ~ (a, b, c, d, e, f)) => IsTuple 6 t
instance (t ~ (a, b, c, d, e, f, g)) => IsTuple 7 t