    module Agda.Interaction.CommandLine
      ( runInteractionLoop
      ) where

    import Control.Monad
    import Control.Monad.Except
    import Control.Monad.IO.Class ( MonadIO(..) )
    import Control.Monad.State
    import Control.Monad.Reader

    import qualified Data.List as List
    import Data.Maybe

    import Text.Read (readMaybe)

    import Agda.Interaction.Base hiding (Command)
    import Agda.Interaction.BasicOps as BasicOps hiding (parseExpr)
    import Agda.Interaction.Imports ( CheckResult, crInterface )
    import Agda.Interaction.Monad

    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Common
    import Agda.Syntax.Internal (telToList, alwaysUnblock)
    import qualified Agda.Syntax.Internal as I
    import Agda.Syntax.Parser
    import Agda.Syntax.Position
    import Agda.Syntax.Scope.Base
    import Agda.Syntax.Translation.ConcreteToAbstract
    import Agda.Syntax.Abstract.Pretty

    import Agda.TypeChecking.Constraints
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Errors
    import Agda.TypeChecking.Pretty ( PrettyTCM(prettyTCM) )
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Warnings (runPM)

    import Agda.Utils.FileName (absolute, AbsolutePath)
    import Agda.Utils.Maybe (caseMaybeM)
    import Agda.Utils.Pretty

    import Agda.Utils.Impossible

    data ReplEnv = ReplEnv
        { ReplEnv -> TCM ()
    replSetupAction     :: TCM ()
        , ReplEnv -> AbsolutePath -> TCM CheckResult
    replTypeCheckAction :: AbsolutePath -> TCM CheckResult
        }

    data ReplState = ReplState
        { ReplState -> Maybe AbsolutePath
    currentFile :: Maybe AbsolutePath
        }

    newtype ReplM a = ReplM { forall a. ReplM a -> ReaderT ReplEnv (StateT ReplState IM) a
    unReplM :: ReaderT ReplEnv (StateT ReplState IM) a }
        deriving
        ( (forall a b. (a -> b) -> ReplM a -> ReplM b)
    -> (forall a b. a -> ReplM b -> ReplM a) -> Functor ReplM
    forall a b. a -> ReplM b -> ReplM a
    forall a b. (a -> b) -> ReplM a -> ReplM b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> ReplM b -> ReplM a
    $c<$ :: forall a b. a -> ReplM b -> ReplM a
    fmap :: forall a b. (a -> b) -> ReplM a -> ReplM b
    $cfmap :: forall a b. (a -> b) -> ReplM a -> ReplM b
    Functor, Functor ReplM
    Functor ReplM
    -> (forall a. a -> ReplM a)
    -> (forall a b. ReplM (a -> b) -> ReplM a -> ReplM b)
    -> (forall a b c. (a -> b -> c) -> ReplM a -> ReplM b -> ReplM c)
    -> (forall a b. ReplM a -> ReplM b -> ReplM b)
    -> (forall a b. ReplM a -> ReplM b -> ReplM a)
    -> Applicative ReplM
    forall a. a -> ReplM a
    forall a b. ReplM a -> ReplM b -> ReplM a
    forall a b. ReplM a -> ReplM b -> ReplM b
    forall a b. ReplM (a -> b) -> ReplM a -> ReplM b
    forall a b c. (a -> b -> c) -> ReplM a -> ReplM b -> ReplM c
    forall (f :: * -> *).
    Functor f
    -> (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    <* :: forall a b. ReplM a -> ReplM b -> ReplM a
    $c<* :: forall a b. ReplM a -> ReplM b -> ReplM a
    *> :: forall a b. ReplM a -> ReplM b -> ReplM b
    $c*> :: forall a b. ReplM a -> ReplM b -> ReplM b
    liftA2 :: forall a b c. (a -> b -> c) -> ReplM a -> ReplM b -> ReplM c
    $cliftA2 :: forall a b c. (a -> b -> c) -> ReplM a -> ReplM b -> ReplM c
    <*> :: forall a b. ReplM (a -> b) -> ReplM a -> ReplM b
    $c<*> :: forall a b. ReplM (a -> b) -> ReplM a -> ReplM b
    pure :: forall a. a -> ReplM a
    $cpure :: forall a. a -> ReplM a
    Applicative, Applicative ReplM
    Applicative ReplM
    -> (forall a b. ReplM a -> (a -> ReplM b) -> ReplM b)
    -> (forall a b. ReplM a -> ReplM b -> ReplM b)
    -> (forall a. a -> ReplM a)
    -> Monad ReplM
    forall a. a -> ReplM a
    forall a b. ReplM a -> ReplM b -> ReplM b
    forall a b. ReplM a -> (a -> ReplM b) -> ReplM b
    forall (m :: * -> *).
    Applicative m
    -> (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    return :: forall a. a -> ReplM a
    $creturn :: forall a. a -> ReplM a
    >> :: forall a b. ReplM a -> ReplM b -> ReplM b
    $c>> :: forall a b. ReplM a -> ReplM b -> ReplM b
    >>= :: forall a b. ReplM a -> (a -> ReplM b) -> ReplM b
    $c>>= :: forall a b. ReplM a -> (a -> ReplM b) -> ReplM b
    Monad, Monad ReplM
    Monad ReplM -> (forall a. IO a -> ReplM a) -> MonadIO ReplM
    forall a. IO a -> ReplM a
    forall (m :: * -> *).
    Monad m -> (forall a. IO a -> m a) -> MonadIO m
    liftIO :: forall a. IO a -> ReplM a
    $cliftIO :: forall a. IO a -> ReplM a
    MonadIO
        , Monad ReplM
    Functor ReplM
    Applicative ReplM
    ReplM PragmaOptions
    ReplM CommandLineOptions
    Functor ReplM
    -> Applicative ReplM
    -> Monad ReplM
    -> ReplM PragmaOptions
    -> ReplM CommandLineOptions
    -> HasOptions ReplM
    forall (m :: * -> *).
    Functor m
    -> Applicative m
    -> Monad m
    -> m PragmaOptions
    -> m CommandLineOptions
    -> HasOptions m
    commandLineOptions :: ReplM CommandLineOptions
    $ccommandLineOptions :: ReplM CommandLineOptions
    pragmaOptions :: ReplM PragmaOptions
    $cpragmaOptions :: ReplM PragmaOptions
    HasOptions, Monad ReplM
    ReplM TCEnv
    Monad ReplM
    -> ReplM TCEnv
    -> (forall a. (TCEnv -> TCEnv) -> ReplM a -> ReplM a)
    -> MonadTCEnv ReplM
    forall a. (TCEnv -> TCEnv) -> ReplM a -> ReplM a
    forall (m :: * -> *).
    Monad m
    -> m TCEnv
    -> (forall a. (TCEnv -> TCEnv) -> m a -> m a)
    -> MonadTCEnv m
    localTC :: forall a. (TCEnv -> TCEnv) -> ReplM a -> ReplM a
    $clocalTC :: forall a. (TCEnv -> TCEnv) -> ReplM a -> ReplM a
    askTC :: ReplM TCEnv
    $caskTC :: ReplM TCEnv
    MonadTCEnv, Monad ReplM
    ReplM TCState
    Monad ReplM
    -> ReplM TCState
    -> (forall a b. Lens' a TCState -> (a -> a) -> ReplM b -> ReplM b)
    -> (forall a. (TCState -> TCState) -> ReplM a -> ReplM a)
    -> ReadTCState ReplM
    forall a. (TCState -> TCState) -> ReplM a -> ReplM a
    forall a b. Lens' a TCState -> (a -> a) -> ReplM b -> ReplM b
    forall (m :: * -> *).
    Monad m
    -> m TCState
    -> (forall a b. Lens' a TCState -> (a -> a) -> m b -> m b)
    -> (forall a. (TCState -> TCState) -> m a -> m a)
    -> ReadTCState m
    withTCState :: forall a. (TCState -> TCState) -> ReplM a -> ReplM a
    $cwithTCState :: forall a. (TCState -> TCState) -> ReplM a -> ReplM a
    locallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> ReplM b -> ReplM b
    $clocallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> ReplM b -> ReplM b
    getTCState :: ReplM TCState
    $cgetTCState :: ReplM TCState
    ReadTCState, Monad ReplM
    ReplM TCState
    Monad ReplM
    -> ReplM TCState
    -> (TCState -> ReplM ())
    -> ((TCState -> TCState) -> ReplM ())
    -> MonadTCState ReplM
    TCState -> ReplM ()
    (TCState -> TCState) -> ReplM ()
    forall (m :: * -> *).
    Monad m
    -> m TCState
    -> (TCState -> m ())
    -> ((TCState -> TCState) -> m ())
    -> MonadTCState m
    modifyTC :: (TCState -> TCState) -> ReplM ()
    $cmodifyTC :: (TCState -> TCState) -> ReplM ()
    putTC :: TCState -> ReplM ()
    $cputTC :: TCState -> ReplM ()
    getTC :: ReplM TCState
    $cgetTC :: ReplM TCState
    MonadTCState, Applicative ReplM
    MonadIO ReplM
    HasOptions ReplM
    MonadTCState ReplM
    MonadTCEnv ReplM
    Applicative ReplM
    -> MonadIO ReplM
    -> MonadTCEnv ReplM
    -> MonadTCState ReplM
    -> HasOptions ReplM
    -> (forall a. TCM a -> ReplM a)
    -> MonadTCM ReplM
    forall a. TCM a -> ReplM a
    forall (tcm :: * -> *).
    Applicative tcm
    -> MonadIO tcm
    -> MonadTCEnv tcm
    -> MonadTCState tcm
    -> HasOptions tcm
    -> (forall a. TCM a -> tcm a)
    -> MonadTCM tcm
    liftTCM :: forall a. TCM a -> ReplM a
    $cliftTCM :: forall a. TCM a -> ReplM a
    MonadTCM
        , MonadError TCErr
        , MonadReader ReplEnv, MonadState ReplState
        )

    runReplM :: Maybe AbsolutePath -> TCM () -> (AbsolutePath -> TCM CheckResult) -> ReplM () -> TCM ()
    runReplM :: Maybe AbsolutePath
    -> TCM ()
    -> (AbsolutePath -> TCM CheckResult)
    -> ReplM ()
    -> TCM ()
    runReplM Maybe AbsolutePath
    initialFile TCM ()
    setup AbsolutePath -> TCM CheckResult
    checkInterface
        = IM () -> TCM ()
    forall a. IM a -> TCM a
    runIM
        (IM () -> TCM ()) -> (ReplM () -> IM ()) -> ReplM () -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (StateT ReplState IM () -> ReplState -> IM ())
    -> ReplState -> StateT ReplState IM () -> IM ()
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip StateT ReplState IM () -> ReplState -> IM ()
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    evalStateT (Maybe AbsolutePath -> ReplState
    ReplState Maybe AbsolutePath
    initialFile)
        (StateT ReplState IM () -> IM ())
    -> (ReplM () -> StateT ReplState IM ()) -> ReplM () -> IM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ReaderT ReplEnv (StateT ReplState IM) ()
     -> ReplEnv -> StateT ReplState IM ())
    -> ReplEnv
    -> ReaderT ReplEnv (StateT ReplState IM) ()
    -> StateT ReplState IM ()
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ReaderT ReplEnv (StateT ReplState IM) ()
    -> ReplEnv -> StateT ReplState IM ()
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT ReplEnv
    replEnv
        (ReaderT ReplEnv (StateT ReplState IM) ()
     -> StateT ReplState IM ())
    -> (ReplM () -> ReaderT ReplEnv (StateT ReplState IM) ())
    -> ReplM ()
    -> StateT ReplState IM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ReplM () -> ReaderT ReplEnv (StateT ReplState IM) ()
    forall a. ReplM a -> ReaderT ReplEnv (StateT ReplState IM) a
    unReplM
      where
      replEnv :: ReplEnv
    replEnv = ReplEnv :: TCM () -> (AbsolutePath -> TCM CheckResult) -> ReplEnv
    ReplEnv
        { replSetupAction :: TCM ()
    replSetupAction     = TCM ()
    setup
        , replTypeCheckAction :: AbsolutePath -> TCM CheckResult
    replTypeCheckAction = AbsolutePath -> TCM CheckResult
    checkInterface
        }

    data ExitCode a = Continue | ContinueIn TCEnv | Return a

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

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

    interaction :: String -> [Command a] -> (String -> TCM (ExitCode a)) -> ReplM a
    interaction :: forall a.
    String -> [Command a] -> (String -> TCM (ExitCode a)) -> ReplM a
    interaction String
    prompt [Command a]
    cmds String -> TCM (ExitCode a)
    eval = ReplM a
    loop
        where
            go :: ExitCode a -> ReplM a
    go (Return a
    x)       = a -> ReplM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x
            go ExitCode a
    Continue         = ReplM a
    loop
            go (ContinueIn TCEnv
    env) = (TCEnv -> TCEnv) -> ReplM a -> ReplM a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (TCEnv -> TCEnv -> TCEnv
    forall a b. a -> b -> a
    const TCEnv
    env) ReplM a
    loop

            loop :: ReplM a
    loop =
                do  Maybe String
    ms <- ReaderT ReplEnv (StateT ReplState IM) (Maybe String)
    -> ReplM (Maybe String)
    forall a. ReaderT ReplEnv (StateT ReplState IM) a -> ReplM a
    ReplM (ReaderT ReplEnv (StateT ReplState IM) (Maybe String)
     -> ReplM (Maybe String))
    -> ReaderT ReplEnv (StateT ReplState IM) (Maybe String)
    -> ReplM (Maybe String)
    forall a b. (a -> b) -> a -> b
    $ StateT ReplState IM (Maybe String)
    -> ReaderT ReplEnv (StateT ReplState IM) (Maybe String)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (StateT ReplState IM (Maybe String)
     -> ReaderT ReplEnv (StateT ReplState IM) (Maybe String))
    -> StateT ReplState IM (Maybe String)
    -> ReaderT ReplEnv (StateT ReplState IM) (Maybe String)
    forall a b. (a -> b) -> a -> b
    $ IM (Maybe String) -> StateT ReplState IM (Maybe String)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IM (Maybe String) -> StateT ReplState IM (Maybe String))
    -> IM (Maybe String) -> StateT ReplState IM (Maybe String)
    forall a b. (a -> b) -> a -> b
    $ String -> IM (Maybe String)
    readline String
    prompt
                    case (String -> [String]) -> Maybe String -> Maybe [String]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap String -> [String]
    words Maybe String
    ms of
                        Maybe [String]
    Nothing               -> a -> ReplM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> ReplM a) -> a -> ReplM a
    forall a b. (a -> b) -> a -> b
    $ String -> a
    forall a. HasCallStack => String -> a
    error String
    "** EOF **"
                        Just []               -> ReplM a
    loop
                        Just ((Char
    ':':String
    cmd):[String]
    args) ->
                            do  case String
    -> [Command a] -> Either [String] ([String] -> ReplM (ExitCode a))
    forall a.
    String
    -> [Command a] -> Either [String] ([String] -> ReplM (ExitCode a))
    matchCommand String
    cmd [Command a]
    cmds of
                                    Right [String] -> ReplM (ExitCode a)
    c -> ExitCode a -> ReplM a
    go (ExitCode a -> ReplM a) -> ReplM (ExitCode a) -> ReplM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ([String] -> ReplM (ExitCode a)
    c [String]
    args)
                                    Left [] ->
                                        do  IO () -> ReplM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Unknown command '" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cmd String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "'"
                                            ReplM a
    loop
                                    Left [String]
    xs ->
                                        do  IO () -> ReplM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "More than one command match: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
                                                                String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    List.intercalate String
    ", " [String]
    xs
                                            ReplM a
    loop
                        Just [String]
    _ ->
                            do  ExitCode a -> ReplM a
    go (ExitCode a -> ReplM a) -> ReplM (ExitCode a) -> ReplM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCM (ExitCode a) -> ReplM (ExitCode a)
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (String -> TCM (ExitCode a)
    eval (String -> TCM (ExitCode a)) -> String -> TCM (ExitCode a)
    forall a b. (a -> b) -> a -> b
    $ Maybe String -> String
    forall a. HasCallStack => Maybe a -> a
    fromJust Maybe String
    ms)
                ReplM a -> (TCErr -> ReplM a) -> ReplM a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \TCErr
    e ->
                    do  String
    s <- TCErr -> ReplM String
    forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
    prettyError TCErr
    e
                        IO () -> ReplM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn String
    s
                        ReplM a
    loop

    runInteractionLoop :: Maybe AbsolutePath -> TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM ()
    runInteractionLoop :: Maybe AbsolutePath
    -> TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM ()
    runInteractionLoop Maybe AbsolutePath
    initialFile TCM ()
    setup AbsolutePath -> TCM CheckResult
    check = Maybe AbsolutePath
    -> TCM ()
    -> (AbsolutePath -> TCM CheckResult)
    -> ReplM ()
    -> TCM ()
    runReplM Maybe AbsolutePath
    initialFile TCM ()
    setup AbsolutePath -> TCM CheckResult
    check ReplM ()
    interactionLoop

    replSetup :: ReplM ()
    replSetup :: ReplM ()
    replSetup = do
        TCM () -> ReplM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReplM ()) -> ReplM (TCM ()) -> ReplM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (ReplEnv -> TCM ()) -> ReplM (TCM ())
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks ReplEnv -> TCM ()
    replSetupAction
        IO () -> ReplM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStr String
    splashScreen

    checkCurrentFile :: ReplM (Maybe CheckResult)
    checkCurrentFile :: ReplM (Maybe CheckResult)
    checkCurrentFile = (AbsolutePath -> ReplM CheckResult)
    -> Maybe AbsolutePath -> ReplM (Maybe CheckResult)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse AbsolutePath -> ReplM CheckResult
    checkFile (Maybe AbsolutePath -> ReplM (Maybe CheckResult))
    -> ReplM (Maybe AbsolutePath) -> ReplM (Maybe CheckResult)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (ReplState -> Maybe AbsolutePath) -> ReplM (Maybe AbsolutePath)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ReplState -> Maybe AbsolutePath
    currentFile

    checkFile :: AbsolutePath -> ReplM CheckResult
    checkFile :: AbsolutePath -> ReplM CheckResult
    checkFile AbsolutePath
    file = TCM CheckResult -> ReplM CheckResult
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM CheckResult -> ReplM CheckResult)
    -> ((AbsolutePath -> TCM CheckResult) -> TCM CheckResult)
    -> (AbsolutePath -> TCM CheckResult)
    -> ReplM CheckResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((AbsolutePath -> TCM CheckResult)
    -> AbsolutePath -> TCM CheckResult
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath
    file) ((AbsolutePath -> TCM CheckResult) -> ReplM CheckResult)
    -> ReplM (AbsolutePath -> TCM CheckResult) -> ReplM CheckResult
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (ReplEnv -> AbsolutePath -> TCM CheckResult)
    -> ReplM (AbsolutePath -> TCM CheckResult)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks ReplEnv -> AbsolutePath -> TCM CheckResult
    replTypeCheckAction

    -- | The interaction loop.
    interactionLoop :: ReplM ()
    interactionLoop :: ReplM ()
    interactionLoop = do
        -- Run the setup action
        ReplM ()
    replSetup
        ReplM ()
    reload
        String -> [Command ()] -> (String -> TCM (ExitCode ())) -> ReplM ()
    forall a.
    String -> [Command a] -> (String -> TCM (ExitCode a)) -> ReplM a
    interaction String
    "Main> " [Command ()]
    commands String -> TCM (ExitCode ())
    forall a. String -> TCM (ExitCode a)
    evalTerm
        where
            ReplM ()
    reload :: ReplM () = do
                Maybe CheckResult
    checked <- ReplM (Maybe CheckResult)
    checkCurrentFile
                TCM () -> ReplM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReplM ()) -> TCM () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ ScopeInfo -> TCM ()
    setScope (ScopeInfo -> TCM ()) -> ScopeInfo -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ScopeInfo
    -> (Interface -> ScopeInfo) -> Maybe Interface -> ScopeInfo
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe ScopeInfo
    emptyScopeInfo Interface -> ScopeInfo
    iInsideScope (CheckResult -> Interface
    crInterface (CheckResult -> Interface) -> Maybe CheckResult -> Maybe Interface
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe CheckResult
    checked)
                -- Andreas, 2021-01-27, issue #5132, make Set and Prop available from Agda.Primitive
                -- if no module is loaded.
                Bool -> ReplM () -> ReplM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Maybe CheckResult -> Bool
    forall a. Maybe a -> Bool
    isNothing Maybe CheckResult
    checked) (ReplM () -> ReplM ()) -> ReplM () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ do
                  -- @open import Agda.Primitive using (Set; Prop)@
                  ReplM [Declaration] -> ReplM ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (ReplM [Declaration] -> ReplM ())
    -> ReplM [Declaration] -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ TCM [Declaration] -> ReplM [Declaration]
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM TCM [Declaration]
    importPrimitives
              ReplM () -> (TCErr -> ReplM ()) -> ReplM ()
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \TCErr
    e -> do
                String
    s <- TCErr -> ReplM String
    forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
    prettyError TCErr
    e
                IO () -> ReplM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn String
    s
                IO () -> ReplM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn String
    "Failed."

            commands :: [Command ()]
    commands =
                [ String
    "quit"        String -> ([String] -> ReplM (ExitCode ())) -> Command ()
    forall {a} {b}. a -> b -> (a, b)
    |>  \[String]
    _ -> ExitCode () -> ReplM (ExitCode ())
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExitCode () -> ReplM (ExitCode ()))
    -> ExitCode () -> ReplM (ExitCode ())
    forall a b. (a -> b) -> a -> b
    $ () -> ExitCode ()
    forall a. a -> ExitCode a
    Return ()
                , String
    "?"           String -> ([String] -> ReplM (ExitCode ())) -> Command ()
    forall {a} {b}. a -> b -> (a, b)
    |>  \[String]
    _ -> ReplM () -> ReplM (ExitCode ())
    forall a b. ReplM a -> ReplM (ExitCode b)
    continueAfter (ReplM () -> ReplM (ExitCode ()))
    -> ReplM () -> ReplM (ExitCode ())
    forall a b. (a -> b) -> a -> b
    $ IO () -> ReplM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ [Command ()] -> IO ()
    forall a. [Command a] -> IO ()
    help [Command ()]
    commands
                , String
    "reload"      String -> ([String] -> ReplM (ExitCode ())) -> Command ()
    forall {a} {b}. a -> b -> (a, b)
    |>  \[String]
    _ -> do ReplM ()
    reload
                                             TCEnv -> ExitCode ()
    forall a. TCEnv -> ExitCode a
    ContinueIn (TCEnv -> ExitCode ()) -> ReplM TCEnv -> ReplM (ExitCode ())
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReplM TCEnv
    forall (m :: * -> *). MonadTCEnv m => m TCEnv
    askTC
                , String
    "constraints" String -> ([String] -> ReplM (ExitCode ())) -> Command ()
    forall {a} {b}. a -> b -> (a, b)
    |> \[String]
    args -> ReplM () -> ReplM (ExitCode ())
    forall a b. ReplM a -> ReplM (ExitCode b)
    continueAfter (ReplM () -> ReplM (ExitCode ()))
    -> ReplM () -> ReplM (ExitCode ())
    forall a b. (a -> b) -> a -> b
    $ TCM () -> ReplM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReplM ()) -> TCM () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> TCM ()
    showConstraints [String]
    args
                , String
    "Context"     String -> ([String] -> ReplM (ExitCode ())) -> Command ()
    forall {a} {b}. a -> b -> (a, b)
    |> \[String]
    args -> ReplM () -> ReplM (ExitCode ())
    forall a b. ReplM a -> ReplM (ExitCode b)
    continueAfter (ReplM () -> ReplM (ExitCode ()))
    -> ReplM () -> ReplM (ExitCode ())
    forall a b. (a -> b) -> a -> b
    $ TCM () -> ReplM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReplM ()) -> TCM () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> TCM ()
    showContext [String]
    args
                , String
    "give"        String -> ([String] -> ReplM (ExitCode ())) -> Command ()
    forall {a} {b}. a -> b -> (a, b)
    |> \[String]
    args -> ReplM () -> ReplM (ExitCode ())
    forall a b. ReplM a -> ReplM (ExitCode b)
    continueAfter (ReplM () -> ReplM (ExitCode ()))
    -> ReplM () -> ReplM (ExitCode ())
    forall a b. (a -> b) -> a -> b
    $ TCM () -> ReplM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReplM ()) -> TCM () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> TCM ()
    giveMeta [String]
    args
                , String
    "Refine"      String -> ([String] -> ReplM (ExitCode ())) -> Command ()
    forall {a} {b}. a -> b -> (a, b)
    |> \[String]
    args -> ReplM () -> ReplM (ExitCode ())
    forall a b. ReplM a -> ReplM (ExitCode b)
    continueAfter (ReplM () -> ReplM (ExitCode ()))
    -> ReplM () -> ReplM (ExitCode ())
    forall a b. (a -> b) -> a -> b
    $ TCM () -> ReplM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReplM ()) -> TCM () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> TCM ()
    refineMeta [String]
    args
                , String
    "metas"       String -> ([String] -> ReplM (ExitCode ())) -> Command ()
    forall {a} {b}. a -> b -> (a, b)
    |> \[String]
    args -> ReplM () -> ReplM (ExitCode ())
    forall a b. ReplM a -> ReplM (ExitCode b)
    continueAfter (ReplM () -> ReplM (ExitCode ()))
    -> ReplM () -> ReplM (ExitCode ())
    forall a b. (a -> b) -> a -> b
    $ TCM () -> ReplM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReplM ()) -> TCM () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> TCM ()
    showMetas [String]
    args
                , String
    "load"        String -> ([String] -> ReplM (ExitCode ())) -> Command ()
    forall {a} {b}. a -> b -> (a, b)
    |> \[String]
    args -> ReplM () -> ReplM (ExitCode ())
    forall a b. ReplM a -> ReplM (ExitCode b)
    continueAfter (ReplM () -> ReplM (ExitCode ()))
    -> ReplM () -> ReplM (ExitCode ())
    forall a b. (a -> b) -> a -> b
    $ ReplM () -> [String] -> ReplM ()
    loadFile ReplM ()
    reload [String]
    args
                , String
    "eval"        String -> ([String] -> ReplM (ExitCode ())) -> Command ()
    forall {a} {b}. a -> b -> (a, b)
    |> \[String]
    args -> ReplM () -> ReplM (ExitCode ())
    forall a b. ReplM a -> ReplM (ExitCode b)
    continueAfter (ReplM () -> ReplM (ExitCode ()))
    -> ReplM () -> ReplM (ExitCode ())
    forall a b. (a -> b) -> a -> b
    $ TCM () -> ReplM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReplM ()) -> TCM () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> TCM ()
    evalIn [String]
    args
                , String
    "typeOf"      String -> ([String] -> ReplM (ExitCode ())) -> Command ()
    forall {a} {b}. a -> b -> (a, b)
    |> \[String]
    args -> ReplM () -> ReplM (ExitCode ())
    forall a b. ReplM a -> ReplM (ExitCode b)
    continueAfter (ReplM () -> ReplM (ExitCode ()))
    -> ReplM () -> ReplM (ExitCode ())
    forall a b. (a -> b) -> a -> b
    $ TCM () -> ReplM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReplM ()) -> TCM () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> TCM ()
    typeOf [String]
    args
                , String
    "typeIn"      String -> ([String] -> ReplM (ExitCode ())) -> Command ()
    forall {a} {b}. a -> b -> (a, b)
    |> \[String]
    args -> ReplM () -> ReplM (ExitCode ())
    forall a b. ReplM a -> ReplM (ExitCode b)
    continueAfter (ReplM () -> ReplM (ExitCode ()))
    -> ReplM () -> ReplM (ExitCode ())
    forall a b. (a -> b) -> a -> b
    $ TCM () -> ReplM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReplM ()) -> TCM () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> TCM ()
    typeIn [String]
    args
                , String
    "wakeup"      String -> ([String] -> ReplM (ExitCode ())) -> Command ()
    forall {a} {b}. a -> b -> (a, b)
    |> \[String]
    _ -> ReplM () -> ReplM (ExitCode ())
    forall a b. ReplM a -> ReplM (ExitCode b)
    continueAfter (ReplM () -> ReplM (ExitCode ()))
    -> ReplM () -> ReplM (ExitCode ())
    forall a b. (a -> b) -> a -> b
    $ TCM () -> ReplM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReplM ()) -> TCM () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ TCM ()
    retryConstraints
                , String
    "scope"       String -> ([String] -> ReplM (ExitCode ())) -> Command ()
    forall {a} {b}. a -> b -> (a, b)
    |> \[String]
    _ -> ReplM () -> ReplM (ExitCode ())
    forall a b. ReplM a -> ReplM (ExitCode b)
    continueAfter (ReplM () -> ReplM (ExitCode ()))
    -> ReplM () -> ReplM (ExitCode ())
    forall a b. (a -> b) -> a -> b
    $ TCM () -> ReplM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReplM ()) -> TCM () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ TCM ()
    showScope
                ]
                where
                    |> :: a -> b -> (a, b)
    (|>) = (,)

    continueAfter :: ReplM a -> ReplM (ExitCode b)
    continueAfter :: forall a b. ReplM a -> ReplM (ExitCode b)
    continueAfter ReplM a
    m = ReplM (ExitCode b) -> ReplM (ExitCode b)
    forall a. ReplM a -> ReplM a
    withCurrentFile (ReplM (ExitCode b) -> ReplM (ExitCode b))
    -> ReplM (ExitCode b) -> ReplM (ExitCode b)
    forall a b. (a -> b) -> a -> b
    $ do
      ReplM a
    m ReplM a -> ReplM (ExitCode b) -> ReplM (ExitCode b)
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> ExitCode b -> ReplM (ExitCode b)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ExitCode b
    forall a. ExitCode a
    Continue

    -- | Set 'envCurrentPath' to the repl's current file
    withCurrentFile :: ReplM a -> ReplM a
    withCurrentFile :: forall a. ReplM a -> ReplM a
    withCurrentFile ReplM a
    cont = do
      Maybe AbsolutePath
    mpath <- (ReplState -> Maybe AbsolutePath) -> ReplM (Maybe AbsolutePath)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ReplState -> Maybe AbsolutePath
    currentFile
      (TCEnv -> TCEnv) -> ReplM a -> ReplM a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\ TCEnv
    e -> TCEnv
    e { envCurrentPath :: Maybe AbsolutePath
    envCurrentPath = Maybe AbsolutePath
    mpath }) ReplM a
    cont

    loadFile :: ReplM () -> [String] -> ReplM ()
    loadFile :: ReplM () -> [String] -> ReplM ()
    loadFile ReplM ()
    reload [String
    file] = do
      AbsolutePath
    absPath <- IO AbsolutePath -> ReplM AbsolutePath
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO AbsolutePath -> ReplM AbsolutePath)
    -> IO AbsolutePath -> ReplM AbsolutePath
    forall a b. (a -> b) -> a -> b
    $ String -> IO AbsolutePath
    absolute String
    file
      (ReplState -> ReplState) -> ReplM ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (\(ReplState Maybe AbsolutePath
    _prevFile) -> Maybe AbsolutePath -> ReplState
    ReplState (AbsolutePath -> Maybe AbsolutePath
    forall a. a -> Maybe a
    Just AbsolutePath
    absPath))
      ReplM () -> ReplM ()
    forall a. ReplM a -> ReplM a
    withCurrentFile ReplM ()
    reload
    loadFile ReplM ()
    _ [String]
    _ = IO () -> ReplM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn String
    ":load file"

    showConstraints :: [String] -> TCM ()
    showConstraints :: [String] -> TCM ()
    showConstraints [] =
        do  [OutputForm Expr Expr]
    cs <- TCM [OutputForm Expr Expr]
    BasicOps.getConstraints
            IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines ((OutputForm Expr Expr -> String)
    -> [OutputForm Expr Expr] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    List.map OutputForm Expr Expr -> String
    forall a. Pretty a => a -> String
    prettyShow [OutputForm Expr Expr]
    cs)
    showConstraints [String]
    _ = IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn String
    ":constraints [cid]"

    showMetas :: [String] -> TCM ()
    showMetas :: [String] -> TCM ()
    showMetas [String
    m] =
        do  InteractionId
    i <- Nat -> InteractionId
    InteractionId (Nat -> InteractionId) -> TCMT IO Nat -> TCMT IO InteractionId
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> TCMT IO Nat
    forall a. Read a => String -> TCM a
    readM String
    m
            InteractionId -> TCM () -> TCM ()
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    i (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
              OutputConstraint Expr InteractionId
    s <- Rewrite
    -> InteractionId -> TCM (OutputConstraint Expr InteractionId)
    typeOfMeta Rewrite
    AsIs InteractionId
    i
              Range
    r <- InteractionId -> TCMT IO Range
    forall (m :: * -> *).
    (MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
    InteractionId -> m Range
    getInteractionRange InteractionId
    i
              Doc
    d <- OutputConstraint Expr InteractionId -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA OutputConstraint Expr InteractionId
    s
              IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> String
    render Doc
    d String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Range -> String
    forall a. Pretty a => a -> String
    prettyShow Range
    r
    showMetas [String
    m,String
    "normal"] =
        do  InteractionId
    i <- Nat -> InteractionId
    InteractionId (Nat -> InteractionId) -> TCMT IO Nat -> TCMT IO InteractionId
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> TCMT IO Nat
    forall a. Read a => String -> TCM a
    readM String
    m
            InteractionId -> TCM () -> TCM ()
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    i (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
              Doc
    s <- OutputConstraint Expr InteractionId -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (OutputConstraint Expr InteractionId -> TCMT IO Doc)
    -> TCM (OutputConstraint Expr InteractionId) -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Rewrite
    -> InteractionId -> TCM (OutputConstraint Expr InteractionId)
    typeOfMeta Rewrite
    Normalised InteractionId
    i
              Range
    r <- InteractionId -> TCMT IO Range
    forall (m :: * -> *).
    (MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
    InteractionId -> m Range
    getInteractionRange InteractionId
    i
              IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> String
    render Doc
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Range -> String
    forall a. Pretty a => a -> String
    prettyShow Range
    r
    showMetas [] =
        do  [OutputConstraint Expr InteractionId]
    interactionMetas <- Rewrite -> TCM [OutputConstraint Expr InteractionId]
    typesOfVisibleMetas Rewrite
    AsIs
            [OutputConstraint Expr NamedMeta]
    hiddenMetas      <- Rewrite -> TCM [OutputConstraint Expr NamedMeta]
    typesOfHiddenMetas  Rewrite
    AsIs
            (Doc -> TCM ()) -> [Doc] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> (Doc -> IO ()) -> Doc -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> IO ()
    forall a. Show a => a -> IO ()
    print) ([Doc] -> TCM ()) -> TCMT IO [Doc] -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (OutputConstraint Expr InteractionId -> TCMT IO Doc)
    -> [OutputConstraint Expr InteractionId] -> TCMT IO [Doc]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM OutputConstraint Expr InteractionId -> TCMT IO Doc
    forall {m :: * -> *} {a}.
    (MonadError TCErr m, MonadTrace m, ToConcrete a,
     Pretty (ConOfAbs a), MonadStConcreteNames m, HasOptions m,
     HasBuiltins m, MonadDebug m) =>
    OutputConstraint a InteractionId -> m Doc
    showII [OutputConstraint Expr InteractionId]
    interactionMetas
            (OutputConstraint Expr NamedMeta -> TCM ())
    -> [OutputConstraint Expr NamedMeta] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ OutputConstraint Expr NamedMeta -> TCM ()
    forall {m :: * -> *} {a}.
    (MonadTrace m, ToConcrete a, Pretty (ConOfAbs a),
     MonadStConcreteNames m, HasOptions m, HasBuiltins m, MonadDebug m,
     MonadIO m) =>
    OutputConstraint a NamedMeta -> m ()
    print' [OutputConstraint Expr NamedMeta]
    hiddenMetas
        where
            showII :: OutputConstraint a InteractionId -> m Doc
    showII OutputConstraint a InteractionId
    o = InteractionId -> m Doc -> m Doc
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId (OutputForm a InteractionId -> InteractionId
    forall a b. OutputForm a b -> b
    outputFormId (OutputForm a InteractionId -> InteractionId)
    -> OutputForm a InteractionId -> InteractionId
    forall a b. (a -> b) -> a -> b
    $ Range
    -> [ProblemId]
    -> Blocker
    -> OutputConstraint a InteractionId
    -> OutputForm a InteractionId
    forall a b.
    Range
    -> [ProblemId] -> Blocker -> OutputConstraint a b -> OutputForm a b
    OutputForm Range
    forall a. Range' a
    noRange [] Blocker
    alwaysUnblock OutputConstraint a InteractionId
    o) (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ OutputConstraint a InteractionId -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA OutputConstraint a InteractionId
    o
            showM :: OutputConstraint a NamedMeta -> m Doc
    showM  OutputConstraint a NamedMeta
    o = MetaId -> m Doc -> m Doc
    forall (m :: * -> *) a.
    (MonadFail m, MonadTCEnv m, ReadTCState m, MonadTrace m) =>
    MetaId -> m a -> m a
    withMetaId (NamedMeta -> MetaId
    nmid (NamedMeta -> MetaId) -> NamedMeta -> MetaId
    forall a b. (a -> b) -> a -> b
    $ OutputForm a NamedMeta -> NamedMeta
    forall a b. OutputForm a b -> b
    outputFormId (OutputForm a NamedMeta -> NamedMeta)
    -> OutputForm a NamedMeta -> NamedMeta
    forall a b. (a -> b) -> a -> b
    $ Range
    -> [ProblemId]
    -> Blocker
    -> OutputConstraint a NamedMeta
    -> OutputForm a NamedMeta
    forall a b.
    Range
    -> [ProblemId] -> Blocker -> OutputConstraint a b -> OutputForm a b
    OutputForm Range
    forall a. Range' a
    noRange [] Blocker
    alwaysUnblock OutputConstraint a NamedMeta
    o) (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ OutputConstraint a NamedMeta -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA OutputConstraint a NamedMeta
    o

            metaId :: OutputConstraint a b -> b
    metaId (OfType b
    i a
    _) = b
    i
            metaId (JustType b
    i) = b
    i
            metaId (JustSort b
    i) = b
    i
            metaId (Assign b
    i a
    e) = b
    i
            metaId OutputConstraint a b
    _ = b
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            print' :: OutputConstraint a NamedMeta -> m ()
    print' OutputConstraint a NamedMeta
    x = do
                Range
    r <- MetaId -> m Range
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Range
    getMetaRange (MetaId -> m Range) -> MetaId -> m Range
    forall a b. (a -> b) -> a -> b
    $ NamedMeta -> MetaId
    nmid (NamedMeta -> MetaId) -> NamedMeta -> MetaId
    forall a b. (a -> b) -> a -> b
    $ OutputConstraint a NamedMeta -> NamedMeta
    forall {a} {b}. OutputConstraint a b -> b
    metaId OutputConstraint a NamedMeta
    x
                Doc
    d <- OutputConstraint a NamedMeta -> m Doc
    forall {m :: * -> *} {a}.
    (MonadTrace m, ToConcrete a, Pretty (ConOfAbs a),
     MonadStConcreteNames m, HasOptions m, HasBuiltins m,
     MonadDebug m) =>
    OutputConstraint a NamedMeta -> m Doc
    showM OutputConstraint a NamedMeta
    x
                IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> String
    render Doc
    d String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "  [ at " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Range -> String
    forall a. Pretty a => a -> String
    prettyShow Range
    r String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " ]"
    showMetas [String]
    _ = IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    ":meta [metaid]"

    showScope :: TCM ()
    showScope :: TCM ()
    showScope = do
      ScopeInfo
    scope <- TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ ScopeInfo -> String
    forall a. Pretty a => a -> String
    prettyShow ScopeInfo
    scope

    metaParseExpr ::  InteractionId -> String -> TCM A.Expr
    metaParseExpr :: InteractionId -> String -> TCM Expr
    metaParseExpr InteractionId
    ii String
    s =
        do  MetaId
    m <- InteractionId -> TCMT IO MetaId
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    ii
            ScopeInfo
    scope <- MetaVariable -> ScopeInfo
    getMetaScope (MetaVariable -> ScopeInfo)
    -> TCMT IO MetaVariable -> TCMT IO ScopeInfo
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
            Range
    r <- MetaVariable -> Range
    forall a. HasRange a => a -> Range
    getRange (MetaVariable -> Range) -> TCMT IO MetaVariable -> TCMT IO Range
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
            -- liftIO $ putStrLn $ prettyShow scope
            let pos :: Position' SrcFile
    pos = Position' SrcFile -> Maybe (Position' SrcFile) -> Position' SrcFile
    forall a. a -> Maybe a -> a
    fromMaybe Position' SrcFile
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Range -> Maybe (Position' SrcFile)
    forall a. Range' a -> Maybe (Position' a)
    rStart Range
    r)
            Expr
    e <- PM Expr -> TCM Expr
    forall a. PM a -> TCM a
    runPM (PM Expr -> TCM Expr) -> PM Expr -> TCM Expr
    forall a b. (a -> b) -> a -> b
    $ Parser Expr -> Position' SrcFile -> String -> PM Expr
    forall a. Parser a -> Position' SrcFile -> String -> PM a
    parsePosString Parser Expr
    exprParser Position' SrcFile
    pos String
    s
            ScopeInfo -> Expr -> ScopeM (AbsOfCon Expr)
    forall c. ToAbstract c => ScopeInfo -> c -> ScopeM (AbsOfCon c)
    concreteToAbstract ScopeInfo
    scope Expr
    e

    actOnMeta :: [String] -> (InteractionId -> A.Expr -> TCM a) -> TCM a
    actOnMeta :: forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
    actOnMeta (String
    is:[String]
    es) InteractionId -> Expr -> TCM a
    f =
         do  Nat
    i <- String -> TCMT IO Nat
    forall a. Read a => String -> TCM a
    readM String
    is
             let ii :: InteractionId
    ii = Nat -> InteractionId
    InteractionId Nat
    i
             Expr
    e <- InteractionId -> String -> TCM Expr
    metaParseExpr InteractionId
    ii ([String] -> String
    unwords [String]
    es)
             InteractionId -> TCM a -> TCM a
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> Expr -> TCM a
    f InteractionId
    ii Expr
    e
    actOnMeta [String]
    _ InteractionId -> Expr -> TCM a
    _ = TCM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    giveMeta :: [String] -> TCM ()
    giveMeta :: [String] -> TCM ()
    giveMeta [String]
    s | [String] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [String]
    s Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Nat
    2 = do
      Expr
    _ <- [String] -> (InteractionId -> Expr -> TCM Expr) -> TCM Expr
    forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
    actOnMeta [String]
    s ((InteractionId -> Expr -> TCM Expr) -> TCM Expr)
    -> (InteractionId -> Expr -> TCM Expr) -> TCM Expr
    forall a b. (a -> b) -> a -> b
    $ \ InteractionId
    ii Expr
    e -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    give UseForce
    WithoutForce InteractionId
    ii Maybe Range
    forall a. Maybe a
    Nothing Expr
    e
      () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    giveMeta [String]
    _ = IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    ": give" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " metaid expr"

    refineMeta :: [String] -> TCM ()
    refineMeta :: [String] -> TCM ()
    refineMeta [String]
    s | [String] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [String]
    s Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Nat
    2 = do
      Expr
    _ <- [String] -> (InteractionId -> Expr -> TCM Expr) -> TCM Expr
    forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
    actOnMeta [String]
    s ((InteractionId -> Expr -> TCM Expr) -> TCM Expr)
    -> (InteractionId -> Expr -> TCM Expr) -> TCM Expr
    forall a b. (a -> b) -> a -> b
    $ \ InteractionId
    ii Expr
    e -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
    refine UseForce
    WithoutForce InteractionId
    ii Maybe Range
    forall a. Maybe a
    Nothing Expr
    e
      () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    refineMeta [String]
    _ = IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    ": refine" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " metaid expr"

    retryConstraints :: TCM ()
    retryConstraints :: TCM ()
    retryConstraints = TCM ()
    wakeupConstraints_

    evalIn :: [String] -> TCM ()
    evalIn :: [String] -> TCM ()
    evalIn [String]
    s | [String] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [String]
    s Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Nat
    2 =
        do  Doc
    d <- [String] -> (InteractionId -> Expr -> TCMT IO Doc) -> TCMT IO Doc
    forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
    actOnMeta [String]
    s ((InteractionId -> Expr -> TCMT IO Doc) -> TCMT IO Doc)
    -> (InteractionId -> Expr -> TCMT IO Doc) -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ \InteractionId
    _ Expr
    e -> Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Expr -> TCMT IO Doc) -> TCM Expr -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ComputeMode -> Expr -> TCM Expr
    evalInCurrent ComputeMode
    DefaultCompute Expr
    e
            IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> IO ()
    forall a. Show a => a -> IO ()
    print Doc
    d
    evalIn [String]
    _ = IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn String
    ":eval metaid expr"

    parseExpr :: String -> TCM A.Expr
    parseExpr :: String -> TCM Expr
    parseExpr String
    s = do
        Expr
    e <- PM Expr -> TCM Expr
    forall a. PM a -> TCM a
    runPM (PM Expr -> TCM Expr) -> PM Expr -> TCM Expr
    forall a b. (a -> b) -> a -> b
    $ Parser Expr -> String -> PM Expr
    forall a. Parser a -> String -> PM a
    parse Parser Expr
    exprParser String
    s
        Expr -> (AbsOfCon Expr -> TCM Expr) -> TCM Expr
    forall c b.
    ToAbstract c =>
    c -> (AbsOfCon c -> ScopeM b) -> ScopeM b
    localToAbstract Expr
    e AbsOfCon Expr -> TCM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    evalTerm :: String -> TCM (ExitCode a)
    evalTerm :: forall a. String -> TCM (ExitCode a)
    evalTerm String
    s =
        do  Expr
    e <- String -> TCM Expr
    parseExpr String
    s
            Expr
    v <- ComputeMode -> Expr -> TCM Expr
    evalInCurrent ComputeMode
    DefaultCompute Expr
    e
            Doc
    e <- Expr -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Expr
    v
            IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> IO ()
    forall a. Show a => a -> IO ()
    print Doc
    e
            ExitCode a -> TCM (ExitCode a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ExitCode a
    forall a. ExitCode a
    Continue

    typeOf :: [String] -> TCM ()
    typeOf :: [String] -> TCM ()
    typeOf [String]
    s =
        do  Expr
    e  <- String -> TCM Expr
    parseExpr ([String] -> String
    unwords [String]
    s)
            Expr
    e0 <- Rewrite -> Expr -> TCM Expr
    typeInCurrent Rewrite
    Normalised Expr
    e
            Expr
    e1 <- Rewrite -> Expr -> TCM Expr
    typeInCurrent Rewrite
    AsIs Expr
    e
            IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> (String -> IO ()) -> String -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> IO ()
    putStrLn (String -> TCM ()) -> TCMT IO String -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Expr -> TCMT IO String
    forall a (m :: * -> *).
    (ToConcrete a, Show (ConOfAbs a), MonadAbsToCon m) =>
    a -> m String
    showA Expr
    e1

    typeIn :: [String] -> TCM ()
    typeIn :: [String] -> TCM ()
    typeIn s :: [String]
    s@(String
    _:String
    _:[String]
    _) =
        [String] -> (InteractionId -> Expr -> TCM ()) -> TCM ()
    forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
    actOnMeta [String]
    s ((InteractionId -> Expr -> TCM ()) -> TCM ())
    -> (InteractionId -> Expr -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \InteractionId
    i Expr
    e ->
        do  Expr
    e1 <- InteractionId -> Rewrite -> Expr -> TCM Expr
    typeInMeta InteractionId
    i Rewrite
    Normalised Expr
    e
            Expr
    e2 <- InteractionId -> Rewrite -> Expr -> TCM Expr
    typeInMeta InteractionId
    i Rewrite
    AsIs Expr
    e
            IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> (String -> IO ()) -> String -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> IO ()
    putStrLn (String -> TCM ()) -> TCMT IO String -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Expr -> TCMT IO String
    forall a (m :: * -> *).
    (ToConcrete a, Show (ConOfAbs a), MonadAbsToCon m) =>
    a -> m String
    showA Expr
    e1
    typeIn [String]
    _ = IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn String
    ":typeIn meta expr"

    showContext :: [String] -> TCM ()
    showContext :: [String] -> TCM ()
    showContext (String
    meta:[String]
    args) = do
        InteractionId
    i <- Nat -> InteractionId
    InteractionId (Nat -> InteractionId) -> TCMT IO Nat -> TCMT IO InteractionId
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> TCMT IO Nat
    forall a. Read a => String -> TCM a
    readM String
    meta
        MetaVariable
    mi <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta (MetaId -> TCMT IO MetaVariable)
    -> TCMT IO MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< InteractionId -> TCMT IO MetaId
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    i
        Closure Range -> TCM () -> TCM ()
    forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m, MonadTrace m) =>
    Closure Range -> m a -> m a
    withMetaInfo (MetaVariable -> Closure Range
    getMetaInfo MetaVariable
    mi) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          [(String, Type)]
    ctx <- (Dom' Term (String, Type) -> (String, Type))
    -> [Dom' Term (String, Type)] -> [(String, Type)]
    forall a b. (a -> b) -> [a] -> [b]
    List.map Dom' Term (String, Type) -> (String, Type)
    forall t e. Dom' t e -> e
    I.unDom ([Dom' Term (String, Type)] -> [(String, Type)])
    -> (Tele (Dom Type) -> [Dom' Term (String, Type)])
    -> Tele (Dom Type)
    -> [(String, Type)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Tele (Dom Type) -> [Dom' Term (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList (Tele (Dom Type) -> [(String, Type)])
    -> TCMT IO (Tele (Dom Type)) -> TCMT IO [(String, Type)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Tele (Dom Type))
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m) =>
    m (Tele (Dom Type))
    getContextTelescope
          ((String, Type) -> Nat -> TCM ())
    -> [(String, Type)] -> [Nat] -> TCM ()
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m ()
    zipWithM_ (String, Type) -> Nat -> TCM ()
    display [(String, Type)]
    ctx ([Nat] -> TCM ()) -> [Nat] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Nat] -> [Nat]
    forall a. [a] -> [a]
    reverse ([Nat] -> [Nat]) -> [Nat] -> [Nat]
    forall a b. (a -> b) -> a -> b
    $ (Nat -> (String, Type) -> Nat)
    -> [Nat] -> [(String, Type)] -> [Nat]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Nat -> (String, Type) -> Nat
    forall a b. a -> b -> a
    const [Nat
    1..] [(String, Type)]
    ctx
        where
            display :: (String, Type) -> Nat -> TCM ()
    display (String
    x, Type
    t) Nat
    n = do
                Type
    t <- case [String]
    args of
                        [String
    "normal"] -> Type -> TCMT IO Type
    forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
    normalise (Type -> TCMT IO Type) -> Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $ Nat -> Type -> Type
    forall a. Subst a => Nat -> a -> a
    raise Nat
    n Type
    t
                        [String]
    _          -> Type -> TCMT IO Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> TCMT IO Type) -> Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $ Nat -> Type -> Type
    forall a. Subst a => Nat -> a -> a
    raise Nat
    n Type
    t
                Doc
    d <- Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
                IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> IO ()
    forall a. Show a => a -> IO ()
    print (Doc -> IO ()) -> Doc -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    text (String -> String
    argNameToString String
    x) Doc -> Doc -> Doc
    <+> Doc
    ":" Doc -> Doc -> Doc
    <+> Doc
    d
    showContext [String]
    _ = IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn String
    ":Context meta"

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

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

    -- Read -------------------------------------------------------------------

    readM :: Read a => String -> TCM a
    readM :: forall a. Read a => String -> TCM a
    readM String
    s = TCMT IO a -> (a -> TCMT IO a) -> Maybe a -> TCMT IO a
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe TCMT IO a
    err a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe a -> TCMT IO a) -> Maybe a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe a
    forall a. Read a => String -> Maybe a
    readMaybe String
    s
      where
      err :: TCMT IO a
    err    = TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (TCErr -> TCMT IO a) -> TCErr -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ String -> TCErr
    strMsg (String -> TCErr) -> String -> TCErr
    forall a b. (a -> b) -> a -> b
    $ String
    "Cannot parse: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s
      strMsg :: String -> TCErr
    strMsg = Range -> Doc -> TCErr
    Exception Range
    forall a. Range' a
    noRange (Doc -> TCErr) -> (String -> Doc) -> String -> TCErr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Doc
    text