{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Language.Symantic.Typing.Constant where

import qualified Data.Kind as Kind
import qualified Data.Map.Strict as Map
import qualified Data.MonoTraversable as MT
import qualified Data.Sequences as Seqs
import Data.NonNull (NonNull)
import Data.Proxy
import Data.Text (Text)
import Data.Type.Equality
import qualified System.IO as IO

import Language.Symantic.Helper.Data.Type.List
import Language.Symantic.Helper.Data.Type.Peano
import Language.Symantic.Typing.Kind

-- * Type 'TyConst'
-- | A /type constant/,
-- indexed at the Haskell type and term level amongst a list of them.
-- When used, @c@ is actually wrapped within a 'Proxy'
-- to be able to handle constants of different 'Kind's.
data TyConst (cs::[Kind.Type]) (c::k) where
	TyConstZ :: SKind k -> TyConst (Proxy c ': cs) (c::k)
	TyConstS :: TyConst cs c -> TyConst (not_c ': cs) c
infixr 5 `TyConstS`

eq_Kind_TyConst :: TyConst cs (x::kx) -> TyConst cs (y::ky) -> Maybe (kx:~:ky)
eq_Kind_TyConst x y = eq_skind (kind_of_TyConst x) (kind_of_TyConst y)

instance TestEquality (TyConst cs) where
	testEquality TyConstZ{} TyConstZ{}     = Just Refl
	testEquality (TyConstS x) (TyConstS y) = testEquality x y
	testEquality _ _                   = Nothing

kind_of_TyConst :: TyConst cs (h::k) -> SKind k
kind_of_TyConst (TyConstZ ki) = ki
kind_of_TyConst (TyConstS c)  = kind_of_TyConst c

-- * Type 'Inj_TyConst'
-- | Convenient type synonym wrapping 'Inj_ConstP'
-- applied on the correct 'Index'.
type Inj_TyConst cs c = Inj_ConstP (Index cs (Proxy c)) cs c

-- | Inject a given /type constant/ @c@ into a list of them,
-- by returning a proof that 'Proxy'@ c@ is in @cs@.
inj_TyConst :: forall cs c. Inj_TyConst cs c => TyConst cs c
inj_TyConst = inj_TyConstP (Proxy @(Index cs (Proxy c)))

-- ** Class 'Inj_ConstP'
class Inj_ConstP p cs c where
	inj_TyConstP :: Proxy p -> TyConst cs c
{- NOTE: using this commented instance fails very badly due to GHC-8.0.1's bug #12933
         which makes it fail to calculate the right kind,
         it seems to wrongly reuse the kind of the first use (sic)…
instance IKind k => Inj_ConstP Zero (Proxy c ': cs) (c::k) where
	inj_TyConstP _ = TyConstZ kind
-}
instance
 ( IKindP (Ty_of_Type k)
 , Type_of_Ty (Ty_of_Type k) ~ k
 ) => Inj_ConstP Zero (Proxy c ': cs) (c::k) where
	inj_TyConstP _ = TyConstZ (kindP (Proxy :: Proxy (Ty_of_Type k)))
instance Inj_ConstP p cs c => Inj_ConstP (Succ p) (not_c ': cs) c where
	inj_TyConstP _p = TyConstS (inj_TyConstP (Proxy @p))

-- * Class 'Proj_TyConst'
-- | Convenient type synonym wrapping 'Proj_TyConstP'
-- applied on the correct 'Index'.
type Proj_TyConst cs c = Proj_TyConstP (Index cs (Proxy c)) cs c

-- | Project a 'TyConst' onto a Haskell type level /type constant/ @c@,
-- returning a proof that the 'TyConst' indexes @c@ iif. it's the case.
proj_TyConst :: forall cs k (c::k) (u::k).
 Proj_TyConst cs c => TyConst cs u -> Proxy c -> Maybe (c :~: u)
proj_TyConst = proj_TyConstP (Proxy @(Index cs (Proxy c)))

(=?) :: forall cs c u. Proj_TyConst cs c => TyConst cs u -> Proxy c -> Maybe (c :~: u)
(=?) = proj_TyConstP (Proxy @(Index cs (Proxy c)))

-- ** Type 'Proj_TyConstP'
class Proj_TyConstP p cs c where
	proj_TyConstP :: Proxy p -> TyConst cs u -> Proxy c -> Maybe (c :~: u)
instance Proj_TyConstP Zero (Proxy c ': cs) c where
	proj_TyConstP _p TyConstZ{} _c = Just Refl
	proj_TyConstP _p TyConstS{} _c = Nothing
instance Proj_TyConstP p cs c => Proj_TyConstP (Succ p) (not_c ': cs) c where
	proj_TyConstP _p TyConstZ{} _c  = Nothing
	proj_TyConstP _p (TyConstS u) c = proj_TyConstP (Proxy @p) u c

-- ** Type 'Proj_TyConsts'
type Proj_TyConsts cs cs_to_proj
 = Concat_Constraints (Proj_TyConstsR cs cs_to_proj)

-- *** Type family 'Proj_TyConstsR'
type family Proj_TyConstsR cs cs_to_proj where
 Proj_TyConstsR cs '[] = '[]
 Proj_TyConstsR cs (Proxy x ': xs) = Proj_TyConst cs x ': Proj_TyConstsR cs xs

-- * Class 'Show_TyConst'
class Show_TyConst cs where
	show_TyConst :: TyConst cs c -> String

-- deriving instance Show (TyConst cs c)
instance Show_TyConst cs => Show (TyConst cs c) where
	show = show_TyConst
instance Show_TyConst '[] where
	show_TyConst = error "Show_TyConst unreachable pattern"

-- TODO: move each of these to a dedicated module.
instance Show_TyConst cs => Show_TyConst (Proxy Bounded ': cs) where
	show_TyConst TyConstZ{} = "Bounded"
	show_TyConst (TyConstS c) = show_TyConst c
instance Show_TyConst cs => Show_TyConst (Proxy Enum ': cs) where
	show_TyConst TyConstZ{} = "Enum"
	show_TyConst (TyConstS c) = show_TyConst c
instance Show_TyConst cs => Show_TyConst (Proxy Fractional ': cs) where
	show_TyConst TyConstZ{} = "Fractional"
	show_TyConst (TyConstS c) = show_TyConst c
instance Show_TyConst cs => Show_TyConst (Proxy Real ': cs) where
	show_TyConst TyConstZ{} = "Real"
	show_TyConst (TyConstS c) = show_TyConst c

-- * Type 'Constants'
-- | Usual 'TyConst's.
type Constants = Terms ++ Constraints

-- ** Type 'Terms'
-- | Usual 'TyConst's of /terms constructors/.
type Terms =
 [ Proxy ()
 , Proxy (,)
 , Proxy (->)
 , Proxy []
 , Proxy Bool
 , Proxy Char
 , Proxy Either
 , Proxy Int
 , Proxy Integer
 , Proxy Integral
 , Proxy IO
 , Proxy IO.Handle
 , Proxy IO.IOMode
 , Proxy Map.Map
 , Proxy Maybe
 , Proxy NonNull
 , Proxy Text
 ]

-- ** Type 'Constraints'
-- | Usual 'TyConst's of /type constraint constructors/.
type Constraints =
 [ Proxy Applicative
 , Proxy Bounded
 , Proxy Enum
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Monad
 , Proxy Monoid
 , Proxy MT.MonoFoldable
 , Proxy MT.MonoFunctor
 , Proxy Num
 , Proxy Ord
 , Proxy Real
 , Proxy Seqs.IsSequence
 , Proxy Seqs.SemiSequence
 , Proxy Show
 , Proxy Traversable
 ]