Safe Haskell	None
Language	Haskell98

Agda.Interaction.BasicOps

Synopsis

Documentation

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

Parses an expression.

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

giveExpr :: MetaId -> Expr -> TCM Expr Source

give Source

Arguments

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

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

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

data Rewrite Source

Constructors

AsIs
Instantiated
HeadNormal
Simplified
Normalised

Instances

Read Rewrite Source

normalForm :: Rewrite -> Type -> TCM Type Source

data OutputForm a b Source

Constructors

OutputForm Range ProblemId (OutputConstraint a b)

Instances

Functor (OutputForm a) Source
(Show a, Show b) => Show (OutputForm a b) Source
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm a b) (OutputForm c d) Source

data OutputConstraint a b Source

Constructors

OfType b a
CmpInType Comparison a b b
CmpElim [Polarity] a [b] [b]
JustType b
CmpTypes Comparison b b
CmpLevels Comparison b b
CmpTeles Comparison b b
JustSort b
CmpSorts Comparison b b
Guard (OutputConstraint a b) ProblemId
Assign b a
TypedAssign b a a
PostponedCheckArgs b [a] a a
IsEmptyType a
SizeLtSat a
FindInScopeOF b a [(a, a)]

Instances

Functor (OutputConstraint a) Source
(Show a, Show b) => Show (OutputConstraint a b) Source
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint a b) (OutputConstraint c d) Source

data OutputConstraint' a b Source

A subset of OutputConstraint.

Constructors

OfType'
Fields ofName :: b ofExpr :: a

Instances

(Pretty a, Pretty b) => Pretty (OutputConstraint' a b) Source
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint' a b) (OutputConstraint' c d) Source

outputFormId :: OutputForm a b -> b Source

showComparison :: Comparison -> String Source

getConstraints :: TCM [OutputForm Expr Expr] Source

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

contextOfMeta :: InteractionId -> Rewrite -> TCM [OutputConstraint' Expr Name] Source

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

withInteractionId :: InteractionId -> TCM a -> TCM a Source

withMetaId :: MetaId -> TCM a -> TCM a Source

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

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.

moduleContents Source

Arguments

:: Rewrite	How should the types be presented
-> Range	The range of the next argument.
-> String	The module name.
-> TCM ([Name], [(Name, Type)])	Module names, names paired up with corresponding types.

Returns the contents of the given module.

whyInScope :: String -> TCM (Maybe LocalVar, [AbstractName], [AbstractModule]) Source