Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




data CommandState Source

Auxiliary state of an interactive computation.




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.

optionsOnReload :: CommandLineOptions

Reset the options on each reload to these.


MonadState CommandState CommandM 

initCommandState :: CommandStateSource

Initial auxiliary interaction state

newtype CommandM a Source

Monad for computing answers to interactive commands.

CommandM is TCM extended with state CommandState.

StateT is in a newtype wrapper because we would like to prevent the accidental use of lift. Instead of lift one can use liftCommandM, see below.




unCommandM :: StateT CommandState TCM a


runCommandM :: CommandM a -> CommandState -> TCM (a, CommandState)Source

Wrapped runStateT for CommandM.

liftCommandM :: TCM a -> CommandM aSource

lift a TCM action to CommandM.

liftCommandM is a customized form of lift for StateT. At the end of the lifted action stInteractionOutputCallback is set to its original value because the value is lost during the execution of some TCM actions.



:: MonadState st m 
=> (forall c. m c -> st -> k (c, st))


-> (forall b. k b -> m b)


-> (forall x. (m a -> k x) -> k x) 
-> m a

reverse lift in double negative position

Build an opposite action to lift for state monads.

commandMToIO :: (forall x. (CommandM a -> IO x) -> IO x) -> CommandM aSource

Opposite of liftIO for CommandM. Use only if main errors are already catched.

runSafeTCM :: TCM a -> TCState -> IO (a, TCState)Source

runSafeTCM runs a safe TMC action (a TCM action which cannot fail)

liftCommandMT :: (forall a. TCM a -> TCM a) -> CommandM a -> CommandM aSource

Lift a TCM action transformer to a CommandM action transformer.

putResponse :: Response -> CommandM ()Source

Put a response by the callback function given by stInteractionOutputCallback.

runInteraction :: IOTCM -> CommandM ()Source

Run an IOTCM value, catch the exceptions, emit output

If an error happens the state of CommandM does not change, but stPersistent may change (which contains successfully loaded interfaces for example).

data Interaction Source

An interactive computation.


Cmd_load FilePath [FilePath]

cmd_load m includes loads the module in file m, using includes as the include directories.

Cmd_compile Backend FilePath [FilePath]

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


Show unsolved metas. If there are no unsolved metas but unsolved constraints show those instead.

Cmd_show_module_contents_toplevel String

Shows all the top-level names in the given module, along with their types. Uses the top-level scope.

Cmd_infer_toplevel Rewrite String

Parse the given expression (as if it were defined at the top-level of the current module) and infer its type.

Cmd_compute_toplevel Bool String

Parse and type check the given expression (as if it were defined at the top-level of the current module) and normalise it.

Cmd_load_highlighting_info FilePath

cmd_load_highlighting_info source loads syntax highlighting information for the module in source, and asks Emacs to apply highlighting info from this file.

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 no highlighting information is printed.

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.

ShowImplicitArgs Bool

Tells Agda whether or not to show implicit arguments.


Toggle display of implicit arguments.

Cmd_give InteractionId Range String

Goal commands

If the range is noRange, then the string comes from the minibuffer rather than the goal.

Cmd_refine InteractionId Range String 
Cmd_intro Bool InteractionId Range String 
Cmd_refine_or_intro Bool InteractionId Range String 
Cmd_auto InteractionId Range String 
Cmd_context Rewrite InteractionId Range String 
Cmd_infer Rewrite InteractionId Range String 
Cmd_goal_type Rewrite InteractionId Range String 
Cmd_goal_type_context Rewrite InteractionId Range String

Displays the current goal and context.

Cmd_goal_type_context_infer Rewrite InteractionId Range String

Displays the current goal and context and infers the type of an expression.

Cmd_show_module_contents InteractionId Range String

Shows all the top-level names in the given module, along with their types. Uses the scope of the given goal.

Cmd_make_case InteractionId Range String 
Cmd_compute Bool InteractionId Range String 


type Parse a = ErrorT String (StateT String Identity) aSource

The Parse monad. StateT state holds the remaining input.

readsToParse :: String -> (String -> Maybe (a, String)) -> Parse aSource

Converter from the type of reads to Parse The first paramter is part of the error message in case the parse fails.

exact :: String -> Parse ()Source

Demand an exact string.

independent :: Interaction -> BoolSource

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

interpret :: Interaction -> CommandM ()Source

Interpret an interaction



:: FilePath 
-> [FilePath] 
-> Bool

Allow unsolved meta-variables?

-> ((Interface, Maybe Warnings) -> CommandM ()) 
-> CommandM () 

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.




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_and :: Doc -> Rewrite -> InteractionId -> t -> t1 -> CommandM ()Source

Displays the current goal, the given document, and the current context.

showModuleContents :: Range -> String -> CommandM ()Source

Shows all the top-level names in the given module, along with their types.

setCommandLineOptions' :: CommandLineOptions -> CommandM ()Source

Sets the command line options and updates the status information.

status :: CommandM StatusSource

Computes some status information.

displayStatus :: CommandM ()Source

Displays/updates status information.

display_info :: DisplayInfo -> CommandM ()Source

display_info does what display_info' False does, but additionally displays some status information (see status and displayStatus).



:: (Expr -> TCM Expr)

The command to perform.

-> (Doc -> DisplayInfo)

The name to use for the buffer displaying the output.

-> String

The expression to parse.

-> CommandM () 

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.

tellToUpdateHighlighting :: Maybe (HighlightingInfo, ModuleToSource) -> IO [Response]Source

Tell to highlight the code using the given highlighting info (unless it is Nothing).

tellEmacsToJumpToError :: Range -> [Response]Source

Tells the Emacs mode to go to the first error position (if any).