{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE NamedFieldPuns         #-}
{-# LANGUAGE OverloadedStrings      #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# OPTIONS_HADDOCK prune not-home #-}
{-|
Copyright   : (c) 2020-2021 Tim Emiola
SPDX-License-Identifier: BSD3
Maintainer  : Tim Emiola <adetokunbo@users.noreply.github.com>

Defines type-level data structures and combinators used by
"System.TmpProc.Docker" and "System.TmpProc.Warp".

'HList' implements a heterogenous list used to define types that represent
multiple concurrent @tmp procs@.

'KV' is intended for internal use within the @tmp-proc@ package. It allows
indexing and sorting of lists of tmp procs.

-}
module System.TmpProc.TypeLevel
  ( -- * Heterogenous List
    HList(..)
  , (&:)
  , hHead
  , hOf
  , ReorderH(..)

    -- * A type-level Key-Value
  , KV(..)
  , select
  , selectMany
  , LookupKV(..)
  , MemberKV(..)
  , ManyMemberKV(..)

    -- * Other combinators
  , IsAbsent
  , IsInProof

    -- * Re-exports
  , module System.TmpProc.TypeLevel.Sort
  )
where

import           Data.Kind                     (Type)
import           Data.Proxy                    (Proxy (..))
import           GHC.Exts                      (Constraint)
import           GHC.TypeLits                  (ErrorMessage (..), Symbol,
                                                TypeError)
import qualified GHC.TypeLits                  as TL
import           System.TmpProc.TypeLevel.Sort

-- $setup
-- >>> import Data.Proxy
-- >>> :set -XDataKinds
-- >>> :set -XTypeApplications


{-| Obtain the first element of a 'HList'. -}
hHead :: HList (a ': as) -> a
hHead :: HList (a : as) -> a
hHead (anyTy
x `HCons` HList manyTys
_) = a
anyTy
x


{-| Get an item in an 'HList' given its type. -}
hOf :: forall y xs . IsInProof y xs => Proxy y -> HList xs -> y
hOf :: Proxy y -> HList xs -> y
hOf Proxy y
proxy = Proxy y -> IsIn y xs -> HList xs -> y
forall x (ys :: [*]). Proxy x -> IsIn x ys -> HList ys -> x
go Proxy y
proxy IsIn y xs
forall t (tys :: [*]). IsInProof t tys => IsIn t tys
provedIsIn
  where
    go :: Proxy x -> IsIn x ys -> HList ys -> x
    go :: Proxy x -> IsIn x ys -> HList ys -> x
go Proxy x
_ IsIn x ys
IsHead            (anyTy
y `HCons` HList manyTys
_)    = x
anyTy
y
    go Proxy x
pxy (IsInTail IsIn x tys
cons) (anyTy
_ `HCons` HList manyTys
rest) = Proxy x -> IsIn x tys -> HList tys -> x
forall x (ys :: [*]). Proxy x -> IsIn x ys -> HList ys -> x
go Proxy x
pxy IsIn x tys
cons HList tys
HList manyTys
rest


{-| Defines a Heterogenous list. -}
data HList :: [*] -> * where
  HNil  :: HList '[]
  HCons :: anyTy -> HList manyTys -> HList (anyTy ': manyTys)


infixr 5 `HCons`
infixr 5 &:

{-| An infix alias for 'HCons'. -}
(&:) :: x -> HList xs -> HList (x ': xs)
&: :: x -> HList xs -> HList (x : xs)
(&:) = x -> HList xs -> HList (x : xs)
forall anyTy (manyTys :: [*]).
anyTy -> HList manyTys -> HList (anyTy : manyTys)
HCons

instance Show (HList '[]) where
  show :: HList '[] -> String
show HList '[]
HNil = String
"HNil"

instance (Show x, Show (HList xs)) => Show (HList (x ': xs)) where
  show :: HList (x : xs) -> String
show (HCons anyTy
x HList manyTys
xs) = anyTy -> String
forall a. Show a => a -> String
show anyTy
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" &: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ HList manyTys -> String
forall a. Show a => a -> String
show HList manyTys
xs

instance Eq (HList '[]) where
  HList '[]
HNil == :: HList '[] -> HList '[] -> Bool
== HList '[]
HNil = Bool
True

instance (Eq x, Eq (HList xs)) => Eq (HList (x ': xs)) where
  (HCons anyTy
x HList manyTys
xs) == :: HList (x : xs) -> HList (x : xs) -> Bool
== (HCons anyTy
y HList manyTys
ys) = anyTy
x anyTy -> anyTy -> Bool
forall a. Eq a => a -> a -> Bool
== anyTy
anyTy
y Bool -> Bool -> Bool
&& HList manyTys
xs HList manyTys -> HList manyTys -> Bool
forall a. Eq a => a -> a -> Bool
== HList manyTys
HList manyTys
ys


{-| Use a type-level symbol as /key/ type that indexes a /value/ type. -}
data KV :: Symbol -> * -> * where
  V :: a -> KV s a


{-| A constraint that confirms that a type is not present in a type-level list. -}
type family IsAbsent e r :: Constraint where
  IsAbsent e '[]           = ()
  IsAbsent e (e ': _)      = TypeError (NotAbsentErr e)
  IsAbsent e (e' ': tail)  = IsAbsent e tail


type NotAbsentErr e =
  ('TL.Text " type " ':<>: 'TL.ShowType e) ':<>:
  ('TL.Text " is already in this type list, and is not allowed again")


{-| Proves a symbol and its type occur as entry in a list of @'KV'@ types. -}
data LookupKV (k :: Symbol) t (xs :: [*]) where
  AtHead :: LookupKV k t (KV k t ': kvs)
  OtherKeys :: LookupKV k t kvs -> LookupKV k t (KV ok ot ': kvs)


{-| Generate proof instances of 'LookupKV'. -}
class MemberKV (k :: Symbol) (t :: *) (xs :: [*]) where
  lookupProof :: LookupKV k t xs

instance {-# Overlapping #-} MemberKV k t '[KV k t] where
  lookupProof :: LookupKV k t '[KV k t]
lookupProof = LookupKV k t '[KV k t]
forall (k :: Symbol) t (kvs :: [*]). LookupKV k t (KV k t : kvs)
AtHead @k @t @'[]

instance {-# Overlapping #-} MemberKV k t (KV k t ': kvs) where
  lookupProof :: LookupKV k t (KV k t : kvs)
lookupProof = LookupKV k t (KV k t : kvs)
forall (k :: Symbol) t (kvs :: [*]). LookupKV k t (KV k t : kvs)
AtHead @k @t @kvs

instance MemberKV k t kvs => MemberKV k t (KV ok ot ': kvs) where
  lookupProof :: LookupKV k t (KV ok ot : kvs)
lookupProof = LookupKV k t kvs -> LookupKV k t (KV ok ot : kvs)
forall (k :: Symbol) t (kvs :: [*]) (ok :: Symbol) ot.
LookupKV k t kvs -> LookupKV k t (KV ok ot : kvs)
OtherKeys LookupKV k t kvs
forall (k :: Symbol) t (xs :: [*]).
MemberKV k t xs =>
LookupKV k t xs
lookupProof


{-| Select an item from an 'HList' of @'KV's@ by /key/.


/N.B/ Returns the first item. It assumes the keys in the KV HList are unique.
/TODO:/ enforce this rule using a constraint.


==== __Examples__


>>> select @"d" @Double  @'[KV "b" Bool, KV "d" Double] (V True &:  V (3.1 :: Double) &: HNil)
3.1

-}
select
  :: forall k t xs . MemberKV k t xs
  => HList xs
  -> t
select :: HList xs -> t
select = LookupKV k t xs -> HList xs -> t
forall (k1 :: Symbol) t1 (xs1 :: [*]).
LookupKV k1 t1 xs1 -> HList xs1 -> t1
go (LookupKV k t xs -> HList xs -> t)
-> LookupKV k t xs -> HList xs -> t
forall a b. (a -> b) -> a -> b
$ MemberKV k t xs => LookupKV k t xs
forall (k :: Symbol) t (xs :: [*]).
MemberKV k t xs =>
LookupKV k t xs
lookupProof @k @t @xs
  where
    go :: LookupKV k1 t1 xs1 -> HList xs1 -> t1
    go :: LookupKV k1 t1 xs1 -> HList xs1 -> t1
go LookupKV k1 t1 xs1
AtHead (V x `HCons` HList manyTys
_)         = t1
x
    go (OtherKeys LookupKV k1 t1 kvs
cons) (anyTy
_ `HCons` HList manyTys
y) = LookupKV k1 t1 kvs -> HList kvs -> t1
forall (k1 :: Symbol) t1 (xs1 :: [*]).
LookupKV k1 t1 xs1 -> HList xs1 -> t1
go LookupKV k1 t1 kvs
cons HList kvs
HList manyTys
y


{-| Proves that symbols with corresponding types occur as a 'KV' in a
  list of 'KV' types

/Note/ - both the list symbols and @'KV'@ types need to be sorted, with @'KV'@
types sorted by key. /TODO:/ is there an easy way to incorporate this rule into
the proof ?

-}
data LookupMany (keys :: [Symbol]) (t :: [*]) (xs :: [*]) where
  FirstOfMany :: LookupMany (k ': '[]) (t ': '[]) (KV k t ': kvs)

  NextOfMany
    :: LookupMany ks ts kvs
    -> LookupMany (k ': ks) (t ': ts) (KV k t ': kvs)

  ManyOthers :: LookupMany ks ts kvs -> LookupMany ks ts (KV ok ot ': kvs)


{-| Generate proof instances of 'LookupMany'. -}
class ManyMemberKV (ks :: [Symbol]) (ts :: [*]) (kvs :: [*])  where
  manyProof :: LookupMany ks ts kvs

instance {-# Overlapping #-} ManyMemberKV '[k] '[t] (KV k t ': ks) where
  manyProof :: LookupMany '[k] '[t] (KV k t : ks)
manyProof = LookupMany '[k] '[t] (KV k t : ks)
forall (k :: Symbol) t (ks :: [*]).
LookupMany '[k] '[t] (KV k t : ks)
FirstOfMany @k @t @ks

instance {-# Overlapping #-} ManyMemberKV ks ts kvs => ManyMemberKV (k ': ks) (t ': ts) (KV k t ': kvs) where
  manyProof :: LookupMany (k : ks) (t : ts) (KV k t : kvs)
manyProof = LookupMany ks ts kvs -> LookupMany (k : ks) (t : ts) (KV k t : kvs)
forall (ks :: [Symbol]) (ts :: [*]) (kvs :: [*]) (k :: Symbol) t.
LookupMany ks ts kvs -> LookupMany (k : ks) (t : ts) (KV k t : kvs)
NextOfMany LookupMany ks ts kvs
forall (ks :: [Symbol]) (ts :: [*]) (kvs :: [*]).
ManyMemberKV ks ts kvs =>
LookupMany ks ts kvs
manyProof

instance ManyMemberKV ks ts kvs  => ManyMemberKV ks ts (KV ok ot ': kvs) where
  manyProof :: LookupMany ks ts (KV ok ot : kvs)
manyProof = LookupMany ks ts kvs -> LookupMany ks ts (KV ok ot : kvs)
forall (ks :: [Symbol]) (ts :: [*]) (kvs :: [*]) (ok :: Symbol) ot.
LookupMany ks ts kvs -> LookupMany ks ts (KV ok ot : kvs)
ManyOthers LookupMany ks ts kvs
forall (ks :: [Symbol]) (ts :: [*]) (kvs :: [*]).
ManyMemberKV ks ts kvs =>
LookupMany ks ts kvs
manyProof


{-| Select items with specified keys from an @'HList'@ of @'KV's@ by /key/.

/N.B./ this this is an internal function.

The keys must be provided in the same order as they occur in the
HList, any other order will likely result in an compiler error.

==== __Examples__


>>> selectMany @'["b"] @'[Bool] @'[KV "b" Bool, KV "d" Double] (V True &:  V (3.1 :: Double) &: HNil)
True &: HNil

-}
selectMany
  :: forall ks ts xs . ManyMemberKV ks ts xs
  => HList xs
  -> HList ts
selectMany :: HList xs -> HList ts
selectMany = LookupMany ks ts xs -> HList xs -> HList ts
forall (ks1 :: [Symbol]) (ts1 :: [*]) (xs1 :: [*]).
LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go (LookupMany ks ts xs -> HList xs -> HList ts)
-> LookupMany ks ts xs -> HList xs -> HList ts
forall a b. (a -> b) -> a -> b
$ ManyMemberKV ks ts xs => LookupMany ks ts xs
forall (ks :: [Symbol]) (ts :: [*]) (kvs :: [*]).
ManyMemberKV ks ts kvs =>
LookupMany ks ts kvs
manyProof @ks @ts @xs
  where
    go :: LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
    go :: LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go LookupMany ks1 ts1 xs1
FirstOfMany (V x `HCons` HList manyTys
_)       = t
x t -> HList '[] -> HList '[t]
forall anyTy (manyTys :: [*]).
anyTy -> HList manyTys -> HList (anyTy : manyTys)
`HCons` HList '[]
HNil
    go (NextOfMany LookupMany ks ts kvs
cons) (V x `HCons` HList manyTys
y) = t
x t -> HList ts -> HList (t : ts)
forall anyTy (manyTys :: [*]).
anyTy -> HList manyTys -> HList (anyTy : manyTys)
`HCons` LookupMany ks ts kvs -> HList kvs -> HList ts
forall (ks1 :: [Symbol]) (ts1 :: [*]) (xs1 :: [*]).
LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go LookupMany ks ts kvs
cons HList kvs
HList manyTys
y
    go (ManyOthers LookupMany ks1 ts1 kvs
cons) (anyTy
_ `HCons` HList manyTys
y)   = LookupMany ks1 ts1 kvs -> HList kvs -> HList ts1
forall (ks1 :: [Symbol]) (ts1 :: [*]) (xs1 :: [*]).
LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go LookupMany ks1 ts1 kvs
cons HList kvs
HList manyTys
y


{-| Allows reordering of similar @'HList's@.

==== __Examples__


>>> hReorder @_ @'[Bool, Int] ('c' &: (3 :: Int) &: True &: (3.1 :: Double) &: HNil)
True &: 3 &: HNil

>>> hReorder @_ @'[Double, Bool, Int] ('c' &: (3 :: Int) &: True &: (3.1 :: Double) &: HNil)
3.1 &: True &: 3 &: HNil

-}
class ReorderH xs ys where
  hReorder :: HList xs -> HList ys

instance ReorderH xs '[] where
  hReorder :: HList xs -> HList '[]
hReorder HList xs
_ = HList '[]
HNil

instance (IsInProof y xs, ReorderH xs ys) => ReorderH xs (y ': ys) where
  hReorder :: HList xs -> HList (y : ys)
hReorder HList xs
xs = Proxy y -> HList xs -> y
forall y (xs :: [*]). IsInProof y xs => Proxy y -> HList xs -> y
hOf @y Proxy y
forall k (t :: k). Proxy t
Proxy HList xs
xs y -> HList ys -> HList (y : ys)
forall anyTy (manyTys :: [*]).
anyTy -> HList manyTys -> HList (anyTy : manyTys)
`HCons` HList xs -> HList ys
forall (xs :: [*]) (ys :: [*]).
ReorderH xs ys =>
HList xs -> HList ys
hReorder HList xs
xs


{-| Proves a type is present in a list of other types. -}
data IsIn t (xs :: [Type]) where
  IsHead   :: IsIn t (t ': tys)
  IsInTail :: IsIn t tys -> IsIn t (otherTy ': tys)


{-| Generate proof instances of 'IsIn'. -}
class IsInProof t (tys :: [Type]) where
  provedIsIn :: IsIn t tys

instance {-# Overlapping #-} IsInProof t (t ': tys) where
  provedIsIn :: IsIn t (t : tys)
provedIsIn = IsIn t (t : tys)
forall t (tys :: [*]). IsIn t (t : tys)
IsHead @t @tys

instance IsInProof t tys => IsInProof t (a : tys) where
  provedIsIn :: IsIn t (a : tys)
provedIsIn = IsIn t tys -> IsIn t (a : tys)
forall t (tys :: [*]) otherTy. IsIn t tys -> IsIn t (otherTy : tys)
IsInTail IsIn t tys
forall t (tys :: [*]). IsInProof t tys => IsIn t tys
provedIsIn