{-# 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.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.Megaparsec ()


main :: IO ()
main = do
	args <- Env.getArgs
	let modsTy = Sym.modulesTyInj @LCC.Sym.SS @LCC.Sym.SRC
	let impsTy = Sym.importTypes @LCC.Sym.SS []
	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
	forM_ args $ \arg -> do
		ast <- printError $ parseTe (impsTy, modsTy) (impsTe, modsTe) $ Text.pack arg
		te  <- printError $ readTe ast
		evalTe te

printError :: Show err => Either err a -> IO a
printError (Left err) = error $ show err
printError (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


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) =>
 TermVT src ss '[] ->
 IO ()
evalTe (TermVT (Term q t (TeSym te))) = do
	putStrLn $ "Type = " <> show (q #> t)
	case proveConstraint q of
	 Nothing -> putStrLn $ "Cannot prove Constraint: " <> show q
	 Just Dict -> do
		Text.putStrLn $ "View = " <> view (betaT $ te CtxTeZ)
		case proveConstraint $ Sym.tyShow t of
		 Nothing -> putStrLn $ "No Show instance for type: " <> show t
		 Just Dict -> putStrLn $ "Eval = " <> show (eval $ te CtxTeZ)

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