module Agda.Interaction.CommandLine where

import Control.Monad.Reader

import qualified Data.List as List
import Data.Maybe

import Agda.Interaction.Base hiding (Command)
import Agda.Interaction.BasicOps as BasicOps hiding (parseExpr)
import Agda.Interaction.Monad

import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Internal (telToList)
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.TheTypeChecker
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.Except ( MonadError(catchError) )
import Agda.Utils.Monad
import Agda.Utils.Pretty

import Agda.Utils.Impossible

data ExitCode a = Continue | ContinueIn TCEnv | Return a

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

matchCommand :: String -> [Command a] -> Either [String] ([String] -> TCM (ExitCode a))
matchCommand :: String
-> [Command a] -> Either [String] ([String] -> TCM (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] -> TCM (ExitCode a)
m)] -> ([String] -> TCM (ExitCode a))
-> Either [String] ([String] -> TCM (ExitCode a))
forall a b. b -> Either a b
Right [String] -> TCM (ExitCode a)
m
        [Command a]
xs      -> [String] -> Either [String] ([String] -> TCM (ExitCode a))
forall a b. a -> Either a b
Left ([String] -> Either [String] ([String] -> TCM (ExitCode a)))
-> [String] -> Either [String] ([String] -> TCM (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)) -> IM a
interaction :: String -> [Command a] -> (String -> TCM (ExitCode a)) -> IM a
interaction String
prompt [Command a]
cmds String -> TCM (ExitCode a)
eval = IM a
loop
    where
        go :: ExitCode a -> IM a
go (Return a
x)       = a -> IM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
        go ExitCode a
Continue         = IM a
loop
        go (ContinueIn TCEnv
env) = (TCEnv -> TCEnv) -> IM a -> IM 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) IM a
loop

        loop :: IM a
loop =
            do  Maybe String
ms <- String -> IM (Maybe String)
readline String
prompt
                case (String -> [String]) -> Maybe String -> Maybe [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> [String]
words Maybe String
ms of
                    Maybe [String]
Nothing               -> a -> IM a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> IM a) -> a -> IM a
forall a b. (a -> b) -> a -> b
$ String -> a
forall a. HasCallStack => String -> a
error String
"** EOF **"
                    Just []               -> IM a
loop
                    Just ((Char
':':String
cmd):[String]
args) ->
                        do  case String
-> [Command a] -> Either [String] ([String] -> TCM (ExitCode a))
forall a.
String
-> [Command a] -> Either [String] ([String] -> TCM (ExitCode a))
matchCommand String
cmd [Command a]
cmds of
                                Right [String] -> TCM (ExitCode a)
c -> ExitCode a -> IM a
go (ExitCode a -> IM a) -> TCMT (InputT IO) (ExitCode a) -> IM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM (ExitCode a) -> TCMT (InputT IO) (ExitCode a)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM ([String] -> TCM (ExitCode a)
c [String]
args)
                                Left [] ->
                                    do  IO () -> TCMT (InputT IO) ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCMT (InputT IO) ()) -> IO () -> TCMT (InputT IO) ()
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
"'"
                                        IM a
loop
                                Left [String]
xs ->
                                    do  IO () -> TCMT (InputT IO) ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCMT (InputT IO) ()) -> IO () -> TCMT (InputT IO) ()
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
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (String -> [String] -> [String]
forall a. a -> [a] -> [a]
List.intersperse String
", " [String]
xs)
                                        IM a
loop
                    Just [String]
_ ->
                        do  ExitCode a -> IM a
go (ExitCode a -> IM a) -> TCMT (InputT IO) (ExitCode a) -> IM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM (ExitCode a) -> TCMT (InputT IO) (ExitCode 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)
            IM a -> (TCErr -> IM a) -> IM a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
e ->
                do  String
