| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Interaction.GhciTop

Synopsis

data State = State {

theTCState :: TCState
theInteractionPoints :: [InteractionId]
theCurrentFile :: Maybe (AbsolutePath, ClockTime)

}

initState :: State
theState :: IORef State

data Interaction = Interaction {

isIndependent :: Bool
command :: TCM (Maybe ModuleName)

}

ioTCM_ :: TCM a -> IO a
ioTCM :: FilePath -> Maybe FilePath -> Interaction -> IO ()
cmd_load :: FilePath -> [FilePath] -> Interaction
cmd_load' :: FilePath -> [FilePath] -> Bool -> ((Interface, Maybe Warnings) -> TCM ()) -> Interaction
cmd_compile :: FilePath -> [FilePath] -> Interaction
cmd_constraints :: Interaction
cmd_metas :: Interaction
cmd_reset :: Interaction
type GoalCommand = InteractionId -> Range -> String -> Interaction
cmd_give :: GoalCommand
cmd_refine :: GoalCommand
cmd_intro :: GoalCommand
cmd_refine_or_intro :: GoalCommand
cmd_auto :: GoalCommand
sortInteractionPoints :: [InteractionId] -> TCM [InteractionId]
prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc
prettyContext :: Rewrite -> InteractionId -> TCM Doc
cmd_context :: Rewrite -> GoalCommand
cmd_infer :: Rewrite -> GoalCommand
cmd_goal_type :: Rewrite -> GoalCommand
cmd_goal_type_context :: Rewrite -> GoalCommand
cmd_goal_type_context_infer :: Rewrite -> GoalCommand
setCommandLineOptions :: CommandLineOptions -> TCM ()

data Status = Status {

sShowImplicitArguments :: Bool
sChecked :: Bool

}

status :: TCM Status
showStatus :: Status -> String
displayStatus :: Status -> IO ()
display_info' :: String -> String -> IO ()
display_info :: String -> String -> TCM ()
display_infoD :: String -> Doc -> TCM ()
response :: Lisp String -> String
responseString :: Lisp String -> String
respond :: Lisp String -> IO ()

data Lisp a

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

takenNameStr :: TCM [String]
refreshStr :: [String] -> String -> ([String], String)
cmd_make_case :: GoalCommand
cmd_solveAll :: Interaction
class LowerMeta a where

lowerMeta :: a -> a

cmd_compute :: Bool -> GoalCommand
parseAndDoAtToplevel :: (Expr -> TCM Expr) -> String -> String -> Interaction
cmd_infer_toplevel :: Rewrite -> String -> Interaction
cmd_compute_toplevel :: Bool -> String -> Interaction
cmd_write_highlighting_info :: FilePath -> FilePath -> Interaction
cmd_goals :: FilePath -> Interaction
tellEmacsToJumpToError :: Range -> IO ()
showImplicitArgs :: Bool -> Interaction
toggleImplicitArgs :: Interaction
errorTitle :: String
displayErrorAndExit :: Status -> Range -> String -> IO a
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

Documentation

data State | Source

Constructors

State |

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 |

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

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

ioTCM | Source

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

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

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

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

Methods

lowerMeta :: a -> a | Source

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

:: Bool | Ignore abstract?
-> GoalCommand |

parseAndDoAtToplevel | Source

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

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

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

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

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

:: |
=> 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 `AbsolutePath`s. Precondition: The path must be absolute.
Produced by Haddock version 2.4.2