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

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.InteractionTop

Contents

- Orphan instances

Synopsis

- showOpenMetas :: TCM [String]
- data GiveRefine
  - = Give
  - | Refine
  - | Intro
  - | ElaborateGive
- data CompilerBackend
  - = LaTeX
  - | QuickLaTeX
  - | OtherBackend String
- type Parse a = ExceptT String (StateT String Identity) a
- data Remove
  - = Remove
  - | Keep
- data IOTCM' range = IOTCM FilePath HighlightingLevel HighlightingMethod (Interaction' range)
- type IOTCM = IOTCM' Range
- data Interaction' range
  - = Cmd_load FilePath [String]
  - | Cmd_compile CompilerBackend FilePath [String]
  - | Cmd_constraints
  - | Cmd_metas
  - | Cmd_show_module_contents_toplevel Rewrite String
  - | Cmd_search_about_toplevel Rewrite String
  - | Cmd_solveAll Rewrite
  - | Cmd_solveOne Rewrite InteractionId range String
  - | Cmd_autoOne InteractionId range String
  - | Cmd_autoAll
  - | Cmd_infer_toplevel Rewrite String
  - | Cmd_compute_toplevel ComputeMode String
  - | Cmd_load_highlighting_info FilePath
  - | Cmd_tokenHighlighting FilePath Remove
  - | Cmd_highlight InteractionId range String
  - | ShowImplicitArgs Bool
  - | ToggleImplicitArgs
  - | Cmd_give UseForce InteractionId range String
  - | 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
  - | Cmd_goal_type_context Rewrite InteractionId range String
  - | Cmd_goal_type_context_infer Rewrite InteractionId range String
  - | Cmd_goal_type_context_check Rewrite InteractionId range String
  - | Cmd_show_module_contents Rewrite InteractionId range String
  - | 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
  - | Cmd_abort
- type Interaction = Interaction' Range
- data CommandQueue = CommandQueue {
  - commands :: !(TChan (Integer, Command))
  - abort :: !(TVar (Maybe Integer))
  }
- type Command = Command' IOTCM
- data Command' a
  - = Command !a
  - | Done
  - | Error String
- type CommandM = StateT CommandState TCM
- type OldInteractionScopes = Map InteractionId ScopeInfo
- data CommandState = CommandState {
  - theInteractionPoints :: [InteractionId]
  - theCurrentFile :: Maybe (AbsolutePath, ClockTime)
  - optionsOnReload :: CommandLineOptions
  - oldInteractionScopes :: !OldInteractionScopes
  - commandQueue :: !CommandQueue
  }
- initCommandState :: CommandQueue -> CommandState
- 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 a. TCM a -> TCM a) -> CommandM a -> CommandM a
- liftCommandMTLocalState :: (forall a. TCM a -> TCM a) -> 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
- readsToParse :: String -> (String -> Maybe (a, String)) -> Parse a
- parseToReadsPrec :: Parse a -> Int -> String -> [(a, String)]
- exact :: String -> Parse ()
- readParse :: Read a => Parse a
- parens' :: Parse a -> Parse a
- independent :: Interaction -> Bool
- updateInteractionPointsAfter :: Interaction -> Bool
- interpret :: Interaction -> CommandM ()
- interpretWarnings :: CommandM (String, String)
- solveInstantiatedGoals :: Rewrite -> Maybe InteractionId -> CommandM ()
- cmd_load' :: FilePath -> [String] -> Bool -> Mode -> ((Interface, MaybeWarnings) -> CommandM ()) -> CommandM ()
- withCurrentFile :: CommandM a -> CommandM a
- give_gen :: UseForce -> InteractionId -> Range -> String -> GiveRefine -> CommandM ()
- highlightExpr :: Expr -> TCM ()
- sortInteractionPoints :: [InteractionId] -> TCM [InteractionId]
- prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc
- prettyContext :: Rewrite -> Bool -> InteractionId -> TCM Doc
- cmd_helper_function :: Rewrite -> InteractionId -> Range -> String -> TCM Doc
- cmd_goal_type_context_and :: Doc -> Rewrite -> InteractionId -> Range -> String -> StateT CommandState (TCMT IO) ()
- 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 ()
- refreshStr :: [String] -> String -> ([String], String)
- nameModifiers :: [String]
- parseAndDoAtToplevel :: (Expr -> TCM Doc) -> (Doc -> DisplayInfo) -> String -> CommandM ()
- maybeTimed :: CommandM a -> CommandM (Maybe Doc, a)
- tellToUpdateHighlighting :: Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource) -> IO [Response]
- tellEmacsToJumpToError :: Range -> [Response]

