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

import Data.Proxy (Proxy(..))
import Data.Semigroup (Semigroup(..))
import Data.String (String)
import Data.Type.Equality

import Language.Symantic.Grammar (Gram_Meta(..))
import Language.Symantic.Helper.Data.Type.List
import Language.Symantic.Helper.Data.Type.Peano

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

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

instance Source src => Sourced (TokenR src ts rs t) where
	type Source_of (TokenR src ts rs t) = src
	source_of (TokenZ src _) = src
	source_of (TokenS tok)   = source_of tok
	source_is (TokenZ _ tok) src = TokenZ src tok
	source_is (TokenS tok)   src = TokenS $ source_is tok src

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

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

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

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

-- *** Type 'TestEquality_TokenR'
instance
 TestEquality_TokenR src ts rs =>
 TestEquality (TokenR src ts rs) where
	testEquality = testEqualityR
class TestEquality_TokenR src (ts::[*]) (rs::[*]) where
	testEqualityR :: TokenR src ts rs x
	              -> TokenR src ts rs y
	              -> Maybe (x :~: y)
instance
 ( Eq src
 , Eq (TokenT src ts t)
 , TestEquality_TokenR src ts (r ': rs)
 ) => TestEquality_TokenR src ts (t ': r ': rs) where
	testEqualityR (TokenZ _xl x) (TokenZ _yl y)
	 | {-xl == yl &&-} x == y
	 = Just Refl
	testEqualityR (TokenS x) (TokenS y) = testEqualityR x y
	testEqualityR _ _ = Nothing
instance
 ( Eq src
 , Eq (TokenT src ts t)
 ) => TestEquality_TokenR src ts (t ': '[]) where
	testEqualityR (TokenZ _xl x) (TokenZ _yl y)
	 | {-xl == yl &&-} x == y
	 = Just Refl
	testEqualityR _ _ = Nothing

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

-- *** Type 'Show_TokenR'
instance Show_TokenR src ts rs => Show (TokenR src ts rs t) where
	show = show_TokenR
class Show_TokenR src (ts::[*]) (rs::[*]) where
	show_TokenR :: TokenR src ts rs x -> String
instance
 ( Show src
 , Show (TokenT src ts t)
 , Show_TokenR src ts (r ': rs)
 ) => Show_TokenR src ts (t ': r ': rs) where
	show_TokenR (TokenZ m t) = show (m, t)
	show_TokenR (TokenS rs) = show_TokenR rs
instance
 ( Show src
 , Show (TokenT src ts t)
 ) => Show_TokenR src 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 src (ts::[*])
 = forall t. EToken (Token src ts t)

instance (Eq_Token src ts, Eq src) => Eq (EToken src ts) where
	EToken x == EToken y = eq_TokenR (==) x y
instance Show_Token src ts => Show (EToken src ts) where
	show (EToken x) = show x
instance Source src => Sourced (EToken src ts) where
	type Source_of (EToken src ts) = src
	source_of (EToken tok) = source_of tok
	source_is (EToken tok) src = EToken $ source_is tok src

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

inj_Token
 :: forall src ts t.
    Inj_Token src ts t
 => src
 -> TokenT src ts (Proxy t)
 -> Token  src ts (Proxy t)
inj_Token = inj_TokenP (Proxy @(Index ts (Proxy t)))

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

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

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

-- *** Type family 'Inj_TokensR'
type family Inj_TokensR src ts ts_to_inj where
 Inj_TokensR src ts '[] = '[]
 Inj_TokensR src ts (Proxy t ': rs) = Inj_Token src ts t ': Inj_TokensR src ts rs

-- * 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 src ts t u.
 Proj_Token ts t
 => Token src ts u
 -> Maybe (Proxy t :~: u, src, TokenT src ts u)
proj_Token = proj_TokenP (Proxy @(Index ts (Proxy t)))

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

-- ** Type 'Proj_TokenP'
class Proj_TokenP p ts rs t where
	proj_TokenP
	 :: Proxy p -> TokenR src ts rs u
	 -> Maybe (Proxy t :~: u, src, TokenT src ts u)
instance Proj_TokenP Zero ts (Proxy t ': rs) t where
	proj_TokenP _p (TokenZ src tok) = Just (Refl, src, 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 @p) u

-- * Class 'Source'
class Source src where
	sourceLess :: src
instance Source () where
	sourceLess = ()

-- * Class 'Inj_Source'
class Source src => Inj_Source a src where
	inj_Source :: a -> src
instance Inj_Source a () where
	inj_Source _ = ()

-- ** Type 'Sourced'
class Source (Source_of a) => Sourced a where
	type Source_of a
	source_of :: a -> Source_of a
	source_is :: a -> Source_of a -> a
infixl 5 `source_is`

source :: (Inj_Source src (Source_of a), Sourced a) => a -> src -> a
source a src = a `source_is` inj_Source src

-- ** Type 'Text_of_Source'
type family Text_of_Source (src :: *) :: *

sourceG :: forall meta src g a.
 ( Gram_Meta meta g
 , meta ~ Text_of_Source src
 , Inj_Source meta src
 , Functor g
 ) => g (src -> a) -> g a
sourceG g = metaG $ (\f (txt::Text_of_Source src) -> f (inj_Source txt :: src)) <$> g

-- * Type 'At'
-- | Attach a source.
data At src a
 =   At src a
 deriving (Eq, Show)

instance Functor (At src) where
	fmap f (At src a) = At src (f a)
unAt :: At src a -> a
unAt (At _ a) = a

-- * Type 'BinTree'
-- | Binary Tree.
data BinTree a
 =   BinTree0 a
 |   BinTree1 (BinTree a) (BinTree a)
 deriving (Eq, Show)

instance Semigroup (BinTree a) where
	(<>) = BinTree1
instance Functor BinTree where
	fmap f (BinTree0 a)   = BinTree0 (f a)
	fmap f (BinTree1 x y) = BinTree1 (fmap f x) (fmap f y)
instance Applicative BinTree where
	pure = BinTree0
	BinTree0 f     <*> BinTree0 a   = BinTree0 (f a)
	BinTree0 f     <*> BinTree1 x y = BinTree1 (f  <$> x) (f  <$> y)
	BinTree1 fx fy <*> a            = BinTree1 (fx <*> a) (fy <*> a)
instance Monad BinTree where
	return = BinTree0
	BinTree0 a   >>= f = f a
	BinTree1 x y >>= f = BinTree1 (x >>= f) (y >>= f)
instance Foldable BinTree where
	foldMap f (BinTree0 a)   = f a
	foldMap f (BinTree1 x y) = foldMap f x `mappend` foldMap f y
	foldr f acc (BinTree0 a)   = f a acc
	foldr f acc (BinTree1 x y) = foldr f (foldr f acc y) x
	foldl f acc (BinTree0 a)   = f acc a
	foldl f acc (BinTree1 x y) = foldl f (foldl f acc x) y
instance Traversable BinTree where
	traverse f (BinTree0 a)   = BinTree0 <$> f a
	traverse f (BinTree1 x y) = BinTree1 <$> traverse f x <*> traverse f y