{-# 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 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   (Sourced 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 (Sourced _ x) == Token_Type_Var (Sourced _ 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 (Sourced _ 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_Char 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_Char 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_Char 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 "TypeFun" $
                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 "TypeList" $
                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 "TypeTuple2" $
                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 "TypeApp" $
                foldl1' BinTree2 <$> some (g_type_atom)
        g_type_atom :: CF g (AST_Type src)
        g_type_atom = rule "TypeAtom" $
                try (parens g_type) <+>
                g_type_const <+>
                g_type_var
        g_type_const :: CF g (AST_Type src)
        g_type_const = rule "TypeConst" $
                lexeme $ catch $ source $ getBefore $
                (\n (impsTy, modsTy) src -> BinTree0 . Token_Type_Const <$> readTyName impsTy modsTy src n)
                 <$> g_ModNameTy
        g_type_var :: CF g (AST_Type src)
        g_type_var = rule "TypeVar" $
                lexeme $ source $
                (\n ns src -> BinTree0 $ Token_Type_Var $ Sourced 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 $ Sourced src name

-- * Type 'Error_Type'
data Error_Type src
 =   Error_Type_Constant_unknown (Sourced 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_const
 , g_type_var
 -- , g_type_symbol
 ]