Agda-2.2.10: 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 Independence
= Independent (Maybe [FilePath])
| Dependent
data Interaction = Interaction {
independence :: Independence
command :: TCM (Maybe ModuleName)
}
isIndependent :: Interaction -> Bool
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
data Backend
= MAlonzo
| Epic
cmd_compile :: Backend -> FilePath -> [FilePath] -> Interaction
cmd_constraints :: Interaction
cmd_metas :: 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 -> Bool -> 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
showModuleContents :: Range -> String -> TCM ()
cmd_show_module_contents :: GoalCommand
cmd_show_module_contents_toplevel :: String -> Interaction
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
data Lisp a
= A a
| L [Lisp a]
| Q (Lisp a)
| Cons (Lisp a) (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
tellEmacsToJumpToError :: Range -> IO ()
showImplicitArgs :: Bool -> Interaction
toggleImplicitArgs :: Interaction
errorTitle :: String
displayErrorAndExit :: Status -> Range -> String -> IO a
ensureFileLoaded :: AbsolutePath -> TCM ()
getCurrentFile :: IO FilePath
makeSilent :: Interaction -> Interaction
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
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 Independence Source
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 Source

An interactive computation.

Is the command independent?

Constructors
Interaction
independence :: IndependenceIs 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 -> BoolSource
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.

data Backend Source
Available backends.
Constructors
MAlonzo
Epic
cmd_compile :: Backend -> FilePath -> [FilePath] -> InteractionSource
cmd_compile b m includes compiles the module in file m using the backend b, using includes as the include directories.
cmd_constraints :: InteractionSource
cmd_metas :: InteractionSource
type GoalCommand = InteractionId -> Range -> String -> InteractionSource
If the range is noRange, then the string comes from the minibuffer rather than the goal.
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?
-> BoolPrint the elements in reverse order?
-> InteractionId
-> TCM Doc
Pretty-prints the context of the given meta-variable.
cmd_context :: Rewrite -> GoalCommandSource
cmd_infer :: Rewrite -> GoalCommandSource
cmd_goal_type :: Rewrite -> GoalCommandSource
cmd_goal_type_context :: Rewrite -> GoalCommandSource

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

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.
showModuleContents :: Range -> String -> TCM ()Source
Shows all the top-level names in the given module, along with their types.
cmd_show_module_contents :: GoalCommandSource
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 -> InteractionSource
Shows all the top-level names in the given module, along with their types. Uses the top-level scope.
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.
data Lisp a Source
Constructors
A a
L [Lisp a]
Q (Lisp a)
Cons (Lisp a) (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 use 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.

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 ()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
:: StatusThe 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.
ensureFileLoaded :: AbsolutePath -> TCM ()Source

Outermost error handler.

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

getCurrentFile :: IO FilePathSource
makeSilent :: Interaction -> InteractionSource
Changes the Interaction so that its first action is to turn off all debug messages.
top_command' :: FilePath -> Interaction -> IO ()Source
goal_command :: InteractionId -> GoalCommand -> String -> IO ()Source
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 and valid.

Produced by Haddock version 2.6.1