{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

module Data.Type.Sing where

import           Data.Bifunctor
import           Data.Kind
import           Data.Singletons
import           Data.Singletons.Prelude.List hiding (Length, Reverse, sReverse, Head, (%:++), Replicate)
import           Data.Type.Index
import           Data.Type.Length
import           Data.Type.Nat
import           Data.Type.Product
import           Data.Type.Uniform
import           Type.Class.Known
import           Type.Class.Witness
import           Type.Family.Constraint
import           Type.Family.List
import           Type.Family.List.Util
import           Type.Family.Nat

instance Witness ØC (SingI a) (Sing a) where
    q \\ s = withSingI s q


singLength
    :: Sing ns
    -> Length ns
singLength = \case
    SNil        -> LZ
    _ `SCons` s -> LS (singLength s)

singProd
    :: Sing as
    -> Prod Sing as
singProd = \case
    SNil         -> Ø
    s `SCons` ss -> s :< singProd ss

prodSing
    :: Prod Sing as
    -> Sing as
prodSing = \case
    Ø        -> SNil
    s :< ss -> s `SCons` prodSing ss

splitSing
    :: Length ns
    -> Sing (ns ++ ms)
    -> (Sing ns, Sing ms)
splitSing = \case
    LZ   -> \ss -> (SNil, ss)
    LS l -> \case
      s `SCons` ss -> first (s `SCons`) (splitSing l ss)

takeSing
    :: Length ns
    -> Length ms
    -> Sing (ns ++ ms)
    -> Sing ns
takeSing = \case
    LZ   -> \_ _ -> SNil
    LS l -> \lM -> \case
      s `SCons` ss -> s `SCons` takeSing l lM ss

singProdNat
    :: forall (as :: [N]). ()
    => Sing as
    -> Prod Nat as
singProdNat = \case
    SNil              -> Ø
    (SN n) `SCons` ns -> n :< singProdNat ns


data instance Sing (n :: N) where
    SN :: { getNat :: !(Nat n) } -> Sing n

instance Known Nat a => SingI (a :: N) where
    sing = SN known

entailNat
    :: forall n. (SingI n :- Known Nat n)
entailNat = Sub $ case (sing :: Sing n) of
                    SN n -> Wit \\ n

singSings
    :: forall ns. ()
    => SingI ns :- ListC (SingI <$> ns)
singSings = Sub (witSings (sing :: Sing ns))

witSings
    :: forall ns. ()
    => Sing ns
    -> Wit (ListC (SingI <$> ns))
witSings = \case SNil         -> Wit
                 s `SCons` ss -> case witSings ss of
                                   Wit -> withSingI s Wit


entailEvery
    :: forall (as :: [k]) (f :: k -> Constraint). ()
    => (forall (a :: k). SingI a :- f a)
    -> (SingI as :- Every f as)
entailEvery e = Sub (go (sing :: Sing as))
  where
    go :: forall bs. ()
       => Sing bs
       -> Wit (Every f bs)
    go = \case
      SNil         -> Wit
      s `SCons` ss -> case go ss of
                        Wit -> withSingI s (Wit \\ (e :: SingI (Head bs) :- f (Head bs)))

singUniform
    :: Uniform a (b ': bs)
    -> (SingI b :- SingI a)
singUniform = \case
    US _ -> Sub Wit

entailSing
    :: forall a b. ()
    => (Sing a -> Sing b)
    -> (SingI a :- SingI b)
entailSing f = Sub $ withSingI (f (sing :: Sing a)) Wit

entailSing2
    :: forall a b c. ()
    => (Sing a -> Sing b -> Sing c)
    -> ((SingI a, SingI b) :- SingI c)
entailSing2 f = Sub $ withSingI (f (sing :: Sing a) (sing :: Sing b)) Wit

singWit
    :: forall a p q t. (p, Witness p q t)
    => (Sing a -> t)
    -> (SingI a :- q)
singWit f = Sub $ Wit \\ f (sing :: Sing a)

infixr 5 %:++

(%:++)
    :: Sing as
    -> Sing bs
    -> Sing (as ++ bs)
(%:++) = \case
    SNil         -> id
    x `SCons` xs -> \ys ->
      x `SCons` (xs %:++ ys)

sReverse
    :: Sing as
    -> Sing (Reverse as)
sReverse = \case
    SNil         -> SNil
    x `SCons` xs -> sReverse xs `sSnoc` x

sSnoc
    :: Sing as
    -> Sing a
    -> Sing (as >: a)
sSnoc = \case
    SNil         -> (`SCons` SNil)
    x `SCons` xs -> (x `SCons`) . (xs `sSnoc`)

sOnly
    :: Sing a
    -> Sing '[a]
sOnly = (`SCons` SNil)

replicateSing
    :: Sing a
    -> Nat n
    -> Sing (Replicate n a)
replicateSing s = \case
    Z_   -> SNil
    S_ n -> s `SCons` replicateSing s n