{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Main where

import Control.Applicative (Applicative(..))
import Control.Monad (Monad(..), void)
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.Trans.Class as MT (MonadTrans(..))
import Data.Bool (Bool(..))
import Data.Char (Char)
import Data.Either (Either(..))
import Data.Eq (Eq(..))
import Data.Function (($), (.), id)
import Data.Functor (Functor(..), (<$>))
import Data.Maybe (Maybe(..), maybe)
import Data.Semigroup ((<>))
import Data.String (String)
import Data.Text (Text)
import Prelude (error, succ, Integer)
import System.Console.Haskeline as HL
import System.IO (IO, putStr, putStrLn, print)
import Text.Show (Show(..))
import qualified Control.Monad.Classes as MC
import qualified Control.Monad.Trans.State.Strict as SS
import qualified Data.Char as Char
import qualified Data.List as L
import qualified Data.Map.Strict as Map
import qualified Data.Text as T
import qualified Data.Text as Text
import qualified Data.Text.IO as Text
import qualified System.Console.Haskeline.History as HL
import qualified System.IO as IO
import qualified Text.Megaparsec as P

import Language.Symantic as Sym
import qualified Language.Symantic.Document as D
import qualified Language.Symantic.Grammar as G
import qualified Language.Symantic.Lib as Sym

import qualified Hcompta.LCC.Sym as LCC.Sym
import qualified Hcompta.LCC as LCC
import qualified Hcompta.LCC.Lib.Strict as S
import Hcompta.LCC.Read ()
import Hcompta.LCC.Write (Writeable(..), context_write)

-- dbg :: Show a => String -> a -> a
-- dbg msg x = trace (msg ++ " = " ++ show x) x

main :: IO ()
main = do
	runInputT defaultSettings
	 { historyFile    = Just ".hcompta.history"
	 , autoAddHistory = False
	 } $
		S.evalState (LCC.state_sym @LCC.Sym.SRC @LCC.Sym.SS) $
		unREPL (loop True 0)
	where
	loop :: forall src ss.
	 Show src =>
	 Syms ss Eval =>
	 Syms ss View =>
	 Syms ss (BetaT View) =>
	 ReadTe src ss =>
	 Gram_Term src ss (G src ss (InputT IO)) =>
	 Bool -> Integer -> REPL src ss ()
	loop ok i = do
		let prompt =
			"\SOH\ESC["
			 <> (if ok then "32" else "31")
			 <> ";1m\STX"
			 <> show i
			 <> "\SOH\ESC[34;1m\STX>\SOH\ESC[0;48;05;233m\STX "
		-- Σ
		line <- readLine prompt
		case line of
		 Nothing -> loop ok i
		 Just l -> do
			void $ REPL $ lift $
				HL.modifyHistory $
				HL.addHistoryRemovingAllDupes l
			REPL (parseTe $ Text.pack l) >>= \case
			 Left err -> do
				liftIO $ putStr $ P.parseErrorPretty err
				loop False (succ i)
			 Right expr ->
				case expr of
				 Command_Def nam ast -> runTe nam ast
				 Command_Eval    ast -> runTe "it" ast
		where
		runTe nam ast =
			case readTe ast of
			 Left err -> do
				liftIO $ print err
				loop False (succ i)
			 Right te -> do
				REPL $ do
					MC.modify $ \(imps::Imports NameTe, mods) ->
						(imps, insTerm nam te mods)
					evalTe te
				loop True (succ i)
		insTerm :: Sym.NameTe -> Sym.TermVT src ss '[] -> Sym.Modules src ss -> Sym.Modules src ss
		insTerm n t = Sym.insertTermVT ([] `Sym.Mod` t) n (Sym.Fixity2 Sym.infixN5)

type G src ss m =
 P.ParsecT P.Dec Text
           (S.StateT (LCC.State_Sym src ss) m)

data Command src ss
 =   Command_Eval (AST_Term src ss)
 |   Command_Def  NameTe (AST_Term src ss)
 deriving (Eq, Show)

parseTe ::
 forall ss src m.
 Monad m =>
 Gram_Term src ss (G src ss m) =>
 Text -> S.StateT (LCC.State_Sym src ss) m
                  (Either (P.ParseError Char P.Dec) (Command src ss))
parseTe = P.runParserT g ""
	where
	g :: G src ss m (Command src ss)
	g = G.unCF $ G.try gCmdLet G.<+> gCmdEval
	gCmdLet =
		Command_Def
		 <$  G.optional (G.try $ G.symbol "let")
		 <*> Sym.g_NameTe
		 <*  G.symbol "="
		 <*> Sym.g_term
		 <*  G.eoi
	gCmdEval =
		Command_Eval
		 <$> Sym.g_term
		 <*  G.eoi

-- * Type 'ReadTe'
type ReadTe src ss =
 ( SourceInj (TypeVT src)    src
 , SourceInj (KindK src)     src
 , SourceInj (AST_Type src)  src
 )

readTe ::
 forall src ss.
 ( Syms ss Eval
 , Syms ss View
 , Syms ss (BetaT View)
 , ReadTe src ss
 ) =>
 AST_Term src ss ->
 Either (Error_Term src) (TermVT src ss '[])
readTe = Sym.readTerm CtxTyZ

-- | Lifted 'D.ansiIO' on 'IO.stdout'. Helper.
ansiIO :: MonadIO m => D.ANSI_IO -> m ()
ansiIO = liftIO . (`D.ansiIO` IO.stdout)

evalTe ::
 forall src ss m.
 Source src =>
 Syms ss View =>
 Syms ss Eval =>
 Syms ss (BetaT View) =>
 MonadIO m =>
 TermVT src ss '[] ->
 S.StateT (LCC.State_Sym src ss) m ()
evalTe (TermVT (Term q t (TeSym te))) = do
	printTy (q #> t) >>= ansiIO . ("Type: " <>)
	case proveConstraint q of
	 Nothing -> printTy q >>= ansiIO . ("Cannot prove Constraint: " <>)
	 Just Dict -> liftIO $ do
		Text.putStrLn $ "View: " <> view (betaT $ te CtxTeZ)
		case t of
		 io:@aTy | Just HRefl <- proj_ConstKiTy @_ @IO io -> do
			a <- eval $ te CtxTeZ
			printTe aTy a
		 aTy ->
			let a = eval $ te CtxTeZ in
			printTe aTy a

printTy ::
 forall src ss m vs t d.
 Source src =>
 D.Doc_Text d =>
 D.Doc_Color d =>
 MonadIO m =>
 Type src vs t ->
 S.StateT (LCC.State_Sym src ss) m d
printTy ty = do
	(impsTy, _ :: Sym.ModulesTy src) <- MC.get
	return $ Sym.docType
		Sym.config_Doc_Type
		 { config_Doc_Type_vars_numbering = False
		 , config_Doc_Type_imports        = impsTy
		 } 0 ty <> D.eol

printTe :: Source src => Type src vs a -> a -> IO ()
printTe aTy a =
	case proveConstraint $ LCC.Sym.tyWriteable
	 (allocVarsR (lenVars aTy) $ LCC.Sym.tyContext_Write @_ @'[] ~> LCC.Sym.tyANSI_IO) aTy of
	 Just Dict -> (`D.ansiIO` IO.stdout) $ write a context_write
	 Nothing ->
		case proveConstraint $ Sym.tyShow aTy of
		 Nothing -> putStrLn $ "No Show instance for type: " <> show aTy
		 Just Dict -> print a


-- * Type 'REPL'
-- /Read Eval Print Loop/ monad.
newtype REPL src ss a
 =      REPL
 {    unREPL :: S.StateT (LCC.State_Sym src ss) (InputT IO) a }
 deriving ( Functor
          , Applicative
          , Monad
          , MonadIO
          -- , MonadState State_REPL
          )
{-
instance MonadTrans (REPL src ss) where
	lift = REPL . lift . lift
-}
type instance MC.CanDo (REPL src ss) (MC.EffState (LCC.State_Sym src ss)) = 'False
type instance MC.CanDo (REPL src ss) (MC.EffState (Sym.Imports ns, Sym.Modules src ss)) = 'False
type instance MC.CanDo (REPL src ss) (MC.EffState (Sym.Imports ns, Sym.ModulesTy src))  = 'False

-- * Type 'State_REPL'
data State_REPL
 =   State_REPL
 {   state_repl_env :: ()
 }



readLine :: String -> REPL src ss (Maybe String)
readLine prompt = do
	line <- REPL . lift $ getInputLine prompt
	case line of
	 Just l@(':':_) -> return $ Just l
	 Just l@(_:_) | L.last l == ' ' -> readLines l
	 Just l  -> return $ Just l
	 Nothing -> return Nothing
	where
	readLines :: String -> REPL src ss (Maybe String)
	readLines acc = do
		line <- REPL . lift $ getInputLine ""
		case line of
		 Just l@(_:_) | L.last l == ' ' -> readLines $ acc <> l
		 Just l  -> return $ Just $ acc <> l
		 Nothing -> return $ Just acc




docModules ::
 Source src =>
 D.Doc_Text d =>
 D.Doc_Color d =>
 D.Doc_Decoration d =>
 ReadTe src ss =>
 Sym.Imports Sym.NameTy ->
 Sym.Modules src ss -> d
docModules imps (Sym.Modules mods) =
	Map.foldrWithKey
	 (\p m doc -> docModule imps p m <> doc)
	 D.empty
	 mods

docModule ::
 forall src ss d.
 Source src =>
 D.Doc_Text d =>
 D.Doc_Color d =>
 D.Doc_Decoration d =>
 ReadTe src ss =>
 Sym.Imports Sym.NameTy ->
 Sym.PathMod -> Sym.Module src ss -> d
docModule imps m Sym.ByFixity
 { Sym.byPrefix
 , Sym.byInfix
 , Sym.byPostfix
 } =
	go docFixityInfix   byInfix <>
	go docFixityPrefix  byPrefix <>
	go docFixityPostfix byPostfix
	where
	go :: (fixy -> d) -> ModuleFixy src ss fixy -> d
	go docFixy =
		Map.foldrWithKey
		 (\n Sym.Tokenizer
			 { Sym.token_fixity
			 , Sym.token_term = t
			 } doc ->
			docPathTe m n <>
			docFixy token_fixity <>
			D.space <> D.bold (D.yellower "::") <> D.space <>
			docTokenTerm imps (t Sym.noSource) <>
			D.eol <> doc)
		 D.empty

docTokenTerm ::
 forall src ss d.
 Source src =>
 D.Doc_Text d =>
 D.Doc_Color d =>
 ReadTe src ss =>
 Sym.Imports Sym.NameTy ->
 Sym.Token_Term src ss -> d
docTokenTerm imps t =
	case Sym.readTerm CtxTyZ (G.BinTree0 t) of
	 Left{} -> error "[BUG] docTokenTerm: readTerm failed"
	 Right (Sym.TermVT te) ->
		Sym.docType Sym.config_Doc_Type
		 { config_Doc_Type_vars_numbering = False
		 , config_Doc_Type_imports        = imps
		 } 0 $ Sym.typeOfTerm te

docFixityInfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Infix -> t
docFixityInfix = \case
	 Sym.Infix Nothing 5 -> D.empty
	 Sym.Infix a p ->
		let docAssoc = \case
			 Sym.AssocL -> "l"
			 Sym.AssocR -> "r"
			 Sym.AssocB Sym.SideL -> "l"
			 Sym.AssocB Sym.SideR -> "r" in
		D.magenta $ " infix" <> maybe D.empty docAssoc a <>
		D.space <> D.bold (D.bluer (D.int p))
docFixityPrefix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t
docFixityPrefix p = D.magenta $ " prefix "  <> D.bold (D.bluer (D.int $ Sym.unifix_prece p))
docFixityPostfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t
docFixityPostfix p = D.magenta $ " postfix " <> D.bold (D.bluer (D.int $ Sym.unifix_prece p))

docPathTe ::
 D.Doc_Text d =>
 D.Doc_Color d =>
 PathMod -> NameTe -> d
docPathTe ms (NameTe n) =
	D.catH $
	L.intersperse (D.charH '.') $
	((\(NameMod m) -> D.textH m) <$> ms) <>
	[(if isOp n then id else D.yellower) $ D.text n]
	where
	isOp = T.all $ \case '_' -> True; '\'' -> True; c -> Char.isAlphaNum c


{-
mainSym :: IO ()
mainSym = do
	args <- Env.getArgs
	let sym@(LCC.State_Sym (impsTy,_modsTy) (_impsTe,patchModsTe -> modsTe)) =
		LCC.state_sym @LCC.Sym.SRC @LCC.Sym.SS
	(`D.ansiIO` IO.stderr) $ docModules impsTy modsTe
	let arg = Text.unwords $ Text.pack <$> args
	ast <- printError $ parseTe sym arg
	{-
	ast <- (foldr1 G.BinTree2 <$>) $ forM args $ \arg -> do
		printError $ parseTe sym $ Text.pack arg
	-}
	_te <- printError $ readTe ast
	return ()
	{-
	evalTe impsTy te
	forM_ args $ \arg -> do
		ast <- printError $ parseTe (impsTy, modsTy) (impsTe, modsTe) $ Text.pack arg
		te  <- printError $ readTe ast
		evalTe impsTy te
	-}
	where
	patchModsTe = Sym.deleteDefTermInfix ([] `Mod` "$")

printError :: Show err => MonadIO m => Either err a -> m a
printError (Left err) = liftIO $ error $ show err
printError (Right a)  = return a

parseTe ::
 forall ss src m.
 m ~ Identity =>
 Show src =>
 G.Gram_Source src (G src ss m) =>
 Gram_Term src ss (G src ss m) =>
 LCC.State_Sym src ss ->
 Text -> Either (P.ParseError Char P.Dec) (Command src ss)
parseTe sym inp =
	runIdentity $
	S.evalState sym $
	P.runParserT g "" inp
	where
	g :: G src ss Identity (Command src ss)
	g = G.unCF $
		G.try (Command_Def <$> Sym.g_NameTe <* G.lexeme (G.char '=') <*> Sym.g_term <* G.eoi) G.<+>
		(Command_Eval <$> Sym.g_term <* G.eoi)
-}