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

import Data.Proxy
import Data.Type.Equality
import qualified Data.Kind as K

import Language.Symantic.Grammar
import Language.Symantic.Helper.Data.Type.List
import Language.Symantic.Helper.Data.Type.Peano
import Language.Symantic.Helper.Data.Type.Equality
import Language.Symantic.Parsing
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 src (cs::[K.Type]) (c::k) where
	TyConstZ :: Kind src k -> TyConst src (Proxy c ': cs) (c::k)
	TyConstS :: TyConst src cs c -> TyConst src (not_c ': cs) c
infixr 5 `TyConstS`

eqTyConst :: TyConst xs cs (x::k) -> TyConst ys cs (y::k) -> Maybe (x:~:y)
eqTyConst TyConstZ{} TyConstZ{}     = Just Refl
eqTyConst (TyConstS x) (TyConstS y) = eqTyConst x y
eqTyConst _ _                       = Nothing

eqKiTyConst :: TyConst xs cs (x::kx) -> TyConst ys cs (y::ky) -> Maybe (x:~~:y)
eqKiTyConst TyConstZ{} TyConstZ{}     = Just KRefl
eqKiTyConst (TyConstS x) (TyConstS y) = eqKiTyConst x y
eqKiTyConst _ _                       = Nothing

instance TestEquality (TyConst src cs) where
	testEquality = eqTyConst

kindTyConst :: TyConst src cs (h::k) -> Kind src k
kindTyConst (TyConstZ ki) = ki
kindTyConst (TyConstS c)  = kindTyConst c

-- * Type 'Inj_TyConst'
-- | Convenient type synonym wrapping 'Inj_TyConstP'
-- applied on the correct 'Index'.
type Inj_TyConst cs c = Inj_TyConstP (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 c src cs. (Inj_TyConst cs c, Source src) => TyConst src cs c
inj_TyConst = inj_TyConstP (Proxy @(Index cs (Proxy c)))

-- ** Class 'Inj_TyConstP'
class Inj_TyConstP p cs c where
	inj_TyConstP :: Source src => Proxy p -> TyConst src 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 Inj_Kind k => Inj_TyConstP Zero (Proxy c ': cs) (c::k) where
	inj_TyConstP _ = TyConstZ kind
-}
instance
 ( Inj_KindP (Ty_of_Type k)
 , Type_of_Ty (Ty_of_Type k) ~ k
 ) => Inj_TyConstP Zero (Proxy c ': cs) (c::k) where
	inj_TyConstP _ = TyConstZ (inj_KindP (Proxy @(Ty_of_Type k)) sourceLess)
instance Inj_TyConstP p cs c => Inj_TyConstP (Succ p) (not_c ': cs) c where
	inj_TyConstP _p = TyConstS (inj_TyConstP (Proxy @p))

-- ** Type 'Inj_TyConsts'
type Inj_TyConsts cs cs_to_inj
 = Concat_Constraints (Inj_TyConstsR cs cs_to_inj)

-- *** Type family 'Inj_TyConstsR'
type family Inj_TyConstsR cs cs_to_inj where
 Inj_TyConstsR cs '[] = '[]
 Inj_TyConstsR cs (Proxy x ': xs) = Inj_TyConst cs x ': Inj_TyConstsR cs xs

-- * 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 c src cs u.
 Proj_TyConst cs c => TyConst src cs u -> Maybe (c :~: u)
proj_TyConst u = proj_TyConstP (Proxy @(Index cs (Proxy c))) u (Proxy @c)

-- | Like 'proj_TyConst', but prove also that the 'Kind's are equal.
proj_TyConstKi :: forall kc (c::kc) src cs ku (u::ku).
 Inj_Kind kc => Proj_TyConst cs c =>
 TyConst src cs u -> Maybe (c :~~: u)
proj_TyConstKi u = do
	Refl <- eqKi (inj_Kind @kc @()) (kindTyConst u)
	Refl <- proj_TyConstP (Proxy @(Index cs (Proxy c))) u (Proxy @c)
	Just KRefl

(=?) :: forall src cs c u. Proj_TyConst cs c => TyConst src 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 src 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 src cs c -> String
instance Show_TyConst cs => Show (TyConst src cs c) where
	show = show_TyConst

instance Show_TyConstC c => Show_TyConst (Proxy c ': '[]) where
	show_TyConst TyConstZ{} = show_TyConstC (Proxy @c)
	show_TyConst TyConstS{} = error "[BUG] show_TyConst: TyConstS cannot happen here"
instance
 ( Show_TyConstC c
 , Show_TyConst (Proxy cc ': cs)
 ) => Show_TyConst (Proxy c ': Proxy cc ': cs) where
	show_TyConst TyConstZ{}    = show_TyConstC (Proxy @ c)
	show_TyConst (TyConstS cs) = show_TyConst cs

-- ** Class 'Show_TyConstC'
class Show_TyConstC c where
	show_TyConstC :: Proxy c -> String

-- TODO: move each of these to a dedicated module.
instance Show_TyConstC Fractional where
	show_TyConstC _ = "Fractional"

-- * Class 'Fixity_TyConst'
class Fixity_TyConst (cs::[K.Type]) where
	fixity_TyConst :: TyConst src cs c -> Fixity
instance Fixity_TyConstC c => Fixity_TyConst (Proxy c ': '[]) where
	fixity_TyConst TyConstZ{} = fixity_TyConstC (Proxy @c)
	fixity_TyConst TyConstS{} = error "[BUG] fixity_TyConst: TyConstS cannot happen here"
instance
 ( Fixity_TyConstC c
 , Fixity_TyConst (Proxy cc ': cs)
 ) => Fixity_TyConst (Proxy c ': Proxy cc ': cs) where
	fixity_TyConst TyConstZ{}    = fixity_TyConstC (Proxy @ c)
	fixity_TyConst (TyConstS cs) = fixity_TyConst cs

-- ** Class 'Fixity_TyConstC'
class Fixity_TyConstC c where
	fixity_TyConstC :: Proxy c -> Fixity
	fixity_TyConstC _ = FixityInfix infixN5