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 :: 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
getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint) -> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
getIPBoundary :: Rewrite -> InteractionId -> TCM [IPBoundary' 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 :: String -> TCM (Maybe LocalVar, [AbstractName], [AbstractModule])

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

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

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

getIPBoundary :: Rewrite -> InteractionId -> TCM [IPBoundary' 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 :: String -> TCM (Maybe LocalVar, [AbstractName], [AbstractModule]) Source #

Orphan instances

Reify Constraint Source #
Instance details Associated Types type ReifiesTo Constraint Source # 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 Source # Methods reify :: MonadReify m => ProblemConstraint -> m (ReifiesTo ProblemConstraint) Source # reifyWhen :: MonadReify m => Bool -> ProblemConstraint -> m (ReifiesTo ProblemConstraint) Source #
Pretty c => Pretty (IPBoundary' c) Source #
Instance details Methods pretty :: IPBoundary' c -> Doc Source # prettyPrec :: Int -> IPBoundary' c -> Doc Source # prettyList :: [IPBoundary' c] -> Doc Source #
ToConcrete a => ToConcrete (IPBoundary' a) Source #
Instance details Associated Types type ConOfAbs (IPBoundary' a) Source # Methods toConcrete :: IPBoundary' a -> AbsToCon (ConOfAbs (IPBoundary' a)) Source # bindToConcrete :: IPBoundary' a -> (ConOfAbs (IPBoundary' a) -> AbsToCon b) -> AbsToCon b Source #
Reify a => Reify (IPBoundary' a) Source #
Instance details Associated Types type ReifiesTo (IPBoundary' a) Source # 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) Source # Methods toConcrete :: OutputConstraint' a b -> AbsToCon (ConOfAbs (OutputConstraint' a b)) Source # bindToConcrete :: OutputConstraint' a b -> (ConOfAbs (OutputConstraint' a b) -> AbsToCon b0) -> AbsToCon b0 Source #
(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint a b) Source #
Instance details Associated Types type ConOfAbs (OutputConstraint a b) Source # Methods toConcrete :: OutputConstraint a b -> AbsToCon (ConOfAbs (OutputConstraint a b)) Source # bindToConcrete :: OutputConstraint a b -> (ConOfAbs (OutputConstraint a b) -> AbsToCon b0) -> AbsToCon b0 Source #
(ToConcrete a, ToConcrete b) => ToConcrete (OutputForm a b) Source #
Instance details Associated Types type ConOfAbs (OutputForm a b) Source # Methods toConcrete :: OutputForm a b -> AbsToCon (ConOfAbs (OutputForm a b)) Source # bindToConcrete :: OutputForm a b -> (ConOfAbs (OutputForm a b) -> AbsToCon b0) -> AbsToCon b0 Source #