    {-# LANGUAGE NondecreasingIndentation #-}
    {-# OPTIONS_GHC -fno-cse #-}
    {-# OPTIONS_GHC -fno-warn-orphans #-}

    module Agda.Interaction.InteractionTop
      ( module Agda.Interaction.InteractionTop
      )
      where

    import Prelude hiding (null)

    import Control.Concurrent
    import Control.Concurrent.Async
    import Control.Concurrent.STM.TChan
    import Control.Concurrent.STM.TVar
    import qualified Control.Exception  as E

    import Control.Monad.Except         ( MonadError(..), ExceptT(..), runExceptT )
    import Control.Monad.IO.Class       ( MonadIO(..) )
    import Control.Monad.State          ( MonadState(..), gets, modify, runStateT )
    import Control.Monad.STM
    import Control.Monad.State          ( StateT )

    import qualified Data.Char as Char
    import Data.Function (on)
    import qualified Data.List as List
    import qualified Data.Map as Map
    import qualified Data.Set as Set
    import Data.Maybe

    import System.Directory
    import System.FilePath

    import Agda.TypeChecking.Monad as TCM
    import qualified Agda.TypeChecking.Pretty as TCP
    import Agda.TypeChecking.Errors
    import Agda.TypeChecking.Opacity (saturateOpaqueBlocks)
    import Agda.TypeChecking.Rules.Term (checkExpr, isType_)
    import Agda.TypeChecking.Warnings (warning)

    import Agda.Syntax.Fixity
    import Agda.Syntax.Position
    import Agda.Syntax.Parser
    import Agda.Syntax.Common
    import Agda.Syntax.Concrete as C
    import Agda.Syntax.Concrete.Glyph
    import Agda.Syntax.Abstract as A
    import Agda.Syntax.Abstract.Pretty
    import Agda.Syntax.Info (mkDefInfo)
    import Agda.Syntax.Translation.ConcreteToAbstract
    import Agda.Syntax.Translation.AbstractToConcrete
    import Agda.Syntax.Translation.InternalToAbstract (reify)
    import Agda.Syntax.Scope.Base
    import Agda.Syntax.TopLevelModuleName

    import Agda.Interaction.Base
    import Agda.Interaction.ExitCode (pattern TCMError, exitAgdaWith)
    import Agda.Interaction.FindFile
    import Agda.Interaction.Options
    import Agda.Interaction.Options.Lenses as Lenses
    import Agda.Interaction.MakeCase
    import Agda.Interaction.SearchAbout
    import Agda.Interaction.Response hiding (Function, ExtendedLambda)
    import qualified Agda.Interaction.Response as R
    import qualified Agda.Interaction.BasicOps as B
    import Agda.Interaction.Highlighting.Precise hiding (Error, Postulate, singleton)
    import Agda.Interaction.Imports  ( Mode, pattern ScopeCheck, pattern TypeCheck )
    import qualified Agda.Interaction.Imports as Imp
    import Agda.Interaction.Command
      (CommandM, liftLocalState, revLift, revLiftTC, localStateCommandM)
    import Agda.Interaction.Highlighting.Generate

    import Agda.Compiler.Backend

    import Agda.Mimer.Mimer as Mimer
    import qualified Control.DeepSeq as DeepSeq

    import Agda.Utils.Either
    import Agda.Utils.FileName
    import Agda.Utils.Function
    import Agda.Utils.Hash
    import Agda.Utils.IO (showIOException)
    import Agda.Utils.Lens
    import qualified Agda.Utils.Maybe.Strict as Strict
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Syntax.Common.Pretty hiding (Mode)
    import qualified Agda.Utils.ProfileOptions as Profile
    import Agda.Utils.Singleton
    import Agda.Utils.String
    import Agda.Utils.Time
    import Agda.Utils.Tuple
    import Agda.Utils.WithDefault (lensCollapseDefault, lensKeepDefault)

    import Agda.Utils.Impossible

    -- | Opposite of 'liftIO' for 'CommandM'.
    --
    -- This function should only be applied to computations that are
    -- guaranteed not to raise any errors (except for 'IOException's).

    commandMToIO :: (forall x . (CommandM a -> IO x) -> IO x) -> CommandM a
    commandMToIO :: forall a. (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a
    commandMToIO forall x. (CommandM a -> IO x) -> IO x
    ci_i = (forall c.
     StateT CommandState TCM c -> CommandState -> TCM (c, CommandState))
    -> (forall b. TCM b -> StateT CommandState TCM b)
    -> (forall x. (CommandM a -> TCM x) -> TCM x)
    -> CommandM a
    forall st (m :: * -> *) (k :: * -> *) a.
    MonadState st m =>
    (forall c. m c -> st -> k (c, st))
    -> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
    revLift StateT CommandState TCM c -> CommandState -> TCM (c, CommandState)
    forall c.
    StateT CommandState TCM c -> CommandState -> TCM (c, CommandState)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT TCM b -> StateT CommandState TCM b
    forall b. TCM b -> StateT CommandState TCM b
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift ((forall x. (CommandM a -> TCM x) -> TCM x) -> CommandM a)
    -> (forall x. (CommandM a -> TCM x) -> TCM x) -> CommandM a
    forall a b. (a -> b) -> a -> b
    $ \CommandM a -> TCM x
    ct -> (forall c. TCM c -> TCState -> IO (c, TCState))
    -> (forall b. IO b -> TCM b)
    -> (forall x. (TCM x -> IO x) -> IO x)
    -> TCM x
    forall (m :: * -> *) (k :: * -> *) a.
    MonadTCState m =>
    (forall c. m c -> TCState -> k (c, TCState))
    -> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
    revLiftTC TCM c -> TCState -> IO (c, TCState)
    forall c. TCM c -> TCState -> IO (c, TCState)
    runSafeTCM IO b -> TCM b
    forall b. IO b -> TCM b
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO ((forall x. (TCM x -> IO x) -> IO x) -> TCM x)
    -> (forall x. (TCM x -> IO x) -> IO x) -> TCM x
    forall a b. (a -> b) -> a -> b
    $ (CommandM a -> IO x) -> IO x
    forall x. (CommandM a -> IO x) -> IO x
    ci_i ((CommandM a -> IO x) -> IO x)
    -> ((TCM x -> IO x) -> CommandM a -> IO x)
    -> (TCM x -> IO x)
    -> IO x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((TCM x -> IO x) -> (CommandM a -> TCM x) -> CommandM a -> IO x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CommandM a -> TCM x
    ct)

    -- | Lift a TCM action transformer to a CommandM action transformer.

    liftCommandMT :: (forall x . TCM x -> TCM x) -> CommandM a -> CommandM a
    liftCommandMT :: forall a. (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
    liftCommandMT forall x. TCM x -> TCM x
    f CommandM a
    m = (forall c.
     StateT CommandState TCM c -> CommandState -> TCM (c, CommandState))
    -> (forall b. TCM b -> StateT CommandState TCM b)
    -> (forall x. (CommandM a -> TCM x) -> TCM x)
    -> CommandM a
    forall st (m :: * -> *) (k :: * -> *) a.
    MonadState st m =>
    (forall c. m c -> st -> k (c, st))
    -> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
    revLift StateT CommandState TCM c -> CommandState -> TCM (c, CommandState)
    forall c.
    StateT CommandState TCM c -> CommandState -> TCM (c, CommandState)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT TCM b -> StateT CommandState TCM b
    forall b. TCM b -> StateT CommandState TCM b
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift ((forall x. (CommandM a -> TCM x) -> TCM x) -> CommandM a)
    -> (forall x. (CommandM a -> TCM x) -> TCM x) -> CommandM a
    forall a b. (a -> b) -> a -> b
    $ TCM x -> TCM x
    forall x. TCM x -> TCM x
    f (TCM x -> TCM x)
    -> ((CommandM a -> TCM x) -> TCM x)
    -> (CommandM a -> TCM x)
    -> TCM x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((CommandM a -> TCM x) -> CommandM a -> TCM x
    forall a b. (a -> b) -> a -> b
    $ CommandM a
    m)

    -- | Ditto, but restore state.

    liftCommandMTLocalState :: (forall x . TCM x -> TCM x) -> CommandM a -> CommandM a
    liftCommandMTLocalState :: forall a. (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
    liftCommandMTLocalState forall x. TCM x -> TCM x
    f = (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
    forall a. (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
    liftCommandMT TCM x -> TCM x
    forall x. TCM x -> TCM x
    f (CommandM a -> CommandM a)
    -> (CommandM a -> CommandM a) -> CommandM a -> CommandM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CommandM a -> CommandM a
    forall a. CommandM a -> CommandM a
    localStateCommandM

    -- | Put a response by the callback function given by 'stInteractionOutputCallback'.

    putResponse :: Response -> CommandM ()
    putResponse :: Response -> CommandM ()
    putResponse = TCM () -> CommandM ()
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> CommandM ())
    -> (Response -> TCM ()) -> Response -> CommandM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Response -> TCM ()
    appInteractionOutputCallback

    -- | A Lens for 'theInteractionPoints'.

    modifyTheInteractionPoints :: ([InteractionId] -> [InteractionId]) -> CommandM ()
    modifyTheInteractionPoints :: ([InteractionId] -> [InteractionId]) -> CommandM ()
    modifyTheInteractionPoints [InteractionId] -> [InteractionId]
    f = (CommandState -> CommandState) -> CommandM ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((CommandState -> CommandState) -> CommandM ())
    -> (CommandState -> CommandState) -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ \ CommandState
    s ->
      CommandState
    s { theInteractionPoints = f (theInteractionPoints s) }

    -- * Operations for manipulating 'oldInteractionScopes'.

    -- | A Lens for 'oldInteractionScopes'.
    modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
    modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
    modifyOldInteractionScopes OldInteractionScopes -> OldInteractionScopes
    f = (CommandState -> CommandState) -> CommandM ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((CommandState -> CommandState) -> CommandM ())
    -> (CommandState -> CommandState) -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ \ CommandState
    s ->
      CommandState
    s { oldInteractionScopes = f $ oldInteractionScopes s }

    insertOldInteractionScope :: InteractionId -> ScopeInfo -> CommandM ()
    insertOldInteractionScope :: InteractionId -> ScopeInfo -> CommandM ()
    insertOldInteractionScope InteractionId
    ii ScopeInfo
    scope = do
      TCM () -> CommandM ()
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> CommandM ()) -> TCM () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> String -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "interaction.scope" Int
    20 (String -> TCM ()) -> String -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String
    "inserting old interaction scope " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ InteractionId -> String
    forall a. Show a => a -> String
    show InteractionId
    ii
      (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
    modifyOldInteractionScopes ((OldInteractionScopes -> OldInteractionScopes) -> CommandM ())
    -> (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ InteractionId
    -> ScopeInfo -> OldInteractionScopes -> OldInteractionScopes
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert InteractionId
    ii ScopeInfo
    scope

    removeOldInteractionScope :: InteractionId -> CommandM ()
    removeOldInteractionScope :: InteractionId -> CommandM ()
    removeOldInteractionScope InteractionId
    ii = do
      TCM () -> CommandM ()
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> CommandM ()) -> TCM () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> String -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "interaction.scope" Int
    20 (String -> TCM ()) -> String -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String
    "removing old interaction scope " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ InteractionId -> String
    forall a. Show a => a -> String
    show InteractionId
    ii
      (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
    modifyOldInteractionScopes ((OldInteractionScopes -> OldInteractionScopes) -> CommandM ())
    -> (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> OldInteractionScopes -> OldInteractionScopes
    forall k a. Ord k => k -> Map k a -> Map k a
    Map.delete InteractionId
    ii

    getOldInteractionScope :: InteractionId -> CommandM ScopeInfo
    getOldInteractionScope :: InteractionId -> CommandM ScopeInfo
    getOldInteractionScope InteractionId
    ii = do
      ms <- (CommandState -> Maybe ScopeInfo)
    -> StateT CommandState TCM (Maybe ScopeInfo)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ((CommandState -> Maybe ScopeInfo)
     -> StateT CommandState TCM (Maybe ScopeInfo))
    -> (CommandState -> Maybe ScopeInfo)
    -> StateT CommandState TCM (Maybe ScopeInfo)
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> OldInteractionScopes -> Maybe ScopeInfo
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup InteractionId
    ii (OldInteractionScopes -> Maybe ScopeInfo)
    -> (CommandState -> OldInteractionScopes)
    -> CommandState
    -> Maybe ScopeInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CommandState -> OldInteractionScopes
    oldInteractionScopes
      case ms of
        Maybe ScopeInfo
    Nothing    -> String -> CommandM ScopeInfo
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    String -> m a
    __IMPOSSIBLE_VERBOSE__ (String -> CommandM ScopeInfo) -> String -> CommandM ScopeInfo
    forall a b. (a -> b) -> a -> b
    $ String
    "not an old interaction point: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ InteractionId -> String
    forall a. Show a => a -> String
    show InteractionId
    ii
        Just ScopeInfo
    scope -> ScopeInfo -> CommandM ScopeInfo
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ScopeInfo
    scope

    -- | Do setup and error handling for a command.

    handleCommand_ :: CommandM () -> CommandM ()
    handleCommand_ :: CommandM () -> CommandM ()
    handleCommand_ = (forall a. CommandM a -> CommandM a)
    -> CommandM () -> CommandM () -> CommandM ()
    handleCommand CommandM a -> CommandM a
    forall a. a -> a
    forall a. CommandM a -> CommandM a
    id (() -> CommandM ()
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())

    handleCommand :: (forall a. CommandM a -> CommandM a) -> CommandM () -> CommandM () -> CommandM ()
    handleCommand :: (forall a. CommandM a -> CommandM a)
    -> CommandM () -> CommandM () -> CommandM ()
    handleCommand forall a. CommandM a -> CommandM a
    wrap CommandM ()
    onFail CommandM ()
    cmd = CommandM () -> CommandM ()
    handleNastyErrors (CommandM () -> CommandM ()) -> CommandM () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ CommandM () -> CommandM ()
    forall a. CommandM a -> CommandM a
    wrap (CommandM () -> CommandM ()) -> CommandM () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ do
        oldState <- StateT CommandState TCM TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC

        -- -- Andreas, 2016-11-18 OLD CODE:
        -- -- onFail and handleErr are executed in "new" command state (not TCState).
        -- -- But it seems that if an exception is raised, it is identical to the old state,
        -- -- see code for catchErr.
        -- res <- (`catchErr` (return . Just)) $ Nothing <$ cmd
        -- maybe (return ()) (\ e -> onFail >> handleErr e) res

        -- Andreas, 2016-11-18 NEW CODE: execute onFail and handleErr in handler
        -- which means (looking at catchErr) they run in state s rathern than s'.
        -- Yet, it looks like s == s' in case the command failed.
        cmd `catchErr` \ TCErr
    e -> do
          CommandM ()
    onFail
          Maybe HighlightingMethod -> TCErr -> CommandM ()
    handleErr Maybe HighlightingMethod
    forall a. Maybe a
    Nothing TCErr
    e
          -- Andreas, 2016-11-18, issue #2174
          -- Reset TCState after error is handled, to get rid of metas created during failed command
          TCM () -> CommandM ()
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> CommandM ()) -> TCM () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ do
            newPersistentState <- Lens' TCState PersistentTCState -> TCMT IO PersistentTCState
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
    Lens' TCState PersistentTCState
    lensPersistentState
            putTC oldState
            lensPersistentState `setTCLens` newPersistentState

      where
        -- Preserves state so we can do unsolved meta highlighting
        catchErr :: CommandM a -> (TCErr -> CommandM a) -> CommandM a
        catchErr :: forall a. CommandM a -> (TCErr -> CommandM a) -> CommandM a
    catchErr CommandM a
    m TCErr -> CommandM a
    h = do
          s       <- StateT CommandState TCM CommandState
    forall s (m :: * -> *). MonadState s m => m s
    get
          (x, s') <- lift $ do runStateT m s
             `catchError_` \ TCErr
    e ->
               CommandM a -> CommandState -> TCM (a, CommandState)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT (TCErr -> CommandM a
    h TCErr
    e) CommandState
    s
          put s'
          return x

        -- Handle every possible kind of error (#637), except for
        -- AsyncCancelled, which is used to abort Agda.
        handleNastyErrors :: CommandM () -> CommandM ()
        handleNastyErrors :: CommandM () -> CommandM ()
    handleNastyErrors CommandM ()
    m = (forall x. (CommandM () -> IO x) -> IO x) -> CommandM ()
    forall a. (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a
    commandMToIO ((forall x. (CommandM () -> IO x) -> IO x) -> CommandM ())
    -> (forall x. (CommandM () -> IO x) -> IO x) -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ \ CommandM () -> IO x
    toIO -> do

          let asyncHandler :: AsyncCancelled -> m (Either AsyncCancelled b)
    asyncHandler e :: AsyncCancelled
    e@AsyncCancelled
    AsyncCancelled = Either AsyncCancelled b -> m (Either AsyncCancelled b)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (AsyncCancelled -> Either AsyncCancelled b
    forall a b. a -> Either a b
    Left AsyncCancelled
    e)

              ioHandler :: IOException -> IO (Either AsyncCancelled x)
    ioHandler (IOException
    e :: E.IOException) = x -> Either AsyncCancelled x
    forall a b. b -> Either a b
    Right (x -> Either AsyncCancelled x)
    -> IO x -> IO (Either AsyncCancelled x)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
                CommandM () -> IO x
    toIO (CommandM () -> IO x) -> CommandM () -> IO x
    forall a b. (a -> b) -> a -> b
    $ Maybe HighlightingMethod -> TCErr -> CommandM ()
    handleErr (HighlightingMethod -> Maybe HighlightingMethod
    forall a. a -> Maybe a
    Just HighlightingMethod
    Direct) (TCErr -> CommandM ()) -> TCErr -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ Maybe TCState -> Range -> IOException -> TCErr
    IOException Maybe TCState
    forall a. Maybe a
    Nothing Range
    forall a. Range' a
    noRange IOException
    e

              generalHandler :: SomeException -> IO (Either AsyncCancelled x)
    generalHandler (SomeException
    e :: E.SomeException) = x -> Either AsyncCancelled x
    forall a b. b -> Either a b
    Right (x -> Either AsyncCancelled x)
    -> IO x -> IO (Either AsyncCancelled x)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
                CommandM () -> IO x
    toIO (CommandM () -> IO x) -> CommandM () -> IO x
    forall a b. (a -> b) -> a -> b
    $ Maybe HighlightingMethod -> TCErr -> CommandM ()
    handleErr (HighlightingMethod -> Maybe HighlightingMethod
    forall a. a -> Maybe a
    Just HighlightingMethod
    Direct) (TCErr -> CommandM ()) -> TCErr -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ String -> TCErr
    GenericException (String -> TCErr) -> String -> TCErr
    forall a b. (a -> b) -> a -> b
    $ SomeException -> String
    forall e. Exception e => e -> String
    showIOException SomeException
    e

          r <- (x -> Either AsyncCancelled x
    forall a b. b -> Either a b
    Right (x -> Either AsyncCancelled x)
    -> IO x -> IO (Either AsyncCancelled x)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> CommandM () -> IO x
    toIO CommandM ()
    m)
                 IO (Either AsyncCancelled x)
    -> (AsyncCancelled -> IO (Either AsyncCancelled x))
    -> IO (Either AsyncCancelled x)
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `E.catch` AsyncCancelled -> IO (Either AsyncCancelled x)
    forall {m :: * -> *} {b}.
    Monad m =>
    AsyncCancelled -> m (Either AsyncCancelled b)
    asyncHandler
                 IO (Either AsyncCancelled x)
    -> (IOException -> IO (Either AsyncCancelled x))
    -> IO (Either AsyncCancelled x)
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `E.catch` IOException -> IO (Either AsyncCancelled x)
    ioHandler
                 IO (Either AsyncCancelled x)
    -> (SomeException -> IO (Either AsyncCancelled x))
    -> IO (Either AsyncCancelled x)
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `E.catch` SomeException -> IO (Either AsyncCancelled x)
    generalHandler
          case r of
            Right x
    x -> x -> IO x
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return x
    x
            Left AsyncCancelled
    e  -> AsyncCancelled -> IO x
    forall e a. (HasCallStack, Exception e) => e -> IO a
    E.throwIO AsyncCancelled
    e

        -- Displays an error and instructs Emacs to jump to the site of the
        -- error. Because this function may switch the focus to another file
        -- the status information is also updated.
        handleErr :: Maybe HighlightingMethod -> TCErr -> CommandM ()
    handleErr Maybe HighlightingMethod
    method TCErr
    e = do

          -- TODO: make a better predicate for this
          noError <- TCMT IO Bool -> StateT CommandState TCM Bool
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO Bool -> StateT CommandState TCM Bool)
    -> TCMT IO Bool -> StateT CommandState TCM Bool
    forall a b. (a -> b) -> a -> b
    $ String -> Bool
    forall a. Null a => a -> Bool
    null (String -> Bool) -> TCMT IO String -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCErr -> TCMT IO String
    forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
    renderError TCErr
    e
          unless noError do

            unsolved <- lift $ computeUnsolvedInfo
            err     <- lift $ errorHighlighting e
            modFile <- lift $ useTC stModuleToSource
            method  <- case method of
              Maybe HighlightingMethod
    Nothing -> TCMT IO HighlightingMethod
    -> StateT CommandState TCM HighlightingMethod
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO HighlightingMethod
     -> StateT CommandState TCM HighlightingMethod)
    -> TCMT IO HighlightingMethod
    -> StateT CommandState TCM HighlightingMethod
    forall a b. (a -> b) -> a -> b
    $ Lens' TCEnv HighlightingMethod -> TCMT IO HighlightingMethod
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (HighlightingMethod -> f HighlightingMethod) -> TCEnv -> f TCEnv
    Lens' TCEnv HighlightingMethod
    eHighlightingMethod
              Just HighlightingMethod
    m  -> HighlightingMethod -> StateT CommandState TCM HighlightingMethod
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HighlightingMethod
    m
            let info = HighlightingInfoBuilder -> HighlightingInfo
    forall a b. Convert a b => a -> b
    convert (HighlightingInfoBuilder -> HighlightingInfo)
    -> HighlightingInfoBuilder -> HighlightingInfo
    forall a b. (a -> b) -> a -> b
    $ HighlightingInfoBuilder
    err HighlightingInfoBuilder
    -> HighlightingInfoBuilder -> HighlightingInfoBuilder
    forall a. Semigroup a => a -> a -> a
    <> HighlightingInfoBuilder
    unsolved
                         -- Errors take precedence over unsolved things.

            showImpl <- lift $ optShowImplicit <$> useTC stPragmaOptions
            showIrr <- lift $ optShowIrrelevant <$> useTC stPragmaOptions
            do
              mapM_ putResponse $
                [ Resp_DisplayInfo $ Info_Error $ Info_GenericError e ] ++
                tellEmacsToJumpToError (getRange e) ++
                [ Resp_HighlightingInfo info KeepHighlighting
                                        method modFile ] ++
                [ Resp_Status $ Status { sChecked = False
                                       , sShowImplicitArguments = showImpl
                                       , sShowIrrelevantArguments = showIrr
                                       } ]
              whenM (optExitOnError <$> commandLineOptions) $
                liftIO $ exitAgdaWith TCMError

    -- | Run an 'IOTCM' value, catch the exceptions, emit output
    --
    --   If an error happens the state of 'CommandM' does not change,
    --   but stPersistent may change (which contains successfully
    --   loaded interfaces for example).

    runInteraction :: IOTCM -> CommandM ()
    runInteraction :: IOTCM -> CommandM ()
    runInteraction IOTCM
    iotcm =
      (forall a. CommandM a -> CommandM a)
    -> CommandM () -> CommandM () -> CommandM ()
    handleCommand CommandM a -> CommandM a
    forall a. CommandM a -> CommandM a
    inEmacs CommandM ()
    onFail (CommandM () -> CommandM ()) -> CommandM () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ do
        currentAbs <- IO AbsolutePath -> StateT CommandState TCM AbsolutePath
    forall a. IO a -> StateT CommandState TCM a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO AbsolutePath -> StateT CommandState TCM AbsolutePath)
    -> IO AbsolutePath -> StateT CommandState TCM AbsolutePath
    forall a b. (a -> b) -> a -> b
    $ String -> IO AbsolutePath
    absolute String
    current
        cf  <- gets theCurrentFile
        cmd <- if independent cmd then return cmd else do
          when (Just currentAbs /= (currentFilePath <$> cf)) $ do
            let mode = Mode
    TypeCheck
            cmd_load' current [] True mode $ \CheckResult
    _ -> () -> CommandM ()
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          cf <- fromMaybe __IMPOSSIBLE__ <$> gets theCurrentFile
          return $ case iotcm (Just (currentFileModule cf)) of
            IOTCM String
    _ HighlightingLevel
    _ HighlightingMethod
    _ Interaction' Range
    cmd -> Interaction' Range
    cmd

        withCurrentFile $ interpret cmd

        cf' <- gets theCurrentFile
        when (updateInteractionPointsAfter cmd
                &&
              Just currentAbs == (currentFilePath <$> cf')) $ do
            putResponse . Resp_InteractionPoints =<< gets theInteractionPoints

      where
        -- The ranges in cmd might be incorrect because of the use of
        -- Nothing here. That is taken care of above.
        IOTCM String
    current HighlightingLevel
    highlighting HighlightingMethod
    highlightingMethod Interaction' Range
    cmd = IOTCM
    iotcm Maybe TopLevelModuleName
    forall a. Maybe a
    Nothing

        inEmacs :: forall a. CommandM a -> CommandM a
        inEmacs :: forall a. CommandM a -> CommandM a
    inEmacs = (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
    forall a. (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
    liftCommandMT ((forall x. TCM x -> TCM x) -> CommandM a -> CommandM a)
    -> (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
    forall a b. (a -> b) -> a -> b
    $ TCEnv -> TCMT IO x -> TCMT IO x
    forall (m :: * -> *) a. MonadTCEnv m => TCEnv -> m a -> m a
    withEnv (TCEnv -> TCMT IO x -> TCMT IO x)
    -> TCEnv -> TCMT IO x -> TCMT IO x
    forall a b. (a -> b) -> a -> b
    $ TCEnv
    initEnv
                { envHighlightingLevel  = highlighting
                , envHighlightingMethod = highlightingMethod
                }

        -- If an independent command fails we should reset theCurrentFile (Issue853).
        onFail :: CommandM ()
    onFail | Interaction' Range -> Bool
    independent Interaction' Range
    cmd = (CommandState -> CommandState) -> CommandM ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((CommandState -> CommandState) -> CommandM ())
    -> (CommandState -> CommandState) -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ \ CommandState
    s -> CommandState
    s { theCurrentFile = Nothing }
               | Bool
    otherwise       = () -> CommandM ()
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    ------------------------------------------------------------------------
    -- Command queues

    -- | If the next command from the command queue is anything but an
    -- actual command, then the command is returned.
    --
    -- If the command is an 'IOTCM' command, then the following happens:
    -- The given computation is applied to the command and executed. If an
    -- abort command is encountered (and acted upon), then the computation
    -- is interrupted, the persistent state and all options are restored,
    -- and some commands are sent to the frontend. If the computation was
    -- not interrupted, then its result is returned.

    -- TODO: It might be nice if some of the changes to the persistent
    -- state inflicted by the interrupted computation were preserved.

    maybeAbort :: (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
    maybeAbort :: forall a. (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
    maybeAbort IOTCM -> CommandM a
    m = do
      commandState <- StateT CommandState TCM CommandState
    forall s (m :: * -> *). MonadState s m => m s
    get
      let q = CommandState -> CommandQueue
    commandQueue CommandState
    commandState
      (n, cmd) <- liftIO $ atomically $ readTChan (commands q)
      case cmd of
        Command
    Done      -> Command' (Maybe a) -> StateT CommandState TCM (Command' (Maybe a))
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Command' (Maybe a)
    forall a. Command' a
    Done
        Error String
    e   -> Command' (Maybe a) -> StateT CommandState TCM (Command' (Maybe a))
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> Command' (Maybe a)
    forall a. String -> Command' a
    Error String
    e)
        Command IOTCM
    c -> do
          tcState <- StateT CommandState TCM TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
          tcEnv   <- askTC
          result  <- liftIO $ race
                       (runTCM tcEnv tcState $
                        runStateT (m c) commandState)
                       (waitForAbort n q)
          case result of
            Left ((a
    x, CommandState
    commandState'), TCState
    tcState') -> do
              TCState -> CommandM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    tcState'
              CommandState -> CommandM ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put CommandState
    commandState'
              case IOTCM
    c Maybe TopLevelModuleName
    forall a. Maybe a
    Nothing of
                IOTCM String
    _ HighlightingLevel
    _ HighlightingMethod
    _ Interaction' Range
    Cmd_exit -> do
                  Response -> CommandM ()
    putResponse Response
    forall tcErr tcWarning warningsAndNonFatalErrors.
    Response_boot tcErr tcWarning warningsAndNonFatalErrors
    Resp_DoneExiting
                  Command' (Maybe a) -> StateT CommandState TCM (Command' (Maybe a))
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Command' (Maybe a)
    forall a. Command' a
    Done
                IOTCM' Range
    _ -> Command' (Maybe a) -> StateT CommandState TCM (Command' (Maybe a))
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe a -> Command' (Maybe a)
    forall a. a -> Command' a
    Command (a -> Maybe a
    forall a. a -> Maybe a
    Just a
    x))
            Right Integer
    a -> do
              IO () -> CommandM ()
    forall a. IO a -> StateT CommandState TCM a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> CommandM ()) -> IO () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ CommandQueue -> Integer -> IO ()
    popAbortedCommands CommandQueue
    q Integer
    a
              TCState -> CommandM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC (TCState -> CommandM ()) -> TCState -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ Lens' TCState PragmaOptions -> LensSet TCState PragmaOptions
    forall o i. Lens' o i -> LensSet o i
    set (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
    forall a. LensPragmaOptions a => Lens' a PragmaOptions
    Lens' TCState PragmaOptions
    lensPragmaOptions (TCState
    tcState TCState -> Lens' TCState PragmaOptions -> PragmaOptions
    forall o i. o -> Lens' o i -> i
    ^. (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
    forall a. LensPragmaOptions a => Lens' a PragmaOptions
    Lens' TCState PragmaOptions
    lensPragmaOptions) (TCState -> TCState) -> TCState -> TCState
    forall a b. (a -> b) -> a -> b
    $
                PersistentTCState -> TCState
    initStateFromPersistentState (PersistentTCState -> TCState) -> PersistentTCState -> TCState
    forall a b. (a -> b) -> a -> b
    $ TCState -> PersistentTCState
    stPersistentState TCState
    tcState
              CommandState -> CommandM ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (CommandState -> CommandM ()) -> CommandState -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ (CommandQueue -> CommandState
    initCommandState (CommandState -> CommandQueue
    commandQueue CommandState
    commandState))
                { optionsOnReload = optionsOnReload commandState
                }
              Response -> CommandM ()
    putResponse Response
    forall tcErr tcWarning warningsAndNonFatalErrors.
    Response_boot tcErr tcWarning warningsAndNonFatalErrors
    Resp_DoneAborting
              CommandM ()
    displayStatus
              Command' (Maybe a) -> StateT CommandState TCM (Command' (Maybe a))
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe a -> Command' (Maybe a)
    forall a. a -> Command' a
    Command Maybe a
    forall a. Maybe a
    Nothing)
      where

      -- Returns if the currently executing command should be aborted.
      -- The "abort number" is returned.

      waitForAbort
        :: Integer       -- The number of the currently executing command.
        -> CommandQueue  -- The command queue.
        -> IO Integer
      waitForAbort :: Integer -> CommandQueue -> IO Integer
    waitForAbort Integer
    n CommandQueue
    q = do
        STM Integer -> IO Integer
    forall a. STM a -> IO a
    atomically (STM Integer -> IO Integer) -> STM Integer -> IO Integer
    forall a b. (a -> b) -> a -> b
    $ do
          a <- TVar (Maybe Integer) -> STM (Maybe Integer)
    forall a. TVar a -> STM a
    readTVar (CommandQueue -> TVar (Maybe Integer)
    abort CommandQueue
    q)
          case a of
            Just Integer
    a' | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    a' -> Integer -> STM Integer
    forall a. a -> STM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Integer
    a'
            Maybe Integer
    _                 -> STM Integer
    forall a. STM a
    retry

      -- Removes every command for which the command number is at most
      -- the given number (the "abort number") from the command queue.
      --
      -- New commands could be added to the end of the queue while this
      -- computation is running. This does not lead to a race condition,
      -- because those commands have higher command numbers, so they will
      -- not be removed.

      popAbortedCommands :: CommandQueue -> Integer -> IO ()
      popAbortedCommands :: CommandQueue -> Integer -> IO ()
    popAbortedCommands CommandQueue
    q Integer
    n = do
        done <- STM Bool -> IO Bool
    forall a. STM a -> IO a
    atomically (STM Bool -> IO Bool) -> STM Bool -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ do
          cmd <- TChan (Integer, Command) -> STM (Maybe (Integer, Command))
    forall a. TChan a -> STM (Maybe a)
    tryReadTChan (CommandQueue -> TChan (Integer, Command)
    commands CommandQueue
    q)
          case cmd of
            Maybe (Integer, Command)
    Nothing -> Bool -> STM Bool
    forall a. a -> STM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
            Just (Integer, Command)
    c  ->
              if (Integer, Command) -> Integer
    forall a b. (a, b) -> a
    fst (Integer, Command)
    c Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    n then
                Bool -> STM Bool
    forall a. a -> STM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
               else do
                TChan (Integer, Command) -> (Integer, Command) -> STM ()
    forall a. TChan a -> a -> STM ()
    unGetTChan (CommandQueue -> TChan (Integer, Command)
    commands CommandQueue
    q) (Integer, Command)
    c
                Bool -> STM Bool
    forall a. a -> STM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        unless done $
          popAbortedCommands q n

    -- | Creates a command queue, and forks a thread that writes commands
    -- to the queue. The queue is returned.

    initialiseCommandQueue
      :: IO Command
         -- ^ Returns the next command.
      -> IO CommandQueue
    initialiseCommandQueue :: IO Command -> IO CommandQueue
    initialiseCommandQueue IO Command
    next = do
      commands <- IO (TChan (Integer, Command))
    forall a. IO (TChan a)
    newTChanIO
      abort    <- newTVarIO Nothing

      let -- Read commands. The argument is the number of the previous
          -- command (other than abort commands) that was read, if any.
          readCommands Integer
    n = do
            c <- IO Command
    next
            case c of
              Command IOTCM
    c | IOTCM String
    _ HighlightingLevel
    _ HighlightingMethod
    _ Interaction' Range
    Cmd_abort <- IOTCM
    c Maybe TopLevelModuleName
    forall a. Maybe a
    Nothing -> do
                STM () -> IO ()
    forall a. STM a -> IO a
    atomically (STM () -> IO ()) -> STM () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ TVar (Maybe Integer) -> Maybe Integer -> STM ()
    forall a. TVar a -> a -> STM ()
    writeTVar TVar (Maybe Integer)
    abort (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    n)
                Integer -> IO ()
    readCommands Integer
    n
              Command
    _ -> do
                let n' :: Integer
    n' = (Integer -> Integer
    forall a. Enum a => a -> a
    succ Integer
    n)
                STM () -> IO ()
    forall a. STM a -> IO a
    atomically (STM () -> IO ()) -> STM () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ TChan (Integer, Command) -> (Integer, Command) -> STM ()
    forall a. TChan a -> a -> STM ()
    writeTChan TChan (Integer, Command)
    commands (Integer
    n', Command
    c)
                case Command
    c of
                  Command
    Done -> () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                  Command
    _    -> Integer -> IO ()
    readCommands Integer
    n'

      _ <- forkIO (readCommands 0)

      return (CommandQueue { .. })

    ---------------------------------------------------------

    -- | Can the command run even if the relevant file has not been loaded
    --   into the state?

    independent :: Interaction -> Bool
    independent :: Interaction' Range -> Bool
    independent (Cmd_load {})                   = Bool
    True
    independent Cmd_load_no_metas{}             = Bool
    True
    independent (Cmd_compile {})                = Bool
    True
    independent (Cmd_load_highlighting_info {}) = Bool
    True
    independent Cmd_tokenHighlighting {}        = Bool
    True
    independent Interaction' Range
    Cmd_show_version                = Bool
    True
    independent Interaction' Range
    _                               = Bool
    False

    -- | Should 'Resp_InteractionPoints' be issued after the command has
    -- run?

    updateInteractionPointsAfter :: Interaction -> Bool
    updateInteractionPointsAfter :: Interaction' Range -> Bool
    updateInteractionPointsAfter Cmd_load{}                          = Bool
    True
    updateInteractionPointsAfter Cmd_compile{}                       = Bool
    True
    updateInteractionPointsAfter Cmd_backend_top{}                   = Bool
    True
    updateInteractionPointsAfter Cmd_backend_hole{}                  = Bool
    True
    updateInteractionPointsAfter Cmd_constraints{}                   = Bool
    False
    updateInteractionPointsAfter Cmd_metas{}                         = Bool
    False
    updateInteractionPointsAfter Cmd_load_no_metas{}                 = Bool
    False
    updateInteractionPointsAfter Cmd_show_module_contents_toplevel{} = Bool
    False
    updateInteractionPointsAfter Cmd_search_about_toplevel{}         = Bool
    False
    updateInteractionPointsAfter Cmd_solveAll{}                      = Bool
    True
    updateInteractionPointsAfter Cmd_solveOne{}                      = Bool
    True
    updateInteractionPointsAfter Cmd_infer_toplevel{}                = Bool
    False
    updateInteractionPointsAfter Cmd_compute_toplevel{}              = Bool
    False
    updateInteractionPointsAfter Cmd_load_highlighting_info{}        = Bool
    False
    updateInteractionPointsAfter Cmd_tokenHighlighting{}             = Bool
    False
    updateInteractionPointsAfter Cmd_highlight{}                     = Bool
    True
    updateInteractionPointsAfter ShowImplicitArgs{}                  = Bool
    False
    updateInteractionPointsAfter ToggleImplicitArgs{}                = Bool
    False
    updateInteractionPointsAfter ShowIrrelevantArgs{}                = Bool
    False
    updateInteractionPointsAfter ToggleIrrelevantArgs{}              = Bool
    False
    updateInteractionPointsAfter Cmd_give{}                          = Bool
    True
    updateInteractionPointsAfter Cmd_refine{}                        = Bool
    True
    updateInteractionPointsAfter Cmd_intro{}                         = Bool
    True
    updateInteractionPointsAfter Cmd_refine_or_intro{}               = Bool
    True
    updateInteractionPointsAfter Cmd_autoOne{}                       = Bool
    True
    updateInteractionPointsAfter Cmd_autoAll{}                       = Bool
    True
    updateInteractionPointsAfter Cmd_context{}                       = Bool
    False
    updateInteractionPointsAfter Cmd_helper_function{}               = Bool
    False
    updateInteractionPointsAfter Cmd_infer{}                         = Bool
    False
    updateInteractionPointsAfter Cmd_goal_type{}                     = Bool
    False
    updateInteractionPointsAfter Cmd_elaborate_give{}                = Bool
    True
    updateInteractionPointsAfter Cmd_goal_type_context{}             = Bool
    False
    updateInteractionPointsAfter Cmd_goal_type_context_infer{}       = Bool
    False
    updateInteractionPointsAfter Cmd_goal_type_context_check{}       = Bool
    False
    updateInteractionPointsAfter Cmd_show_module_contents{}          = Bool
    False
    updateInteractionPointsAfter Cmd_make_case{}                     = Bool
    True
    updateInteractionPointsAfter Cmd_compute{}                       = Bool
    False
    updateInteractionPointsAfter Cmd_why_in_scope{}                  = Bool
    False
    updateInteractionPointsAfter Cmd_why_in_scope_toplevel{}         = Bool
    False
    updateInteractionPointsAfter Cmd_show_version{}                  = Bool
    False
    updateInteractionPointsAfter Cmd_abort{}                         = Bool
    False
    updateInteractionPointsAfter Cmd_exit{}                          = Bool
    False

    -- | Interpret an interaction

    getBackendName :: CompilerBackend -> BackendName
    getBackendName :: CompilerBackend -> BackendName
    getBackendName = \case
      CompilerBackend
    LaTeX -> BackendName
    "LaTeX"
      CompilerBackend
    QuickLaTeX -> BackendName
    "LaTeX"
      OtherBackend BackendName
    "GHCNoMain" -> BackendName
    "GHC"
      OtherBackend BackendName
    b -> BackendName
    b

    interpret :: Interaction -> CommandM ()

    interpret :: Interaction' Range -> CommandM ()
    interpret (Cmd_load String
    m [String]
    argv) =
      String
    -> [String]
    -> Bool
    -> Mode
    -> (CheckResult -> CommandM ())
    -> CommandM ()
    forall a.
    String
    -> [String]
    -> Bool
    -> Mode
    -> (CheckResult -> CommandM a)
    -> CommandM a
    cmd_load' String
    m [String]
    argv Bool
    True Mode
    mode ((CheckResult -> CommandM ()) -> CommandM ())
    -> (CheckResult -> CommandM ()) -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ \CheckResult
    _ -> Interaction' Range -> CommandM ()
    interpret (Interaction' Range -> CommandM ())
    -> Interaction' Range -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> Interaction' Range
    forall range. Rewrite -> Interaction' range
    Cmd_metas Rewrite
    AsIs
      where
      mode :: Mode
    mode = Mode
    TypeCheck

    interpret (Cmd_compile CompilerBackend
    backend String
    file [String]
    argv) =
      String
    -> [String]
    -> Bool
    -> Mode
    -> (CheckResult -> CommandM ())
    -> CommandM ()
    forall a.
    String
    -> [String]
    -> Bool
    -> Mode
    -> (CheckResult -> CommandM a)
    -> CommandM a
    cmd_load' String
    file [String]
    argv Bool
    allowUnsolved Mode
    mode ((CheckResult -> CommandM ()) -> CommandM ())
    -> (CheckResult -> CommandM ()) -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ \ CheckResult
    checkResult -> do
        ws <- TCM (Set TCWarning) -> StateT CommandState TCM (Set TCWarning)
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM (Set TCWarning) -> StateT CommandState TCM (Set TCWarning))
    -> TCM (Set TCWarning) -> StateT CommandState TCM (Set TCWarning)
    forall a b. (a -> b) -> a -> b
    $ Set TCWarning -> TCM (Set TCWarning)
    forall (m :: * -> *).
    HasOptions m =>
    Set TCWarning -> m (Set TCWarning)
    applyFlagsToTCWarnings (Set TCWarning -> TCM (Set TCWarning))
    -> Set TCWarning -> TCM (Set TCWarning)
    forall a b. (a -> b) -> a -> b
    $ CheckResult -> Set TCWarning
    crWarnings CheckResult
    checkResult
        case null ws of
          Bool
    True -> do
            TCM () -> CommandM ()
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> CommandM ()) -> TCM () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ BackendName -> IsMain -> CheckResult -> TCM ()
    callBackend (CompilerBackend -> BackendName
    getBackendName CompilerBackend
    backend) IsMain
    isMain CheckResult
    checkResult
            DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
     -> CommandM ())
    -> (WarningsAndNonFatalErrors
        -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
    -> WarningsAndNonFatalErrors
    -> CommandM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CompilerBackend
    -> WarningsAndNonFatalErrors
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    forall tcErr tcWarning warningsAndNonFatalErrors.
    CompilerBackend
    -> warningsAndNonFatalErrors
    -> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
    Info_CompilationOk CompilerBackend
    backend (WarningsAndNonFatalErrors -> CommandM ())
    -> StateT CommandState TCM WarningsAndNonFatalErrors -> CommandM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCM WarningsAndNonFatalErrors
    -> StateT CommandState TCM WarningsAndNonFatalErrors
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCM WarningsAndNonFatalErrors
    B.getWarningsAndNonFatalErrors
          Bool
    False -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
     -> CommandM ())
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ Info_Error
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    forall tcErr tcWarning warningsAndNonFatalErrors.
    Info_Error_boot tcErr tcWarning
    -> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
    Info_Error (Info_Error
     -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
    -> Info_Error
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    forall a b. (a -> b) -> a -> b
    $ Set TCWarning -> Info_Error
    forall tcErr tcWarning.
    Set tcWarning -> Info_Error_boot tcErr tcWarning
    Info_CompilationError Set TCWarning
    ws
      where
      allowUnsolved :: Bool
    allowUnsolved = CompilerBackend
    backend CompilerBackend -> [CompilerBackend] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [CompilerBackend
    LaTeX, CompilerBackend
    QuickLaTeX]
      mode :: Mode
    mode | CompilerBackend
    QuickLaTeX <- CompilerBackend
    backend = Mode
    ScopeCheck
           | Bool
    otherwise             = Mode
    TypeCheck
      isMain :: IsMain
    isMain | OtherBackend BackendName
    "GHCNoMain" <- CompilerBackend
    backend = IsMain
    NotMain
             | Bool
    otherwise                           = IsMain
    IsMain

    interpret (Cmd_backend_top CompilerBackend
    backend String
    cmd) =
      BackendName -> String -> CommandM ()
    callBackendInteractTop (CompilerBackend -> BackendName
    getBackendName CompilerBackend
    backend) String
    cmd

    interpret (Cmd_backend_hole InteractionId
    ii Range
    rng String
    s CompilerBackend
    backend String
    cmd) =
      BackendName
    -> String -> InteractionId -> Range -> String -> CommandM ()
    callBackendInteractHole (CompilerBackend -> BackendName
    getBackendName CompilerBackend
    backend) String
    cmd InteractionId
    ii Range
    rng String
    s

    interpret Interaction' Range
    Cmd_constraints =
      DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
     -> CommandM ())
    -> ([OutputForm_boot TCErr Expr Expr]
        -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
    -> [OutputForm_boot TCErr Expr Expr]
    -> CommandM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [OutputForm_boot TCErr Expr Expr]
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    forall tcErr tcWarning warningsAndNonFatalErrors.
    [OutputForm_boot tcErr Expr Expr]
    -> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
    Info_Constraints ([OutputForm_boot TCErr Expr Expr] -> CommandM ())
    -> StateT CommandState TCM [OutputForm_boot TCErr Expr Expr]
    -> CommandM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCM [OutputForm_boot TCErr Expr Expr]
    -> StateT CommandState TCM [OutputForm_boot TCErr Expr Expr]
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCM [OutputForm_boot TCErr Expr Expr]
    B.getConstraints

    interpret (Cmd_metas Rewrite
    norm) = do
      ms <- TCMT IO Goals -> StateT CommandState TCM Goals
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO Goals -> StateT CommandState TCM Goals)
    -> TCMT IO Goals -> StateT CommandState TCM Goals
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> Rewrite -> TCMT IO Goals
    B.getGoals' Rewrite
    norm (Rewrite -> Rewrite -> Rewrite
    forall a. Ord a => a -> a -> a
    max Rewrite
    Simplified Rewrite
    norm)
      display_info . Info_AllGoalsWarnings ms =<< lift B.getWarningsAndNonFatalErrors

    interpret (Cmd_load_no_metas String
    file) = do
      -- Fail if there are open metas.
      let allowMetas :: Bool
    allowMetas = Bool
    False
      String
    -> [String]
    -> Bool
    -> Mode
    -> (CheckResult -> CommandM ())
    -> CommandM ()
    forall a.
    String
    -> [String]
    -> Bool
    -> Mode
    -> (CheckResult -> CommandM a)
    -> CommandM a
    cmd_load' String
    file [] Bool
    allowMetas Mode
    TypeCheck ((CheckResult -> CommandM ()) -> CommandM ())
    -> (CheckResult -> CommandM ()) -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ \ CheckResult
    result -> do
        CheckResult -> CommandM ()
    forall (m :: * -> *).
    (HasOptions m, MonadTCError m) =>
    CheckResult -> m ()
    Imp.raiseNonFatalErrors CheckResult
    result
        StateT CommandState TCM Bool -> CommandM () -> CommandM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM ([MetaId] -> Bool
    forall a. Null a => a -> Bool
    null ([MetaId] -> Bool)
    -> StateT CommandState TCM [MetaId] -> StateT CommandState TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> StateT CommandState TCM [MetaId]
    forall (m :: * -> *). ReadTCState m => m [MetaId]
    getOpenMetas) CommandM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    interpret (Cmd_show_module_contents_toplevel Rewrite
    norm String
    s) =
      CommandM () -> CommandM ()
    forall a. CommandM a -> CommandM a
    atTopLevel (CommandM () -> CommandM ()) -> CommandM () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> Range -> String -> CommandM ()
    showModuleContents Rewrite
    norm Range
    forall a. Range' a
    noRange String
    s

    interpret (Cmd_search_about_toplevel Rewrite
    norm String
    s) =
      CommandM () -> CommandM ()
    forall a. CommandM a -> CommandM a
    atTopLevel (CommandM () -> CommandM ()) -> CommandM () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> Range -> String -> CommandM ()
    searchAbout Rewrite
    norm Range
    forall a. Range' a
    noRange String
    s

    interpret (Cmd_solveAll Rewrite
    norm)        = Rewrite -> Maybe InteractionId -> CommandM ()
    solveInstantiatedGoals Rewrite
    norm Maybe InteractionId
    forall a. Maybe a
    Nothing
    interpret (Cmd_solveOne Rewrite
    norm InteractionId
    ii Range
    _ String
    _) = Rewrite -> Maybe InteractionId -> CommandM ()
    solveInstantiatedGoals Rewrite
    norm' (InteractionId -> Maybe InteractionId
    forall a. a -> Maybe a
    Just InteractionId
    ii)
      -- `solveOne` is called via `agda2-maybe-normalised` which does not use
      -- AsIs < Simplified < Normalised but rather Simplified < Instantiated < Normalised
      -- So we remap the Rewrite modifiers to match solveAll's behaviour.
      -- NB: instantiate is called in getSolvedInteractionPoints no matter what.
      where norm' :: Rewrite
    norm' = case Rewrite
    norm of
                      Rewrite
    Simplified   -> Rewrite
    AsIs
                      Rewrite
    Instantiated -> Rewrite
    Simplified
                      Rewrite
    _            -> Rewrite
    norm

    interpret (Cmd_infer_toplevel Rewrite
    norm String
    s) = do
      (time, expr) <- (Expr -> TCM Expr) -> String -> CommandM (Maybe CPUTime, Expr)
    forall a. (Expr -> TCM a) -> String -> CommandM (Maybe CPUTime, a)
    parseAndDoAtToplevel (Rewrite -> Expr -> TCM Expr
    B.typeInCurrent Rewrite
    norm) String
    s
      state <- get
      display_info $ Info_InferredType state time expr

    interpret (Cmd_compute_toplevel ComputeMode
    cmode String
    s) = do
      (time, expr) <- (Expr -> TCM Expr) -> String -> CommandM (Maybe CPUTime, Expr)
    forall a. (Expr -> TCM a) -> String -> CommandM (Maybe CPUTime, a)
    parseAndDoAtToplevel Expr -> TCM Expr
    action (ComputeMode -> String -> String
    B.computeWrapInput ComputeMode
    cmode String
    s)
      state <- get
      display_info $ Info_NormalForm state cmode time expr
        where
        action :: Expr -> TCM Expr
    action = TCM Expr -> TCM Expr
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    allowNonTerminatingReductions
               (TCM Expr -> TCM Expr) -> (Expr -> TCM Expr) -> Expr -> TCM Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (if ComputeMode -> Bool
    B.computeIgnoreAbstract ComputeMode
    cmode then TCM Expr -> TCM Expr
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode else TCM Expr -> TCM Expr
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    inConcreteMode)
               (TCM Expr -> TCM Expr) -> (Expr -> TCM Expr) -> Expr -> TCM Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ComputeMode -> Expr -> TCM Expr
    B.evalInCurrent ComputeMode
    cmode
    -- interpret (Cmd_compute_toplevel cmode s) =
    --   parseAndDoAtToplevel action Info_NormalForm $ computeWrapInput cmode s
    --   where
    --   action = allowNonTerminatingReductions
    --          . (if computeIgnoreAbstract cmode then ignoreAbstractMode else inConcreteMode)
    --          . (B.showComputed cmode <=< B.evalInCurrent)

    interpret (ShowImplicitArgs Bool
    showImpl) = do
      opts <- TCM CommandLineOptions
    -> StateT CommandState TCM CommandLineOptions
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCM CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
      setCommandLineOpts $
        set (lensPragmaOptions . lensOptShowImplicit . lensKeepDefault) showImpl opts

    interpret Interaction' Range
    ToggleImplicitArgs = do
      opts <- TCM CommandLineOptions
    -> StateT CommandState TCM CommandLineOptions
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCM CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
      setCommandLineOpts $
        over (lensPragmaOptions . lensOptShowImplicit . lensCollapseDefault) not opts

    interpret (ShowIrrelevantArgs Bool
    showIrr) = do
      opts <- TCM CommandLineOptions
    -> StateT CommandState TCM CommandLineOptions
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCM CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
      setCommandLineOpts $
        set (lensPragmaOptions . lensOptShowIrrelevant . lensKeepDefault) showIrr opts

    interpret Interaction' Range
    ToggleIrrelevantArgs = do
      opts <- TCM CommandLineOptions
    -> StateT CommandState TCM CommandLineOptions
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCM CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
      setCommandLineOpts $
        over (lensPragmaOptions . lensOptShowIrrelevant . lensCollapseDefault) not opts

    interpret (Cmd_load_highlighting_info String
    source) = do
      l <- (TCEnv -> HighlightingLevel)
    -> StateT CommandState TCM HighlightingLevel
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> HighlightingLevel
    envHighlightingLevel
      when (l /= None) $ do
        -- Make sure that the include directories have
        -- been set.
        setCommandLineOpts =<< lift commandLineOptions
        resp <- lift $ liftIO . tellToUpdateHighlighting =<< do
          ex        <- liftIO $ doesFileExist source
          absSource <- srcFromPath =<< liftIO (absolute source)
          if ex
            then
               do
                  src <- Imp.parseSource absSource
                  let m = Source -> TopLevelModuleName
    Imp.srcModuleName Source
    src
                  checkModuleName m absSource Nothing
                  mmi <- getVisitedModule m
                  case mmi of
                    Maybe ModuleInfo
    Nothing -> Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    -> TCMT
         IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    forall a. Maybe a
    Nothing
                    Just ModuleInfo
    mi ->
                      if Text -> Hash
    hashText (Source -> Text
    Imp.srcText Source
    src) Hash -> Hash -> Bool
    forall a. Eq a => a -> a -> Bool
    == Interface -> Hash
    iSourceHash (ModuleInfo -> Interface
    miInterface ModuleInfo
    mi)
                        then do
                          modFile <- Lens' TCState ModuleToSource -> TCMT IO ModuleToSource
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (ModuleToSource -> f ModuleToSource) -> TCState -> f TCState
    Lens' TCState ModuleToSource
    stModuleToSource
                          method  <- viewTC eHighlightingMethod
                          return $ Just (iHighlighting $ miInterface mi, method, modFile)
                        else
                          Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    -> TCMT
         IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    forall a. Maybe a
    Nothing
                `catchError` \TCErr
    _ -> Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    -> TCMT
         IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    forall a. Maybe a
    Nothing
            else
              return Nothing
        mapM_ putResponse resp

    interpret (Cmd_tokenHighlighting String
    source Remove
    remove) = do
      info <- do l <- (TCEnv -> HighlightingLevel)
    -> StateT CommandState TCM HighlightingLevel
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> HighlightingLevel
    envHighlightingLevel
                 if l == None
                   then return Nothing
                   else do
                     source' <- liftIO (absolute source)
                     lift $ (Just <$> generateTokenInfo source')
                               `catchError` \TCErr
    _ ->
                            Maybe HighlightingInfo -> TCM (Maybe HighlightingInfo)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe HighlightingInfo
    forall a. Maybe a
    Nothing
          StateT CommandState TCM (Maybe HighlightingInfo)
    -> CommandM () -> StateT CommandState TCM (Maybe HighlightingInfo)
    forall e (m :: * -> *) a. MonadError e m => m a -> m () -> m a
    `finally`
        case Remove
    remove of
          Remove
    Remove -> IO () -> CommandM ()
    forall a. IO a -> StateT CommandState TCM a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> CommandM ()) -> IO () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    removeFile String
    source
          Remove
    Keep   -> () -> CommandM ()
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      case info of
        Just HighlightingInfo
    info' -> TCM () -> CommandM ()
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> CommandM ()) -> TCM () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    RemoveHighlighting HighlightingInfo
    info'
        Maybe HighlightingInfo
    Nothing    -> () -> CommandM ()
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    interpret (Cmd_highlight InteractionId
    ii Range
    rng String
    s) = do
      l <- (TCEnv -> HighlightingLevel)
    -> StateT CommandState TCM HighlightingLevel
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> HighlightingLevel
    envHighlightingLevel
      when (l /= None) $ do
        scope <- getOldInteractionScope ii
        removeOldInteractionScope ii
        handle $ do
          parsed <- try (Info_HighlightingParseError ii) $
                 B.parseExpr rng s
          expr <- try (Info_HighlightingScopeCheckError ii) $
                 concreteToAbstract scope parsed
          lift $ printHighlightingInfo KeepHighlighting =<<
                   generateTokenInfoFromString rng s
          lift $ highlightExpr expr
      where
        handle :: ExceptT Info_Error TCM () -> CommandM ()
        handle :: ExceptT Info_Error TCM () -> CommandM ()
    handle ExceptT Info_Error TCM ()
    m = do
          res <- TCM (Either Info_Error ())
    -> StateT CommandState TCM (Either Info_Error ())
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM (Either Info_Error ())
     -> StateT CommandState TCM (Either Info_Error ()))
    -> TCM (Either Info_Error ())
    -> StateT CommandState TCM (Either Info_Error ())
    forall a b. (a -> b) -> a -> b
    $ ExceptT Info_Error TCM () -> TCM (Either Info_Error ())
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT ExceptT Info_Error TCM ()
    m
          case res of
            Left Info_Error
    err -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
     -> CommandM ())
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ Info_Error
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    forall tcErr tcWarning warningsAndNonFatalErrors.
    Info_Error_boot tcErr tcWarning
    -> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
    Info_Error Info_Error
    err
            Right ()
    _ -> () -> CommandM ()
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        try :: Info_Error -> TCM a -> ExceptT Info_Error TCM a
        try :: forall a. Info_Error -> TCM a -> ExceptT Info_Error TCM a
    try Info_Error
    err TCM a
    m = TCM (Either Info_Error a) -> ExceptT Info_Error TCM a
    forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
    ExceptT (TCM (Either Info_Error a) -> ExceptT Info_Error TCM a)
    -> TCM (Either Info_Error a) -> ExceptT Info_Error TCM a
    forall a b. (a -> b) -> a -> b
    $ do
          ((TCErr -> Info_Error) -> Either TCErr a -> Either Info_Error a
    forall a c b. (a -> c) -> Either a b -> Either c b
    mapLeft (Info_Error -> TCErr -> Info_Error
    forall a b. a -> b -> a
    const Info_Error
    err) (Either TCErr a -> Either Info_Error a)
    -> TCMT IO (Either TCErr a) -> TCM (Either Info_Error a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM a -> TCMT IO (Either TCErr a)
    forall a. TCM a -> TCM (Either TCErr a)
    freshTCM TCM a
    m) TCM (Either Info_Error a)
    -> (TCErr -> TCM (Either Info_Error a))
    -> TCM (Either Info_Error a)
    forall a. TCM a -> (TCErr -> TCM a) -> TCM a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \ TCErr
    _ -> Either Info_Error a -> TCM (Either Info_Error a)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Info_Error -> Either Info_Error a
    forall a b. a -> Either a b
    Left Info_Error
    err)
          -- freshTCM to avoid scope checking creating new interaction points

    interpret (Cmd_give   UseForce
    force InteractionId
    ii Range
    rng String
    s) = UseForce
    -> InteractionId -> Range -> String -> GiveRefine -> CommandM ()
    give_gen UseForce
    force InteractionId
    ii Range
    rng String
    s GiveRefine
    Give
    interpret (Cmd_refine InteractionId
    ii Range
    rng String
    s) = UseForce
    -> InteractionId -> Range -> String -> GiveRefine -> CommandM ()
    give_gen UseForce
    WithoutForce InteractionId
    ii Range
    rng String
    s GiveRefine
    Refine

    interpret (Cmd_intro Bool
    pmLambda InteractionId
    ii Range
    rng String
    _) = do
      ss <- TCMT IO [String] -> StateT CommandState TCM [String]
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO [String] -> StateT CommandState TCM [String])
    -> TCMT IO [String] -> StateT CommandState TCM [String]
    forall a b. (a -> b) -> a -> b
    $ Bool -> InteractionId -> TCMT IO [String]
    B.introTactic Bool
    pmLambda InteractionId
    ii
      liftCommandMT (withInteractionId ii) $ case ss of
        []    -> do
          DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
     -> CommandM ())
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    forall tcErr tcWarning warningsAndNonFatalErrors.
    DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
    Info_Intro_NotFound
        [String
    s]   -> UseForce
    -> InteractionId -> Range -> String -> GiveRefine -> CommandM ()
    give_gen UseForce
    WithoutForce InteractionId
    ii Range
    rng String
    s GiveRefine
    Intro
        String
    _:String
    _:[String]
    _ -> do
          DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
     -> CommandM ())
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ [String]
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    forall tcErr tcWarning warningsAndNonFatalErrors.
    [String]
    -> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
    Info_Intro_ConstructorUnknown [String]
    ss

    interpret (Cmd_refine_or_intro Bool
    pmLambda InteractionId
    ii Range
    r String
    s) = Interaction' Range -> CommandM ()
    interpret (Interaction' Range -> CommandM ())
    -> Interaction' Range -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $
      let s' :: String
    s' = String -> String
    trim String
    s
      in (if String -> Bool
    forall a. Null a => a -> Bool
    null String
    s' then Bool -> InteractionId -> Range -> String -> Interaction' Range
    forall range.
    Bool -> InteractionId -> range -> String -> Interaction' range
    Cmd_intro Bool
    pmLambda else InteractionId -> Range -> String -> Interaction' Range
    forall range.
    InteractionId -> range -> String -> Interaction' range
    Cmd_refine) InteractionId
    ii Range
    r String
    s'

    interpret (Cmd_autoOne Rewrite
    norm InteractionId
    ii Range
    rng String
    str) = do
      iscope <- InteractionId -> CommandM ScopeInfo
    forall (m :: * -> *).
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m ScopeInfo
    getInteractionScope InteractionId
    ii
      (time, result) <- maybeTimed $ Mimer.mimer norm ii rng str
      case result of
        MimerResult
    MimerNoResult -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
     -> CommandM ())
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ String
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    forall tcErr tcWarning warningsAndNonFatalErrors.
    String
    -> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
    Info_Auto String
    "No solution found"
        MimerExpr String
    str -> do
          InteractionId -> ScopeInfo -> CommandM ()
    insertOldInteractionScope InteractionId
    ii ScopeInfo
    iscope
          _ <- TCM Expr -> StateT CommandState TCM Expr
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM Expr -> StateT CommandState TCM Expr)
    -> TCM Expr -> StateT CommandState TCM Expr
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> Range -> String -> TCM Expr
    B.parseExprIn InteractionId
    ii Range
    rng String
    str TCM Expr -> (Expr -> TCM Expr) -> TCM Expr
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    B.give UseForce
    WithForce InteractionId
    ii (Range -> Maybe Range
    forall a. a -> Maybe a
    Just Range
    rng)
          putResponse $ Resp_GiveAction ii $ Give_String str
          modifyTheInteractionPoints (List.delete ii)
          maybe (return ()) (display_info . Info_Time) time
        MimerList [(Int, String)]
    sols -> do
          DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
     -> CommandM ())
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ String
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    forall tcErr tcWarning warningsAndNonFatalErrors.
    String
    -> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
    Info_Auto (String
     -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
    -> String
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $
            [ String
    "Solutions:" ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
            [ String
    "  " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ". " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s | (Int
    i, String
    s) <- [(Int, String)]
    sols ]
        MimerClauses{} -> CommandM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__    -- Mimer can't do case splitting yet

    interpret (Cmd_autoAll Rewrite
    norm) = do
      iis <- StateT CommandState TCM [InteractionId]
    forall (m :: * -> *). ReadTCState m => m [InteractionId]
    getInteractionPoints
      getOldScope <- do
        st <- getTC
        pure $ \ InteractionId
    ii -> TCM ScopeInfo -> CommandM ScopeInfo
    forall b. TCM b -> StateT CommandState TCM b
    liftLocalState (TCM ScopeInfo -> CommandM ScopeInfo)
    -> TCM ScopeInfo -> CommandM ScopeInfo
    forall a b. (a -> b) -> a -> b
    $ TCState -> TCM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    st TCM () -> TCM ScopeInfo -> TCM ScopeInfo
    forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> InteractionId -> TCM ScopeInfo
    forall (m :: * -> *).
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m ScopeInfo
    getInteractionScope InteractionId
    ii
      unless (null iis) $ do
        let time = Int
    1000 Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `div` [InteractionId] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [InteractionId]
    iis
        st <- getTC
        solved <- fmap concat $ forM iis $ \ InteractionId
    ii -> do
          rng <- InteractionId -> StateT CommandState TCM Range
    forall (m :: * -> *).
    (MonadInteractionPoints m, MonadDebug m, MonadError TCErr m) =>
    InteractionId -> m Range
    getInteractionRange InteractionId
    ii
          res <- Mimer.mimer norm ii rng ("-t " ++ show time ++ "ms")
          case res of
            MimerResult
    MimerNoResult -> [InteractionId] -> StateT CommandState TCM [InteractionId]
    forall a. a -> StateT CommandState TCM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
            MimerExpr String
    str -> do
              iscope <- InteractionId -> CommandM ScopeInfo
    getOldScope InteractionId
    ii
              insertOldInteractionScope ii iscope
              _ <- liftTCM $ B.parseExprIn ii rng str >>= B.give WithoutForce ii (Just rng)
              putResponse $ Resp_GiveAction ii $ Give_String str
              pure [ii]
            MimerList{} -> [InteractionId] -> StateT CommandState TCM [InteractionId]
    forall a. a -> StateT CommandState TCM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []    -- Don't list solutions in autoAll
            MimerClauses{} -> StateT CommandState TCM [InteractionId]
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- Mimer can't do case splitting yet
        modifyTheInteractionPoints (List.\\ solved)

    interpret (Cmd_context Rewrite
    norm InteractionId
    ii Range
    _ String
    _) =
      DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
     -> CommandM ())
    -> ([ResponseContextEntry]
        -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
    -> [ResponseContextEntry]
    -> CommandM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . InteractionId
    -> [ResponseContextEntry]
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    forall tcErr tcWarning warningsAndNonFatalErrors.
    InteractionId
    -> [ResponseContextEntry]
    -> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
    Info_Context InteractionId
    ii ([ResponseContextEntry] -> CommandM ())
    -> StateT CommandState TCM [ResponseContextEntry] -> CommandM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCM [ResponseContextEntry]
    -> StateT CommandState TCM [ResponseContextEntry]
    forall b. TCM b -> StateT CommandState TCM b
    liftLocalState (Rewrite -> InteractionId -> TCM [ResponseContextEntry]
    B.getResponseContext Rewrite
    norm InteractionId
    ii)

    interpret (Cmd_helper_function Rewrite
    norm InteractionId
    ii Range
    rng String
    s) = do
      -- Create type of application of new helper function that would solve the goal.
      helperType <- TCM (OutputConstraint' Expr Expr)
    -> CommandM (OutputConstraint' Expr Expr)
    forall b. TCM b -> StateT CommandState TCM b
    liftLocalState (TCM (OutputConstraint' Expr Expr)
     -> CommandM (OutputConstraint' Expr Expr))
    -> TCM (OutputConstraint' Expr Expr)
    -> CommandM (OutputConstraint' Expr Expr)
    forall a b. (a -> b) -> a -> b
    $ InteractionId
    -> TCM (OutputConstraint' Expr Expr)
    -> TCM (OutputConstraint' Expr Expr)
    forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCM (OutputConstraint' Expr Expr)
     -> TCM (OutputConstraint' Expr Expr))
    -> TCM (OutputConstraint' Expr Expr)
    -> TCM (OutputConstraint' Expr Expr)
    forall a b. (a -> b) -> a -> b
    $ TCM (OutputConstraint' Expr Expr)
    -> TCM (OutputConstraint' Expr Expr)
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCM (OutputConstraint' Expr Expr)
     -> TCM (OutputConstraint' Expr Expr))
    -> TCM (OutputConstraint' Expr Expr)
    -> TCM (OutputConstraint' Expr Expr)
    forall a b. (a -> b) -> a -> b
    $ Rewrite
    -> InteractionId
    -> Range
    -> String
    -> TCM (OutputConstraint' Expr Expr)
    B.metaHelperType Rewrite
    norm InteractionId
    ii Range
    rng String
    s
      display_info $ Info_GoalSpecific ii (Goal_HelperFunction helperType)

    interpret (Cmd_infer Rewrite
    norm InteractionId
    ii Range
    rng String
    s) = do
      expr <- TCM Expr -> StateT CommandState TCM Expr
    forall b. TCM b -> StateT CommandState TCM b
    liftLocalState (TCM Expr -> StateT CommandState TCM Expr)
    -> TCM Expr -> StateT CommandState TCM Expr
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> TCM Expr -> TCM Expr
    forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> Rewrite -> Expr -> TCM Expr
    B.typeInMeta InteractionId
    ii Rewrite
    norm (Expr -> TCM Expr) -> TCM Expr -> TCM Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< InteractionId -> Range -> String -> TCM Expr
    B.parseExprIn InteractionId
    ii Range
    rng String
    s
      display_info $ Info_GoalSpecific ii (Goal_InferredType expr)

    interpret (Cmd_goal_type Rewrite
    norm InteractionId
    ii Range
    _ String
    _) =
      DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
     -> CommandM ())
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ InteractionId
    -> GoalDisplayInfo_boot TCErr
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    forall tcErr tcWarning warningsAndNonFatalErrors.
    InteractionId
    -> GoalDisplayInfo_boot tcErr
    -> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
    Info_GoalSpecific InteractionId
    ii (Rewrite -> GoalDisplayInfo_boot TCErr
    forall tcErr. Rewrite -> GoalDisplayInfo_boot tcErr
    Goal_CurrentGoal Rewrite
    norm)

    interpret (Cmd_elaborate_give Rewrite
    norm InteractionId
    ii Range
    rng String
    s) =
      UseForce
    -> InteractionId -> Range -> String -> GiveRefine -> CommandM ()
    give_gen UseForce
    WithoutForce InteractionId
    ii Range
    rng String
    s (GiveRefine -> CommandM ()) -> GiveRefine -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> GiveRefine
    ElaborateGive Rewrite
    norm

    interpret (Cmd_goal_type_context Rewrite
    norm InteractionId
    ii Range
    rng String
    s) =
      GoalTypeAux
    -> Rewrite -> InteractionId -> Range -> String -> CommandM ()
    cmd_goal_type_context_and GoalTypeAux
    GoalOnly Rewrite
    norm InteractionId
    ii Range
    rng String
    s

    interpret (Cmd_goal_type_context_infer Rewrite
    norm InteractionId
    ii Range
    rng String
    s) = do
      -- In case of the empty expression to type, don't fail with
      -- a stupid parse error, but just fall back to
      -- Cmd_goal_type_context.
      aux <- if (Char -> Bool) -> String -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Char -> Bool
    Char.isSpace String
    s
                then GoalTypeAux -> StateT CommandState TCM GoalTypeAux
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return GoalTypeAux
    GoalOnly
                else do
                  TCM GoalTypeAux -> StateT CommandState TCM GoalTypeAux
    forall b. TCM b -> StateT CommandState TCM b
    liftLocalState (TCM GoalTypeAux -> StateT CommandState TCM GoalTypeAux)
    -> TCM GoalTypeAux -> StateT CommandState TCM GoalTypeAux
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> TCM GoalTypeAux -> TCM GoalTypeAux
    forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCM GoalTypeAux -> TCM GoalTypeAux)
    -> TCM GoalTypeAux -> TCM GoalTypeAux
    forall a b. (a -> b) -> a -> b
    $ do
                    parsed <- InteractionId -> Range -> String -> TCM Expr
    B.parseExprIn InteractionId
    ii Range
    rng String
    s
                    (typ, faces) <- B.typeAndFacesInMeta ii norm parsed
                    return (GoalAndHave typ faces)
      cmd_goal_type_context_and aux norm ii rng s

    interpret (Cmd_goal_type_context_check Rewrite
    norm InteractionId
    ii Range
    rng String
    s) = do
      expr <- TCM Expr -> StateT CommandState TCM Expr
    forall b. TCM b -> StateT CommandState TCM b
    liftLocalState (TCM Expr -> StateT CommandState TCM Expr)
    -> TCM Expr -> StateT CommandState TCM Expr
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> TCM Expr -> TCM Expr
    forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
    forall a b. (a -> b) -> a -> b
    $ do
        expr <- InteractionId -> Range -> String -> TCM Expr
    B.parseExprIn InteractionId
    ii Range
    rng String
    s
        goal <- B.typeOfMeta AsIs ii
        term <- case goal of
          OfType InteractionId
    _ Expr
    ty -> Expr -> Type -> TCMT IO Term
    checkExpr Expr
    expr (Type -> TCMT IO Term) -> TCMT IO Type -> TCMT IO Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Expr -> TCMT IO Type
    isType_ Expr
    ty
          OutputConstraint Expr InteractionId
    _           -> TCMT IO Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        reify =<< B.normalForm norm term
      cmd_goal_type_context_and (GoalAndElaboration expr) norm ii rng s

    interpret (Cmd_show_module_contents Rewrite
    norm InteractionId
    ii Range
    rng String
    s) =
      (forall x. TCM x -> TCM x) -> CommandM () -> CommandM ()
    forall a. (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
    liftCommandMT (InteractionId -> TCMT IO x -> TCMT IO x
    forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii) (CommandM () -> CommandM ()) -> CommandM () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> Range -> String -> CommandM ()
    showModuleContents Rewrite
    norm Range
    rng String
    s

    interpret (Cmd_why_in_scope_toplevel String
    s) =
      CommandM () -> CommandM ()
    forall a. CommandM a -> CommandM a
    atTopLevel (CommandM () -> CommandM ()) -> CommandM () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ String -> CommandM ()
    whyInScope String
    s

    interpret (Cmd_why_in_scope InteractionId
    ii Range
    _range String
    s) =
      (forall x. TCM x -> TCM x) -> CommandM () -> CommandM ()
    forall a. (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
    liftCommandMT (InteractionId -> TCMT IO x -> TCMT IO x
    forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii) (CommandM () -> CommandM ()) -> CommandM () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ String -> CommandM ()
    whyInScope String
    s

    interpret (Cmd_make_case InteractionId
    ii Range
    rng String
    s) = do
      (f, casectxt, cs) <- TCMT IO (QName, CaseContext, [Clause])
    -> StateT CommandState TCM (QName, CaseContext, [Clause])
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO (QName, CaseContext, [Clause])
     -> StateT CommandState TCM (QName, CaseContext, [Clause]))
    -> TCMT IO (QName, CaseContext, [Clause])
    -> StateT CommandState TCM (QName, CaseContext, [Clause])
    forall a b. (a -> b) -> a -> b
    $ InteractionId
    -> Range -> String -> TCMT IO (QName, CaseContext, [Clause])
    makeCase InteractionId
    ii Range
    rng String
    s
      liftCommandMT (withInteractionId ii) $ do
        tel <- lift $ lookupSection (qnameModule f) -- don't shadow the names in this telescope
        unicode <- getsTC $ optUseUnicode . getPragmaOptions
        pcs      :: [Doc]      <- lift $ inTopContext $ addContext tel $ mapM prettyAUnqualify cs
        let pcs' :: [String]    = List.map (extlam_dropName unicode casectxt . decorate) pcs
        lift $ reportSDoc "interaction.case" 60 $ TCP.vcat
          [ "InteractionTop.Cmd_make_case"
          , TCP.nest 2 $ TCP.vcat
            [ "cs   = " TCP.<+> TCP.vcat (map prettyA cs)
            , "pcs  = " TCP.<+> TCP.vcat (map return pcs)
            , "pcs' = " TCP.<+> TCP.vcat (map TCP.text pcs')
            ]
          ]
        lift $ reportSDoc "interaction.case" 90 $ TCP.vcat
          [ "InteractionTop.Cmd_make_case"
          , TCP.nest 2 $ TCP.vcat
            [ "cs   = " TCP.<+> TCP.text (show cs)
            ]
          ]
        putResponse $ Resp_MakeCase ii (makeCaseVariant casectxt) pcs'

    interpret (Cmd_compute ComputeMode
    cmode InteractionId
    ii Range
    rng String
    s) = do
      expr <- TCM Expr -> StateT CommandState TCM Expr
    forall b. TCM b -> StateT CommandState TCM b
    liftLocalState (TCM Expr -> StateT CommandState TCM Expr)
    -> TCM Expr -> StateT CommandState TCM Expr
    forall a b. (a -> b) -> a -> b
    $ do
        e <- InteractionId -> Range -> String -> TCM Expr
    B.parseExprIn InteractionId
    ii Range
    rng (String -> TCM Expr) -> String -> TCM Expr
    forall a b. (a -> b) -> a -> b
    $ ComputeMode -> String -> String
    B.computeWrapInput ComputeMode
    cmode String
    s
        withInteractionId ii $ applyWhen (B.computeIgnoreAbstract cmode) ignoreAbstractMode $ B.evalInCurrent cmode e
      display_info $ Info_GoalSpecific ii (Goal_NormalForm cmode expr)

    interpret Interaction' Range
    Cmd_show_version = DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    display_info DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    forall tcErr tcWarning warningsAndNonFatalErrors.
    DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
    Info_Version

    interpret Interaction' Range
    Cmd_abort = () -> CommandM ()
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    interpret Interaction' Range
    Cmd_exit  = () -> CommandM ()
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    decorate :: Doc -> String
    decorate :: Doc -> String
    decorate = Style -> Doc -> String
    forall a. Style -> Doc a -> String
    renderStyle (Style
    style { mode = OneLineMode })

    makeCaseVariant :: CaseContext -> MakeCaseVariant
    makeCaseVariant :: CaseContext -> MakeCaseVariant
    makeCaseVariant CaseContext
    Nothing = MakeCaseVariant
    R.Function
    makeCaseVariant Just{}  = MakeCaseVariant
    R.ExtendedLambda

    -- very dirty hack, string manipulation by dropping the function name
    -- and replacing the last " = " with " -> ". It's important not to replace
    -- the equal sign in named implicit with an arrow!
    extlam_dropName :: UnicodeOrAscii -> CaseContext -> String -> String
    extlam_dropName :: UnicodeOrAscii -> CaseContext -> String -> String
    extlam_dropName UnicodeOrAscii
    _ CaseContext
    Nothing String
    x = String
    x
    extlam_dropName UnicodeOrAscii
    glyphMode Just{}  String
    x
        = [String] -> String
    unwords ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ [String] -> [String]
    forall a. [a] -> [a]
    reverse ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $ [String] -> [String]
    replEquals ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $ [String] -> [String]
    forall a. [a] -> [a]
    reverse ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $ Int -> [String] -> [String]
    forall a. Int -> [a] -> [a]
    drop Int
    1 ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $ String -> [String]
    words String
    x
      where
        arrow :: String
    arrow = Doc -> String
    forall a. Doc a -> String
    render (Doc -> String) -> Doc -> String
    forall a b. (a -> b) -> a -> b
    $ SpecialCharacters -> Doc
    _arrow (SpecialCharacters -> Doc) -> SpecialCharacters -> Doc
    forall a b. (a -> b) -> a -> b
    $ UnicodeOrAscii -> SpecialCharacters
    specialCharactersForGlyphs UnicodeOrAscii
    glyphMode
        replEquals :: [String] -> [String]
    replEquals (String
    "=" : [String]
    ws) = String
    arrow String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    ws
        replEquals (String
    w   : [String]
    ws) = String
    w String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String] -> [String]
    replEquals [String]
    ws
        replEquals []         = []

    -- | Solved goals already instantiated internally
    -- The second argument potentially limits it to one specific goal.
    solveInstantiatedGoals :: Rewrite -> Maybe InteractionId -> CommandM ()
    solveInstantiatedGoals :: Rewrite -> Maybe InteractionId -> CommandM ()
    solveInstantiatedGoals Rewrite
    norm Maybe InteractionId
    mii = do
      -- Andreas, 2016-10-23 issue #2280: throw away meta elims.
      out <- TCM [(InteractionId, Expr)]
    -> StateT CommandState TCM [(InteractionId, Expr)]
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM [(InteractionId, Expr)]
     -> StateT CommandState TCM [(InteractionId, Expr)])
    -> TCM [(InteractionId, Expr)]
    -> StateT CommandState TCM [(InteractionId, Expr)]
    forall a b. (a -> b) -> a -> b
    $ (TCEnv -> TCEnv)
    -> TCM [(InteractionId, Expr)] -> TCM [(InteractionId, Expr)]
    forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\ TCEnv
    e -> TCEnv
    e { envPrintMetasBare = True }) (TCM [(InteractionId, Expr)] -> TCM [(InteractionId, Expr)])
    -> TCM [(InteractionId, Expr)] -> TCM [(InteractionId, Expr)]
    forall a b. (a -> b) -> a -> b
    $ do
        sip <- Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)]
    B.getSolvedInteractionPoints Bool
    False Rewrite
    norm
               -- only solve metas which have a proper instantiation, i.e., not another meta
        let sip' = ([(InteractionId, MetaId, Expr)]
     -> [(InteractionId, MetaId, Expr)])
    -> (InteractionId
        -> [(InteractionId, MetaId, Expr)]
        -> [(InteractionId, MetaId, Expr)])
    -> Maybe InteractionId
    -> [(InteractionId, MetaId, Expr)]
    -> [(InteractionId, MetaId, Expr)]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [(InteractionId, MetaId, Expr)] -> [(InteractionId, MetaId, Expr)]
    forall a. a -> a
    id (\ InteractionId
    ii -> ((InteractionId, MetaId, Expr) -> Bool)
    -> [(InteractionId, MetaId, Expr)]
    -> [(InteractionId, MetaId, Expr)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((InteractionId
    ii InteractionId -> InteractionId -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (InteractionId -> Bool)
    -> ((InteractionId, MetaId, Expr) -> InteractionId)
    -> (InteractionId, MetaId, Expr)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (InteractionId, MetaId, Expr) -> InteractionId
    forall a b c. (a, b, c) -> a
    fst3)) Maybe InteractionId
    mii [(InteractionId, MetaId, Expr)]
    sip
        mapM prt sip'
      putResponse $ Resp_SolveAll out
      where
          prt :: (a, MetaId, a) -> m (a, ConOfAbs a)
    prt (a
    i, MetaId
    m, a
    e) = do
            mi <- MetaVariable -> Closure Range
    getMetaInfo (MetaVariable -> Closure Range)
    -> m MetaVariable -> m (Closure Range)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m
            e' <- withMetaInfo mi $ abstractToConcreteCtx TopCtx e
            return (i, e')

    -- | @cmd_load' file argv unsolvedOk cmd@
    --   loads the module in file @file@,
    --   using @argv@ as the command-line options.
    --
    -- If type checking completes without any exceptions having been
    -- encountered then the command @cmd r@ is executed, where @r@ is the
    -- result of 'Imp.typeCheckMain'.

    cmd_load'
      :: FilePath  -- ^ File to load into interaction.
      -> [String]  -- ^ Arguments to Agda for loading this file
      -> Bool      -- ^ Allow unsolved meta-variables?
      -> Mode      -- ^ Full type-checking, or only scope-checking?
      -> (CheckResult -> CommandM a)
                   -- ^ Continuation after successful loading.
      -> CommandM a
    cmd_load' :: forall a.
    String
    -> [String]
    -> Bool
    -> Mode
    -> (CheckResult -> CommandM a)
    -> CommandM a
    cmd_load' String
    file [String]
    argv Bool
    unsolvedOK Mode
    mode CheckResult -> CommandM a
    cmd = do

        -- Forget the previous "current file" and interaction points.
        (CommandState -> CommandState) -> CommandM ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((CommandState -> CommandState) -> CommandM ())
    -> (CommandState -> CommandState) -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ \ CommandState
    st -> CommandState
    st { theInteractionPoints = []
                            , theCurrentFile       = Nothing
                            }

        -- Update the status. Because the "current file" is not set the
        -- status is not "Checked".
        CommandM ()
    displayStatus

        -- Reset the state, preserving options and decoded modules. Note
        -- that if the include directories have changed, then the decoded
        -- modules are reset by TCM.setCommandLineOptions' below.
        TCM () -> CommandM ()
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCM ()
    resetState

        -- Clear the info buffer to make room for information about which
        -- module is currently being type-checked.
        Response -> CommandM ()
    putResponse Response
    forall tcErr tcWarning warningsAndNonFatalErrors.
    Response_boot tcErr tcWarning warningsAndNonFatalErrors
    Resp_ClearRunningInfo

        -- Remove any prior syntax highlighting.
        Response -> CommandM ()
    putResponse (TokenBased -> Response
    forall tcErr tcWarning warningsAndNonFatalErrors.
    TokenBased
    -> Response_boot tcErr tcWarning warningsAndNonFatalErrors
    Resp_ClearHighlighting TokenBased
    NotOnlyTokenBased)

        -- Parse the file.
        --
        -- Note that options are set below.
        fp  <- IO AbsolutePath -> StateT CommandState TCM AbsolutePath
    forall a. IO a -> StateT CommandState TCM a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO AbsolutePath -> StateT CommandState TCM AbsolutePath)
    -> IO AbsolutePath -> StateT CommandState TCM AbsolutePath
    forall a b. (a -> b) -> a -> b
    $ String -> IO AbsolutePath
    absolute String
    file
        sf  <- liftTCM $ srcFromPath fp
        src <- lift $ Imp.parseSource sf
        -- Andreas, 2024-08-03, see test/interaction/FileNotFound:
        -- Run 'getModificationTime' after 'parseSource',
        -- otherwise the user gets a weird error for non-existing files.
        -- (We assume that parsing is fast in comparison to type-checking,
        -- so it should not matter much whether we get the time stamp
        -- before or after parsing.)
        t   <- liftIO $ getModificationTime file

        -- Store the warnings.
        warnings <- useTC stTCWarnings

        -- All options are reset when a file is reloaded, including the
        -- choice of whether or not to display implicit arguments.
        opts0 <- gets optionsOnReload
        backends <- useTC stBackends
        let (z, warns) = runOptM $ parseBackendOptions backends argv opts0
        mapM_ (lift . warning . OptionWarning) warns
        case z of
          Left String
    err -> TCM () -> CommandM ()
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> CommandM ()) -> TCM () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    OptionError String
    err
          Right ([Backend]
    _, CommandLineOptions
    opts) -> do
            opts <- TCM CommandLineOptions
    -> StateT CommandState TCM CommandLineOptions
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM CommandLineOptions
     -> StateT CommandState TCM CommandLineOptions)
    -> TCM CommandLineOptions
    -> StateT CommandState TCM CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions -> TCM CommandLineOptions
    addTrustedExecutables CommandLineOptions
    opts
            let update = Lens' PragmaOptions Bool -> LensMap PragmaOptions Bool
    forall o i. Lens' o i -> LensMap o i
    over ((WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptAllowUnsolved ((WithDefault 'False -> f (WithDefault 'False))
     -> PragmaOptions -> f PragmaOptions)
    -> ((Bool -> f Bool)
        -> WithDefault 'False -> f (WithDefault 'False))
    -> (Bool -> f Bool)
    -> PragmaOptions
    -> f PragmaOptions
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Bool -> f Bool) -> WithDefault 'False -> f (WithDefault 'False)
    forall a (b :: Bool).
    (Boolean a, Eq a, KnownBool b) =>
    Lens' (WithDefault' a b) a
    Lens' (WithDefault 'False) Bool
    lensKeepDefault) (Bool
    unsolvedOK Bool -> Bool -> Bool
    &&)
                root   = AbsolutePath -> TopLevelModuleName -> AbsolutePath
    projectRoot AbsolutePath
    fp (TopLevelModuleName -> AbsolutePath)
    -> TopLevelModuleName -> AbsolutePath
    forall a b. (a -> b) -> a -> b
    $ Source -> TopLevelModuleName
    Imp.srcModuleName Source
    src
            lift $ TCM.setCommandLineOptions' root $ mapPragmaOptions update opts

        -- Restore the warnings that were saved above.
        modifyTCLens stTCWarnings $ Set.union warnings

        ok <- lift $ Imp.typeCheckMain mode src

        -- 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 <- lift $ sortInteractionPoints =<< getInteractionPoints
          modify $ \CommandState
    st -> CommandState
    st { theInteractionPoints = is
                             , theCurrentFile       = Just $ CurrentFile
                                 { currentFilePath   = fp
                                 , currentFileModule = Imp.srcModuleName src
                                 , currentFileArgs   = argv
                                 , currentFileStamp  = t
                                 }
                             }

        cmd ok

    -- | Set 'envCurrentPath' to 'theCurrentFile', if any.
    withCurrentFile :: CommandM a -> CommandM a
    withCurrentFile :: forall a. CommandM a -> CommandM a
    withCurrentFile CommandM a
    m = do
      mfile <- (CommandState -> Maybe AbsolutePath)
    -> StateT CommandState TCM (Maybe AbsolutePath)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ((CommandState -> Maybe AbsolutePath)
     -> StateT CommandState TCM (Maybe AbsolutePath))
    -> (CommandState -> Maybe AbsolutePath)
    -> StateT CommandState TCM (Maybe AbsolutePath)
    forall a b. (a -> b) -> a -> b
    $ (CurrentFile -> AbsolutePath)
    -> Maybe CurrentFile -> Maybe AbsolutePath
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap CurrentFile -> AbsolutePath
    currentFilePath (Maybe CurrentFile -> Maybe AbsolutePath)
    -> (CommandState -> Maybe CurrentFile)
    -> CommandState
    -> Maybe AbsolutePath
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CommandState -> Maybe CurrentFile
    theCurrentFile
      i <- traverse idFromFile mfile
      localTC (\ TCEnv
    e -> TCEnv
    e { envCurrentPath = i }) m

    atTopLevel :: CommandM a -> CommandM a
    atTopLevel :: forall a. CommandM a -> CommandM a
    atTopLevel CommandM a
    cmd = (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
    forall a. (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
    liftCommandMT TCM x -> TCM x
    forall x. TCM x -> TCM x
    B.atTopLevel CommandM a
    cmd

    ---------------------------------------------------------------------------
    -- Giving, refining.

    data GiveRefine = Give | Refine | Intro | ElaborateGive Rewrite
      deriving (GiveRefine -> GiveRefine -> Bool
    (GiveRefine -> GiveRefine -> Bool)
    -> (GiveRefine -> GiveRefine -> Bool) -> Eq GiveRefine
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: GiveRefine -> GiveRefine -> Bool
    == :: GiveRefine -> GiveRefine -> Bool
    $c/= :: GiveRefine -> GiveRefine -> Bool
    /= :: GiveRefine -> GiveRefine -> Bool
    Eq, Int -> GiveRefine -> String -> String
    [GiveRefine] -> String -> String
    GiveRefine -> String
    (Int -> GiveRefine -> String -> String)
    -> (GiveRefine -> String)
    -> ([GiveRefine] -> String -> String)
    -> Show GiveRefine
    forall a.
    (Int -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    $cshowsPrec :: Int -> GiveRefine -> String -> String
    showsPrec :: Int -> GiveRefine -> String -> String
    $cshow :: GiveRefine -> String
    show :: GiveRefine -> String
    $cshowList :: [GiveRefine] -> String -> String
    showList :: [GiveRefine] -> String -> String
    Show)

    -- | A "give"-like action (give, refine, etc).
    --
    --   @give_gen force ii rng s give_ref mk_newtxt@
    --   acts on interaction point @ii@
    --   occupying range @rng@,
    --   placing the new content given by string @s@,
    --   and replacing @ii@ by the newly created interaction points
    --   in the state if safety checks pass (unless @force@ is applied).
    give_gen
      :: UseForce       -- ^ Should safety checks be skipped?
      -> InteractionId
      -> Range
      -> String
      -> GiveRefine
      -> CommandM ()
    give_gen :: UseForce
    -> InteractionId -> Range -> String -> GiveRefine -> CommandM ()
    give_gen UseForce
    force InteractionId
    ii Range
    rng String
    s0 GiveRefine
    giveRefine = do
      let s :: String
    s = String -> String
    trim String
    s0
      String -> Int -> String -> CommandM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "interaction.give" Int
    20 (String -> CommandM ()) -> String -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ String
    "give_gen  " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s
      -- Andreas, 2015-02-26 if string is empty do nothing rather
      -- than giving a parse error.
      Bool -> CommandM () -> CommandM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (String -> Bool
    forall a. Null a => a -> Bool
    null String
    s) (CommandM () -> CommandM ()) -> CommandM () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ do
        let give_ref :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    give_ref =
              case GiveRefine
    giveRefine of
                GiveRefine
    Give               -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    B.give
                GiveRefine
    Refine             -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    B.refine
                GiveRefine
    Intro              -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    B.refine
                ElaborateGive Rewrite
    norm -> Rewrite
    -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    B.elaborate_give Rewrite
    norm
        -- save scope of the interaction point (for printing the given expr. later)
        scope     <- InteractionId -> CommandM ScopeInfo
    forall (m :: * -> *).
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m ScopeInfo
    getInteractionScope InteractionId
    ii
        -- parse string and "give", obtaining an abstract expression
        -- and newly created interaction points
        (time, (ae, ae0, iis)) <- maybeTimed $ do
            -- Issue 3000: mark the current hole as solved before giving, to avoid confusing it with potential
            -- new interaction points introduced by the give.
            removeInteractionPoint ii
            mis  <- getInteractionPoints
            reportSLn "interaction.give" 30 $ "interaction points before = " ++ show mis
            given <- lift $ B.parseExprIn ii rng s
            ae    <- lift $ give_ref force ii Nothing given
            mis' <- getInteractionPoints
            reportSLn "interaction.give" 30 $ "interaction points after = " ++ show mis'
            return (ae, given, mis' List.\\ mis)
        -- favonia: backup the old scope for highlighting
        insertOldInteractionScope ii scope
        -- sort the new interaction points and put them into the state
        -- in replacement of the old interaction point
        iis' <- sortInteractionPoints iis
        modifyTheInteractionPoints $ replace ii iis'
        -- print abstract expr
        ce        <- abstractToConcreteScope scope ae
        reportS "interaction.give" 30
          [ "ce = " ++ show ce
          , "scopePrecedence = " ++ show (scope ^. scopePrecedence)
          ]

        -- Issue 7218: if the give/refine command creates an extended
        -- lambda, it also needs to be added to the relevant unfolding sets.
        -- The easiest way to make sure this is consistent is to just re-run
        -- the saturation procedures.
        saturateOpaqueBlocks

        -- if the command was @Give@, use the literal user input;
        -- Andreas, 2014-01-15, see issue 1020:
        -- Refine could solve a goal by introducing the sole constructor
        -- without arguments.  Then there are no interaction metas, but
        -- we still cannot just `give' the user string (which may be empty).
        -- WRONG: also, if no interaction metas were created by @Refine@
        -- WRONG: let literally = (giveRefine == Give || null iis) && rng /= noRange
        -- Ulf, 2015-03-30, if we're doing intro we can't do literal give since
        -- there is nothing in the hole (issue 1892).
        let literally = (GiveRefine
    giveRefine GiveRefine -> GiveRefine -> Bool
    forall a. Eq a => a -> a -> Bool
    == GiveRefine
    Give Bool -> Bool -> Bool
    || GiveRefine
    giveRefine GiveRefine -> GiveRefine -> Bool
    forall a. Eq a => a -> a -> Bool
    == GiveRefine
    Refine) Bool -> Bool -> Bool
    && Expr
    ae Expr -> Expr -> Bool
    forall a. Eq a => a -> a -> Bool
    == Expr
    ae0 Bool -> Bool -> Bool
    && Range
    rng Range -> Range -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Range
    forall a. Range' a
    noRange
        -- Ulf, 2014-01-24: This works for give since we're highlighting the string
        -- that's already in the buffer. Doing it before the give action means that
        -- the highlighting is moved together with the text when the hole goes away.
        -- To make it work for refine we'd have to adjust the ranges.
        when literally $ do
          l <- asksTC envHighlightingLevel
          when (l /= None) $ lift $ do
            printHighlightingInfo KeepHighlighting =<<
              generateTokenInfoFromString rng s
            highlightExpr ae
        putResponse $ Resp_GiveAction ii $ mkNewTxt literally ce
        reportSLn "interaction.give" 30 $ "putResponse GiveAction passed"
        -- display new goal set (if not measuring time)
        maybe (interpret $ Cmd_metas AsIs) (display_info . Info_Time) time
        reportSLn "interaction.give" 30 $ "interpret Cmd_metas passed"
      where
        -- Substitutes xs for x in ys.
        replace :: b -> [b] -> t b -> [b]
    replace b
    x [b]
    xs t b
    ys = (b -> [b]) -> t b -> [b]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (\ b
    y -> if b
    y b -> b -> Bool
    forall a. Eq a => a -> a -> Bool
    == b
    x then [b]
    xs else [b
    y]) t b
    ys
        -- For @Give@ we can replace the ii by the user given input.
        mkNewTxt :: Bool -> Expr -> GiveResult
    mkNewTxt Bool
    True  C.Paren{} = GiveResult
    Give_Paren
        mkNewTxt Bool
    True  Expr
    _         = GiveResult
    Give_NoParen
        -- Otherwise, we replace it by the reified value Agda computed.
        mkNewTxt Bool
    False Expr
    ce        = String -> GiveResult
    Give_String (String -> GiveResult) -> String -> GiveResult
    forall a b. (a -> b) -> a -> b
    $ Expr -> String
    forall a. Pretty a => a -> String
    prettyShow Expr
    ce

    highlightExpr :: A.Expr -> TCM ()
    highlightExpr :: Expr -> TCM ()
    highlightExpr Expr
    e =
      (TCEnv -> TCEnv) -> TCM () -> TCM ()
    forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\TCEnv
    st -> TCEnv
    st { envImportPath         = []
                         , envHighlightingLevel  = NonInteractive
                         , envHighlightingMethod = Direct }) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        Declaration -> Level -> Bool -> TCM ()
    generateAndPrintSyntaxInfo Declaration
    decl Level
    Full Bool
    True
      where
        dummy :: Name
    dummy = NameId -> String -> Name
    forall a. MkName a => NameId -> a -> Name
    mkName_ (Hash -> ModuleNameHash -> NameId
    NameId Hash
    0 ModuleNameHash
    noModuleNameHash) (String
    "dummy" :: String)
        info :: DefInfo' Expr
    info  = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' Expr
    forall t.
    Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
    mkDefInfo (Name -> Name
    nameConcrete Name
    dummy) Fixity'
    noFixity' Access
    PublicAccess IsAbstract
    ConcreteDef (Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e)
        decl :: Declaration
    decl  = KindOfName
    -> DefInfo' Expr
    -> ArgInfo
    -> Maybe PragmaPolarities
    -> QName
    -> Expr
    -> Declaration
    A.Axiom KindOfName
    OtherDefName DefInfo' Expr
    info ArgInfo
    defaultArgInfo Maybe PragmaPolarities
    forall a. Maybe a
    Nothing (List1 Name -> QName
    qnameFromList (List1 Name -> QName) -> List1 Name -> QName
    forall a b. (a -> b) -> a -> b
    $ Name -> List1 Name
    forall el coll. Singleton el coll => el -> coll
    singleton Name
    dummy) Expr
    e

    -- | Sorts interaction points based on their ranges.

    sortInteractionPoints
      :: (MonadInteractionPoints m, MonadError TCErr m, MonadDebug m)
      => [InteractionId] -> m [InteractionId]
    sortInteractionPoints :: forall (m :: * -> *).
    (MonadInteractionPoints m, MonadError TCErr m, MonadDebug m) =>
    [InteractionId] -> m [InteractionId]
    sortInteractionPoints [InteractionId]
    is =
      ((InteractionId, Range) -> InteractionId)
    -> [(InteractionId, Range)] -> [InteractionId]
    forall a b. (a -> b) -> [a] -> [b]
    map (InteractionId, Range) -> InteractionId
    forall a b. (a, b) -> a
    fst ([(InteractionId, Range)] -> [InteractionId])
    -> ([(InteractionId, Range)] -> [(InteractionId, Range)])
    -> [(InteractionId, Range)]
    -> [InteractionId]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((InteractionId, Range) -> (InteractionId, Range) -> Ordering)
    -> [(InteractionId, Range)] -> [(InteractionId, Range)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    List.sortBy (Range -> Range -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Range -> Range -> Ordering)
    -> ((InteractionId, Range) -> Range)
    -> (InteractionId, Range)
    -> (InteractionId, Range)
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (InteractionId, Range) -> Range
    forall a b. (a, b) -> b
    snd) ([(InteractionId, Range)] -> [InteractionId])
    -> m [(InteractionId, Range)] -> m [InteractionId]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
        [InteractionId]
    -> (InteractionId -> m (InteractionId, Range))
    -> m [(InteractionId, Range)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [InteractionId]
    is ((InteractionId -> m (InteractionId, Range))
     -> m [(InteractionId, Range)])
    -> (InteractionId -> m (InteractionId, Range))
    -> m [(InteractionId, Range)]
    forall a b. (a -> b) -> a -> b
    $ \ InteractionId
    i -> do
          (InteractionId
    i,) (Range -> (InteractionId, Range))
    -> m Range -> m (InteractionId, Range)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InteractionId -> m Range
    forall (m :: * -> *).
    (MonadInteractionPoints m, MonadDebug m, MonadError TCErr m) =>
    InteractionId -> m Range
    getInteractionRange InteractionId
    i

    -- | Displays the current goal, the given document, and the current
    --   context.
    --
    --   Should not modify the state.

    cmd_goal_type_context_and :: GoalTypeAux -> Rewrite -> InteractionId -> Range ->
                                 String -> CommandM ()
    cmd_goal_type_context_and :: GoalTypeAux
    -> Rewrite -> InteractionId -> Range -> String -> CommandM ()
    cmd_goal_type_context_and GoalTypeAux
    aux Rewrite
    norm InteractionId
    ii Range
    _ String
    _ = do
      ctx <- TCM [ResponseContextEntry]
    -> StateT CommandState TCM [ResponseContextEntry]
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM [ResponseContextEntry]
     -> StateT CommandState TCM [ResponseContextEntry])
    -> TCM [ResponseContextEntry]
    -> StateT CommandState TCM [ResponseContextEntry]
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> InteractionId -> TCM [ResponseContextEntry]
    B.getResponseContext Rewrite
    norm InteractionId
    ii
      constr <- lift $ lookupInteractionId ii >>= B.getConstraintsMentioning norm
      boundary <- lift $ B.getIPBoundary norm ii
      display_info $ Info_GoalSpecific ii (Goal_GoalType norm aux ctx boundary constr)

    -- | Shows all the top-level names in the given module, along with
    -- their types.

    showModuleContents :: Rewrite -> Range -> String -> CommandM ()
    showModuleContents :: Rewrite -> Range -> String -> CommandM ()
    showModuleContents Rewrite
    norm Range
    rng String
    s = do
      (modules, tel, types) <- TCMT IO ([Name], Telescope, [(Name, Type)])
    -> StateT CommandState TCM ([Name], Telescope, [(Name, Type)])
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO ([Name], Telescope, [(Name, Type)])
     -> StateT CommandState TCM ([Name], Telescope, [(Name, Type)]))
    -> TCMT IO ([Name], Telescope, [(Name, Type)])
    -> StateT CommandState TCM ([Name], Telescope, [(Name, Type)])
    forall a b. (a -> b) -> a -> b
    $ Rewrite
    -> Range -> String -> TCMT IO ([Name], Telescope, [(Name, Type)])
    B.moduleContents Rewrite
    norm Range
    rng String
    s
      display_info $ Info_ModuleContents modules tel types

    -- | Shows all the top-level names in scope which mention all the given
    -- identifiers in their type.

    searchAbout :: Rewrite -> Range -> String -> CommandM ()
    searchAbout :: Rewrite -> Range -> String -> CommandM ()
    searchAbout Rewrite
    norm Range
    rg String
    names = do
      String -> (String -> CommandM ()) -> CommandM ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull (String -> String
    trim String
    names) ((String -> CommandM ()) -> CommandM ())
    -> (String -> CommandM ()) -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ \ String
    trimmedNames -> do
        hits <- TCMT IO [(Name, Type)] -> StateT CommandState TCM [(Name, Type)]
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO [(Name, Type)] -> StateT CommandState TCM [(Name, Type)])
    -> TCMT IO [(Name, Type)] -> StateT CommandState TCM [(Name, Type)]
    forall a b. (a -> b) -> a -> b
    $ Rewrite -> Range -> String -> TCMT IO [(Name, Type)]
    findMentions Rewrite
    norm Range
    rg String
    trimmedNames
        display_info $ Info_SearchAbout hits trimmedNames

    -- | Explain why something is in scope.

    whyInScope :: String -> CommandM ()
    whyInScope :: String -> CommandM ()
    whyInScope String
    s = do
      Just file <- (CommandState -> Maybe CurrentFile)
    -> StateT CommandState TCM (Maybe CurrentFile)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets CommandState -> Maybe CurrentFile
    theCurrentFile
      let cwd = String -> String
    takeDirectory (AbsolutePath -> String
    filePath (AbsolutePath -> String) -> AbsolutePath -> String
    forall a b. (a -> b) -> a -> b
    $ CurrentFile -> AbsolutePath
    currentFilePath CurrentFile
    file)
      why <- liftLocalState $ B.whyInScope cwd s
      display_info $ Info_WhyInScope why

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

    setCommandLineOpts :: CommandLineOptions -> CommandM ()
    setCommandLineOpts :: CommandLineOptions -> CommandM ()
    setCommandLineOpts CommandLineOptions
    opts = do
        TCM () -> CommandM ()
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> CommandM ()) -> TCM () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions -> TCM ()
    TCM.setCommandLineOptions CommandLineOptions
    opts
        CommandM ()
    displayStatus

    -- | Computes some status information.
    --
    --   Does not change the state.

    status :: CommandM Status
    status :: CommandM Status
    status = do
      cf       <- (CommandState -> Maybe CurrentFile)
    -> StateT CommandState TCM (Maybe CurrentFile)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets CommandState -> Maybe CurrentFile
    theCurrentFile
      showImpl <- lift showImplicitArguments
      showIrr  <- lift showIrrelevantArguments

      -- 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.
      checked  <- lift $ case cf of
        Maybe CurrentFile
    Nothing -> Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
        Just CurrentFile
    f  -> do
          t <- IO ClockTime -> TCMT IO ClockTime
    forall b. IO b -> TCM b
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO ClockTime -> TCMT IO ClockTime)
    -> IO ClockTime -> TCMT IO ClockTime
    forall a b. (a -> b) -> a -> b
    $ String -> IO ClockTime
    getModificationTime (String -> IO ClockTime) -> String -> IO ClockTime
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> String
    filePath (CurrentFile -> AbsolutePath
    currentFilePath CurrentFile
    f)
          if currentFileStamp f == t
            then
              maybe False (null . miWarnings) <$>
              getVisitedModule (currentFileModule f)
            else
                return False

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

    -- | Displays or updates status information.
    --
    --   Does not change the state.

    displayStatus :: CommandM ()
    displayStatus :: CommandM ()
    displayStatus =
      Response -> CommandM ()
    putResponse (Response -> CommandM ())
    -> (Status -> Response) -> Status -> CommandM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Status -> Response
    forall tcErr tcWarning warningsAndNonFatalErrors.
    Status -> Response_boot tcErr tcWarning warningsAndNonFatalErrors
    Resp_Status  (Status -> CommandM ()) -> CommandM Status -> CommandM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< CommandM Status
    status

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

    display_info :: DisplayInfo -> CommandM ()
    display_info :: DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> CommandM ()
    display_info DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    info = do
      CommandM ()
    displayStatus
      Response -> CommandM ()
    putResponse (Response -> CommandM ()) -> Response -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> Response
    forall tcErr tcWarning warningsAndNonFatalErrors.
    DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
    -> Response_boot tcErr tcWarning warningsAndNonFatalErrors
    Resp_DisplayInfo DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    info

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

    parseAndDoAtToplevel
      :: (A.Expr -> TCM a)
         -- ^ The command to perform.
      -> String
         -- ^ The expression to parse.
      -> CommandM (Maybe CPUTime, a)
    parseAndDoAtToplevel :: forall a. (Expr -> TCM a) -> String -> CommandM (Maybe CPUTime, a)
    parseAndDoAtToplevel Expr -> TCM a
    cmd String
    s = do
      CommandM (Maybe CPUTime, a) -> CommandM (Maybe CPUTime, a)
    forall a. CommandM a -> CommandM a
    localStateCommandM (CommandM (Maybe CPUTime, a) -> CommandM (Maybe CPUTime, a))
    -> CommandM (Maybe CPUTime, a) -> CommandM (Maybe CPUTime, a)
    forall a b. (a -> b) -> a -> b
    $ do
        (e, attrs) <- TCM (Expr, Attributes)
    -> StateT CommandState TCM (Expr, Attributes)
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM (Expr, Attributes)
     -> StateT CommandState TCM (Expr, Attributes))
    -> TCM (Expr, Attributes)
    -> StateT CommandState TCM (Expr, Attributes)
    forall a b. (a -> b) -> a -> b
    $ PM (Expr, Attributes) -> TCM (Expr, Attributes)
    forall a. PM a -> TCM a
    runPM (PM (Expr, Attributes) -> TCM (Expr, Attributes))
    -> PM (Expr, Attributes) -> TCM (Expr, Attributes)
    forall a b. (a -> b) -> a -> b
    $ Parser Expr -> String -> PM (Expr, Attributes)
    forall a. Parser a -> String -> PM (a, Attributes)
    parse Parser Expr
    exprParser String
    s
        lift $ checkAttributes attrs
        maybeTimed $ atTopLevel $ lift $
          cmd =<< concreteToAbstract_ e

    maybeTimed :: CommandM a -> CommandM (Maybe CPUTime, a)
    maybeTimed :: forall a. CommandM a -> CommandM (Maybe CPUTime, a)
    maybeTimed CommandM a
    work = do
      doTime <- TCMT IO Bool -> StateT CommandState TCM Bool
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO Bool -> StateT CommandState TCM Bool)
    -> TCMT IO Bool -> StateT CommandState TCM Bool
    forall a b. (a -> b) -> a -> b
    $ ProfileOption -> TCMT IO Bool
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m Bool
    hasProfileOption ProfileOption
    Profile.Interactive
      if not doTime
        then (Nothing,) <$> work
        else do
          (r, time) <- measureTime work
          return (Just time, r)

    -- | Tell to highlight the code using the given highlighting
    -- info (unless it is @Nothing@).

    tellToUpdateHighlighting
      :: Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource) -> IO [Response]
    tellToUpdateHighlighting :: Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    -> IO [Response]
    tellToUpdateHighlighting Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
    Nothing                = [Response] -> IO [Response]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
    tellToUpdateHighlighting (Just (HighlightingInfo
    info, HighlightingMethod
    method, ModuleToSource
    modFile)) =
      [Response] -> IO [Response]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [HighlightingInfo
    -> RemoveTokenBasedHighlighting
    -> HighlightingMethod
    -> ModuleToSource
    -> Response
    forall tcErr tcWarning warningsAndNonFatalErrors.
    HighlightingInfo
    -> RemoveTokenBasedHighlighting
    -> HighlightingMethod
    -> ModuleToSource
    -> Response_boot tcErr tcWarning warningsAndNonFatalErrors
    Resp_HighlightingInfo HighlightingInfo
    info RemoveTokenBasedHighlighting
    KeepHighlighting HighlightingMethod
    method ModuleToSource
    modFile]

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

    tellEmacsToJumpToError :: Range -> [Response]
    tellEmacsToJumpToError :: Range -> [Response]
    tellEmacsToJumpToError Range
    r =
      case Range -> Maybe (Position' (Maybe RangeFile))
    forall a. Range' a -> Maybe (Position' a)
    rStart Range
    r of
        Maybe (Position' (Maybe RangeFile))
    Nothing                                           -> []
        Just (Pn { srcFile :: forall a. Position' a -> a
    srcFile = Maybe RangeFile
    Strict.Nothing })            -> []
        Just (Pn { srcFile :: forall a. Position' a -> a
    srcFile = Strict.Just RangeFile
    f, posPos :: forall a. Position' a -> Word32
    posPos = Word32
    p }) ->
           [ String -> Word32 -> Response
    forall tcErr tcWarning warningsAndNonFatalErrors.
    String
    -> Word32
    -> Response_boot tcErr tcWarning warningsAndNonFatalErrors
    Resp_JumpToError (AbsolutePath -> String
    filePath (RangeFile -> AbsolutePath
    rangeFilePath RangeFile
    f)) Word32
    p ]