# Documentation

showOpenMetas :: TCM [String] Source #

Print open metas nicely.

data GiveRefine Source #

Constructors

Give |
Refine |
Intro |
ElaborateGive |

Instances

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

data CompilerBackend Source #

Available backends.

Constructors

LaTeX |
QuickLaTeX |
OtherBackend String |

Instances

Eq CompilerBackend Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods (==) :: CompilerBackend -> CompilerBackend -> Bool Source # (/=) :: CompilerBackend -> CompilerBackend -> Bool Source #
Read CompilerBackend Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods readsPrec :: Int -> ReadS CompilerBackend Source # readList :: ReadS [CompilerBackend] Source # readPrec :: ReadPrec CompilerBackend Source # readListPrec :: ReadPrec [CompilerBackend] Source #
Show CompilerBackend Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods showsPrec :: Int -> CompilerBackend -> ShowS Source # show :: CompilerBackend -> String Source # showList :: [CompilerBackend] -> ShowS Source #

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

The `Parse` monad. `StateT` state holds the remaining input.

data Remove Source #

Used to indicate whether something should be removed or not.

Constructors

Remove |
Keep |

Instances

Read Remove Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods readsPrec :: Int -> ReadS Remove Source # readList :: ReadS [Remove] Source # readPrec :: ReadPrec Remove Source # readListPrec :: ReadPrec [Remove] Source #
Show Remove Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods showsPrec :: Int -> Remove -> ShowS Source # show :: Remove -> String Source # showList :: [Remove] -> ShowS Source #

data IOTCM' range Source #

Constructors

