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

import Data.Maybe (fromMaybe)
import Data.Typeable
import qualified Data.Map.Strict as Map

import Language.Symantic.Grammar
import Language.Symantic.Typing.List
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
import Language.Symantic.Typing.Module

-- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
readType ::
 SourceInj (KindK src) src =>
 SourceInj (TypeVT src) src =>
 SourceInj (AST_Type src) src =>
 Imports NameTy ->
 ModulesTy src ->
 AST_Type src ->
 Either (Error_Type src) (TypeVT src)
readType is ms ast | EVars vs <- readVars (EVars VarsZ) ast = do
	TypeT ty <- readTyVars is ms 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 =>
 Imports NameTy ->
 ModulesTy src ->
 Vars src vs ->
 AST_Type src ->
 Either (Error_Type src) (TypeT src vs)
readTyVars is ms vs ast@(BinTree0 (Token_Type_Const (At _src name))) =
	readTyName is ms (sourceInj ast) (lenVars vs) name
readTyVars _is _ms vs ast@(BinTree0 (Token_Type_Var (At _src name))) =
	case lookupVars name vs of
	 Just (EVar v) -> Right $ TypeT $ TyVar (sourceInj ast) name v
	 Nothing -> error "[BUG] readTyVars: lookupVars failed"
readTyVars is ms vs ast@(ast_x `BinTree2` ast_y) = do
	TypeT ty_x <- readTyVars is ms vs ast_x
	TypeT ty_y <- readTyVars is ms 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

-- | Lookup a 'TyConst' or 'Type' synonym
-- associated with given 'NameTy' in given 'ModulesTy',
-- building it for a @vs@ of given 'Len'.
readTyName ::
 Source src =>
 Imports NameTy ->
 ModulesTy src -> src -> Len vs -> Mod NameTy ->
 Either (Error_Type src) (TypeT src vs)
readTyName is ms src len name@(m `Mod` n) =
	let m' = fromMaybe m $ lookupImports FixyInfix name is in
	case Map.lookup (m' `Mod` n) ms of
	 Just (TypeTLen t) -> Right $ t len
	 Nothing -> Left $ Error_Type_Constant_unknown $ At src name

-- | 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 (At _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

-- * Type 'Error_Type'
data Error_Type src
 =   Error_Type_Constant_unknown (At src (Mod NameTy))
 |   Error_Type_Con_Kind         (Con_Kind src)
 deriving (Eq, Show)
instance ErrorInj (Error_Type src) (Error_Type src) where
	errorInj = id
instance ErrorInj (Con_Kind src) (Error_Type src) where
	errorInj = Error_Type_Con_Kind