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

import Data.Maybe (isJust)
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 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
	testEquality (TokenZ x) (TokenZ y) | x == y = Just Refl
	testEquality (TokenS x) (TokenS y) | Just Refl <- testEquality x y = Just Refl
	testEquality _ _ = Nothing
instance
 Eq (TokenT ss (Proxy s)) =>
 TestEquality (TokenR ss (Proxy s ': '[])) where
	testEquality (TokenZ x) (TokenZ y) | x == y = Just Refl
	testEquality _ _ = Nothing
instance TestEquality (TokenR ss rs) => Eq (TokenR ss rs s) where
	x == y = isJust $ testEquality 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 $ testEquality x y
instance Show_Token ss => Show (EToken src ss) where
	show (EToken _src x) = show x
instance Source src => Sourced (EToken src ss) where
	type Source_of (EToken src ss)  = src
	source_of (EToken src _tok)     = src
	source_is (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

-- * 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 :: *) :: *
type instance Text_of_Source () = ()

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