Agda-2.2.6: 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 Interaction Source

An interactive computation.




isIndependent :: Bool

Can the command run even if the relevant file has not been loaded into the state?

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.

cmd_compile :: FilePath -> [FilePath] -> InteractionSource

cmd_compile m includes compiles the module in file m, using includes as the include directories.

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


-> InteractionId 
-> TCM Doc 

Pretty-prints the context of the given meta-variable.

cmd_context :: Rewrite -> GoalCommandSource

prettyContext lays out n : e on (at least) two lines if n has at least longNameLength characters.

cmd_goal_type_context :: Rewrite -> GoalCommandSource

Displays the current goal and context plus the given document.

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.

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.

responseString :: Lisp String -> StringSource

Formats a response string.

respond :: Lisp String -> IO ()Source

Responds to a query.

data Lisp a Source


A a 
L [Lisp a] 
Q (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 used 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.



:: FilePath

If the module name in this file does not match that of the current module (or the module name cannot be determined), then an empty list of goals is returned.

-> Interaction 

Returns the interaction ids for all goals in the current module, in the order in which they appear in the module. If there is no current module, then an empty list of goals is returned.

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.

mkAbsolute :: FilePath -> AbsolutePathSource

Constructs AbsolutePaths.

Precondition: The path must be absolute.