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

import Data.Map.Strict (Map)
import Data.Typeable
import qualified Data.Map.Strict as Map
import qualified Data.Text as Text

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

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

-- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
readTyVars ::
 forall vs src.
 Inj_Source (KindK src) src =>
 Inj_Source (TypeVT src) src =>
 Inj_Source (AST_Type src) src =>
 Name2Type src ->
 Vars src vs ->
 AST_Type src ->
 Either (Error_Type src) (TypeT src vs)
readTyVars cs vs ast@(BinTree0 (Token_Type_Const (At _src name))) =
	readTyName cs (inj_Source ast) (lenVars vs) name
readTyVars _cs vs ast@(BinTree0 (Token_Type_Var (At _src name))) =
	case lookupVars name vs of
	 Just (EVar v) -> Right $ TypeT $ TyVar (inj_Source ast) name v
	 Nothing -> error "[BUG] readTyVars: lookupVars failed"
readTyVars cs vs ast@(ast_x `BinTree2` ast_y) = do
	TypeT ty_x <- readTyVars cs vs ast_x
	TypeT ty_y <- readTyVars cs 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 (inj_Source ast) ty_x ty_y

-- | Lookup a 'TyConst' or 'Type' synonym
-- associated with given 'NameTy' in given 'Name2Type',
-- building it for a @vs@ of given 'Len'.
readTyName ::
 Source src =>
 Name2Type src -> src -> Len vs -> NameTy ->
 Either (Error_Type src) (TypeT src vs)
readTyName cs src len name =
	case Map.lookup name cs 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 'Name2Type'
type Name2Type src = Map NameTy (TypeTLen src)

-- ** Type 'TypeTLen'
-- | Like 'TypeT', but needing a @(@'Len'@ vs)@ to be built.
--
-- Useful to build a 'Name2Type' which can be used
-- whatever will be the @(@'Len'@ vs)@ given to 'readTyVars'.
newtype TypeTLen src = TypeTLen (forall vs. Len vs -> TypeT src vs)
instance Source src => Eq (TypeTLen src) where
	TypeTLen x == TypeTLen y = x LenZ == y LenZ
instance Source src => Show (TypeTLen src) where
	showsPrec p (TypeTLen t) = showsPrec p $ t LenZ

-- ** Class 'Inj_Name2Type'
-- | Derive a 'Name2Type' from the given type-level list
-- of 'Proxy'-fied /type constants/.
class Inj_Name2Type cs where
	inj_Name2Type :: Source src => Name2Type src
instance Inj_Name2Type '[] where
	inj_Name2Type = Map.empty
instance
 ( Inj_KindP (Ty_of_Type (K c))
 , K c ~ Type_of_Ty (Ty_of_Type (K c))
 , Constable c
 , Inj_Name2Type cs
 ) => Inj_Name2Type (Proxy c ': cs) where
	inj_Name2Type =
		Map.insert
		 (NameTy $ Text.pack $ show $ typeRep (Proxy @c))
		 (TypeTLen $ \len -> TypeT $ TyConst noSource len $
			inj_ConstKi @(K c) @c $
			inj_KindP @(Ty_of_Type (K c)) noSource) $
		inj_Name2Type @cs

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