{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Typing.Read where

import Control.Applicative ((<|>))
import Data.Maybe (fromMaybe)

import Language.Symantic.Parsing
import Language.Symantic.Typing.Kind
import Language.Symantic.Typing.Type
import Language.Symantic.Typing.Show ()
import Language.Symantic.Typing.Grammar

-- * Class 'Read_TyName'
-- | Read a 'Type' from a 'TyName'.
type Read_TyName cs = Read_TyNameR cs cs

read_TyName
 :: forall src ctx ss cs.
    Source src
 => Read_TyNameR cs cs
 => src -> TyName
 -> Maybe (EType src ctx ss cs)
read_TyName = read_TyNameR (Proxy @cs)

-- ** Class 'Read_TyNameR'
class Read_TyNameR cs rs where
	read_TyNameR
	 :: Source src
	 => Proxy rs -> src -> TyName
	 -> Maybe (EType src ctx ss cs)
instance Read_TyNameR cs '[] where
	read_TyNameR _rs _src _n = Nothing
instance
 ( Read_TyNameC cs c
 , Read_TyNameR cs rs
 ) => Read_TyNameR cs (Proxy c ': rs) where
	read_TyNameR _rs src n =
		read_TyNameC (Proxy @c)  src n <|>
		read_TyNameR (Proxy @rs) src n

-- ** Class 'Read_TyNameC'
class Read_TyNameC cs c where
	read_TyNameC
	 :: Source src
	 => Proxy c -> src -> TyName
	 -> Maybe (EType src ctx ss cs)

-- * Type 'Error_Type'
data Error_Type src
 =   Error_Type_Token_invalid    src
 |   Error_Type_Constant_unknown (At src TyName)
 |   Error_Type_Con_Kind         (Con_Kind src)
 deriving (Eq, Show)

instance Inj_Error (Error_Type src) (Error_Type src) where
	inj_Error = id
instance Inj_Error (Con_Kind src) (Error_Type src) where
	inj_Error = inj_Error . Error_Type_Con_Kind

-- * Class 'Read_Type'
-- | Read a 'Type' from an 'AST_Type'.
class Read_Type cs where
	read_Type
	 :: forall ctx ss src err ret.
	    Inj_Error  (Error_Type src) err
	 => Inj_Error  (Con_Kind   src) err
	 => Inj_Source (EKind src) src
	 => Inj_Source (EType src '[] ss cs) src
	 => Inj_Source (AST_Type src) src
	 => AST_Type src
	 -> (forall k h. Type src ctx ss cs (h::k) -> Either err ret)
	 -> Either err ret

instance Read_TyName cs => Read_Type cs where
	read_Type
	 :: forall ctx ss src err ret.
	    Inj_Error  (Error_Type src) err
	 => Inj_Error  (Con_Kind   src) err
	 => Inj_Source (EKind src) src
	 => Inj_Source (EType src '[] ss cs) src
	 => Inj_Source (AST_Type src) src
	 => AST_Type src
	 -> (forall k h. Type src ctx ss cs (h::k) -> Either err ret)
	 -> Either err ret
	read_Type ast@(BinTree0 (proj_EToken -> Just (_src, Token_Type_Name name))) k =
		fromMaybe (Left $ inj_Error $ Error_Type_Constant_unknown @src $ At (inj_Source ast) name) $ do
			EType typ <- read_TyName (inj_Source ast) name
			Just $ k typ
	read_Type ast@(ast_x `BinTree1` ast_y) k =
		read_Type @cs @ctx @ss ast_x $ \ty_x ->
		read_Type @cs @ctx @ss ast_y $ \ty_y ->
		if_KiArrow (kindTy ty_x) $ \Refl ki_x_a _ki_x_b ->
		if_EqKind ki_x_a (kindTy ty_y) $ \Refl ->
		k $ TyApp (inj_Source ast) ty_x ty_y
	read_Type ast _k = Left $ inj_Error $ Error_Type_Token_invalid @src $ inj_Source ast
	 -- TODO: make this an "Oops, the impossible happened"?

-- | Read a 'Type'.
readTy
 :: Read_TyName cs
 => Inj_Source (AST_Type src) src
 => Inj_Source (EType src '[] ss cs) src
 => Inj_Source (EKind src) src
 => AST_Type src
 -> Either (Error_Type src) (EType src ctx ss cs)
readTy tok = read_Type tok (Right . EType)