Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.BasicOps

Contents

- Orphan instances

Synopsis

- parseExpr :: Range -> String -> TCM Expr
- parseExprIn :: InteractionId -> Range -> String -> TCM Expr
- giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM Term
- redoChecks :: Maybe InteractionId -> TCM ()
- give_ :: Bool -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Term
- give :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
- elaborate_give :: Rewrite -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
- refine :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
- evalInCurrent :: ComputeMode -> Expr -> TCM Expr
- evalInMeta :: InteractionId -> ComputeMode -> Expr -> TCM Expr
- normalForm :: (Reduce t, Simplify t, Instantiate t, Normalise t) => Rewrite -> t -> TCM t
- computeIgnoreAbstract :: ComputeMode -> Bool
- computeWrapInput :: ComputeMode -> String -> String
- showComputed :: ComputeMode -> Expr -> TCM Doc
- outputFormId :: OutputForm a b -> b
- 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
- getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint) -> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
- getIPBoundary :: Rewrite -> InteractionId -> TCM [IPFace' Expr]
- typeAndFacesInMeta :: InteractionId -> Rewrite -> Expr -> TCM (Expr, [IPFace' Expr])
- getGoals :: TCM Goals
- getGoals' :: Rewrite -> Rewrite -> TCM Goals
- showGoals :: Goals -> TCM String
- getWarningsAndNonFatalErrors :: TCM WarningsAndNonFatalErrors
- getResponseContext :: Rewrite -> InteractionId -> TCM [ResponseContextEntry]
- getSolvedInteractionPoints :: Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)]
- 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 [ResponseContextEntry]
- typeInCurrent :: Rewrite -> Expr -> TCM Expr
- typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr
- introTactic :: Bool -> InteractionId -> TCM [String]
- atTopLevel :: TCM a -> TCM a
- parseName :: Range -> String -> TCM QName
- isQName :: Expr -> Maybe QName
- isName :: Expr -> Maybe Name
- moduleContents :: Rewrite -> Range -> String -> TCM ([Name], Telescope, [(Name, Type)])
- getRecordContents :: Rewrite -> Expr -> TCM ([Name], Telescope, [(Name, Type)])
- getModuleContents :: Rewrite -> Maybe QName -> TCM ([Name], Telescope, [(Name, Type)])
- whyInScope :: FilePath -> String -> TCM WhyInScopeData

# Documentation

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

Parses an expression.

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

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

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

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

give_ Source #

Arguments

:: Bool | Elaborating?
-> UseForce | Skip safety checks?
-> InteractionId | Hole.
-> Maybe Range |
-> Expr | The expression to give.
-> TCM Term | Value of the expression

Auxiliary definition for `give` and `elaborate_give`.

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

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

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 #

showComputed :: ComputeMode -> Expr -> TCM Doc Source #

outputFormId :: OutputForm a b -> b Source #

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

reifyElimToExpr :: MonadReify m => Elim -> m Expr Source #

prettyConstraints :: [Closure Constraint] -> TCM [OutputForm Expr Expr] Source #

getConstraints :: TCM [OutputForm Expr Expr] Source #

namedMetaOf :: OutputConstraint Expr a -> a Source #

getConstraintsMentioning :: Rewrite -> MetaId -> TCM [OutputForm Expr Expr] Source #

stripConstraintPids :: Constraints -> Constraints Source #

interactionIdToMetaId :: ReadTCState m => InteractionId -> m MetaId Source #

Converts an `InteractionId` to a `MetaId`.

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

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

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

typeAndFacesInMeta :: InteractionId -> Rewrite -> Expr -> TCM (Expr, [IPFace' Expr]) Source #

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.

getWarningsAndNonFatalErrors :: TCM WarningsAndNonFatalErrors Source #

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.

typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta) Source #

typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputConstraint Expr InteractionId) Source #

typeOfMeta' :: Rewrite -> (InteractionId, MetaId) -> TCM (OutputConstraint Expr InteractionId) Source #

typesOfVisibleMetas :: Rewrite -> TCM [OutputConstraint Expr InteractionId] Source #

typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta] Source #

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.

typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr Source #

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.

isName :: Expr -> Maybe Name Source #

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 type ReifiesTo Constraint = OutputConstraint Expr Expr

Methods

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

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

Reify ProblemConstraint Source # |

Instance details

Associated Types

type ReifiesTo ProblemConstraint |
Instance details Defined in Agda.Interaction.BasicOps type ReifiesTo ProblemConstraint = Closure (OutputForm Expr Expr)

Methods

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

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

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 type ConOfAbs (IPBoundary' a) = IPBoundary' (ConOfAbs a)

Methods

toConcrete :: MonadToConcrete m => IPBoundary' a -> m (ConOfAbs (IPBoundary' a)) Source #

bindToConcrete :: MonadToConcrete m => IPBoundary' a -> (ConOfAbs (IPBoundary' a) -> m b) -> m b Source #

Reify a => Reify (IPBoundary' a) Source # |

Instance details

Associated Types

type ReifiesTo (IPBoundary' a) |
Instance details Defined in Agda.Interaction.BasicOps type ReifiesTo (IPBoundary' a) = IPBoundary' (ReifiesTo a)

Methods

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

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

(Pretty a, Pretty b) => Pretty (OutputConstraint' a b) Source # |
Instance details Methods pretty :: OutputConstraint' a b -> Doc Source # prettyPrec :: Int -> OutputConstraint' a b -> Doc Source # prettyList :: [OutputConstraint' a b] -> Doc Source #
(Pretty a, Pretty b) => Pretty (OutputConstraint a b) Source # |
Instance details Methods pretty :: OutputConstraint a b -> Doc Source # prettyPrec :: Int -> OutputConstraint a b -> Doc Source # prettyList :: [OutputConstraint a b] -> Doc Source #
(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 type ConOfAbs (OutputConstraint' a b) = OutputConstraint' (ConOfAbs a) (ConOfAbs b)

Methods

toConcrete :: MonadToConcrete m => OutputConstraint' a b -> m (ConOfAbs (OutputConstraint' a b)) Source #

bindToConcrete :: MonadToConcrete m => OutputConstraint' a b -> (ConOfAbs (OutputConstraint' a b) -> m b0) -> m b0 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 type ConOfAbs (OutputConstraint a b) = OutputConstraint (ConOfAbs a) (ConOfAbs b)

Methods

toConcrete :: MonadToConcrete m => OutputConstraint a b -> m (ConOfAbs (OutputConstraint a b)) Source #

bindToConcrete :: MonadToConcrete m => OutputConstraint a b -> (ConOfAbs (OutputConstraint a b) -> m b0) -> m b0 Source #

(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 type ConOfAbs (OutputForm a b) = OutputForm (ConOfAbs a) (ConOfAbs b)

Methods

toConcrete :: MonadToConcrete m => OutputForm a b -> m (ConOfAbs (OutputForm a b)) Source #

bindToConcrete :: MonadToConcrete m => OutputForm a b -> (ConOfAbs (OutputForm a b) -> m b0) -> m b0 Source #

(Pretty a, Pretty b) => PrettyTCM (OutputForm a b) Source # |
Instance details Methods prettyTCM :: MonadPretty m => OutputForm a b -> m Doc Source #