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

import Control.Applicative (Applicative(..))
import Control.Monad (Monad(..), forM)
import Data.Bool (Bool(..))
import Data.Char (Char)
import Data.Either (Either(..), either)
import Data.Eq (Eq)
import Data.Function (($), (.), id)
import Data.Functor (Functor(..), (<$>))
import Data.Functor.Identity (Identity(..))
import Data.Foldable (foldr1)
import Data.Maybe (Maybe(..), maybe)
import Data.Semigroup ((<>))
import Data.Text (Text)
import Prelude (error)
import System.IO (IO, putStrLn)
import Text.Show (Show(..))
import qualified Control.Monad.Classes.Run 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.Environment as Env
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 Hcompta.LCC.Read ()

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


main :: IO ()
main = do
	args <- Env.getArgs
	let modsTy = Sym.modulesTyInj @LCC.Sym.SS @LCC.Sym.SRC
	let impsTy = Sym.importTypes @LCC.Sym.CS []
	let modsTe :: Modules LCC.Sym.SRC LCC.Sym.SS =
		either (error . show) id $
		Sym.deleteDefTermInfix ([] `Mod` "$") `fmap`
		modulesInj
	let impsTe = [] `Sym.importModules` modsTe
	(`D.ansiIO` IO.stderr) $ docModules impsTy modsTe
	let arg = Text.unwords $ Text.pack <$> args
	ast <- printError $ parseTe (impsTy, modsTy) (impsTe, modsTe) arg
	{-
	ast <- (foldr1 G.BinTree2 <$>) $ forM args $ \arg -> do
		printError $ parseTe (impsTy, modsTy) (impsTe, modsTe) $ Text.pack arg
	-}
	te <- printError $ readTe ast
	evalTe impsTy te
	{-
	forM_ args $ \arg -> do
		ast <- printError $ parseTe (impsTy, modsTy) (impsTe, modsTe) $ Text.pack arg
		te  <- printError $ readTe ast
		evalTe impsTy te
	-}

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


type G src ss =
 P.ParsecT P.Dec Text
           (SS.StateT (Imports NameTe, Modules src ss)
                      ((SS.StateT (Imports NameTy, ModulesTy src))
                                  Identity))

parseTe ::
 forall ss src.
 Gram_Term src ss (G src ss) =>
 (Imports NameTy, ModulesTy src) ->
 (Imports NameTe, Modules src ss) ->
 Text -> Either (P.ParseError Char P.Dec) (AST_Term src ss)
parseTe tys tes inp =
	runIdentity $
	MC.evalStateStrict tys $
	MC.evalStateStrict tes $
	P.runParserT g "" inp
	where g = G.unCF $ Sym.g_term <* G.eoi

type ReadTe src ss =
 ( Gram_Term    src ss (G src ss)
 , ImportTypes      ss
 , ModulesInj   src ss
 , ModulesTyInj     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
 , Eq src
 , Show src
 ) =>
 AST_Term src ss ->
 Either (Error_Term src) (TermVT src ss '[])
readTe = Sym.readTerm CtxTyZ

evalTe ::
 Source src =>
 Syms ss View =>
 Syms ss Eval =>
 Syms ss (BetaT View) =>
 Sym.Imports Sym.NameTy ->
 TermVT src ss '[] ->
 IO ()
evalTe imps (TermVT (Term q t (TeSym te))) = do
	(`D.ansiIO` IO.stdout) $ "Type = " <> Sym.docType
		Sym.config_Doc_Type
		 { config_Doc_Type_vars_numbering = False
		 , config_Doc_Type_imports        = imps
		 } 0 (q #> t) <> D.eol
	case proveConstraint q of
	 Nothing -> putStrLn $ "Cannot prove Constraint: " <> show q
	 Just Dict -> do
		Text.putStrLn $ "View = " <> view (betaT $ te CtxTeZ)
		case t of
		 TyApp _ io aTy | Just HRefl <- proj_ConstKiTy @_ @IO io -> do
			a <- eval $ te CtxTeZ
			case proveConstraint $ Sym.tyShow aTy of
			 Nothing -> putStrLn $ "No Show instance for type: " <> show aTy
			 Just Dict -> putStrLn $ "Eval = " <> show a
		 _ ->
			let a = eval $ te CtxTeZ in
			case proveConstraint $ Sym.tyShow t of
			 Nothing -> putStrLn $ "No Show instance for type: " <> show t
			 Just Dict -> putStrLn $ "Eval = " <> show a

{-
main :: IO ()
main = do
	args <- Env.getArgs
	forM_ args $ \arg ->
		readCompta @LCC.Sym.SRC @SS arg >>= \case
		 Left (Error_Read_Syntax err) ->
			showParseError err >>=
			(`Doc.ansiIO` stderr)
		 Left (Error_Read_Semantic err) -> error $ show err
		 Right (r, warns) -> do
			print warns
			-- print r
			(`Doc.ansiIO` stdout) $
				d_compta context_write r

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

printErrorS :: Show err => S.Either err a -> IO a
printErrorS (S.Left err) = error $ show err
printErrorS (S.Right a)  = return a
-}

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 =>
 Sym.PathMod -> Sym.NameTe -> d
docPathTe (ms::Sym.PathMod) (Sym.NameTe n) =
	D.catH $
	L.intersperse (D.charH '.') $
	((\(Sym.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