| 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 Term
- redoChecks :: Maybe InteractionId -> TCM ()
- give :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
- elaborate_give :: Rewrite -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
- refine :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
- evalInCurrent :: ComputeMode -> Expr -> TCM Expr
- evalInMeta :: InteractionId -> ComputeMode -> Expr -> TCM Expr
- normalForm :: (Reduce t, Simplify t, Instantiate 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
- interactionIdToMetaId :: ReadTCState m => InteractionId -> m MetaId
- getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint) -> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
- getIPBoundary :: Rewrite -> InteractionId -> TCM [IPFace' Expr]
- typeAndFacesInMeta :: InteractionId -> Rewrite -> Expr -> TCM (Expr, [IPFace' Expr])
- getGoals :: TCM Goals
- getGoals' :: Rewrite -> Rewrite -> 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
- introTactic :: Bool -> InteractionId -> TCM [String]
- atTopLevel :: TCM a -> TCM a
- parseName :: Range -> String -> TCM QName
- isQName :: Expr -> Maybe QName
- isName :: Expr -> Maybe Name
- moduleContents :: Rewrite -> Range -> String -> TCM ([Name], Telescope, [(Name, Type)])
- getRecordContents :: Rewrite -> Expr -> TCM ([Name], Telescope, [(Name, Type)])
- getModuleContents :: Rewrite -> Maybe QName -> TCM ([Name], Telescope, [(Name, Type)])
- whyInScope :: FilePath -> String -> TCM WhyInScopeData
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
| :: Rewrite | Normalise result? |
| -> UseForce | Skip safety checks? |
| -> InteractionId | Hole. |
| -> Maybe Range | |
| -> Expr | The expression to give. |
| -> TCM Expr | If successful, return the elaborated expression. |
Try to fill hole by elaborated expression.
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.
evalInCurrent :: ComputeMode -> Expr -> TCM Expr Source #
Evaluate the given expression in the current environment
evalInMeta :: InteractionId -> ComputeMode -> Expr -> TCM Expr Source #
normalForm :: (Reduce t, Simplify t, Instantiate 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 #
interactionIdToMetaId :: ReadTCState m => InteractionId -> m MetaId Source #
Converts an InteractionId to a MetaId.
getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint) -> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr] Source #
getIPBoundary :: Rewrite -> InteractionId -> TCM [IPFace' Expr] Source #
Reify the boundary of an interaction point as something that can be shown to the user.
typeAndFacesInMeta :: InteractionId -> Rewrite -> Expr -> TCM (Expr, [IPFace' 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 #
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. |
| -> Maybe 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 :: FilePath -> String -> TCM WhyInScopeData Source #