Agda.Interaction.BasicOps

Documentation

parseExpr :: Range -> String -> TCM Expr

Parses an expression.

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

giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM Term

redoChecks :: Maybe InteractionId -> TCM ()

After a give, redo termination etc. checks for function which was complemented.

give

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

elaborate_give

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.

refine

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

Evaluate the given expression in the current environment

evalInMeta :: InteractionId -> ComputeMode -> Expr -> TCM Expr

normalForm :: (Reduce t, Simplify t, Instantiate t, Normalise t) => Rewrite -> t -> TCM t

Modifier for interactive commands, specifying the amount of normalization in the output.

computeIgnoreAbstract :: ComputeMode -> Bool

Modifier for the interactive computation command, specifying the mode of computation and result display.

computeWrapInput :: ComputeMode -> String -> String

showComputed :: ComputeMode -> Expr -> TCM Doc

outputFormId :: OutputForm a b -> b

Modifier for interactive commands, specifying whether safety checks should be ignored.

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

Converts an InteractionId to a MetaId.

getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint) -> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]

getIPBoundary :: Rewrite -> InteractionId -> TCM [IPBoundary' Expr]

getGoals :: TCM Goals

Goals and Warnings

getGoals'

Arguments

:: Rewrite

Degree of normalization of goals.

-> Rewrite

Degree of normalization of hidden goals.

-> TCM Goals

showGoals :: Goals -> TCM String

Print open metas nicely.

getWarningsAndNonFatalErrors :: TCM WarningsAndNonFatalErrors

getResponseContext

Arguments

:: Rewrite

Normalise?

-> InteractionId

-> TCM [ResponseContextEntry]

Collecting the context of the given meta-variable.

getSolvedInteractionPoints :: Bool -> Rewrite -> 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)

Create type of application of new helper function that would solve the goal.

contextOfMeta :: InteractionId -> Rewrite -> TCM [ResponseContextEntry]

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

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

introTactic :: Bool -> InteractionId -> TCM [String]

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

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.

isQName :: Expr -> Maybe QName

Check whether an expression is a (qualified) identifier.

isName :: Expr -> Maybe Name

moduleContents

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.

getRecordContents

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.

getModuleContents

Arguments

:: Rewrite

Amount of normalization in types.

-> Maybe QName

Module name, Nothing if top-level module.

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

Orphan instances

Reify Constraint

Associated Types

type ReifiesTo Constraint

Methods

reify :: MonadReify m => Constraint -> m (ReifiesTo Constraint)

reifyWhen :: MonadReify m => Bool -> Constraint -> m (ReifiesTo Constraint)

Reify ProblemConstraint

Associated Types

type ReifiesTo ProblemConstraint

Methods

reify :: MonadReify m => ProblemConstraint -> m (ReifiesTo ProblemConstraint)

reifyWhen :: MonadReify m => Bool -> ProblemConstraint -> m (ReifiesTo ProblemConstraint)

ToConcrete a => ToConcrete (IPBoundary' a)

Associated Types

type ConOfAbs (IPBoundary' a)

Methods

toConcrete :: IPBoundary' a -> AbsToCon (ConOfAbs (IPBoundary' a))

bindToConcrete :: IPBoundary' a -> (ConOfAbs (IPBoundary' a) -> AbsToCon b) -> AbsToCon b

Reify a => Reify (IPBoundary' a)

Associated Types

type ReifiesTo (IPBoundary' a)

Methods

reify :: MonadReify m => IPBoundary' a -> m (ReifiesTo (IPBoundary' a))

reifyWhen :: MonadReify m => Bool -> IPBoundary' a -> m (ReifiesTo (IPBoundary' a))

Pretty c => Pretty (IPBoundary' c)

Methods

pretty :: IPBoundary' c -> Doc

prettyPrec :: Int -> IPBoundary' c -> Doc

prettyList :: [IPBoundary' c] -> Doc

(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint a b)

Associated Types

type ConOfAbs (OutputConstraint a b)

Methods

toConcrete :: OutputConstraint a b -> AbsToCon (ConOfAbs (OutputConstraint a b))

bindToConcrete :: OutputConstraint a b -> (ConOfAbs (OutputConstraint a b) -> AbsToCon b0) -> AbsToCon b0

(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint' a b)

Associated Types

type ConOfAbs (OutputConstraint' a b)

Methods

toConcrete :: OutputConstraint' a b -> AbsToCon (ConOfAbs (OutputConstraint' a b))

bindToConcrete :: OutputConstraint' a b -> (ConOfAbs (OutputConstraint' a b) -> AbsToCon b0) -> AbsToCon b0

(ToConcrete a, ToConcrete b) => ToConcrete (OutputForm a b)

Associated Types

type ConOfAbs (OutputForm a b)

Methods

toConcrete :: OutputForm a b -> AbsToCon (ConOfAbs (OutputForm a b))

bindToConcrete :: OutputForm a b -> (ConOfAbs (OutputForm a b) -> AbsToCon b0) -> AbsToCon b0

(Pretty a, Pretty b) => PrettyTCM (OutputForm a b)

Methods

prettyTCM :: MonadPretty m => OutputForm a b -> m Doc

(Pretty a, Pretty b) => Pretty (OutputConstraint a b)

Methods

pretty :: OutputConstraint a b -> Doc

prettyPrec :: Int -> OutputConstraint a b -> Doc

prettyList :: [OutputConstraint a b] -> Doc

(Pretty a, Pretty b) => Pretty (OutputConstraint' a b)

Methods

pretty :: OutputConstraint' a b -> Doc

prettyPrec :: Int -> OutputConstraint' a b -> Doc

prettyList :: [OutputConstraint' a b] -> Doc

(Pretty a, Pretty b) => Pretty (OutputForm a b)

Methods

pretty :: OutputForm a b -> Doc

prettyPrec :: Int -> OutputForm a b -> Doc

prettyList :: [OutputForm a b] -> Doc