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 -> 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
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
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
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
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
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
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
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
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
    = forall a. IM a -> TCM a
runIM
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Maybe AbsolutePath -> ReplState
ReplState Maybe AbsolutePath
initialFile)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReplEnv
replEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. (a -> Bool) -> [a] -> [a]
List.filter (forall a. Eq a => [a] -> [a] -> Bool
List.isPrefixOf String
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [Command a]
cmds of
        [(String
_,[String] -> ReplM (ExitCode a)
m)] -> forall a b. b -> Either a b
Right [String] -> ReplM (ExitCode a)
m
        [Command a]
xs      -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
List.map 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)       = forall (m :: * -> *) a. Monad m => a -> m a
return a
x
        go ExitCode a
Continue         = ReplM a
loop
        go (ContinueIn TCEnv
env) = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (forall a b. a -> b -> a
const TCEnv
env) ReplM a
loop

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

checkCurrentFile :: ReplM (Maybe CheckResult)
checkCurrentFile :: ReplM (Maybe CheckResult)
checkCurrentFile = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse AbsolutePath -> ReplM CheckResult
checkFile forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (a -> b) -> a -> b
$ AbsolutePath
file) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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
    forall a.
String -> [Command a] -> (String -> TCM (ExitCode a)) -> ReplM a
interaction String
"Main> " [(String, [String] -> ReplM (ExitCode ()))]
commands forall a. String -> TCM (ExitCode a)
evalTerm
    where
        ReplM ()
reload :: ReplM () = do
            Maybe CheckResult
checked <- ReplM (Maybe CheckResult)
checkCurrentFile
            forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ ScopeInfo -> TCM ()
setScope forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe ScopeInfo
emptyScopeInfo Interface -> ScopeInfo
iInsideScope (CheckResult -> Interface
crInterface 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.
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Maybe a -> Bool
isNothing Maybe CheckResult
checked) forall a b. (a -> b) -> a -> b
$ do
              -- @open import Agda.Primitive using (Set; Prop)@
              forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM ScopeM [Declaration]
importPrimitives
          forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
e -> do
            String
s <- forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
prettyError TCErr
e
            forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
s
            forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Failed."

        commands :: [(String, [String] -> ReplM (ExitCode ()))]
commands =
            [ String
"quit"        forall {a} {b}. a -> b -> (a, b)
|>  \[String]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> ExitCode a
Return ()
            , String
"?"           forall {a} {b}. a -> b -> (a, b)
|>  \[String]
_ -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. [Command a] -> IO ()
help [(String, [String] -> ReplM (ExitCode ()))]
commands
            , String
"reload"      forall {a} {b}. a -> b -> (a, b)
|>  \[String]
_ -> do ReplM ()
reload
                                         forall a. TCEnv -> ExitCode a
ContinueIn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
            , String
"constraints" forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
showConstraints [String]
args
            , String
"Context"     forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
showContext [String]
args
            , String
"give"        forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
giveMeta [String]
args
            , String
"Refine"      forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
refineMeta [String]
args
            , String
"metas"       forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
showMetas [String]
args
            , String
"load"        forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ ReplM () -> [String] -> ReplM ()
loadFile ReplM ()
reload [String]
args
            , String
"eval"        forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
evalIn [String]
args
            , String
"typeOf"      forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
typeOf [String]
args
            , String
"typeIn"      forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
typeIn [String]
args
            , String
"wakeup"      forall {a} {b}. a -> b -> (a, b)
|> \[String]
_ -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ TCM ()
retryConstraints
            , String
"scope"       forall {a} {b}. a -> b -> (a, b)
|> \[String]
_ -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM 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 = forall a. ReplM a -> ReplM a
withCurrentFile forall a b. (a -> b) -> a -> b
$ do
  ReplM a
m forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return 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 <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ReplState -> Maybe AbsolutePath
currentFile
  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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO AbsolutePath
absolute String
file
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\(ReplState Maybe AbsolutePath
_prevFile) -> Maybe AbsolutePath -> ReplState
ReplState (forall a. a -> Maybe a
Just AbsolutePath
absPath))
  forall a. ReplM a -> ReplM a
withCurrentFile ReplM ()
reload
loadFile ReplM ()
_ [String]
_ = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO 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
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines (forall a b. (a -> b) -> [a] -> [b]
List.map forall a. Pretty a => a -> String
prettyShow [OutputForm Expr Expr]
cs)
showConstraints [String]
_ = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Read a => String -> TCM a
readM String
m
        forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
i 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 <- forall (m :: * -> *).
(MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange InteractionId
i
          Doc
d <- forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA OutputConstraint Expr InteractionId
s
          forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ Doc -> String
render Doc
d forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow Range
r
showMetas [String
m,String
"normal"] =
    do  InteractionId
i <- Nat -> InteractionId
InteractionId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Read a => String -> TCM a
readM String
m
        forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
i forall a b. (a -> b) -> a -> b
$ do
          Doc
s <- forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA 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 <- forall (m :: * -> *).
(MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange InteractionId
i
          forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ Doc -> String
render Doc
s forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ 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
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> IO ()
print) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {m :: * -> *} {a}.
(MonadError TCErr m, MonadTrace m, ToConcrete a,
 Pretty (ConOfAbs a), MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc)) =>
OutputConstraint a InteractionId -> m Doc
showII [OutputConstraint Expr InteractionId]
interactionMetas
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {m :: * -> *} {a}.
(MonadTrace m, ToConcrete a, Pretty (ConOfAbs a),
 MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc), MonadIO m) =>
OutputConstraint a NamedMeta -> m ()
print' [OutputConstraint Expr NamedMeta]
hiddenMetas
    where
        showII :: OutputConstraint a InteractionId -> m Doc