s <- TCM String -> TCMT (InputT IO) String
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM String -> TCMT (InputT IO) String)
-> TCM String -> TCMT (InputT IO) String
forall a b. (a -> b) -> a -> b
$ TCErr -> TCM String
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
prettyError TCErr
e
                    IO () -> TCMT (InputT IO) ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCMT (InputT IO) ()) -> IO () -> TCMT (InputT IO) ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
s
                    IM a
loop

-- | The interaction loop.
interactionLoop :: TCM (Maybe Interface) -> IM ()
interactionLoop :: TCM (Maybe Interface) -> TCMT (InputT IO) ()
interactionLoop TCM (Maybe Interface)
doTypeCheck =
    do  TCM () -> TCMT (InputT IO) ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCM ()
reload
        String
-> [Command ()]
-> (String -> TCM (ExitCode ()))
-> TCMT (InputT IO) ()
forall a.
String -> [Command a] -> (String -> TCM (ExitCode a)) -> IM a
interaction String
"Main> " [Command ()]
commands String -> TCM (ExitCode ())
forall a. String -> TCM (ExitCode a)
evalTerm
    where
        reload :: TCM ()
reload = do
            Maybe Interface
mi <- TCM (Maybe Interface)
doTypeCheck
            -- Note that mi is Nothing if (1) there is no input file or
            -- (2) the file type checked with unsolved metas and
            -- --allow-unsolved-metas was used. In the latter case the
            -- behaviour of agda -I may be surprising. If agda -I ever
            -- becomes properly supported again, then this behaviour
            -- should perhaps be fixed.
            ScopeInfo -> TCM ()
setScope (ScopeInfo -> TCM ()) -> ScopeInfo -> TCM ()
forall a b. (a -> b) -> a -> b
$ case Maybe Interface
mi of
              Just Interface
i  -> Interface -> ScopeInfo
iInsideScope Interface
i
              Maybe Interface
Nothing -> ScopeInfo
emptyScopeInfo
          TCM () -> (TCErr -> TCM ()) -> TCM ()
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
e -> do
            String
s <- TCErr -> TCM String
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
prettyError TCErr
e
            IO () -> TCM ()
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
s
            IO () -> TCM ()
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
"Failed."

        commands :: [Command ()]
commands =
            [ String
"quit"        String -> ([String] -> TCM (ExitCode ())) -> Command ()
forall a b. a -> b -> (a, b)
|>  \[String]
_ -> ExitCode () -> TCM (ExitCode ())
forall (m :: * -> *) a. Monad m => a -> m a
return (ExitCode () -> TCM (ExitCode ()))
-> ExitCode () -> TCM (ExitCode ())
forall a b. (a -> b) -> a -> b
$ () -> ExitCode ()
forall a. a -> ExitCode a
Return ()
            , String
"?"           String -> ([String] -> TCM (ExitCode ())) -> Command ()
forall a b. a -> b -> (a, b)
|>  \[String]
_ -> TCM () -> TCM (ExitCode ())
forall a b. TCM a -> TCM (ExitCode b)
continueAfter (TCM () -> TCM (ExitCode ())) -> TCM () -> TCM (ExitCode ())
forall a b. (a -> b) -> a -> b
$ IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Command ()] -> IO ()
forall a. [Command a] -> IO ()
help [Command ()]
commands
            , String
"reload"      String -> ([String] -> TCM (ExitCode ())) -> Command ()
forall a b. a -> b -> (a, b)
|>  \[String]
_ -> do TCM ()
reload
                                         TCEnv -> ExitCode ()
