<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Agda.Syntax.Translation.InternalToAbstract</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();setSynopsis("mini_Agda-Syntax-Translation-InternalToAbstract.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Syntax-Translation-InternalToAbstract.html">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul><p class="caption">Agda-2.3.2.1: A dependently typed functional programming language and proof assistant</p></div><div id="content"><div id="module-header"><table class="info"><tr><th>Safe Haskell</th><td>None</td></tr></table><p class="caption">Agda.Syntax.Translation.InternalToAbstract</p></div><div id="description"><p class="caption">Description</p><div class="doc"><p>Translating from internal syntax to abstract syntax. Enables nice
pretty printing of internal syntax.
</p><p>TODO
</p><ul><li> numbers on metas
- fake dependent functions to independent functions
- meta parameters
- shadowing
</li></ul></div></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><span class="keyword">class</span> <a href="#t:Reify">Reify</a> i a | i -> a <span class="keyword">where</span><ul class="subs"><li><a href="#v:reify">reify</a> :: i -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a</li></ul></li><li class="src short"><span class="keyword">class</span> <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> i a => <a href="#t:ReifyWhen">ReifyWhen</a> i a <span class="keyword">where</span><ul class="subs"><li><a href="#v:reifyWhen">reifyWhen</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a> -> i -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a</li></ul></li><li class="src short"><span class="keyword">type</span> <a href="#t:NamedClause">NamedClause</a> = <a href="Agda-Syntax-Abstract-Name.html#t:QNamed">QNamed</a> <a href="Agda-Syntax-Internal.html#t:Clause">Clause</a></li><li class="src short"><a href="#v:reifyPatterns">reifyPatterns</a> :: <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Pattern">Pattern</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Abstract.html#t:Pattern">Pattern</a>]</li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:Reify" class="def">Reify</a> i a | i -> a <span class="keyword">where</span><a href="src/Agda-Syntax-Translation-InternalToAbstract.html#Reify" class="link">Source</a></p><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:reify" class="def">reify</a> :: i -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a<a href="src/Agda-Syntax-Translation-InternalToAbstract.html#reify" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:Reify" class="caption collapser" onclick="toggleSection('i:Reify')">Instances</p><div id="section.i:Reify" class="show"><table><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> <a href="Agda-Syntax-Internal.html#t:ClauseBody">ClauseBody</a> <a href="Agda-Syntax-Abstract.html#t:RHS">RHS</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> <a href="Agda-Syntax-Internal.html#t:Level">Level</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> <a href="Agda-Syntax-Abstract.html#t:Telescope">Telescope</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> <a href="Agda-Syntax-Internal.html#t:Elim">Elim</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> <a href="Agda-TypeChecking-Monad-Base.html#t:DisplayTerm">DisplayTerm</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:NamedClause">NamedClause</a> <a href="Agda-Syntax-Abstract.html#t:Clause">Clause</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> <a href="Agda-TypeChecking-Monad-Base.html#t:ProblemConstraint">ProblemConstraint</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Closure">Closure</a> (<a href="Agda-Interaction-BasicOps.html#t:OutputForm">OutputForm</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a>))</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Constraint">Constraint</a> (<a href="Agda-Interaction-BasicOps.html#t:OutputConstraint">OutputConstraint</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a>)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> i a => <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> [i] [a]</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:ReifyWhen">ReifyWhen</a> i a => <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> i) (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc"><p>Skip reification of implicit and irrelevant args if option is off.
</p></td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> i a => <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> i) (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Free.html#t:Free">Free</a> i, <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> i a) => <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> (<a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> i) (<a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a>, a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> i1 a1, <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> i2 a2) => <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> (i1, i2) (a1, a2)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> i a => <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> n i) (<a href="Agda-Syntax-Common.html#t:Named">Named</a> n a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> t t', <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> a a') => <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Judgement">Judgement</a> t a) (<a href="Agda-TypeChecking-Monad-Base.html#t:Judgement">Judgement</a> t' a')</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">class</span> <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> i a => <a name="t:ReifyWhen" class="def">ReifyWhen</a> i a <span class="keyword">where</span><a href="src/Agda-Syntax-Translation-InternalToAbstract.html#ReifyWhen" class="link">Source</a></p><div class="doc"><p><code>ReifyWhen</code> is a auxiliary type class to reify <code><a href="Agda-Syntax-Common.html#t:Arg">Arg</a></code>.
</p><p><code>reifyWhen False</code> should produce an <code>underscore</code>.
This function serves to reify hidden/irrelevant things.
</p></div><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:reifyWhen" class="def">reifyWhen</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a> -> i -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a<a href="src/Agda-Syntax-Translation-InternalToAbstract.html#reifyWhen" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:ReifyWhen" class="caption collapser" onclick="toggleSection('i:ReifyWhen')">Instances</p><div id="section.i:ReifyWhen" class="show"><table><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> i <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a> => <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:ReifyWhen">ReifyWhen</a> i <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:ReifyWhen">ReifyWhen</a> i a => <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:ReifyWhen">ReifyWhen</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> i) (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:ReifyWhen">ReifyWhen</a> i a => <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:ReifyWhen">ReifyWhen</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> n i) (<a href="Agda-Syntax-Common.html#t:Named">Named</a> n a)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:NamedClause" class="def">NamedClause</a> = <a href="Agda-Syntax-Abstract-Name.html#t:QNamed">QNamed</a> <a href="Agda-Syntax-Internal.html#t:Clause">Clause</a><a href="src/Agda-Syntax-Translation-InternalToAbstract.html#NamedClause" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:reifyPatterns" class="def">reifyPatterns</a> :: <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Pattern">Pattern</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Abstract.html#t:Pattern">Pattern</a>]<a href="src/Agda-Syntax-Translation-InternalToAbstract.html#reifyPatterns" class="link">Source</a></p></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.11.0</p></div></body></html>
