module Language.Parser.Ptera.Data.HFList (
    T,
    HFList (..),
    Membership,

    Concat,
    hconcat,

    hfoldrWithIndex,
    htraverseWithIndex,
    hmapWithIndex,
    hfoldMWithIndex,
    hforMWithIndex,
    hfoldlWithIndex,

    DictF (..),
) where

import           Language.Parser.Ptera.Prelude

import           Type.Membership               (Membership)
import qualified Unsafe.Coerce                 as Unsafe


type T = HFList

data HFList :: (k -> Type) -> [k] -> Type where
    HFNil :: HFList f '[]
    HFCons :: f x -> HFList f xs -> HFList f (x ': xs)


type family Concat (xs1 :: [k]) (xs2 :: [k]) :: [k] where
    Concat '[] xs2 =
        xs2
    Concat (x ': xs1) xs2 =
        x ': Concat xs1 xs2

hconcat :: HFList f xs1 -> HFList f xs2 -> HFList f (Concat xs1 xs2)
hconcat :: forall {k} (f :: k -> *) (xs1 :: [k]) (xs2 :: [k]).
HFList f xs1 -> HFList f xs2 -> HFList f (Concat xs1 xs2)
hconcat HFList f xs1
l1 HFList f xs2
l2 = case HFList f xs1
l1 of
    HFList f xs1
HFNil ->
        HFList f xs2
l2
    HFCons f x
x HFList f xs
l1' ->
        forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
f x -> HFList f xs -> HFList f (x : xs)
HFCons f x
x do forall {k} (f :: k -> *) (xs1 :: [k]) (xs2 :: [k]).
HFList f xs1 -> HFList f xs2 -> HFList f (Concat xs1 xs2)
hconcat HFList f xs
l1' HFList f xs2
l2

hfoldrWithIndex
    :: forall f r xs
    .  (forall x ys. Membership xs x -> f x -> r ys -> r (x ': ys)) -> r '[]
    -> HFList f xs -> r xs
hfoldrWithIndex :: forall {k} (f :: k -> *) (r :: [k] -> *) (xs :: [k]).
(forall (x :: k) (ys :: [k]).
 Membership xs x -> f x -> r ys -> r (x : ys))
-> r '[] -> HFList f xs -> r xs
hfoldrWithIndex forall (x :: k) (ys :: [k]).
Membership xs x -> f x -> r ys -> r (x : ys)
f r '[]
z0 = forall (ys :: [k]). Int -> HFList f ys -> r ys
go Int
0 where
    go :: Int -> HFList f ys -> r ys
    go :: forall (ys :: [k]). Int -> HFList f ys -> r ys
go Int
m0 = \case
        HFList f ys
HFNil ->
            r '[]
z0
        HFCons f x
y HFList f xs
l -> do
            let m1 :: Int
m1 = Int
m0 forall a. Num a => a -> a -> a
+ Int
1
            forall (x :: k) (ys :: [k]).
Membership xs x -> f x -> r ys -> r (x : ys)
f
                do forall {k} (xs :: [k]) (x :: k). Int -> Membership xs x
unsafeMembership Int
m0
                do f x
y
                do forall (ys :: [k]). Int -> HFList f ys -> r ys
go Int
m1 HFList f xs
l

htraverseWithIndex
    :: forall m f g xs
    .  Applicative m
    => (forall x. Membership xs x -> f x -> m (g x))
    -> HFList f xs -> m (HFList g xs)
htraverseWithIndex :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (xs :: [k]).
Applicative m =>
(forall (x :: k). Membership xs x -> f x -> m (g x))
-> HFList f xs -> m (HFList g xs)
htraverseWithIndex forall (x :: k). Membership xs x -> f x -> m (g x)
f = coerce :: forall a b. Coercible a b => a -> b
coerce HFList f xs -> TraverseHFList m g xs
go0 where
    go0 :: HFList f xs -> TraverseHFList m g xs
go0 = forall {k} (f :: k -> *) (r :: [k] -> *) (xs :: [k]).
(forall (x :: k) (ys :: [k]).
 Membership xs x -> f x -> r ys -> r (x : ys))
-> r '[] -> HFList f xs -> r xs
hfoldrWithIndex forall (x :: k) (ys :: [k]).
Membership xs x
-> f x -> TraverseHFList m g ys -> TraverseHFList m g (x : ys)
go do forall {k} (m :: * -> *) (f :: k -> *) (xs :: [k]).
m (HFList f xs) -> TraverseHFList m f xs
TraverseHFList do forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (f :: k -> *). HFList f '[]
HFNil

    go
        :: forall x ys. Membership xs x -> f x
        -> TraverseHFList m g ys -> TraverseHFList m g (x ': ys)
    go :: forall (x :: k) (ys :: [k]).
Membership xs x
-> f x -> TraverseHFList m g ys -> TraverseHFList m g (x : ys)
go Membership xs x
m f x
x = \case
        TraverseHFList m (HFList g ys)
acc0 ->
            forall {k} (m :: * -> *) (f :: k -> *) (xs :: [k]).
m (HFList f xs) -> TraverseHFList m f xs
TraverseHFList do forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
f x -> HFList f xs -> HFList f (x : xs)
HFCons forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (x :: k). Membership xs x -> f x -> m (g x)
f Membership xs x
m f x
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (HFList g ys)
acc0

newtype TraverseHFList m f xs = TraverseHFList (m (HFList f xs))

hmapWithIndex
    :: (forall x. Membership xs x -> f x -> g x)
    -> HFList f xs -> HFList g xs
hmapWithIndex :: forall {k} (xs :: [k]) (f :: k -> *) (g :: k -> *).
(forall (x :: k). Membership xs x -> f x -> g x)
-> HFList f xs -> HFList g xs
hmapWithIndex forall (x :: k). Membership xs x -> f x -> g x
f HFList f xs
l = forall a. Identity a -> a
runIdentity
    do forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (xs :: [k]).
Applicative m =>
(forall (x :: k). Membership xs x -> f x -> m (g x))
-> HFList f xs -> m (HFList g xs)
htraverseWithIndex
        do \Membership xs x
m f x
x -> forall a. a -> Identity a
Identity do forall (x :: k). Membership xs x -> f x -> g x
f Membership xs x
m f x
x
        do HFList f xs
l

hfoldMWithIndex :: forall m r f xs
    .  Monad m
    => r -> (forall x. r -> Membership xs x -> f x -> m r)
    -> HFList f xs -> m r
hfoldMWithIndex :: forall {k} (m :: * -> *) r (f :: k -> *) (xs :: [k]).
Monad m =>
r
-> (forall (x :: k). r -> Membership xs x -> f x -> m r)
-> HFList f xs
-> m r
hfoldMWithIndex r
z0 forall (x :: k). r -> Membership xs x -> f x -> m r
f = forall (ys :: [k]). Int -> r -> HFList f ys -> m r
go Int
0 r
z0 where
    go :: Int -> r -> HFList f ys -> m r
    go :: forall (ys :: [k]). Int -> r -> HFList f ys -> m r
go Int
m1 r
z1 = \case
        HFList f ys
HFNil ->
            forall (f :: * -> *) a. Applicative f => a -> f a
pure r
z1
        HFCons f x
y HFList f xs
l -> do
            r
z2 <- forall (x :: k). r -> Membership xs x -> f x -> m r
f r
z1
                do forall {k} (xs :: [k]) (x :: k). Int -> Membership xs x
unsafeMembership Int
m1
                do f x
y
            let m2 :: Int
m2 = Int
m1 forall a. Num a => a -> a -> a
+ Int
1
            forall (ys :: [k]). Int -> r -> HFList f ys -> m r
go Int
m2 r
z2 HFList f xs
l

hforMWithIndex
    :: forall m f xs
    .  Applicative m
    => HFList f xs -> (forall x. Membership xs x -> f x -> m ()) -> m ()
hforMWithIndex :: forall {k} (m :: * -> *) (f :: k -> *) (xs :: [k]).
Applicative m =>
HFList f xs
-> (forall (x :: k). Membership xs x -> f x -> m ()) -> m ()
hforMWithIndex HFList f xs
l0 forall (x :: k). Membership xs x -> f x -> m ()
f = forall (ys :: [k]). Int -> HFList f ys -> m ()
go Int
0 HFList f xs
l0 where
    go :: Int -> HFList f ys -> m ()
    go :: forall (ys :: [k]). Int -> HFList f ys -> m ()
go Int
m1 = \case
        HFList f ys
HFNil ->
            forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        HFCons f x
y HFList f xs
l -> forall a b. a -> b -> a
const
            forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (x :: k). Membership xs x -> f x -> m ()
f
                do forall {k} (xs :: [k]) (x :: k). Int -> Membership xs x
unsafeMembership Int
m1
                do f x
y
            forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (ys :: [k]). Int -> HFList f ys -> m ()
go
                do Int
m1 forall a. Num a => a -> a -> a
+ Int
1
                HFList f xs
l

hfoldlWithIndex
    :: r -> (forall x. r -> Membership xs x -> f x -> r)
    -> HFList f xs -> r
hfoldlWithIndex :: forall {k} r (xs :: [k]) (f :: k -> *).
r
-> (forall (x :: k). r -> Membership xs x -> f x -> r)
-> HFList f xs
-> r
hfoldlWithIndex r
z0 forall (x :: k). r -> Membership xs x -> f x -> r
f = coerce :: forall a b. Coercible a b => a -> b
coerce
    do forall {k} (m :: * -> *) r (f :: k -> *) (xs :: [k]).
Monad m =>
r
-> (forall (x :: k). r -> Membership xs x -> f x -> m r)
-> HFList f xs
-> m r
hfoldMWithIndex r
z0 \r
z Membership xs x
m f x
x -> forall a. a -> Identity a
Identity do forall (x :: k). r -> Membership xs x -> f x -> r
f r
z Membership xs x
m f x
x


data DictF :: (k -> Constraint) -> k -> Type where
    DictF :: c x => DictF c x


unsafeMembership :: Int -> Membership xs x
unsafeMembership :: forall {k} (xs :: [k]) (x :: k). Int -> Membership xs x
unsafeMembership = forall a b. a -> b
Unsafe.unsafeCoerce