{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}

module Skeletest.Internal.Utils.HList (
  HList (..),
  uncheck,
  toListWith,
  toListWithM,
  hzip,
  hzipWithM,
) where

import Data.Functor.Const (Const (..))
import Data.Functor.Identity (runIdentity)
import GHC.Generics ((:*:) (..))

data HList f xs where
  HNil :: HList f '[]
  HCons :: f x -> HList f xs -> HList f (x ': xs)

uncheck :: HList (Const a) xs -> [a]
uncheck :: forall {k} a (xs :: [k]). HList (Const a) xs -> [a]
uncheck = (forall (x :: k). Const a x -> a) -> HList (Const a) xs -> [a]
forall {k} (f :: k -> *) y (xs :: [k]).
(forall (x :: k). f x -> y) -> HList f xs -> [y]
toListWith Const a x -> a
forall (x :: k). Const a x -> a
forall {k} a (b :: k). Const a b -> a
getConst

toListWith :: (forall x. f x -> y) -> HList f xs -> [y]
toListWith :: forall {k} (f :: k -> *) y (xs :: [k]).
(forall (x :: k). f x -> y) -> HList f xs -> [y]
toListWith forall (x :: k). f x -> y
f = Identity [y] -> [y]
forall a. Identity a -> a
runIdentity (Identity [y] -> [y])
-> (HList f xs -> Identity [y]) -> HList f xs -> [y]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: k). f x -> Identity y) -> HList f xs -> Identity [y]
forall {k} (m :: * -> *) (f :: k -> *) y (xs :: [k]).
Monad m =>
(forall (x :: k). f x -> m y) -> HList f xs -> m [y]
toListWithM (y -> Identity y
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (y -> Identity y) -> (f x -> y) -> f x -> Identity y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> y
forall (x :: k). f x -> y
f)

toListWithM :: (Monad m) => (forall x. f x -> m y) -> HList f xs -> m [y]
toListWithM :: forall {k} (m :: * -> *) (f :: k -> *) y (xs :: [k]).
Monad m =>
(forall (x :: k). f x -> m y) -> HList f xs -> m [y]
toListWithM forall (x :: k). f x -> m y
f = \case
  HList f xs
HNil -> [y] -> m [y]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  HCons f x
x HList f xs
xs -> (:) (y -> [y] -> [y]) -> m y -> m ([y] -> [y])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> m y
forall (x :: k). f x -> m y
f f x
x m ([y] -> [y]) -> m [y] -> m [y]
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (x :: k). f x -> m y) -> HList f xs -> m [y]
forall {k} (m :: * -> *) (f :: k -> *) y (xs :: [k]).
Monad m =>
(forall (x :: k). f x -> m y) -> HList f xs -> m [y]
toListWithM f x -> m y
forall (x :: k). f x -> m y
f HList f xs
xs

hzip :: HList f xs -> HList g xs -> HList (f :*: g) xs
hzip :: forall {k} (f :: k -> *) (xs :: [k]) (g :: k -> *).
HList f xs -> HList g xs -> HList (f :*: g) xs
hzip = \cases
  HList f xs
HNil HList g xs
HNil -> HList (f :*: g) xs
HList (f :*: g) '[]
forall {k} (f :: k -> *). HList f '[]
HNil
  (HCons f x
f HList f xs
fs) (HCons g x
g HList g xs
gs) -> (:*:) f g x -> HList (f :*: g) xs -> HList (f :*: g) (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
f x -> HList f xs -> HList f (x : xs)
HCons (f x
f f x -> g x -> (:*:) f g x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g x
g x
g) (HList f xs -> HList g xs -> HList (f :*: g) xs
forall {k} (f :: k -> *) (xs :: [k]) (g :: k -> *).
HList f xs -> HList g xs -> HList (f :*: g) xs
hzip HList f xs
fs HList g xs
HList g xs
gs)

hzipWithM ::
  (Monad m) =>
  (forall x. f x -> g x -> m (h x))
  -> HList f xs
  -> HList g xs
  -> m (HList h xs)
hzipWithM :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (xs :: [k]).
Monad m =>
(forall (x :: k). f x -> g x -> m (h x))
-> HList f xs -> HList g xs -> m (HList h xs)
hzipWithM forall (x :: k). f x -> g x -> m (h x)
k = \cases
  HList f xs
HNil HList g xs
HNil -> HList h xs -> m (HList h xs)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HList h xs
HList h '[]
forall {k} (f :: k -> *). HList f '[]
HNil
  (HCons f x
f HList f xs
fs) (HCons g x
g HList g xs
gs) -> h x -> HList h xs -> HList h xs
h x -> HList h xs -> HList h (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
f x -> HList f xs -> HList f (x : xs)
HCons (h x -> HList h xs -> HList h xs)
-> m (h x) -> m (HList h xs -> HList h xs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> g x -> m (h x)
forall (x :: k). f x -> g x -> m (h x)
k f x
f g x
g x
g m (HList h xs -> HList h xs) -> m (HList h xs) -> m (HList h xs)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (x :: k). f x -> g x -> m (h x))
-> HList f xs -> HList g xs -> m (HList h xs)
forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (xs :: [k]).
Monad m =>
(forall (x :: k). f x -> g x -> m (h x))
-> HList f xs -> HList g xs -> m (HList h xs)
hzipWithM f x -> g x -> m (h x)
forall (x :: k). f x -> g x -> m (h x)
k HList f xs
fs HList g xs
HList g xs
gs