Agda.Interaction.GhciTop

Synopsis

Documentation

data State Source

Constructors

State

Fields

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.

initState :: State Source

theState :: IORef State Source

data Interaction Source

An interactive computation.

Constructors

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

ioTCM Source

Arguments

:: 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] -> Interaction Source

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

cmd_load'Source

Arguments

:: 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] -> Interaction Source

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

cmd_constraints :: Interaction Source

cmd_metas :: Interaction Source

cmd_reset :: Interaction Source

type GoalCommand = InteractionId -> Range -> String -> Interaction Source

cmd_give :: GoalCommand Source

cmd_refine :: GoalCommand Source

cmd_intro :: GoalCommand Source

cmd_refine_or_intro :: GoalCommand Source

cmd_auto :: GoalCommand Source

sortInteractionPoints :: [InteractionId] -> TCM [InteractionId]Source

Sorts interaction points based on their ranges.

prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc Source

Pretty-prints the type of the meta-variable.

prettyContext Source

Arguments

:: Rewrite	Normalise?
-> InteractionId
-> TCM Doc

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

cmd_context :: Rewrite -> GoalCommand Source

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

cmd_infer :: Rewrite -> GoalCommand Source

cmd_goal_type :: Rewrite -> GoalCommand Source

cmd_goal_type_context :: Rewrite -> GoalCommand Source

Displays the current goal and context plus the given document.

Displays the current goal and context.

cmd_goal_type_context_infer :: Rewrite -> GoalCommand Source

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.

Constructors

Status
Fields sShowImplicitArguments :: Bool Are implicit arguments displayed? sChecked :: Bool Has the module been successfully type checked?

status :: TCM Status Source

Computes some status information.

showStatus :: Status -> String Source

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 -> String Source

Formats a response command.

responseString :: Lisp String -> String Source

Formats a response string.

respond :: Lisp String -> IO ()Source

Responds to a query.

data Lisp a Source

Constructors

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

Instances

Pretty a => Show (Lisp a)
Pretty a => Pretty (Lisp a)

takenNameStr :: TCM [String]Source

refreshStr :: [String] -> String -> ([String], String)Source

cmd_make_case :: GoalCommand Source

cmd_solveAll :: Interaction Source

class LowerMeta a whereSource

Methods

lowerMeta :: a -> aSource

Instances

LowerMeta Declaration
LowerMeta WhereClause
LowerMeta RHS
LowerMeta TypedBinding
LowerMeta TypedBindings
LowerMeta LamBinding
LowerMeta Expr
LowerMeta a => LowerMeta [a]
LowerMeta a => LowerMeta (Arg a)
LowerMeta a => LowerMeta (Named name a)

cmd_compute Source

Arguments

:: Bool	Ignore abstract?
-> GoalCommand

parseAndDoAtToplevel Source

Arguments

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

cmd_infer_toplevel Source

Arguments

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

cmd_compute_toplevel Source

Arguments

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

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.

cmd_goals Source

Arguments

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

showImplicitArgs Source

Arguments

:: Bool	Show them?
-> Interaction

Tells Agda whether or not to show implicit arguments.

toggleImplicitArgs :: Interaction Source

Toggle display of implicit arguments.

errorTitle :: String Source

When an error message is displayed the following title should be used, if appropriate.

displayErrorAndExit Source

Arguments

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

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 Source

Constructs AbsolutePaths.

Precondition: The path must be absolute.