Agda-2.6.1.3: 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).

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 :: Expr -> TCM Expr Source #

Evaluate the given expression in the current environment

normalForm :: (Reduce t, Simplify 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.

outputFormId :: OutputForm a b -> b Source #

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

getGoals :: TCM Goals Source #

Goals and Warnings

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.

-> QName

Module name.

-> TCM ([Name], Telescope, [(Name, Type)])

Module names, context extension, names paired up with corresponding types.

Returns the contents of the given module.

Orphan instances

Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # 
Instance details

Reify Constraint (OutputConstraint Expr Expr) Source # 
Instance details

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

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

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

(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

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

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

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