|
|
|
|
Synopsis |
|
|
|
Documentation |
|
|
Constructors | State | | theTCState :: TCState | | theInteractionPoints :: [InteractionId] | The interaction points of the buffer, in the order in which
they appear in the buffer. The interaction points are
recorded in theTCState, but when new interaction points are
added by give or refine Agda does not ensure that the ranges
of later interaction points are updated.
| theCurrentFile :: Maybe (AbsolutePath, ClockTime) | The file which the state applies to. Only stored if the
module was successfully type checked (potentially with
warnings). The ClockTime is the modification time stamp of
the file when it was last loaded.
|
|
|
|
|
|
|
|
|
|
Can the command run even if the relevant file has not been loaded
into the state?
| Constructors | Independent (Maybe [FilePath]) | Yes. If the argument is Just is, then is is used as the
command's include directories.
| Dependent | |
|
|
|
|
An interactive computation.
Is the command independent?
| Constructors | Interaction | | independence :: Independence | Is the command independent?
| command :: TCM (Maybe ModuleName) | If a module name is returned, then syntax highlighting
information will be written for the given module (by ioTCM).
|
|
|
|
|
|
|
|
Run a TCM computation in the current state. Should only
be used for debugging.
|
|
|
:: FilePath | The current file. If this file does not match
theCurrentFile, and the Interaction is not
"independent", then an error is raised.
| -> 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 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.
|
|
|
|
Available backends.
| Constructors | |
|
|
|
cmd_compile b m includes compiles the module in file m using
the backend b, using includes as the include directories.
|
|
|
|
|
|
|
If the range is noRange, then the string comes from the
minibuffer rather than the goal.
|
|
|
|
|
|
|
|
|
|
|
|
|
Sorts interaction points based on their ranges.
|
|
|
Pretty-prints the type of the meta-variable.
|
|
|
|
|
|
|
|
|
|
|
|
Displays the current goal, the given document, and the current
context.
Displays the current goal and context.
|
|
|
Displays the current goal and context and infers the type of an
expression.
|
|
|
Shows all the top-level names in the given module, along with
their types.
|
|
|
Shows all the top-level names in the given module, along with
their types. Uses the scope of the given goal.
|
|
|
Shows all the top-level names in the given module, along with
their types. Uses the top-level scope.
|
|
|
Sets the command line options and updates the status information.
|
|
|
Status information.
| Constructors | Status | | sShowImplicitArguments :: Bool | Are implicit arguments displayed?
| sChecked :: Bool | Has the module been successfully type checked?
|
|
|
|
|
|
Computes some status information.
|
|
|
Shows status information.
|
|
|
Displays/updates status information.
|
|
|
display_info' header content displays content (with header
header) in some suitable way.
|
|
|
display_info does what display_info' does, but additionally
displays some status information (see status and
displayStatus).
|
|
|
Like display_info, but takes a Doc instead of a String.
|
|
|
Formats a response command.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:: 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 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.
|
|
|
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.
|
|
|
|
Toggle display of implicit arguments.
|
|
|
When an error message is displayed the following title should be
used, if appropriate.
|
|
|
:: Status | The new status information.
| -> Range | | -> String | | -> IO a | | 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.
|
|
|
|
Outermost error handler.
Raises an error if the given file is not the one currently
loaded.
|
|
|
|
|
Changes the Interaction so that its first action is to turn off
all debug messages.
|
|
|
|
|
|
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 |
|
|
Constructs AbsolutePaths.
Precondition: The path must be absolute and valid.
|
|
Produced by Haddock version 2.6.1 |