Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
- class Reify i a | i -> a where
- data NamedClause = NamedClause QName Bool Clause
- reifyPatterns :: MonadTCM tcm => [NamedArg DeBruijnPattern] -> tcm [NamedArg Pattern]
Documentation
class Reify i a | i -> a where Source #
Reify MetaId Expr Source # | |
Reify Name Name Source # | |
Reify Literal Expr Source # | |
Reify Level Expr Source # | |
Reify Sort Expr Source # | |
Reify Telescope Telescope Source # | |
Reify Type Expr Source # | |
Reify Term Expr Source # | |
Reify Expr Expr Source # | |
Reify DisplayTerm Expr Source # | |
Reify NamedClause Clause Source # | |
Reify (QNamed Clause) Clause Source # | |
Reify i a => Reify [i] [a] Source # | |
Reify i a => Reify (Dom i) (Arg a) Source # | |
Reify i a => Reify (Arg i) (Arg a) Source # | Skip reification of implicit and irrelevant args if option is off. |
Reify i a => Reify (Elim' i) (Elim' a) Source # | |
(Free i, Reify i a) => Reify (Abs i) (Name, a) Source # | |
(Reify i1 a1, Reify i2 a2) => Reify (i1, i2) (a1, a2) Source # | |
Reify i a => Reify (Named n i) (Named n a) Source # | |
(Reify i1 a1, Reify i2 a2, Reify i3 a3) => Reify (i1, i2, i3) (a1, a2, a3) Source # | |
(Reify i1 a1, Reify i2 a2, Reify i3 a3, Reify i4 a4) => Reify (i1, i2, i3, i4) (a1, a2, a3, a4) Source # | |
data NamedClause Source #
NamedClause QName Bool Clause | Also tracks whether module parameters should be dropped from the patterns. |
reifyPatterns :: MonadTCM tcm => [NamedArg DeBruijnPattern] -> tcm [NamedArg Pattern] Source #
Assumes that pattern variables have been added to the context already. Picks pattern variable names from context.