Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 :: StateSource
theState :: IORef StateSource
data Interaction Source
An interactive computation.
Constructors
Interaction
isIndependent :: BoolCan 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.
ioTCMSource
:: FilePathThe current file. If this file does not match theCurrentFile, and the Interaction is not "independent", then an error is raised.
-> Maybe FilePathSyntax 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] -> InteractionSource
cmd_load m includes loads the module in file m, using includes as the include directories.
cmd_load'Source
:: FilePath
-> [FilePath]
-> BoolAllow 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] -> InteractionSource
cmd_compile m includes compiles the module in file m, using includes as the include directories.
cmd_constraints :: InteractionSource
cmd_metas :: InteractionSource
cmd_reset :: InteractionSource
type GoalCommand = InteractionId -> Range -> String -> InteractionSource
cmd_give :: GoalCommandSource
cmd_refine :: GoalCommandSource
cmd_intro :: GoalCommandSource
cmd_refine_or_intro :: GoalCommandSource
cmd_auto :: GoalCommandSource
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.
prettyContextSource
:: RewriteNormalise?
-> InteractionId
-> TCM Doc
Pretty-prints the context of the given meta-variable.
cmd_context :: Rewrite -> GoalCommandSource
prettyContext lays out n : e on (at least) two lines if n has at least longNameLength characters.
cmd_infer :: Rewrite -> GoalCommandSource
cmd_goal_type :: Rewrite -> GoalCommandSource
cmd_goal_type_context :: Rewrite -> GoalCommandSource

Displays the current goal and context plus the given document.

Displays the current goal and context.

cmd_goal_type_context_infer :: Rewrite -> GoalCommandSource
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 :: BoolAre implicit arguments displayed?
sChecked :: BoolHas the module been successfully type checked?
status :: TCM StatusSource
Computes some status information.
showStatus :: Status -> StringSource
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 -> StringSource
Formats a response command.
responseString :: Lisp String -> StringSource
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)
takenNameStr :: TCM [String]Source
refreshStr :: [String] -> String -> ([String], String)Source
cmd_make_case :: GoalCommandSource
cmd_solveAll :: InteractionSource
class LowerMeta a whereSource
Methods
lowerMeta :: a -> aSource
cmd_computeSource
:: BoolIgnore abstract?
-> GoalCommand
parseAndDoAtToplevelSource
:: Expr -> TCM ExprThe command to perform.
-> StringThe name to used for the buffer displaying the output.
-> StringThe 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_toplevelSource
:: RewriteNormalise 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_toplevelSource
:: BoolIgnore 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 -> InteractionSource
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_goalsSource
:: FilePathIf 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).
showImplicitArgsSource
:: BoolShow them?
-> Interaction
Tells Agda whether or not to show implicit arguments.
toggleImplicitArgs :: InteractionSource
Toggle display of implicit arguments.
errorTitle :: StringSource
When an error message is displayed the following title should be used, if appropriate.
displayErrorAndExitSource
::
=> Status
-> 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 -> AbsolutePathSource

Constructs AbsolutePaths.

Precondition: The path must be absolute.

Produced by Haddock version 2.6.0