    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.Common.Pretty
    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.Utils.FileName (absolute, AbsolutePath)
    import Agda.Utils.Maybe (caseMaybeM)

    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
    $cfmap :: forall a b. (a -> b) -> ReplM a -> ReplM b
    fmap :: forall a b. (a -> b) -> ReplM a -> ReplM b
    $c<$ :: forall a b. a -> ReplM b -> ReplM a
    <$ :: forall a b. a -> ReplM b -> ReplM a
    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
    $cpure :: forall a. a -> ReplM a
    pure :: forall a. a -> ReplM a
    $c<*> :: forall a b. ReplM (a -> b) -> ReplM a -> ReplM b
    <*> :: forall a b. ReplM (a -> b) -> ReplM a -> ReplM b
    $cliftA2 :: forall a b c. (a -> b -> c) -> ReplM a -> ReplM b -> ReplM c
    liftA2 :: forall a b c. (a -> b -> c) -> ReplM a -> ReplM b -> ReplM c
    $c*> :: forall a b. ReplM a -> ReplM b -> ReplM b
    *> :: forall a b. ReplM a -> ReplM b -> ReplM b
    $c<* :: forall a b. ReplM a -> ReplM b -> ReplM a
    <* :: forall a b. ReplM a -> ReplM b -> 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
    $c>>= :: forall a b. ReplM a -> (a -> ReplM b) -> ReplM b
    >>= :: forall a b. ReplM a -> (a -> ReplM b) -> ReplM b
    $c>> :: forall a b. ReplM a -> ReplM b -> ReplM b
    >> :: forall a b. ReplM a -> ReplM b -> ReplM b
    $creturn :: forall a. a -> ReplM a
    return :: forall a. a -> ReplM a
    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
    $cliftIO :: forall a. IO a -> ReplM a
    liftIO :: 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
    $cpragmaOptions :: ReplM PragmaOptions
    pragmaOptions :: ReplM PragmaOptions
    $ccommandLineOptions :: ReplM CommandLineOptions
    commandLineOptions :: ReplM CommandLineOptions
    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
    $caskTC :: ReplM TCEnv
    askTC :: ReplM TCEnv
    $clocalTC :: forall a. (TCEnv -> TCEnv) -> ReplM a -> ReplM a
    localTC :: forall a. (TCEnv -> TCEnv) -> ReplM a -> ReplM a
    MonadTCEnv, Monad ReplM
    ReplM TCState
    Monad ReplM =>
    ReplM TCState
    -> (forall a b. Lens' TCState a -> (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' TCState a -> (a -> a) -> ReplM b -> ReplM b
    forall (m :: * -> *).
    Monad m =>
    m TCState
    -> (forall a b. Lens' TCState a -> (a -> a) -> m b -> m b)
    -> (forall a. (TCState -> TCState) -> m a -> m a)
    -> ReadTCState m
    $cgetTCState :: ReplM TCState
    getTCState :: ReplM TCState
    $clocallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> ReplM b -> ReplM b
    locallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> ReplM b -> ReplM b
    $cwithTCState :: forall a. (TCState -> TCState) -> ReplM a -> ReplM a
    withTCState :: forall a. (TCState -> TCState) -> ReplM a -> ReplM a
    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
    $cgetTC :: ReplM TCState
    getTC :: ReplM TCState
    $cputTC :: TCState -> ReplM ()
    putTC :: TCState -> ReplM ()
    $cmodifyTC :: (TCState -> TCState) -> ReplM ()
    modifyTC :: (TCState -> TCState) -> ReplM ()
    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
    $cliftTCM :: forall a. TCM a -> ReplM a
    liftTCM :: forall a. TCM a -> ReplM a
    MonadTCM
        , MonadError TCErr
        , MonadReader ReplEnv, MonadState ReplState
        , Monad ReplM
    Monad ReplM =>
    (FileId -> ReplM AbsolutePath)
    -> (AbsolutePath -> ReplM FileId) -> MonadFileId ReplM
    AbsolutePath -> ReplM FileId
    FileId -> ReplM AbsolutePath
    forall (m :: * -> *).
    Monad m =>
    (FileId -> m AbsolutePath)
    -> (AbsolutePath -> m FileId) -> MonadFileId m
    $cfileFromId :: FileId -> ReplM AbsolutePath
    fileFromId :: FileId -> ReplM AbsolutePath
    $cidFromFile :: AbsolutePath -> ReplM FileId
    idFromFile :: AbsolutePath -> ReplM FileId
    MonadFileId
        )

    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
        { 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 a. 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 a. (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  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 (m :: * -> *) a. Monad m => m a -> ReaderT ReplEnv m a
    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 (m :: * -> *) a. Monad m => m a -> StateT ReplState m a
    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 fmap words ms of
                        Maybe [String]
    Nothing               -> a -> ReplM a
    forall a. 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 a. IO a -> ReplM a
    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 a. IO a -> ReplM a
    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 a. TCM a -> ReplM 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 a. 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  s <- TCErr -> ReplM String
    forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
    renderError TCErr
    e
                        liftIO $ putStrLn s
                        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 a. TCM a -> ReplM a
    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 a. IO a -> ReplM a
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Maybe a -> f (Maybe 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 a. TCM a -> ReplM a
    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
                checked <- ReplM (Maybe CheckResult)
    checkCurrentFile
                liftTCM $ setScope $ maybe emptyScopeInfo (iInsideScope . crInterface) checked
                -- Andreas, 2021-01-27, issue #5132, make Set and Prop available from Agda.Primitive
                -- if no module is loaded.
                when (isNothing checked) $ do
                  -- @open import Agda.Primitive using (Set; Prop)@
                  void $ liftTCM importPrimitives
              ReplM () -> (TCErr -> ReplM ()) -> ReplM ()
    forall a. 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
                s <- TCErr -> ReplM String
    forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
    renderError TCErr
    e
                liftIO $ putStrLn s
                liftIO $ putStrLn "Failed."

            commands :: [Command ()]
    commands =
                [ String
    "quit"        String -> ([String] -> ReplM (ExitCode ())) -> Command ()
    forall {a} {b}. a -> b -> (a, b)
    |>  \[String]
    _ -> ExitCode () -> ReplM (ExitCode ())
    forall a. a -> ReplM a
    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 a. IO a -> ReplM a
    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 a. TCM a -> ReplM a
    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 a. TCM a -> ReplM a
    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 a. TCM a -> ReplM a
    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 a. TCM a -> ReplM a
    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 a. TCM a -> ReplM a
    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 a. TCM a -> ReplM a
    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 a. TCM a -> ReplM a
    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 a. TCM a -> ReplM a
    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 a. TCM a -> ReplM a
    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 a. TCM a -> ReplM a
    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 a b. ReplM a -> ReplM b -> ReplM b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> ExitCode b -> ReplM (ExitCode b)
    forall a. a -> ReplM a
    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
      mpath <- (ReplState -> Maybe AbsolutePath) -> ReplM (Maybe AbsolutePath)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ReplState -> Maybe AbsolutePath
    currentFile
      i <- traverse idFromFile mpath
      localTC (\ TCEnv
    e -> TCEnv
    e { envCurrentPath = i }) cont

    loadFile :: ReplM () -> [String] -> ReplM ()
    loadFile :: ReplM () -> [String] -> ReplM ()
    loadFile ReplM ()
    reload [String
    file] = do
      absPath <- IO AbsolutePath -> ReplM AbsolutePath
    forall a. IO a -> ReplM a
    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
      modify (\(ReplState Maybe AbsolutePath
    _prevFile) -> Maybe AbsolutePath -> ReplState
    ReplState (AbsolutePath -> Maybe AbsolutePath
    forall a. a -> Maybe a
    Just AbsolutePath
    absPath))
      withCurrentFile reload
    loadFile ReplM ()
    _ [String]
    _ = IO () -> ReplM ()
    forall a. IO a -> ReplM a
    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  cs <- TCM [OutputForm Expr Expr]
    BasicOps.getConstraints
            liftIO $ putStrLn $ unlines (List.map prettyShow cs)
    showConstraints [String]
    _ = IO () -> TCM ()
    forall a. IO a -> TCMT IO a
    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  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
            withInteractionId i $ do
              s <- typeOfMeta AsIs i
              r <- getInteractionRange i
              d <- prettyA s
              liftIO $ putStrLn $ render d ++ " " ++ prettyShow r
    showMetas [String
    m,String
    "normal"] =
        do  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
            withInteractionId i $ do
              s <- prettyA =<< typeOfMeta Normalised i
              r <- getInteractionRange i
              liftIO $ putStrLn $ render s ++ " " ++ prettyShow r
    showMetas [] =
        do  interactionMetas <- Rewrite -> TCM [OutputConstraint Expr InteractionId]
    typesOfVisibleMetas Rewrite
    AsIs
            hiddenMetas      <- typesOfHiddenMetas  AsIs
            mapM_ (liftIO . print) =<< mapM showII interactionMetas
            mapM_ print' hiddenMetas
        where
            showII :: OutputConstraint_boot TCErr a InteractionId -> m (Doc Aspects)
    showII OutputConstraint_boot TCErr a InteractionId
    o = InteractionId -> m (Doc Aspects) -> m (Doc Aspects)
    forall (m :: * -> *) a.
    (MonadDebug 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_boot TCErr a InteractionId
    -> OutputForm a InteractionId
    forall tcErr a b.
    Range
    -> [ProblemId]
    -> Blocker
    -> OutputConstraint_boot tcErr a b
    -> OutputForm_boot tcErr a b
    OutputForm Range
    forall a. Range' a
    noRange [] Blocker
    alwaysUnblock OutputConstraint_boot TCErr a InteractionId
    o) (m (Doc Aspects) -> m (Doc Aspects))
    -> m (Doc Aspects) -> m (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ OutputConstraint_boot TCErr a InteractionId -> m (Doc Aspects)
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m (Doc Aspects)
    prettyA OutputConstraint_boot TCErr a InteractionId
    o
            showM :: OutputConstraint_boot TCErr a NamedMeta -> m (Doc Aspects)
    showM  OutputConstraint_boot TCErr a NamedMeta
    o = MetaId -> m (Doc Aspects) -> m (Doc Aspects)
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
     ReadTCState 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_boot TCErr a NamedMeta
    -> OutputForm a NamedMeta
    forall tcErr a b.
    Range
    -> [ProblemId]
    -> Blocker
    -> OutputConstraint_boot tcErr a b
    -> OutputForm_boot tcErr a b
    OutputForm Range
    forall a. Range' a
    noRange [] Blocker
    alwaysUnblock OutputConstraint_boot TCErr a NamedMeta
    o) (m (Doc Aspects) -> m (Doc Aspects))
    -> m (Doc Aspects) -> m (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ OutputConstraint_boot TCErr a NamedMeta -> m (Doc Aspects)
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m (Doc Aspects)
    prettyA OutputConstraint_boot TCErr a NamedMeta
    o

            metaId :: OutputConstraint_boot tcErr 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_boot tcErr a b
    _ = b
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            print' :: OutputConstraint_boot TCErr a NamedMeta -> m ()
    print' OutputConstraint_boot TCErr a NamedMeta
    x = do
                r <- MetaId -> m Range
    forall (m :: * -> *).
    (HasCallStack, MonadDebug 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_boot TCErr a NamedMeta -> NamedMeta
    forall {tcErr} {a} {b}. OutputConstraint_boot tcErr a b -> b
    metaId OutputConstraint_boot TCErr a NamedMeta
    x
                d <- showM x
                liftIO $ putStrLn $ render d ++ "  [ at " ++ prettyShow r ++ " ]"
    showMetas [String]
    _ = IO () -> TCM ()
    forall a. IO a -> TCMT IO a
    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
      scope <- TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      liftIO $ putStrLn $ prettyShow scope

    metaParseExpr ::  InteractionId -> String -> TCM A.Expr
    metaParseExpr :: InteractionId -> String -> TCM Expr
    metaParseExpr InteractionId
    ii String
    s =
        do  m <- InteractionId -> TCMT IO MetaId
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    ii
            scope <- getMetaScope <$> lookupLocalMeta m
            r <- getRange <$> lookupLocalMeta m
            -- liftIO $ putStrLn $ prettyShow scope
            let 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)
            (e, attrs) <- runPM $ parsePosString exprParser pos s
            checkAttributes attrs
            concreteToAbstract scope 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  i <- String -> TCMT IO Nat
    forall a. Read a => String -> TCM a
    readM String
    is
             let ii = Nat -> InteractionId
    InteractionId Nat
    i
             e <- metaParseExpr ii (unwords es)
             withInteractionId ii $ f ii 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 a. [a] -> 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
      _ <- [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
      return ()
    giveMeta [String]
    _ = IO () -> TCM ()
    forall a. IO a -> TCMT IO a
    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 a. [a] -> 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
      _ <- [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
      return ()
    refineMeta [String]
    _ = IO () -> TCM ()
    forall a. IO a -> TCMT IO a
    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 a. [a] -> 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  d <- [String]
    -> (InteractionId -> Expr -> TCMT IO (Doc Aspects))
    -> TCMT IO (Doc Aspects)
    forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
    actOnMeta [String]
    s ((InteractionId -> Expr -> TCMT IO (Doc Aspects))
     -> TCMT IO (Doc Aspects))
    -> (InteractionId -> Expr -> TCMT IO (Doc Aspects))
    -> TCMT IO (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ \InteractionId
    _ Expr
    e -> Expr -> TCMT IO (Doc Aspects)
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m (Doc Aspects)
    prettyA (Expr -> TCMT IO (Doc Aspects))
    -> TCM Expr -> TCMT IO (Doc Aspects)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ComputeMode -> Expr -> TCM Expr
    evalInCurrent ComputeMode
    DefaultCompute Expr
    e
            liftIO $ print d
    evalIn [String]
    _ = IO () -> TCM ()
    forall a. IO a -> TCMT IO a
    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
        (e, attrs) <- 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
        checkAttributes attrs
        localToAbstract e return

    evalTerm :: String -> TCM (ExitCode a)
    evalTerm :: forall a. String -> TCM (ExitCode a)
    evalTerm String
    s =
        do  e <- String -> TCM Expr
    parseExpr String
    s
            v <- evalInCurrent DefaultCompute e
            e <- prettyTCM v
            liftIO $ print e
            return Continue

    typeOf :: [String] -> TCM ()
    typeOf :: [String] -> TCM ()
    typeOf [String]
    s =
        do  e  <- String -> TCM Expr
    parseExpr ([String] -> String
    unwords [String]
    s)
            e0 <- typeInCurrent Normalised e
            e1 <- typeInCurrent AsIs e
            liftIO . print =<< prettyA 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  e1 <- InteractionId -> Rewrite -> Expr -> TCM Expr
    typeInMeta InteractionId
    i Rewrite
    Normalised Expr
    e
            e2 <- typeInMeta i AsIs e
            liftIO . print =<< prettyA e1
    typeIn [String]
    _ = IO () -> TCM ()
    forall a. IO a -> TCMT IO a
    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
        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
        mi <- lookupLocalMeta =<< lookupInteractionId i
        withMetaInfo (getMetaInfo mi) $ do
          ctx <- List.map I.unDom . telToList <$> getContextTelescope
          zipWithM_ display ctx $ reverse $ zipWith const [1..] ctx
        where
            display :: (String, Type) -> Nat -> TCM ()
    display (String
    x, Type
    t) Nat
    n = do
                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 a. a -> TCMT IO a
    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
                d <- prettyTCM t
                liftIO $ print $ text (argNameToString x) <+> ":" <+> d
    showContext [String]
    _ = IO () -> TCM ()
    forall a. IO a -> TCMT IO a
    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 = TCM a -> (a -> TCM a) -> Maybe a -> TCM a
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe TCM a
    err a -> TCM a
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe a -> TCM a) -> Maybe a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe a
    forall a. Read a => String -> Maybe a
    readMaybe String
    s
      where
      err :: TCM a
    err = TCErr -> TCM a
    forall a. TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (TCErr -> TCM a) -> TCErr -> TCM a
    forall a b. (a -> b) -> a -> b
    $ String -> TCErr
    GenericException (String -> TCErr) -> String -> TCErr
    forall a b. (a -> b) -> a -> b
    $ String
    "Cannot parse: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s