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.Common.Pretty.ANSI (putDocLn)
import Agda.Syntax.Internal (telToList, alwaysUnblock)
import qualified Agda.Syntax.Internal as I
import Agda.Syntax.Parser
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.Syntax.Abstract.Pretty

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

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

import Agda.Utils.Impossible

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

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

newtype ReplM a = ReplM { forall a. ReplM a -> ReaderT ReplEnv (StateT ReplState IM) a
unReplM :: ReaderT ReplEnv (StateT ReplState IM) a }
    deriving
    ( (forall a b. (a -> b) -> ReplM a -> ReplM b)
-> (forall a b. a -> ReplM b -> ReplM a) -> Functor ReplM
forall a b. a -> ReplM b -> ReplM a
forall a b. (a -> b) -> ReplM a -> ReplM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> ReplM a -> ReplM b
fmap :: forall a b. (a -> b) -> ReplM a -> ReplM b
$c<$ :: forall a b. a -> ReplM b -> ReplM a
<$ :: forall a b. a -> ReplM b -> ReplM a
Functor, Functor ReplM
Functor ReplM =>
(forall a. a -> ReplM a)
-> (forall a b. ReplM (a -> b) -> ReplM a -> ReplM b)
-> (forall a b c. (a -> b -> c) -> ReplM a -> ReplM b -> ReplM c)
-> (forall a b. ReplM a -> ReplM b -> ReplM b)
-> (forall a b. ReplM a -> ReplM b -> ReplM a)
-> Applicative ReplM
forall a. a -> ReplM a
forall a b. ReplM a -> ReplM b -> ReplM a
forall a b. ReplM a -> ReplM b -> ReplM b
forall a b. ReplM (a -> b) -> ReplM a -> ReplM b
forall a b c. (a -> b -> c) -> ReplM a -> ReplM b -> ReplM c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> ReplM a
pure :: forall a. a -> ReplM a
$c<*> :: forall a b. ReplM (a -> b) -> ReplM a -> ReplM b
<*> :: forall a b. ReplM (a -> b) -> ReplM a -> ReplM b
$cliftA2 :: forall a b c. (a -> b -> c) -> ReplM a -> ReplM b -> ReplM c
liftA2 :: forall a b c. (a -> b -> c) -> ReplM a -> ReplM b -> ReplM c
$c*> :: forall a b. ReplM a -> ReplM b -> ReplM b
*> :: forall a b. ReplM a -> ReplM b -> ReplM b
$c<* :: forall a b. ReplM a -> ReplM b -> ReplM a
<* :: forall a b. ReplM a -> ReplM b -> ReplM a
Applicative, Applicative ReplM
Applicative ReplM =>
(forall a b. ReplM a -> (a -> ReplM b) -> ReplM b)
-> (forall a b. ReplM a -> ReplM b -> ReplM b)
-> (forall a. a -> ReplM a)
-> Monad ReplM
forall a. a -> ReplM a
forall a b. ReplM a -> ReplM b -> ReplM b
forall a b. ReplM a -> (a -> ReplM b) -> ReplM b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. ReplM a -> (a -> ReplM b) -> ReplM b
>>= :: forall a b. ReplM a -> (a -> ReplM b) -> ReplM b
$c>> :: forall a b. ReplM a -> ReplM b -> ReplM b
>> :: forall a b. ReplM a -> ReplM b -> ReplM b
$creturn :: forall a. a -> ReplM a
return :: forall a. a -> ReplM a
Monad, Monad ReplM
Monad ReplM => (forall a. IO a -> ReplM a) -> MonadIO ReplM
forall a. IO a -> ReplM a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall a. IO a -> ReplM a
liftIO :: forall a. IO a -> ReplM a
MonadIO
    , Monad ReplM
Functor ReplM
Applicative ReplM
ReplM PragmaOptions
ReplM CommandLineOptions
(Functor ReplM, Applicative ReplM, Monad ReplM) =>
ReplM PragmaOptions -> ReplM CommandLineOptions -> HasOptions ReplM
forall (m :: * -> *).
(Functor m, Applicative m, Monad m) =>
m PragmaOptions -> m CommandLineOptions -> HasOptions m
$cpragmaOptions :: ReplM PragmaOptions
pragmaOptions :: ReplM PragmaOptions
$ccommandLineOptions :: ReplM CommandLineOptions
commandLineOptions :: ReplM CommandLineOptions
HasOptions, Monad ReplM
ReplM TCEnv
Monad ReplM =>
ReplM TCEnv
-> (forall a. (TCEnv -> TCEnv) -> ReplM a -> ReplM a)
-> MonadTCEnv ReplM
forall a. (TCEnv -> TCEnv) -> ReplM a -> ReplM a
forall (m :: * -> *).
Monad m =>
m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> m a -> m a) -> MonadTCEnv m
$caskTC :: ReplM TCEnv
askTC :: ReplM TCEnv
$clocalTC :: forall a. (TCEnv -> TCEnv) -> ReplM a -> ReplM a
localTC :: forall a. (TCEnv -> TCEnv) -> ReplM a -> ReplM a
MonadTCEnv, Monad ReplM
ReplM SessionState
ReplM TCState
Monad ReplM =>
ReplM TCState
-> (forall a b. Lens' TCState a -> (a -> a) -> ReplM b -> ReplM b)
-> ReplM SessionState
-> (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)
-> m SessionState
-> (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
$cgetSessionState :: ReplM SessionState
getSessionState :: ReplM SessionState
$cwithTCState :: forall a. (TCState -> TCState) -> ReplM a -> ReplM a
withTCState :: forall a. (TCState -> TCState) -> ReplM a -> ReplM a
ReadTCState, Monad ReplM
ReplM TCState
Monad ReplM =>
ReplM TCState
-> (TCState -> ReplM ())
-> ((TCState -> TCState) -> ReplM ())
-> MonadTCState ReplM
TCState -> ReplM ()
(TCState -> TCState) -> ReplM ()
forall (m :: * -> *).
Monad m =>
m TCState
-> (TCState -> m ())
-> ((TCState -> TCState) -> m ())
-> MonadTCState m
$cgetTC :: ReplM TCState
getTC :: ReplM TCState
$cputTC :: TCState -> ReplM ()
putTC :: TCState -> ReplM ()
$cmodifyTC :: (TCState -> TCState) -> ReplM ()
modifyTC :: (TCState -> TCState) -> ReplM ()
MonadTCState, Applicative ReplM
MonadIO ReplM
HasOptions ReplM
MonadTCState ReplM
MonadTCEnv ReplM
(Applicative ReplM, MonadIO ReplM, MonadTCEnv ReplM,
 MonadTCState ReplM, HasOptions ReplM) =>
(forall a. TCM a -> ReplM a) -> MonadTCM ReplM
forall a. TCM a -> ReplM a
forall (tcm :: * -> *).
(Applicative tcm, MonadIO tcm, MonadTCEnv tcm, MonadTCState tcm,
 HasOptions tcm) =>
(forall a. TCM a -> tcm a) -> MonadTCM tcm
$cliftTCM :: forall a. TCM a -> ReplM a
liftTCM :: forall a. TCM a -> ReplM a
MonadTCM
    , MonadError TCErr
    , MonadReader ReplEnv, MonadState ReplState
    , Monad ReplM
Monad ReplM =>
(HasCallStack => FileId -> ReplM AbsolutePath)
-> (AbsolutePath -> ReplM FileId) -> MonadFileId ReplM
HasCallStack => FileId -> ReplM AbsolutePath
AbsolutePath -> ReplM FileId
forall (m :: * -> *).
Monad m =>
(HasCallStack => FileId -> m AbsolutePath)
-> (AbsolutePath -> m FileId) -> MonadFileId m
$cfileFromId :: HasCallStack => FileId -> ReplM AbsolutePath
fileFromId :: HasCallStack => FileId -> ReplM AbsolutePath
$cidFromFile :: AbsolutePath -> ReplM FileId
idFromFile :: AbsolutePath -> ReplM FileId
MonadFileId
    )

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

data ExitCode a = Continue | ContinueIn TCEnv | Return a

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

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

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

        loop :: ReplM a
loop =
            do  ms <- ReaderT ReplEnv (StateT ReplState IM) (Maybe [Char])
-> ReplM (Maybe [Char])
forall a. ReaderT ReplEnv (StateT ReplState IM) a -> ReplM a
ReplM (ReaderT ReplEnv (StateT ReplState IM) (Maybe [Char])
 -> ReplM (Maybe [Char]))
-> ReaderT ReplEnv (StateT ReplState IM) (Maybe [Char])
-> ReplM (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ StateT ReplState IM (Maybe [Char])
-> ReaderT ReplEnv (StateT ReplState IM) (Maybe [Char])
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 [Char])
 -> ReaderT ReplEnv (StateT ReplState IM) (Maybe [Char]))