IOTCM FilePath HighlightingLevel HighlightingMethod (Interaction' range) |

Instances

Functor IOTCM' Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods fmap :: (a -> b) -> IOTCM' a -> IOTCM' b Source # (<$) :: a -> IOTCM' b -> IOTCM' a Source #
Foldable IOTCM' Source # |

Instance details

Defined in Agda.Interaction.InteractionTop

Methods

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

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

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

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

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

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

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

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

toList :: IOTCM' a -> [a] Source #

null :: IOTCM' a -> Bool Source #

length :: IOTCM' a -> Int Source #

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

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

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

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

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

Traversable IOTCM' Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods traverse :: Applicative f => (a -> f b) -> IOTCM' a -> f (IOTCM' b) Source # sequenceA :: Applicative f => IOTCM' (f a) -> f (IOTCM' a) Source # mapM :: Monad m => (a -> m b) -> IOTCM' a -> m (IOTCM' b) Source # sequence :: Monad m => IOTCM' (m a) -> m (IOTCM' a) Source #
Read range => Read (IOTCM' range) Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods readsPrec :: Int -> ReadS (IOTCM' range) Source # readList :: ReadS [IOTCM' range] Source # readPrec :: ReadPrec (IOTCM' range) Source # readListPrec :: ReadPrec [IOTCM' range] Source #
Show range => Show (IOTCM' range) Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods showsPrec :: Int -> IOTCM' range -> ShowS Source # show :: IOTCM' range -> String Source # showList :: [IOTCM' range] -> ShowS Source #

type IOTCM = IOTCM' Range Source #

data Interaction' range Source #

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' Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods fmap :: (a -> b) -> Interaction' a -> Interaction' b Source # (<$) :: a -> Interaction' b -> Interaction' a Source #
Foldable Interaction' Source # |

Instance details

Defined in Agda.Interaction.InteractionTop

Methods

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

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

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

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

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

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

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

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

toList :: Interaction' a -> [a] Source #

null :: Interaction' a -> Bool Source #

length :: Interaction' a -> Int Source #

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

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

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

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

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

Traversable Interaction' Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods traverse :: Applicative f => (a -> f b) -> Interaction' a -> f (Interaction' b) Source # sequenceA :: Applicative f => Interaction' (f a) -> f (Interaction' a) Source # mapM :: Monad m => (a -> m b) -> Interaction' a -> m (Interaction' b) Source # sequence :: Monad m => Interaction' (m a) -> m (Interaction' a) Source #
Read range => Read (Interaction' range) Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods readsPrec :: Int -> ReadS (Interaction' range) Source # readList :: ReadS [Interaction' range] Source # readPrec :: ReadPrec (Interaction' range) Source # readListPrec :: ReadPrec [Interaction' range] Source #
Show range => Show (Interaction' range) Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods showsPrec :: Int -> Interaction' range -> ShowS Source # show :: Interaction' range -> String Source # showList :: [Interaction' range] -> ShowS Source #

type Interaction = Interaction' Range Source #

An interactive computation.

data CommandQueue Source #

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

IOTCM commands.

data Command' a Source #

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) Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods showsPrec :: Int -> Command' a -> ShowS Source # show :: Command' a -> String Source # showList :: [Command' a] -> ShowS Source #

type CommandM = StateT CommandState TCM Source #

Monad for computing answers to interactive commands.

`CommandM` is `TCMT` extended with state `CommandState`.

type OldInteractionScopes = Map InteractionId ScopeInfo Source #

data CommandState Source #

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

Initial auxiliary interaction state

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`. Use only if main errors are already catched.

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

Lift a TCM action transformer to a CommandM action transformer.

liftCommandMTLocalState :: (forall a. TCM a -> TCM a) -> 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.

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

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

exact :: String -> Parse () Source #

Demand an exact string.

readParse :: Read a => Parse a Source #

parens' :: Parse a -> Parse a Source #

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

interpretWarnings :: CommandM (String, String) Source #

Show warnings

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

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

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 :: [InteractionId] -> TCM [InteractionId] Source #

Sorts interaction points based on their ranges.

prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc Source #

Pretty-prints the type of the meta-variable.

prettyContext Source #

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

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

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

nameModifiers :: [String] Source #

parseAndDoAtToplevel Source #

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

# Orphan instances

Read AbsolutePath Source # |
Instance details Methods readsPrec :: Int -> ReadS AbsolutePath Source # readList :: ReadS [AbsolutePath] Source # readPrec :: ReadPrec AbsolutePath Source # readListPrec :: ReadPrec [AbsolutePath] Source #
Read InteractionId Source # |
Instance details Methods readsPrec :: Int -> ReadS InteractionId Source # readList :: ReadS [InteractionId] Source # readPrec :: ReadPrec InteractionId Source # readListPrec :: ReadPrec [InteractionId] Source #
Read a => Read (Range' a) Source # | Note that the grammar implemented by this instance does not necessarily match the current representation of ranges.
Instance details Methods readsPrec :: Int -> ReadS (Range' a) Source # readList :: ReadS [Range' a] Source # readPrec :: ReadPrec (Range' a) Source # readListPrec :: ReadPrec [Range' a] Source #
Read a => Read (Interval' a) Source # |
Instance details Methods readsPrec :: Int -> ReadS (Interval' a) Source # readList :: ReadS [Interval' a] Source # readPrec :: ReadPrec (Interval' a) Source # readListPrec :: ReadPrec [Interval' a] Source #
Read a => Read (Position' a) Source # |
Instance details Methods readsPrec :: Int -> ReadS (Position' a) Source # readList :: ReadS [Position' a] Source # readPrec :: ReadPrec (Position' a) Source # readListPrec :: ReadPrec [Position' a] Source #