Safe Haskell | None |
---|
- data CommandState = CommandState {}
- initCommandState :: CommandState
- newtype CommandM a = CommandM {
- unCommandM :: StateT CommandState TCM a
- runCommandM :: CommandM a -> CommandState -> TCM (a, CommandState)
- liftCommandM :: 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
- commandMToIO :: (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a
- runSafeTCM :: TCM a -> TCState -> IO (a, TCState)
- liftCommandMT :: (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
- putResponse :: Response -> CommandM ()
- runInteraction :: IOTCM -> CommandM ()
- data Interaction
- = Cmd_load FilePath [FilePath]
- | Cmd_compile Backend FilePath [FilePath]
- | Cmd_constraints
- | Cmd_metas
- | Cmd_show_module_contents_toplevel String
- | Cmd_solveAll
- | Cmd_infer_toplevel Rewrite String
- | Cmd_compute_toplevel Bool String
- | Cmd_load_highlighting_info FilePath
- | ShowImplicitArgs Bool
- | ToggleImplicitArgs
- | Cmd_give InteractionId Range String
- | Cmd_refine InteractionId Range String
- | Cmd_intro Bool InteractionId Range String
- | Cmd_refine_or_intro Bool InteractionId Range String
- | Cmd_auto InteractionId Range String
- | Cmd_context Rewrite InteractionId Range String
- | Cmd_infer Rewrite InteractionId Range String
- | Cmd_goal_type Rewrite InteractionId Range String
- | Cmd_goal_type_context Rewrite InteractionId Range String
- | Cmd_goal_type_context_infer Rewrite InteractionId Range String
- | Cmd_show_module_contents InteractionId Range String
- | Cmd_make_case InteractionId Range String
- | Cmd_compute Bool InteractionId Range String
- data IOTCM = IOTCM FilePath HighlightingLevel HighlightingMethod Interaction
- type Parse a = ErrorT String (StateT String Identity) a
- 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
- interpret :: Interaction -> CommandM ()
- type GoalCommand = InteractionId -> Range -> String -> Interaction
- cmd_load' :: FilePath -> [FilePath] -> Bool -> ((Interface, Maybe Warnings) -> CommandM ()) -> CommandM ()
- data Backend
- give_gen :: InteractionId -> Range -> String -> (InteractionId -> Maybe Range -> Expr -> TCMT IO (Expr, [InteractionId])) -> (Range -> String -> Expr -> GiveResult) -> CommandM ()
- give_gen' :: (InteractionId -> Maybe Range -> Expr -> TCMT IO (Expr, [InteractionId])) -> (Range -> String -> Expr -> GiveResult) -> InteractionId -> Range -> String -> CommandM ()
- sortInteractionPoints :: [InteractionId] -> TCM [InteractionId]
- prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc
- prettyContext :: Rewrite -> Bool -> InteractionId -> TCM Doc
- cmd_goal_type_context_and :: Doc -> Rewrite -> InteractionId -> t -> t1 -> CommandM ()
- showModuleContents :: Range -> String -> CommandM ()
- setCommandLineOptions' :: CommandLineOptions -> CommandM ()
- status :: CommandM Status
- displayStatus :: CommandM ()
- display_info :: DisplayInfo -> CommandM ()
- takenNameStr :: TCM [String]
- refreshStr :: [String] -> String -> ([String], String)
- nameModifiers :: [[Char]]
- class LowerMeta a where
- lowerMeta :: a -> a
- preMeta :: Expr
- preUscore :: Expr
- parseAndDoAtToplevel :: (Expr -> TCM Expr) -> (Doc -> DisplayInfo) -> String -> CommandM ()
- tellToUpdateHighlighting :: Maybe (HighlightingInfo, ModuleToSource) -> IO [Response]
- tellEmacsToJumpToError :: Range -> [Response]
Documentation
data CommandState Source
Auxiliary state of an interactive computation.
CommandState | |
|
MonadState CommandState CommandM |
initCommandState :: CommandStateSource
Initial auxiliary interaction state
Monad for computing answers to interactive commands.
CommandM
is TCM
extended with state CommandState
.
StateT
is in a newtype wrapper because we would like to prevent
the accidental use of lift
.
Instead of lift
one can use liftCommandM
, see below.
CommandM | |
|
runCommandM :: CommandM a -> CommandState -> TCM (a, CommandState)Source
Wrapped runStateT
for CommandM
.
liftCommandM :: TCM a -> CommandM aSource
lift a TCM action to CommandM.
liftCommandM
is a customized form of lift
for StateT
.
At the end of the lifted action stInteractionOutputCallback
is set
to its original value because the value is lost during the execution
of some TCM actions.
:: 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.
commandMToIO :: (forall x. (CommandM a -> IO x) -> IO x) -> CommandM aSource
Opposite of liftIO
for CommandM
.
Use only if main errors are already catched.
runSafeTCM :: TCM a -> TCState -> IO (a, TCState)Source
runSafeTCM
runs a safe TMC
action (a TCM
action which cannot fail)
liftCommandMT :: (forall a. TCM a -> TCM a) -> CommandM a -> CommandM aSource
Lift a TCM action transformer to a CommandM action transformer.
putResponse :: Response -> CommandM ()Source
Put a response by the callback function given by stInteractionOutputCallback
.
runInteraction :: IOTCM -> CommandM ()Source
data Interaction Source
An interactive computation.
Cmd_load FilePath [FilePath] |
|
Cmd_compile Backend FilePath [FilePath] |
|
Cmd_constraints | |
Cmd_metas | Show unsolved metas. If there are no unsolved metas but unsolved constraints show those instead. |
Cmd_show_module_contents_toplevel String | Shows all the top-level names in the given module, along with their types. Uses the top-level scope. |
Cmd_solveAll | |
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 Bool 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 |
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. |
ShowImplicitArgs Bool | Tells Agda whether or not to show implicit arguments. |
ToggleImplicitArgs | Toggle display of implicit arguments. |
Cmd_give InteractionId Range String | Goal commands If the range is |
Cmd_refine InteractionId Range String | |
Cmd_intro Bool InteractionId Range String | |
Cmd_refine_or_intro Bool InteractionId Range String | |
Cmd_auto InteractionId Range String | |
Cmd_context Rewrite InteractionId Range String | |
Cmd_infer Rewrite InteractionId Range String | |
Cmd_goal_type Rewrite InteractionId Range String | |
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_show_module_contents 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 Bool InteractionId Range String |
type Parse a = ErrorT String (StateT String Identity) aSource
The Parse
monad.
StateT
state holds the remaining input.
independent :: Interaction -> BoolSource
Can the command run even if the relevant file has not been loaded into the state?
interpret :: Interaction -> CommandM ()Source
Interpret an interaction
type GoalCommand = InteractionId -> Range -> String -> InteractionSource
:: FilePath | |
-> [FilePath] | |
-> Bool | Allow unsolved meta-variables? |
-> ((Interface, Maybe Warnings) -> CommandM ()) | |
-> CommandM () |
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
result of typeCheck
.
give_gen :: InteractionId -> Range -> String -> (InteractionId -> Maybe Range -> Expr -> TCMT IO (Expr, [InteractionId])) -> (Range -> String -> Expr -> GiveResult) -> CommandM ()Source
give_gen' :: (InteractionId -> Maybe Range -> Expr -> TCMT IO (Expr, [InteractionId])) -> (Range -> String -> Expr -> GiveResult) -> InteractionId -> Range -> String -> CommandM ()Source
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.
:: Rewrite | Normalise? |
-> Bool | Print the elements in reverse order? |
-> InteractionId | |
-> TCM Doc |
Pretty-prints the context of the given meta-variable.
cmd_goal_type_context_and :: Doc -> Rewrite -> InteractionId -> t -> t1 -> CommandM ()Source
Displays the current goal, the given document, and the current context.
showModuleContents :: Range -> String -> CommandM ()Source
Shows all the top-level names in the given module, along with their types.
setCommandLineOptions' :: CommandLineOptions -> CommandM ()Source
Sets the command line options and updates the status information.
displayStatus :: CommandM ()Source
Displays/updates status information.
display_info :: DisplayInfo -> CommandM ()Source
display_info
does what
does, but
additionally displays some status information (see display_info'
Falsestatus
and
displayStatus
).
takenNameStr :: TCM [String]Source
nameModifiers :: [[Char]]Source
LowerMeta ModuleApplication | |
LowerMeta Declaration | |
LowerMeta WhereClause | |
LowerMeta RHS | |
LowerMeta TypedBinding | |
LowerMeta TypedBindings | |
LowerMeta LamBinding | |
LowerMeta Expr | |
LowerMeta a => LowerMeta [a] | |
LowerMeta (Maybe Expr) | |
LowerMeta a => LowerMeta (Arg a) | |
LowerMeta (OpApp Expr) | |
LowerMeta a => LowerMeta (Named name a) |
:: (Expr -> TCM Expr) | 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.
tellToUpdateHighlighting :: Maybe (HighlightingInfo, 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).