{-# LANGUAGE CPP, TypeSynonymInstances #-}
{-# OPTIONS -fno-cse #-}

module Agda.Interaction.GhciTop
  ( module Agda.Interaction.GhciTop
  , module Agda.TypeChecker
  , module Agda.TypeChecking.MetaVars
  , module Agda.TypeChecking.Reduce
  , module Agda.TypeChecking.Errors

  , module Agda.Syntax.Position
  , module Agda.Syntax.Parser
--  , module SC  -- trivial clash removal: remove all!
--  , module SA
--  , module SI
  , module Agda.Syntax.Scope.Base
  , module Agda.Syntax.Scope.Monad
  , module Agda.Syntax.Translation.ConcreteToAbstract
  , module Agda.Syntax.Translation.AbstractToConcrete
  , module Agda.Syntax.Translation.InternalToAbstract
  , module Agda.Syntax.Abstract.Name

  , module Agda.Interaction.Exceptions

  , mkAbsolute
  )
  where

import System.Directory
import qualified System.IO as IO
import System.IO.Unsafe
import Data.Char
import Data.Maybe
import Data.IORef
import Data.Function
import Control.Applicative

import Agda.Utils.Fresh
import Agda.Utils.Monad
import Agda.Utils.Pretty as P
import Agda.Utils.String
import Agda.Utils.FileName
import Agda.Utils.Tuple
import qualified Agda.Utils.IO.Locale as LocIO
import qualified Agda.Utils.IO.UTF8 as UTF8

import Control.Monad.Error
import Control.Monad.Reader
import Control.Monad.State hiding (State)
import Control.Exception
import Data.List as List
import qualified Data.Map as Map
import System.Exit
import qualified System.Mem as System
import System.Time
import Text.PrettyPrint

import Agda.TypeChecker
import Agda.TypeChecking.Monad as TM
  hiding (initState, setCommandLineOptions)
import qualified Agda.TypeChecking.Monad as TM
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Serialise (encodeFile)

import Agda.Syntax.Position
import Agda.Syntax.Parser
import qualified Agda.Syntax.Parser.Tokens as T
import Agda.Syntax.Concrete as SC
import Agda.Syntax.Common as SCo
import Agda.Syntax.Concrete.Name as CN
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Abstract as SA
import Agda.Syntax.Abstract.Pretty
import Agda.Syntax.Internal as SI
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad hiding (bindName, withCurrentModule)
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.Syntax.Translation.AbstractToConcrete hiding (withScope)
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Abstract.Name

import Agda.Interaction.Exceptions
import Agda.Interaction.FindFile
import Agda.Interaction.Options
import Agda.Interaction.MakeCase
import qualified Agda.Interaction.BasicOps as B
import qualified Agda.Interaction.CommandLine.CommandLine as CL
import Agda.Interaction.Highlighting.Emacs
import Agda.Interaction.Highlighting.Generate
import qualified Agda.Interaction.Imports as Imp

import Agda.Termination.TermCheck

import qualified Agda.Compiler.MAlonzo.Compiler as MAlonzo

import qualified Agda.Auto.Auto as Auto

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

data State = State
  { theTCState           :: TCState
  , theInteractionPoints :: [InteractionId]
    -- ^ The interaction points of the buffer, in the order in which
    --   they appear in the buffer. The interaction points are
    --   recorded in 'theTCState', but when new interaction points are
    --   added by give or refine Agda does not ensure that the ranges
    --   of later interaction points are updated.
  , theCurrentFile       :: Maybe (AbsolutePath, ClockTime)
    -- ^ The file which the state applies to. Only stored if the
    -- module was successfully type checked (potentially with
    -- warnings). The 'ClockTime' is the modification time stamp of
    -- the file when it was last loaded.
  }

initState :: State
initState = State
  { theTCState           = TM.initState
  , theInteractionPoints = []
  , theCurrentFile       = Nothing
  }

{-# NOINLINE theState #-}
theState :: IORef State
theState = unsafePerformIO $ newIORef initState

-- | An interactive computation.

data Interaction = Interaction
  { isIndependent :: Bool
    -- ^ Can the command run even if the relevant file has not been
    -- loaded into the state?
  , command :: TCM (Maybe ModuleName)
    -- ^ If a module name is returned, then syntax highlighting
    -- information will be written for the given module (by 'ioTCM').
  }

-- | Run a TCM computation in the current state. Should only
--   be used for debugging.
ioTCM_ :: TCM a -> IO a
ioTCM_ m = do
  tcs <- readIORef theState
  Right (x, s) <- runTCM $ do
    put $ theTCState tcs
    x <- withEnv initEnv m
    s <- get
    return (x, s)
  writeIORef theState $ tcs { theTCState = s }
  return x

-- | Runs a 'TCM' computation. All calls from the Emacs mode should be
-- wrapped in this function.

ioTCM :: FilePath
         -- ^ The current file. If this file does not match
         -- 'theCurrentFile', and the 'Interaction' is not
         -- \"independent\", then an error is raised.
      -> Maybe FilePath
         -- ^ Syntax highlighting information will be written to this
         -- file, if any.
      -> Interaction
      -> IO ()
ioTCM current highlightingFile cmd = infoOnException $ do
#if MIN_VERSION_base(4,2,0)
  -- Ensure that UTF-8 is used for communication with the Emacs mode.
  IO.hSetEncoding IO.stdout IO.utf8
#endif

  current <- absolute current

  -- Read the state.
  State { theTCState     = st
        , theCurrentFile = f
        } <- readIORef theState

  -- Run the computation.
  r <- if not (isIndependent cmd) && Just current /= (fst <$> f) then
         let s = "Error: First load the file." in
         return $ Right $ Left (s, TCErr Nothing $ Exception noRange s)
        else
         runTCM $ catchError (do
             put st
             x  <- withEnv initEnv $ command cmd
             st <- get
             return (Right (x, st))
           ) (\e -> do
             s <- prettyError e
             return (Left (s, e))
           )

  -- Update the state.
  case r of
    Right (Right (m, st')) ->
      modifyIORef theState $ \s ->
        s { theTCState   = st'
          }
    _ | isIndependent cmd ->
      modifyIORef theState $ \s ->
        s { theCurrentFile = Nothing }
    _ -> return ()

  -- Write out syntax highlighting info.
  case highlightingFile of
    Nothing -> return ()
    Just f  -> do
      let errHi e s = errHighlighting e
                        `mplus`
                      ((\h -> (h, Map.empty)) <$>
                           generateErrorInfo (getRange e) s)
      UTF8.writeFile f $
        showHighlightingInfo $
          case r of
            Right (Right (mm, st')) -> do
              m  <- mm
              mi <- Map.lookup (SA.toTopLevelModuleName m)
                               (stVisitedModules st')
              return ( iHighlighting $ miInterface mi
                     , stModuleToSource st'
                     )
            Right (Left (s, e)) -> errHi e (Just s)
            Left e              -> errHi e Nothing

  -- If an error was encountered, display an error message and exit
  -- with an error code.
  let errStatus = Status { sChecked               = False
                         , sShowImplicitArguments =
                             optShowImplicit $ stPragmaOptions st
                         }
  case r of
    Right (Right _)     -> return ()
    Right (Left (s, e)) -> displayErrorAndExit errStatus (getRange e) s
    Left e              -> displayErrorAndExit errStatus (getRange e) $
                             tcErrString e

-- | @cmd_load m includes@ loads the module in file @m@, using
-- @includes@ as the include directories.

cmd_load :: FilePath -> [FilePath] -> Interaction
cmd_load m includes =
  cmd_load' m includes True (\_ -> command cmd_metas >> return ())

-- | @cmd_load' m includes cmd cmd2@ loads the module in file @m@,
-- using @includes@ as the include directories.
--
-- If type checking completes without any exceptions having been
-- encountered then the command @cmd r@ is executed, where @r@ is the
-- result of 'Imp.typeCheck'.

cmd_load' :: FilePath -> [FilePath]
          -> Bool -- ^ Allow unsolved meta-variables?
          -> ((Interface, Maybe Imp.Warnings) -> TCM ())
          -> Interaction
cmd_load' file includes unsolvedOK cmd = Interaction True $ do
  -- Forget the previous "current file" and interaction points.
  liftIO $ modifyIORef theState $ \s ->
    s { theInteractionPoints = []
      , theCurrentFile       = Nothing
      }

  f <- liftIO $ absolute file
  t <- liftIO $ getModificationTime file

  -- All options are reset when a file is reloaded, including the
  -- choice of whether or not to display implicit arguments.
  oldIncs <- getIncludeDirs
  setCommandLineOptions $
    defaultOptions { optAllowUnsolved = unsolvedOK
                   , optIncludeDirs   = includes
                   }

  -- Reset the state, preserving options and decoded modules. Note
  -- that Imp.typeCheck resets the decoded modules if the include
  -- directories have changed.
  preserveDecodedModules resetState

  ok <- Imp.typeCheck file Imp.ProjectRoot (Just oldIncs)

  -- The module type checked. If the file was not changed while the
  -- type checker was running then the interaction points and the
  -- "current file" are stored.
  t' <- liftIO $ getModificationTime file
  when (t == t') $ do
    is <- sortInteractionPoints =<< getInteractionPoints
    liftIO $ modifyIORef theState $ \s ->
      s { theInteractionPoints = is
        , theCurrentFile       = Just (f, t)
        }

  cmd ok

  liftIO System.performGC

  return $ Just $ iModuleName (fst ok)

-- | @cmd_compile m includes@ compiles the module in file @m@, using
-- @includes@ as the include directories.

cmd_compile :: FilePath -> [FilePath] -> Interaction
cmd_compile file includes =
  cmd_load' file includes False (\(i, mw) ->
    case mw of
      Nothing -> do
        MAlonzo.compilerMain i
        display_info "*Compilation result*"
                   "The module was successfully compiled."
      Just w ->
        display_info errorTitle $ unlines
          [ "You can only compile modules without unsolved metavariables"
          , "or termination checking problems."
          ])

cmd_constraints :: Interaction
cmd_constraints = Interaction False $ do
    cs <- map show <$> B.getConstraints
    display_info "*Constraints*" (unlines cs)
    return Nothing

-- Show unsolved metas. If there are no unsolved metas but unsolved constraints
-- show those instead.
cmd_metas :: Interaction
cmd_metas = Interaction False $ do -- CL.showMetas []
  ims <- fst <$> B.typeOfMetas B.AsIs
  hms <- snd <$> B.typeOfMetas B.Normalised -- show unsolved implicit arguments normalised
  if not $ null ims && null hms
    then do
      di <- mapM (\i -> B.withInteractionId (B.outputFormId i) (showA i)) ims
      dh <- mapM showA' hms
      display_info "*All Goals*" $ unlines $ di ++ dh
      return Nothing
    else do
      cs <- B.getConstraints
      if null cs
        then display_info "*All Goals*" "" >> return Nothing
        else command cmd_constraints
  where
    metaId (B.OfType i _) = i
    metaId (B.JustType i) = i
    metaId (B.JustSort i) = i
    metaId (B.Assign i e) = i
    metaId _ = __IMPOSSIBLE__
    showA' m = do
      r <- getMetaRange (metaId m)
      d <- B.withMetaId (B.outputFormId m) (showA m)
      return $ d ++ "  [ at " ++ show r ++ " ]"

cmd_reset :: Interaction
cmd_reset = Interaction True $ do
  preserveDecodedModules resetState
  return Nothing

type GoalCommand = InteractionId -> Range -> String -> Interaction

cmd_give :: GoalCommand
cmd_give = give_gen B.give $ \s ce -> case ce of (SC.Paren _ _)-> "'paren"
                                                 _             -> "'no-paren"

cmd_refine :: GoalCommand
cmd_refine = give_gen B.refine $ \s -> quote . show

give_gen give_ref mk_newtxt ii rng s = Interaction False $ do
  scope     <- getInteractionScope ii
  (ae, iis) <- give_ref ii Nothing =<< B.parseExprIn ii rng s
  let newtxt = A . mk_newtxt s $ abstractToConcrete (makeEnv scope) ae
  iis       <- sortInteractionPoints iis
  liftIO $ modifyIORef theState $ \s ->
             s { theInteractionPoints =
                   replace ii iis (theInteractionPoints s) }
  liftIO $ LocIO.putStrLn $ response $
             L [A "agda2-give-action", showNumIId ii, newtxt]
  command cmd_metas
  return Nothing
  where
  -- Substitutes xs for x in ys.
  replace x xs ys = concatMap (\y -> if y == x then xs else [y]) ys

cmd_intro :: GoalCommand
cmd_intro ii rng _ = Interaction False $ do
  ss <- B.introTactic ii
  B.withInteractionId ii $ case ss of
    []    -> do
      display_infoD "*Intro*" $ text "No introduction forms found."
      return Nothing
    [s]   -> command $ cmd_refine ii rng s
    _:_:_ -> do
      display_infoD "*Intro*" $
        sep [ text "Don't know which constructor to introduce of"
            , let mkOr []     = []
                  mkOr [x, y] = [text x <+> text "or" <+> text y]
                  mkOr (x:xs) = text x : mkOr xs
              in nest 2 $ fsep $ punctuate comma (mkOr ss)
            ]
      return Nothing

cmd_refine_or_intro :: GoalCommand
cmd_refine_or_intro ii rng s =
  (if null s then cmd_intro else cmd_refine) ii rng s

cmd_auto :: GoalCommand
cmd_auto ii rng s = Interaction False $ do
  (xs, msg) <- Auto.auto ii rng s
  mapM_ (\(ii, s) -> do
    liftIO $ modifyIORef theState $ \s ->
      s { theInteractionPoints = filter (/= ii) (theInteractionPoints s) }
    liftIO $ LocIO.putStrLn $ response $ L [A "agda2-give-action", showNumIId ii, A $ quote s]
   ) xs
  case msg of
   Nothing -> command cmd_metas >> return ()
   Just msg -> display_info "*Auto*" msg
  return Nothing

-- | Sorts interaction points based on their ranges.

sortInteractionPoints :: [InteractionId] -> TCM [InteractionId]
sortInteractionPoints is =
  map fst . sortBy (compare `on` snd) <$>
    mapM (\i -> (,) i <$> getInteractionRange i) is

-- | Pretty-prints the type of the meta-variable.

prettyTypeOfMeta :: B.Rewrite -> InteractionId -> TCM Doc
prettyTypeOfMeta norm ii = do
  form <- B.typeOfMeta norm ii
  case form of
    B.OfType _ e -> prettyA e
    _            -> text <$> showA form

-- | Pretty-prints the context of the given meta-variable.

prettyContext
  :: B.Rewrite      -- ^ Normalise?
  -> InteractionId
  -> TCM Doc
prettyContext norm ii = B.withInteractionId ii $ do
  ctx <- B.contextOfMeta ii norm
  es  <- mapM (prettyA . B.ofExpr) ctx
  ns  <- mapM (showA   . B.ofName) ctx
  let maxLen = maximum $ 0 : filter (< longNameLength) (map length ns)
  return $ vcat $
           map (\(n, e) -> text n $$ nest (maxLen + 1) (text ":") <+> e) $
           zip ns es

-- | 'prettyContext' lays out @n : e@ on (at least) two lines if @n@
-- has at least @longNameLength@ characters.

longNameLength = 10

cmd_context :: B.Rewrite -> GoalCommand
cmd_context norm ii _ _ = Interaction False $ do
  display_infoD "*Context*" =<< prettyContext norm ii
  return Nothing

cmd_infer :: B.Rewrite -> GoalCommand
cmd_infer norm ii rng s = Interaction False $ do
  display_infoD "*Inferred Type*"
    =<< B.withInteractionId ii
          (prettyA =<< B.typeInMeta ii norm =<< B.parseExprIn ii rng s)
  return Nothing

cmd_goal_type :: B.Rewrite -> GoalCommand
cmd_goal_type norm ii _ _ = Interaction False $ do
  s <- B.withInteractionId ii $ prettyTypeOfMeta norm ii
  display_infoD "*Current Goal*" s
  return Nothing

-- | Displays the current goal and context plus the given document.

cmd_goal_type_context_and doc norm ii _ _ = do
  goal <- B.withInteractionId ii $ prettyTypeOfMeta norm ii
  ctx  <- prettyContext norm ii
  display_infoD "*Goal type etc.*"
                (ctx $+$
                 text (replicate 60 '\x2014') $+$
                 text "Goal:" <+> goal $+$
                 doc)
  return Nothing

-- | Displays the current goal and context.

cmd_goal_type_context :: B.Rewrite -> GoalCommand
cmd_goal_type_context norm ii rng s = Interaction False $
  cmd_goal_type_context_and P.empty norm ii rng s

-- | Displays the current goal and context /and/ infers the type of an
-- expression.

cmd_goal_type_context_infer :: B.Rewrite -> GoalCommand
cmd_goal_type_context_infer norm ii rng s = Interaction False $ do
  typ <- B.withInteractionId ii $
           prettyA =<< B.typeInMeta ii norm =<< B.parseExprIn ii rng s
  cmd_goal_type_context_and (text "Have:" <+> typ) norm ii rng s

-- | Sets the command line options and updates the status information.

setCommandLineOptions :: CommandLineOptions -> TCM ()
setCommandLineOptions opts = do
  TM.setCommandLineOptions PersistentOptions opts
  liftIO . displayStatus =<< status

-- | Status information.

data Status = Status
  { sShowImplicitArguments :: Bool
    -- ^ Are implicit arguments displayed?
  , sChecked               :: Bool
    -- ^ Has the module been successfully type checked?
  }

-- | Computes some status information.

status :: TCM Status
status = do
  showImpl <- showImplicitArguments

  -- Check if the file was successfully type checked, and has not
  -- changed since. Note: This code does not check if any dependencies
  -- have changed, and uses a time stamp to check for changes.
  cur      <- theCurrentFile <$> liftIO (readIORef theState)
  checked  <- case cur of
    Nothing     -> return False
    Just (f, t) -> do
      t' <- liftIO $ getModificationTime $ filePath f
      case t == t' of
        False -> return False
        True  ->
          not . miWarnings . maybe __IMPOSSIBLE__ id <$>
            (getVisitedModule =<<
               maybe __IMPOSSIBLE__ id .
                 Map.lookup f <$> sourceToModule)

  return $ Status { sShowImplicitArguments = showImpl
                  , sChecked               = checked
                  }

-- | Shows status information.

showStatus :: Status -> String
showStatus s = intercalate "," $ catMaybes [checked, showImpl]
  where
  boolToMaybe b x = if b then Just x else Nothing

  checked  = boolToMaybe (sChecked               s) "Checked"
  showImpl = boolToMaybe (sShowImplicitArguments s) "ShowImplicit"

-- | Displays\/updates status information.

displayStatus :: Status -> IO ()
displayStatus s =
  LocIO.putStrLn $ response $
    L [A "agda2-status-action", A (quote $ showStatus s)]

-- | @display_info' header content@ displays @content@ (with header
-- @header@) in some suitable way.

display_info' :: String -> String -> IO ()
display_info' bufname content =
  LocIO.putStrLn $ response $
    L [ A "agda2-info-action"
      , A (quote bufname)
      , A (quote content)
      ]

-- | @display_info@ does what 'display_info'' does, but additionally
-- displays some status information (see 'status' and
-- 'displayStatus').

display_info :: String -> String -> TCM ()
display_info bufname content = do
  liftIO . displayStatus =<< status
  liftIO $ display_info' bufname content

-- | Like 'display_info', but takes a 'Doc' instead of a 'String'.

display_infoD :: String -> Doc -> TCM ()
display_infoD bufname content = display_info bufname (render content)

-- | Formats a response command.

response :: Lisp String -> String
response l = show (text "agda2_mode_code" <+> pretty l)

-- | Formats a response string.

responseString :: Lisp String -> String
responseString s = response $
  L [A "setq", A "agda2-response", s]

-- | Responds to a query.

respond :: Lisp String -> IO ()
respond = LocIO.putStrLn . responseString

data Lisp a = A a | L [Lisp a] | Q (Lisp a)

instance Pretty a => Pretty (Lisp a) where
  pretty (A a ) = pretty a
  pretty (L xs) = parens (sep (List.map pretty xs))
  pretty (Q x)  = text "'"<>pretty x

instance Pretty String where pretty = text

instance Pretty a => Show (Lisp a) where show = show . pretty

showNumIId = A . tail . show

takenNameStr :: TCM [String]
takenNameStr = do
  xss <- sequence [ List.map (fst . unArg) <$> getContext
                  , Map.keys <$> asks envLetBindings
                  , List.map qnameName . Map.keys . sigDefinitions <$> getSignature
		  ]
  return $ concat [ parts $ nameConcrete x | x <- concat xss]
  where
    parts x = [ s | Id s <- nameParts x ]

refreshStr :: [String] -> String -> ([String], String)
refreshStr taken s = go nameModifiers where
  go (m:mods) = let s' = s ++ m in
                if s' `elem` taken then go mods else (s':taken, s')
  go _        = __IMPOSSIBLE__

nameModifiers = "" : "'" : "''" : [show i | i <-[3..]]

cmd_make_case :: GoalCommand
cmd_make_case ii rng s = Interaction False $ do
  cs <- makeCase ii rng s
  B.withInteractionId ii $ do
    pcs <- mapM prettyA cs
    liftIO $ LocIO.putStrLn $ response $
      L [ A "agda2-make-case-action",
          Q $ L $ List.map (A . quote . renderStyle (style { mode = OneLineMode })) pcs
        ]
  return Nothing

cmd_solveAll :: Interaction
cmd_solveAll = Interaction False $ do
  out <- getInsts
  liftIO $ LocIO.putStrLn $ response $
    L[ A"agda2-solveAll-action" , Q . L $ concatMap prn out]
  return Nothing
  where
  getInsts = mapM lowr =<< B.getSolvedInteractionPoints
    where
      lowr (i, m, e) = do
        mi <- getMetaInfo <$> lookupMeta m
        e <- withMetaInfo mi $ lowerMeta <$> abstractToConcrete_ e
        return (i, e)
  prn (ii,e)= [showNumIId ii, A $ quote $ show e]

class LowerMeta a where lowerMeta :: a -> a
instance LowerMeta SC.Expr where
  lowerMeta = go where
    go e = case e of
      Ident _              -> e
      SC.Lit _             -> e
      SC.QuestionMark _ _  -> preMeta
      SC.Underscore _ _    -> preUscore
      SC.App r e1 ae2      -> case appView e of
        SC.AppView (SC.QuestionMark _ _) _ -> preMeta
        SC.AppView (SC.Underscore   _ _) _ -> preUscore
        _ -> SC.App r (go e1) (lowerMeta ae2)
      SC.WithApp r e es	   -> SC.WithApp r (lowerMeta e) (lowerMeta es)
      SC.Lam r bs e1       -> SC.Lam r (lowerMeta bs) (go e1)
      SC.AbsurdLam r h     -> SC.AbsurdLam r h
      SC.Fun r ae1 e2      -> SC.Fun r (lowerMeta ae1) (go e2)
      SC.Pi tb e1          -> SC.Pi (lowerMeta tb) (go e1)
      SC.Set _             -> e
      SC.Prop _            -> e
      SC.SetN _ _          -> e
      SC.ETel tel          -> SC.ETel (lowerMeta tel)
      SC.Let r ds e1       -> SC.Let r (lowerMeta ds) (go e1)
      Paren r e1           -> case go e1 of
        q@(SC.QuestionMark _ Nothing) -> q
        e2                            -> Paren r e2
      Absurd _          -> e
      As r n e1         -> As r n (go e1)
      SC.Dot r e	-> SC.Dot r (go e)
      SC.RawApp r es	-> SC.RawApp r (lowerMeta es)
      SC.OpApp r x es	-> SC.OpApp r x (lowerMeta es)
      SC.Rec r fs	-> SC.Rec r (List.map (id -*- lowerMeta) fs)
      SC.HiddenArg r e	-> SC.HiddenArg r (lowerMeta e)

instance LowerMeta SC.LamBinding where
  lowerMeta b@(SC.DomainFree _ _) = b
  lowerMeta (SC.DomainFull tb)    = SC.DomainFull (lowerMeta tb)

instance LowerMeta SC.TypedBindings where
  lowerMeta (SC.TypedBindings r h bs) = SC.TypedBindings r h (lowerMeta bs)

instance LowerMeta SC.TypedBinding where
  lowerMeta (SC.TBind r ns e) = SC.TBind r ns (lowerMeta e)
  lowerMeta (SC.TNoBind e)    = SC.TNoBind (lowerMeta e)

instance LowerMeta SC.RHS where
    lowerMeta (SC.RHS e)    = SC.RHS (lowerMeta e)
    lowerMeta  SC.AbsurdRHS = SC.AbsurdRHS

instance LowerMeta SC.Declaration where
  lowerMeta = go where
    go d = case d of
      TypeSig n e1                  -> TypeSig n (lowerMeta e1)
      SC.Field h n e1               -> SC.Field h n (lowerMeta e1)
      FunClause lhs rhs whcl        -> FunClause lhs (lowerMeta rhs) (lowerMeta whcl)
      Data r ind n tel e1 cs        -> Data r ind n
                                         (lowerMeta tel) (lowerMeta e1) (lowerMeta cs)
      SC.Record r n c tel e1 cs     -> SC.Record r n c
                                         (lowerMeta tel) (lowerMeta e1) (lowerMeta cs)
      Infix _ _                     -> d
      Mutual r ds                   -> Mutual r (lowerMeta ds)
      Abstract r ds                 -> Abstract r (lowerMeta ds)
      Private r ds                  -> Private r (lowerMeta ds)
      Postulate r sigs              -> Postulate r (lowerMeta sigs)
      SC.Primitive r sigs           -> SC.Primitive r (lowerMeta sigs)
      SC.Open _ _ _                 -> d
      SC.Import _ _ _ _ _           -> d
      SC.Pragma _                   -> d
      ModuleMacro r n tel e1 op dir -> ModuleMacro r n
                                         (lowerMeta tel) (lowerMeta e1) op dir
      SC.Module r qn tel ds         -> SC.Module r qn (lowerMeta tel) (lowerMeta ds)

instance LowerMeta SC.WhereClause where
  lowerMeta SC.NoWhere		= SC.NoWhere
  lowerMeta (SC.AnyWhere ds)	= SC.AnyWhere $ lowerMeta ds
  lowerMeta (SC.SomeWhere m ds) = SC.SomeWhere m $ lowerMeta ds

instance LowerMeta a => LowerMeta [a] where
  lowerMeta as = List.map lowerMeta as

instance LowerMeta a => LowerMeta (Arg a) where
  lowerMeta aa = fmap lowerMeta aa

instance LowerMeta a => LowerMeta (Named name a) where
  lowerMeta aa = fmap lowerMeta aa


preMeta   = SC.QuestionMark noRange Nothing
preUscore = SC.Underscore   noRange Nothing

cmd_compute :: Bool -- ^ Ignore abstract?
               -> GoalCommand
cmd_compute ignore ii rng s = Interaction False $ do
  e <- B.parseExprIn ii rng s
  d <- B.withInteractionId ii $ do
         let c = B.evalInCurrent e
         v <- if ignore then ignoreAbstractMode c else c
         prettyA v
  display_info "*Normal Form*" (show d)
  return Nothing

-- | Parses and scope checks an expression (using the \"inside scope\"
-- as the scope), performs the given command with the expression as
-- input, and displays the result.

parseAndDoAtToplevel
  :: (SA.Expr -> TCM SA.Expr)
     -- ^ The command to perform.
  -> String
     -- ^ The name to used for the buffer displaying the output.
  -> String
     -- ^ The expression to parse.
  -> Interaction
parseAndDoAtToplevel cmd title s = Interaction False $ do
  e <- liftIO $ parse exprParser s
  display_info title =<< do
    mCurrent <- stCurrentModule <$> get
    case mCurrent of
      Nothing      -> return "Error: First load the file."
      Just current -> do
        r <- getVisitedModule (SA.toTopLevelModuleName current)
        case r of
          Nothing -> __IMPOSSIBLE__
          Just mi -> do
            setScope $ iInsideScope $ miInterface mi
            showA =<< cmd =<< concreteToAbstract_ e
  return Nothing

-- | Parse the given expression (as if it were defined at the
-- top-level of the current module) and infer its type.

cmd_infer_toplevel
  :: B.Rewrite  -- ^ Normalise the type?
  -> String
  -> Interaction
cmd_infer_toplevel norm =
  parseAndDoAtToplevel (B.typeInCurrent norm) "*Inferred Type*"

-- | Parse and type check the given expression (as if it were defined
-- at the top-level of the current module) and normalise it.

cmd_compute_toplevel :: Bool -- ^ Ignore abstract?
                     -> String -> Interaction
cmd_compute_toplevel ignore =
  parseAndDoAtToplevel (if ignore then ignoreAbstractMode . c else c)
                       "*Normal Form*"
  where c = B.evalInCurrent

------------------------------------------------------------------------
-- Syntax highlighting

-- | @cmd_write_highlighting_info source target@ writes syntax
-- highlighting information for the module in @source@ into @target@.
-- If the module does not exist, or its module name is malformed or
-- cannot be determined, or the module has not already been visited,
-- or the cached info is out of date, then the representation of \"no
-- highlighting information available\" is instead written to
-- @target@.

cmd_write_highlighting_info :: FilePath -> FilePath -> Interaction
cmd_write_highlighting_info source target = Interaction True $ do
  liftIO . UTF8.writeFile target . showHighlightingInfo =<< do
    ex <- liftIO $ doesFileExist source
    case ex of
      False -> return Nothing
      True  -> do
        mmi <- (getVisitedModule =<< Imp.moduleName source)
                 `catchError`
               \_ -> return Nothing
        case mmi of
          Nothing     -> return Nothing
          Just mi -> do
            sourceT <- liftIO $ getModificationTime source
            if sourceT <= miTimeStamp mi
             then do
              modFile <- stModuleToSource <$> get
              return $ Just (iHighlighting $ miInterface mi, modFile)
             else
              return Nothing
  return Nothing

-- | Returns the interaction ids for all goals in the current module,
-- in the order in which they appear in the module. If there is no
-- current module, then an empty list of goals is returned.

cmd_goals :: FilePath
             -- ^ If the module name in this file does not match that
             -- of the current module (or the module name cannot be
             -- determined), then an empty list of goals is returned.
          -> Interaction
cmd_goals f = Interaction True $ do
  is <- do
    ex <- liftIO $ doesFileExist f
    case ex of
      False -> return []
      True  -> do
        mm       <- (Just <$> Imp.moduleName f)
                      `catchError`
                    \_ -> return Nothing
        mCurrent <- stCurrentModule <$> get
        if mm == (SA.toTopLevelModuleName <$> mCurrent) then
          theInteractionPoints <$> liftIO (readIORef theState)
         else
          return []
  liftIO $ respond $ Q $ L $ List.map showNumIId is
  return Nothing

-- | Tells the Emacs mode to go to the first error position (if any).

tellEmacsToJumpToError :: Range -> IO ()
tellEmacsToJumpToError r = do
  case rStart r of
    Nothing                                    -> return ()
    Just (Pn { srcFile = Nothing })            -> return ()
    Just (Pn { srcFile = Just f, posPos = p }) ->
      LocIO.putStrLn $ response $
        L [ A "annotation-goto"
          , Q $ L [A (quote $ filePath f), A ".", A (show p)]
          ]

------------------------------------------------------------------------
-- Implicit arguments

-- | Tells Agda whether or not to show implicit arguments.

showImplicitArgs :: Bool -- ^ Show them?
                 -> Interaction
showImplicitArgs showImpl = Interaction False $ do
  opts <- commandLineOptions
  setCommandLineOptions (opts { optShowImplicit = showImpl })
  return Nothing

-- | Toggle display of implicit arguments.

toggleImplicitArgs :: Interaction
toggleImplicitArgs = Interaction False $ do
  opts <- commandLineOptions
  setCommandLineOptions (opts { optShowImplicit =
                                  not $ optShowImplicit opts })
  return Nothing

------------------------------------------------------------------------
-- Error handling

-- | When an error message is displayed the following title should be
-- used, if appropriate.

errorTitle :: String
errorTitle = "*Error*"

-- | Displays an error, instructs Emacs to jump to the site of the
-- error, and terminates the program. Because this function may switch
-- the focus to another file the status information is also updated.

displayErrorAndExit :: Status
                       -- ^ The new status information.
                    -> Range -> String -> IO a
displayErrorAndExit status r s = do
  display_info' errorTitle s
  tellEmacsToJumpToError r
  displayStatus status
  exitWith (ExitFailure 1)

-- | Outermost error handler.

infoOnException m =
  failOnException (displayErrorAndExit s) m `catchImpossible` \e ->
    displayErrorAndExit s noRange (show e)
  where
  s = Status { sChecked               = False
             , sShowImplicitArguments = False
               -- Educated guess... This field is not important, so it
               -- does not really matter if it is displayed
               -- incorrectly when an unexpected error has occurred.
             }