module Language.Symantic.Parsing.Token where

import Data.Semigroup (Semigroup(..))

import Language.Symantic.Grammar (Gram_Meta(..))

-- * Type 'Token'
type Token ss = TokenR ss ss

-- ** Type 'TokenR'
data TokenR (ss::[*]) (rs::[*]) (s:: *) where
	TokenZ :: TokenT ss s -> TokenR ss (s ': rs) s
	TokenS :: TokenR ss rs s -> TokenR ss (not_s ': rs) s
infixr 5 `TokenS`

-- ** Data family 'TokenT'
data family TokenT (ss::[*]) (s:: *) :: *

-- * Class 'Eq_Token'
type Eq_Token ss = TestEquality (Token ss)
instance
 ( Eq (TokenT ss (Proxy s))
 , TestEquality (TokenR ss (r ': rs))
 ) => TestEquality (TokenR ss (Proxy s ': r ': rs)) where
	ctxtEquality (TokenZ x) (TokenZ y) | x == y = Just Refl
	ctxtEquality (TokenS x) (TokenS y) | Just Refl <- ctxtEquality x y = Just Refl
	ctxtEquality _ _ = Nothing
instance
 Eq (TokenT ss (Proxy s)) =>
 TestEquality (TokenR ss (Proxy s ': '[])) where
	ctxtEquality (TokenZ x) (TokenZ y) | x == y = Just Refl
	ctxtEquality _ _ = Nothing
instance TestEquality (TokenR ss rs) => Eq (TokenR ss rs s) where
	x == y = isJust $ ctxtEquality x y

-- ** Type 'Show_Token'
type Show_Token ss = Show_TokenR ss ss

-- *** Type 'Show_TokenR'
class Show_TokenR (ss::[*]) (rs::[*]) where
	show_TokenR :: TokenR ss rs x -> String
instance
 ( Show (TokenT ss (Proxy s))
 , Show_TokenR ss (r ': rs)
 ) => Show_TokenR ss (Proxy s ': r ': rs) where
	show_TokenR (TokenZ s)  = show s
	show_TokenR (TokenS rs) = show_TokenR rs
instance
 Show (TokenT ss (Proxy s)) =>
 Show_TokenR ss (Proxy s ': '[]) where
	show_TokenR (TokenZ s) = show s
	show_TokenR TokenS{}   = error "Oops, the impossible happened..."
instance Show_TokenR ss rs => Show (TokenR ss rs s) where
	show = show_TokenR

-- * Type 'Inj_Token'
-- | Convenient type synonym wrapping 'Inj_TokenP'
-- applied on the correct 'Index'.
type Inj_Token ss s
 =   Inj_TokenP (Index ss (Proxy s)) ss ss s

inj_Token
 :: forall ss s. Inj_Token ss s
 => TokenT ss (Proxy s)
 -> Token  ss (Proxy s)
inj_Token = inj_TokenP (Proxy @(Index ss (Proxy s)))

-- ** Class 'Inj_TokenP'
class Inj_TokenP p ss rs (s::ks) where
	inj_TokenP :: Proxy p -> TokenT ss (Proxy s) -> TokenR ss rs (Proxy s)
instance Inj_TokenP Zero ss (Proxy s ': rs) s where
	inj_TokenP _ = TokenZ
instance
 Inj_TokenP p ss rs s =>
 Inj_TokenP (Succ p) ss (not_t ': rs) s where
	inj_TokenP _p = TokenS . inj_TokenP (Proxy @p)

-- ** Type 'Inj_Tokens'
type Inj_Tokens ss ts_to_inj
 = Concat_Constraints (Inj_TokensR ss ts_to_inj)

-- *** Type family 'Inj_TokensR'
type family Inj_TokensR ss ts_to_inj where
 Inj_TokensR ss '[] = '[]
 Inj_TokensR ss (Proxy s ': rs) = Inj_Token ss s ': Inj_TokensR ss rs

-- * Class 'Proj_Token'
-- | Convenient type synonym wrapping 'Proj_TokenP'
-- applied on the correct 'Index'.
type Proj_Token ss s
 =   Proj_TokenP (Index ss (Proxy s)) ss ss s

proj_Token
 :: forall ss s u.
    Proj_Token ss s
 => Token ss u
 -> Maybe (Proxy s :~: u, TokenT ss u)
proj_Token = proj_TokenP (Proxy @(Index ss (Proxy s)))

-- ** Type 'Proj_TokenP'
class Proj_TokenP p ss rs s where
	proj_TokenP
	 :: Proxy p -> TokenR ss rs u
	 -> Maybe (Proxy s :~: u, TokenT ss u)
instance Proj_TokenP Zero ss (Proxy s ': rs) s where
	proj_TokenP _p (TokenZ tok) = Just (Refl, tok)
	proj_TokenP _p TokenS{}     = Nothing
instance Proj_TokenP p ss rs s => Proj_TokenP (Succ p) ss (not_t ': rs) s where
	proj_TokenP _p TokenZ{}   = Nothing
	proj_TokenP _p (TokenS u) = proj_TokenP (Proxy @p) u

-- ** Type 'EToken'
-- | Existential 'Token'.
data EToken src (ss::[*])
 = forall s. EToken src (Token ss (Proxy s))

instance Eq_Token ss => Eq (EToken src ss) where
	EToken _sx x == EToken _sy y = isJust $ ctxtEquality x y
instance Show_Token ss => Show (EToken src ss) where
	show (EToken _src x) = show x
type instance SourceOf (EToken src ss) = src
instance Source src => Sourced (EToken src ss) where
	sourceOf (EToken src _tok)     = src
	setSource (EToken _src tok) src = EToken src tok

inj_EToken
 :: forall src ss s.
    Inj_Token ss s
 => src -> TokenT ss (Proxy s) -> EToken src ss
inj_EToken src = EToken src . inj_TokenP (Proxy @(Index ss (Proxy s)))

proj_EToken
 :: forall src ss s.
    Proj_Token ss s
 => EToken src ss
 -> Maybe (src, TokenT ss (Proxy s))
proj_EToken (EToken src (tok::TokenR ss ss (Proxy u))) =
	case proj_Token tok of
	 Just (Refl :: Proxy s :~: Proxy u, to) -> Just (src, to)
	 Nothing -> Nothing