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 -> 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
    )

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  Maybe String
ms <- ReaderT ReplEnv (StateT ReplState IM) (Maybe String)
-> ReplM (Maybe String)
forall a. ReaderT ReplEnv (StateT ReplState IM) a -> ReplM a
ReplM (ReaderT ReplEnv (StateT ReplState IM) (Maybe String)
 -> ReplM (Maybe String))
-> ReaderT ReplEnv (StateT ReplState IM) (Maybe String)
-> ReplM (Maybe String)
forall a b. (a -> b) -> a -> b
$ StateT ReplState IM (Maybe String)
-> ReaderT ReplEnv (StateT ReplState IM) (Maybe String)
forall (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 (String -> [String]) -> Maybe String -> Maybe [String]
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> [String]
words Maybe String
ms of
                    Maybe [String]
Nothing               -> a -> ReplM a
forall 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  String
s <- TCErr -> ReplM String
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
renderError TCErr
e
                    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
s
                    ReplM a
loop

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

replSetup :: ReplM ()
replSetup :: ReplM ()
replSetup = do
    TCM () -> ReplM ()
forall 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
            Maybe CheckResult
checked <- ReplM (Maybe CheckResult)
checkCurrentFile
            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
$ ScopeInfo -> TCM ()
setScope (ScopeInfo -> TCM ()) -> ScopeInfo -> TCM ()
forall a b. (a -> b) -> a -> b
$ ScopeInfo
-> (CheckResult -> ScopeInfo) -> Maybe CheckResult -> ScopeInfo
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ScopeInfo
emptyScopeInfo (Interface -> ScopeInfo
iInsideScope (Interface -> ScopeInfo)
-> (CheckResult -> Interface) -> CheckResult -> ScopeInfo
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.
            Bool -> ReplM () -> ReplM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe CheckResult -> Bool
forall a. Maybe a -> Bool
isNothing Maybe CheckResult
checked) (ReplM () -> ReplM ()) -> ReplM () -> ReplM ()
forall a b. (a -> b) -> a -> b
$ do
              -- @open import Agda.Primitive using (Set; Prop)@
              ReplM [Declaration] -> ReplM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ReplM [Declaration] -> ReplM ())
-> ReplM [Declaration] -> ReplM ()
forall a b. (a -> b) -> a -> b
$ TCM [Declaration] -> ReplM [Declaration]
forall a. TCM a -> ReplM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCM [Declaration]
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
            String
s <- TCErr -> ReplM String
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
renderError TCErr
e
            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
s
            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
"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
  Maybe AbsolutePath
mpath <- (ReplState -> Maybe AbsolutePath) -> ReplM (Maybe AbsolutePath)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ReplState -> Maybe AbsolutePath
currentFile
  (TCEnv -> TCEnv) -> ReplM a -> ReplM a
forall a. (TCEnv -> TCEnv) -> ReplM a -> ReplM a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envCurrentPath = mpath }) ReplM a
cont

loadFile :: ReplM () -> [String] -> ReplM ()
loadFile :: ReplM () -> [String] -> ReplM ()
loadFile ReplM ()
reload [String
file] = do
  AbsolutePath
absPath <- IO AbsolutePath -> ReplM AbsolutePath
forall 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
  (ReplState -> ReplState) -> ReplM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\(ReplState Maybe AbsolutePath
_prevFile) -> Maybe AbsolutePath -> ReplState
ReplState (AbsolutePath -> Maybe AbsolutePath
forall a. a -> Maybe a
Just AbsolutePath
absPath))
  ReplM () -> ReplM ()
forall a. ReplM a -> ReplM a
withCurrentFile ReplM ()
reload
loadFile ReplM ()
_ [String]
_ = IO () -> ReplM ()
forall 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  [OutputForm Expr Expr]
cs <- TCM [OutputForm Expr Expr]
BasicOps.getConstraints
        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] -> String
