Agda.Interaction.BasicOps

Documentation

parseExpr :: Range -> String -> TCM Expr

Parses an expression.

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

giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM ()

redoChecks :: Maybe InteractionId -> TCM ()

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

give

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

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

Evaluate the given expression in the current environment

evalInMeta :: InteractionId -> Expr -> TCM Expr

data Rewrite

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

Constructors

AsIs

Instantiated

HeadNormal

Simplified

Normalised

Instances

Read Rewrite

Defined in Agda.Interaction.BasicOps

Methods

readsPrec :: Int -> ReadS Rewrite

readList :: ReadS [Rewrite]

readPrec :: ReadPrec Rewrite

readListPrec :: ReadPrec [Rewrite]

Show Rewrite

Defined in Agda.Interaction.BasicOps

Methods

showsPrec :: Int -> Rewrite -> ShowS

show :: Rewrite -> String

showList :: [Rewrite] -> ShowS

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

data ComputeMode

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

Constructors

DefaultCompute

IgnoreAbstract

UseShowInstance

Instances

Eq ComputeMode

Defined in Agda.Interaction.BasicOps

Methods

(==) :: ComputeMode -> ComputeMode -> Bool

(/=) :: ComputeMode -> ComputeMode -> Bool

Read ComputeMode

Defined in Agda.Interaction.BasicOps

Methods

readsPrec :: Int -> ReadS ComputeMode

readList :: ReadS [ComputeMode]

readPrec :: ReadPrec ComputeMode

readListPrec :: ReadPrec [ComputeMode]

Show ComputeMode

Defined in Agda.Interaction.BasicOps

Methods

showsPrec :: Int -> ComputeMode -> ShowS

show :: ComputeMode -> String

showList :: [ComputeMode] -> ShowS

computeIgnoreAbstract :: ComputeMode -> Bool

computeWrapInput :: ComputeMode -> String -> String

showComputed :: ComputeMode -> Expr -> TCM Doc

data UseForce

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

Constructors

WithForce

Ignore additional checks, like termination/positivity...

WithoutForce

Don't ignore any checks.

Instances

Eq UseForce

Defined in Agda.Interaction.BasicOps

Methods

(==) :: UseForce -> UseForce -> Bool

(/=) :: UseForce -> UseForce -> Bool

Read UseForce

Defined in Agda.Interaction.BasicOps

Methods

readsPrec :: Int -> ReadS UseForce

readList :: ReadS [UseForce]

readPrec :: ReadPrec UseForce

readListPrec :: ReadPrec [UseForce]

Show UseForce

Defined in Agda.Interaction.BasicOps

Methods

showsPrec :: Int -> UseForce -> ShowS

show :: UseForce -> String

showList :: [UseForce] -> ShowS

data OutputForm a b

Constructors

OutputForm Range [ProblemId] (OutputConstraint a b)

Instances

Reify ProblemConstraint (Closure (OutputForm Expr Expr))

Defined in Agda.Interaction.BasicOps

Methods

reify :: ProblemConstraint -> TCM (Closure (OutputForm Expr Expr))

reifyWhen :: Bool -> ProblemConstraint -> TCM (Closure (OutputForm Expr Expr))

Functor (OutputForm a)

Defined in Agda.Interaction.BasicOps

Methods

fmap :: (a0 -> b) -> OutputForm a a0 -> OutputForm a b

(<$) :: a0 -> OutputForm a b -> OutputForm a a0

(Pretty a, Pretty b) => Pretty (OutputForm a b)

Defined in Agda.Interaction.BasicOps

Methods

pretty :: OutputForm a b -> Doc

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

prettyList :: [OutputForm a b] -> Doc

(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm a b) (OutputForm c d)

Defined in Agda.Interaction.BasicOps

Methods

toConcrete :: OutputForm a b -> AbsToCon (OutputForm c d)

bindToConcrete :: OutputForm a b -> (OutputForm c d -> AbsToCon b0) -> AbsToCon b0

data OutputConstraint a b

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

FindInstanceOF b a [(a, a)]

PTSInstance b b

PostponedCheckFunDef QName a

Instances

Reify Constraint (OutputConstraint Expr Expr)

Defined in Agda.Interaction.BasicOps

Methods

reify :: Constraint -> TCM (OutputConstraint Expr Expr)

reifyWhen :: Bool -> Constraint -> TCM (OutputConstraint Expr Expr)

Functor (OutputConstraint a)

Defined in Agda.Interaction.BasicOps

Methods

fmap :: (a0 -> b) -> OutputConstraint a a0 -> OutputConstraint a b

(<$) :: a0 -> OutputConstraint a b -> OutputConstraint a a0

(Pretty a, Pretty b) => Pretty (OutputConstraint a b)

Defined in Agda.Interaction.BasicOps

Methods

pretty :: OutputConstraint a b -> Doc

prettyPrec :: Int -> OutputConstraint a b -> Doc

prettyList :: [OutputConstraint a b] -> Doc

(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint a b) (OutputConstraint c d)

Defined in Agda.Interaction.BasicOps

Methods

toConcrete :: OutputConstraint a b -> AbsToCon (OutputConstraint c d)

bindToConcrete :: OutputConstraint a b -> (OutputConstraint c d -> AbsToCon b0) -> AbsToCon b0

data OutputConstraint' a b

A subset of OutputConstraint.

Constructors

OfType'

Fields

• ofName :: b
• ofExpr :: a

Instances

(Pretty a, Pretty b) => Pretty (OutputConstraint' a b)

Defined in Agda.Interaction.BasicOps

Methods

pretty :: OutputConstraint' a b -> Doc

prettyPrec :: Int -> OutputConstraint' a b -> Doc

prettyList :: [OutputConstraint' a b] -> Doc

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

Defined in Agda.Interaction.BasicOps

Methods

toConcrete :: OutputConstraint' a b -> AbsToCon (OutputConstraint' c d)

bindToConcrete :: OutputConstraint' a b -> (OutputConstraint' c d -> AbsToCon b0) -> AbsToCon b0

outputFormId :: OutputForm a b -> b

reifyElimToExpr :: Elim -> TCM Expr

getConstraints :: TCM [OutputForm Expr Expr]

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

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

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)

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 [OutputConstraint' Expr Name]

typeInCurrent :: Rewrite -> Expr -> TCM Expr

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

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

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

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

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

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

Parse a name.

isQName :: Expr -> Maybe QName

Check whether an expression is a (qualified) identifier.

moduleContents

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

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

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.

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

Orphan instances

Reify ProblemConstraint (Closure (OutputForm Expr Expr))

Methods

reify :: ProblemConstraint -> TCM (Closure (OutputForm Expr Expr))

reifyWhen :: Bool -> ProblemConstraint -> TCM (Closure (OutputForm Expr Expr))

Reify Constraint (OutputConstraint Expr Expr)

Methods

reify :: Constraint -> TCM (OutputConstraint Expr Expr)

reifyWhen :: Bool -> Constraint -> TCM (OutputConstraint Expr Expr)