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

-- import qualified Control.Monad.Classes as MC
import Control.Monad (Monad(..), forM_)
import Data.Char (Char)
import Data.Either (Either(..))
import Data.Either (either)
import Data.Eq (Eq)
import Data.Function (($), (.), id)
import Data.Maybe (Maybe(..))
import Data.Semigroup ((<>))
import Data.Text (Text)
import System.IO (IO, putStrLn)
import Text.Show (Show(..))
import qualified Control.Monad.Trans.State.Strict as SS
import qualified Data.Text as Text
import qualified Data.Text.IO as Text
import qualified System.Environment as Env
import qualified Text.Megaparsec as P

import Language.Symantic.Grammar
import Language.Symantic as Sym
import qualified Language.Symantic.Lib as Sym

-- import qualified Hcompta.LCC as LCC
import qualified Hcompta.LCC.Sym as LCC.Sym
import Hcompta.LCC.Megaparsec ()

import Control.Applicative (Applicative(..))
import Data.Functor (Functor(..))
import Data.Functor.Identity (Identity(..))
import Data.Proxy (Proxy(..))
import qualified Control.Monad.Classes.Run as MC
import Prelude (error)

type SS = LCC.Sym.SS
type SRC = ()

main :: IO ()
main = do
	args <- Env.getArgs
	forM_ args $ \arg -> do
		ast <- printError $ parseTe @SS @SRC (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

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

readTe ::
 forall src ss.
 ( Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Sym.Imports, Modules src ss) Identity))
 , Syms ss Eval
 , Syms ss View
 , Syms ss (BetaT View)
 , Inj_Modules src ss
 , Eq src
 , Show src
 , Inj_Source (TypeVT src) src
 , Inj_Source (TypeT src '[]) src
 , Inj_Source (KindK src) src
 , Inj_Source (AST_Type src) src
 , Inj_Name2Type ss
 ) =>
 AST_Term src ss ->
 Either (Error_Term src) (TermVT src ss '[])
readTe ast =
	let tys = inj_Name2Type (Proxy @ss) in
	Sym.readTerm tys 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
-}