module Agda.Interaction.CommandLine
( runInteractionLoop
) where
import Control.Monad
import Control.Monad.Except
import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.State
import Control.Monad.Reader
import qualified Data.List as List
import Data.Maybe
import Text.Read (readMaybe)
import Agda.Interaction.Base hiding (Command)
import Agda.Interaction.BasicOps as BasicOps hiding (parseExpr)
import Agda.Interaction.Imports ( CheckResult, crInterface )
import Agda.Interaction.Monad
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty
import Agda.Syntax.Internal (telToList, alwaysUnblock)
import qualified Agda.Syntax.Internal as I
import Agda.Syntax.Parser
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.Syntax.Abstract.Pretty
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Pretty ( PrettyTCM(prettyTCM) )
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Warnings (runPM)
import Agda.Utils.FileName (absolute, AbsolutePath)
import Agda.Utils.Maybe (caseMaybeM)
import Agda.Utils.Impossible
data ReplEnv = ReplEnv
{ ReplEnv -> TCM ()
replSetupAction :: TCM ()
, ReplEnv -> AbsolutePath -> TCM CheckResult
replTypeCheckAction :: AbsolutePath -> TCM CheckResult
}
data ReplState = ReplState
{ ReplState -> Maybe AbsolutePath
currentFile :: Maybe AbsolutePath
}
newtype ReplM a = ReplM { forall a. ReplM a -> ReaderT ReplEnv (StateT ReplState IM) a
unReplM :: ReaderT ReplEnv (StateT ReplState IM) a }
deriving
( forall a b. a -> ReplM b -> ReplM a
forall a b. (a -> b) -> ReplM a -> ReplM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> ReplM b -> ReplM a
$c<$ :: forall a b. a -> ReplM b -> ReplM a
fmap :: forall a b. (a -> b) -> ReplM a -> ReplM b
$cfmap :: forall a b. (a -> b) -> ReplM a -> ReplM b
Functor, Functor ReplM
forall a. a -> ReplM a
forall a b. ReplM a -> ReplM b -> ReplM a
forall a b. ReplM a -> ReplM b -> ReplM b
forall a b. ReplM (a -> b) -> ReplM a -> ReplM b
forall a b c. (a -> b -> c) -> ReplM a -> ReplM b -> ReplM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. ReplM a -> ReplM b -> ReplM a
$c<* :: forall a b. ReplM a -> ReplM b -> ReplM a
*> :: forall a b. ReplM a -> ReplM b -> ReplM b
$c*> :: forall a b. ReplM a -> ReplM b -> ReplM b
liftA2 :: forall a b c. (a -> b -> c) -> ReplM a -> ReplM b -> ReplM c
$cliftA2 :: forall a b c. (a -> b -> c) -> ReplM a -> ReplM b -> ReplM c
<*> :: forall a b. ReplM (a -> b) -> ReplM a -> ReplM b
$c<*> :: forall a b. ReplM (a -> b) -> ReplM a -> ReplM b
pure :: forall a. a -> ReplM a
$cpure :: forall a. a -> ReplM a
Applicative, Applicative ReplM
forall a. a -> ReplM a
forall a b. ReplM a -> ReplM b -> ReplM b
forall a b. ReplM a -> (a -> ReplM b) -> ReplM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> ReplM a
$creturn :: forall a. a -> ReplM a
>> :: forall a b. ReplM a -> ReplM b -> ReplM b
$c>> :: forall a b. ReplM a -> ReplM b -> ReplM b
>>= :: forall a b. ReplM a -> (a -> ReplM b) -> ReplM b
$c>>= :: forall a b. ReplM a -> (a -> ReplM b) -> ReplM b
Monad, Monad ReplM
forall a. IO a -> ReplM a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> ReplM a
$cliftIO :: forall a. IO a -> ReplM a
MonadIO
, Monad ReplM
Functor ReplM
Applicative ReplM
ReplM PragmaOptions
ReplM CommandLineOptions
forall (m :: * -> *).
Functor m
-> Applicative m
-> Monad m
-> m PragmaOptions
-> m CommandLineOptions
-> HasOptions m
commandLineOptions :: ReplM CommandLineOptions
$ccommandLineOptions :: ReplM CommandLineOptions
pragmaOptions :: ReplM PragmaOptions
$cpragmaOptions :: ReplM PragmaOptions
HasOptions, Monad ReplM
ReplM TCEnv
forall a. (TCEnv -> TCEnv) -> ReplM a -> ReplM a
forall (m :: * -> *).
Monad m
-> m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> m a -> m a)
-> MonadTCEnv m
localTC :: forall a. (TCEnv -> TCEnv) -> ReplM a -> ReplM a
$clocalTC :: forall a. (TCEnv -> TCEnv) -> ReplM a -> ReplM a
askTC :: ReplM TCEnv
$caskTC :: ReplM TCEnv
MonadTCEnv, Monad ReplM
ReplM TCState
forall a. (TCState -> TCState) -> ReplM a -> ReplM a
forall a b. Lens' TCState a -> (a -> a) -> ReplM b -> ReplM b
forall (m :: * -> *).
Monad m
-> m TCState
-> (forall a b. Lens' TCState a -> (a -> a) -> m b -> m b)
-> (forall a. (TCState -> TCState) -> m a -> m a)
-> ReadTCState m
withTCState :: forall a. (TCState -> TCState) -> ReplM a -> ReplM a
$cwithTCState :: forall a. (TCState -> TCState) -> ReplM a -> ReplM a
locallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> ReplM b -> ReplM b
$clocallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> ReplM b -> ReplM b
getTCState :: ReplM TCState
$cgetTCState :: ReplM TCState
ReadTCState, Monad ReplM
ReplM TCState
TCState -> ReplM ()
(TCState -> TCState) -> ReplM ()
forall (m :: * -> *).
Monad m
-> m TCState
-> (TCState -> m ())
-> ((TCState -> TCState) -> m ())
-> MonadTCState m
modifyTC :: (TCState -> TCState) -> ReplM ()
$cmodifyTC :: (TCState -> TCState) -> ReplM ()
putTC :: TCState -> ReplM ()
$cputTC :: TCState -> ReplM ()
getTC :: ReplM TCState
$cgetTC :: ReplM TCState
MonadTCState, Applicative ReplM
MonadIO ReplM
HasOptions ReplM
MonadTCState ReplM
MonadTCEnv ReplM
forall a. TCM a -> ReplM a
forall (tcm :: * -> *).
Applicative tcm
-> MonadIO tcm
-> MonadTCEnv tcm
-> MonadTCState tcm
-> HasOptions tcm
-> (forall a. TCM a -> tcm a)
-> MonadTCM tcm
liftTCM :: forall a. TCM a -> ReplM a
$cliftTCM :: forall a. TCM a -> ReplM a
MonadTCM
, MonadError TCErr
, MonadReader ReplEnv, MonadState ReplState
)
runReplM :: Maybe AbsolutePath -> TCM () -> (AbsolutePath -> TCM CheckResult) -> ReplM () -> TCM ()
runReplM :: Maybe AbsolutePath
-> TCM ()
-> (AbsolutePath -> TCM CheckResult)
-> ReplM ()
-> TCM ()
runReplM Maybe AbsolutePath
initialFile TCM ()
setup AbsolutePath -> TCM CheckResult
checkInterface
= forall a. IM a -> TCM a
runIM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Maybe AbsolutePath -> ReplState
ReplState Maybe AbsolutePath
initialFile)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReplEnv
replEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ReplM a -> ReaderT ReplEnv (StateT ReplState IM) a
unReplM
where
replEnv :: ReplEnv
replEnv = ReplEnv
{ replSetupAction :: TCM ()
replSetupAction = TCM ()
setup
, replTypeCheckAction :: AbsolutePath -> TCM CheckResult
replTypeCheckAction = AbsolutePath -> TCM CheckResult
checkInterface
}
data ExitCode a = Continue | ContinueIn TCEnv | Return a
type Command a = (String, [String] -> ReplM (ExitCode a))
matchCommand :: String -> [Command a] -> Either [String] ([String] -> ReplM (ExitCode a))
matchCommand :: forall a.
String
-> [Command a] -> Either [String] ([String] -> ReplM (ExitCode a))
matchCommand String
x [Command a]
cmds =
case forall a. (a -> Bool) -> [a] -> [a]
List.filter (forall a. Eq a => [a] -> [a] -> Bool
List.isPrefixOf String
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [Command a]
cmds of
[(String
_,[String] -> ReplM (ExitCode a)
m)] -> forall a b. b -> Either a b
Right [String] -> ReplM (ExitCode a)
m
[Command a]
xs -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
List.map forall a b. (a, b) -> a
fst [Command a]
xs
interaction :: String -> [Command a] -> (String -> TCM (ExitCode a)) -> ReplM a
interaction :: forall a.
String -> [Command a] -> (String -> TCM (ExitCode a)) -> ReplM a
interaction String
prompt [Command a]
cmds String -> TCM (ExitCode a)
eval = ReplM a
loop
where
go :: ExitCode a -> ReplM a
go (Return a
x) = forall (m :: * -> *) a. Monad m => a -> m a
return a
x
go ExitCode a
Continue = ReplM a
loop
go (ContinueIn TCEnv
env) = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (forall a b. a -> b -> a
const TCEnv
env) ReplM a
loop
loop :: ReplM a
loop =
do Maybe String
ms <- forall a. ReaderT ReplEnv (StateT ReplState IM) a -> ReplM a
ReplM forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ String -> IM (Maybe String)
readline String
prompt
case forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> [String]
words Maybe String
ms of
Maybe [String]
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => String -> a
error String
"** EOF **"
Just [] -> ReplM a
loop
Just ((Char
':':String
cmd):[String]
args) ->
do case forall a.
String
-> [Command a] -> Either [String] ([String] -> ReplM (ExitCode a))
matchCommand String
cmd [Command a]
cmds of
Right [String] -> ReplM (ExitCode a)
c -> ExitCode a -> ReplM a
go forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ([String] -> ReplM (ExitCode a)
c [String]
args)
Left [] ->
do forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Unknown command '" forall a. [a] -> [a] -> [a]
++ String
cmd forall a. [a] -> [a] -> [a]
++ String
"'"
ReplM a
loop
Left [String]
xs ->
do forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"More than one command match: " forall a. [a] -> [a] -> [a]
++
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " [String]
xs
ReplM a
loop
Just [String]
_ ->
do ExitCode a -> ReplM a
go forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (String -> TCM (ExitCode a)
eval forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => Maybe a -> a
fromJust Maybe String
ms)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
e ->
do String
s <- forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
renderError TCErr
e
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
s
ReplM a
loop
runInteractionLoop :: Maybe AbsolutePath -> TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM ()
runInteractionLoop :: Maybe AbsolutePath
-> TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM ()
runInteractionLoop Maybe AbsolutePath
initialFile TCM ()
setup AbsolutePath -> TCM CheckResult
check = Maybe AbsolutePath
-> TCM ()
-> (AbsolutePath -> TCM CheckResult)
-> ReplM ()
-> TCM ()
runReplM Maybe AbsolutePath
initialFile TCM ()
setup AbsolutePath -> TCM CheckResult
check ReplM ()
interactionLoop
replSetup :: ReplM ()
replSetup :: ReplM ()
replSetup = do
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ReplEnv -> TCM ()
replSetupAction
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStr String
splashScreen
checkCurrentFile :: ReplM (Maybe CheckResult)
checkCurrentFile :: ReplM (Maybe CheckResult)
checkCurrentFile = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse AbsolutePath -> ReplM CheckResult
checkFile forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ReplState -> Maybe AbsolutePath
currentFile
checkFile :: AbsolutePath -> ReplM CheckResult
checkFile :: AbsolutePath -> ReplM CheckResult
checkFile AbsolutePath
file = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (a -> b) -> a -> b
$ AbsolutePath
file) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ReplEnv -> AbsolutePath -> TCM CheckResult
replTypeCheckAction
interactionLoop :: ReplM ()
interactionLoop :: ReplM ()
interactionLoop = do
ReplM ()
replSetup
ReplM ()
reload
forall a.
String -> [Command a] -> (String -> TCM (ExitCode a)) -> ReplM a
interaction String
"Main> " [(String, [String] -> ReplM (ExitCode ()))]
commands forall a. String -> TCM (ExitCode a)
evalTerm
where
ReplM ()
reload :: ReplM () = do
Maybe CheckResult
checked <- ReplM (Maybe CheckResult)
checkCurrentFile
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ ScopeInfo -> TCM ()
setScope forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe ScopeInfo
emptyScopeInfo (Interface -> ScopeInfo
iInsideScope forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckResult -> Interface
crInterface) Maybe CheckResult
checked
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Maybe a -> Bool
isNothing Maybe CheckResult
checked) forall a b. (a -> b) -> a -> b
$ do
forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM ScopeM [Declaration]
importPrimitives
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
e -> do
String
s <- forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
renderError TCErr
e
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
s
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Failed."
commands :: [(String, [String] -> ReplM (ExitCode ()))]
commands =
[ String
"quit" forall {a} {b}. a -> b -> (a, b)
|> \[String]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> ExitCode a
Return ()
, String
"?" forall {a} {b}. a -> b -> (a, b)
|> \[String]
_ -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. [Command a] -> IO ()
help [(String, [String] -> ReplM (ExitCode ()))]
commands
, String
"reload" forall {a} {b}. a -> b -> (a, b)
|> \[String]
_ -> do ReplM ()
reload
forall a. TCEnv -> ExitCode a
ContinueIn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
, String
"constraints" forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
showConstraints [String]
args
, String
"Context" forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
showContext [String]
args
, String
"give" forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
giveMeta [String]
args
, String
"Refine" forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
refineMeta [String]
args
, String
"metas" forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
showMetas [String]
args
, String
"load" forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ ReplM () -> [String] -> ReplM ()
loadFile ReplM ()
reload [String]
args
, String
"eval" forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
evalIn [String]
args
, String
"typeOf" forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
typeOf [String]
args
, String
"typeIn" forall {a} {b}. a -> b -> (a, b)
|> \[String]
args -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
typeIn [String]
args
, String
"wakeup" forall {a} {b}. a -> b -> (a, b)
|> \[String]
_ -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ TCM ()
retryConstraints
, String
"scope" forall {a} {b}. a -> b -> (a, b)
|> \[String]
_ -> forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ TCM ()
showScope
]
where
|> :: a -> b -> (a, b)
(|>) = (,)
continueAfter :: ReplM a -> ReplM (ExitCode b)
continueAfter :: forall a b. ReplM a -> ReplM (ExitCode b)
continueAfter ReplM a
m = forall a. ReplM a -> ReplM a
withCurrentFile forall a b. (a -> b) -> a -> b
$ do
ReplM a
m forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. ExitCode a
Continue
withCurrentFile :: ReplM a -> ReplM a
withCurrentFile :: forall a. ReplM a -> ReplM a
withCurrentFile ReplM a
cont = do
Maybe AbsolutePath
mpath <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ReplState -> Maybe AbsolutePath
currentFile
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envCurrentPath :: Maybe AbsolutePath
envCurrentPath = Maybe AbsolutePath
mpath }) ReplM a
cont
loadFile :: ReplM () -> [String] -> ReplM ()
loadFile :: ReplM () -> [String] -> ReplM ()
loadFile ReplM ()
reload [String
file] = do
AbsolutePath
absPath <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO AbsolutePath
absolute String
file
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\(ReplState Maybe AbsolutePath
_prevFile) -> Maybe AbsolutePath -> ReplState
ReplState (forall a. a -> Maybe a
Just AbsolutePath
absPath))
forall a. ReplM a -> ReplM a
withCurrentFile ReplM ()
reload
loadFile ReplM ()
_ [String]
_ = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
":load file"
showConstraints :: [String] -> TCM ()
showConstraints :: [String] -> TCM ()
showConstraints [] =
do [OutputForm Expr Expr]
cs <- TCM [OutputForm Expr Expr]
BasicOps.getConstraints
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines (forall a b. (a -> b) -> [a] -> [b]
List.map forall a. Pretty a => a -> String
prettyShow [OutputForm Expr Expr]
cs)
showConstraints [String]
_ = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
":constraints [cid]"
showMetas :: [String] -> TCM ()
showMetas :: [String] -> TCM ()
showMetas [String
m] =
do InteractionId
i <- Nat -> InteractionId
InteractionId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Read a => String -> TCM a
readM String
m
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
i forall a b. (a -> b) -> a -> b
$ do
OutputConstraint Expr InteractionId
s <- Rewrite
-> InteractionId -> TCM (OutputConstraint Expr InteractionId)
typeOfMeta Rewrite
AsIs InteractionId
i
Range
r <- forall (m :: * -> *).
(MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange InteractionId
i
Doc Aspects
d <- forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyA OutputConstraint Expr InteractionId
s
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall a. Doc a -> String
render Doc Aspects
d forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow Range
r
showMetas [String
m,String
"normal"] =
do InteractionId
i <- Nat -> InteractionId
InteractionId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Read a => String -> TCM a
readM String
m
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
i forall a b. (a -> b) -> a -> b
$ do
Doc Aspects
s <- forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyA forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Rewrite
-> InteractionId -> TCM (OutputConstraint Expr InteractionId)
typeOfMeta Rewrite
Normalised InteractionId
i
Range
r <- forall (m :: * -> *).
(MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange InteractionId
i
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall a. Doc a -> String
render Doc Aspects
s forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow Range
r
showMetas [] =
do [OutputConstraint Expr InteractionId]
interactionMetas <- Rewrite -> TCM [OutputConstraint Expr InteractionId]
typesOfVisibleMetas Rewrite
AsIs
[OutputConstraint Expr NamedMeta]
hiddenMetas <- Rewrite -> TCM [OutputConstraint Expr NamedMeta]
typesOfHiddenMetas Rewrite
AsIs
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> IO ()
print) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {m :: * -> *} {a}.
(MonadError TCErr m, MonadTrace m, ToConcrete a,
Pretty (ConOfAbs a), MonadFresh NameId m, MonadInteractionPoints m,
MonadStConcreteNames m, PureTCM m, IsString (m (Doc Aspects)),
Null (m (Doc Aspects)), Semigroup (m (Doc Aspects))) =>
OutputConstraint a InteractionId -> m (Doc Aspects)
showII [OutputConstraint Expr InteractionId]
interactionMetas
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {m :: * -> *} {a}.
(MonadTrace m, ToConcrete a, Pretty (ConOfAbs a),
MonadFresh NameId m, MonadInteractionPoints m,
MonadStConcreteNames m, PureTCM m, IsString (m (Doc Aspects)),
Null (m (Doc Aspects)), Semigroup (m (Doc Aspects)), MonadIO m) =>
OutputConstraint a NamedMeta -> m ()
print' [OutputConstraint Expr NamedMeta]
hiddenMetas
where
showII :: OutputConstraint a InteractionId -> m (Doc Aspects)
showII OutputConstraint a InteractionId
o = forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId (forall a b. OutputForm a b -> b
outputFormId forall a b. (a -> b) -> a -> b
$ forall a b.
Range
-> [ProblemId] -> Blocker -> OutputConstraint a b -> OutputForm a b
OutputForm forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint a InteractionId
o) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyA OutputConstraint a InteractionId
o
showM :: OutputConstraint a NamedMeta -> m (Doc Aspects)
showM OutputConstraint a NamedMeta
o = forall (m :: * -> *) a.
(HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
ReadTCState m) =>
MetaId -> m a -> m a
withMetaId (NamedMeta -> MetaId
nmid forall a b. (a -> b) -> a -> b
$ forall a b. OutputForm a b -> b
outputFormId forall a b. (a -> b) -> a -> b
$ forall a b.
Range
-> [ProblemId] -> Blocker -> OutputConstraint a b -> OutputForm a b
OutputForm forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint a NamedMeta
o) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyA OutputConstraint a NamedMeta
o
metaId :: OutputConstraint a b -> b
metaId (OfType b
i a
_) = b
i
metaId (JustType b
i) = b
i
metaId (JustSort b
i) = b
i
metaId (Assign b
i a
e) = b
i
metaId OutputConstraint a b
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
print' :: OutputConstraint a NamedMeta -> m ()
print' OutputConstraint a NamedMeta
x = do
Range
r <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange forall a b. (a -> b) -> a -> b
$ NamedMeta -> MetaId
nmid forall a b. (a -> b) -> a -> b
$ forall {a} {b}. OutputConstraint a b -> b
metaId OutputConstraint a NamedMeta
x
Doc Aspects
d <- forall {m :: * -> *} {a}.
(MonadTrace m, ToConcrete a, Pretty (ConOfAbs a),
MonadFresh NameId m, MonadInteractionPoints m,
MonadStConcreteNames m, PureTCM m, IsString (m (Doc Aspects)),
Null (m (Doc Aspects)), Semigroup (m (Doc Aspects))) =>
OutputConstraint a NamedMeta -> m (Doc Aspects)
showM OutputConstraint a NamedMeta
x
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall a. Doc a -> String
render Doc Aspects
d forall a. [a] -> [a] -> [a]
++ String
" [ at " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow Range
r forall a. [a] -> [a] -> [a]
++ String
" ]"
showMetas [String]
_ = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
":meta [metaid]"
showScope :: TCM ()
showScope :: TCM ()
showScope = do
ScopeInfo
scope <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> String
prettyShow ScopeInfo
scope
metaParseExpr :: InteractionId -> String -> TCM A.Expr
metaParseExpr :: InteractionId -> String -> TCM Expr
metaParseExpr InteractionId
ii String
s =
do MetaId
m <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
ScopeInfo
scope <- MetaVariable -> ScopeInfo
getMetaScope forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
Range
r <- forall a. HasRange a => a -> Range
getRange forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
let pos :: Position' SrcFile
pos = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. Range' a -> Maybe (Position' a)
rStart Range
r)
(Expr
e, Attributes
attrs) <- forall a. PM a -> TCM a
runPM forall a b. (a -> b) -> a -> b
$ forall a.
Parser a -> Position' SrcFile -> String -> PM (a, Attributes)
parsePosString Parser Expr
exprParser Position' SrcFile
pos String
s
Attributes -> TCM ()
checkAttributes Attributes
attrs
forall c. ToAbstract c => ScopeInfo -> c -> ScopeM (AbsOfCon c)
concreteToAbstract ScopeInfo
scope Expr
e
actOnMeta :: [String] -> (InteractionId -> A.Expr -> TCM a) -> TCM a
actOnMeta :: forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta (String
is:[String]
es) InteractionId -> Expr -> TCM a
f =
do Nat
i <- forall a. Read a => String -> TCM a
readM String
is
let ii :: InteractionId
ii = Nat -> InteractionId
InteractionId Nat
i
Expr
e <- InteractionId -> String -> TCM Expr
metaParseExpr InteractionId
ii ([String] -> String
unwords [String]
es)
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$ InteractionId -> Expr -> TCM a
f InteractionId
ii Expr
e
actOnMeta [String]
_ InteractionId -> Expr -> TCM a
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
giveMeta :: [String] -> TCM ()
giveMeta :: [String] -> TCM ()
giveMeta [String]
s | forall (t :: * -> *) a. Foldable t => t a -> Nat
length [String]
s forall a. Ord a => a -> a -> Bool
>= Nat
2 = do
Expr
_ <- forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta [String]
s forall a b. (a -> b) -> a -> b
$ \ InteractionId
ii Expr
e -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
give UseForce
WithoutForce InteractionId
ii forall a. Maybe a
Nothing Expr
e
forall (m :: * -> *) a. Monad m => a -> m a
return ()
giveMeta [String]
_ = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
": give" forall a. [a] -> [a] -> [a]
++ String
" metaid expr"
refineMeta :: [String] -> TCM ()
refineMeta :: [String] -> TCM ()
refineMeta [String]
s | forall (t :: * -> *) a. Foldable t => t a -> Nat
length [String]
s forall a. Ord a => a -> a -> Bool
>= Nat
2 = do
Expr
_ <- forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta [String]
s forall a b. (a -> b) -> a -> b
$ \ InteractionId
ii Expr
e -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
refine UseForce
WithoutForce InteractionId
ii forall a. Maybe a
Nothing Expr
e
forall (m :: * -> *) a. Monad m => a -> m a
return ()
refineMeta [String]
_ = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
": refine" forall a. [a] -> [a] -> [a]
++ String
" metaid expr"
retryConstraints :: TCM ()
retryConstraints :: TCM ()
retryConstraints = TCM ()
wakeupConstraints_
evalIn :: [String] -> TCM ()
evalIn :: [String] -> TCM ()
evalIn [String]
s | forall (t :: * -> *) a. Foldable t => t a -> Nat
length [String]
s forall a. Ord a => a -> a -> Bool
>= Nat
2 =
do Doc Aspects
d <- forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta [String]
s forall a b. (a -> b) -> a -> b
$ \InteractionId
_ Expr
e -> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyA forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ComputeMode -> Expr -> TCM Expr
evalInCurrent ComputeMode
DefaultCompute Expr
e
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> IO ()
print Doc Aspects
d
evalIn [String]
_ = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
":eval metaid expr"
parseExpr :: String -> TCM A.Expr
parseExpr :: String -> TCM Expr
parseExpr String
s = do
(Expr
e, Attributes
attrs) <- forall a. PM a -> TCM a
runPM forall a b. (a -> b) -> a -> b
$ forall a. Parser a -> String -> PM (a, Attributes)
parse Parser Expr
exprParser String
s
Attributes -> TCM ()
checkAttributes Attributes
attrs
forall c b.
ToAbstract c =>
c -> (AbsOfCon c -> ScopeM b) -> ScopeM b
localToAbstract Expr
e forall (m :: * -> *) a. Monad m => a -> m a
return
evalTerm :: String -> TCM (ExitCode a)
evalTerm :: forall a. String -> TCM (ExitCode a)
evalTerm String
s =
do Expr
e <- String -> TCM Expr
parseExpr String
s
Expr
v <- ComputeMode -> Expr -> TCM Expr
evalInCurrent ComputeMode
DefaultCompute Expr
e
Doc Aspects
e <- forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
prettyTCM Expr
v
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> IO ()
print Doc Aspects
e
forall (m :: * -> *) a. Monad m => a -> m a
return forall a. ExitCode a
Continue
typeOf :: [String] -> TCM ()
typeOf :: [String] -> TCM ()
typeOf [String]
s =
do Expr
e <- String -> TCM Expr
parseExpr ([String] -> String
unwords [String]
s)
Expr
e0 <- Rewrite -> Expr -> TCM Expr
typeInCurrent Rewrite
Normalised Expr
e
Expr
e1 <- Rewrite -> Expr -> TCM Expr
typeInCurrent Rewrite
AsIs Expr
e
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(ToConcrete a, Show (ConOfAbs a), MonadAbsToCon m) =>
a -> m String
showA Expr
e1
typeIn :: [String] -> TCM ()
typeIn :: [String] -> TCM ()
typeIn s :: [String]
s@(String
_:String
_:[String]
_) =
forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta [String]
s forall a b. (a -> b) -> a -> b
$ \InteractionId
i Expr
e ->
do Expr
e1 <- InteractionId -> Rewrite -> Expr -> TCM Expr
typeInMeta InteractionId
i Rewrite
Normalised Expr
e
Expr
e2 <- InteractionId -> Rewrite -> Expr -> TCM Expr
typeInMeta InteractionId
i Rewrite
AsIs Expr
e
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(ToConcrete a, Show (ConOfAbs a), MonadAbsToCon m) =>
a -> m String
showA Expr
e1
typeIn [String]
_ = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
":typeIn meta expr"
showContext :: [String] -> TCM ()
showContext :: [String] -> TCM ()
showContext (String
meta:[String]
args) = do
InteractionId
i <- Nat -> InteractionId
InteractionId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Read a => String -> TCM a
readM String
meta
MetaVariable
mi <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
i
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mi) forall a b. (a -> b) -> a -> b
$ do
[(String, Type)]
ctx <- forall a b. (a -> b) -> [a] -> [b]
List.map forall t e. Dom' t e -> e
I.unDom forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Tele (Dom t) -> [Dom (String, t)]
telToList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (String, Type) -> Nat -> TCM ()
display [(String, Type)]
ctx forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a b. a -> b -> a
const [Nat
1..] [(String, Type)]
ctx
where
display :: (String, Type) -> Nat -> TCM ()
display (String
x, Type
t) Nat
n = do
Type
t <- case [String]
args of
[String
"normal"] -> forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise Nat
n Type
t
[String]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise Nat
n Type
t
Doc Aspects
d <- forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
prettyTCM Type
t
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> IO ()
print forall a b. (a -> b) -> a -> b
$ forall a. String -> Doc a
text (String -> String
argNameToString String
x) forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
":" forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
d
showContext [String]
_ = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
":Context meta"
splashScreen :: String
splashScreen :: String
splashScreen = [String] -> String
unlines
[ String
" _ "
, String
" ____ | |"
, String
" / __ \\ | |"
, String
" | |__| |___ __| | ___"
, String
" | __ / _ \\/ _ |/ __\\ Agda Interactive"
, String
" | | |/ /_\\ \\/_| / /_| \\"
, String
" |_| |\\___ /____\\_____/ Type :? for help."
, String
" __/ /"
, String
" \\__/"
, String
""
, String
"The interactive mode is no longer under active development. Use at your own risk."
]
help :: [Command a] -> IO ()
help :: forall a. [Command a] -> IO ()
help [Command a]
cs = String -> IO ()
putStr forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines forall a b. (a -> b) -> a -> b
$
[ String
"Command overview" ] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
List.map forall {b}. (String, b) -> String
explain [Command a]
cs forall a. [a] -> [a] -> [a]
++
[ String
"<exp> Infer type of expression <exp> and evaluate it." ]
where
explain :: (String, b) -> String
explain (String
x,b
_) = String
":" forall a. [a] -> [a] -> [a]
++ String
x
readM :: Read a => String -> TCM a
readM :: forall a. Read a => String -> TCM a
readM String
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCM a
err forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Read a => String -> Maybe a
readMaybe String
s
where
err :: TCM a
err = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String -> TCErr
strMsg forall a b. (a -> b) -> a -> b
$ String
"Cannot parse: " forall a. [a] -> [a] -> [a]
++ String
s
strMsg :: String -> TCErr
strMsg = Range -> Doc Aspects -> TCErr
Exception forall a. Range' a
noRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. String -> Doc a
text