forall a. TCEnv -> ExitCode a
ContinueIn (TCEnv -> ExitCode ()) -> TCMT IO TCEnv -> TCM (ExitCode ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
            , String
"constraints" String -> ([String] -> TCM (ExitCode ())) -> Command ()
forall a b. a -> b -> (a, b)
|> \[String]
args -> TCM () -> TCM (ExitCode ())
forall a b. TCM a -> TCM (ExitCode b)
continueAfter (TCM () -> TCM (ExitCode ())) -> TCM () -> TCM (ExitCode ())
forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
showConstraints [String]
args
            , String
"Context"     String -> ([String] -> TCM (ExitCode ())) -> Command ()
forall a b. a -> b -> (a, b)
|> \[String]
args -> TCM () -> TCM (ExitCode ())
forall a b. TCM a -> TCM (ExitCode b)
continueAfter (TCM () -> TCM (ExitCode ())) -> TCM () -> TCM (ExitCode ())
forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
showContext [String]
args
            , String
"give"        String -> ([String] -> TCM (ExitCode ())) -> Command ()
forall a b. a -> b -> (a, b)
|> \[String]
args -> TCM () -> TCM (ExitCode ())
forall a b. TCM a -> TCM (ExitCode b)
continueAfter (TCM () -> TCM (ExitCode ())) -> TCM () -> TCM (ExitCode ())
forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
giveMeta [String]
args
            , String
"Refine"      String -> ([String] -> TCM (ExitCode ())) -> Command ()
forall a b. a -> b -> (a, b)
|> \[String]
args -> TCM () -> TCM (ExitCode ())
forall a b. TCM a -> TCM (ExitCode b)
continueAfter (TCM () -> TCM (ExitCode ())) -> TCM () -> TCM (ExitCode ())
forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
refineMeta [String]
args
            , String
"metas"       String -> ([String] -> TCM (ExitCode ())) -> Command ()
forall a b. a -> b -> (a, b)
|> \[String]
args -> TCM () -> TCM (ExitCode ())
forall a b. TCM a -> TCM (ExitCode b)
continueAfter (TCM () -> TCM (ExitCode ())) -> TCM () -> TCM (ExitCode ())
forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
showMetas [String]
args
            , String
"load"        String -> ([String] -> TCM (ExitCode ())) -> Command ()
forall a b. a -> b -> (a, b)
|> \[String]
args -> TCM () -> TCM (ExitCode ())
forall a b. TCM a -> TCM (ExitCode b)
continueAfter (TCM () -> TCM (ExitCode ())) -> TCM () -> TCM (ExitCode ())
forall a b. (a -> b) -> a -> b
$ TCM () -> [String] -> TCM ()
loadFile TCM ()
reload [String]
args
            , String
"eval"        String -> ([String] -> TCM (ExitCode ())) -> Command ()
forall a b. a -> b -> (a, b)
|> \[String]
args -> TCM () -> TCM (ExitCode ())
forall a b. TCM a -> TCM (ExitCode b)
continueAfter (TCM () -> TCM (ExitCode ())) -> TCM () -> TCM (ExitCode ())
forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
evalIn [String]
args
            , String
"typeOf"      String -> ([String] -> TCM (ExitCode ())) -> Command ()
forall a b. a -> b -> (a, b)
|> \[String]
args -> TCM () -> TCM (ExitCode ())
forall a b. TCM a -> TCM (ExitCode b)
continueAfter (TCM () -> TCM (ExitCode ())) -> TCM () -> TCM (ExitCode ())
forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
typeOf [String]
args
            , String
"typeIn"      String -> ([String] -> TCM (ExitCode ())) -> Command ()
forall a b. a -> b -> (a, b)
|> \[String]
args -> TCM () -> TCM (ExitCode ())
forall a b. TCM a -> TCM (ExitCode b)
continueAfter (TCM () -> TCM (ExitCode ())) -> TCM () -> TCM (ExitCode ())
forall a b. (a -> b) -> a -> b
$ [String] -> TCM ()
typeIn [String]
args
            , String
"wakeup"      String -> ([String] -> TCM (ExitCode ())) -> Command ()
forall a b. a -> b -> (a, b)
|> \[String]
_ -> TCM () -> TCM (ExitCode ())
forall a b. TCM a -> TCM (ExitCode b)
continueAfter (TCM () -> TCM (ExitCode ())) -> TCM () -> TCM (ExitCode ())
forall a b. (a -> b) -> a -> b
$ TCM ()
retryConstraints
            , String
"scope"       String -> ([String] -> TCM (ExitCode ())) -> Command ()
forall a b. a -> b -> (a, b)
|> \[String]
_ -> TCM () -> TCM (ExitCode ())
forall a b. TCM a -> TCM (ExitCode b)
continueAfter (TCM () -> TCM (ExitCode ())) -> TCM () -> TCM (ExitCode ())
forall a b. (a -> b) -> a -> b
$ TCM ()
showScope
            ]
            where
                |> :: a -> b -> (a, b)
