Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.CommandLine

Synopsis

- 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))
- interaction :: String -> [Command a] -> (String -> TCM (ExitCode a)) -> IM a
- interactionLoop :: TCM (Maybe Interface) -> IM ()
- continueAfter :: TCM a -> TCM (ExitCode b)
- withCurrentFile :: TCM a -> TCM a
- loadFile :: TCM () -> [String] -> TCM ()
- showConstraints :: [String] -> TCM ()
- showMetas :: [String] -> TCM ()
- showScope :: TCM ()
- metaParseExpr :: InteractionId -> String -> TCM Expr
- actOnMeta :: [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
- giveMeta :: [String] -> TCM ()
- refineMeta :: [String] -> TCM ()
- retryConstraints :: TCM ()
- evalIn :: [String] -> TCM ()
- parseExpr :: String -> TCM Expr
- evalTerm :: String -> TCM (ExitCode a)
- typeOf :: [String] -> TCM ()
- typeIn :: [String] -> TCM ()
- showContext :: [String] -> TCM ()
- splashScreen :: String
- help :: [Command a] -> IO ()

# Documentation

data ExitCode a Source #

Constructors

Continue |
ContinueIn TCEnv |
Return a |

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

matchCommand :: String -> [Command a] -> Either [String] ([String] -> TCM (ExitCode a)) Source #

interaction :: String -> [Command a] -> (String -> TCM (ExitCode a)) -> IM a Source #

interactionLoop :: TCM (Maybe Interface) -> IM () Source #

The interaction loop.

continueAfter :: TCM a -> TCM (ExitCode b) Source #

withCurrentFile :: TCM a -> TCM a Source #

Set `envCurrentPath` to `optInputFile`.

loadFile :: TCM () -> [String] -> TCM () Source #

showConstraints :: [String] -> TCM () Source #

showMetas :: [String] -> TCM () Source #

showScope :: TCM () Source #

metaParseExpr :: InteractionId -> String -> TCM Expr Source #

actOnMeta :: [String] -> (InteractionId -> Expr -> TCM a) -> TCM a Source #

giveMeta :: [String] -> TCM () Source #

refineMeta :: [String] -> TCM () Source #

retryConstraints :: TCM () Source #

evalIn :: [String] -> TCM () Source #

parseExpr :: String -> TCM Expr Source #

evalTerm :: String -> TCM (ExitCode a) Source #

typeOf :: [String] -> TCM () Source #

typeIn :: [String] -> TCM () Source #

showContext :: [String] -> TCM () Source #

splashScreen :: String Source #

The logo that prints when Agda is started in interactive mode.

help :: [Command a] -> IO () Source #

The help message