{-# 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 mods::Modules LCC.Sym.SRC LCC.Sym.SS =
		either (error . show) id $
		Sym.deleteDefTermInfix ([] `Mod` "$") `fmap`
		modulesInj
	(`D.ansiIO` IO.stderr) $ docModules mods
	forM_ args $ \arg -> do
		ast <- printError $ parseTe mods (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.Modules src ss -> d
docModules (Sym.Modules mods) =
	Map.foldrWithKey
	 (\p m doc -> docModule 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.PathMod -> Sym.Module src ss -> d
docModule m Sym.Module
 { Sym.module_infix
 , Sym.module_prefix
 , Sym.module_postfix
 } =
	go docFixityInfix   module_infix <>
	go docFixityPrefix  module_prefix <>
	go docFixityPostfix module_postfix
	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 (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.Token_Term src ss -> d
docTokenTerm t =
	let n2t = name2typeInj @ss in
	case Sym.readTerm n2t 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
		 } 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))

docPathMod :: D.Doc_Text d => PathMod -> d
docPathMod (p::Sym.PathMod) =
	D.catH $
	L.intersperse (D.charH '.') $
	(\(Sym.NameMod n) -> D.textH n) <$> 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



parseTe ::
 Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Sym.Imports, Modules src ss) Identity)) =>
 Sym.Modules src ss ->
 Text ->
 Either (P.ParseError Char P.Dec) (AST_Term src ss)
parseTe mods inp =
	let imps = importQualifiedAs [] mods in
	fmap reduceTeApp $
	runIdentity $
	MC.evalStateStrict (imps, mods) $
	P.runParserT g "" inp
	where
	g = G.unCF $ Sym.g_term <* G.eoi

type ReadTe src ss =
 ( Gram_Term    src ss (P.ParsecT P.Dec Text (SS.StateT (Sym.Imports, Modules src ss) Identity))
 , ModulesInj   src ss
 , Name2TypeInj     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 ast =
	let n2t = name2typeInj @ss in
	Sym.readTerm n2t CtxTyZ ast

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

{-
parse :: Text -> IO (Sym.EToken LCC.Meta SS)
parse inp = do
	print inp
	let mods = Sym.inj_Modules @SS
	{-
	let mods' = mods
		 { Sym.tokenizers_infix =
			ins [] (Sym.tokenize2 "&" (Sym.infixR 0) Sym.Token_Term_App) $
			del [] "$" $
			Sym.tokenizers_infix mods
		 }
	-}
	print mods
	(lr, ctx_tks) <-
		S.runState mods' $
		P.runParserT (Gram.unCF $ Sym.g_term <* Gram.eoi) "" inp
	case lr of
	 Left (err::P.ParseError (P.Token Text) P.Dec) -> error $ P.parseErrorPretty err
	 Right to -> return to
	where
	del m n      = Map.adjust (Map.delete n) m
	ins m (n, a) = Map.insertWith (<>) m (Map.singleton n a)

compile :: Sym.EToken LCC.Meta SS -> IO (Sym.TermVT SRC SS)
compile to = do
	case Sym.compileWithoutCtx to of
	 Left err -> error $ show err
	 Right te -> return te

-- Sym.Tokenizers
type instance MC.CanDo (S.StateT (Sym.Tokenizers LCC.Meta is) m)
                       (MC.EffState (Sym.Tokenizers LCC.Meta is)) = 'True
instance Monad m => MC.MonadStateN 'MC.Zero (Sym.Tokenizers LCC.Meta is) (S.StateT (Sym.Tokenizers LCC.Meta is) m) where
	stateN _px = S.StateT . g.state
-}