(|>) = (,)

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

-- | Set 'envCurrentPath' to 'optInputFile'.
withCurrentFile :: TCM a -> TCM a
withCurrentFile :: TCM a -> TCM a
withCurrentFile TCM a
cont = do
  Maybe AbsolutePath
mpath <- TCM (Maybe AbsolutePath)
getInputFile'
  (TCEnv -> TCEnv) -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envCurrentPath :: Maybe AbsolutePath
envCurrentPath = Maybe AbsolutePath
mpath }) TCM a
cont

loadFile :: TCM () -> [String] -> TCM ()
loadFile :: TCM () -> [String] -> TCM ()
loadFile TCM ()
reload [String
file] = do
  String -> TCM ()
setInputFile String
file
  TCM () -> TCM ()
forall a. TCM a -> TCM a
withCurrentFile TCM ()
reload
loadFile TCM ()
_ [String]
_ = IO () -> TCM ()
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
":load file"

showConstraints :: [String] -> TCM ()
showConstraints :: [String] -> TCM ()
showConstraints [] =
    do  [OutputForm Expr Expr]
cs <- TCM [OutputForm Expr Expr]
BasicOps.getConstraints
        IO () -> TCM ()
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 (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 e (m :: * -> *) a.
(Error e, MonadError e m, Read a) =>
String -> m a
readM String
m
        InteractionId -> TCM () -> TCM ()
forall a. InteractionId -> TCM a -> TCM 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 c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA OutputConstraint Expr InteractionId
s
          IO () -> TCM ()
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. Show a => a -> String
show Doc
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Range -> String
forall a. Show a => a -> String
show 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 e (m :: * -> *) a.
(Error e, MonadError e m, Read a) =>
String -> m a
readM String
m
        InteractionId -> TCM () -> TCM ()
forall a. InteractionId -> TCM a -> TCM 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 c a (m :: * -> *).
(Pretty c, ToConcrete a c, 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 (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. Show a => a -> String
show Doc
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Range -> String
forall a. Show a => a -> String
show 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 (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)
mapM OutputConstraint Expr InteractionId -> TCMT IO Doc
forall a c.
(ToConcrete a c, Pretty c) =>
OutputConstraint a InteractionId -> TCMT IO 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 a c.
(ToConcrete a c, Pretty c) =>
OutputConstraint a NamedMeta -> TCM ()
print' [OutputConstraint Expr NamedMeta]
hiddenMetas
    where
        showII :: OutputConstraint a InteractionId -> TCMT IO Doc
showII OutputConstraint a InteractionId
o = InteractionId -> TCMT IO Doc -> TCMT IO Doc
forall a. InteractionId -> TCM a -> TCM 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]
-> OutputConstraint a InteractionId
-> OutputForm a InteractionId
forall a b.
Range -> [ProblemId] -> OutputConstraint a b -> OutputForm a b
OutputForm Range
forall a. Range' a
noRange [] OutputConstraint a InteractionId
o) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ OutputConstraint a InteractionId -> TCMT IO Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA OutputConstraint a InteractionId
o
        showM :: OutputConstraint a NamedMeta -> TCMT IO Doc
showM  OutputConstraint a NamedMeta
o = MetaId -> TCMT IO Doc -> TCMT IO Doc
forall a. MetaId -> TCM a -> TCM 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]
-> OutputConstraint a NamedMeta
-> OutputForm a NamedMeta
forall a b.
Range -> [ProblemId] -> OutputConstraint a b -> OutputForm a b
OutputForm Range
forall a. Range' a
noRange [] OutputConstraint a NamedMeta
o) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ OutputConstraint a NamedMeta -> TCMT IO Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA OutputConstraint a NamedMeta
o

        metaId :: OutputConstraint a p -> p
