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

Safe Haskell | None

Agda.Syntax.Translation.InternalToAbstract

Description

Translating from internal syntax to abstract syntax. Enables nice pretty printing of internal syntax.

TODO

- numbers on metas - fake dependent functions to independent functions - meta parameters - shadowing

Synopsis

- class Reify i a | i -> a where
  - reify :: i -> TCM a
- class Reify i a => ReifyWhen i a where
  - reifyWhen :: Bool -> i -> TCM a
- type NamedClause = QNamed Clause
- reifyPatterns :: Telescope -> Permutation -> [Arg Pattern] -> TCM [NamedArg Pattern]

# Documentation

class Reify i a | i -> a where

Methods

reify :: i -> TCM a

Instances

Reify Literal Expr |
Reify ClauseBody RHS |
Reify MetaId Expr |
Reify Level Expr |
Reify Sort Expr |
Reify Telescope Telescope |
Reify Type Expr |
Reify Elim Expr |
Reify Term Expr |
Reify Expr Expr |
Reify DisplayTerm Expr |
Reify NamedClause Clause |
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) |
Reify Constraint (OutputConstraint Expr Expr) |
Reify i a => Reify [i] [a] |
ReifyWhen i a => Reify (Arg i) (Arg a) | Skip reification of implicit and irrelevant args if option is off.
Reify i a => Reify (Dom i) (Arg a) |
(Free i, Reify i a) => Reify (Abs i) (Name, a) |
(Reify i1 a1, Reify i2 a2) => Reify (i1, i2) (a1, a2) |
Reify i a => Reify (Named n i) (Named n a) |
(Reify t t', Reify a a') => Reify (Judgement t a) (Judgement t' a') |

class Reify i a => ReifyWhen i a where

`ReifyWhen` is a auxiliary type class to reify `Arg`.

`reifyWhen False` should produce an `underscore`. This function serves to reify hidden/irrelevant things.

Methods

reifyWhen :: Bool -> i -> TCM a

Instances

Reify i Expr => ReifyWhen i Expr |
ReifyWhen i a => ReifyWhen (Arg i) (Arg a) |
ReifyWhen i a => ReifyWhen (Named n i) (Named n a) |

type NamedClause = QNamed Clause

reifyPatterns :: Telescope -> Permutation -> [Arg Pattern] -> TCM [NamedArg Pattern]