{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Type.Membership.HList (HList(..)
  , hindex
  , hfoldrWithIndex
  , htraverse
  , htraverseWithIndex
  , hlength) where

import Type.Membership.Internal

hindex :: HList h xs -> Membership xs x -> h x
hindex :: HList h xs -> Membership xs x -> h x
hindex HList h xs
HNil Membership xs x
_ = [Char] -> h x
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"
hindex (HCons h x
x HList h xs
xs) Membership xs x
m = Membership (x : xs) x
-> ((x :~: x) -> h x) -> (Membership xs x -> h x) -> h x
forall k (y :: k) (xs :: [k]) (x :: k) r.
Membership (y : xs) x
-> ((x :~: y) -> r) -> (Membership xs x -> r) -> r
testMembership Membership xs x
Membership (x : xs) x
m (\x :~: x
Refl -> h x
h x
x) (HList h xs -> Membership xs x -> h x
forall k (h :: k -> *) (xs :: [k]) (x :: k).
HList h xs -> Membership xs x -> h x
hindex HList h xs
xs)

htraverse :: forall f g h xs. Applicative f => (forall x. g x -> f (h x)) -> HList g xs -> f (HList h xs)
htraverse :: (forall (x :: k). g x -> f (h x)) -> HList g xs -> f (HList h xs)
htraverse forall (x :: k). g x -> f (h x)
f = HList g xs -> f (HList h xs)
forall (ts :: [k]). HList g ts -> f (HList h ts)
go where
  go :: HList g ts -> f (HList h ts)
  go :: HList g ts -> f (HList h ts)
go HList g ts
HNil = HList h '[] -> f (HList h '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure HList h '[]
forall k (h :: k -> *). HList h '[]
HNil
  go (HCons g x
h HList g xs
xs) = h x -> HList h xs -> HList h (x : xs)
forall a (h :: a -> *) (x :: a) (xs :: [a]).
h x -> HList h xs -> HList h (x : xs)
HCons (h x -> HList h xs -> HList h (x : xs))
-> f (h x) -> f (HList h xs -> HList h (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g x -> f (h x)
forall (x :: k). g x -> f (h x)
f g x
h f (HList h xs -> HList h (x : xs))
-> f (HList h xs) -> f (HList h (x : xs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> HList g xs -> f (HList h xs)
forall (ts :: [k]). HList g ts -> f (HList h ts)
go HList g xs
xs
{-# INLINE htraverse #-}

hlength :: HList h xs -> Int
hlength :: HList h xs -> Int
hlength = Int -> HList h xs -> Int
forall k (h :: k -> *) (xs :: [k]). Int -> HList h xs -> Int
go Int
0 where
  go :: Int -> HList h xs -> Int
  go :: Int -> HList h xs -> Int
go Int
n HList h xs
HNil = Int
n
  go Int
n (HCons h x
_ HList h xs
xs) = let !n' :: Int
n' = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 in Int -> HList h xs -> Int
forall k (h :: k -> *) (xs :: [k]). Int -> HList h xs -> Int
go Int
n' HList h xs
xs
{-# INLINE hlength #-}