Agda.Interaction.InteractionTop

Documentation

showOpenMetas :: TCM [String]

Print open metas nicely.

data GiveRefine

Constructors

Give

Refine

Intro

ElaborateGive

Instances

Eq GiveRefine

Defined in Agda.Interaction.InteractionTop

Methods

(==) :: GiveRefine -> GiveRefine -> Bool

(/=) :: GiveRefine -> GiveRefine -> Bool

Show GiveRefine

Defined in Agda.Interaction.InteractionTop

Methods

showsPrec :: Int -> GiveRefine -> ShowS

show :: GiveRefine -> String

showList :: [GiveRefine] -> ShowS

data CompilerBackend

Available backends.

Constructors

LaTeX

QuickLaTeX

OtherBackend String

Instances

Eq CompilerBackend

Defined in Agda.Interaction.InteractionTop

Methods

(==) :: CompilerBackend -> CompilerBackend -> Bool

(/=) :: CompilerBackend -> CompilerBackend -> Bool

Read CompilerBackend

Defined in Agda.Interaction.InteractionTop

Methods

readsPrec :: Int -> ReadS CompilerBackend

readList :: ReadS [CompilerBackend]

readPrec :: ReadPrec CompilerBackend

readListPrec :: ReadPrec [CompilerBackend]

Show CompilerBackend

Defined in Agda.Interaction.InteractionTop

Methods

showsPrec :: Int -> CompilerBackend -> ShowS

show :: CompilerBackend -> String

showList :: [CompilerBackend] -> ShowS

type Parse a = ExceptT String (StateT String Identity) a

The Parse monad. StateT state holds the remaining input.

data Remove

Used to indicate whether something should be removed or not.

Constructors

Remove

Keep

Instances

Read Remove

Defined in Agda.Interaction.InteractionTop

Methods

readsPrec :: Int -> ReadS Remove

readList :: ReadS [Remove]

readPrec :: ReadPrec Remove

readListPrec :: ReadPrec [Remove]

Show Remove

Defined in Agda.Interaction.InteractionTop

Methods

showsPrec :: Int -> Remove -> ShowS

show :: Remove -> String

showList :: [Remove] -> ShowS

data IOTCM' range

Constructors

IOTCM FilePath HighlightingLevel HighlightingMethod (Interaction' range)

Instances

Functor IOTCM'

Defined in Agda.Interaction.InteractionTop

Methods

fmap :: (a -> b) -> IOTCM' a -> IOTCM' b

(<$) :: a -> IOTCM' b -> IOTCM' a

Foldable IOTCM'

Defined in Agda.Interaction.InteractionTop

Methods

fold :: Monoid m => IOTCM' m -> m

foldMap :: Monoid m => (a -> m) -> IOTCM' a -> m

foldr :: (a -> b -> b) -> b -> IOTCM' a -> b

foldr' :: (a -> b -> b) -> b -> IOTCM' a -> b

foldl :: (b -> a -> b) -> b -> IOTCM' a -> b

foldl' :: (b -> a -> b) -> b -> IOTCM' a -> b

foldr1 :: (a -> a -> a) -> IOTCM' a -> a

foldl1 :: (a -> a -> a) -> IOTCM' a -> a

toList :: IOTCM' a -> [a]

null :: IOTCM' a -> Bool

length :: IOTCM' a -> Int

elem :: Eq a => a -> IOTCM' a -> Bool

maximum :: Ord a => IOTCM' a -> a

minimum :: Ord a => IOTCM' a -> a

sum :: Num a => IOTCM' a -> a

product :: Num a => IOTCM' a -> a

Traversable IOTCM'

Defined in Agda.Interaction.InteractionTop

Methods

traverse :: Applicative f => (a -> f b) -> IOTCM' a -> f (IOTCM' b)

sequenceA :: Applicative f => IOTCM' (f a) -> f (IOTCM' a)

mapM :: Monad m => (a -> m b) -> IOTCM' a -> m (IOTCM' b)

sequence :: Monad m => IOTCM' (m a) -> m (IOTCM' a)

