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
interactionLoop :: ReplM ()
interactionLoop :: ReplM ()
interactionLoop = do
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
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
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
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
d <- OutputConstraint Expr InteractionId -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
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 -> String
forall a. Doc a -> String
render Doc
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
s <- OutputConstraint Expr InteractionId -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (OutputConstraint Expr InteractionId -> TCMT IO Doc)
-> TCM (OutputConstraint Expr InteractionId) -> TCMT IO Doc
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 -> String
forall a. Doc a -> String
render Doc
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 -> TCM ()) -> [Doc] -> 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 -> IO ()) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> IO ()
forall a. Show a => a -> IO ()
print) ([Doc] -> TCM ()) -> TCMT IO [Doc] -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (OutputConstraint Expr InteractionId -> TCMT IO Doc)
-> [OutputConstraint Expr InteractionId] -> TCMT IO [Doc]
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
forall {m :: * -> *} {a}.
(MonadError TCErr m, MonadTrace m, ToConcrete a,
Pretty (ConOfAbs a), MonadFresh NameId m, MonadInteractionPoints m,
MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
Semigroup (m Doc)) =>
OutputConstraint_boot TCErr a InteractionId -> m Doc
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), Null (m Doc),
Semigroup (m Doc), MonadIO m) =>
OutputConstraint_boot TCErr a NamedMeta -> m ()
print' [OutputConstraint Expr NamedMeta]
hiddenMetas
where
showII :: OutputConstraint_boot TCErr a InteractionId -> m Doc
showII OutputConstraint_boot TCErr a InteractionId
o = InteractionId -> m Doc -> m Doc
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_boot TCErr a InteractionId
-> OutputForm a InteractionId
forall tcErr a b.
Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot tcErr a b
-> OutputForm_boot tcErr a b
OutputForm Range
forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint_boot TCErr a InteractionId
o) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ OutputConstraint_boot TCErr a InteractionId -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA OutputConstraint_boot TCErr a InteractionId
o
showM :: OutputConstraint_boot TCErr a NamedMeta -> m Doc
showM OutputConstraint_boot TCErr a NamedMeta
o = MetaId -> m Doc -> m Doc
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_boot TCErr a NamedMeta
-> OutputForm a NamedMeta
forall tcErr a b.
Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot tcErr a b
-> OutputForm_boot tcErr a b
OutputForm Range
forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint_boot TCErr a NamedMeta
o) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ OutputConstraint_boot TCErr a NamedMeta -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
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
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_boot TCErr a NamedMeta -> NamedMeta
forall {tcErr} {a} {b}. OutputConstraint_boot tcErr a b -> b
metaId OutputConstraint_boot TCErr a NamedMeta
x
Doc
d <- OutputConstraint_boot TCErr a NamedMeta -> m Doc
forall {m :: * -> *} {a}.
(MonadTrace m, ToConcrete a, Pretty (ConOfAbs a),
MonadFresh NameId m, MonadInteractionPoints m,
MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
Semigroup (m Doc)) =>
OutputConstraint_boot TCErr a NamedMeta -> m Doc
showM OutputConstraint_boot TCErr 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 -> String
forall a. Doc a -> String
render Doc
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
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
d <- [String] -> (InteractionId -> Expr -> TCMT IO Doc) -> TCMT IO Doc
forall a. [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta [String]
s ((InteractionId -> Expr -> TCMT IO Doc) -> TCMT IO Doc)
-> (InteractionId -> Expr -> TCMT IO Doc) -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ \InteractionId
_ Expr
e -> Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> TCMT IO Doc) -> TCM Expr -> TCMT IO Doc
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 -> IO ()
forall a. Show a => a -> IO ()
print Doc
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
e <- Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
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 -> IO ()
forall a. Show a => a -> IO ()
print Doc
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
d <- Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
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 -> IO ()
forall a. Show a => a -> IO ()
print (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Doc
forall a. String -> Doc a
text (String -> String
argNameToString String
x) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
":" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
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"
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 (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
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 -> TCErr
Exception Range
forall a. Range' a
noRange (Doc -> TCErr) -> (String -> Doc) -> String -> TCErr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
forall a. String -> Doc a
text