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, [InteractionId])
- addDecl :: Declaration -> TCM [InteractionId]
- refine :: InteractionId -> Maybe Range -> Expr -> TCM (Expr, [InteractionId])
- evalInCurrent :: Expr -> TCM Expr
- evalInMeta :: InteractionId -> Expr -> TCM Expr
- data Rewrite
- = AsIs
- | Instantiated
- | HeadNormal
- | Normalised
- data OutputForm a b = OutputForm 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
- | IsEmptyType a
- | FindInScopeOF b
- 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 :: TCM [(InteractionId, MetaId, Expr)]
- typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr MetaId)
- typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputConstraint Expr InteractionId)
- typesOfVisibleMetas :: Rewrite -> TCM [OutputConstraint Expr InteractionId]
- typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr MetaId]
- 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 :: InteractionId -> TCM [String]
- atTopLevel :: TCM a -> TCM a
- moduleContents :: Range -> String -> TCM ([Name], [(Name, Type)])
Documentation
parseExprIn :: InteractionId -> Range -> String -> TCM Expr
give :: InteractionId -> Maybe Range -> Expr -> TCM (Expr, [InteractionId])
addDecl :: Declaration -> TCM [InteractionId]
refine :: InteractionId -> Maybe Range -> Expr -> TCM (Expr, [InteractionId])
evalInCurrent :: Expr -> TCM Expr
Evaluate the given expression in the current environment
evalInMeta :: InteractionId -> Expr -> TCM Expr
data Rewrite
Constructors
AsIs | |
Instantiated | |
HeadNormal | |
Normalised |
data OutputForm a b
Constructors
OutputForm 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 | |
IsEmptyType a | |
FindInScopeOF b |
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 :: TCM [(InteractionId, MetaId, Expr)]
typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr MetaId)
typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputConstraint Expr InteractionId)
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 :: 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.