{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Parsing.Token where

import Data.Proxy (Proxy(..))
import Data.String (String)
import Data.Type.Equality
import Language.Symantic.Lib.Data.Type.List
import Language.Symantic.Lib.Data.Type.Peano

-- * Type 'Token'
type Token meta ts = TokenR meta ts ts

-- ** Type 'TokenR'
data TokenR meta (ts::[*]) (rs::[*]) (t:: *) where
	TokenZ :: meta -> TokenT meta ts t
	       -> TokenR meta ts (t ': rs) t
	TokenS :: TokenR meta ts rs t -> TokenR meta ts (not_t ': rs) t
infixr 5 `TokenS`

-- ** Data family 'TokenT'
data family TokenT meta (ts::[*]) (t:: *) :: *

-- ** Type 'Eq_Token'
type Eq_Token meta ts = Eq_TokenR meta ts ts

-- *** Type 'Eq_TokenR'
instance Eq_TokenR meta ts rs => Eq (TokenR meta ts rs t) where
	(==) = eq_TokenR
class Eq_TokenR meta (ts::[*]) (rs::[*]) where
	eq_TokenR :: TokenR meta ts rs x -> TokenR meta ts rs y -> Bool
instance
 ( Eq meta
 , Eq (TokenT meta ts t)
 , Eq_TokenR meta ts (r ': rs)
 ) => Eq_TokenR meta ts (t ': r ': rs) where
	eq_TokenR (TokenZ mx x) (TokenZ my y) = mx == my && x == y
	eq_TokenR (TokenS x) (TokenS y) = eq_TokenR x y
	eq_TokenR _ _ = False
instance
 ( Eq meta
 , Eq (TokenT meta ts t)
 ) => Eq_TokenR meta ts (t ': '[]) where
	eq_TokenR (TokenZ mx x) (TokenZ my y) = mx == my && x == y
	eq_TokenR _ _ = False

-- ** Type 'TestEquality_Token'
type TestEquality_Token meta ts = TestEquality_TokenR meta ts ts

-- *** Type 'TestEquality_TokenR'
instance TestEquality_TokenR meta ts rs => TestEquality (TokenR meta ts rs) where
	testEquality = testEqualityR
class TestEquality_TokenR meta (ts::[*]) (rs::[*]) where
	testEqualityR :: TokenR meta ts rs x -> TokenR meta ts rs y -> Maybe (x :~: y)
instance
 ( Eq meta
 , Eq (TokenT meta ts t)
 , TestEquality_TokenR meta ts (r ': rs)
 ) => TestEquality_TokenR meta ts (t ': r ': rs) where
	testEqualityR (TokenZ mx x) (TokenZ my y)
	 | mx == my && x == y
	 = Just Refl
	testEqualityR (TokenS x) (TokenS y) = testEqualityR x y
	testEqualityR _ _ = Nothing
instance
 ( Eq meta
 , Eq (TokenT meta ts t)
 ) => TestEquality_TokenR meta ts (t ': '[]) where
	testEqualityR (TokenZ mx x) (TokenZ my y)
	 | mx == my && x == y
	 = Just Refl
	testEqualityR _ _ = Nothing

-- ** Type 'Show_Token'
type Show_Token meta ts = Show_TokenR meta ts ts

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

-- ** Type 'EToken'
-- | Existential 'Token'.
data EToken meta (ts::[*]) = forall t. EToken (Token meta ts t)

instance Eq_Token meta ts => Eq (EToken meta ts) where
	EToken x == EToken y = eq_TokenR x y
instance Show_Token meta ts => Show (EToken meta ts) where
	show (EToken x) = show x

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

inj_token
 :: forall meta ts t. Inj_Token meta ts t
 => meta
 -> TokenT meta ts (Proxy t)
 -> Token  meta ts (Proxy t)
inj_token = inj_tokenP (Proxy::Proxy (Index ts (Proxy t)))

-- ** Class 'Inj_TokenP'
class Inj_TokenP p meta ts rs (t::kt) where
	inj_tokenP :: Proxy p -> meta
	 -> TokenT meta ts    (Proxy t)
	 -> TokenR meta ts rs (Proxy t)
instance Inj_TokenP Zero meta ts (Proxy t ': rs) t where
	inj_tokenP _ = TokenZ
instance
 Inj_TokenP p meta ts rs t =>
 Inj_TokenP (Succ p) meta ts (not_t ': rs) t where
	inj_tokenP _p meta = TokenS . inj_tokenP (Proxy::Proxy p) meta

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

proj_token :: forall meta ts t u.
 Proj_Token ts t
 => Token meta ts u
 -> Maybe (Proxy t :~: u, meta, TokenT meta ts u)
proj_token = proj_tokenP (Proxy::Proxy (Index ts (Proxy t)))

proj_etoken :: forall meta ts t.
 Proj_Token ts t
 => EToken meta ts
 -> Maybe (TokenT meta ts (Proxy t))
proj_etoken (EToken (tok::TokenR meta ts ts u)) =
	case proj_token tok of
	 Just (Refl :: Proxy t :~: u, _meta, tokD) -> Just tokD
	 Nothing -> Nothing

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

-- * Type 'At'
-- | Attach a location.
data At meta ts a
 =   At (Maybe (EToken meta ts)) a
deriving instance (Eq_Token meta ts, Eq a) => Eq (At meta ts a)
deriving instance (Show_Token meta ts, Show a) => Show (At meta ts a)
instance Functor (At meta ts) where
	fmap f (At at a) = At at (f a)
unAt :: At meta ts a -> a
unAt (At _ a) = a

-- * Class 'Meta_of'
class Meta_of tok where
	type Meta_Of tok
	meta_of :: tok -> Meta_Of tok
instance Meta_of (TokenR meta ts rs t) where
	type Meta_Of (TokenR meta ts rs t) = meta
	meta_of (TokenZ m _) = m
	meta_of (TokenS t) = meta_of t
instance Meta_of (EToken meta ts) where
	type Meta_Of (EToken meta ts) = meta
	meta_of (EToken t) = meta_of t