{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Compiling.Grammar where

import Control.Arrow (left)
import Control.Monad (void)
import Data.Semigroup (Semigroup(..))
import Data.Map.Strict (Map)
import Prelude hiding (any)
import qualified Data.Function as Fun
import qualified Data.Map.Strict as Map
import qualified Data.Text as Text

import Language.Symantic.Grammar as G
import Language.Symantic.Typing
import Language.Symantic.Compiling.Module

-- * Class 'Gram_Term_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_Term_Name g where
        g_ModNameTe :: CF g (Mod NameTe)
        g_ModNameTe = rule "ModNameTe" $
                lexeme $
                        g_ModNameTeId <+>
                        parens g_ModNameTeOp
        g_NameTe :: CF g NameTe
        g_NameTe = rule "NameTe" $
                lexeme $
                        g_NameTeId <+>
                        parens g_NameTeOp

        g_ModNameTeId :: CF g (Mod NameTe)
        g_ModNameTeId = rule "ModNameTeId" $
                Mod
                 <$> option [] (try $ g_PathMod <* char '.')
                 <*> g_NameTeId
        g_NameTeId :: CF g NameTe
        g_NameTeId = rule "NameTeId" $
                (NameTe . Text.pack <$>) $
                (identG `minus`) $
                Fun.const
                 <$> g_NameTeIdKey
                 <*. (any `but` g_NameTeIdTail)
                where
                identG = (:) <$> headG <*> many (cfOf g_NameTeIdTail)
                headG  = unicat $ Unicat_Letter
        g_NameTeIdTail :: Terminal g Char
        g_NameTeIdTail = rule "NameTeIdTail" $
                unicat Unicat_Letter <+>
                unicat Unicat_Number
        g_NameTeIdKey :: Reg rl g String
        g_NameTeIdKey = rule "NameTeIdKey" $
                choice $ string <$> ["in", "let"]

        g_ModNameTeOp :: CF g (Mod NameTe)
        g_ModNameTeOp = rule "ModNameTeOp" $
                Mod
                 <$> option [] (try $ g_PathMod <* char '.')
                 <*> g_NameTeOp
        g_NameTeOp :: CF g NameTe
        g_NameTeOp = rule "NameTeOp" $
                (NameTe . Text.pack <$>) $
                (some (cfOf g_NameTeOpOk) `minus`) $
                Fun.const
                 <$> g_NameTeOpKey
                 <*. (any `but` g_NameTeOpOk)
        g_NameTeOpOk :: Terminal g Char
        g_NameTeOpOk = rule "NameTeOpOk" $
                choice (unicat <$>
                 [ Unicat_Symbol
                 , Unicat_Punctuation
                 , Unicat_Mark
                 ]) `but` koG
                where
                koG = choice (char <$> ['(', ')', '`', '\'', ',', '[', ']'])
        g_NameTeOpKey :: Reg rl g String
        g_NameTeOpKey = rule "NameTeOpKey" $
                choice $ string <$> ["\\", "->", "=", "@"]

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

-- * Class 'Gram_Term_Type'
class
 ( Gram_Char g
 , Gram_Rule g
 , Gram_Alt g
 , Gram_AltApp g
 , Gram_App g
 , Gram_CF g
 , Gram_Comment g
 , Gram_Term_Name g
 , Gram_Type src g
 ) => Gram_Term_Type src g where
        g_term_abst_decl :: CF g (NameTe, AST_Type src)
        g_term_abst_decl = rule "TermAbstDecl" $
                parens $ (,)
                 <$> g_NameTe
                 <*  (symbol "::" <+> symbol ":")
                 -- NOTE: "::" is Haskell compatibility and ":" is another common notation.
                 <*> g_type

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

-- ** Type 'Error_Term_Gram'
data Error_Term_Gram
 =   Error_Term_Gram_Fixity Error_Fixity
 |   Error_Term_Gram_Term_incomplete
 |   Error_Term_Gram_Type_applied_to_nothing
 |   Error_Term_Gram_not_applicable
 |   Error_Term_Gram_application
 |   Error_Term_Gram_application_mismatch
 |   Error_Term_Gram_Module Error_Module
 deriving (Eq, Show)

-- * Class 'Gram_Term'
class
 ( Gram_Source src g
 , Gram_Error Error_Term_Gram g
 , Gram_Char g
 , Gram_Rule g
 , Gram_Alt g
 , Gram_App g
 , Gram_AltApp g
 , Gram_CF g
 , Gram_Comment g
 , Gram_Type src g
 , Gram_Term_Name g
 , Gram_Term_Type src g
 , Gram_Term_Atoms src ss g
 , Gram_State (Imports NameTe, Modules src ss) g
 ) => Gram_Term src ss g where
        g_term :: CF g (AST_Term src ss)
        g_term = rule "Term" $
                choice
                 [ try g_term_abst
                 , g_term_operators
                 , g_term_let
                 ]
        g_term_operators :: CF g  (AST_Term src ss)
        g_term_operators = rule "TermOperators" $
                G.catch $
                left Error_Term_Gram_Fixity <$>
                g_ops
                where
                g_ops :: CF g (Either Error_Fixity  (AST_Term src ss))
                g_ops = operators g_term_atom g_prefix g_infix g_postfix
                g_prefix  :: CF g (Unifix, AST_Term src ss -> AST_Term src ss)
                g_postfix :: CF g (Unifix, AST_Term src ss -> AST_Term src ss)
                g_infix, g_app :: CF g (Infix,  AST_Term src ss -> AST_Term src ss -> AST_Term src ss)
                g_app     = rule "TermApp"     $ G.source $ op_app <$> pure ()
                g_prefix  = rule "TermPrefix"  $ G.catch $ G.source $ G.getAfter $ op_prefix  <$> g_op_prefix
                g_postfix = rule "TermPostfix" $ G.catch $ G.source $ G.getAfter $ op_postfix <$> g_op_postfix
                g_infix   = rule "TermInfix"   $ try (G.catch $ G.source $ G.getAfter $ op_infix <$> g_op_infix) <+> g_app
                op_app :: () -> src -> (Infix, AST_Term src ss -> AST_Term src ss -> AST_Term src ss)
                op_app () src =
                        (Infix (Just AssocL) 9,) $ \a b ->
                                (BinTree0 (Token_Term_App src) `BinTree2` a) `BinTree2` b
                op_infix :: Mod NameTe -> (Imports NameTe, Modules src ss) -> src ->
                 Either Error_Term_Gram
                        (Infix, AST_Term src ss -> AST_Term src ss -> AST_Term src ss)
                op_infix name (imps, mods) src = do
                        t <- Error_Term_Gram_Module `left`
                                lookupDefTerm FixyInfix imps name mods
                        Right $ (token_fixity t,) $ \a b ->
                                (BinTree0 (token_term t src) `BinTree2` a) `BinTree2` b
                op_prefix, op_postfix ::
                 Mod NameTe ->
                 (Imports NameTe, Modules src ss) ->
                 src ->
                 Either Error_Term_Gram
                        (Unifix, AST_Term src ss -> AST_Term src ss)
                op_prefix name (imps, mods) src = do
                        t <- Error_Term_Gram_Module `left`
                                lookupDefTerm FixyPrefix imps name mods
                        Right $ (token_fixity t,) $ \a ->
                                BinTree0 (token_term t src) `BinTree2` a
                op_postfix name (imps, mods) src = do
                        t <- Error_Term_Gram_Module `left`
                                lookupDefTerm FixyPostfix imps name mods
                        Right $ (token_fixity t,) $ \a ->
                                BinTree0 (token_term t src) `BinTree2` a
                g_op_postfix :: CF g (Mod NameTe)
                g_op_postfix = rule "TermOpPostfix" $
                        lexeme $
                                g_backquote *> g_ModNameTeId <+> -- <* (G.cfOf $ Gram.Term (pure ' ') `but` g_backquote)
                                g_ModNameTeOp
                g_op_infix :: CF g (Mod NameTe)
                g_op_infix = rule "TermOpInfix" $
                        lexeme $
                                between g_backquote g_backquote g_ModNameTeId <+>
                                try g_ModNameTeOp <+>
                                pure (Mod [] " ")
                g_op_prefix :: CF g (Mod NameTe)
                g_op_prefix = rule "TermOpPrefix" $
                        lexeme $
                                g_ModNameTeId <* g_backquote <+>
                                g_ModNameTeOp
                g_backquote :: Gram_Char g' => g' Char
                g_backquote = char '`'

        g_term_atom :: CF g  (AST_Term src ss)
        g_term_atom = rule "TermAtom" $
                choice $
                 {-(try (
			G.source $
			(\typ src -> BinTree0 $ inj_EToken src $ Token_Term_Type typ)
			 <$ char '@' <*> g_type) :) $
		 -}
                 (try <$> g_term_atomsR @_ @_ @ss) <>
                 [ try $ G.catch $ G.source $ G.getAfter $
                        (\m (imps, mods) src ->
                                case lookupDefTerm FixyInfix imps m mods of
                                 Right t -> Right $ BinTree0 $ token_term t src
                                 Left err ->
                                        case m of
                                         [] `Mod` n -> Right $ BinTree0 $ Token_Term_Var src n
                                         _ -> Left $ Error_Term_Gram_Module err
                         ) <$> g_ModNameTe
                 , g_term_group
                 ]
        g_term_group :: CF g (AST_Term src ss)
        g_term_group = rule "TermGroup" $ parens g_term
        g_term_abst :: CF g (AST_Term src ss)
        g_term_abst = rule "TermAbst" $
                G.source $
                ((\(xs, te) src ->
                        foldr (\(x, ty_x) ->
                                BinTree0 . Token_Term_Abst src x ty_x) te xs) <$>) $
                g_term_abst_args_body
                 (symbol "\\" *> some g_term_abst_decl <* symbol "->")
                 g_term
        g_term_abst_args_body
         :: CF g [(NameTe, AST_Type src)]
         -> CF g (AST_Term src ss)
         -> CF g ([(NameTe, AST_Type src)], AST_Term src ss)
        -- g_term_abst_args_body args body = (,) <$> args <*> body
        g_term_abst_args_body cf_args cf_body =
                G.stateBefore $
                (\a b (imps::Imports NameTe, mods::Modules src ss) -> ((imps, mods), (a, b)))
                 <$> G.stateAfter ((<$> cf_args) $ \args (imps::Imports NameTe, mods) ->
                        ((setArgsImps args imps, setArgsMods args mods), args))
                 <*> cf_body
                where
                setArgsImps args (Imports imps) = Imports $ Map.alter (alterArgsImps args) [] imps
                alterArgsImps args = \case
                 Nothing -> Just mempty
                 Just m -> Just $ mapMapFixity (delArgImp args) m
                delArgImp :: [(NameTe, _a)] -> Map NameTe PathMod -> Map NameTe PathMod
                delArgImp = flip $ foldr $ \(n, _) -> Map.delete n

                setArgsMods args (Modules mods) = Modules $ Map.alter (alterArgsMods args) [] mods
                alterArgsMods args = \case
                 Nothing -> Just moduleEmpty{byInfix = mempty `insArgMod` args}
                 Just m -> Just m
                         { byPrefix  = byPrefix  m `delArgMod` args
                         , byInfix   = byInfix   m `insArgMod` args
                         , byPostfix = byPostfix m `delArgMod` args
                         }
                delArgMod :: ModuleFixy src ss Unifix -> [(NameTe, _a)] -> ModuleFixy src ss Unifix
                delArgMod = foldr $ \(n, _) -> Map.delete n
                insArgMod :: ModuleFixy src ss Infix -> [(NameTe, _a)] -> ModuleFixy src ss Infix
                insArgMod = foldr $ \(n, _) ->
                        Map.insert n Tokenizer
                         { token_term   = (`Token_Term_Var` n)
                         , token_fixity = infixN5
                         }
        g_term_let :: CF g  (AST_Term src ss)
        g_term_let = rule "TermLet" $
                G.source $
                (\name args bound body src ->
                        BinTree0 $
                        Token_Term_Let src name
                         (foldr (\(x, ty_x) ->
                                BinTree0 . Token_Term_Abst src x ty_x) bound args) body)
                 <$  symbol "let"
                 <*> g_NameTe
                 <*> many g_term_abst_decl
                 <*  symbol "="
                 <*> g_term
                 <*  symbol "in"
                 <*> g_term

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

-- ** Class 'Gram_Term_Atoms'
type Gram_Term_Atoms src ss g = Gram_Term_AtomsR src ss ss g

-- *** Class 'Gram_Term_AtomsR'
class Gram_Term_AtomsR src (ss::[*]) (rs::[*]) g where
        g_term_atomsR :: [CF g (AST_Term src ss)]
instance Gram_Term_AtomsR src ss '[] g where
        g_term_atomsR = []
instance
 ( Gram_Term_AtomsFor src ss g t
 , Gram_Term_AtomsR src ss rs g
 ) => Gram_Term_AtomsR src ss (Proxy t ': rs) g where
        g_term_atomsR =
                g_term_atomsFor @_ @_ @_ @t <>
                g_term_atomsR @_ @_ @rs

-- *** Class 'Gram_Term_AtomsFor'
class Gram_Term_AtomsFor src ss g t where
        g_term_atomsFor :: [CF g (AST_Term src ss)]
        g_term_atomsFor = []

gram_term
 :: forall g.
 ( Gram_Term () '[Proxy (->), Proxy Integer] g
 ) => [CF g ()]
gram_term =
 [ voiD g_term
 , voiD g_term_operators
 , voiD g_term_atom
 , voiD g_term_group
 , voiD g_term_abst
 , void (g_term_abst_decl::CF g (NameTe, AST_Type ()))
 , voiD g_term_let
 , void g_ModNameTe
 , void g_NameTe
 , void g_NameTeId
 , void $ G.cfOf g_NameTeIdTail
 , void $ G.cfOf g_NameTeIdKey
 , void g_ModNameTeOp
 , void g_NameTeOp
 , void $ G.cfOf g_NameTeOpOk
 , void $ G.cfOf g_NameTeOpKey
 ] where
        voiD :: CF g (AST_Term () '[Proxy (->), Proxy Integer]) -> CF g ()
        voiD = (() <$)