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

Safe Haskell | Safe-Infered

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

- apps :: (Expr, [Arg Expr]) -> TCM Expr
- exprInfo :: ExprInfo
- reifyApp :: Expr -> [Arg Term] -> TCM Expr
- class Reify i a | i -> a where
  - reify :: i -> TCM a
- reifyDisplayForm :: QName -> Args -> TCM Expr -> TCM Expr
- reifyDisplayFormP :: LHS -> TCM LHS
- data NamedClause = NamedClause QName Clause
- stripImplicits :: [NamedArg Pattern] -> [Pattern] -> TCM ([NamedArg Pattern], [Pattern])
- class DotVars a where
  - dotVars :: a -> Set Name
- reifyPatterns :: Telescope -> Permutation -> [Arg Pattern] -> TCM [NamedArg Pattern]

# Documentation

apps :: (Expr, [Arg Expr]) -> TCM Expr

exprInfo :: ExprInfo

reifyApp :: Expr -> [Arg Term] -> TCM Expr

class Reify i a | i -> a where

Methods

reify :: i -> TCM a

Instances

Reify Literal Expr |
Reify MetaId Expr |
Reify ClauseBody RHS |
Reify Telescope Telescope |
Reify Level Expr |
Reify Sort Expr |
Reify Elim Expr |
Reify Type Expr |
Reify Term Expr |
Reify DisplayTerm Expr |
Reify NamedClause Clause |
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) |
Reify Constraint (OutputConstraint Expr Expr) |
Reify i a => Reify [i] [a] |
Reify i a => Reify (Arg 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 t t', Reify a a') => Reify (Judgement t a) (Judgement t' a') |

reifyDisplayForm :: QName -> Args -> TCM Expr -> TCM Expr

reifyDisplayFormP :: LHS -> TCM LHS

data NamedClause

Constructors

NamedClause QName Clause |

Instances

PrettyTCM NamedClause |
Reify NamedClause Clause |

stripImplicits :: [NamedArg Pattern] -> [Pattern] -> TCM ([NamedArg Pattern], [Pattern])

class DotVars a where

`dotVars ps` gives all the variables inside of dot patterns of `ps` It is only invoked for patternish things. (Ulf O-tone!) Use it for printing l.h.sides: which of the implicit arguments have to be made explicit.

Methods

dotVars :: a -> Set Name

Instances

DotVars Pattern |
DotVars RHS |
DotVars Clause |
DotVars TypedBinding |
DotVars TypedBindings |
DotVars Expr | Getting all(!) variables of an expression. It should only get free ones, but it does not matter to include the bound ones.
DotVars a => DotVars [a] |
DotVars a => DotVars (Arg a) |
(DotVars a, DotVars b) => DotVars (a, b) |
DotVars a => DotVars (Named s a) |

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