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

Safe HaskellSafe-Infered

Agda.Interaction.GhciTop

Synopsis

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.

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

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.

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

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

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)

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

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.

makeSilent :: Interaction -> Interaction

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

mkAbsolute :: FilePath -> AbsolutePath

Constructs AbsolutePaths.

Precondition: The path must be absolute and valid.