metaId (OfType p
i a
_) = p
i
        metaId (JustType p
i) = p
i
        metaId (JustSort p
i) = p
i
        metaId (Assign p
i a
e) = p
i
        metaId OutputConstraint a p
_ = p
forall a. HasCallStack => a
__IMPOSSIBLE__
        print' :: OutputConstraint a NamedMeta -> TCM ()
print' OutputConstraint a NamedMeta
x = do
            Range
r <- MetaId -> TCMT IO Range
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Range
getMetaRange (MetaId -> TCMT IO Range) -> MetaId -> TCMT IO Range
forall a b. (a -> b) -> a -> b
$ NamedMeta -> MetaId
nmid (NamedMeta -> MetaId) -> NamedMeta -> MetaId
forall a b. (a -> b) -> a -> b
$ OutputConstraint a NamedMeta -> NamedMeta
forall a p. OutputConstraint a p -> p
metaId OutputConstraint a NamedMeta
x
            Doc
d <- OutputConstraint a NamedMeta -> TCMT IO Doc
forall a c.
(ToConcrete a c, Pretty c) =>
OutputConstraint a NamedMeta -> TCMT IO Doc
showM OutputConstraint a NamedMeta
x
            IO () -> TCM ()
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. Show a => a -> String
show Doc
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  [ at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Range -> String
forall a. Show a => a -> String
show Range
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ]"
showMetas [String]
_ = IO () -> TCM ()
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 (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ ScopeInfo -> IO ()
forall a. Show a => a -> IO ()
print 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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
        Range
r <- MetaVariable -> Range
forall t. HasRange t => t -> 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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
        --liftIO $ putStrLn $ show scope
        let pos :: Position' SrcFile
pos = case Range -> Maybe (Position' SrcFile)
forall a. Range' a -> Maybe (Position' a)
rStart Range
r of
                    Maybe (Position' SrcFile)
Nothing  -> Position' SrcFile
forall a. HasCallStack => a
__IMPOSSIBLE__
                    Just Position' SrcFile
pos -> Position' SrcFile
pos
        Expr
e <- PM Expr -> TCM Expr
forall a. PM a -> TCM a
runPM (PM Expr -> TCM Expr) -> PM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ Parser Expr -> Position' SrcFile -> String -> PM Expr
forall a. Parser a -> Position' SrcFile -> String -> PM a
parsePosString Parser Expr
exprParser Position' SrcFile
pos String
s
        ScopeInfo -> Expr -> TCM Expr
forall c a. ToAbstract c a => ScopeInfo -> c -> ScopeM a
concreteToAbstract ScopeInfo
scope Expr
e

actOnMeta :: [String] -> (InteractionId -> A.Expr -> TCM a) -> TCM a
actOnMeta :: [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 e (m :: * -> *) a.
(Error e, MonadError e m, Read a) =>
String -> m 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 a. InteractionId -> TCM a -> TCM 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 (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 (m :: * -> *) a. Monad m => a -> m a
return ()
giveMeta [String]
_ = IO () -> TCM ()
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 (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 (m :: * -> *) a. Monad m => a -> m a
return ()
refineMeta [String]
_ = IO () -> TCM ()
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 () -> TCM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCM ()
wakeupConstraints_


evalIn :: [String] -> TCM ()
evalIn :: [String] -> TCM ()
evalIn [String]
s | [String] -> 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 c a (m :: * -> *).
(Pretty c, ToConcrete a c, 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
=<< Expr -> TCM Expr
evalInCurrent Expr
e
        IO () -> TCM ()
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 (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 <- PM Expr -> TCM Expr
forall a. PM a -> TCM a
runPM (PM Expr -> TCM Expr) -> PM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ Parser Expr -> String -> PM Expr
forall a. Parser a -> String -> PM a
parse Parser Expr
exprParser String
s
    Expr -> (Expr -> TCM Expr) -> TCM Expr
forall c a b. ToAbstract c a => c -> (a -> ScopeM b) -> ScopeM b
localToAbstract Expr
e Expr -> TCM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return

evalTerm :: String -> TCM (ExitCode a)
evalTerm :: String -> TCM (ExitCode a)
evalTerm String
s =
    do  Expr
e <- String -> TCM Expr
parseExpr String
s
        Term
v <- Expr -> TCMT IO Term
evalInCurrent Expr
e
        Doc
e <- Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
        IO () -> TCM ()
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. Show a => a -> String
show Doc
e
        ExitCode a -> TCM (ExitCode a)
forall (m :: * -> *) a. Monad m => a -> m a
return ExitCode a
forall a. ExitCode a
Continue
    where
        evalInCurrent :: Expr -> TCMT IO Term
evalInCurrent Expr
e = do
          (Term
v,Type
t) <- Expr -> TCM (Term, Type)
inferExpr Expr
e
          Term
v'    <- Term -> TCMT IO Term
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
v
          Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v'


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 (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 ()) -> TCM String -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCM String
forall c a (m :: * -> *).
(Show c, ToConcrete a c, 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 (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 ()) -> TCM String -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCM String
forall c a (m :: * -> *).
(Show c, ToConcrete a c, MonadAbsToCon m) =>
a -> m String
showA Expr
e1
typeIn [String]
_ = IO () -> TCM ()
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 e (m :: * -> *) a.
(Error e, MonadError e m, Read a) =>
String -> m a
readM String
meta
    MetaVariable
mi <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta (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 a. Closure Range -> TCM a -> TCM 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 ()
forall t a (m :: * -> *).
(Subst t a, MonadReduce m, Normalise a, PrettyTCM a,
 MonadAddContext m, MonadInteractionPoints m, MonadFresh NameId m,
 HasConstInfo m, HasBuiltins m, MonadStConcreteNames m,
 IsString (m Doc), Null (m Doc), Semigroup (m Doc), MonadIO m) =>
(String, a) -> Nat -> m ()
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, a) -> Nat -> m ()
display (String
x, a
t) Nat
n = do
            a
t <- case [String]
args of
                    [String
"normal"] -> a -> m a
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ Nat -> a -> a
forall t a. Subst t a => Nat -> a -> a
raise Nat
n a
t
                    [String]
_          -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ Nat -> a -> a
forall t a. Subst t a => Nat -> a -> a
raise Nat
n a
t
            Doc
d <- a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
t
            IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
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
text (String -> String
argNameToString String
x) Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Doc
d
showContext [String]
_ = IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
":Context meta"

-- | The logo that prints when Agda is started in interactive mode.
splashScreen :: String
splashScreen :: String
splashScreen = [String] -> String
unlines
    [ String
"                 _ "
    , String
"   ____         | |"
    , String
"  / __ \\        | |"
    , String
" | |__| |___  __| | ___"
    , String
" |  __  / _ \\/ _  |/ __\\     Agda Interactive"
    , String
" | |  |/ /_\\ \\/_| / /_| \\"
    , String
" |_|  |\\___  /____\\_____/    Type :? for help."
    , String
"        __/ /"
    , String
"        \\__/"
    , String
""
    -- , "The interactive mode is no longer supported. Don't complain if it doesn't work."
    , String
"The interactive mode is no longer under active development. Use at your own risk."
    ]

-- | The help message
help :: [Command a] -> IO ()
help :: [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