Read range => Read (IOTCM' range)

Defined in Agda.Interaction.InteractionTop

Methods

readsPrec :: Int -> ReadS (IOTCM' range)

readList :: ReadS [IOTCM' range]

readPrec :: ReadPrec (IOTCM' range)

readListPrec :: ReadPrec [IOTCM' range]

Show range => Show (IOTCM' range)

Defined in Agda.Interaction.InteractionTop

Methods

showsPrec :: Int -> IOTCM' range -> ShowS

show :: IOTCM' range -> String

showList :: [IOTCM' range] -> ShowS

type IOTCM = IOTCM' Range

data Interaction' range

Constructors

Cmd_load FilePath [String]

cmd_load m argv loads the module in file m, using argv as the command-line options.

Cmd_compile CompilerBackend FilePath [String]

cmd_compile b m argv compiles the module in file m using the backend b, using argv as the command-line options.

Cmd_constraints

Cmd_metas

Show unsolved metas. If there are no unsolved metas but unsolved constraints show those instead.

Cmd_show_module_contents_toplevel Rewrite String

Shows all the top-level names in the given module, along with their types. Uses the top-level scope.

Cmd_search_about_toplevel Rewrite String

Shows all the top-level names in scope which mention all the given identifiers in their type.

Cmd_solveAll Rewrite

Solve (all goals / the goal at point) whose values are determined by the constraints.

Cmd_solveOne Rewrite InteractionId range String

Cmd_autoOne InteractionId range String

Solve (all goals / the goal at point) by using Auto.

Cmd_autoAll

Cmd_infer_toplevel Rewrite String

Parse the given expression (as if it were defined at the top-level of the current module) and infer its type.

Cmd_compute_toplevel ComputeMode String

Parse and type check the given expression (as if it were defined at the top-level of the current module) and normalise it.

Cmd_load_highlighting_info FilePath

cmd_load_highlighting_info source loads syntax highlighting information for the module in source, and asks Emacs to apply highlighting info from this file.

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 no highlighting information is printed.

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.

Cmd_tokenHighlighting FilePath Remove

Tells Agda to compute token-based highlighting information for the file.

This command works even if the file's module name does not match its location in the file system, or if the file is not scope-correct. Furthermore no file names are put in the generated output. Thus it is fine to put source code into a temporary file before calling this command. However, the file extension should be correct.

If the second argument is Remove, then the (presumably temporary) file is removed after it has been read.

Cmd_highlight InteractionId range String

Tells Agda to compute highlighting information for the expression just spliced into an interaction point.

ShowImplicitArgs Bool

Tells Agda whether or not to show implicit arguments.

ToggleImplicitArgs

Toggle display of implicit arguments.

Cmd_give UseForce InteractionId range String

Goal commands

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

Cmd_refine InteractionId range String

Cmd_intro Bool InteractionId range String

Cmd_refine_or_intro Bool InteractionId range String

Cmd_context Rewrite InteractionId range String

Cmd_helper_function Rewrite InteractionId range String

Cmd_infer Rewrite InteractionId range String

Cmd_goal_type Rewrite InteractionId range String

Cmd_elaborate_give Rewrite InteractionId range String

Grabs the current goal's type and checks the expression in the hole against it. Returns the elaborated term.

Cmd_goal_type_context Rewrite InteractionId range String

Displays the current goal and context.

Cmd_goal_type_context_infer Rewrite InteractionId range String

Displays the current goal and context and infers the type of an expression.

Cmd_goal_type_context_check Rewrite InteractionId range String

Grabs the current goal's type and checks the expression in the hole against it.

Cmd_show_module_contents Rewrite InteractionId range String

Shows all the top-level names in the given module, along with their types. Uses the scope of the given goal.

Cmd_make_case InteractionId range String

Cmd_compute ComputeMode InteractionId range String

Cmd_why_in_scope InteractionId range String

Cmd_why_in_scope_toplevel String

Cmd_show_version

Displays version of the running Agda

Cmd_abort

Abort the current computation.

Does nothing if no computation is in progress.

Instances

Functor Interaction'

Defined in Agda.Interaction.InteractionTop

Methods

fmap :: (a -> b) -> Interaction' a -> Interaction' b

(<$) :: a -> Interaction' b -> Interaction' a

Foldable Interaction'

Defined in Agda.Interaction.InteractionTop

Methods

fold :: Monoid m => Interaction' m -> m

foldMap :: Monoid m => (a -> m) -> Interaction' a -> m

foldr :: (a -> b -> b) -> b -> Interaction' a -> b

foldr' :: (a -> b -> b) -> b -> Interaction' a -> b

foldl :: (b -> a -> b) -> b -> Interaction' a -> b

foldl' :: (b -> a -> b) -> b -> Interaction' a -> b

foldr1 :: (a -> a -> a) -> Interaction' a -> a

foldl1 :: (a -> a -> a) -> Interaction' a -> a

toList :: Interaction' a -> [a]

null :: Interaction' a -> Bool

length :: Interaction' a -> Int

elem :: Eq a => a -> Interaction' a -> Bool

maximum :: Ord a => Interaction' a -> a

minimum :: Ord a => Interaction' a -> a

sum :: Num a => Interaction' a -> a

product :: Num a => Interaction' a -> a

Traversable Interaction'

Defined in Agda.Interaction.InteractionTop

Methods

traverse :: Applicative f => (a -> f b) -> Interaction' a -> f (Interaction' b)

sequenceA :: Applicative f => Interaction' (f a) -> f (Interaction' a)

mapM :: Monad m => (a -> m b) -> Interaction' a -> m (Interaction' b)

sequence :: Monad m => Interaction' (m a) -> m (Interaction' a)

Read range => Read (Interaction' range)

Defined in Agda.Interaction.InteractionTop

Methods

readsPrec :: Int -> ReadS (Interaction' range)

readList :: ReadS [Interaction' range]

readPrec :: ReadPrec (Interaction' range)

readListPrec :: ReadPrec [Interaction' range]

Show range => Show (Interaction' range)

Defined in Agda.Interaction.InteractionTop

Methods

showsPrec :: Int -> Interaction' range -> ShowS

show :: Interaction' range -> String

showList :: [Interaction' range] -> ShowS

type Interaction = Interaction' Range

An interactive computation.

data CommandQueue

Command queues.

Constructors

CommandQueue

Fields

• commands :: !(TChan (Integer, Command))

  Commands that should be processed, in the order in which they should be processed. Each command is associated with a number, and the numbers are strictly increasing. Abort commands are not put on this queue.

• abort :: !(TVar (Maybe Integer))

  When this variable is set to Just n an attempt is made to abort all commands with a command number that is at most n.

type Command = Command' IOTCM

IOTCM commands.

data Command' a

A generalised command type.

Constructors

Command !a

A command.

Done

Stop processing commands.

Error String

An error message for a command that could not be parsed.

Instances

Show a => Show (Command' a)

Defined in Agda.Interaction.InteractionTop

Methods

showsPrec :: Int -> Command' a -> ShowS

show :: Command' a -> String

showList :: [Command' a] -> ShowS

type CommandM = StateT CommandState TCM

Monad for computing answers to interactive commands.

CommandM is TCMT extended with state CommandState.

type OldInteractionScopes = Map InteractionId ScopeInfo

data CommandState

Auxiliary state of an interactive computation.

Constructors

CommandState

Fields

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

• optionsOnReload :: CommandLineOptions

  Reset the options on each reload to these.

• oldInteractionScopes :: !OldInteractionScopes

  We remember (the scope of) old interaction points to make it possible to parse and compute highlighting information for the expression that it got replaced by.

• commandQueue :: !CommandQueue

  The command queue.

  This queue should only be manipulated by initialiseCommandQueue and maybeAbort.

initCommandState :: CommandQueue -> CommandState

Initial auxiliary interaction state

localStateCommandM :: CommandM a -> CommandM a

Restore both TCState and CommandState.

liftLocalState :: TCM a -> CommandM a

Restore TCState, do not touch CommandState.

revLift

Arguments

:: MonadState st m

=> (forall c. m c -> st -> k (c, st))

run

-> (forall b. k b -> m b)

lift

-> (forall x. (m a -> k x) -> k x)

-> m a

reverse lift in double negative position

Build an opposite action to lift for state monads.

revLiftTC

Arguments

:: MonadTCState m

=> (forall c. m c -> TCState -> k (c, TCState))

run

-> (forall b. k b -> m b)

lift

-> (forall x. (m a -> k x) -> k x)

-> m a

reverse lift in double negative position

commandMToIO :: (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a

Opposite of liftIO for CommandM. Use only if main errors are already catched.

liftCommandMT :: (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a

Lift a TCM action transformer to a CommandM action transformer.

liftCommandMTLocalState :: (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a

Ditto, but restore state.

putResponse :: Response -> CommandM ()

Put a response by the callback function given by stInteractionOutputCallback.

modifyTheInteractionPoints :: ([InteractionId] -> [InteractionId]) -> CommandM ()

A Lens for theInteractionPoints.

modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()

A Lens for oldInteractionScopes.

insertOldInteractionScope :: InteractionId -> ScopeInfo -> CommandM ()

removeOldInteractionScope :: InteractionId -> CommandM ()

getOldInteractionScope :: InteractionId -> CommandM ScopeInfo

handleCommand_ :: CommandM () -> CommandM ()

Do setup and error handling for a command.

handleCommand :: (forall a. CommandM a -> CommandM a) -> CommandM () -> CommandM () -> CommandM ()

runInteraction :: IOTCM -> CommandM ()

Run an IOTCM value, catch the exceptions, emit output

If an error happens the state of CommandM does not change, but stPersistent may change (which contains successfully loaded interfaces for example).

maybeAbort :: (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))

If the next command from the command queue is anything but an actual command, then the command is returned.

If the command is an IOTCM command, then the following happens: The given computation is applied to the command and executed. If an abort command is encountered (and acted upon), then the computation is interrupted, the persistent state and all options are restored, and some commands are sent to the frontend. If the computation was not interrupted, then its result is returned.

initialiseCommandQueue

Arguments

:: IO Command

Returns the next command.

-> IO CommandQueue

Creates a command queue, and forks a thread that writes commands to the queue. The queue is returned.

readsToParse :: String -> (String -> Maybe (a, String)) -> Parse a

Converter from the type of reads to Parse The first paramter is part of the error message in case the parse fails.

parseToReadsPrec :: Parse a -> Int -> String -> [(a, String)]

exact :: String -> Parse ()

Demand an exact string.

readParse :: Read a => Parse a

parens' :: Parse a -> Parse a

independent :: Interaction -> Bool

Can the command run even if the relevant file has not been loaded into the state?

updateInteractionPointsAfter :: Interaction -> Bool

Should Resp_InteractionPoints be issued after the command has run?

interpret :: Interaction -> CommandM ()

Interpret an interaction

interpretWarnings :: CommandM (String, String)

Show warnings

solveInstantiatedGoals :: Rewrite -> Maybe InteractionId -> CommandM ()

Solved goals already instantiated internally The second argument potentially limits it to one specific goal.

cmd_load'

Arguments

:: FilePath

-> [String]

-> Bool

Allow unsolved meta-variables?

-> Mode

Full type-checking, or only scope-checking?

-> ((Interface, MaybeWarnings) -> CommandM ())

-> CommandM ()

cmd_load' file argv unsolvedOk cmd loads the module in file file, using argv as the command-line options.

If type checking completes without any exceptions having been encountered then the command cmd r is executed, where r is the result of typeCheckMain.

withCurrentFile :: CommandM a -> CommandM a

Set envCurrentPath to theCurrentFile, if any.

give_gen

Arguments

:: UseForce

Should safety checks be skipped?

-> InteractionId

-> Range

-> String

-> GiveRefine

-> CommandM ()

A "give"-like action (give, refine, etc).

give_gen force ii rng s give_ref mk_newtxt acts on interaction point ii occupying range rng, placing the new content given by string s, and replacing ii by the newly created interaction points in the state if safety checks pass (unless force is applied).

highlightExpr :: Expr -> TCM ()

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_helper_function :: Rewrite -> InteractionId -> Range -> String -> TCM Doc

Create type of application of new helper function that would solve the goal.

cmd_goal_type_context_and :: Doc -> Rewrite -> InteractionId -> Range -> String -> StateT CommandState (TCMT IO) ()

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

Should not modify the state.

showModuleContents :: Rewrite -> Range -> String -> CommandM ()

Shows all the top-level names in the given module, along with their types.

searchAbout :: Rewrite -> Range -> String -> CommandM ()

Shows all the top-level names in scope which mention all the given identifiers in their type.

whyInScope :: String -> CommandM ()

Explain why something is in scope.

setCommandLineOpts :: CommandLineOptions -> CommandM ()

Sets the command line options and updates the status information.

status :: CommandM Status

Computes some status information.

Does not change the state.

displayStatus :: CommandM ()

Displays or updates status information.

Does not change the state.

display_info :: DisplayInfo -> CommandM ()

display_info does what display_info' False does, but additionally displays some status information (see status and displayStatus).

refreshStr :: [String] -> String -> ([String], String)

nameModifiers :: [String]

parseAndDoAtToplevel

Arguments

:: (Expr -> TCM Doc)

The command to perform.

-> (Doc -> DisplayInfo)

The name to use for the buffer displaying the output.

-> String

The expression to parse.

-> CommandM ()

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.

maybeTimed :: CommandM a -> CommandM (Maybe Doc, a)

tellToUpdateHighlighting :: Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource) -> IO [Response]

Tell to highlight the code using the given highlighting info (unless it is Nothing).

tellEmacsToJumpToError :: Range -> [Response]

Tells the Emacs mode to go to the first error position (if any).

Orphan instances

Read AbsolutePath

Methods

readsPrec :: Int -> ReadS AbsolutePath

readList :: ReadS [AbsolutePath]

readPrec :: ReadPrec AbsolutePath

readListPrec :: ReadPrec [AbsolutePath]

Read InteractionId

Methods

readsPrec :: Int -> ReadS InteractionId

readList :: ReadS [InteractionId]

readPrec :: ReadPrec InteractionId

readListPrec :: ReadPrec [InteractionId]

Read a => Read (Range' a)

Note that the grammar implemented by this instance does not necessarily match the current representation of ranges.

Methods

readsPrec :: Int -> ReadS (Range' a)

readList :: ReadS [Range' a]

readPrec :: ReadPrec (Range' a)

readListPrec :: ReadPrec [Range' a]

Read a => Read (Interval' a)

Methods

readsPrec :: Int -> ReadS (Interval' a)

readList :: ReadS [Interval' a]

readPrec :: ReadPrec (Interval' a)

readListPrec :: ReadPrec [Interval' a]

Read a => Read (Position' a)

Methods

readsPrec :: Int -> ReadS (Position' a)

readList :: ReadS [Position' a]

readPrec :: ReadPrec (Position' a)

readListPrec :: ReadPrec [Position' a]