Agda-2.2.4: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Interaction.GhciTop
Synopsis
data State = State {
theTCState :: TCState
theUndoStack :: [TCState]
theTopLevel :: Maybe TopLevelInfo
theInteractionPoints :: [InteractionId]
}
initState :: State
theState :: IORef State
ioTCM :: TCM a -> IO a
cmd_load :: FilePath -> [FilePath] -> IO ()
cmd_load' :: FilePath -> [FilePath] -> Bool -> (CreateInterfaceResult -> TCM ()) -> IO () -> IO ()
cmd_compile :: FilePath -> [FilePath] -> IO ()
cmd_constraints :: IO ()
cmd_metas :: IO ()
cmd_undo :: IO ()
cmd_reset :: IO ()
type GoalCommand = InteractionId -> Range -> String -> IO ()
cmd_give :: GoalCommand
cmd_refine :: 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_and :: Doc -> Rewrite -> GoalCommand
cmd_goal_type_context :: Rewrite -> GoalCommand
cmd_goal_type_context_infer :: Rewrite -> GoalCommand
setCommandLineOptions :: CommandLineOptions -> TCM ()
displayStatus :: TCM ()
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)
takenNameStr :: TCM [String]
refreshStr :: [String] -> String -> ([String], String)
cmd_make_case :: GoalCommand
cmd_solveAll :: IO ()
class LowerMeta a where
lowerMeta :: a -> a
cmd_compute :: Bool -> GoalCommand
parseAndDoAtToplevel :: (Expr -> TCM Expr) -> String -> String -> IO ()
cmd_infer_toplevel :: Rewrite -> String -> IO ()
cmd_compute_toplevel :: Bool -> String -> IO ()
tellEmacsToUpdateGoals :: IO ()
tellEmacsToReloadSyntaxInfo :: IO ()
tellEmacsToJumpToError :: Range -> IO ()
showImplicitArgs :: Bool -> IO ()
toggleImplicitArgs :: IO ()
errorTitle :: String
displayErrorAndExit :: Either TCErr (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
Documentation
data State Source
Constructors
State
theTCState :: TCState
theUndoStack :: [TCState]
theTopLevel :: Maybe TopLevelInfoInvariant: The TopLevelInfo corresponds to a type-correct module.
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.
initState :: StateSource
theState :: IORef StateSource
ioTCM :: TCM a -> IO aSource
cmd_load :: FilePath -> [FilePath] -> IO ()Source
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?
-> CreateInterfaceResult -> TCM ()
-> IO ()
-> IO ()

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 second component of the result of createInterface.

The command cmd2 is executed as the final step of cmd_load', unless an exception is encountered.

cmd_compile :: FilePath -> [FilePath] -> IO ()Source
cmd_compile m includes compiles the module in file m, using includes as the include directories.
cmd_constraints :: IO ()Source
cmd_metas :: IO ()Source
cmd_undo :: IO ()Source
cmd_reset :: IO ()Source
type GoalCommand = InteractionId -> Range -> String -> IO ()Source
cmd_give :: GoalCommandSource
cmd_refine :: 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_and :: Doc -> Rewrite -> GoalCommandSource
Displays the current goal and context plus the given document.
cmd_goal_type_context :: Rewrite -> GoalCommandSource
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.
displayStatus :: TCM ()Source
Displays/updates some status information (currently just indicates whether or not implicit arguments are shown).
display_info :: String -> String -> TCM ()Source
display_info header content displays content (with header header) in some suitable way, and also displays some status information (see displayStatus).
display_infoD :: String -> Doc -> TCM ()Source
Like display_info, but takes a Doc instead of a String.
response :: Lisp String -> StringSource
data Lisp a Source
Constructors
A a
L [Lisp a]
Q (Lisp a)
show/hide Instances
Pretty a => Show (Lisp a)
Pretty a => Pretty (Lisp a)
takenNameStr :: TCM [String]Source
refreshStr :: [String] -> String -> ([String], String)Source
cmd_make_case :: GoalCommandSource
cmd_solveAll :: IO ()Source
class LowerMeta a whereSource
Methods
lowerMeta :: a -> aSource
show/hide Instances
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.
-> IO ()
Parses and scope checks an expression (using insideScope topLevel as the scope), performs the given command with the expression as input, and displays the result.
cmd_infer_toplevelSource
:: RewriteNormalise the type?
-> String
-> IO ()
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
-> IO ()
Parse and type check the given expression (as if it were defined at the top-level of the current module) and normalise it.
tellEmacsToUpdateGoals :: IO ()Source
Tell the Emacs mode to rescan the buffer for goals.
tellEmacsToReloadSyntaxInfo :: IO ()Source
Tell the Emacs mode to reload the highlighting information. This includes rescanning the buffer for goals.
tellEmacsToJumpToError :: Range -> IO ()Source
Tells the Emacs mode to reload the highlighting information and go to the first error position (if any).
showImplicitArgsSource
:: BoolShow them?
-> IO ()
Tells Agda whether or not to show implicit arguments.
toggleImplicitArgs :: IO ()Source
Toggle display of implicit arguments.
errorTitle :: StringSource
When an error message is displayed the following title should be used, if appropriate.
displayErrorAndExit :: Either TCErr (Range, String) -> IO aSource
Displays an error (represented either as a TCErr or as a Range and a message) and terminates the program.
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
Produced by Haddock version 2.4.2