showII OutputConstraint a InteractionId
o = forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId (forall a b. OutputForm a b -> b
outputFormId forall a b. (a -> b) -> a -> b
$ forall a b.
Range
-> [ProblemId] -> Blocker -> OutputConstraint a b -> OutputForm a b
OutputForm forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint a InteractionId
o) forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a.
(HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
 ReadTCState m) =>
MetaId -> m a -> m a
withMetaId (NamedMeta -> MetaId
nmid forall a b. (a -> b) -> a -> b
$ forall a b. OutputForm a b -> b
outputFormId forall a b. (a -> b) -> a -> b
$ forall a b.
Range
-> [ProblemId] -> Blocker -> OutputConstraint a b -> OutputForm a b
OutputForm forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint a NamedMeta
o) forall a b. (a -> b) -> a -> b
$ 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
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
        print' :: OutputConstraint a NamedMeta -> m ()
print' OutputConstraint a NamedMeta
x = do
            Range
r <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange forall a b. (a -> b) -> a -> b
$ NamedMeta -> MetaId
nmid forall a b. (a -> b) -> a -> b
$ forall {a} {b}. OutputConstraint a b -> b
metaId OutputConstraint a NamedMeta
x
            Doc
d <- forall {m :: * -> *} {a}.
(MonadTrace m, ToConcrete a, Pretty (ConOfAbs a),
 MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc)) =>
OutputConstraint a NamedMeta -> m Doc
showM OutputConstraint a NamedMeta
x
            forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ Doc -> String
render Doc
d forall a. [a] -> [a] -> [a]
++ String
"  [ at " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow Range
r forall a. [a] -> [a] -> [a]
++ String
" ]"
showMetas [String]
_ = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
":meta [metaid]"


showScope :: TCM ()
showScope :: TCM ()
showScope = do
  ScopeInfo
scope <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
        ScopeInfo
scope <- MetaVariable -> ScopeInfo
getMetaScope forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
        Range
r <- forall a. HasRange a => a -> Range
getRange forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
        -- liftIO $ putStrLn $ prettyShow scope
        let pos :: Position' SrcFile
pos = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. Range' a -> Maybe (Position' a)
rStart Range
r)
        (Expr
e, CohesionAttributes
coh) <- forall a. PM a -> TCM a
runPM forall a b. (a -> b) -> a -> b
$ forall a.
Parser a
-> Position' SrcFile -> String -> PM (a, CohesionAttributes)
parsePosString Parser Expr
exprParser Position' SrcFile
pos String
s
        CohesionAttributes -> TCM ()
checkCohesionAttributes CohesionAttributes
coh
        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 <- 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)
         forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$ InteractionId -> Expr -> TCM a
f InteractionId
ii Expr
e
actOnMeta [String]
_ InteractionId -> Expr -> TCM a
_ = forall a. HasCallStack => a
__IMPOSSIBLE__


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



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



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


evalIn :: [String] -> TCM ()
evalIn :: [String] -> TCM ()
evalIn [String]
s | forall (t :: * -> *) a. Foldable t => t a -> Nat
length [String]
s forall a. Ord a => a -> a -> Bool
>= Nat
2 =
    do  Doc
d <- forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta [String]
s forall a b. (a -> b) -> a -> b
$ \InteractionId
_ Expr
e -> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ComputeMode -> Expr -> TCM Expr
evalInCurrent ComputeMode
DefaultCompute Expr
e
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> IO ()
print Doc
d
evalIn [String]
_ = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO 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, CohesionAttributes
coh) <- forall a. PM a -> TCM a
runPM forall a b. (a -> b) -> a -> b
$ forall a. Parser a -> String -> PM (a, CohesionAttributes)
parse Parser Expr
exprParser String
s
    CohesionAttributes -> TCM ()
checkCohesionAttributes CohesionAttributes
coh
    forall c b.
ToAbstract c =>
c -> (AbsOfCon c -> ScopeM b) -> ScopeM b
localToAbstract Expr
e 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 <- forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
v
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> IO ()
print Doc
e
        forall (m :: * -> *) a. Monad m => a -> m a
return 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
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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]
_) =
    forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta [String]
s 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
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(ToConcrete a, Show (ConOfAbs a), MonadAbsToCon m) =>
a -> m String
showA Expr
e1
typeIn [String]
_ = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Read a => String -> TCM a
readM String
meta
    MetaVariable
mi <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
i
    forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mi) forall a b. (a -> b) -> a -> b
$ do
      [(String, Type)]
ctx <- forall a b. (a -> b) -> [a] -> [b]
List.map forall t e. Dom' t e -> e
I.unDom forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Tele (Dom t) -> [Dom (String, t)]
telToList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
      forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (String, Type) -> Nat -> TCM ()
display [(String, Type)]
ctx forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith 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"] -> forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise Nat
n Type
t
                    [String]
_          -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise Nat
n Type
t
            Doc
d <- forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
            forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> IO ()
print 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]
_ = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO 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 forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines forall a b. (a -> b) -> a -> b
$
    [ String
"Command overview" ] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
List.map forall {b}. (String, b) -> String
explain [Command a]
cs 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
":" 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 = forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCM a
err forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Read a => String -> Maybe a
readMaybe String
s
  where
  err :: TCM a
err    = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String -> TCErr
strMsg forall a b. (a -> b) -> a -> b
$ String
"Cannot parse: " forall a. [a] -> [a] -> [a]
++ String
s
  strMsg :: String -> TCErr
strMsg = Range -> Doc -> TCErr
Exception forall a. Range' a
noRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
text