Agda.Interaction.GhciTop

Documentation

data State

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

theState :: IORef State

data Independence

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

data Interaction

An interactive computation.

Is the command independent?

Constructors

Interaction

Fields

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

isIndependent :: Interaction -> Bool

ioTCM_ :: TCM a -> IO a

Run a TCM computation in the current state. Should only be used for debugging.

ioTCM

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

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

cmd_load'

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.

data Backend

Available backends.

Constructors

MAlonzo

Epic

JS

cmd_compile :: Backend -> FilePath -> [FilePath] -> Interaction

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

cmd_constraints :: Interaction

cmd_metas :: Interaction

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

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

cmd_give :: GoalCommand

cmd_refine :: GoalCommand

give_gen :: ToConcrete a2 a1 => (InteractionId -> Maybe a -> Expr -> TCMT IO (a2, [InteractionId])) -> (Range -> String -> a1 -> String) -> InteractionId -> Range -> String -> Interaction

give_gen' :: ToConcrete a2 a1 => (InteractionId -> Maybe a -> Expr -> TCMT IO (a2, [InteractionId])) -> (Range -> String -> a1 -> String) -> InteractionId -> Range -> String -> TCMT IO (Maybe a3)

cmd_intro :: GoalCommand

cmd_refine_or_intro :: GoalCommand

cmd_auto :: GoalCommand

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

Sorts interaction points based on their ranges.

prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc

Pretty-prints the type of the meta-variable.

prettyContext

Arguments

:: Rewrite

Normalise?

-> Bool

Print the elements in reverse order?

-> InteractionId

-> TCM Doc

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

cmd_context :: Rewrite -> GoalCommand

cmd_infer :: Rewrite -> GoalCommand

cmd_goal_type :: Rewrite -> GoalCommand

cmd_goal_type_context_and :: Doc -> Rewrite -> InteractionId -> t -> t1 -> TCMT IO (Maybe a)

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

cmd_goal_type_context :: Rewrite -> GoalCommand

Displays the current goal and context.

cmd_goal_type_context_infer :: Rewrite -> GoalCommand

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

showModuleContents :: Range -> String -> TCM ()

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

cmd_show_module_contents :: GoalCommand

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

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

setCommandLineOptions :: CommandLineOptions -> TCM ()

Sets the command line options and updates the status information.

data Status

Status information.

Constructors

Status

Fields

sShowImplicitArguments :: Bool

Are implicit arguments displayed?

sChecked :: Bool

Has the module been successfully type checked?

status :: TCM Status

Computes some status information.

showStatus :: Status -> String

Shows status information.

displayStatus :: Status -> IO ()

Displays/updates status information.

display_info' :: String -> String -> IO ()

display_info' header content displays content (with header header) in some suitable way.

display_info :: String -> String -> TCM ()

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

display_infoD :: String -> Doc -> TCM ()

Like display_info, but takes a Doc instead of a String.

showNumIId :: InteractionId -> Lisp [Char]

takenNameStr :: TCM [String]

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

nameModifiers :: [[Char]]

cmd_make_case :: GoalCommand

cmd_solveAll :: Interaction

class LowerMeta a where

Methods

lowerMeta :: a -> a

Instances

LowerMeta ModuleApplication

LowerMeta Declaration

LowerMeta WhereClause

LowerMeta RHS

LowerMeta TypedBinding

LowerMeta TypedBindings

LowerMeta LamBinding

LowerMeta Expr

LowerMeta a => LowerMeta [a]

LowerMeta (Maybe Expr)

LowerMeta a => LowerMeta (Arg a)

LowerMeta (OpApp Expr)

LowerMeta a => LowerMeta (Named name a)

preMeta :: Expr

preUscore :: Expr

cmd_compute

Arguments

:: Bool

Ignore abstract?

-> GoalCommand

parseAndDoAtToplevel

Arguments

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

cmd_infer_toplevel

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

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

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

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

showImplicitArgs

Arguments

:: Bool

Show them?

-> Interaction

Tells Agda whether or not to show implicit arguments.

toggleImplicitArgs :: Interaction

Toggle display of implicit arguments.

errorTitle :: String

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

displayErrorAndExit

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.

infoOnException :: IO a -> IO a

Outermost error handler.

ensureFileLoaded :: AbsolutePath -> TCM ()

Raises an error if the given file is not the one currently loaded.

getCurrentFile :: IO FilePath

makeSilent :: Interaction -> Interaction

Changes the Interaction so that its first action is to turn off all debug messages.

top_command' :: FilePath -> Interaction -> IO ()

goal_command :: InteractionId -> GoalCommand -> String -> IO ()

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

Constructs AbsolutePaths.

Precondition: The path must be absolute and valid.