{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Typing.Type where

import Control.Applicative (Applicative(..), Alternative(..))
import qualified Data.Char as Char
import Data.Monoid ((<>))
import Data.Proxy
import Data.Maybe (fromMaybe, isJust)
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Type.Equality
import qualified Data.Kind as K

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

-- * Type 'Type'

-- | /Type of terms/.
--
-- * @cs@: /type constants/, fixed at compile time.
-- * @h@: indexed Haskell type.
--
-- * 'TyConst': /type constant/, selected amongst @cs@.
-- * @(:$)@: /type application/.
data Type (cs::[K.Type]) (h::k) where
	TyConst :: Const cs c -> Type  cs c
	(:$) :: Type cs f -> Type cs x -> Type cs (f x)
	-- TODO: TyVar :: SKind k -> Type cs (v::k)
infixl 9 :$

-- | 'Type' constructor to be used
-- with @TypeApplications@
-- and @NoMonomorphismRestriction@.
ty :: forall c cs. Inj_Const cs c => Type cs c
ty = TyConst inj_const
 -- NOTE: The forall brings @c@ first in the type variables,
 -- which is convenient to use @TypeApplications@.

instance TestEquality (Type cs) where
	testEquality = eq_type
instance Eq (Type cs h) where
	_x == _y = True
instance Show_Const cs => Show (Type cs h) where
	show = show_type
-- deriving instance Show_Const cs => Show (Type cs h)

kind_of :: Type cs (h::k) -> SKind k
kind_of t =
	case t of
	 TyConst c -> kind_of_const c
	 f :$ _x ->
		case kind_of f of
		 _kx `SKiArrow` kf -> kf

eq_type
 :: Type cs (x::k) -> Type cs (y::k) -> Maybe (x:~:y)
eq_type (TyConst x) (TyConst y)
 | Just Refl <- testEquality x y
 = Just Refl
eq_type (xf :$ xx) (yf :$ yx)
 | Just Refl <- eq_skind (kind_of xf) (kind_of yf)
 , Just Refl <- eq_type xf yf
 , Just Refl <- eq_type xx yx
 = Just Refl
eq_type _ _ = Nothing

eq_kind_type
 :: Type cs (x::kx) -> Type cs (y::ky) -> Maybe (kx:~:ky)
eq_kind_type (TyConst x) (TyConst y)
 | Just Refl <- eq_kind_const x y
 = Just Refl
eq_kind_type (xf :$ xx) (yf :$ yx)
 | Just Refl <- eq_kind_type xf yf
 , Just Refl <- eq_kind_type xx yx
 = Just Refl
eq_kind_type _x _y = Nothing

show_type :: Show_Const cs => Type cs h -> String
show_type (TyConst c) = show c
show_type (f@(:$){} :$ a@(:$){}) = "(" <> show_type f <> ") (" <> show_type a <> ")"
show_type (f@(:$){} :$ a) = "(" <> show_type f <> ") " <> show_type a
show_type (f :$ a@(:$){}) = show_type f <> " (" <> show_type a <> ")"
show_type (f :$ a) = show_type f <> " " <> show_type a
-- show_type (TyVar v) = "t" <> show (integral_from_peano v::Integer)

-- | Cons a @new_c@ to @cs@.
type_lift :: Type cs c -> Type (new_c ': cs) c
type_lift (TyConst c) = TyConst (ConstS c)
type_lift (f :$ a) = type_lift f :$ type_lift a

-- * Type 'EType'
-- | Existential for 'Type'.
data EType cs = forall h. EType (Type cs h)

instance Eq (EType cs) where
	EType x == EType y
	 | Just Refl <- eq_kind_type x y
	 = isJust $ eq_type x y
	_x == _y = False
instance Show_Const cs => Show (EType cs) where
	show (EType t) = show t

-- * Type 'KType'
-- | Existential for 'Type' of a known 'Kind'.
data KType cs k = forall (h::k). KType (Type cs h)

instance Eq (KType cs ki) where
	KType x == KType y = isJust $ eq_type x y
instance Show_Const cs => Show (KType cs ki) where
	show (KType t) = show_type t

-- * Type 'Token_Type'
type Token_Type = Type '[] ()

data instance TokenT meta ts (Proxy Token_Type)
 = Token_Type Text [EToken meta ts]
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Token_Type))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Token_Type))

