{-# 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 (($))
import Data.Functor ((<$>))
-- import Data.Maybe (Maybe(..))
-- import Data.Semigroup ((<>))
-- import Data.Text (Text)
import System.IO (IO, stdout, stderr)
import Text.Show (Show(..))
import qualified Data.Strict as S
-- 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 qualified Language.Symantic.Document as Doc
-- 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 (showParseError)
-- import Hcompta.LCC.Grammar
import Hcompta.LCC.Read
import Hcompta.LCC.Document

-- 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 ->
		readCompta @SRC @SS arg >>= \case
		 Left (Error_Read_Syntax err) ->
			showParseError err >>=
			(`Doc.ansiIO` stderr)
		 Left (Error_Read_Semantic err) -> error $ show err
		 Right r -> do
			-- 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

{-
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 = importModulesAs [] 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
-}