unlines ((OutputForm Expr Expr -> String)
-> [OutputForm Expr Expr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
List.map OutputForm Expr Expr -> String
forall a. Pretty a => a -> String
prettyShow [OutputForm Expr Expr]
cs)
showConstraints [String]
_ = IO () -> TCM ()
forall 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  InteractionId
i <- Nat -> InteractionId
InteractionId (Nat -> InteractionId) -> TCMT IO Nat -> TCMT IO InteractionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> TCMT IO Nat
forall a. Read a => String -> TCM a
readM String
m
        InteractionId -> TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
i (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          OutputConstraint Expr InteractionId
s <- Rewrite
-> InteractionId -> TCM (OutputConstraint Expr InteractionId)
typeOfMeta Rewrite
AsIs InteractionId
i
          Range
r <- InteractionId -> TCMT IO Range
forall (m :: * -> *).
(MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange InteractionId
i
          Doc Aspects
d <- OutputConstraint Expr InteractionId -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyA OutputConstraint Expr InteractionId
s
          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
$ Doc Aspects -> String
forall a. Doc a -> String
render Doc Aspects
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Range -> String
forall a. Pretty a => a -> String
prettyShow Range
r
showMetas [String
m,String
"normal"] =
    do  InteractionId
i <- Nat -> InteractionId
InteractionId (Nat -> InteractionId) -> TCMT IO Nat -> TCMT IO InteractionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> TCMT IO Nat
forall a. Read a => String -> TCM a
readM String
m
        InteractionId -> TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
i (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          Doc Aspects
s <- OutputConstraint Expr InteractionId -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyA (OutputConstraint Expr InteractionId -> TCMT IO (Doc Aspects))
-> TCM (OutputConstraint Expr InteractionId)
-> TCMT IO (Doc Aspects)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Rewrite
-> InteractionId -> TCM (OutputConstraint Expr InteractionId)
typeOfMeta Rewrite
Normalised InteractionId
i
          Range
r <- InteractionId -> TCMT IO Range
forall (m :: * -> *).
(MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange InteractionId
i
          IO () -> TCM ()
forall 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
$ Doc Aspects -> String
forall a. Doc a -> String
render Doc Aspects
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Range -> String
forall a. Pretty a => a -> String
prettyShow Range
r
showMetas [] =
    do  [OutputConstraint Expr InteractionId]
interactionMetas <- Rewrite -> TCM [OutputConstraint Expr InteractionId]
typesOfVisibleMetas Rewrite
AsIs
        [OutputConstraint Expr NamedMeta]
hiddenMetas      <- Rewrite -> TCM [OutputConstraint Expr NamedMeta]
typesOfHiddenMetas  Rewrite
AsIs
        (Doc Aspects -> TCM ()) -> [Doc Aspects] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IO () -> TCM ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ())
-> (Doc Aspects -> IO ()) -> Doc Aspects -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Aspects -> IO ()
forall a. Show a => a -> IO ()
print) ([Doc Aspects] -> TCM ()) -> TCMT IO [Doc Aspects] -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (OutputConstraint Expr InteractionId -> TCMT IO (Doc Aspects))
-> [OutputConstraint Expr InteractionId] -> TCMT IO [Doc Aspects]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM OutputConstraint Expr InteractionId -> TCMT IO (Doc Aspects)
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
        (OutputConstraint Expr NamedMeta -> TCM ())
-> [OutputConstraint Expr NamedMeta] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ OutputConstraint Expr NamedMeta -> TCM ()
forall {m :: * -> *} {a}.
(MonadTrace m, ToConcrete a, Pretty (ConOfAbs a),
 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 = InteractionId -> m (Doc Aspects) -> m (Doc Aspects)
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId (OutputForm a InteractionId -> InteractionId
forall a b. OutputForm a b -> b
outputFormId (OutputForm a InteractionId -> InteractionId)
-> OutputForm a InteractionId -> InteractionId
forall a b. (a -> b) -> a -> b
$ Range
-> [ProblemId]
-> Blocker
-> OutputConstraint a InteractionId
-> OutputForm a InteractionId
forall a b.
Range
-> [ProblemId] -> Blocker -> OutputConstraint a b -> OutputForm a b
OutputForm Range
forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint a InteractionId
o) (m (Doc Aspects) -> m (Doc Aspects))
-> m (Doc Aspects) -> m (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ OutputConstraint a InteractionId -> m (Doc Aspects)
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 = 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 a NamedMeta
-> OutputForm a NamedMeta
forall a b.
Range
-> [ProblemId] -> Blocker -> OutputConstraint a b -> OutputForm a b
OutputForm Range
forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint a NamedMeta
o) (m (Doc Aspects) -> m (Doc Aspects))
-> m (Doc Aspects) -> m (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ OutputConstraint a NamedMeta -> m (Doc Aspects)
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
_ = b
forall a. HasCallStack => a
__IMPOSSIBLE__
        print' :: OutputConstraint a NamedMeta -> m ()
print' OutputConstraint a NamedMeta
x = do
            Range
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 a NamedMeta -> NamedMeta
forall {a} {b}. OutputConstraint a b -> b
metaId OutputConstraint a NamedMeta
x
            Doc Aspects
d <- OutputConstraint a NamedMeta -> m (Doc Aspects)
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
            IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc Aspects -> String
forall a. Doc a -> String
render Doc Aspects
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  [ at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Range -> String
forall a. Pretty a => a -> String
prettyShow Range
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ]"
showMetas [String]
_ = IO () -> TCM ()
forall 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
  ScopeInfo
scope <- TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  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
$ ScopeInfo -> String
forall a. Pretty a => a -> String
prettyShow ScopeInfo
scope

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

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


giveMeta :: [String] -> TCM ()
giveMeta :: [String] -> TCM ()
giveMeta [String]
s | [String] -> Nat
forall 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
  Expr
_ <- [String] -> (InteractionId -> Expr -> TCM Expr) -> TCM Expr
forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta [String]
s ((InteractionId -> Expr -> TCM Expr) -> TCM Expr)
-> (InteractionId -> Expr -> TCM Expr) -> TCM Expr
forall a b. (a -> b) -> a -> b
$ \ InteractionId
ii Expr
e -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
give UseForce
WithoutForce InteractionId
ii Maybe Range
forall a. Maybe a
Nothing Expr
e
  () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
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
  Expr
_ <- [String] -> (InteractionId -> Expr -> TCM Expr) -> TCM Expr
forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta [String]
s ((InteractionId -> Expr -> TCM Expr) -> TCM Expr)
-> (InteractionId -> Expr -> TCM Expr) -> TCM Expr
forall a b. (a -> b) -> a -> b
$ \ InteractionId
ii Expr
e -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
refine UseForce
WithoutForce InteractionId
ii Maybe Range
forall a. Maybe a
Nothing Expr
e
  () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
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  Doc Aspects
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
        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
$ Doc Aspects -> IO ()
forall a. Show a => a -> IO ()
print Doc Aspects
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
    (Expr
e, Attributes
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
    Attributes -> TCM ()
checkAttributes Attributes
attrs
    Expr -> (AbsOfCon Expr -> TCM Expr) -> TCM Expr
forall c b.
ToAbstract c =>
c -> (AbsOfCon c -> ScopeM b) -> ScopeM b
localToAbstract Expr
e Expr -> TCM Expr
AbsOfCon Expr -> TCM Expr
forall a. a -> TCMT IO a
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 <- Expr -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *). MonadPretty m => Expr -> m (Doc Aspects)
prettyTCM Expr
v
        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
$ Doc Aspects -> IO ()
forall a. Show a => a -> IO ()
print Doc Aspects
e
        ExitCode a -> TCM (ExitCode a)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ExitCode a
forall a. ExitCode a
Continue

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

typeIn :: [String] -> TCM ()
typeIn :: [String] -> TCM ()
typeIn s :: [String]
s@(String
_:String
_:[String]
_) =
    [String] -> (InteractionId -> Expr -> TCM ()) -> TCM ()
forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta [String]
s ((InteractionId -> Expr -> TCM ()) -> TCM ())
-> (InteractionId -> Expr -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \InteractionId
i Expr
e ->
    do  Expr
e1 <- InteractionId -> Rewrite -> Expr -> TCM Expr
typeInMeta InteractionId
i Rewrite
Normalised Expr
e
        Expr
e2 <- InteractionId -> Rewrite -> Expr -> TCM Expr
typeInMeta InteractionId
i Rewrite
AsIs Expr
e
        IO () -> TCM ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> (String -> IO ()) -> String -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> TCM ()) -> TCMT IO String -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCMT IO String
forall a (m :: * -> *).
(ToConcrete a, Show (ConOfAbs a), MonadAbsToCon m) =>
a -> m String
showA Expr
e1
typeIn [String]
_ = IO () -> TCM ()
forall 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
    InteractionId
i <- Nat -> InteractionId
InteractionId (Nat -> InteractionId) -> TCMT IO Nat -> TCMT IO InteractionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> TCMT IO Nat
forall a. Read a => String -> TCM a
readM String
meta
    MetaVariable
mi <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta (MetaId -> TCMT IO MetaVariable)
-> TCMT IO MetaId -> TCMT IO MetaVariable
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
i
    Closure Range -> TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mi) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      [(String, Type)]
ctx <- (Dom' Term (String, Type) -> (String, Type))
-> [Dom' Term (String, Type)] -> [(String, Type)]
forall a b. (a -> b) -> [a] -> [b]
List.map Dom' Term (String, Type) -> (String, Type)
forall t e. Dom' t e -> e
I.unDom ([Dom' Term (String, Type)] -> [(String, Type)])
-> (Tele (Dom Type) -> [Dom' Term (String, Type)])
-> Tele (Dom Type)
-> [(String, Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom Type) -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList (Tele (Dom Type) -> [(String, Type)])
-> TCMT IO (Tele (Dom Type)) -> TCMT IO [(String, Type)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
      ((String, Type) -> Nat -> TCM ())
-> [(String, Type)] -> [Nat] -> TCM ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (String, Type) -> Nat -> TCM ()
display [(String, Type)]
ctx ([Nat] -> TCM ()) -> [Nat] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Nat] -> [Nat]
forall a. [a] -> [a]
reverse ([Nat] -> [Nat]) -> [Nat] -> [Nat]
forall a b. (a -> b) -> a -> b
$ (Nat -> (String, Type) -> Nat)
-> [Nat] -> [(String, Type)] -> [Nat]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Nat -> (String, Type) -> Nat
forall a b. a -> b -> a
const [Nat
1..] [(String, Type)]
ctx
    where
        display :: (String, Type) -> Nat -> TCM ()
display (String
x, Type
t) Nat
n = do
            Type
t <- case [String]
args of
                    [String
"normal"] -> Type -> TCMT IO Type
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Nat -> Type -> Type
forall a. Subst a => Nat -> a -> a
raise Nat
n Type
t
                    [String]
_          -> Type -> TCMT IO Type
forall 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
            Doc Aspects
d <- Type -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *). MonadPretty m => Type -> m (Doc Aspects)
prettyTCM Type
t
            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
$ Doc Aspects -> IO ()
forall a. Show a => a -> IO ()
print (Doc Aspects -> IO ()) -> Doc Aspects -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Doc Aspects
forall a. String -> Doc a
text (String -> String
argNameToString String
x) Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
":" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
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
strMsg (String -> TCErr) -> String -> TCErr
forall a b. (a -> b) -> a -> b
$ String
"Cannot parse: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
  strMsg :: String -> TCErr
strMsg = Range -> Doc Aspects -> TCErr
Exception Range
forall a. Range' a
noRange (Doc Aspects -> TCErr)
-> (String -> Doc Aspects) -> String -> TCErr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc Aspects
forall a. String -> Doc a
text