Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.BasicOps

Synopsis

Documentation

parseExpr :: Range -> String -> TCM Expr Source #

Parses an expression.

redoChecks :: Maybe InteractionId -> TCM () Source #

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

give Source #

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

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

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

Evaluate the given expression in the current environment

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

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

computeIgnoreAbstract :: ComputeMode -> Bool Source #

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

computeWrapInput :: ComputeMode -> String -> String Source #

outputFormId :: OutputForm a b -> b Source #

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

getIPBoundary :: Rewrite -> InteractionId -> TCM [IPFace' Expr] Source #

Reify the boundary of an interaction point as something that can be shown to the user.

getGoals :: TCM Goals Source #

Goals and Warnings

getGoals' Source #

Arguments

:: Rewrite

Degree of normalization of goals.

-> Rewrite

Degree of normalization of hidden goals.

-> TCM Goals 

showGoals :: Goals -> TCM String Source #

Print open metas nicely.

getResponseContext Source #

Arguments

:: Rewrite

Normalise?

-> InteractionId 
-> TCM [ResponseContextEntry] 

Collecting the context of the given meta-variable.

getSolvedInteractionPoints :: Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)] Source #

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.

metaHelperType :: Rewrite -> InteractionId -> Range -> String -> TCM (OutputConstraint' Expr Expr) Source #

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

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

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

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.

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

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

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

Parse a name.

isQName :: Expr -> Maybe QName Source #

Check whether an expression is a (qualified) identifier.

moduleContents Source #

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

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

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

Orphan instances

Reify Constraint Source # 
Instance details

Associated Types

type ReifiesTo Constraint 
Instance details

Defined in Agda.Interaction.BasicOps

Reify ProblemConstraint Source # 
Instance details

Pretty c => Pretty (IPFace' c) Source # 
Instance details

Methods

pretty :: IPFace' c -> Doc Source #

prettyPrec :: Int -> IPFace' c -> Doc Source #

prettyList :: [IPFace' c] -> Doc Source #

ToConcrete a => ToConcrete (IPBoundary' a) Source # 
Instance details

Associated Types

type ConOfAbs (IPBoundary' a) 
Instance details

Defined in Agda.Interaction.BasicOps

Reify a => Reify (IPBoundary' a) Source # 
Instance details

Associated Types

type ReifiesTo (IPBoundary' a) 
Instance details

Defined in Agda.Interaction.BasicOps

(Pretty a, Pretty b) => Pretty (OutputConstraint' a b) Source # 
Instance details

(Pretty a, Pretty b) => Pretty (OutputConstraint a b) Source # 
Instance details

(Pretty a, Pretty b) => Pretty (OutputForm a b) Source # 
Instance details

Methods

pretty :: OutputForm a b -> Doc Source #

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

prettyList :: [OutputForm a b] -> Doc Source #

(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint' a b) Source # 
Instance details

Associated Types

type ConOfAbs (OutputConstraint' a b) 
Instance details

Defined in Agda.Interaction.BasicOps

(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint a b) Source # 
Instance details

Associated Types

type ConOfAbs (OutputConstraint a b) 
Instance details

Defined in Agda.Interaction.BasicOps

(ToConcrete a, ToConcrete b) => ToConcrete (OutputForm a b) Source # 
Instance details

Associated Types

type ConOfAbs (OutputForm a b) 
Instance details

Defined in Agda.Interaction.BasicOps

(Pretty a, Pretty b) => PrettyTCM (OutputForm a b) Source # 
Instance details

Methods

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