{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# 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 (..)
  , (&:)
  , only
  , (&:&)
  , both
  , 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 :: forall a (as :: [*]). HList (a : as) -> a
hHead (anyTy
x `HCons` HList manyTys
_) = anyTy
x


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


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


infixr 5 `HCons`, &:


-- | An infix alias for 'HCons'.
(&:) :: x -> HList xs -> HList (x ': xs)
&: :: forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
(&:) = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
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) = forall a. Show a => a -> String
show anyTy
x forall a. [a] -> [a] -> [a]
++ String
" &: " forall a. [a] -> [a] -> [a]
++ 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 forall a. Eq a => a -> a -> Bool
== anyTy
y Bool -> Bool -> Bool
&& HList manyTys
xs forall a. Eq a => a -> a -> Bool
== HList manyTys
ys


-- | Construct a two-item HList.
both :: x -> y -> HList '[x, y]
both :: forall x y. x -> y -> HList '[x, y]
both x
v y
w = x
v forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
&: y
w forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
&: HList '[]
HNil


infixr 6 `both`, &:&


-- | An infix alias for 'both'.
(&:&) :: x -> y -> HList '[x, y]
&:& :: forall x y. x -> y -> HList '[x, y]
(&:&) = forall x y. x -> y -> HList '[x, y]
both


-- | Construct a singleton HList
only :: x -> HList '[x]
only :: forall x. x -> HList '[x]
only x
v = x
v forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
&: HList '[]
HNil


-- | Use a type-level symbol as /key/ type that indexes a /value/ type.
data KV :: Symbol -> Type -> Type 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 :: [Type]) 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 :: Type) (xs :: [Type]) where
  lookupProof :: LookupKV k t xs


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


instance {-# OVERLAPPING #-} MemberKV k t (KV k t ': kvs) where
  lookupProof :: LookupKV k t (KV k t : kvs)
lookupProof = forall (k :: Symbol) t (tys :: [*]). LookupKV k t (KV k t : tys)
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 = forall (k :: Symbol) t (tys :: [*]) (otherTy :: Symbol) ot.
LookupKV k t tys -> LookupKV k t (KV otherTy ot : tys)
OtherKeys 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 :: forall (k :: Symbol) t (xs :: [*]).
MemberKV k t xs =>
HList xs -> t
select = forall (k1 :: Symbol) t1 (xs1 :: [*]).
LookupKV k1 t1 xs1 -> HList xs1 -> t1
go forall a b. (a -> b) -> a -> b
$ 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 :: forall (k1 :: Symbol) t1 (xs1 :: [*]).
LookupKV k1 t1 xs1 -> HList xs1 -> t1
go LookupKV k1 t1 xs1
AtHead (V t1
x `HCons` HList manyTys
_) = t1
x
    go (OtherKeys LookupKV k1 t1 kvs
cons) (anyTy
_ `HCons` HList manyTys
y) = forall (k1 :: Symbol) t1 (xs1 :: [*]).
LookupKV k1 t1 xs1 -> HList xs1 -> t1
go LookupKV k1 t1 kvs
cons 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 :: [Type]) (xs :: [Type]) 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 :: [Type]) (kvs :: [Type]) 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 = 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 = forall (tys :: [Symbol]) (otherTy :: [*]) (ot :: [*]) (k :: Symbol)
       t.
LookupMany tys otherTy ot
-> LookupMany (k : tys) (t : otherTy) (KV k t : ot)
NextOfMany 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 = forall (ks :: [Symbol]) (ts :: [*]) (tys :: [*])
       (otherTy :: Symbol) ot.
LookupMany ks ts tys -> LookupMany ks ts (KV otherTy ot : tys)
ManyOthers 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 :: forall (ks :: [Symbol]) (ts :: [*]) (xs :: [*]).
ManyMemberKV ks ts xs =>
HList xs -> HList ts
selectMany = forall (ks1 :: [Symbol]) (ts1 :: [*]) (xs1 :: [*]).
LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go forall a b. (a -> b) -> a -> b
$ 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 :: forall (ks1 :: [Symbol]) (ts1 :: [*]) (xs1 :: [*]).
LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go LookupMany ks1 ts1 xs1
FirstOfMany (V t
x `HCons` HList manyTys
_) = t
x forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList '[]
HNil
    go (NextOfMany LookupMany ks ts kvs
cons) (V t
x `HCons` HList manyTys
y) = t
x forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall (ks1 :: [Symbol]) (ts1 :: [*]) (xs1 :: [*]).
LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go LookupMany ks ts kvs
cons HList manyTys
y
    go (ManyOthers LookupMany ks1 ts1 kvs
cons) (anyTy
_ `HCons` HList manyTys
y) = forall (ks1 :: [Symbol]) (ts1 :: [*]) (xs1 :: [*]).
LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go LookupMany ks1 ts1 kvs
cons 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 = forall y (xs :: [*]). IsInProof y xs => Proxy y -> HList xs -> y
hOf @y forall {k} (t :: k). Proxy t
Proxy HList xs
xs forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` 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 = 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 = forall t (tys :: [*]) otherTy. IsIn t tys -> IsIn t (otherTy : tys)
IsInTail forall t (tys :: [*]). IsInProof t tys => IsIn t tys
provedIsIn