{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Data.TypeMap.Internal.List where

import Data.TypeMap.Internal.Unsafe

-- | List-backed type-map.
newtype TypeList d = TypeList [Any]

type role TypeList nominal

-- | Empty list.
empty :: TypeList '[]
empty :: TypeList '[]
empty = [Any] -> TypeList '[]
forall k (d :: k). [Any] -> TypeList d
TypeList []

-- | Access an element indexed by its type @a@. /O(n)/
--
-- If @a@ is associated to @b@ in the type list @d@:
--
-- @
-- 'index' @a (l :: 'TypeList' d) :: b
-- @
--
-- >>> let l = (0 :: Int) <| True <| "Hello" <| empty :: TypeList '[ '("a", Int), '("b", Bool), '("c", String)]
-- >>> index @"c" l
-- "Hello"
index
  :: forall a d
  .  KnownNat (Index a d)
  => TypeList d -> Lookup a d
index :: TypeList d -> Lookup a d
index = (forall c. [c] -> Int -> c) -> TypeList d -> Lookup a d
forall k (a :: k) (d :: [(k, *)]) (f :: * -> *)
       (m :: [(k, *)] -> *).
(KnownNat (Index a d), Coercible (f Any) (m d)) =>
(forall c. f c -> Int -> c) -> m d -> Lookup a d
unsafeIndex @a forall c. [c] -> Int -> c
(!!)

-- | Add an element to the beginning of a list. /O(1)/
cons
  :: forall a d b
  .  b -> TypeList d -> TypeList ('(a, b) ': d)
cons :: b -> TypeList d -> TypeList ('(a, b) : d)
cons = (forall c. c -> [c] -> [c])
-> b -> TypeList d -> TypeList ('(a, b) : d)
forall k (a :: k) (d :: [(k, *)]) b (f :: * -> *)
       (m :: [(k, *)] -> *).
(Coercible (f Any) (m d), Coercible (f Any) (m ('(a, b) : d))) =>
(forall c. c -> f c -> f c) -> b -> m d -> m ('(a, b) : d)
unsafeCons (:)

-- | Synonym of 'cons'.
(<|)
  :: forall a d b
  .  b -> TypeList d -> TypeList ('(a, b) ': d)
<| :: b -> TypeList d -> TypeList ('(a, b) : d)
(<|) = b -> TypeList d -> TypeList ('(a, b) : d)
forall k (a :: k) (d :: [(k, *)]) b.
b -> TypeList d -> TypeList ('(a, b) : d)
cons

infixr 5 <|, `cons`

-- | Add an element to the end of a list. /O(n)/
snoc
  :: forall a d b
  .  (Last d ~ '(a, b))
  => TypeList (Init d) -> b -> TypeList d
snoc :: TypeList (Init d) -> b -> TypeList d
snoc = (forall c. [c] -> c -> [c]) -> TypeList (Init d) -> b -> TypeList d
forall k (a :: k) (d :: [(k, *)]) b (f :: * -> *)
       (m :: [(k, *)] -> *).
(Last d ~ '(a, b), Coercible (f Any) (m (Init d)),
 Coercible (f Any) (m d)) =>
(forall c. f c -> c -> f c) -> m (Init d) -> b -> m d
unsafeSnoc @a (\[c]
xs c
x -> [c]
xs [c] -> [c] -> [c]
forall a. [a] -> [a] -> [a]
++ [c
x])

-- | Synonym of 'snoc'.
(|>)
  :: forall a d b
  .  (Last d ~ '(a, b))
  => TypeList (Init d) -> b -> TypeList d
|> :: TypeList (Init d) -> b -> TypeList d
(|>) = TypeList (Init d) -> b -> TypeList d
forall k (a :: k) (d :: [(k, *)]) b.
(Last d ~ '(a, b)) =>
TypeList (Init d) -> b -> TypeList d
snoc

infixr 5 |>, `snoc`