Agda-2.6.0.1: 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 ()
- redoChecks :: Maybe InteractionId -> TCM ()
- give :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
- refine :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
- evalInCurrent :: Expr -> TCM Expr
- evalInMeta :: InteractionId -> Expr -> TCM Expr
- data Rewrite
  - = AsIs
  - | Instantiated
  - | HeadNormal
  - | Simplified
  - | Normalised
- normalForm :: (Reduce t, Simplify t, Normalise t) => Rewrite -> t -> TCM t
- data ComputeMode
  - = DefaultCompute
  - | IgnoreAbstract
  - | UseShowInstance
- computeIgnoreAbstract :: ComputeMode -> Bool
- computeWrapInput :: ComputeMode -> String -> String
- showComputed :: ComputeMode -> Expr -> TCM Doc
- data UseForce
  - = WithForce
  - | WithoutForce
- data OutputForm a b = OutputForm Range [ProblemId] (OutputConstraint a b)
- data OutputConstraint a b
  - = 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
- data OutputConstraint' a b = OfType' {
  - ofName :: b
  - ofExpr :: a
  }
- 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)]
- 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
- typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr
- withInteractionId :: InteractionId -> TCM a -> TCM a
- withMetaId :: MetaId -> TCM a -> TCM a
- introTactic :: Bool -> InteractionId -> TCM [String]
- atTopLevel :: TCM a -> TCM a
- parseName :: Range -> String -> TCM QName
- isQName :: Expr -> Maybe QName
- moduleContents :: Rewrite -> Range -> String -> TCM ([Name], Telescope, [(Name, Type)])
- getRecordContents :: Rewrite -> Expr -> TCM ([Name], Telescope, [(Name, Type)])
- getModuleContents :: Rewrite -> 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 () 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``).

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

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

data Rewrite Source #

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

Constructors

AsIs |
Instantiated |
HeadNormal |
Simplified |
Normalised |

Instances

Read Rewrite Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods readsPrec :: Int -> ReadS Rewrite Source # readList :: ReadS [Rewrite] Source # readPrec :: ReadPrec Rewrite Source # readListPrec :: ReadPrec [Rewrite] Source #
Show Rewrite Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods showsPrec :: Int -> Rewrite -> ShowS Source # show :: Rewrite -> String Source # showList :: [Rewrite] -> ShowS Source #

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

data ComputeMode Source #

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

Constructors

DefaultCompute |
IgnoreAbstract |
UseShowInstance |

Instances

Eq ComputeMode Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods (==) :: ComputeMode -> ComputeMode -> Bool Source # (/=) :: ComputeMode -> ComputeMode -> Bool Source #
Read ComputeMode Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods readsPrec :: Int -> ReadS ComputeMode Source # readList :: ReadS [ComputeMode] Source # readPrec :: ReadPrec ComputeMode Source # readListPrec :: ReadPrec [ComputeMode] Source #
Show ComputeMode Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods showsPrec :: Int -> ComputeMode -> ShowS Source # show :: ComputeMode -> String Source # showList :: [ComputeMode] -> ShowS Source #

computeIgnoreAbstract :: ComputeMode -> Bool Source #

computeWrapInput :: ComputeMode -> String -> String Source #

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

data UseForce Source #

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 Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods (==) :: UseForce -> UseForce -> Bool Source # (/=) :: UseForce -> UseForce -> Bool Source #
Read UseForce Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods readsPrec :: Int -> ReadS UseForce Source # readList :: ReadS [UseForce] Source # readPrec :: ReadPrec UseForce Source # readListPrec :: ReadPrec [UseForce] Source #
Show UseForce Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods showsPrec :: Int -> UseForce -> ShowS Source # show :: UseForce -> String Source # showList :: [UseForce] -> ShowS Source #

data OutputForm a b Source #

Constructors

OutputForm Range [ProblemId] (OutputConstraint a b) |

Instances

Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source # reifyWhen :: Bool -> ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source #
Functor (OutputForm a) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods fmap :: (a0 -> b) -> OutputForm a a0 -> OutputForm a b Source # (<$) :: a0 -> OutputForm a b -> OutputForm a a0 Source #
(Pretty a, Pretty b) => Pretty (OutputForm a b) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods pretty :: OutputForm a b -> Doc Source # prettyPrec :: Int -> OutputForm a b -> Doc Source # prettyList :: [OutputForm a b] -> Doc Source #
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm a b) (OutputForm c d) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods toConcrete :: OutputForm a b -> AbsToCon (OutputForm c d) Source # bindToConcrete :: OutputForm a b -> (OutputForm c d -> AbsToCon b0) -> AbsToCon b0 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 |
FindInstanceOF b a [(a, a)] |
PTSInstance b b |
PostponedCheckFunDef QName a |

Instances

Reify Constraint (OutputConstraint Expr Expr) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: Constraint -> TCM (OutputConstraint Expr Expr) Source # reifyWhen :: Bool -> Constraint -> TCM (OutputConstraint Expr Expr) Source #
Functor (OutputConstraint a) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods fmap :: (a0 -> b) -> OutputConstraint a a0 -> OutputConstraint a b Source # (<$) :: a0 -> OutputConstraint a b -> OutputConstraint a a0 Source #
(Pretty a, Pretty b) => Pretty (OutputConstraint a b) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods pretty :: OutputConstraint a b -> Doc Source # prettyPrec :: Int -> OutputConstraint a b -> Doc Source # prettyList :: [OutputConstraint a b] -> Doc Source #
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint a b) (OutputConstraint c d) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods toConcrete :: OutputConstraint a b -> AbsToCon (OutputConstraint c d) Source # bindToConcrete :: OutputConstraint a b -> (OutputConstraint c d -> AbsToCon b0) -> AbsToCon b0 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 # |
Instance details Defined in Agda.Interaction.BasicOps Methods pretty :: OutputConstraint' a b -> Doc Source # prettyPrec :: Int -> OutputConstraint' a b -> Doc Source # prettyList :: [OutputConstraint' a b] -> Doc Source #
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint' a b) (OutputConstraint' c d) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods toConcrete :: OutputConstraint' a b -> AbsToCon (OutputConstraint' c d) Source # bindToConcrete :: OutputConstraint' a b -> (OutputConstraint' c d -> AbsToCon b0) -> AbsToCon b0 Source #

outputFormId :: OutputForm a b -> b Source #

reifyElimToExpr :: Elim -> TCM Expr Source #

getConstraints :: TCM [OutputForm Expr Expr] Source #

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

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 #

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 #

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.

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

# Orphan instances

Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # |
Instance details Methods reify :: ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source # reifyWhen :: Bool -> ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source #
Reify Constraint (OutputConstraint Expr Expr) Source # |
Instance details Methods reify :: Constraint -> TCM (OutputConstraint Expr Expr) Source # reifyWhen :: Bool -> Constraint -> TCM (OutputConstraint Expr Expr) Source #