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.TypeChecking.Warnings (runPM)

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 -> 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' 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
withTCState :: forall a. (TCState -> TCState) -> ReplM a -> ReplM a
$cwithTCState :: forall a. (TCState -> TCState) -> ReplM a -> ReplM a
locallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> ReplM b -> ReplM b
$clocallyTCState :: forall a b. Lens' TCState a -> (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
renderError 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckResult -> Interface
crInterface) 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
renderError 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 Aspects
d <- forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
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
$ forall a. Doc a -> String
render Doc Aspects
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 Aspects
s <- forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
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
$ forall a. Doc a -> String
render Doc Aspects
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 Aspects)),
 Null (m (Doc Aspects)), Semigroup (m (Doc Aspects))) =>
OutputConstraint a InteractionId -> m (Doc Aspects)
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 Aspects)),
 Null (m (Doc Aspects)), Semigroup (m (Doc Aspects)), MonadIO m) =>
OutputConstraint a NamedMeta -> m ()
print' [OutputConstraint Expr NamedMeta]
hiddenMetas
    where
        showII :: OutputConstraint a InteractionId -> m (Doc Aspects)
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 Aspects)
prettyA OutputConstraint a InteractionId
o
        showM :: OutputConstraint a NamedMeta -> m (Doc Aspects)
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 Aspects)
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 Aspects
d <- forall {m :: * -> *} {a}.
(MonadTrace m, ToConcrete a, Pretty (ConOfAbs a),
 MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m (Doc Aspects)),
 Null (m (Doc Aspects)), Semigroup (m (Doc Aspects))) =>
OutputConstraint a NamedMeta -> m (Doc Aspects)
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
$ forall a. Doc a -> String
render Doc Aspects
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, Attributes
attrs) <- forall a. PM a -> TCM a
runPM forall a b. (a -> b) -> a -> b
$ forall a.
Parser a -> Position' SrcFile -> String -> PM (a, Attributes)
parsePosString Parser Expr
exprParser Position' SrcFile
pos String
s
        Attributes -> TCM ()
checkAttributes Attributes
attrs
        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 Aspects
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 Aspects)
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 Aspects
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, Attributes
attrs) <- forall a. PM a -> TCM a
runPM forall a b. (a -> b) -> a -> b
$ forall a. Parser a -> String -> PM (a, Attributes)
parse Parser Expr
exprParser String
s
    Attributes -> TCM ()
checkAttributes Attributes
attrs
    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 Aspects
e <- forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
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 Aspects
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 Aspects
d <- forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
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
$ forall a. String -> Doc a
text (String -> String
argNameToString String
x) forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
":" forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
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 Aspects -> TCErr
Exception forall a. Range' a
noRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. String -> Doc a
text