instance
 ( Read_TypeNameR Text cs rs
 , Inj_Const cs Token_Type
 ) => Read_TypeNameR Text cs (Proxy Token_Type ': rs) where
	read_typenameR _rs "Type" k = k (ty @Token_Type)
	read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Token_Type ': cs) where
	show_const ConstZ{} = "Type"
	show_const (ConstS c) = show_const c

-- * Class 'Compile_Type'
-- | Try to build a 'Type' from name data.
class Compile_Type ts cs where
	compile_type
	 :: ( MonoLift (Error_Type meta ts) err
	    , MonoLift (Constraint_Kind meta ts) err )
	 => EToken meta ts
	 -> (forall k h. Type cs (h::k) -> Either err ret)
	 -> Either err ret

compile_etype
 :: Read_TypeName Text cs
 => EToken meta '[Proxy Token_Type]
 -> Either (Error_Type meta '[Proxy Token_Type]) (EType cs)
compile_etype tok = compile_type tok (Right . EType)

-- ** Type 'Constraint_Kind'
data Constraint_Kind meta ts
 =   Constraint_Kind_Eq    (At meta ts EKind) (At meta ts EKind)
 |   Constraint_Kind_Arrow (At meta ts EKind)
deriving instance (Eq_TokenR meta ts ts) => Eq (Constraint_Kind meta ts)
deriving instance (Show_TokenR meta ts ts) => Show (Constraint_Kind meta ts)

check_kind
 :: MonoLift (Constraint_Kind meta ts) err
 => At meta ts (SKind x)
 -> At meta ts (SKind y)
 -> ((x :~: y) -> Either err ret) -> Either err ret
check_kind x y k =
	case unAt x `eq_skind` unAt y of
	 Just Refl -> k Refl
	 Nothing -> Left $ olift $
		Constraint_Kind_Eq (EKind <$> x) (EKind <$> y)

check_kind_arrow
 :: MonoLift (Constraint_Kind meta ts) err
 => At meta ts (SKind x)
 -> (forall a b. (x :~: (a -> b)) -> SKind a -> SKind b -> Either err ret)
 -> Either err ret
check_kind_arrow x k =
	case unAt x of
	 a `SKiArrow` b -> k Refl a b
	 _ -> Left $ olift $
		Constraint_Kind_Arrow (EKind <$> x)

-- ** Type 'Error_Type'
data Error_Type meta ts
 =   Error_Type_Token_invalid    (EToken meta ts)
 |   Error_Type_Constant_unknown (At meta ts Text)
 |   Error_Type_Constraint_Kind  (Constraint_Kind meta ts)
deriving instance (Eq_TokenR meta ts ts) => Eq (Error_Type meta ts)
deriving instance (Show_TokenR meta ts ts) => Show (Error_Type meta ts)

-- * Class 'Read_TypeName'
type Read_TypeName raw cs = Read_TypeNameR raw cs cs

read_typename
 :: forall raw cs ret.
 Read_TypeNameR raw cs cs
 => raw -> (forall k c. Type cs (c::k) -> Maybe ret)
 -> Maybe ret
read_typename = read_typenameR (Proxy @cs)

-- ** Class 'Read_TypeNameR'
class Read_TypeNameR raw cs rs where
	read_typenameR
	 :: Proxy rs -> raw -> (forall k c. Type cs (c::k) -> Maybe ret)
	 -> Maybe ret

instance Read_TypeNameR raw cs '[] where
	read_typenameR _cs _c _k = Nothing

-- TODO: move each of these to a dedicated module.
instance
 ( Read_TypeNameR Text cs rs
 , Inj_Const cs Bounded
 ) => Read_TypeNameR Text cs (Proxy Bounded ': rs) where
	read_typenameR _cs "Bounded" k = k (ty @Bounded)
	read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance
 ( Read_TypeNameR Text cs rs
 , Inj_Const cs Enum
 ) => Read_TypeNameR Text cs (Proxy Enum ': rs) where
	read_typenameR _cs "Enum" k = k (ty @Enum)
	read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance
 ( Read_TypeNameR Text cs rs
 , Inj_Const cs Fractional
 ) => Read_TypeNameR Text cs (Proxy Fractional ': rs) where
	read_typenameR _cs "Fractional" k = k (ty @Fractional)
	read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance
 ( Read_TypeNameR Text cs rs
 , Inj_Const cs Real
 ) => Read_TypeNameR Text cs (Proxy Real ': rs) where
	read_typenameR _cs "Real" k = k (ty @Real)
	read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance
 ( Read_TypeNameR Text cs rs
 , Inj_Const cs []
 , Inj_Const cs Char
 ) => Read_TypeNameR Text cs (Proxy String ': rs) where
	read_typenameR _cs "String" k = k (ty @[] :$ ty @Char)
	read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k

instance
 ( Read_TypeName Text cs
 , Proj_Token ts Token_Type
 ) => Compile_Type ts cs where
	compile_type
	 :: forall meta err ret.
	 ( MonoLift (Error_Type meta ts) err
	 , MonoLift (Constraint_Kind meta ts) err
	 ) => EToken meta ts
	 -> (forall k h. Type cs (h::k) -> Either err ret)
	 -> Either err ret
	compile_type tok@(proj_etoken -> Just (Token_Type cst args)) kk =
		fromMaybe (Left $ olift $ Error_Type_Constant_unknown $ At (Just tok) cst) $
		read_typename cst $ \typ -> Just $
		go args typ kk
		where
		go :: [EToken meta ts]
		 -> Type cs h
		 -> (forall k' h'. Type cs (h'::k') -> Either err ret)
		 -> Either err ret
		go [] typ k = k typ
		go (tok_x:tok_xs) ty_f k =
			compile_type tok_x $ \(ty_x::Type cs (h'::k')) ->
			check_kind_arrow
			 (At (Just tok) $ kind_of ty_f) $ \Refl ki_f_a _ki_f_b ->
			check_kind
			 (At (Just tok) ki_f_a)
			 (At (Just tok_x) $ kind_of ty_x) $ \Refl ->
			go tok_xs (ty_f :$ ty_x) k
	compile_type tok _k = Left $ olift $ Error_Type_Token_invalid tok

-- * Type 'Types'
data Types cs (hs::[K.Type]) where
	TypesZ :: Types cs '[]
	TypesS :: Type  cs h
	       -> Types cs hs
	       -> Types cs (Proxy h ': hs)
infixr 5 `TypesS`

etypes :: Types cs hs -> [EType cs]
etypes TypesZ = []
etypes (TypesS t ts) = EType t : etypes ts

-- | Build the left spine of a 'Type'.
spine_of_type
 :: Type cs h
 -> (forall kc (c::kc) hs. Const cs c -> Types cs hs -> ret) -> ret
spine_of_type (TyConst c) k = k c TypesZ
spine_of_type (f :$ a) k = spine_of_type f $ \c as -> k c (a `TypesS` as)

-- * Type 'UnProxy'
type family UnProxy (x::K.Type) :: k where
	UnProxy (Proxy x) = x

-- * Class 'MonoLift'
class MonoLift a b where
	olift :: a -> b
instance MonoLift
 (Error_Type meta ts)
 (Error_Type meta ts) where
	olift = id
instance
 MonoLift (Constraint_Kind meta ts) (Error_Type meta ts) where
	olift = olift . Error_Type_Constraint_Kind

-- * Class 'Gram_Type'
type ToType p = EToken (Context p) '[Proxy Token_Type]
class
 ( Alt p
 , Alter p
 , Alternative p
 , App p
 , Gram_CF p
 , Gram_Rule p
 , Gram_Term p
 , Gram_Lexer p
 , Gram_Context p
 ) => Gram_Type p where
	typeP :: CF p (ToType p)
	typeP = rule "type" $ type_fun
	type_fun :: CF p (ToType p)
	type_fun = rule "type_fun" $
		context $ \meta ->
		let f a b = inj_etoken meta $ Token_Type "(->)" [a, b] in
		infixrP f type_list (symbol "->") typeP
	type_list :: CF p (ToType p)
	type_list = rule "type_list" $
		context $ \meta ->
		let f = inj_etoken meta . Token_Type "[]" in
		inside f (symbol "[") (option [] (pure <$> typeP)) (symbol "]") type_tuple2
	type_tuple2 :: CF p (ToType p)
	type_tuple2 = rule "type_tuple2" $
		context $ \meta ->
		let f a b = inj_etoken meta $ Token_Type "(,)" [a, b] in
		parens (infixrP f typeP (symbol ",") typeP) <+> type_app
	type_app :: CF p (ToType p)
	type_app = rule "type_app" $
		(\(EToken (TokenZ meta (Token_Type f as)):as') ->
			(EToken (TokenZ meta (Token_Type f (as <> as')))))
		 <$> some type_atom
	type_atom :: CF p (ToType p)
	type_atom = rule "type_atom" $
		parens typeP <+>
		type_name <+>
		type_symbol
	type_name :: CF p (ToType p)
	type_name = rule "type_name" $
		context $ \meta ->
		lexeme $
		(\c cs -> EToken $ TokenZ meta $ Token_Type (Text.pack $ c:cs) [])
		 <$> unicat (Unicat Char.UppercaseLetter)
		 <*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])
	type_symbol :: CF p (ToType p)
	type_symbol = rule "type_symbol" $
		context $ \meta ->
		let f s = inj_etoken meta $ (`Token_Type` []) $
			Text.concat ["(", Text.pack s, ")"] in
		(f <$>) $ parens $ many $ choice (unicat <$>
		 [ Unicat_Symbol
		 , Unicat_Punctuation
		 , Unicat_Mark
		 ]) `but` char ')'

deriving instance Gram_Type p => Gram_Type (CF p)
instance Gram_Type EBNF
instance Gram_Type RuleDef

gram_type :: Gram_Type p => [CF p (ToType p)]
gram_type =
 [ typeP
 , type_fun
 , type_list
 , type_tuple2
 , type_app
 , type_atom
 , type_name
 , type_symbol
 ]