{-# LANGUAGE GADTs #-}
module Language.Symantic.Compiling.Read where

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

import Language.Symantic.Grammar
import Language.Symantic.Typing

import Language.Symantic.Compiling.Grammar
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Beta

-- | Read a 'TermVT' from and 'AST_Term'.
readTe ::
 forall src ss ts.
 Source src =>
 Inj_Source (TypeVT src) src =>
 Inj_Source (KindK src) src =>
 Inj_Source (AST_Type src) src =>
 Constable (->) =>
 Name2Type src ->
 AST_Term src ss ->
 CtxTy src ts ->
 Either (Error_Term src) (TermVT src ss ts)
readTe cs ast ctxTe = do
	ts <- go ctxTe `traverse` ast
	inj_Error `left` betasTe ts
	where
	go ::
	 forall ts'.
	 CtxTy src ts' ->
	 Token_Term src ss ->
	 Either (Error_Term src) (TermVT src ss ts')
	go _ts (Token_Term (TermVT_CF te)) = Right $ TermVT te
	go ts  (Token_Term_Var _src name)  = teVar name ts
	go _ts (Token_Term_App _src)       = Right $ TermVT teApp
	go ts  (Token_Term_Abst _src name_arg ast_ty_arg ast_body) = do
		TypeVT ty_arg <- inj_Error `left` readTy cs ast_ty_arg
		when_EqKind (inj_Kind @K.Type) (kindOf ty_arg) $ \Refl ->
			case lenVars ty_arg of
			 LenS{} -> Left $ Error_Term_polymorphic $ TypeVT ty_arg
			 LenZ | (TypeK qa, TypeK ta) <- unQualTy ty_arg -> do
				TermVT (Term qr tr (TeSym res)) <- readTe cs ast_body (CtxTyS name_arg ta ts)
				let (qa', qr') = appendVars qa qr
				let (ta', tr') = appendVars ta tr
				Right $ TermVT $ Term @_ @_ @_ @_ @(_ #> _) (qa' # qr') (ta' ~> tr') $
					TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
	go ts (Token_Term_Let _src name ast_arg ast_body) = do
		TermVT (Term qa ta (TeSym arg)) <- readTe cs ast_arg ts
		case lenVars ta of
		 LenS{} -> Left $ Error_Term_polymorphic $ TypeVT (qa #> ta)
		 LenZ -> do
			TermVT (Term qr tr (TeSym res)) <- readTe cs ast_body $ CtxTyS name ta ts
			let (qa', qr') = appendVars qa qr
			let tr' = allocVarsL (lenVars ta) tr
			Right $ TermVT $ Term @_ @_ @_ @_ @(_ #> _) (qa' # qr') tr' $
				TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)

teVar ::
 forall ss src ts.
 Source src =>
 NameTe -> CtxTy src ts -> Either (Error_Term src) (TermVT src ss ts)
teVar name CtxTyZ = Left $ Error_Term_unbound name
teVar name (CtxTyS n ty _) | n == name =
	Right $ TermVT $ Term @_ @_ @_ @_ @(_ #> _) noConstraint ty $
		TeSym $ \(te `CtxTeS` _) -> te
teVar name (CtxTyS _n _typ ts') = do
	TermVT (Term q t (TeSym te)) <- teVar @ss name ts'
	Right $ TermVT $ Term @_ @_ @_ @_ @(_ #> _) q t $
		TeSym $ \(_ `CtxTeS` ts) -> te ts

teApp ::
 Source src => Constable (->) =>
 Term src ss ts '[Proxy (a::K.Type), Proxy (b::K.Type)] ((a -> b) -> a -> b)
teApp =
	Term noConstraint ((a ~> b) ~> a ~> b) $
	TeSym $ const apply
	where
	a :: Source src => Type src '[Proxy a, Proxy b] (a::K.Type)
	a = tyVar "a" $ varZ
	b :: Source src => Type src '[Proxy a, Proxy b] (b::K.Type)
	b = tyVar "b" $ VarS varZ

-- | Reduce number of 'Token_Term_App' in given 'AST_Term' by converting them into 'BinTree2'.
--
-- NOTE: 'Token_Term_App' exists only to handle unifix operators applied to arguments.
reduceTeApp :: AST_Term src ss -> AST_Term src ss
reduceTeApp (BinTree2 x y) =
	case reduceTeApp x of
	 BinTree0 Token_Term_App{} `BinTree2` x' -> reduceTeApp x' `BinTree2` reduceTeApp y
	 _ -> reduceTeApp x `BinTree2` reduceTeApp y
reduceTeApp (BinTree0 (Token_Term_Abst src n ty te)) = BinTree0 $ Token_Term_Abst src n ty (reduceTeApp te)
reduceTeApp (BinTree0 (Token_Term_Let  src n bo te)) = BinTree0 $ Token_Term_Let  src n (reduceTeApp bo) (reduceTeApp te)
reduceTeApp x@BinTree0{} = x

-- * Type 'CtxTy'
-- | /Typing context/
-- accumulating at each /lambda abstraction/
-- the 'Type' of the introduced variable.
-- It is built top-down from the closest
-- including /lambda abstraction/ to the farest.
data CtxTy src (ts::[K.Type]) where
	CtxTyZ :: CtxTy src '[]
	CtxTyS :: NameTe
	       -> Type  src '[] t
	       -> CtxTy src ts
	       -> CtxTy src (t ': ts)
infixr 5 `CtxTyS`

appendCtxTy
 :: CtxTy src ts0
 -> CtxTy src ts1
 -> CtxTy src (ts0 ++ ts1)
appendCtxTy CtxTyZ c          = c
appendCtxTy (CtxTyS n t c) c' = CtxTyS n t $ appendCtxTy c c'

-- * Type 'Error_Term'
data Error_Term src
 =   Error_Term_unbound NameTe
 |   Error_Term_polymorphic (TypeVT src)
 |   Error_Term_qualified (TypeVT src)
 |   Error_Term_Type (Error_Type src)
 |   Error_Term_Beta (Error_Beta src)
 {-   Error_Term_Con_Type (Con_Type src ss) -}
 {-   Error_Term_Con_Kind (Con_Kind src) -}
 deriving (Eq, Show)
instance Inj_Error (Error_Type src) (Error_Term src) where
	inj_Error = Error_Term_Type
instance Inj_Error (Error_Beta src) (Error_Term src) where
	inj_Error = Error_Term_Beta
instance Inj_Error (Con_Kind src) (Error_Term src) where
	inj_Error = Error_Term_Type . inj_Error

-- * Type 'SrcTe'
data SrcTe txt ss
 =   SrcTe_Less
 |   SrcTe_Text     txt
 |   SrcTe_AST_Term (AST_Term (SrcTe txt ss) ss)
 |   SrcTe_AST_Type (AST_Type (SrcTe txt ss))
 |   SrcTe_Kind     (KindK    (SrcTe txt ss))
 |   SrcTe_Type     (TypeVT   (SrcTe txt ss))
 |   SrcTe_Term
 deriving (Eq, Show)

type instance Text_of_Source (SrcTe txt ss) = txt

instance Source (SrcTe txt ss) where
	noSource = SrcTe_Less
instance Inj_Source txt (SrcTe txt ss) where
	inj_Source = SrcTe_Text
instance Inj_Source (AST_Term (SrcTe txt ss) ss) (SrcTe txt ss) where
	inj_Source = SrcTe_AST_Term
instance Inj_Source (AST_Type (SrcTe txt ss)) (SrcTe txt ss) where
	inj_Source = SrcTe_AST_Type
instance Inj_Source (KindK (SrcTe txt ss)) (SrcTe txt ss) where
	inj_Source = SrcTe_Kind
instance Inj_Source (TypeVT (SrcTe txt ss)) (SrcTe txt ss) where
	inj_Source = SrcTe_Type