Safe Haskell | None |
---|---|
Language | Haskell98 |
Agda.Interaction.BasicOps
- parseExpr :: Range -> String -> TCM Expr
- parseExprIn :: InteractionId -> Range -> String -> TCM Expr
- giveExpr :: MetaId -> Expr -> TCM Expr
- give :: InteractionId -> Maybe Range -> Expr -> TCM Expr
- refine :: InteractionId -> Maybe Range -> Expr -> TCM Expr
- evalInCurrent :: Expr -> TCM Expr
- evalInMeta :: InteractionId -> Expr -> TCM Expr
- data Rewrite
- normalForm :: Rewrite -> Type -> TCM Type
- data OutputForm a b = OutputForm Range ProblemId (OutputConstraint a b)
- data OutputConstraint a b
- = OfType b a
- | CmpInType Comparison a b b
- | CmpElim [Polarity] a [b] [b]
- | JustType b
- | CmpTypes Comparison b b
- | CmpLevels Comparison b b
- | CmpTeles Comparison b b
- | JustSort b
- | CmpSorts Comparison b b
- | Guard (OutputConstraint a b) ProblemId
- | Assign b a
- | TypedAssign b a a
- | PostponedCheckArgs b [a] a a
- | IsEmptyType a
- | FindInScopeOF b a [(a, a)]
- data OutputConstraint' a b = OfType' {}
- outputFormId :: OutputForm a b -> b
- showComparison :: Comparison -> String
- getConstraints :: TCM [OutputForm Expr Expr]
- getSolvedInteractionPoints :: Bool -> 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 [OutputConstraint' Expr Name]
- 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
- moduleContents :: Rewrite -> Range -> String -> TCM ([Name], [(Name, Type)])
- whyInScope :: String -> TCM (Maybe LocalVar, [AbstractName], [AbstractModule])
Documentation
parseExprIn :: InteractionId -> Range -> String -> TCM Expr
Arguments
:: 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
:: 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 :: Expr -> TCM Expr
Evaluate the given expression in the current environment
evalInMeta :: InteractionId -> Expr -> TCM Expr
normalForm :: Rewrite -> Type -> TCM Type
data OutputForm a b
Constructors
OutputForm Range ProblemId (OutputConstraint a b) |
Instances
Functor (OutputForm a) | |
(Show a, Show b) => Show (OutputForm a b) | |
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm a b) (OutputForm c d) |
data OutputConstraint a b
Constructors
OfType b a | |
CmpInType Comparison a b b | |
CmpElim [Polarity] a [b] [b] | |
JustType b | |
CmpTypes Comparison b b | |
CmpLevels Comparison b b | |
CmpTeles Comparison b b | |
JustSort b | |
CmpSorts Comparison b b | |
Guard (OutputConstraint a b) ProblemId | |
Assign b a | |
TypedAssign b a a | |
PostponedCheckArgs b [a] a a | |
IsEmptyType a | |
FindInScopeOF b a [(a, a)] |
Instances
Functor (OutputConstraint a) | |
(Show a, Show b) => Show (OutputConstraint a b) | |
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint a b) (OutputConstraint c d) |
data OutputConstraint' a b
A subset of OutputConstraint
.
Instances
(Pretty a, Pretty b) => Pretty (OutputConstraint' a b) | |
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint' a b) (OutputConstraint' c d) |
outputFormId :: OutputForm a b -> b
showComparison :: Comparison -> String
getConstraints :: TCM [OutputForm Expr Expr]
getSolvedInteractionPoints :: Bool -> TCM [(InteractionId, MetaId, Expr)]
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)
typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputConstraint Expr InteractionId)
typeOfMeta' :: Rewrite -> (InteractionId, MetaId) -> TCM (OutputConstraint Expr InteractionId)
metaHelperType :: Rewrite -> InteractionId -> Range -> String -> TCM (OutputConstraint' Expr Expr)
contextOfMeta :: InteractionId -> Rewrite -> TCM [OutputConstraint' Expr Name]
typeInCurrent :: Rewrite -> Expr -> TCM Expr
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
withInteractionId :: InteractionId -> TCM a -> TCM a
withMetaId :: MetaId -> TCM a -> TCM a
introTactic :: Bool -> InteractionId -> TCM [String]
atTopLevel :: TCM a -> TCM a
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], [(Name, Type)]) | Module names, names paired up with corresponding types. |
Returns the contents of the given module.
whyInScope :: String -> TCM (Maybe LocalVar, [AbstractName], [AbstractModule])