{-# language DataKinds #-}
{-# language FlexibleContexts #-}
{-# language FlexibleInstances #-}
{-# language GADTs #-}
{-# language LambdaCase #-}
{-# language StandaloneKindSignatures #-}
{-# language TypeOperators #-}

module Rel8.Kind.Labels
  ( Labels
  , SLabels( SNil, SCons )
  , KnownLabels( labelsSing )
  , renderLabels
  )
where

-- base
import Data.Kind ( Constraint, Type )
import Data.List.NonEmpty ( NonEmpty, nonEmpty )
import Data.Maybe ( fromMaybe )
import Data.Proxy ( Proxy( Proxy ) )
import GHC.TypeLits ( KnownSymbol, Symbol, symbolVal )
import Prelude


type Labels :: Type
type Labels = [Symbol]


type SLabels :: Labels -> Type
data SLabels labels where
  SNil :: SLabels '[]
  SCons :: KnownSymbol label => Proxy label -> SLabels labels -> SLabels (label ': labels)


type KnownLabels :: Labels -> Constraint
class KnownLabels labels where
  labelsSing :: SLabels labels


instance KnownLabels '[] where
  labelsSing :: SLabels '[]
labelsSing = SLabels '[]
SNil


instance (KnownSymbol label, KnownLabels labels) =>
  KnownLabels (label ': labels)
 where
  labelsSing :: SLabels (label : labels)
labelsSing = Proxy label -> SLabels labels -> SLabels (label : labels)
forall (label :: Symbol) (labels :: Labels).
KnownSymbol label =>
Proxy label -> SLabels labels -> SLabels (label : labels)
SCons Proxy label
forall k (t :: k). Proxy t
Proxy SLabels labels
forall (labels :: Labels). KnownLabels labels => SLabels labels
labelsSing


renderLabels :: SLabels labels -> NonEmpty String
renderLabels :: SLabels labels -> NonEmpty String
renderLabels = NonEmpty String -> Maybe (NonEmpty String) -> NonEmpty String
forall a. a -> Maybe a -> a
fromMaybe (String -> NonEmpty String
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"anon") (Maybe (NonEmpty String) -> NonEmpty String)
-> (SLabels labels -> Maybe (NonEmpty String))
-> SLabels labels
-> NonEmpty String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> Maybe (NonEmpty String)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty ([String] -> Maybe (NonEmpty String))
-> (SLabels labels -> [String])
-> SLabels labels
-> Maybe (NonEmpty String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SLabels labels -> [String]
forall (labels :: Labels). SLabels labels -> [String]
go
  where
    go :: SLabels labels -> [String]
    go :: SLabels labels -> [String]
go = \case
      SLabels labels
SNil -> []
      SCons Proxy label
label SLabels labels
labels -> Proxy label -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy label
label String -> [String] -> [String]
forall a. a -> [a] -> [a]
: SLabels labels -> [String]
forall (labels :: Labels). SLabels labels -> [String]
go SLabels labels
labels