{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Compiling.Term
 ( module Language.Symantic.Compiling.Term
 , module Language.Symantic.Compiling.Term.Grammar
 ) where

import Control.Arrow (left)
import Data.Proxy (Proxy(..))
import qualified Data.Kind as K

import Language.Symantic.Helper.Data.Type.List
import Language.Symantic.Helper.Data.Type.Peano
import Language.Symantic.Parsing
import Language.Symantic.Typing

import Language.Symantic.Compiling.Term.Grammar

-- | The function 'Type' @(->)@,
-- with an infix notation more readable.
(~>) :: Source src
     => Inj_TyConst cs (->)
     => Type src ctx ss cs a
     -> Type src ctx ss cs b
     -> Type src ctx ss cs (a -> b)
(~>) a b = (ty @(->) `tyApp` a) `tyApp` b
infixr 5 ~>

-- * Type 'Inj_Sym'
-- | Convenient type synonym wrapping 'Inj_SymP'
-- applied on the correct 'Index'.
type Inj_Sym ss s = Inj_SymP (Index ss (Proxy s)) ss s

-- | Inject a given /symantic/ @s@ into a list of them,
-- by returning a function which given a 'TeSym' on @s@
-- returns the same 'TeSym' on @ss@.
inj_Sym :: forall s ss ctx h.
 Inj_Sym ss s
 => TeSym ctx '[Proxy s] h
 -> TeSym ctx ss h
inj_Sym = inj_SymP (Proxy @(Index ss (Proxy s)))

-- ** Class 'Inj_SymP'
class Inj_SymP p ss s where
	inj_SymP :: Proxy p -> TeSym ctx '[Proxy s] h -> TeSym ctx ss h
instance Inj_SymP Zero (Proxy s ': ss) (s::k) where
	inj_SymP _ = \(TeSym te) -> TeSym te
instance Inj_SymP p ss s => Inj_SymP (Succ p) (not_s ': ss) s where
	inj_SymP _p = \(te::TeSym ctx '[Proxy s] h) ->
		case inj_SymP (Proxy @p) te :: TeSym ctx ss h of
		 TeSym te' -> TeSym te'

-- * Type 'CtxTy'
-- | GADT for a /typing context/:
-- accumulating at each /lambda abstraction/
-- the 'Type' of the introduced variable.
data CtxTy src ss (cs::[K.Type]) (hs::[K.Type]) where
	CtxTyZ :: CtxTy src ss cs '[]
	CtxTyS :: TeName
	       -> Type src ctx ss cs h
	       -> CtxTy src ss cs hs
	       -> CtxTy src ss cs (h ': hs)
infixr 5 `CtxTyS`

appendCtxTy
 :: CtxTy src ss cs hs0
 -> CtxTy src ss cs hs1
 -> CtxTy src ss cs (hs0 ++ hs1)
appendCtxTy CtxTyZ c          = c
appendCtxTy (CtxTyS n t c) c' = CtxTyS n t $ appendCtxTy c c'

-- * Class 'Compile'
class Compile cs ss where
	compile :: Source src
	        => Inj_Source (EType src '[] ss cs) src
	        => Inj_Source (EKind src) src
	        => Inj_Source (AST_Type src) src
	        => AST_Term src ss
	        -> CtxTy src ss cs ctx
	        -- ^ The bound variables in scope and their types:
	        -- built top-down in the heterogeneous list @ctx@,
	        -- from the closest including /lambda abstraction/ to the farest.
	        -> Either (Error_Term src ss cs)
	                  (KTerm src ctx ss cs)
instance
 ( Show_TyConst cs
 , Inj_TyConst  cs (->)
 , Proj_TyConst cs (->)
 , Proj_TyConst cs (#>)
 , Proj_TyCon   cs
 , Read_TyName  cs
 , CompileR ss cs ss
 ) => Compile cs ss where
	compile :: forall src ctx. Source src
	        => Inj_Source (EType src '[] ss cs) src
	        => Inj_Source (EKind src) src
	        => Inj_Source (AST_Type src) src
	        => AST_Term src ss
	        -> CtxTy src ss cs ctx
	        -> Either (Error_Term src ss cs)
	                  (KTerm src ctx ss cs)
	compile tr ctx = do
		ts <- go `traverse` tr
		(_vs, Just m) <- inj_Error `left` evalTreeKT ts
		Right $ polyTy `bindKT` m
		where
		go :: Token_Term src ss
		   -> Either (Error_Term src ss cs)
		             (KTerm src ctx ss cs)
		go (Token_Term (EToken _src tok)) = Right $ compileR tok
		go (Token_Term_Abst _src name_arg tok_ty_arg tok_body) =
			read_Type tok_ty_arg $ \(ty_arg::Type src ctx ss cs h) ->
			if_EqKind (inj_Kind @K.Type) (kindTy ty_arg) $ \Refl -> do
			KT (Term ty_res (TeSym res)) <- -- FIXME: pattern failure
				compile tok_body (CtxTyS name_arg ty_arg ctx)
			Right $ KT $ Term (ty_arg ~> unTerms ty_res) $
				TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
		go (Token_Term_Var _src nam) = lookupTeVar nam ctx
			where
			lookupTeVar :: forall ctxTy.
			    TeName
			 -> CtxTy src ss cs ctxTy
			 -> Either (Error_Term src ss cs)
			           (KTerm src ctxTy ss cs)
			lookupTeVar name ctxTy =
				case ctxTy of
				 CtxTyZ -> Left $ Error_Term_unbound name
				 CtxTyS n typ _ | n == name ->
					Right $ KT $ Term (unTerms typ) $
						TeSym $ \(te `CtxTeS` _) -> te
				 CtxTyS _n _typ ctxTy' -> do
					KT t <- lookupTeVar name ctxTy'
					case t of
					 Term typ (TeSym te) ->
						Right $ KT $ Term (unTerms typ) $ -- TODO: optimize?
							TeSym $ \(_ `CtxTeS` c) -> te c
					 _ -> error "[BUG] lookupTeVar: impossible case"
		go (Token_Term_Let _src name tok_bound tok_body) = do
			KT (Term ty_bound (TeSym bound)) <- -- FIXME: pattern failure
				compile tok_bound ctx
			KT (Term ty_res   (TeSym res))   <- -- FIXME: pattern failure
				compile tok_body (CtxTyS name ty_bound ctx)
			Right $ KT $ Term (unTerms ty_res) $
				TeSym $ \c -> let_ (bound c) $ \arg -> res (arg `CtxTeS` c)
		go (Token_Term_App _ctx) =
			Right $
				tyQuant "a" $ \a ->
				tyQuant "b" $ \b ->
				KT $ Term ((a ~> b) ~> a ~> b) $
				TeSym $ \_c -> apply

-- ** Class 'CompileR'
-- | Intermediate type class to construct an instance of 'Compile'
-- from many instances of 'CompileS', one for each item of @ss@.
class CompileR (ss::[K.Type]) (cs::[K.Type]) (ssR::[K.Type]) where
	compileR :: Source src
	         => Inj_Source (EType src '[] ss cs) src
	         => Inj_Source (EKind src) src
	         => Inj_Source (AST_Type src) src
	         => TokenR ss ssR s
	         -> KTerm src ctx ss cs
-- | Recurse into the given 'TokenR'
-- to call the 'compileS' instance associated
-- to the 'TokenT' it contains.
instance
 ( CompileS ss cs s
 , CompileR ss cs (r ': ssR)
 ) => CompileR ss cs (Proxy s ': r ': ssR) where
	compileR = \case
	 TokenZ to -> compileS to
	 TokenS to -> compileR to
-- | End the recursion.
instance
 CompileS ss cs s =>
 CompileR ss cs (Proxy s ': '[]) where
	compileR (TokenZ to) = compileS to
	compileR TokenS{}    = error "[BUG] compileR: TokenS is impossible here"

-- ** Class 'CompileS'
-- | Handle the work of 'Compile' for a given /symantic/ @s@.
class CompileS (ss::[K.Type]) (cs::[K.Type]) (s::ks) where
	compileS :: Source src
	         => Inj_Source (EType src '[] ss cs) src
	         => Inj_Source (EKind src) src
	         => Inj_Source (AST_Type src) src
	         => TokenT ss (Proxy s)
	         -> KTerm src ctx ss cs

instance Inj_Error (Error_Type src) (Error_Term src ss cs) where
	inj_Error = Error_Term_Typing
instance Inj_Error (Con_Kind src) (Error_Term src ss cs) where
	inj_Error = Error_Term_Typing . Error_Type_Con_Kind
instance Inj_Error (Error_TeApp src ss cs) (Error_Term src ss cs) where
	inj_Error = Error_Term_TeApp

-- * Type 'Error_Term'
data Error_Term src ss cs
 =   Error_Term_unbound TeName
 |   Error_Term_Typing (Error_Type src)
 |   Error_Term_TeApp (Error_TeApp src ss cs)
 |   Error_Term_Con_Type (Con_Type src '[] ss cs)
 {-    Error_Term_Con_Kind (Con_Kind src) -}
deriving instance
 ( Eq src
 , Eq_Token ss
 , Inj_Source (EType src '[] ss cs) src
 ) => Eq (Error_Term src ss cs)
deriving instance
 ( Show src
 , Show_Token ss
 , Show_TyConst cs
 , Fixity_TyConst cs
 ) => Show (Error_Term src ss cs)


-- * Type 'TyConsts'
type TyConsts ss = Nub (TyConstsR ss)

-- * Type family 'TyConstsR'
type family TyConstsR (ss::[K.Type]) where
	TyConstsR '[]       = '[]
	TyConstsR (s ': ss) = TyConstsS s ++ TyConstsR ss

-- * Type family 'TyConstsS'
type family TyConstsS (s:: K.Type) :: [K.Type]

-- * Type family 'TyConsts_imported_by'
-- | Return the /type constant/s that a given /type constant/
-- wants to be part of the final list of /type constants/.
type family TyConsts_imported_by (c:: K.Type) :: [K.Type]





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

instance Source (Src txt ss cs) where
	sourceLess = Src_Less
instance Inj_Source txt (Src txt ss cs) where
	inj_Source = Src_Text
instance Inj_Source (EToken (Src txt ss cs) ss) (Src txt ss cs) where
	inj_Source = Src_Token
instance Inj_Source (AST_Term (Src txt ss cs) ss) (Src txt ss cs) where
	inj_Source = Src_AST_Term
instance Inj_Source (AST_Type (Src txt ss cs)) (Src txt ss cs) where
	inj_Source = Src_AST_Type
instance Inj_Source (EKind (Src txt ss cs)) (Src txt ss cs) where
	inj_Source = Src_Kind
instance Inj_Source (EType (Src txt ss cs) '[] ss cs) (Src txt ss cs) where
	inj_Source = Src_Type