-> StateT ReplState IM (Maybe [Char])
-> ReaderT ReplEnv (StateT ReplState IM) (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ IM (Maybe [Char]) -> StateT ReplState IM (Maybe [Char])
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 [Char]) -> StateT ReplState IM (Maybe [Char]))
-> IM (Maybe [Char]) -> StateT ReplState IM (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ [Char] -> IM (Maybe [Char])
readline [Char]
prompt
                case fmap words ms of
                    Maybe [[Char]]
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
$ [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"** EOF **"
                    Just []               -> ReplM a
loop
                    Just ((Char
':':[Char]
cmd):[[Char]]
args) ->
                        do  case [Char]
-> [Command a] -> Either [[Char]] ([[Char]] -> ReplM (ExitCode a))
forall a.
[Char]
-> [Command a] -> Either [[Char]] ([[Char]] -> ReplM (ExitCode a))
matchCommand [Char]
cmd [Command a]
cmds of
                                Right [[Char]] -> 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
=<< ([[Char]] -> ReplM (ExitCode a)
c [[Char]]
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
$ [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Unknown command '" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
cmd [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"'"
                                        ReplM a
loop
                                Left [[Char]]
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
$ [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"More than one command match: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                                                            [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
", " [[Char]]
xs
                                        ReplM a
loop
                    Just [[Char]]
_ ->
                        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 ([Char] -> TCM (ExitCode a)
eval ([Char] -> TCM (ExitCode a)) -> [Char] -> TCM (ExitCode a)
forall a b. (a -> b) -> a -> b
$ Maybe [Char] -> [Char]
forall a. HasCallStack => Maybe a -> a
fromJust Maybe [Char]
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  Doc Aspects -> ReplM ()
forall (m :: * -> *).
(MonadIO m, HasOptions m) =>
Doc Aspects -> m ()
putDocLn (Doc Aspects -> ReplM ()) -> ReplM (Doc Aspects) -> ReplM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCErr -> ReplM (Doc Aspects)
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm (Doc Aspects)
prettyError TCErr
e
                    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
$ [Char] -> IO ()
putStr [Char]
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
    [Char] -> [Command ()] -> ([Char] -> TCM (ExitCode ())) -> ReplM ()
forall a.
[Char] -> [Command a] -> ([Char] -> TCM (ExitCode a)) -> ReplM a
interaction [Char]
"Main> " [Command ()]
commands [Char] -> TCM (ExitCode ())
forall a. [Char] -> TCM (ExitCode a)
evalTerm
    where
        ReplM ()
reload :: ReplM () = do
            checked <- ReplM (Maybe CheckResult)
checkCurrentFile
            liftTCM $ do
              case checked of
                Maybe CheckResult
Nothing    -> ScopeInfo -> TCM ()
setScope ScopeInfo
emptyScopeInfo
                Just CheckResult
scope -> do ScopeInfo -> TCM ()
setScope (Interface -> ScopeInfo
iInsideScope (Interface -> ScopeInfo) -> Interface -> ScopeInfo
forall a b. (a -> b) -> a -> b
$ CheckResult -> Interface
crInterface CheckResult
scope)
                                 TCM ()
forall (m :: * -> *). MonadTCState m => m ()
recomputeInverseScope
            -- Andreas, 2021-01-27, issue #5132, make Set and Prop available from Agda.Primitive
            -- if no module is loaded.
            when (isNothing checked) $ do
              -- @open import Agda.Primitive using (Set; Prop)@
              void $ liftTCM importPrimitives
          ReplM () -> (TCErr -> ReplM ()) -> ReplM ()
forall a. ReplM a -> (TCErr -> ReplM a) -> ReplM a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
e -> do
            Doc Aspects -> ReplM ()
forall (m :: * -> *).
(MonadIO m, HasOptions m) =>
Doc Aspects -> m ()
putDocLn (Doc Aspects -> ReplM ()) -> ReplM (Doc Aspects) -> ReplM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCErr -> ReplM (Doc Aspects)
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm (Doc Aspects)
prettyError 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
$ [Char] -> IO ()
putStrLn [Char]
"Failed."

        commands :: [Command ()]
commands =
            [ [Char]
"quit"        [Char] -> ([[Char]] -> ReplM (ExitCode ())) -> Command ()
forall {a} {b}. a -> b -> (a, b)
|>  \[[Char]]
_ -> 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 ()
            , [Char]
"?"           [Char] -> ([[Char]] -> ReplM (ExitCode ())) -> Command ()
forall {a} {b}. a -> b -> (a, b)
|>  \[[Char]]
_ -> 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
            , [Char]
"reload"      [Char] -> ([[Char]] -> ReplM (ExitCode ())) -> Command ()
forall {a} {b}. a -> b -> (a, b)
|>  \[[Char]]
_ -> 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
            , [Char]
"constraints" [Char] -> ([[Char]] -> ReplM (ExitCode ())) -> Command ()
forall {a} {b}. a -> b -> (a, b)
|> \[[Char]]
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
$ [[Char]] -> TCM ()
showConstraints [[Char]]
args
            , [Char]
"Context"     [Char] -> ([[Char]] -> ReplM (ExitCode ())) -> Command ()
forall {a} {b}. a -> b -> (a, b)
|> \[[Char]]
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
$ [[Char]] -> TCM ()
showContext [[Char]]
args
            , [Char]
"give"        [Char] -> ([[Char]] -> ReplM (ExitCode ())) -> Command ()
forall {a} {b}. a -> b -> (a, b)
|> \[[Char]]
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
$ [[Char]] -> TCM ()
giveMeta [[Char]]
args
            , [Char]
"Refine"      [Char] -> ([[Char]] -> ReplM (ExitCode ())) -> Command ()
forall {a} {b}. a -> b -> (a, b)
|> \[[Char]]
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
$ [[Char]] -> TCM ()
refineMeta [[Char]]
args
            , [Char]
"metas"       [Char] -> ([[Char]] -> ReplM (ExitCode ())) -> Command ()
forall {a} {b}. a -> b -> (a, b)
|> \[[Char]]
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
$ [[Char]] -> TCM ()
showMetas [[Char]]
args
            , [Char]
"load"        [Char] -> ([[Char]] -> ReplM (ExitCode ())) -> Command ()
forall {a} {b}. a -> b -> (a, b)
|> \[[Char]]
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 () -> [[Char]] -> ReplM ()
loadFile ReplM ()
reload [[Char]]
args
            , [Char]
"eval"        [Char] -> ([[Char]] -> ReplM (ExitCode ())) -> Command ()
forall {a} {b}. a -> b -> (a, b)
|> \[[Char]]
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
$ [[Char]] -> TCM ()
evalIn [[Char]]
args
            , [Char]
"typeOf"      [Char] -> ([[Char]] -> ReplM (ExitCode ())) -> Command ()
forall {a} {b}. a -> b -> (a, b)
|> \[[Char]]
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
$ [[Char]] -> TCM ()
typeOf [[Char]]
args
            , [Char]
"typeIn"      [Char] -> ([[Char]] -> ReplM (ExitCode ())) -> Command ()
forall {a} {b}. a -> b -> (a, b)
|> \[[Char]]
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
$ [[Char]] -> TCM ()
typeIn [[Char]]
args
            , [Char]
"wakeup"      [Char] -> ([[Char]] -> ReplM (ExitCode ())) -> Command ()
forall {a} {b}. a -> b -> (a, b)
|> \[[Char]]
_ -> 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
            , [Char]
"scope"       [Char] -> ([[Char]] -> ReplM (ExitCode ())) -> Command ()
forall {a} {b}. a -> b -> (a, b)
|> \[[Char]]
_ -> ReplM () -> ReplM (ExitCode ())
forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter (ReplM () -> ReplM (ExitCode ()))
-> ReplM () -> ReplM (ExitCode ())
forall a b. (a -> b) -> a -> b
$ TCM () -> ReplM ()
forall a. TCM a -> ReplM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM () -> ReplM ()) -> TCM () -> ReplM ()
forall a b. (a -> b) -> a -> b
$ TCM ()
showScope
            ]
            where
                |> :: a -> b -> (a, b)
(|>) = (,)

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

-- | Set 'envCurrentPath' to the repl's current file
withCurrentFile :: ReplM a -> ReplM a
withCurrentFile :: forall a. ReplM a -> ReplM a
withCurrentFile ReplM a
cont = do
  mpath <- (ReplState -> Maybe AbsolutePath) -> ReplM (Maybe AbsolutePath)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ReplState -> Maybe AbsolutePath
currentFile
  i <- traverse idFromFile mpath
  localTC (set eCurrentPath i) cont

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

showConstraints :: [String] -> TCM ()
showConstraints :: [[Char]] -> TCM ()
showConstraints [] =
    do  cs <- Rewrite -> TCM [OutputForm Expr Expr]
BasicOps.getConstraints Rewrite
AsIs
        liftIO $ putStrLn $ unlines (List.map prettyShow cs)
showConstraints [[Char]]
_ = 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
$ [Char] -> IO ()
putStrLn [Char]
":constraints [cid]"


showMetas :: [String] -> TCM ()
showMetas :: [[Char]] -> TCM ()
showMetas [[Char]
m] =
    do  i <- Int -> InteractionId
InteractionId (Int -> InteractionId) -> TCMT IO Int -> TCMT IO InteractionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> TCMT IO Int
forall a. Read a => [Char] -> TCM a
readM [Char]
m
        withInteractionId i $ do
          s <- typeOfMeta AsIs i
          r <- getInteractionRange i
          d <- prettyA s
          liftIO $ putStrLn $ render d ++ " " ++ prettyShow r
showMetas [[Char]
m,[Char]
"normal"] =
    do  i <- Int -> InteractionId
InteractionId (Int -> InteractionId) -> TCMT IO Int -> TCMT IO InteractionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> TCMT IO Int
forall a. Read a => [Char] -> TCM a
readM [Char]
m
        withInteractionId i $ do
          s <- prettyA =<< typeOfMeta Normalised i
          r <- getInteractionRange i
          liftIO $ putStrLn $ render s ++ " " ++ prettyShow r
showMetas [] =
    do  interactionMetas <- Rewrite -> TCM [OutputConstraint_boot TCErr Expr InteractionId]
typesOfVisibleMetas Rewrite
AsIs
        hiddenMetas      <- typesOfHiddenMetas  AsIs
        mapM_ (liftIO . print) =<< mapM showII interactionMetas
        mapM_ print' hiddenMetas
    where
        showII :: OutputConstraint_boot TCErr a InteractionId -> m (Doc Aspects)
showII OutputConstraint_boot TCErr a InteractionId
o = InteractionId -> m (Doc Aspects) -> m (Doc Aspects)
forall (m :: * -> *) a.
(MonadDebug m, MonadError TCErr 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' SrcFile
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot TCErr a InteractionId
-> OutputForm a InteractionId
forall tcErr a b.
Range' SrcFile
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot tcErr a b
-> OutputForm_boot tcErr a b
OutputForm Range' SrcFile
forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint_boot TCErr a InteractionId
o) (m (Doc Aspects) -> m (Doc Aspects))
-> m (Doc Aspects) -> m (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ OutputConstraint_boot TCErr a InteractionId -> m (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyA OutputConstraint_boot TCErr a InteractionId
o
        showM :: OutputConstraint_boot TCErr a NamedMeta -> m (Doc Aspects)
showM  OutputConstraint_boot TCErr a NamedMeta
o = MetaId -> m (Doc Aspects) -> m (Doc Aspects)
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m, MonadTrace m) =>
MetaId -> m a -> m a
withMetaId (NamedMeta -> MetaId
nmid (NamedMeta -> MetaId) -> NamedMeta -> MetaId
forall a b. (a -> b) -> a -> b
$ OutputForm a NamedMeta -> NamedMeta
forall a b. OutputForm a b -> b
outputFormId (OutputForm a NamedMeta -> NamedMeta)
-> OutputForm a NamedMeta -> NamedMeta
forall a b. (a -> b) -> a -> b
$ Range' SrcFile
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot TCErr a NamedMeta
-> OutputForm a NamedMeta
forall tcErr a b.
Range' SrcFile
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot tcErr a b
-> OutputForm_boot tcErr a b
OutputForm Range' SrcFile
forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint_boot TCErr a NamedMeta
o) (m (Doc Aspects) -> m (Doc Aspects))
-> m (Doc Aspects) -> m (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ OutputConstraint_boot TCErr a NamedMeta -> m (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyA OutputConstraint_boot TCErr a NamedMeta
o

        metaId :: OutputConstraint_boot tcErr a b -> b
metaId (OfType b
i a
_) = b
i
        metaId (JustType b
i) = b
i
        metaId (JustSort b
i) = b
i
        metaId (Assign b
i a
e) = b
i
        metaId OutputConstraint_boot tcErr a b
_ = b
forall a. HasCallStack => a
__IMPOSSIBLE__
        print' :: OutputConstraint_boot TCErr a NamedMeta -> m ()
print' OutputConstraint_boot TCErr a NamedMeta
x = do
            r <- MetaId -> m (Range' SrcFile)
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m (Range' SrcFile)
getMetaRange (MetaId -> m (Range' SrcFile)) -> MetaId -> m (Range' SrcFile)
forall a b. (a -> b) -> a -> b
$ NamedMeta -> MetaId
nmid (NamedMeta -> MetaId) -> NamedMeta -> MetaId
forall a b. (a -> b) -> a -> b
$ OutputConstraint_boot TCErr a NamedMeta -> NamedMeta
forall {tcErr} {a} {b}. OutputConstraint_boot tcErr a b -> b
metaId OutputConstraint_boot TCErr a NamedMeta
x
            d <- showM x
            liftIO $ putStrLn $ render d ++ "  [ at " ++ prettyShow r ++ " ]"
showMetas [[Char]]
_ = 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
$ [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
":meta [metaid]"


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

metaParseExpr ::  InteractionId -> String -> TCM A.Expr
metaParseExpr :: InteractionId -> [Char] -> TCM Expr
metaParseExpr InteractionId
ii [Char]
s =
    do  m <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
        scope <- getMetaScope <$> lookupLocalMeta m
        r <- getRange <$> lookupLocalMeta m
        -- liftIO $ putStrLn $ prettyShow scope
        let pos = Position' SrcFile -> Maybe (Position' SrcFile) -> Position' SrcFile
forall a. a -> Maybe a -> a
fromMaybe Position' SrcFile
forall a. HasCallStack => a
__IMPOSSIBLE__ (Range' SrcFile -> Maybe (Position' SrcFile)
forall a. Range' a -> Maybe (Position' a)
rStart Range' SrcFile
r)
        (e, attrs) <- runPM $ parsePosString exprParser pos s
        checkAttributes attrs
        concreteToAbstract scope e

actOnMeta :: [String] -> (InteractionId -> A.Expr -> TCM a) -> TCM a
actOnMeta :: forall a. [[Char]] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta ([Char]
is:[[Char]]
es) InteractionId -> Expr -> TCM a
f =
     do  i <- [Char] -> TCMT IO Int
forall a. Read a => [Char] -> TCM a
readM [Char]
is
         let ii = Int -> InteractionId
InteractionId Int
i
         e <- metaParseExpr ii (unwords es)
         withInteractionId ii $ f ii e
actOnMeta [[Char]]
_ InteractionId -> Expr -> TCM a
_ = TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__


giveMeta :: [String] -> TCM ()
giveMeta :: [[Char]] -> TCM ()
giveMeta [[Char]]
s | [[Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Char]]
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2 = do
  _ <- [[Char]] -> (InteractionId -> Expr -> TCM Expr) -> TCM Expr
forall a. [[Char]] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta [[Char]]
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 -> Expr -> TCM Expr
give UseForce
WithoutForce InteractionId
ii Expr
e
  return ()
giveMeta [[Char]]
_ = 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
$ [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
": give" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" metaid expr"



refineMeta :: [String] -> TCM ()
refineMeta :: [[Char]] -> TCM ()
refineMeta [[Char]]
s | [[Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Char]]
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2 = do
  _ <- [[Char]] -> (InteractionId -> Expr -> TCM Expr) -> TCM Expr
forall a. [[Char]] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta [[Char]]
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 -> Expr -> TCM Expr
refine UseForce
WithoutForce InteractionId
ii Expr
e
  return ()
refineMeta [[Char]]
_ = 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
$ [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
": refine" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" metaid expr"



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


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

parseExpr :: String -> TCM A.Expr
parseExpr :: [Char] -> TCM Expr
parseExpr [Char]
s = do
    (e, attrs) <- PM (Expr, Attributes) -> TCM (Expr, Attributes)
forall a. PM a -> TCM a
runPM (PM (Expr, Attributes) -> TCM (Expr, Attributes))
-> PM (Expr, Attributes) -> TCM (Expr, Attributes)
forall a b. (a -> b) -> a -> b
$ Parser Expr -> [Char] -> PM (Expr, Attributes)
forall a. Parser a -> [Char] -> PM (a, Attributes)
parse Parser Expr
exprParser [Char]
s
    checkAttributes attrs
    localToAbstract e return

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

typeOf :: [String] -> TCM ()
typeOf :: [[Char]] -> TCM ()
typeOf [[Char]]
s =
    do  e  <- [Char] -> TCM Expr
parseExpr ([[Char]] -> [Char]
unwords [[Char]]
s)
        e0 <- typeInCurrent Normalised e
        e1 <- typeInCurrent AsIs e
        liftIO . print =<< prettyA e1

typeIn :: [String] -> TCM ()
typeIn :: [[Char]] -> TCM ()
typeIn s :: [[Char]]
s@([Char]
_:[Char]
_:[[Char]]
_) =
    [[Char]] -> (InteractionId -> Expr -> TCM ()) -> TCM ()
forall a. [[Char]] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta [[Char]]
s ((InteractionId -> Expr -> TCM ()) -> TCM ())
-> (InteractionId -> Expr -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \InteractionId
i Expr
e ->
    do  e1 <- InteractionId -> Rewrite -> Expr -> TCM Expr
typeInMeta InteractionId
i Rewrite
Normalised Expr
e
        e2 <- typeInMeta i AsIs e
        liftIO . print =<< prettyA e1
typeIn [[Char]]
_ = 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
$ [Char] -> IO ()
putStrLn [Char]
":typeIn meta expr"

showContext :: [String] -> TCM ()
showContext :: [[Char]] -> TCM ()
showContext ([Char]
meta:[[Char]]
args) = do
    i <- Int -> InteractionId
InteractionId (Int -> InteractionId) -> TCMT IO Int -> TCMT IO InteractionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> TCMT IO Int
forall a. Read a => [Char] -> TCM a
readM [Char]
meta
    mi <- lookupLocalMeta =<< lookupInteractionId i
    withMetaInfo (getMetaInfo mi) $ do
      ctx <- List.map I.unDom . telToList <$> getContextTelescope
      zipWithM_ display ctx $ reverse $ zipWith const [1..] ctx
    where
        display :: ([Char], Type) -> Int -> TCM ()
display ([Char]
x, Type
t) Int
n = do
            t <- case [[Char]]
args of
                    [[Char]
"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
$ Int -> Type -> Type
forall a. Subst a => Int -> a -> a
raise Int
n Type
t
                    [[Char]]
_          -> 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
$ Int -> Type -> Type
forall a. Subst a => Int -> a -> a
raise Int
n Type
t
            d <- prettyTCM t
            liftIO $ print $ text (argNameToString x) <+> ":" <+> d
showContext [[Char]]
_ = 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
$ [Char] -> IO ()
putStrLn [Char]
":Context meta"

-- | The logo that prints when Agda is started in interactive mode.
splashScreen :: String
splashScreen :: [Char]
splashScreen = [[Char]] -> [Char]
unlines
    [ [Char]
"                 _ "
    , [Char]
"   ____         | |"
    , [Char]
"  / __ \\        | |"
    , [Char]
" | |__| |___  __| | ___"
    , [Char]
" |  __  / _ \\/ _  |/ __\\     Agda Interactive"
    , [Char]
" | |  |/ /_\\ \\/_| / /_| \\"
    , [Char]
" |_|  |\\___  /____\\_____/    Type :? for help."
    , [Char]
"        __/ /"
    , [Char]
"        \\__/"
    , [Char]
""
    -- , "The interactive mode is no longer supported. Don't complain if it doesn't work."
    , [Char]
"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 = [Char] -> IO ()
putStr ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
    [ [Char]
"Command overview" ] [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ (Command a -> [Char]) -> [Command a] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
List.map Command a -> [Char]
forall {b}. ([Char], b) -> [Char]
explain [Command a]
cs [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++
    [ [Char]
"<exp> Infer type of expression <exp> and evaluate it." ]
    where
        explain :: ([Char], b) -> [Char]
explain ([Char]
x,b
_) = [Char]
":" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
x

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

readM :: Read a => String -> TCM a
readM :: forall a. Read a => [Char] -> TCM a
readM [Char]
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
$ [Char] -> Maybe a
forall a. Read a => [Char] -> Maybe a
readMaybe [Char]
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
$ [Char] -> TCErr
GenericException ([Char] -> TCErr) -> [Char] -> TCErr
forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot parse: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s