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

import Control.Monad (Monad(..), forM_, (=<<))
import Data.Eq (Eq)
import Data.Typeable (Typeable)
import Data.Either (Either(..))
import Data.Function (($))
import Data.Functor ((<$>))
import Data.List.NonEmpty (NonEmpty)
import System.IO (IO, stdout, stderr, print)
import Text.Show (Show(..))
import qualified Data.Strict as S
import qualified System.Environment as Env

import qualified Language.Symantic.Document as Doc
import qualified Language.Symantic as Sym

import qualified Hcompta.LCC.Sym as LCC.Sym
import Hcompta.LCC.Megaparsec (showParseError)
import Hcompta.LCC.Posting (SourcePos)
import Hcompta.LCC.Read
import Hcompta.LCC.Document
import Hcompta.LCC.Compta
import Hcompta.LCC.Source
import Hcompta.LCC.Sym.Compta ()

import Prelude (error)

type SS  = LCC.Sym.SS'

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

{-
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
-}