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 :: 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
HFList f (Concat xs1 xs2)
l2
    HFCons f x
x HFList f xs
l1' ->
        f x -> HFList f (Concat xs xs2) -> HFList f (x : Concat xs xs2)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> HFList f xs -> HFList f (x : xs)
HFCons f x
x do HFList f xs -> HFList f xs2 -> HFList f (Concat xs xs2)
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 (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 = Int -> HFList f xs -> r xs
forall (ys :: [k]). Int -> HFList f ys -> r ys
go Int
0 where
    go :: Int -> HFList f ys -> r ys
    go :: Int -> HFList f ys -> r ys
go Int
m0 = \case
        HFList f ys
HFNil ->
            r ys
r '[]
z0
        HFCons f x
y HFList f xs
l -> do
            let m1 :: Int
m1 = Int
m0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
            Membership xs x -> f x -> r xs -> r (x : xs)
forall (x :: k) (ys :: [k]).
Membership xs x -> f x -> r ys -> r (x : ys)
f
                do Int -> Membership xs x
forall k (xs :: [k]) (x :: k). Int -> Membership xs x
unsafeMembership Int
m0
                do f x
y
                do Int -> HFList f xs -> r xs
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 (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 = (HFList f xs -> TraverseHFList m g xs)
-> HFList f xs -> m (HFList g xs)
coerce HFList f xs -> TraverseHFList m g xs
go0 where
    go0 :: HFList f xs -> TraverseHFList m g xs
go0 = (forall (x :: k) (ys :: [k]).
 Membership xs x
 -> f x -> TraverseHFList m g ys -> TraverseHFList m g (x : ys))
-> TraverseHFList m g '[] -> HFList f xs -> TraverseHFList m g xs
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 m (HFList g '[]) -> TraverseHFList m g '[]
forall k (m :: * -> *) (f :: k -> *) (xs :: [k]).
m (HFList f xs) -> TraverseHFList m f xs
TraverseHFList do HFList g '[] -> m (HFList g '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure HFList g '[]
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 :: 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 ->
            m (HFList g (x : ys)) -> TraverseHFList m g (x : ys)
forall k (m :: * -> *) (f :: k -> *) (xs :: [k]).
m (HFList f xs) -> TraverseHFList m f xs
TraverseHFList do g x -> HFList g ys -> HFList g (x : ys)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> HFList f xs -> HFList f (x : xs)
HFCons (g x -> HFList g ys -> HFList g (x : ys))
-> m (g x) -> m (HFList g ys -> HFList g (x : ys))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Membership xs x -> f x -> m (g x)
forall (x :: k). Membership xs x -> f x -> m (g x)
f Membership xs x
m f x
x m (HFList g ys -> HFList g (x : ys))
-> m (HFList g ys) -> m (HFList g (x : ys))
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 (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 = Identity (HFList g xs) -> HFList g xs
forall a. Identity a -> a
runIdentity
    do (forall (x :: k). Membership xs x -> f x -> Identity (g x))
-> HFList f xs -> Identity (HFList g xs)
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 -> g x -> Identity (g x)
forall a. a -> Identity a
Identity do Membership xs x -> f x -> g x
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 :: 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 = Int -> r -> HFList f xs -> m r
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 :: Int -> r -> HFList f ys -> m r
go Int
m1 r
z1 = \case
        HFList f ys
HFNil ->
            r -> m r
forall (f :: * -> *) a. Applicative f => a -> f a
pure r
z1
        HFCons f x
y HFList f xs
l -> do
            r
z2 <- r -> Membership xs x -> f x -> m r
forall (x :: k). r -> Membership xs x -> f x -> m r
f r
z1
                do Int -> Membership xs x
forall k (xs :: [k]) (x :: k). Int -> Membership xs x
unsafeMembership Int
m1
                do f x
y
            let m2 :: Int
m2 = Int
m1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
            Int -> r -> HFList f xs -> m r
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 :: 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 = Int -> HFList f xs -> m ()
forall (ys :: [k]). Int -> HFList f ys -> m ()
go Int
0 HFList f xs
l0 where
    go :: Int -> HFList f ys -> m ()
    go :: Int -> HFList f ys -> m ()
go Int
m1 = \case
        HFList f ys
HFNil ->
            () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        HFCons f x
y HFList f xs
l -> () -> () -> ()
forall a b. a -> b -> a
const
            (() -> () -> ()) -> m () -> m (() -> ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Membership xs x -> f x -> m ()
forall (x :: k). Membership xs x -> f x -> m ()
f
                do Int -> Membership xs x
forall k (xs :: [k]) (x :: k). Int -> Membership xs x
unsafeMembership Int
m1
                do f x
y
            m (() -> ()) -> m () -> m ()
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> HFList f xs -> m ()
forall (ys :: [k]). Int -> HFList f ys -> m ()
go
                do Int
m1 Int -> Int -> Int
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 :: 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 = (HFList f xs -> Identity r) -> HFList f xs -> r
coerce
    do r
-> (forall (x :: k). r -> Membership xs x -> f x -> Identity r)
-> HFList f xs
-> Identity r
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 -> r -> Identity r
forall a. a -> Identity a
Identity do r -> Membership xs x -> f x -> r
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 :: Int -> Membership xs x
unsafeMembership = Int -> Membership xs x
forall a b. a -> b
Unsafe.unsafeCoerce