{-# LANGUAGE UndecidableInstances #-}

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

{- |
Copyright   :  (c) 2023 Yamada Ryo
License     :  MPL-2.0 (see the file LICENSE)
Maintainer  :  ymdfield@outlook.jp
Stability   :  experimental
Portability :  portable

An implementation of an open union for higher-order effects using
the [extensible](https://hackage.haskell.org/package/extensible) package as a backend.
-}
module Data.Hefty.Extensible where

import Control.Effect.Class (Signature)
import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap)
import Data.Extensible (Forall, Match (Match), htabulateFor, leadership, match)
import Data.Extensible.Sum (exhaust, strikeAt, (<:|), type (:/) (EmbedAt))
import Data.Free.Extensible (TypeIndex, findFirstMembership)
import Data.Hefty.Union (
    UnionH (
        HasMembershipH,
        absurdUnionH,
        inject0H,
        injectH,
        projectH,
        weakenH,
        (|+:)
    ),
 )
import Data.Proxy (Proxy (Proxy))
import GHC.TypeNats (KnownNat)
import Type.Membership (nextMembership)

{- |
An implementation of an open union for higher-order effects using
the [extensible](https://hackage.haskell.org/package/extensible) package as a backend.
-}
newtype ExtensibleUnionH hs f a = ExtensibleUnionH {forall (hs :: [Signature]) (f :: * -> *) a.
ExtensibleUnionH hs f a -> hs :/ FieldAppH f a
unExtensibleUnionH :: hs :/ FieldAppH f a}

newtype FieldAppH f a (h :: Signature) = FieldAppH {forall (f :: * -> *) a (h :: Signature). FieldAppH f a h -> h f a
unFieldAppH :: h f a}

instance Forall HFunctor hs => HFunctor (ExtensibleUnionH hs) where
    hfmap :: forall (f :: * -> *) (g :: * -> *).
(f :-> g) -> ExtensibleUnionH hs f :-> ExtensibleUnionH hs g
hfmap f :-> g
f =
        forall (hs :: [Signature]) (f :: * -> *) a.
(hs :/ FieldAppH f a) -> ExtensibleUnionH hs f a
ExtensibleUnionH
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (xs :: [k]) (h :: k -> *) a.
(xs :& Match h a) -> (xs :/ h) -> a
match
                ( forall {k} (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (h :: k -> *).
Forall c xs =>
proxy c
-> (forall (x :: k). c x => Membership xs x -> h x) -> xs :& h
htabulateFor @HFunctor forall {k} (t :: k). Proxy t
Proxy \Membership hs x
w ->
                    forall {k} (h :: k -> *) r (x :: k). (h x -> r) -> Match h r x
Match forall a b. (a -> b) -> a -> b
$ forall {k} (xs :: [k]) (x :: k) (h :: k -> *).
Membership xs x -> h x -> xs :/ h
EmbedAt Membership hs x
w forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a (h :: Signature). h f a -> FieldAppH f a h
FieldAppH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: Signature) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap f :-> g
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a (h :: Signature). FieldAppH f a h -> h f a
unFieldAppH
                )
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (hs :: [Signature]) (f :: * -> *) a.
ExtensibleUnionH hs f a -> hs :/ FieldAppH f a
unExtensibleUnionH
    {-# INLINE hfmap #-}

-- todo: Functor, Foldable, Traversable instances

instance UnionH ExtensibleUnionH where
    type HasMembershipH _ h hs = KnownNat (TypeIndex hs h)

    injectH :: forall (h :: Signature) (hs :: [Signature]) (f :: * -> *).
HasMembershipH ExtensibleUnionH h hs =>
h f ~> ExtensibleUnionH hs f
injectH = forall (hs :: [Signature]) (f :: * -> *) a.
(hs :/ FieldAppH f a) -> ExtensibleUnionH hs f a
ExtensibleUnionH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (xs :: [k]) (x :: k) (h :: k -> *).
Membership xs x -> h x -> xs :/ h
EmbedAt forall {k} (xs :: [k]) (x :: k).
KnownNat (TypeIndex xs x) =>
Membership xs x
findFirstMembership forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a (h :: Signature). h f a -> FieldAppH f a h
FieldAppH
    {-# INLINE injectH #-}

    projectH :: forall (h :: Signature) (hs :: [Signature]) (f :: * -> *) a.
HasMembershipH ExtensibleUnionH h hs =>
ExtensibleUnionH hs f a -> Maybe (h f a)
projectH (ExtensibleUnionH hs :/ FieldAppH f a
u) = forall (f :: * -> *) a (h :: Signature). FieldAppH f a h -> h f a
unFieldAppH forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (h :: k -> *) (x :: k) (xs :: [k]).
Membership xs x -> (xs :/ h) -> Maybe (h x)
strikeAt forall {k} (xs :: [k]) (x :: k).
KnownNat (TypeIndex xs x) =>
Membership xs x
findFirstMembership hs :/ FieldAppH f a
u
    {-# INLINE projectH #-}

    absurdUnionH :: forall (f :: * -> *) a x. ExtensibleUnionH '[] f a -> x
absurdUnionH = forall {k} (h :: k -> *) r. ('[] :/ h) -> r
exhaust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (hs :: [Signature]) (f :: * -> *) a.
ExtensibleUnionH hs f a -> hs :/ FieldAppH f a
unExtensibleUnionH
    {-# INLINE absurdUnionH #-}

    inject0H :: forall (h :: Signature) (f :: * -> *) (hs :: [Signature]).
h f ~> ExtensibleUnionH (h : hs) f
inject0H = forall (hs :: [Signature]) (f :: * -> *) a.
(hs :/ FieldAppH f a) -> ExtensibleUnionH hs f a
ExtensibleUnionH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (xs :: [k]) (x :: k) (h :: k -> *).
Membership xs x -> h x -> xs :/ h
EmbedAt forall {k} (x :: k) (xs :: [k]). Membership (x : xs) x
leadership forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a (h :: Signature). h f a -> FieldAppH f a h
FieldAppH
    {-# INLINE inject0H #-}

    weakenH :: forall (hs :: [Signature]) (f :: * -> *) (h :: Signature).
ExtensibleUnionH hs f ~> ExtensibleUnionH (h : hs) f
weakenH (ExtensibleUnionH (EmbedAt Membership hs x
w FieldAppH f x x
e)) =
        forall (hs :: [Signature]) (f :: * -> *) a.
(hs :/ FieldAppH f a) -> ExtensibleUnionH hs f a
ExtensibleUnionH forall a b. (a -> b) -> a -> b
$ forall {k} (xs :: [k]) (x :: k) (h :: k -> *).
Membership xs x -> h x -> xs :/ h
EmbedAt (forall {k} (xs :: [k]) (y :: k) (x :: k).
Membership xs y -> Membership (x : xs) y
nextMembership Membership hs x
w) FieldAppH f x x
e
    {-# INLINE weakenH #-}

    h f a -> r
f |+: :: forall (h :: Signature) (f :: * -> *) a r (hs :: [Signature]).
(h f a -> r)
-> (ExtensibleUnionH hs f a -> r)
-> ExtensibleUnionH (h : hs) f a
-> r
|+: ExtensibleUnionH hs f a -> r
g = (h f a -> r
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a (h :: Signature). FieldAppH f a h -> h f a
unFieldAppH forall {k} (h :: k -> *) (x :: k) r (xs :: [k]).
(h x -> r) -> ((xs :/ h) -> r) -> ((x : xs) :/ h) -> r
<:| ExtensibleUnionH hs f a -> r
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (hs :: [Signature]) (f :: * -> *) a.
(hs :/ FieldAppH f a) -> ExtensibleUnionH hs f a
ExtensibleUnionH) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (hs :: [Signature]) (f :: * -> *) a.
ExtensibleUnionH hs f a -> hs :/ FieldAppH f a
unExtensibleUnionH
    {-# INLINE (|+:) #-}