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

Agda.Interaction.BasicOps

Synopsis

- parseExpr :: Range -> String -> TCM Expr
- parseExprIn :: InteractionId -> Range -> String -> TCM Expr
- giveExpr :: MetaId -> Expr -> TCM Expr
- give :: InteractionId -> Maybe Range -> Expr -> TCM (Expr, [InteractionId])
- addDecl :: Declaration -> TCM [InteractionId]
- refine :: InteractionId -> Maybe Range -> Expr -> TCM (Expr, [InteractionId])
- evalInCurrent :: Expr -> TCM Expr
- evalInMeta :: InteractionId -> Expr -> TCM Expr
- data Rewrite
  - = AsIs
  - | Instantiated
  - | HeadNormal
  - | Normalised
- data OutputForm a b
  - = OfType b a
  - | CmpInType Comparison a b b
  - | CmpTerms [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 (OutputForm a b) [OutputForm a b]
  - | Assign b a
  - | TypedAssign b a a
  - | IsEmptyType a
- data OutputForm' a b = OfType' {
  - ofName :: b
  - ofExpr :: a
  }
- outputFormId :: OutputForm a b -> b
- showComparison :: Comparison -> String
- judgToOutputForm :: Judgement a c -> OutputForm a c
- getConstraint :: Int -> TCM (OutputForm Expr Expr)
- getConstraints :: TCM [OutputForm Expr Expr]
- getSolvedInteractionPoints :: TCM [(InteractionId, MetaId, Expr)]
- typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputForm Expr MetaId)
- typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputForm Expr InteractionId)
- typesOfVisibleMetas :: Rewrite -> TCM [OutputForm Expr InteractionId]
- typesOfHiddenMetas :: Rewrite -> TCM [OutputForm Expr MetaId]
- contextOfMeta :: InteractionId -> Rewrite -> TCM [OutputForm' 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 :: InteractionId -> TCM [String]
- atTopLevel :: TCM a -> TCM a
- moduleContents :: Range -> String -> TCM ([Name], [(Name, Type)])

# Documentation

parseExpr :: Range -> String -> TCM Expr

Parses an expression.

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

giveExpr :: MetaId -> Expr -> TCM Expr

give :: InteractionId -> Maybe Range -> Expr -> TCM (Expr, [InteractionId])

addDecl :: Declaration -> TCM [InteractionId]

refine :: InteractionId -> Maybe Range -> Expr -> TCM (Expr, [InteractionId])

evalInCurrent :: Expr -> TCM Expr

Evaluate the given expression in the current environment

evalInMeta :: InteractionId -> Expr -> TCM Expr

data Rewrite

Constructors

AsIs |
Instantiated |
HeadNormal |
Normalised |

data OutputForm a b

Constructors

OfType b a |
CmpInType Comparison a b b |
CmpTerms [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 (OutputForm a b) [OutputForm a b] |
Assign b a |
TypedAssign b a a |
IsEmptyType a |

Instances

Reify Constraint (OutputForm Expr Expr) |
Functor (OutputForm a) |
(Show a, Show b) => Show (OutputForm a b) |
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm a b) (OutputForm c d) |

data OutputForm' a b

A subset of `OutputForm`.

Constructors

OfType' |

Fields

ofName :: b
ofExpr :: a

Instances

(Pretty a, Pretty b) => Pretty (OutputForm' a b) |
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm' a b) (OutputForm' c d) |

outputFormId :: OutputForm a b -> b

showComparison :: Comparison -> String

judgToOutputForm :: Judgement a c -> OutputForm a c

getConstraint :: Int -> TCM (OutputForm Expr Expr)

getConstraints :: TCM [OutputForm Expr Expr]

getSolvedInteractionPoints :: TCM [(InteractionId, MetaId, Expr)]

typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputForm Expr MetaId)

typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputForm Expr InteractionId)

typesOfVisibleMetas :: Rewrite -> TCM [OutputForm Expr InteractionId]

typesOfHiddenMetas :: Rewrite -> TCM [OutputForm Expr MetaId]

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

typeInCurrent :: Rewrite -> Expr -> TCM Expr

Returns the type of the expression in the current environment

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

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

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

introTactic :: InteractionId -> TCM [String]

atTopLevel :: TCM a -> TCM a

Runs the given computation as if in an anonymous goal at the end of the top-level module.

moduleContents

Arguments

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