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 :: (Reduce a, Simplify a, Normalise a) => Rewrite -> a -> TCMT IO a
- 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
- judgToOutputForm :: Judgement a c -> OutputConstraint a c
- 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 :: Range -> String -> TCM ([Name], [(Name, Type)])
- whyInScope :: String -> TCM (Maybe Name, [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
data OutputForm a b
Constructors
OutputForm Range ProblemId (OutputConstraint a b) |
Instances
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) | |
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
Reify Constraint (OutputConstraint Expr Expr) | |
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
judgToOutputForm :: Judgement a c -> OutputConstraint a c
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
:: 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 Name, [AbstractName], [AbstractModule])