- data State = State {}
- initState :: State
- theState :: IORef State
- data Independence
- = Independent (Maybe [FilePath])
- | Dependent
- data Interaction = Interaction {}
- isIndependent :: Interaction -> Bool
- ioTCM_ :: TCM a -> IO a
- ioTCM :: FilePath -> Maybe FilePath -> Interaction -> IO ()
- cmd_load :: FilePath -> [FilePath] -> Interaction
- cmd_load' :: FilePath -> [FilePath] -> Bool -> ((Interface, Maybe Warnings) -> TCM ()) -> Interaction
- data Backend
- cmd_compile :: Backend -> FilePath -> [FilePath] -> Interaction
- cmd_constraints :: Interaction
- cmd_metas :: Interaction
- type GoalCommand = InteractionId -> Range -> String -> Interaction
- cmd_give :: GoalCommand
- cmd_refine :: GoalCommand
- cmd_intro :: GoalCommand
- cmd_refine_or_intro :: GoalCommand
- cmd_auto :: GoalCommand
- sortInteractionPoints :: [InteractionId] -> TCM [InteractionId]
- prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc
- prettyContext :: Rewrite -> Bool -> InteractionId -> TCM Doc
- cmd_context :: Rewrite -> GoalCommand
- cmd_infer :: Rewrite -> GoalCommand
- cmd_goal_type :: Rewrite -> GoalCommand
- cmd_goal_type_context :: Rewrite -> GoalCommand
- cmd_goal_type_context_infer :: Rewrite -> GoalCommand
- showModuleContents :: Range -> String -> TCM ()
- cmd_show_module_contents :: GoalCommand
- cmd_show_module_contents_toplevel :: String -> Interaction
- setCommandLineOptions :: CommandLineOptions -> TCM ()
- data Status = Status {}
- status :: TCM Status
- showStatus :: Status -> String
- displayStatus :: Status -> IO ()
- display_info' :: String -> String -> IO ()
- display_info :: String -> String -> TCM ()
- display_infoD :: String -> Doc -> TCM ()
- takenNameStr :: TCM [String]
- refreshStr :: [String] -> String -> ([String], String)
- cmd_make_case :: GoalCommand
- cmd_solveAll :: Interaction
- class LowerMeta a where
- lowerMeta :: a -> a
- cmd_compute :: Bool -> GoalCommand
- parseAndDoAtToplevel :: (Expr -> TCM Expr) -> String -> String -> Interaction
- cmd_infer_toplevel :: Rewrite -> String -> Interaction
- cmd_compute_toplevel :: Bool -> String -> Interaction
- cmd_write_highlighting_info :: FilePath -> FilePath -> Interaction
- tellEmacsToJumpToError :: Range -> IO ()
- showImplicitArgs :: Bool -> Interaction
- toggleImplicitArgs :: Interaction
- errorTitle :: String
- displayErrorAndExit :: Status -> Range -> String -> IO a
- ensureFileLoaded :: AbsolutePath -> TCM ()
- getCurrentFile :: IO FilePath
- makeSilent :: Interaction -> Interaction
- top_command' :: FilePath -> Interaction -> IO ()
- goal_command :: InteractionId -> GoalCommand -> String -> IO ()
- module Agda.TypeChecker
- module Agda.TypeChecking.MetaVars
- module Agda.TypeChecking.Reduce
- module Agda.TypeChecking.Errors
- module Agda.Syntax.Position
- module Agda.Syntax.Parser
- module Agda.Syntax.Scope.Base
- module Agda.Syntax.Scope.Monad
- module Agda.Syntax.Translation.ConcreteToAbstract
- module Agda.Syntax.Translation.AbstractToConcrete
- module Agda.Syntax.Translation.InternalToAbstract
- module Agda.Syntax.Abstract.Name
- module Agda.Interaction.Exceptions
- mkAbsolute :: FilePath -> AbsolutePath
Documentation
State | |
|
data Independence Source
Can the command run even if the relevant file has not been loaded into the state?
Independent (Maybe [FilePath]) | Yes. If the argument is |
Dependent |
data Interaction Source
An interactive computation.
Is the command independent?
Interaction | |
|
Run a TCM computation in the current state. Should only be used for debugging.
:: FilePath | The current file. If this file does not match
|
-> Maybe FilePath | Syntax highlighting information will be written to this file, if any. |
-> Interaction | |
-> IO () |
Runs a TCM
computation. All calls from the Emacs mode should be
wrapped in this function.
cmd_load :: FilePath -> [FilePath] -> InteractionSource
cmd_load m includes
loads the module in file m
, using
includes
as the include directories.
:: FilePath | |
-> [FilePath] | |
-> Bool | Allow unsolved meta-variables? |
-> ((Interface, Maybe Warnings) -> TCM ()) | |
-> Interaction |
cmd_load' m includes cmd cmd2
loads the module in file m
,
using includes
as the include directories.
If type checking completes without any exceptions having been
encountered then the command cmd r
is executed, where r
is the
result of typeCheck
.
cmd_compile :: Backend -> FilePath -> [FilePath] -> InteractionSource
cmd_compile b m includes
compiles the module in file m
using
the backend b
, using includes
as the include directories.
type GoalCommand = InteractionId -> Range -> String -> InteractionSource
If the range is noRange
, then the string comes from the
minibuffer rather than the goal.
sortInteractionPoints :: [InteractionId] -> TCM [InteractionId]Source
Sorts interaction points based on their ranges.
prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM DocSource
Pretty-prints the type of the meta-variable.
:: Rewrite | Normalise? |
-> Bool | Print the elements in reverse order? |
-> InteractionId | |
-> TCM Doc |
Pretty-prints the context of the given meta-variable.
cmd_goal_type_context :: Rewrite -> GoalCommandSource
Displays the current goal, the given document, and the current context.
Displays the current goal and context.
cmd_goal_type_context_infer :: Rewrite -> GoalCommandSource
Displays the current goal and context and infers the type of an expression.
showModuleContents :: Range -> String -> TCM ()Source
Shows all the top-level names in the given module, along with their types.
cmd_show_module_contents :: GoalCommandSource
Shows all the top-level names in the given module, along with their types. Uses the scope of the given goal.
cmd_show_module_contents_toplevel :: String -> InteractionSource
Shows all the top-level names in the given module, along with their types. Uses the top-level scope.
setCommandLineOptions :: CommandLineOptions -> TCM ()Source
Sets the command line options and updates the status information.
Status information.
Status | |
|
showStatus :: Status -> StringSource
Shows status information.
displayStatus :: Status -> IO ()Source
Displays/updates status information.
display_info' :: String -> String -> IO ()Source
display_info' header content
displays content
(with header
header
) in some suitable way.
display_info :: String -> String -> TCM ()Source
display_info
does what display_info'
does, but additionally
displays some status information (see status
and
displayStatus
).
display_infoD :: String -> Doc -> TCM ()Source
Like display_info
, but takes a Doc
instead of a String
.
takenNameStr :: TCM [String]Source
LowerMeta ModuleApplication | |
LowerMeta Declaration | |
LowerMeta WhereClause | |
LowerMeta RHS | |
LowerMeta TypedBinding | |
LowerMeta TypedBindings | |
LowerMeta LamBinding | |
LowerMeta Expr | |
LowerMeta a => LowerMeta [a] | |
LowerMeta (Maybe Expr) | |
LowerMeta a => LowerMeta (Arg a) | |
LowerMeta (OpApp Expr) | |
LowerMeta a => LowerMeta (Named name a) |
:: Bool | Ignore abstract? |
-> GoalCommand |
:: (Expr -> TCM Expr) | The command to perform. |
-> String | The name to use for the buffer displaying the output. |
-> String | The expression to parse. |
-> Interaction |
Parses and scope checks an expression (using the "inside scope" as the scope), performs the given command with the expression as input, and displays the result.
:: Rewrite | Normalise the type? |
-> String | |
-> Interaction |
Parse the given expression (as if it were defined at the top-level of the current module) and infer its type.
:: Bool | Ignore abstract? |
-> String | |
-> Interaction |
Parse and type check the given expression (as if it were defined at the top-level of the current module) and normalise it.
cmd_write_highlighting_info :: FilePath -> FilePath -> InteractionSource
cmd_write_highlighting_info source target
writes syntax
highlighting information for the module in source
into target
.
If the module does not exist, or its module name is malformed or
cannot be determined, or the module has not already been visited,
or the cached info is out of date, then the representation of "no
highlighting information available" is instead written to
target
.
This command is used to load syntax highlighting information when a new file is opened, and it would probably be annoying if jumping to the definition of an identifier reset the proof state, so this command tries not to do that. One result of this is that the command uses the current include directories, whatever they happen to be.
tellEmacsToJumpToError :: Range -> IO ()Source
Tells the Emacs mode to go to the first error position (if any).
:: Bool | Show them? |
-> Interaction |
Tells Agda whether or not to show implicit arguments.
toggleImplicitArgs :: InteractionSource
Toggle display of implicit arguments.
When an error message is displayed the following title should be used, if appropriate.
Displays an error, instructs Emacs to jump to the site of the error, and terminates the program. Because this function may switch the focus to another file the status information is also updated.
ensureFileLoaded :: AbsolutePath -> TCM ()Source
Outermost error handler.
Raises an error if the given file is not the one currently loaded.
makeSilent :: Interaction -> InteractionSource
Changes the Interaction
so that its first action is to turn off
all debug messages.
top_command' :: FilePath -> Interaction -> IO ()Source
goal_command :: InteractionId -> GoalCommand -> String -> IO ()Source
module Agda.TypeChecker
module Agda.TypeChecking.MetaVars
module Agda.TypeChecking.Reduce
module Agda.TypeChecking.Errors
module Agda.Syntax.Position
module Agda.Syntax.Parser
module Agda.Syntax.Scope.Base
module Agda.Syntax.Scope.Monad
module Agda.Syntax.Abstract.Name
module Agda.Interaction.Exceptions
mkAbsolute :: FilePath -> AbsolutePathSource
Constructs AbsolutePath
s.
Precondition: The path must be absolute and valid.