{-# 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(..))
import qualified Data.Char as Char
import Data.Monoid ((<>))
import Data.Proxy
import Data.Maybe (fromMaybe, isJust)
import Data.String (IsString(..))
import Data.Text (Text)
import qualified Data.List as List
import qualified Data.Text as Text
import Data.Type.Equality
import qualified Data.Kind as K
import GHC.Exts (Constraint)
import Data.Void (Void)
import Unsafe.Coerce (unsafeCoerce)
import GHC.Prim (Any)

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

-- * Type 'Type'

-- | /Type of terms/.
--
-- * @vs@: /type variables/, fixed at compile time.
-- * @cs@: /type constants/, fixed at compile time.
-- * @h@: indexed Haskell type.
-- * @k@: indexed Haskell kind of @h@.
--
-- * 'TyConst': /type constant/, selected amongst @cs@.
-- * 'TyVar': /type variable/.
--   Note that only the kind @k@ is coerced,
--   @h@ being set to 'Any' to loose the type indexing.
--   Note also that there is no De Bruijn encoding done to link 'TyPi's and 'TyVar's.
-- * 'TyPi': /type abstraction/.
--   Note that only the kind @k@ is coerced,
--   @h@ being set to 'Any' to loose the type indexing.
-- * @(:$)@: /type application/.
-- * @(:=>)@: /type constraint/.
--   Note that there is no proof of the 'Constraint' attached.
--
-- See also: https://ghc.haskell.org/trac/ghc/wiki/Typeable
-- Which currently concludes:
-- "Why kind equalities, then? Given the fact that Richard's branch
-- doesn't solve this problem, what is it good for?
-- It still works wonders in the mono-kinded case,
-- such as for decomposing ->.
-- It's just that poly-kinded constructors are still a pain."

data Type (cs::[K.Type]) (h::k) where
	TyConst :: TyConst cs c -> Type cs c
	(:$)    :: Type cs f -> Type cs x -> Type cs (f x)
	TyVar   :: SKind k -> Var -> Type cs (Any::k)
	TyPi    :: SKind kv -> (forall (v::kv). Type cs v -> Type cs (Any::k)) -> Type cs (Any::k)
	(:=>)   :: {-c =>-} Type cs (c::Constraint) -> Type cs h -> Type cs h
infixl 9 :$
infixl 1 :=>

-- | /beta-reduction/: when possible, substitute
-- the abstraction of a 'TyPi' with a given 'Type'.
tyApp :: Type cs a -> Type cs b -> Maybe (Type cs a)
tyApp (TyPi kv f) v
 | Just Refl <- eq_SKind kv (kind_of v)
 = Just (f v)
tyApp _f _v = Nothing
infixl 2 `tyApp`

-- * Type 'Var'
type Var = Int

-- | Drop the type index.
-- 
-- Useful when the type index cannot represent the wanted type,
-- like a polymorphic type.
tyVoid :: Type cs (a::k) -> Type cs (Any::Void)
tyVoid = unsafeCoerce
kindVoid :: SKind k -> SKind Void
kindVoid = unsafeCoerce
reflVoid :: (x::Void) :~: (y::Void)
reflVoid = unsafeCoerce Refl

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

kind_of :: Type cs (h::k) -> SKind k
kind_of t =
	case t of
	 TyConst c -> kind_of_TyConst c
	 f :$ _x ->
		case kind_of f of
		 _kx `SKiArrow` kf -> kf
	 _c :=> x -> kind_of x
	 TyVar k _v -> k
	 TyPi k f -> kind_of $ f (TyVar k 0)

-- | Return the smallest 'Var' not used in given 'Type'.
freeTyVar :: Type cs (h::k) -> Var
freeTyVar = (+ 1) . maxTyVar (-1)
	where
	maxTyVar :: Var -> Type cs h -> Var
	maxTyVar m TyConst{}     = m
	maxTyVar m (f :$ a)      = maxTyVar m f `max` maxTyVar m a
	maxTyVar m (TyVar _kv v) = max m v
	maxTyVar m (TyPi kv f)   = maxTyVar m $ f $ TyVar kv (-1)
	maxTyVar m (_c :=> x)    = maxTyVar m x

-- | Return the 'Var's (without doubles) used in given 'Type'.
freeTyVars :: Type cs (h::k) -> [Var]
freeTyVars = List.nub . go
	where
	go :: Type cs h -> [Var]
	go TyConst{}     = []
	go (f :$ a)      = go f `List.union` go a
	go (TyVar _kv v) | v >= 0    = [v]
	                 | otherwise = []
	go (TyPi kv f)   = go $ f $ TyVar kv (-1)
	go (_c :=> x)    = go x

eq_Type :: Type cs (x::k)
        -> Type cs (y::k)
        -> Maybe (x:~:y)
eq_Type = eq (-1)
	where
	eq :: Var
	   -> Type cs (x::k)
	   -> Type cs (y::k)
	   -> Maybe (x:~:y)
	eq _v (TyConst x) (TyConst y)
	 | Just Refl <- testEquality x y
	 = Just Refl
	eq v (xf :$ xx) (yf :$ yx)
	 | Just Refl <- eq_SKind (kind_of xf) (kind_of yf)
	 , Just Refl <- eq v xf yf
	 , Just Refl <- eq v xx yx
	 = Just Refl
	eq v (TyPi xk x::Type cs xv) (TyPi xy y::Type cs yv)
	 | Just Refl <- eq_SKind xk xy
	 , Just Refl <- eq (v - 1) (x $ TyVar xk v) (y $ TyVar xy v)
	 = Just Refl
	eq _v (TyVar xk x) (TyVar yk y)
	 | Just Refl <- eq_SKind xk yk
	 , True <- x == y
	 = Just Refl
	eq v (xc :=> x) (yc :=> y)
	 | Just Refl <- eq v xc yc
	 , Just Refl <- eq v x y
	 = Just Refl
	eq _ _ _ = Nothing

eq_Kind_Type :: Type cs (x::kx)
             -> Type cs (y::ky)
             -> Maybe (kx:~:ky)
eq_Kind_Type = eq
	where
	eq :: Type cs (x::kx)
	   -> Type cs (y::ky)
	   -> Maybe (kx:~:ky)
	eq (TyConst x) (TyConst y)
	 | Just Refl <- eq_Kind_TyConst x y
	 = Just Refl
	eq (xf :$ xx) (yf :$ yx)
	 | Just Refl <- eq xf yf
	 , Just Refl <- eq xx yx
	 = Just Refl
	eq (TyPi xk x::Type cs xv) (TyPi xy y::Type cs yv)
	 | Just Refl <- eq_SKind xk xy
	 , Just Refl <- eq (x $ TyVar xk 0) (y $ TyVar xy 0)
	 = Just Refl
	eq (TyVar kx _x) (TyVar ky _y)
	 | Just Refl <- eq_SKind kx ky
	 = Just Refl
	eq (_xc :=> x) (_yc :=> y)
	 | Just Refl <- eq x y
	 = Just Refl
	eq _x _y = Nothing

show_Type :: Show_TyConst cs => Int -> Type cs h -> ShowS
show_Type pr t = go (freeTyVar t) pr t
	where
	go :: Show_TyConst cs => Var -> Int -> Type cs h -> ShowS
	go _v p (TyConst c)   = showsPrec p c
	go _v p (TyVar _kv v) = showString "a" . showsPrec p v
	go v p (f :$ a) =
		showParen (p > 10) $
		go v 11 f .
		showString " " .
		go v 11 a
	go v p (c :=> a) =
		showParen (p > 10) $
		go v 11 c .
		showString " => " .
		go v 11 a
	go v p (TyPi kv f) =
		let var = TyVar kv v in
		showParen (p > 10) $
		showString "forall " .
		go v p var .
		showString ". " .
		go v 11 (f var)

instance TestEquality (Type cs) where
	testEquality = eq_Type
instance Eq (Type cs h) where
	_x == _y = True
instance Show_TyConst cs => Show (Type cs h) where
	showsPrec = show_Type

-- * 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_TyConst 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_TyConst cs => Show (KType cs ki) where
	showsPrec p (KType t) = show_Type p t

-- * Type 'TyName'
newtype TyName = TyName Text
 deriving (Eq, Ord, Show)
instance IsString TyName where
	fromString = TyName . fromString

-- * Class 'Read_TyName'
type Read_TyName raw cs = Read_TyNameR raw cs cs

read_TyName
 :: forall raw cs ret.
 Read_TyNameR raw cs cs
 => raw -> (forall k c. Type cs (c::k) -> Maybe ret)
 -> Maybe ret
read_TyName = read_TyNameR (Proxy @cs)

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

instance Read_TyNameR raw cs '[] where
	read_TyNameR _cs _c _k = Nothing

-- TODO: move each of these to a dedicated module.
instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs Fractional
 ) => Read_TyNameR TyName cs (Proxy Fractional ': rs) where
	read_TyNameR _cs (TyName "Fractional") k = k (ty @Fractional)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs []
 , Inj_TyConst cs Char
 ) => Read_TyNameR TyName cs (Proxy String ': rs) where
	read_TyNameR _cs (TyName "String") k = k (ty @[] :$ ty @Char)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k

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

data instance TokenT meta ts (Proxy Token_Type)
 = Token_Type TyName [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_TyNameR TyName cs rs
 , Inj_TyConst cs Token_Type
 ) => Read_TyNameR TyName cs (Proxy Token_Type ': rs) where
	read_TyNameR _rs (TyName "Type") k = k (ty @Token_Type)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy Token_Type ': cs) where
	show_TyConst TyConstZ{} = "Type"
	show_TyConst (TyConstS c) = show_TyConst c

-- * Type 'Error_Type'
data Error_Type meta ts
 =   Error_Type_Token_invalid    (EToken meta ts)
 |   Error_Type_Constant_unknown (At meta ts TyName)
 |   Error_Type_Con_Kind  (Con_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 'MonoLift'
class MonoLift a b where
	olift :: a -> b
instance MonoLift
 (Error_Type meta ts)
 (Error_Type meta ts) where
	olift = id
instance
 MonoLift (Con_Kind meta ts) (Error_Type meta ts) where
	olift = olift . Error_Type_Con_Kind

-- * Type 'Con_Kind'
data Con_Kind meta ts
 =   Con_Kind_Eq    (At meta ts EKind) (At meta ts EKind)
 |   Con_Kind_Arrow (At meta ts EKind)
deriving instance (Eq_TokenR meta ts ts) => Eq (Con_Kind meta ts)
deriving instance (Show_TokenR meta ts ts) => Show (Con_Kind meta ts)

check_Kind
 :: MonoLift (Con_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 $
		Con_Kind_Eq (EKind <$> x) (EKind <$> y)

check_Kind_Arrow
 :: MonoLift (Con_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 $
		Con_Kind_Arrow (EKind <$> x)

-- * Class 'Compile_Type'

-- | Try to build a 'Type' from an 'EToken'.
class Compile_Type ts cs where
	compile_Type
	 :: ( MonoLift (Error_Type meta ts) err
	    , MonoLift (Con_Kind meta ts) err )
	 => EToken meta ts
	 -> (forall k h. Type cs (h::k) -> Either err ret)
	 -> Either err ret

instance
 ( Read_TyName TyName cs
 , Proj_Token ts Token_Type
 ) => Compile_Type ts cs where
	compile_Type
	 :: forall meta err ret.
	 ( MonoLift (Error_Type meta ts) err
	 , MonoLift (Con_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_TyName 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

compile_EType
 :: Read_TyName TyName cs
 => EToken meta '[Proxy Token_Type]
 -> Either (Error_Type meta '[Proxy Token_Type]) (EType cs)
compile_EType tok = compile_Type tok (Right . EType)

-- * 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 ka (a::ka) hs.
     Either Var (TyConst cs a) -> Types cs hs -> ret)
 -> ret
spine_of_Type = go
	where
	go :: Type cs h
	   -> (forall ka (a::ka) hs.
	      Either Var (TyConst cs a) -> Types cs hs -> ret)
	   -> ret
	go (TyConst c)   k = k (Right c) TypesZ
	go (f :$ a)      k = go f $ \c as -> k c (a `TypesS` as)
	go (TyVar _kv v) k = k (Left v) TypesZ
	go (TyPi _kv _f) _k = undefined -- FIXME: see what to do in this case.
	go (_c :=> x)    k = go x k

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

-- * Class 'Gram_Type'
type TokType meta = EToken meta '[Proxy Token_Type]
class
 ( Alt g
 , Alter g
 , App g
 , Try g
 , Gram_CF g
 , Gram_Rule g
 , Gram_Terminal g
 , Gram_Lexer g
 , Gram_Op g
 , Gram_Meta meta g
 ) => Gram_Type meta g where
	g_type :: CF g (TokType meta)
	g_type = rule "type" $ g_type_fun
	g_type_fun :: CF g (TokType meta)
	g_type_fun = rule "type_fun" $
		infixrG g_type_list (metaG $ op <$ symbol "->")
		where op meta a b = inj_EToken meta $ Token_Type "(->)" [a, b]
	g_type_list :: CF g (TokType meta)
	g_type_list = rule "type_list" $
		metaG $ inside f
		 (symbol "[") (option [] (pure <$> g_type)) (symbol "]")
		 (const <$> g_type_tuple2)
		where f a meta = inj_EToken meta $ Token_Type "[]" a
	g_type_tuple2 :: CF g (TokType meta)
	g_type_tuple2 = rule "type_tuple2" $
		try (parens (infixrG g_type (metaG $ op <$ symbol ","))) <+> g_type_app
		where op meta a b = inj_EToken meta $ Token_Type "(,)" [a, b]
	g_type_app :: CF g (TokType meta)
	g_type_app = rule "type_app" $
		f <$> some g_type_atom
		where
		f :: [TokType meta] -> TokType meta
		f (EToken (TokenZ meta (Token_Type a as)):as') =
			EToken $ TokenZ meta $ Token_Type a $ as <> as'
		f _ = error "Oops, the impossible happened"
	g_type_atom :: CF g (TokType meta)
	g_type_atom = rule "type_atom" $
		try (parens g_type) <+>
		g_type_name <+>
		g_type_symbol
	g_type_name :: CF g (TokType meta)
	g_type_name = rule "type_name" $
		metaG $ lexeme $
		(\c cs meta -> EToken $ TokenZ meta $ Token_Type (TyName $ Text.pack $ c:cs) [])
		 <$> unicat (Unicat Char.UppercaseLetter)
		 <*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])
	g_type_symbol :: CF g (TokType meta)
	g_type_symbol = rule "type_symbol" $
		metaG $ (f <$>) $
		parens $ many $ cf_of_Terminal $ choice g_ok `but` choice g_ko
		where
		f s meta = inj_EToken meta $ (`Token_Type` []) $
			TyName $ Text.concat ["(", Text.pack s, ")"]
		g_ok = unicat <$>
		 [ Unicat_Symbol
		 , Unicat_Punctuation
		 , Unicat_Mark
		 ]
		g_ko = char <$> ['(', ')', '`']

deriving instance Gram_Type meta g => Gram_Type meta (CF g)
instance Gram_Type meta EBNF
instance Gram_Type meta RuleDef

-- | List of the rules of 'Gram_Type'.
gram_type :: Gram_Type meta g => [CF g (TokType meta)]
gram_type =
 [ g_type
 , g_type_fun
 , g_type_list
 , g_type_tuple2
 , g_type_app
 , g_type_atom
 , g_type_name
 , g_type_symbol
 ]