{-# 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.Proxy (Proxy(..))
import Data.Semigroup (Semigroup(..))
import Data.String (IsString(..))
import Prelude hiding (any)
import qualified Data.Char as Char
import qualified Data.Text as Text
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map

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 (At src (Mod NameTy))
 |   Token_Type_Var   (At src NameVar)
 -- deriving (Eq, Show)
instance Source src => Eq (Token_Type src) where
	Token_Type_Const (At _ x) == Token_Type_Const (At _ y) = x == y
	Token_Type_Var   (At _ x) == Token_Type_Var   (At _ y) = x == y
	_ == _ = False
instance Source src => Show (Token_Type src) where
	showsPrec p (Token_Type_Const (At _ 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

-- ** 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 $ \len -> TypeT $ TyConst noSource len $
			constKiInj @(K c) @c $
			kindInjP @(Ty_of_Type (K 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
 , NameTyOf (->)
 , NameTyOf []
 , NameTyOf (,)
 ) => 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 $ At src $ nameTyOf $ Proxy @(->))
	-- 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 src = BinTree0 $ Token_Type_Const $ At src $ nameTyOf $ Proxy @[]
	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 $ At src $ nameTyOf $ Proxy @(,))
	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_symbol
	g_type_name_const :: CF g (AST_Type src)
	g_type_name_const = rule "type_name_const" $
		lexeme $ source $
		(\n src -> BinTree0 $ Token_Type_Const $ At src n)
		 <$> g_ModNameTy
		 -- <$> unicat (Unicat Char.UppercaseLetter)
		 -- <*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])
	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])
	{-
	g_type_symbol :: CF g (AST_Type src)
	g_type_symbol = rule "type_symbol" $
		source $ (mk <$>) $
		parens $ many $ cfOf $ choice g_ok `but` choice g_ko
		where
		mk s src = BinTree0 $ Token_Type_Const $ At src $ Mod [] $ fromString $ "(" ++ s ++ ")"
		g_ok = unicat <$>
		 [ Unicat_Symbol
		 , Unicat_Punctuation
		 , Unicat_Mark
		 ]
		g_ko = char <$> ['(', ')', '`']
	-}

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

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