{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE PolyKinds #-}
module Language.Symantic.Typing.Read where

import Language.Symantic.Grammar
import Language.Symantic.Typing.Kind
import Language.Symantic.Typing.Type
import Language.Symantic.Typing.Show ()
import Language.Symantic.Typing.Grammar
import Language.Symantic.Typing.Variable

-- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
readType ::
 SourceInj (KindK src) src =>
 SourceInj (TypeVT src) src =>
 SourceInj (AST_Type src) src =>
 AST_Type src ->
 Either (Error_Type src) (TypeVT src)
readType ast | EVars vs <- readVars (EVars VarsZ) ast = do
	TypeT ty <- readTyVars vs ast
	Right $ TypeVT ty

-- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
readTyVars ::
 forall vs src.
 SourceInj (KindK src) src =>
 SourceInj (TypeVT src) src =>
 SourceInj (AST_Type src) src =>
 Vars src vs ->
 AST_Type src ->
 Either (Error_Type src) (TypeT src vs)
readTyVars vs (BinTree0 (Token_Type_Const (TypeTLen t))) =
	Right $ t (lenVars vs)
	-- readTyName is ms (sourceInj ast) (lenVars vs) name
readTyVars vs (BinTree0 (Token_Type_Var (Sourced src name))) =
	case lookupVars name vs of
	 Just (EVar v) -> Right $ TypeT $ TyVar src name v
	 Nothing -> error "[BUG] readTyVars: lookupVars failed"
readTyVars vs ast@(ast_x `BinTree2` ast_y) = do
	TypeT ty_x <- readTyVars vs ast_x
	TypeT ty_y <- readTyVars vs ast_y
	when_KiFun (kindOf ty_x) $ \Refl ki_x_a _ki_x_b ->
		when_EqKind ki_x_a (kindOf ty_y) $ \Refl ->
			Right $ TypeT $ TyApp (sourceInj ast) ty_x ty_y

-- | Return the given 'EVars' augmented by the ones used in given 'AST_Type'.
readVars :: Source src => EVars src -> AST_Type src -> EVars src
readVars evs@(EVars vs) (BinTree0 (Token_Type_Var (Sourced _src name))) =
	case lookupVars name vs of
	 Just{} -> evs
	 Nothing -> do
		let kv = KiType noSource
		let vs' = VarsS name kv vs
		EVars vs'
readVars evs BinTree0{} = evs
readVars evs (BinTree2 x y) =
	readVars (readVars evs x) y