{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Typing.Grammar where

import Control.Applicative (Applicative(..))
import Data.List (foldl1')
import Data.Map.Strict (Map)
import Data.Maybe (fromMaybe)
import Data.Semigroup (Semigroup(..))
import Data.String (IsString(..))
import Prelude hiding (any)
import qualified Data.Char as Char
import qualified Data.Map.Strict as Map
import qualified Data.Text as Text

import Language.Symantic.Grammar as G
import Language.Symantic.Typing.Kind
import Language.Symantic.Typing.Variable
import Language.Symantic.Typing.List
import Language.Symantic.Typing.Module
import Language.Symantic.Typing.Type

-- * Type 'AST_Type'
-- | /Abstract Syntax Tree/ of 'Token_Type'.
type AST_Type src = BinTree (Token_Type src)

-- ** Type 'Token_Type'
data Token_Type src
 =   Token_Type_Const (TypeTLen src)
 |   Token_Type_Var   (At src NameVar)
 -- deriving (Eq, Show)
instance Source src => Eq (Token_Type src) where
	Token_Type_Const (TypeTLen x) == Token_Type_Const (TypeTLen y) = x LenZ == y LenZ
	Token_Type_Var (At _ x) == Token_Type_Var (At _ y) = x == y
	_ == _ = False
instance (Source src, Show (TypeT src '[])) => Show (Token_Type src) where
	showsPrec p (Token_Type_Const x) =
		showParen (p >= 10) $
		showString "Token_Type_Const" .
		showChar ' ' . showsPrec 10 x
	showsPrec p (Token_Type_Var (At _ x)) =
		showParen (p >= 10) $
		showString "Token_Type_Var" .
		showChar ' ' . showsPrec 10 x

-- * Type 'ModulesTy'
type ModulesTy src = Map (Mod NameTy) (TypeTLen src)

-- ** Type 'TypeTLen'
-- | Like 'TypeT', but needing a @(@'Len'@ vs)@ to be built.
--
-- Useful to build a 'ModulesTy' 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 (TypeT src '[])) => Show (TypeTLen src) where
	showsPrec p (TypeTLen t) = showsPrec p $ t LenZ

typeTLen ::
 forall c src.
 Source src =>
 Constable c =>
 KindInjP (Ty_of_Type (K c)) =>
 K c ~ Type_of_Ty (Ty_of_Type (K c)) =>
 src ->
 TypeTLen src
typeTLen src =
	TypeTLen $ \len -> TypeT $
		TyConst src len $
		constKiInj @(K c) @c $
		kindInjP @(Ty_of_Type (K c)) noSource

-- ** Class 'ModulesTyInj'
-- | Derive a 'ModulesTy' from the given type-level list
-- of 'Proxy'-fied /type constants/.
class ModulesTyInj ts where
	modulesTyInj :: Source src => ModulesTy src
instance ModulesTyInj '[] where
	modulesTyInj = Map.empty
instance
 ( KindInjP (Ty_of_Type (K c))
 , K c ~ Type_of_Ty (Ty_of_Type (K c))
 , Constable c
 , ModulesTyInj ts
 ) => ModulesTyInj (Proxy c ': ts) where
	modulesTyInj =
		Map.insert
		 (nameTyOf $ Proxy @c)
		 (typeTLen @c noSource) $
		modulesTyInj @ts


-- * Class 'Gram_Mod'
class
 ( Gram_Terminal g
 , Gram_Rule g
 , Gram_Alt g
 , Gram_Try g
 , Gram_App g
 , Gram_AltApp g
 , Gram_RegL g
 , Gram_CF g
 , Gram_Comment g
 , Gram_Op g
 ) => Gram_Mod g where
	g_PathMod :: CF g PathMod
	g_PathMod = rule "PathMod" $
		infixrG
		 (pure <$> g_NameMod)
		 (op <$ char '.')
		where op = (<>)
	g_NameMod :: CF g NameMod
	g_NameMod = rule "NameMod" $
		NameMod . Text.pack <$> identG
		where
		identG = (:) <$> headG <*> many (cfOf tailG)
		headG = unicat $ Unicat Char.UppercaseLetter
		tailG :: Terminal g Char
		tailG =
			unicat Unicat_Letter <+>
			unicat Unicat_Number

deriving instance Gram_Mod g => Gram_Mod (CF g)
instance Gram_Mod EBNF
instance Gram_Mod RuleEBNF

-- * Class 'Gram_Type_Name'
class
 ( Gram_Terminal g
 , Gram_Rule g
 , Gram_Alt g
 , Gram_Try g
 , Gram_App g
 , Gram_AltApp g
 , Gram_RegL g
 , Gram_CF g
 , Gram_Comment g
 , Gram_Op g
 , Gram_Mod g
 ) => Gram_Type_Name g where
	g_ModNameTy :: CF g (Mod NameTy)
	g_ModNameTy = rule "ModNameTy" $
		lexeme $
			g_ModNameTyId <+>
			parens g_ModNameTyOp
	
	g_ModNameTyId :: CF g (Mod NameTy)
	g_ModNameTyId = rule "ModNameTyId" $
		Mod
		 <$> option [] (try $ g_PathMod <* char '.')
		 <*> g_NameTyId
	g_NameTyId :: CF g NameTy
	g_NameTyId = rule "NameTyId" $
		NameTy . Text.pack <$> identTyG
		where
		identTyG = (:) <$> headTyG <*> many (cfOf tailTyG)
		headTyG = unicat $ Unicat Char.UppercaseLetter
		tailTyG :: Terminal g Char
		tailTyG =
			unicat Unicat_Letter <+>
			unicat Unicat_Number
	
	g_ModNameTyOp :: CF g (Mod NameTy)
	g_ModNameTyOp = rule "ModNameTyOp" $
		Mod
		 <$> option [] (try $ g_PathMod <* char '.')
		 <*> g_NameTyOp
	g_NameTyOp :: CF g NameTy
	g_NameTyOp = rule "NameTyOp" $
		NameTy . Text.pack <$> many (cfOf okG)
		where
		okG :: Terminal g Char
		okG = choice (unicat <$>
			 [ Unicat_Symbol
			 , Unicat_Punctuation
			 , Unicat_Mark
			 ]) `but` koG
		koG = choice (char <$> ['(', ')', '`', '\'', '[', ']'])

deriving instance Gram_Type_Name g => Gram_Type_Name (CF g)
instance Gram_Type_Name EBNF
instance Gram_Type_Name RuleEBNF

-- * Class 'Gram_Type'
-- | Read an 'AST_Type' from a textual source.
class
 ( Gram_Source src g
 , Gram_Terminal g
 , Gram_Rule g
 , Gram_Alt g
 , Gram_Try g
 , Gram_App g
 , Gram_AltApp g
 , Gram_CF g
 , Gram_Comment g
 , Gram_Op g
 , Gram_Type_Name g
 , Gram_Error (Error_Type src) g
 , Gram_State (Imports NameTy, ModulesTy src) g
 , Constable (->)
 , Constable []
 , Constable (,)
 ) => Gram_Type src g where
	g_type :: CF g (AST_Type src)
	g_type = rule "type" $ g_type_fun
	g_type_fun :: CF g (AST_Type src)
	g_type_fun = rule "type_fun" $
		infixrG g_type_list (source $ op <$ symbol "->")
		where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ typeTLen @(->) src)
	-- TODO: maybe not harcoding g_type_list and g_type_tuple2
	g_type_list :: CF g (AST_Type src)
	g_type_list = rule "type_list" $
		source $ inside mk
		 (symbol "[") (optional g_type) (symbol "]")
		 (const <$> g_type_tuple2)
		where
		mk Nothing  src = tok src
		mk (Just a) src = BinTree2 (tok src) a
		tok = BinTree0 . Token_Type_Const . typeTLen @[]
	g_type_tuple2 :: CF g (AST_Type src)
	g_type_tuple2 = rule "type_tuple2" $
		try (parens (infixrG (g_type) (source $ op <$ symbol ","))) <+> (g_type_app)
		where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ typeTLen @(,) src)
	g_type_app :: CF g (AST_Type src)
	g_type_app = rule "type_app" $
		foldl1' BinTree2 <$> some (g_type_atom)
	g_type_atom :: CF g (AST_Type src)
	g_type_atom = rule "type_atom" $
		try (parens g_type) <+>
		g_type_name_const <+>
		g_type_name_var
	g_type_name_const :: CF g (AST_Type src)
	g_type_name_const = rule "type_name_const" $
		lexeme $ catch $ source $ getBefore $
		(\n (impsTy, modsTy) src -> BinTree0 . Token_Type_Const <$> readTyName impsTy modsTy src n)
		 <$> g_ModNameTy
	g_type_name_var :: CF g (AST_Type src)
	g_type_name_var = rule "type_name_var" $
		lexeme $ source $
		(\n ns src -> BinTree0 $ Token_Type_Var $ At src $ fromString $ n:ns)
		 <$> unicat (Unicat Char.LowercaseLetter)
		 <*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])

deriving instance Gram_Type src g => Gram_Type src (CF g)
instance
 ( Gram_Source src EBNF
 , Constable (->)
 , Constable (,)
 , Constable []
 ) => Gram_Type src EBNF
instance
 ( Gram_Source src RuleEBNF
 , Constable (->)
 , Constable (,)
 , Constable []
 ) => Gram_Type src RuleEBNF

-- | 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 -> Mod NameTy ->
 Either (Error_Type src) (TypeTLen src)
readTyName is ms src name@(m `Mod` n) =
	let m' = fromMaybe m $ lookupImports FixyInfix name is in
	case Map.lookup (m' `Mod` n) ms of
	 Just t -> Right t
	 Nothing -> Left $ Error_Type_Constant_unknown $ At src name

-- * 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

-- | List of the rules of 'Gram_Type'.
gram_type :: Gram_Type () g => [CF g (AST_Type ())]
gram_type =
 [ g_type
 , g_type_fun
 , g_type_list
 , g_type_tuple2
 , g_type_app
 , g_type_atom
 , g_type_name_const
 , g_type_name_var
 -- , g_type_symbol
 ]