{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Typing.Type where

import Data.Monoid ((<>))
import Data.Proxy
import Data.Maybe (fromMaybe, isJust)
import Data.Type.Equality
import qualified Data.Kind as K

import Language.Symantic.Typing.Kind
import Language.Symantic.Typing.Constant
import Language.Symantic.Typing.Syntax

-- * 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)
	{-
	TyVar
	 :: SKind k
	 -> Type cs (v::k)
	-}
infixl 9 :$

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)

-- * 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 ty) = show ty

-- * 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 ty) = show_type ty

-- * Class 'Type_from'
-- | Try to build a 'Type' from raw data.
class Type_from ast cs where
	type_from
	 :: ast
	 -> (forall k h. Type cs (h::k) -> Either (Error_Type cs ast) ret)
	 -> Either (Error_Type cs ast) ret

-- ** Type 'Error_Type'
data Error_Type cs ast
 =   Error_Type_Constant_unknown    (At ast (Lexem ast))
 |   Error_Type_Kind_mismatch       (At ast EKind) (At ast EKind)
 |   Error_Type_Kind_not_applicable (At ast EKind)
deriving instance (Eq ast, Eq (Lexem ast)) => Eq (Error_Type cs ast)
deriving instance (Show ast, Show (Lexem ast), Show_Const cs) => Show (Error_Type cs ast)

instance
 ( Const_from (Lexem ast) cs
 , AST ast
 ) => Type_from ast cs where
	type_from ast kk =
		fromMaybe (Left $ Error_Type_Constant_unknown $ At (Just ast) $ ast_lexem ast) $
		const_from (ast_lexem ast) $ \c -> Just $
		go (ast_nodes ast) (TyConst c) kk
		where
		go :: [ast]
		 -> Type cs h
		 -> (forall k' h'. Type cs (h'::k') -> Either (Error_Type cs ast) ret)
		 -> Either (Error_Type cs ast) ret
		go [] ty k = k ty
		go (ast_x:ast_xs) ty_f k =
			type_from ast_x $ \ty_x ->
			case kind_of ty_f of
			 ki_f_a `SKiArrow` _ki_f_b ->
				let ki_x = kind_of ty_x in
				case eq_skind ki_f_a ki_x of
				 Just Refl -> go ast_xs (ty_f :$ ty_x) k
				 Nothing -> Left $ Error_Type_Kind_mismatch
					 (At (Just ast)   $ EKind ki_f_a)
					 (At (Just ast_x) $ EKind ki_x)
			 ki -> Left $ Error_Type_Kind_not_applicable $ At (Just ast) $ EKind ki

-- * Type 'Args'
data Args (cs::[K.Type]) (args::[K.Type]) where
	ArgZ :: Args cs '[]
	ArgS :: Type cs arg
	     -> Args cs args
	     -> Args cs (Proxy arg ': args)
infixr 5 `ArgS`

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

-- * Usual 'Type's

-- | The '()' 'Type'
tyUnit :: Inj_Const cs () => Type cs ()
tyUnit = TyConst inj_const