| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.BasicOps
Contents
Synopsis
- parseExpr :: Range -> String -> TCM Expr
- parseExprIn :: InteractionId -> Range -> String -> TCM Expr
- giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM ()
- redoChecks :: Maybe InteractionId -> TCM ()
- give :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
- refine :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
- evalInCurrent :: Expr -> TCM Expr
- evalInMeta :: InteractionId -> Expr -> TCM Expr
- normalForm :: (Reduce t, Simplify t, Normalise t) => Rewrite -> t -> TCM t
- computeIgnoreAbstract :: ComputeMode -> Bool
- computeWrapInput :: ComputeMode -> String -> String
- showComputed :: ComputeMode -> Expr -> TCM Doc
- outputFormId :: OutputForm a b -> b
- reifyElimToExpr :: MonadReify m => Elim -> m Expr
- prettyConstraints :: [Closure Constraint] -> TCM [OutputForm Expr Expr]
- getConstraints :: TCM [OutputForm Expr Expr]
- namedMetaOf :: OutputConstraint Expr a -> a
- getConstraintsMentioning :: Rewrite -> MetaId -> TCM [OutputForm Expr Expr]
- stripConstraintPids :: Constraints -> Constraints
- getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint) -> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
- getIPBoundary :: Rewrite -> InteractionId -> TCM [IPBoundary' Expr]
- getGoals :: TCM Goals
- showGoals :: Goals -> TCM String
- getWarningsAndNonFatalErrors :: TCM WarningsAndNonFatalErrors
- getResponseContext :: Rewrite -> InteractionId -> TCM [ResponseContextEntry]
- getSolvedInteractionPoints :: Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)]
- typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
- typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputConstraint Expr InteractionId)
- typeOfMeta' :: Rewrite -> (InteractionId, MetaId) -> TCM (OutputConstraint Expr InteractionId)
- typesOfVisibleMetas :: Rewrite -> TCM [OutputConstraint Expr InteractionId]
- typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta]
- metaHelperType :: Rewrite -> InteractionId -> Range -> String -> TCM (OutputConstraint' Expr Expr)
- contextOfMeta :: InteractionId -> Rewrite -> TCM [ResponseContextEntry]
- typeInCurrent :: Rewrite -> Expr -> TCM Expr
- typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr
- withInteractionId :: InteractionId -> TCM a -> TCM a
- withMetaId :: MetaId -> TCM a -> TCM a
- introTactic :: Bool -> InteractionId -> TCM [String]
- atTopLevel :: TCM a -> TCM a
- parseName :: Range -> String -> TCM QName
- isQName :: Expr -> Maybe QName
- moduleContents :: Rewrite -> Range -> String -> TCM ([Name], Telescope, [(Name, Type)])
- getRecordContents :: Rewrite -> Expr -> TCM ([Name], Telescope, [(Name, Type)])
- getModuleContents :: Rewrite -> QName -> TCM ([Name], Telescope, [(Name, Type)])
- whyInScope :: String -> TCM (Maybe LocalVar, [AbstractName], [AbstractModule])
Documentation
parseExprIn :: InteractionId -> Range -> String -> TCM Expr Source #
redoChecks :: Maybe InteractionId -> TCM () Source #
After a give, redo termination etc. checks for function which was complemented.
Arguments
| :: UseForce | Skip safety checks? |
| -> InteractionId | Hole. |
| -> Maybe Range | |
| -> Expr | The expression to give. |
| -> TCM Expr | If successful, the very expression is returned unchanged. |
Try to fill hole by expression.
Returns the given expression unchanged
(for convenient generalization to refine
Arguments
| :: UseForce | Skip safety checks when giving? |
| -> InteractionId | Hole. |
| -> Maybe Range | |
| -> Expr | The expression to refine the hole with. |
| -> TCM Expr | The successfully given expression. |
Try to refine hole by expression e.
This amounts to successively try to give e, e ?, e ? ?, ...
Returns the successfully given expression.
evalInMeta :: InteractionId -> Expr -> TCM Expr Source #
normalForm :: (Reduce t, Simplify t, Normalise t) => Rewrite -> t -> TCM t Source #
Modifier for interactive commands, specifying the amount of normalization in the output.
computeIgnoreAbstract :: ComputeMode -> Bool Source #
Modifier for the interactive computation command, specifying the mode of computation and result display.
computeWrapInput :: ComputeMode -> String -> String Source #
showComputed :: ComputeMode -> Expr -> TCM Doc Source #
outputFormId :: OutputForm a b -> b Source #
Modifier for interactive commands, specifying whether safety checks should be ignored.
reifyElimToExpr :: MonadReify m => Elim -> m Expr Source #
prettyConstraints :: [Closure Constraint] -> TCM [OutputForm Expr Expr] Source #
getConstraints :: TCM [OutputForm Expr Expr] Source #
namedMetaOf :: OutputConstraint Expr a -> a Source #
getConstraintsMentioning :: Rewrite -> MetaId -> TCM [OutputForm Expr Expr] Source #
getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint) -> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr] Source #
getIPBoundary :: Rewrite -> InteractionId -> TCM [IPBoundary' Expr] Source #
Arguments
| :: Rewrite | Normalise? |
| -> InteractionId | |
| -> TCM [ResponseContextEntry] |
Collecting the context of the given meta-variable.
getSolvedInteractionPoints :: Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)] Source #
getSolvedInteractionPoints True returns all solutions,
even if just solved by another, non-interaction meta.
getSolvedInteractionPoints False only returns metas that
are solved by a non-meta.
typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta) Source #
typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputConstraint Expr InteractionId) Source #
typeOfMeta' :: Rewrite -> (InteractionId, MetaId) -> TCM (OutputConstraint Expr InteractionId) Source #
metaHelperType :: Rewrite -> InteractionId -> Range -> String -> TCM (OutputConstraint' Expr Expr) Source #
Create type of application of new helper function that would solve the goal.
contextOfMeta :: InteractionId -> Rewrite -> TCM [ResponseContextEntry] Source #
Gives a list of names and corresponding types. This list includes not only the local variables in scope, but also the let-bindings.
typeInCurrent :: Rewrite -> Expr -> TCM Expr Source #
Returns the type of the expression in the current environment We wake up irrelevant variables just in case the user want to invoke that command in an irrelevant context.
typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr Source #
withInteractionId :: InteractionId -> TCM a -> TCM a Source #
introTactic :: Bool -> InteractionId -> TCM [String] Source #
The intro tactic.
Returns the terms (as strings) that can be used to refine the goal. Uses the coverage checker to find out which constructors are possible.
atTopLevel :: TCM a -> TCM a Source #
Runs the given computation as if in an anonymous goal at the end of the top-level module.
Sets up current module, scope, and context.
Arguments
| :: Rewrite | How should the types be presented? |
| -> Range | The range of the next argument. |
| -> String | The module name. |
| -> TCM ([Name], Telescope, [(Name, Type)]) | Module names, context extension needed to print types, names paired up with corresponding types. |
Returns the contents of the given module or record.
Arguments
| :: Rewrite | Amount of normalization in types. |
| -> Expr | Expression presumably of record type. |
| -> TCM ([Name], Telescope, [(Name, Type)]) | Module names, context extension, names paired up with corresponding types. |
Returns the contents of the given record identifier.
Arguments
| :: Rewrite | Amount of normalization in types. |
| -> QName | Module name. |
| -> TCM ([Name], Telescope, [(Name, Type)]) | Module names, context extension, names paired up with corresponding types. |
Returns the contents of the given module.
whyInScope :: String -> TCM (Maybe LocalVar, [AbstractName], [AbstractModule]) Source #