Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Interaction.InteractionTop

Synopsis

data GiveRefine
- = Give
- | Refine
- | Intro
- | ElaborateGive Rewrite
localStateCommandM :: CommandM a -> CommandM a
liftLocalState :: TCM a -> CommandM a
revLift :: MonadState st m => (forall c. m c -> st -> k (c, st)) -> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
revLiftTC :: MonadTCState m => (forall c. m c -> TCState -> k (c, TCState)) -> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
commandMToIO :: (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a
liftCommandMT :: (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMTLocalState :: (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
putResponse :: Response -> CommandM ()
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 ()
runInteraction :: IOTCM -> CommandM ()
maybeAbort :: (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
initialiseCommandQueue :: IO Command -> IO CommandQueue
independent :: Interaction -> Bool
updateInteractionPointsAfter :: Interaction -> Bool
interpret :: Interaction -> CommandM ()
solveInstantiatedGoals :: Rewrite -> Maybe InteractionId -> CommandM ()
cmd_load' :: FilePath -> [String] -> Bool -> Mode -> (CheckResult -> CommandM a) -> CommandM a
withCurrentFile :: CommandM a -> CommandM a
atTopLevel :: CommandM a -> CommandM a
give_gen :: UseForce -> InteractionId -> Range -> String -> GiveRefine -> CommandM ()
highlightExpr :: Expr -> TCM ()
sortInteractionPoints :: (MonadInteractionPoints m, MonadError TCErr m, MonadFail m) => [InteractionId] -> m [InteractionId]
cmd_goal_type_context_and :: GoalTypeAux -> Rewrite -> InteractionId -> Range -> String -> CommandM ()
showModuleContents :: Rewrite -> Range -> String -> CommandM ()
searchAbout :: Rewrite -> Range -> String -> CommandM ()
whyInScope :: String -> CommandM ()
setCommandLineOpts :: CommandLineOptions -> CommandM ()
status :: CommandM Status
displayStatus :: CommandM ()
display_info :: DisplayInfo -> CommandM ()
parseAndDoAtToplevel :: (Expr -> TCM a) -> String -> CommandM (Maybe CPUTime, a)
maybeTimed :: CommandM a -> CommandM (Maybe CPUTime, a)
tellToUpdateHighlighting :: Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource) -> IO [Response]
tellEmacsToJumpToError :: Range -> [Response]

Documentation

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 # show :: GiveRefine -> String # showList :: [GiveRefine] -> ShowS #
Eq GiveRefine Source #
Instance details Defined in Agda.Interaction.InteractionTop Methods (==) :: GiveRefine -> GiveRefine -> Bool # (/=) :: GiveRefine -> GiveRefine -> Bool #

localStateCommandM :: CommandM a -> CommandM a Source #

Restore both TCState and CommandState.

liftLocalState :: TCM a -> CommandM a Source #

Restore TCState, do not touch CommandState.

revLift Source #

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 Source #

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 Source #

Opposite of liftIO for CommandM.

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

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.

putResponse :: Response -> CommandM () Source #

Put a response by the callback function given by stInteractionOutputCallback.

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 #

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

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.

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.

independent :: Interaction -> Bool Source #

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

updateInteractionPointsAfter :: Interaction -> Bool Source #

Should Resp_InteractionPoints be issued after the command has run?

interpret :: Interaction -> CommandM () Source #

Interpret an interaction

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

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

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.

withCurrentFile :: CommandM a -> CommandM a Source #

Set envCurrentPath to theCurrentFile, if any.

atTopLevel :: CommandM a -> CommandM a 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).

highlightExpr :: Expr -> TCM () Source #

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

Sorts interaction points based on their ranges.

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.

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.

whyInScope :: String -> CommandM () Source #

Explain why something is in scope.

setCommandLineOpts :: CommandLineOptions -> CommandM () Source #

Sets the command line options and updates the status information.

status :: CommandM Status Source #

Computes some status information.

Does not change the state.

displayStatus :: CommandM () Source #

Displays or updates status information.

Does not change the state.

display_info :: DisplayInfo -> CommandM () Source #

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

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.

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

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

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

tellEmacsToJumpToError :: Range -> [Response] Source #

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