{-# LANGUAGE CPP #-}

module Agda.Interaction.CommandLine.CommandLine where

import Control.Monad.Error
import Control.Monad.Reader
import Control.Applicative
import Data.Char
import Data.Set as Set
import Data.Map as Map
import Data.List as List
import Data.Maybe
import qualified Agda.Utils.IO.Locale as LocIO

import Agda.Interaction.BasicOps as BasicOps
import Agda.Interaction.Monad

import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Parser
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad
import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Abstract.Pretty

import Text.PrettyPrint

import Agda.TypeChecker
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Monad
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Substitute

import Agda.Utils.Monad
import Agda.Utils.Fresh

#include "../../undefined.h"
import Agda.Utils.Impossible

data ExitCode a = Continue | ContinueIn TCEnv | Return a

type Command a = (String, [String] -> TCM (ExitCode a))

matchCommand :: String -> [Command a] -> Either [String] ([String] -> TCM (ExitCode a))
matchCommand x cmds =
    case List.filter (isPrefixOf x . fst) cmds of
	[(_,m)]	-> Right m
	xs	-> Left $ List.map fst xs

interaction :: String -> [Command a] -> (String -> TCM (ExitCode a)) -> IM a
interaction prompt cmds eval = loop
    where
	go (Return x)	    = return x
	go Continue	    = loop
	go (ContinueIn env) = local (const env) loop

	loop =
	    do	ms <- readline prompt
		case fmap words ms of
		    Nothing		  -> return $ error "** EOF **"
		    Just []		  -> loop
		    Just ((':':cmd):args) ->
			do  case matchCommand cmd cmds of
				Right c	-> go =<< liftTCM (c args)
				Left []	->
				    do	liftIO $ LocIO.putStrLn $ "Unknown command '" ++ cmd ++ "'"
					loop
				Left xs	->
				    do	liftIO $ LocIO.putStrLn $ "More than one command match: " ++ concat (intersperse ", " xs)
					loop
		    Just _ ->
			do  go =<< liftTCM (eval $ fromJust ms)
	    `catchError` \e ->
		do  s <- prettyError e
		    liftIO $ LocIO.putStrLn s
		    loop

-- | The interaction loop.
interactionLoop :: TCM (Maybe Interface) -> IM ()
interactionLoop typeCheck =
    do  liftTCM reload
	interaction "Main> " commands evalTerm
    where
	reload = do
	    mi <- typeCheck
            -- Note that mi is Nothing if (1) there is no input file or
            -- (2) the file type checked with unsolved metas and
            -- --allow-unsolved-metas was used. In the latter case the
            -- behaviour of agda -I may be surprising. If agda -I ever
            -- becomes properly supported again, then this behaviour
            -- should perhaps be fixed.
            setScope $ case mi of
              Just i  -> iInsideScope i
              Nothing -> emptyScopeInfo
	  `catchError` \e -> do
	    s <- prettyError e
	    liftIO $ LocIO.putStrLn s
	    liftIO $ LocIO.putStrLn "Failed."

	commands =
	    [ "quit"	    |>  \_ -> return $ Return ()
	    , "?"	    |>  \_ -> continueAfter $ liftIO $ help commands
	    , "reload"	    |>  \_ -> do reload
					 ContinueIn <$> ask
	    , "constraints" |> \args -> continueAfter $ showConstraints args
	    , "Context"	    |> \args -> continueAfter $ showContext args
            , "give"	    |> \args -> continueAfter $ giveMeta args
            , "Refine"	    |> \args -> continueAfter $ refineMeta args
	    , "metas"	    |> \args -> continueAfter $ showMetas args
            , "load"	    |> \args -> continueAfter $ loadFile reload args
	    , "eval"	    |> \args -> continueAfter $ evalIn args
            , "typeOf"      |> \args -> continueAfter $ typeOf args
            , "typeIn"      |> \args -> continueAfter $ typeIn args
	    , "wakeup"	    |> \_ -> continueAfter $ retryConstraints
	    , "scope"	    |> \_ -> continueAfter $ showScope
	    ]
	    where
		(|>) = (,)

continueAfter :: TCM a -> TCM (ExitCode b)
continueAfter m = m >> return Continue

loadFile :: TCM () -> [String] -> TCM ()
loadFile reload [file] =
    do	setInputFile file
	reload
loadFile _ _ = liftIO $ LocIO.putStrLn ":load file"

showConstraints :: [String] -> TCM ()
showConstraints [c] =
    do	i  <- readM c
	cc <- normalise =<< lookupConstraint i
	d  <- prettyTCM $ clValue cc
	liftIO $ LocIO.print d
showConstraints [] =
    do	cs <- BasicOps.getConstraints
	liftIO $ LocIO.putStrLn $ unlines (List.map show cs)
showConstraints _ = liftIO $ LocIO.putStrLn ":constraints [cid]"


showMetas :: [String] -> TCM ()
showMetas [m] =
    do	i <- InteractionId <$> readM m
	withInteractionId i $ do
	  s <- typeOfMeta AsIs i
	  r <- getInteractionRange i
	  d <- showA s
	  liftIO $ LocIO.putStrLn $ d ++ " " ++ show r
showMetas [m,"normal"] =
    do	i <- InteractionId <$> readM m
	withInteractionId i $ do
	  s <- showA =<< typeOfMeta Normalised i
	  r <- getInteractionRange i
	  liftIO $ LocIO.putStrLn $ s ++ " " ++ show r
showMetas [] =
    do  (interactionMetas,hiddenMetas) <- typeOfMetas AsIs
        mapM_ (liftIO . LocIO.putStrLn) =<< mapM showII interactionMetas
	mapM_ print' hiddenMetas
    where
	showII o = withInteractionId (outputFormId o) $ showA o
	showM  o = withMetaId (outputFormId o) $ showA o

	metaId (OfType i _) = i
	metaId (JustType i) = i
	metaId (JustSort i) = i
	metaId (Assign i e) = i
	metaId _ = __IMPOSSIBLE__
	print' x = do
	    r <- getMetaRange (metaId x)
	    d <- showM x
	    liftIO $ LocIO.putStrLn $ d ++ "  [ at " ++ show r ++ " ]"
showMetas _ = liftIO $ LocIO.putStrLn $ ":meta [metaid]"


showScope :: TCM ()
showScope = do
  scope <- getScope
  liftIO $ LocIO.print scope

metaParseExpr ::  InteractionId -> String -> TCM A.Expr
metaParseExpr ii s =
    do	m <- lookupInteractionId ii
        scope <- getMetaScope <$> lookupMeta m
        r <- getRange <$> lookupMeta m
        --liftIO $ LocIO.putStrLn $ show scope
        let pos = case rStart r of
                    Nothing  -> __IMPOSSIBLE__
                    Just pos -> pos
	e <- liftIO $ parsePosString exprParser pos s
	concreteToAbstract scope e

actOnMeta :: [String] -> (InteractionId -> A.Expr -> TCM a) -> TCM a
actOnMeta (is:es) f =
     do  i <- readM is
         let ii = InteractionId i
         e <- metaParseExpr ii (unwords es)
         withInteractionId ii $ f ii e
actOnMeta _ _ = __IMPOSSIBLE__


giveMeta :: [String] -> TCM ()
giveMeta s | length s >= 2 =
    do  actOnMeta s (\ii -> \e  -> give ii Nothing e)
        return ()
giveMeta _ = liftIO $ LocIO.putStrLn $ ": give" ++ " metaid expr"



refineMeta :: [String] -> TCM ()
refineMeta s | length s >= 2 =
    do  actOnMeta s (\ii -> \e  -> refine ii Nothing e)
        return ()
refineMeta _ = liftIO $ LocIO.putStrLn $ ": refine" ++ " metaid expr"



retryConstraints :: TCM ()
retryConstraints = liftTCM wakeupConstraints


evalIn :: [String] -> TCM ()
evalIn s | length s >= 2 =
    do	d <- actOnMeta s $ \_ e -> prettyA =<< evalInCurrent e
        liftIO $ LocIO.print d
evalIn _ = liftIO $ LocIO.putStrLn ":eval metaid expr"

parseExpr :: String -> TCM A.Expr
parseExpr s = do
    e <- liftIO $ parse exprParser s
    localToAbstract e return

evalTerm :: String -> TCM (ExitCode a)
evalTerm s =
    do	e <- parseExpr s
        v <- evalInCurrent e
	e <- prettyTCM v
	liftIO $ LocIO.putStrLn $ show e
	return Continue
    where
	evalInCurrent e = do
	  t <- newTypeMeta_
	  v <- checkExpr e t
	  v' <- normalise v
	  return v'


typeOf :: [String] -> TCM ()
typeOf s =
    do  e  <- parseExpr (unwords s)
        e0 <- typeInCurrent Normalised e
        e1 <- typeInCurrent AsIs e
	liftIO . LocIO.putStrLn =<< showA e1

typeIn :: [String] -> TCM ()
typeIn s@(_:_:_) =
    actOnMeta s $ \i e ->
    do	e1  <- typeInMeta i Normalised e
        e2 <- typeInMeta i AsIs e
	liftIO . LocIO.putStrLn =<< showA e1
typeIn _ = liftIO $ LocIO.putStrLn ":typeIn meta expr"

showContext :: [String] -> TCM ()
showContext (meta:args) = do
    i <- InteractionId <$> readM meta
    mi <- lookupMeta =<< lookupInteractionId i
    withMetaInfo (getMetaInfo mi) $ do
    ctx <- List.map unArg . telToList <$> getContextTelescope
    zipWithM_ display ctx $ reverse $ zipWith const [1..] ctx
    where
	display (x, t) n = do
	    t <- case args of
		    ["normal"] -> normalise $ raise n t
		    _	       -> return $ raise n t
	    d <- prettyTCM t
	    liftIO $ LocIO.print $ text x <+> text ":" <+> d
showContext _ = liftIO $ LocIO.putStrLn ":Context meta"

-- | The logo that prints when Agda is started in interactive mode.
splashScreen :: String
splashScreen = unlines
    [ "                 _ "
    , "   ____         | |"
    , "  / __ \\        | |"
    , " | |__| |___  __| | ___"
    , " |  __  / _ \\/ _  |/ __\\     Agda Interactive"
    , " | |  |/ /_\\ \\/_| / /_| \\"
    , " |_|  |\\___  /____\\_____/    Type :? for help."
    , "        __/ /"
    , "        \\__/"
    , ""
    , "The interactive mode is no longer supported. Don't complain if it doesn't work."
    ]

-- | The help message
help :: [Command a] -> IO ()
help cs = LocIO.putStr $ unlines $
    [ "Command overview" ] ++ List.map explain cs ++
    [ "<exp> Infer type of expression <exp> and evaluate it." ]
    where
	explain (x,_) = ":" ++ x