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




data State Source




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.

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 Just is, then is is used as the command's include directories.


data Interaction Source

An interactive computation.

Is the command independent?




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).

ioTCM_ :: TCM a -> IO aSource

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 :: 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.

data Backend Source

Available backends.



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


-> 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.

data Status Source

Status information.




sShowImplicitArguments :: Bool

Are implicit arguments displayed?

sChecked :: Bool

Has the module been successfully type checked?

status :: TCM StatusSource

Computes some status information.

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.

response :: Lisp String -> StringSource

Formats a response command.

data Lisp a Source


A a 
L [Lisp a] 
Q (Lisp a) 
Cons (Lisp a) (Lisp a) 


Pretty a => Show (Lisp a) 
Pretty a => Pretty (Lisp 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.

errorTitle :: StringSource

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.

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.

mkAbsolute :: FilePath -> AbsolutePathSource

Constructs AbsolutePaths.

Precondition: The path must be absolute and valid.