{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Eta reduce" #-}

-- | implements a heterogeneous list to use for forests of heterogeneous trees
module Data.HTree.List
  ( -- * heterogeneous list
    HList ((:::), HSing, ..)

    -- * mapping
  , hcmap
  , hmap

    -- * traversing
  , htraverse
  , hctraverse

    -- * folding
  , hcFold

    -- * helpers
  , allTopHList
  , hconcat
  )
where

import Data.Functor.Identity (Identity (Identity, runIdentity))
import Data.HTree.Constraint (withDict, pattern Dict, type Dict)
import Data.HTree.Families (All, Top, type (++))
import Data.Kind (Type)

-- | A heterogeneous list
--
-- >>> "bla" `HCons` 23 `HCons` HNil :: HList Identity '[ String, Int ]
-- HCons (Identity "bla") (HCons (Identity 23) HNil)
type HList :: forall k. (k -> Type) -> [k] -> Type
data HList f ts where
  HCons :: forall f x xs. f x -> HList f xs -> HList f (x : xs)
  HNil :: forall f. HList f '[]

-- | pattern synonym for 'HCons'
--
-- >>> t = "bla" ::: 23 ::: HNil :: HList Identity '[ String, Int ]
-- >>> t
-- HCons (Identity "bla") (HCons (Identity 23) HNil)
-- >>> case t of (x ::: _) -> runIdentity x
-- "bla"
pattern (:::) :: forall f x xs. f x -> HList f xs -> HList f (x : xs)
pattern x ::: xs = HCons x xs

-- | pattern that allows to construct a singleton HList
--
-- >>> HSing 42 :: HList Identity '[ Int ]
-- HCons (Identity 42) HNil
pattern HSing :: forall f a. f a -> HList f '[a]
pattern HSing x = HCons x HNil

-- | map with a function that maps forall f a
hmap :: forall f g xs. (forall a. f a -> g a) -> HList f xs -> HList g xs
hmap f l = withDict (allTopHList l) $ hcmap @Top @f @g f l

-- | map with a constraint that holds for all elements of the  list
--
-- >>> import Data.Functor.Const
-- >>> hcmap @Show (Const . show . runIdentity) (42 `HCons` HSing "bla" :: HList Identity '[ Int, String ])
-- HCons (Const "42") (HCons (Const "\"bla\"") HNil)
hcmap :: forall c f g xs. All c xs => (forall a. c a => f a -> g a) -> HList f xs -> HList g xs
hcmap f = runIdentity . hctraverse @c @Identity @f @g (Identity . f)

-- | traverse a structure with a function
htraverse :: forall t f g xs. Applicative t => (forall a. f a -> t (g a)) -> HList f xs -> t (HList g xs)
htraverse f l = withDict (allTopHList l) $ hctraverse @Top @t @f @g f l

-- | traverse a structure such that a constraint holds; this is the workhorse of mapping and traversing
--
-- >>> import Data.Functor.Const
-- >>> hctraverse @Show (Just . Const . show . runIdentity) (42 `HCons` HSing "bla" :: HList Identity '[ Int, String ])
-- Just (HCons (Const "42") (HCons (Const "\"bla\"") HNil))
hctraverse :: forall c t f g xs. (All c xs, Applicative t) => (forall a. c a => f a -> t (g a)) -> HList f xs -> t (HList g xs)
hctraverse _ HNil = pure HNil
hctraverse f (HCons x xs) = HCons <$> f x <*> hctraverse @c @t @f @g f xs

-- | foldr for HLists.
hcFold :: forall c f b xs. All c xs => (forall a. c a => f a -> b -> b) -> b -> HList f xs -> b
hcFold _ def HNil = def
hcFold f def (x `HCons` xs) = f x $ hcFold @c f def xs

-- | witnesses that for all HLists, we can always derive the All Top constraint
allTopHList :: forall f xs. HList f xs -> Dict (All Top xs)
allTopHList HNil = Dict
allTopHList (HCons _ xs) = case allTopHList xs of
  Dict -> Dict

-- | concats two heterogeneous lists
hconcat :: forall f xs ys. HList f xs -> HList f ys -> HList f (xs ++ ys)
hconcat HNil ys = ys
hconcat (x `HCons` xs) ys = x `HCons` xs `hconcat` ys

infixr 5 `HCons`

infixr 5 :::

infixr 5 `hconcat`

deriving stock instance Show (HList f '[])

deriving stock instance (Show (f x), Show (HList f xs)) => Show (HList f (x : xs))

deriving stock instance Eq (HList f '[])

deriving stock instance (Eq (f x), Eq (HList f xs)) => Eq (HList f (x : xs))