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

import Data.Maybe (fromMaybe)

import Language.Symantic.Parsing
import Language.Symantic.Typing.Kind
import Language.Symantic.Typing.Constant
import Language.Symantic.Typing.Type
import Language.Symantic.Typing.Grammar

-- * Class 'CompileTyName'
-- | Read a 'Type' from a 'TyName'.
type CompileTyName cs = Compile_TyNameR cs cs

compileTyName
 :: forall src cs ret.
 (Compile_TyNameR cs cs, Source src)
 => src -> TyName
 -> (forall k c. Type src cs (c::k) -> Maybe ret)
 -> Maybe ret
compileTyName = compile_TyNameR (Proxy @cs)

-- ** Class 'Compile_TyNameR'
class Compile_TyNameR cs rs where
	compile_TyNameR
	 :: Source src
	 => Proxy rs -> src -> TyName
	 -> (forall k c. Type src cs (c::k) -> Maybe ret)
	 -> Maybe ret

instance Compile_TyNameR cs '[] where
	compile_TyNameR _rs _src _n _k = Nothing

-- TODO: move each of these to a dedicated module.
instance
 ( Compile_TyNameR cs rs
 , Inj_TyConst cs Fractional
 ) => Compile_TyNameR  cs (Proxy Fractional ': rs) where
	compile_TyNameR _cs src (TyName "Fractional") k = k (tySourced @Fractional src)
	compile_TyNameR _rs src n k = compile_TyNameR (Proxy @rs) src n k
instance
 ( Compile_TyNameR cs rs
 , Inj_TyConst cs []
 , Inj_TyConst cs Char
 ) => Compile_TyNameR cs (Proxy String ': rs) where
	compile_TyNameR _cs src (TyName "String") k = k (TyApp src (tySourced @[] src) (tySourced @Char src))
	compile_TyNameR _rs src n k = compile_TyNameR (Proxy @rs) src n k

-- * 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 'CompileTy'
-- | Read a 'Type' from an 'AST_Type'.
class CompileTy cs where
	compileTy ::
	 ( Inj_Error  (Error_Type src) err
	 , Inj_Error  (Con_Kind   src) err
	 , Inj_Source (EKind src)    src
	 , Inj_Source (EType src cs) src
	 , Inj_Source (AST_Type src) src
	 ) => AST_Type src
	 -> (forall k h. Type src cs (h::k) -> Either err ret)
	 -> Either err ret

instance
 ( CompileTyName cs
 ) => CompileTy cs where
	compileTy
	 :: forall src err ret.
	 ( Inj_Error  (Error_Type src) err
	 , Inj_Error  (Con_Kind   src) err
	 , Inj_Source (EKind src)    src
	 , Inj_Source (EType src cs) src
	 , Inj_Source (AST_Type src) src
	 ) => AST_Type src
	 -> (forall k h. Type src cs (h::k) -> Either err ret)
	 -> Either err ret
	compileTy 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) $
		compileTyName (inj_Source ast) name $ \typ -> Just $
		k typ
	compileTy ast@(ast_x `BinTree1` ast_y) k =
		compileTy @cs ast_x $ \ty_x ->
		compileTy @cs 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
	compileTy ast _k = Left $ inj_Error $ Error_Type_Token_invalid @src $ inj_Source ast
	 -- TODO: make this an "Oops, the impossible happened"?

compile_EType
 :: ( CompileTyName cs
    , Inj_Source (AST_Type src) src
    , Inj_Source (EType src cs) src
    , Inj_Source (EKind src)    src
    )
 => AST_Type src
 -> Either (Error_Type src) (EType src cs)
compile_EType tok = compileTy tok (Right . EType)


-- * Type 'Src'
data Src txt cs is
 =   Src_Less
 |   Src_Text     txt
 |   Src_Token    (EToken (Src txt cs is) is)
 |   Src_AST_Term (AST_Term (Src txt cs is) is)
 |   Src_AST_Type (AST_Type (Src txt cs is))
 |   Src_Type     (EType  (Src txt cs is) cs)
 |   Src_Term
deriving instance (Eq_Token (Src txt cs is) is, Eq txt) => Eq (Src txt cs is)
deriving instance
 ( Show_Token (Src txt cs is) is
 , Show_TyConst cs
 , Show txt
 , Fixity_TyConst cs
 , Source txt
 ) => Show (Src txt cs is)
type instance Text_of_Source (Src txt cs is) = txt

instance Source (Src txt cs is) where
	sourceLess = Src_Less
instance Inj_Source txt (Src txt cs is) where
	inj_Source = Src_Text
instance Inj_Source (EToken (Src txt cs is) is) (Src txt cs is) where
	inj_Source = Src_Token
instance Inj_Source (AST_Term (Src txt cs is) is) (Src txt cs is) where
	inj_Source = Src_AST_Term
instance Inj_Source (AST_Type (Src txt cs is)) (Src txt cs is) where
	inj_Source = Src_AST_Type
instance Inj_Source (EType (Src txt cs is) cs) (Src txt cs is) where
	inj_Source = Src_Type