Agda.Interaction.BasicOps

Documentation

parseExpr :: Range -> String -> TCM Expr

Parses an expression.

parseExprIn :: InteractionId -> Range -> String -> TCM Expr

giveExpr :: MetaId -> Expr -> TCM Expr

give

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).

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 Rewrite

Constructors

AsIs

Instantiated

HeadNormal

Simplified

Normalised

Instances

Read Rewrite

normalForm :: (Normalise a, Simplify a, Reduce a) => Rewrite -> a -> TCMT IO a

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.

Constructors

OfType'

Fields

ofName :: b

ofExpr :: a

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)

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

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.

parseName :: Range -> String -> TCM QName

Parse a name.

moduleContents

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 Name, [AbstractName], [AbstractModule])