Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.InteractionTop

Synopsis

- putResponse :: Response -> CommandM ()
- commandMToIO :: (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a
- whyInScope :: String -> CommandM ()
- status :: CommandM Status
- initialiseCommandQueue :: IO Command -> IO CommandQueue
- maybeAbort :: (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
- atTopLevel :: CommandM a -> CommandM a
- withCurrentFile :: CommandM a -> CommandM a
- data GiveRefine
  - = Give
  - | Refine
  - | Intro
  - | ElaborateGive Rewrite
- liftCommandMT :: (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
- liftCommandMTLocalState :: (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
- modifyTheInteractionPoints :: ([InteractionId] -> [InteractionId]) -> CommandM ()
- modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
- insertOldInteractionScope :: InteractionId -> ScopeInfo -> CommandM ()
- removeOldInteractionScope :: InteractionId -> CommandM ()
- getOldInteractionScope :: InteractionId -> CommandM ScopeInfo
- handleCommand_ :: CommandM () -> CommandM ()
- handleCommand :: (forall a. CommandM a -> CommandM a) -> CommandM () -> CommandM () -> CommandM ()
- tellEmacsToJumpToError :: Range -> [Response]
- runInteraction :: IOTCM -> CommandM ()
- independent :: Interaction -> Bool
- cmd_load' :: FilePath -> [String] -> Bool -> Mode -> (CheckResult -> CommandM a) -> CommandM a
- interpret :: Interaction -> CommandM ()
- updateInteractionPointsAfter :: Interaction -> Bool
- displayStatus :: CommandM ()
- getBackendName :: CompilerBackend -> BackendName
- display_info :: DisplayInfo -> CommandM ()
- showModuleContents :: Rewrite -> Range -> String -> CommandM ()
- searchAbout :: Rewrite -> Range -> String -> CommandM ()
- solveInstantiatedGoals :: Rewrite -> Maybe InteractionId -> CommandM ()
- parseAndDoAtToplevel :: (Expr -> TCM a) -> String -> CommandM (Maybe CPUTime, a)
- setCommandLineOpts :: CommandLineOptions -> CommandM ()
- tellToUpdateHighlighting :: Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource) -> IO [Response]
- highlightExpr :: Expr -> TCM ()
- give_gen :: UseForce -> InteractionId -> Range -> String -> GiveRefine -> CommandM ()
- maybeTimed :: CommandM a -> CommandM (Maybe CPUTime, a)
- cmd_goal_type_context_and :: GoalTypeAux -> Rewrite -> InteractionId -> Range -> String -> CommandM ()
- extlam_dropName :: UnicodeOrAscii -> CaseContext -> String -> String
- decorate :: Doc -> String
- makeCaseVariant :: CaseContext -> MakeCaseVariant
- sortInteractionPoints :: (MonadInteractionPoints m, MonadError TCErr m, MonadDebug m) => [InteractionId] -> m [InteractionId]

# Documentation

putResponse :: Response -> CommandM () Source #

Put a response by the callback function given by `stInteractionOutputCallback`.

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

Opposite of `liftIO` for `CommandM`.

This function should only be applied to computations that are guaranteed not to raise any errors (except for `IOException`s).

whyInScope :: String -> CommandM () Source #

Explain why something is in scope.

status :: CommandM Status Source #

Computes some status information.

Does not change the state.

initialiseCommandQueue Source #

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.

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

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.

atTopLevel :: CommandM a -> CommandM a Source #

withCurrentFile :: CommandM a -> CommandM a Source #

Set `envCurrentPath` to `theCurrentFile`, if any.

data GiveRefine Source #

Constructors

Give |
Refine |
Intro |
ElaborateGive Rewrite |

#### Instances

Instances details

Show GiveRefine Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods showsPrec :: Int -> GiveRefine -> ShowS Source # show :: GiveRefine -> String Source # showList :: [GiveRefine] -> ShowS Source #
Eq GiveRefine Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods (==) :: GiveRefine -> GiveRefine -> Bool Source # (/=) :: GiveRefine -> GiveRefine -> Bool Source #

liftCommandMT :: (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a Source #

Lift a TCM action transformer to a CommandM action transformer.

liftCommandMTLocalState :: (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a Source #

Ditto, but restore state.

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

A Lens for `theInteractionPoints`.

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

A Lens for `oldInteractionScopes`.

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

removeOldInteractionScope :: InteractionId -> CommandM () Source #

getOldInteractionScope :: InteractionId -> CommandM ScopeInfo Source #

handleCommand_ :: CommandM () -> CommandM () Source #

Do setup and error handling for a command.

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

tellEmacsToJumpToError :: Range -> [Response] Source #

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

runInteraction :: IOTCM -> CommandM () Source #

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

independent :: Interaction -> Bool Source #

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

cmd_load' Source #

Arguments

:: FilePath | File to load into interaction.
-> [String] | Arguments to Agda for loading this file
-> Bool | Allow unsolved meta-variables?
-> Mode | Full type-checking, or only scope-checking?
-> (CheckResult -> CommandM a) | Continuation after successful loading.
-> CommandM a |

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

interpret :: Interaction -> CommandM () Source #

updateInteractionPointsAfter :: Interaction -> Bool Source #

Should `Resp_InteractionPoints` be issued after the command has run?

displayStatus :: CommandM () Source #

Displays or updates status information.

Does not change the state.

getBackendName :: CompilerBackend -> BackendName Source #

Interpret an interaction

display_info :: DisplayInfo -> CommandM () Source #

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

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

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

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

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

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

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

parseAndDoAtToplevel Source #

Arguments

:: (Expr -> TCM a) | The command to perform.
-> String | The expression to parse.
-> CommandM (Maybe CPUTime, a) |

Parses and scope checks an expression (using the "inside scope" as the scope), performs the given command with the expression as input, and returns the result and the time it takes.

setCommandLineOpts :: CommandLineOptions -> CommandM () Source #

Sets the command line options and updates the status information.

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

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

highlightExpr :: Expr -> TCM () Source #

give_gen Source #

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

maybeTimed :: CommandM a -> CommandM (Maybe CPUTime, a) Source #

cmd_goal_type_context_and :: GoalTypeAux -> Rewrite -> InteractionId -> Range -> String -> CommandM () Source #

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

Should not modify the state.

extlam_dropName :: UnicodeOrAscii -> CaseContext -> String -> String Source #

decorate :: Doc -> String Source #

makeCaseVariant :: CaseContext -> MakeCaseVariant Source #

sortInteractionPoints :: (MonadInteractionPoints m, MonadError TCErr m, MonadDebug m) => [InteractionId] -> m [InteractionId] Source #

Sorts interaction points based on their ranges.