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

Safe Haskell | None

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
- rewrite :: (Normalise a, Reduce a) => Rewrite -> a -> TCMT IO a
- data OutputForm a b = OutputForm 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
  - | IsEmptyType a
  - | FindInScopeOF b a [(a, a)]
- data OutputConstraint' a b = OfType' {
  - ofName :: b
  - ofExpr :: a
  }
- outputFormId :: OutputForm a b -> b
- showComparison :: Comparison -> String
- judgToOutputForm :: Judgement a c -> OutputConstraint a c
- getConstraints :: TCM [OutputForm Expr Expr]
- getSolvedInteractionPoints :: TCM [(InteractionId, MetaId, Expr)]
- typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
- typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputConstraint Expr InteractionId)
- typesOfVisibleMetas :: Rewrite -> TCM [OutputConstraint Expr InteractionId]
- typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta]
- 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
- 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 |

Instances

Read Rewrite |

rewrite :: (Normalise a, Reduce a) => Rewrite -> a -> TCMT IO a

data OutputForm a b

Constructors

OutputForm ProblemId (OutputConstraint a b) |

Instances

Reify ProblemConstraint (Closure (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 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 |
IsEmptyType a |
FindInScopeOF b a [(a, a)] |

Instances

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

data OutputConstraint' a b

A subset of `OutputConstraint`.

Constructors

OfType' |

Fields

ofName :: b
ofExpr :: a

Instances

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

outputFormId :: OutputForm a b -> b

showComparison :: Comparison -> String

judgToOutputForm :: Judgement a c -> OutputConstraint a c

getConstraints :: TCM [OutputForm Expr Expr]

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

typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)

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

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

typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta]

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]

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.