{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Main where

import Control.Arrow (left)
import Control.Applicative (Applicative(..))
import Control.Monad (Monad(..), void, when)
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.Trans.Class as MT (MonadTrans(..))
import Data.Bool (Bool(..))
import Data.Char (Char)
import Data.Either (Either(..))
import Data.Eq (Eq(..))
import Data.Function (($), (.), id)
import Data.Functor (Functor(..), (<$>))
import Data.Maybe (Maybe(..), maybe)
import Data.Monoid (Monoid(..))
import Data.Semigroup ((<>))
import Data.String (String)
import Data.Text (Text)
import Prelude (error, succ, Integer, undefined)
import System.Console.Haskeline as HL
import System.IO (IO, putStr, putStrLn, print)
import Text.Show (Show(..))
import qualified Control.Monad.Classes as MC
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.Console.Haskeline.History as HL
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 qualified Hcompta.LCC.Lib.Strict as S
import Hcompta.LCC.Read ()
import Hcompta.LCC.Write (Writeable(..), context_write)

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

main :: IO ()
main = do
	runInputT defaultSettings
	 { historyFile    = Just ".hcompta.history"
	 , autoAddHistory = False
	 } $
		MC.evalStateStrict evalTeUnit $
		S.evalState (LCC.state_sym @LCC.Sym.SRC @(Proxy Eval ': LCC.Sym.SS)) $
		unREPL $ loop True 0
	where
	loop :: forall src ss.
	 Show src =>
	 Syms ss Eval =>
	 -- Syms ss View =>
	 -- Syms ss (BetaT View) =>
	 SymInj ss Eval =>
	 ReadTe src ss =>
	 Gram_Term src ss (G src ss (SS.StateT (TermVT src ss '[]) (InputT IO))) =>
	 Bool -> Integer -> REPL src ss ()
	loop ok i = do
		let prompt =
			"\SOH\ESC["
			 <> (if ok then "32" else "31")
			 <> ";1m\STX"
			 <> show i
			 <> "\SOH\ESC[34;1m\STX>\SOH\ESC[0;48;05;233m\STX "
		-- Σ
		line <- readLine prompt
		case line of
		 Nothing -> loop ok i
		 Just l -> do
			void $ REPL $ lift $ lift $
				HL.modifyHistory $
				HL.addHistoryRemovingAllDupes l
			REPL (parseTe $ Text.pack l) >>= \case
			 Left err -> do
				liftIO $ putStr $ P.parseErrorPretty err
				loop False (succ i)
			 Right expr ->
				case expr of
				 Command_Def  nam ast -> runTe nam ast
				 Command_Bind nam ast -> runTe nam ast
				 Command_Eval     ast -> runTe "ans" ast
		where
		runTe nam ast =
			case readTe ast of
			 Left err -> do
				liftIO $ print err
				loop False (succ i)
			 Right te -> do
				REPL $ do
					MC.modify $ \(imps::Imports NameTe, mods) ->
						(imps, insTerm nam te mods)
					lr_r <- evalTe te
					case lr_r of
					 Right r ->
						when (nam == NameTe "base") $ MC.put r
					 Left (Error_Eval_Cannot_prove_Constraint (TypeVT q)) ->
						printTy q >>= ansiIO . ("Cannot prove Constraint: " <>)
				loop True (succ i)
		insTerm ::
		 Sym.NameTe ->
		 Sym.TermVT src ss '[] ->
		 Sym.Modules src ss ->
		 Sym.Modules src ss
		insTerm n t =
			Sym.insertTermVT ([] `Sym.Mod` t) n $
			Sym.Fixity2 Sym.infixN5

type instance MC.CanDo (S.StateT (LCC.State_Sym src ss) m) (MC.EffState (TermVT src ss '[])) = 'False
-- type instance MC.CanDo (S.StateT (LCC.State_Sym src ss) m) (MC.EffState (EvalVT src)) = 'False

-- * Type 'G'
type G src ss m =
 P.ParsecT P.Dec Text
           (S.StateT (LCC.State_Sym src ss) m)

-- * Type 'Command'
data Command src ss
 =   Command_Eval (AST_Term src ss)
 |   Command_Def  NameTe (AST_Term src ss)
 |   Command_Bind NameTe (AST_Term src ss)
 deriving (Eq, Show)

parseTe ::
 forall ss src m.
 Monad m =>
 Gram_Term src ss (G src ss m) =>
 Text ->
 S.StateT (LCC.State_Sym src ss) m
          (Either (P.ParseError Char P.Dec) (Command src ss))
parseTe = P.runParserT g ""
	where
	g :: G src ss m (Command src ss)
	g = G.unCF $
		G.try gCmdLet G.<+>
		G.try gCmdBind G.<+>
		gCmdEval
	gCmdLet =
		Command_Def
		 <$  G.optional (G.try $ G.symbol "let")
		 <*> Sym.g_NameTe
		 <*  G.symbol "="
		 <*> Sym.g_term
		 <*  G.eoi
	gCmdEval =
		Command_Eval
		 <$> Sym.g_term
		 <*  G.eoi
	gCmdBind =
		Command_Bind
		 <$> Sym.g_NameTe
		 <*  G.symbol "<-"
		 <*> Sym.g_term
		 <*  G.eoi

-- * Type 'ReadTe'
type ReadTe src 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
 ) =>
 AST_Term src ss ->
 Either (Error_Term src) (TermVT src ss '[])
readTe = Sym.readTerm CtxTyZ

-- | Lifted 'D.ansiIO' on 'IO.stdout'. Helper.
ansiIO :: MonadIO m => D.ANSI_IO -> m ()
ansiIO = liftIO . (`D.ansiIO` IO.stdout)

-- * Type 'Error_Eval'
data Error_Eval src
 =   Error_Eval_Cannot_prove_Constraint (TypeVT src)
 deriving (Eq, Show)

evalTe ::
 forall src ss m.
 Source src =>
 Syms ss Eval =>
 -- Syms ss View =>
 -- Syms ss (BetaT View) =>
 SymInj ss Eval =>
 SourceInj (TypeVT src) src =>
 MonadIO m =>
 TermVT src ss '[] ->
 S.StateT (LCC.State_Sym src ss)
          (SS.StateT (TermVT src ss '[]) m)
          (Either (Error_Eval src) (TermVT src ss '[]))
evalTe te@(TermVT (Term q t (TeSym sym))) = do
	printTy (q #> t) >>= ansiIO . ("Type: " <>)
	-- liftIO $ Text.putStrLn $ "View: " <> view (betaT $ sym CtxTeZ)
	case t of
	 io:@aTy | Just HRefl <- proj_ConstKiTy @_ @IO io -> do
		case proveConstraint q of
		 Nothing -> return $ Left $ Error_Eval_Cannot_prove_Constraint $ TypeVT q
		 Just Dict -> do
			a <- liftIO $ eval $ sym CtxTeZ
			let r = TermVT $ teEval_uneval aTy a
			printTe aTy a
			return $ Right r
	 _ -> do
		r@(TermVT (Term q' t' (TeSym sym'))) <- completeTe te
		printTy (q' #> t') >>= ansiIO . ("Type: Completed: " <>)
		case proveConstraint q' of
		 Nothing -> return $ Left $ Error_Eval_Cannot_prove_Constraint $ TypeVT q'
		 Just Dict -> do
			let a = eval $ sym' CtxTeZ
			printTe t' a
			return $ Right r

completeTe ::
 forall src ss m.
 Source src =>
 Syms ss Eval =>
 -- Syms ss View =>
 -- Syms ss (BetaT View) =>
 SourceInj (TypeVT src) src =>
 MonadIO m =>
 TermVT src ss '[] ->
 S.StateT (LCC.State_Sym src ss)
          (SS.StateT (TermVT src ss '[]) m)
          (TermVT src ss '[])
completeTe t = do
	liftIO $ putStrLn "completeTe"
	st :: TermVT src ss '[] <- MC.get
	case betaTerms $ G.BinTree0 t `G.BinTree2` G.BinTree0 st of
	 Left _  -> do
		liftIO $ putStrLn "completeTe: Left"
		return t
	 Right s -> do
		liftIO $ putStrLn "completeTe: Right"
		return s

printTy ::
 forall src ss m vs t d.
 Source src =>
 D.Doc_Text d =>
 D.Doc_Color d =>
 MonadIO m =>
 Type src vs t ->
 S.StateT (LCC.State_Sym src ss) m d
printTy ty = do
	(impsTy, _ :: Sym.ModulesTy src) <- MC.get
	return $ Sym.docType
		Sym.config_Doc_Type
		 { config_Doc_Type_vars_numbering = False
		 , config_Doc_Type_imports        = impsTy
		 } 0 ty <> D.eol

printTe :: Source src => MonadIO m => Type src vs a -> a -> m ()
printTe aTy a =
	case proveConstraint $ LCC.Sym.tyWriteable
	 (allocVarsR (lenVars aTy) $ LCC.Sym.tyContext_Write @_ @'[] ~> LCC.Sym.tyANSI_IO) aTy of
	 Just Dict -> ansiIO $ write a context_write
	 Nothing -> liftIO $
		case proveConstraint $ Sym.tyShow aTy of
		 Nothing -> putStrLn $ "No Show instance for type: " <> show aTy
		 Just Dict -> do
			putStrLn "Show:"
			print a


-- * Type 'REPL'
-- /Read Eval Print Loop/ monad.
newtype REPL src ss a
 =      REPL
 {    unREPL :: S.StateT (LCC.State_Sym src ss)
                         (SS.StateT (TermVT src ss '[])
                                    (InputT IO))
                         a }
 deriving ( Functor
          , Applicative
          , Monad
          , MonadIO
          -- , MonadState State_REPL
          )
{-
instance MonadTrans (REPL src ss) where
	lift = REPL . lift . lift
-}
type instance MC.CanDo (REPL src ss) (MC.EffState (LCC.State_Sym src ss))               = 'False
type instance MC.CanDo (REPL src ss) (MC.EffState (Sym.Imports ns, Sym.Modules src ss)) = 'False
type instance MC.CanDo (REPL src ss) (MC.EffState (Sym.Imports ns, Sym.ModulesTy src))  = 'False
type instance MC.CanDo (REPL src ss) (MC.EffState (Sym.TermVT src ss '[]))              = 'False
-- type instance MC.CanDo (REPL src ss) (MC.EffState (EvalVT src))                       = 'False

{-
-- * Type 'State_REPL'
data State_REPL src ss
 =   State_REPL
 {   state_repl_terms :: LCC.State_Sym src ss
 ,   state_repl_db    :: db
 }

-- State_REPL src ss db
type instance MC.CanDo (S.StateT (State_REPL src ss db) m) (MC.EffState (State_REPL src ss db)) = 'True
instance Monad m => MC.MonadStateN 'MC.Zero (State_REPL src ss db) (S.StateT (State_REPL src ss db) m) where
	stateN _px = S.StateT . SS.state

-- LCC.State_Sym src ss
type instance MC.CanDo (S.StateT (State_REPL src ss db) m) (MC.EffState (State_REPL src ss db)) = 'True
instance Monad m => MC.MonadStateN 'MC.Zero (State_REPL src ss db) (S.StateT (LCC.State_Sym src ss) m) where
	stateN _px f = S.StateT $ SS.state $ \st ->
		(\a -> st{state_repl_terms=a}) <$> f (state_repl_terms st)
-}


readLine :: String -> REPL src ss (Maybe String)
readLine prompt = do
	line <- REPL . lift . lift $ getInputLine prompt
	case line of
	 Just l@(':':_) -> return $ Just l
	 Just l@(_:_) | L.last l == ' ' -> readLines l
	 Just l  -> return $ Just l
	 Nothing -> return Nothing
	where
	readLines :: String -> REPL src ss (Maybe String)
	readLines acc = do
		line <- REPL . lift . lift $ getInputLine ""
		case line of
		 Just l@(_:_) | L.last l == ' ' -> readLines $ acc <> l
		 Just l  -> return $ Just $ acc <> l
		 Nothing -> return $ Just acc




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 =>
 PathMod -> NameTe -> d
docPathTe ms (NameTe n) =
	D.catH $
	L.intersperse (D.charH '.') $
	((\(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


{-
mainSym :: IO ()
mainSym = do
	args <- Env.getArgs
	let sym@(LCC.State_Sym (impsTy,_modsTy) (_impsTe,patchModsTe -> modsTe)) =
		LCC.state_sym @LCC.Sym.SRC @LCC.Sym.SS
	(`D.ansiIO` IO.stderr) $ docModules impsTy modsTe
	let arg = Text.unwords $ Text.pack <$> args
	ast <- printError $ parseTe sym arg
	{-
	ast <- (foldr1 G.BinTree2 <$>) $ forM args $ \arg -> do
		printError $ parseTe sym $ Text.pack arg
	-}
	_te <- printError $ readTe ast
	return ()
	{-
	evalTe impsTy te
	forM_ args $ \arg -> do
		ast <- printError $ parseTe (impsTy, modsTy) (impsTe, modsTe) $ Text.pack arg
		te  <- printError $ readTe ast
		evalTe impsTy te
	-}
	where
	patchModsTe = Sym.deleteDefTermInfix ([] `Mod` "$")

printError :: Show err => MonadIO m => Either err a -> m a
printError (Left err) = liftIO $ error $ show err
printError (Right a)  = return a

parseTe ::
 forall ss src m.
 m ~ Identity =>
 Show src =>
 G.Gram_Source src (G src ss m) =>
 Gram_Term src ss (G src ss m) =>
 LCC.State_Sym src ss ->
 Text -> Either (P.ParseError Char P.Dec) (Command src ss)
parseTe sym inp =
	runIdentity $
	S.evalState sym $
	P.runParserT g "" inp
	where
	g :: G src ss Identity (Command src ss)
	g = G.unCF $
		G.try (Command_Def <$> Sym.g_NameTe <* G.lexeme (G.char '=') <*> Sym.g_term <* G.eoi) G.<+>
		(Command_Eval <$> Sym.g_term <* G.eoi)
-}


evalTeUnit :: Source src => SymInj ss () => TermVT src ss '[]
evalTeUnit = TermVT $ Sym.teUnit -- Term noConstraint Sym.tyUnit $ teSym @() $ Sym.unit

{-
evalTeUnit :: Source src => EvalVT src
evalTeUnit = EvalVT (Sym.tyUnit @_ @'[]) $ eval Sym.unit

-- * Type 'EvalVT'
data EvalVT src = forall vs t. EvalVT (Type src vs t) t

appEvalVT ::
 SourceInj (TypeVT src) src =>
 Constable (->) =>
 EvalVT src ->
 EvalVT src ->
 Either (Error_Beta src) (EvalVT src)
appEvalVT (EvalVT tf te_fun) (EvalVT ta te_arg) =
	let (tf',ta') = appendVars tf ta in
	case unTyFun tf' of
	 Nothing -> Left $ Error_Beta_Term_not_a_function $ TypeVT tf'
	 Just (af,_rf) -> do
		mgu <-
			(Error_Beta_Unify `left`) $
			case (unQualsTy af, unQualsTy ta') of
			 (TypeK af', TypeK ta'') -> unifyType mempty af' ta''
		let tf'' = subst mgu tf'
		let ta'' = subst mgu ta'
		appEval tf'' te_fun ta'' te_arg $ \tr te_res ->
			normalizeVarsTy tr $ \tr' ->
				EvalVT tr' te_res

appEval ::
 forall src vs fun arg ret.
 SourceInj (TypeVT src) src =>
 Constable (->) =>
 Type src vs fun -> fun ->
 Type src vs arg -> arg ->
 (forall res. Type src vs res -> res -> ret) ->
 Either (Error_Beta src) ret
appEval tf fun ta arg k =
	case tf of
	 a2b :@ a2b_a :@ a2b_b
		| Just HRefl <- proj_ConstKiTy @(K (->)) @(->) a2b ->
		case a2b_a `eqType` ta of
		 Nothing   -> Left $ Error_Beta_Type_mismatch (TypeVT a2b_a) (TypeVT ta)
		 Just Refl -> Right $ k a2b_b $ fun arg
	 _ -> Left $ Error_Beta_Term_not_a_function $ TypeVT tf
-}



-- * Class 'Sym_Eval'
type instance Sym Eval = Sym_Eval
class Sym_Eval term where
	uneval :: a -> term a
	default uneval :: Sym_Eval (UnT term) => Trans term => a -> term a
	uneval = trans . uneval

-- Interpreting
instance Sym_Eval Eval where
	uneval a = Eval a
{-
instance Sym_Eval View where
	uneval = View $ \_p _v -> "()"
instance (Sym_Eval r1, Sym_Eval r2) => Sym_Eval (Dup r1 r2) where
	uneval = uneval `Dup` uneval
-}

-- Transforming
instance (Sym_Eval term, Sym_Lambda term) => Sym_Eval (BetaT term)

-- Typing
instance NameTyOf Eval where
	nameTyOf _c = [] `Mod` "Eval"
instance ClassInstancesFor Eval where
instance TypeInstancesFor Eval
instance FixityOf Eval

-- Compiling
instance
 ( SymInj ss Eval
 ) => Gram_Term_AtomsFor src ss g Eval where
instance ModuleFor src ss Eval

-- ** 'Type's
tyEval :: Source src => LenInj vs => Type src vs Eval
tyEval = tyConst @(K Eval) @Eval

-- ** 'Term's
teEval_uneval ::
 Source src => SymInj ss Eval =>
 Type src vs a -> a ->
 Term src ss ts vs (() #> a)
teEval_uneval ty a =
	Term (noConstraintLen $ lenVars ty) ty $
	symInj @Eval $
	TeSym $ \_c -> uneval a