<!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.TypeChecking.CompiledClause</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-TypeChecking-CompiledClause.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-TypeChecking-CompiledClause.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.TypeChecking.CompiledClause</p></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">type</span> <a name="t::-45--62-" class="def">:-></a> key value = <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> key value<a href="src/Agda-TypeChecking-CompiledClause.html#%3A-%3E" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:WithArity" class="def">WithArity</a> c <a href="src/Agda-TypeChecking-CompiledClause.html#WithArity" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:WithArity" class="def">WithArity</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:arity" class="def">arity</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:content" class="def">content</a> :: c</dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:WithArity" class="caption collapser" onclick="toggleSection('i:WithArity')">Instances</p><div id="section.i:WithArity" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Functor">Functor</a> <a href="Agda-TypeChecking-CompiledClause.html#t:WithArity">WithArity</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable1">Typeable1</a> <a href="Agda-TypeChecking-CompiledClause.html#t:WithArity">WithArity</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Foldable.html#t:Foldable">Foldable</a> <a href="Agda-TypeChecking-CompiledClause.html#t:WithArity">WithArity</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Traversable.html#t:Traversable">Traversable</a> <a href="Agda-TypeChecking-CompiledClause.html#t:WithArity">WithArity</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Monoid.html#t:Monoid">Monoid</a> c => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Monoid.html#t:Monoid">Monoid</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:WithArity">WithArity</a> c)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> a => <a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:WithArity">WithArity</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:WithArity">WithArity</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:WithArity">WithArity</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Reduce.html#t:InstantiateFull">InstantiateFull</a> a => <a href="Agda-TypeChecking-Reduce.html#t:InstantiateFull">InstantiateFull</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:WithArity">WithArity</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:WithArity">WithArity</a> a)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Case" class="def">Case</a> c <a href="src/Agda-TypeChecking-CompiledClause.html#Case" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Branches" class="def">Branches</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:conBranches" class="def">conBranches</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> <a href="Agda-TypeChecking-CompiledClause.html#t::-45--62-">:-></a> <a href="Agda-TypeChecking-CompiledClause.html#t:WithArity">WithArity</a> c</dt><dd class="doc"><p>Map from constructor names to their arity and the case subtree
</p></dd><dt class="src"><a name="v:litBranches" class="def">litBranches</a> :: <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a> <a href="Agda-TypeChecking-CompiledClause.html#t::-45--62-">:-></a> c</dt><dd class="doc"><p>Map from literal to case subtree
</p></dd><dt class="src"><a name="v:catchAllBranch" class="def">catchAllBranch</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> c</dt><dd class="doc"><p>(Possibly additional) catch-all clause
</p></dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:Case" class="caption collapser" onclick="toggleSection('i:Case')">Instances</p><div id="section.i:Case" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Functor">Functor</a> <a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable1">Typeable1</a> <a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Foldable.html#t:Foldable">Foldable</a> <a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Traversable.html#t:Traversable">Traversable</a> <a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> a => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Monoid.html#t:Monoid">Monoid</a> m => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Monoid.html#t:Monoid">Monoid</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> m)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> a => <a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Reduce.html#t:InstantiateFull">InstantiateFull</a> a => <a href="Agda-TypeChecking-Reduce.html#t:InstantiateFull">InstantiateFull</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> a)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:CompiledClauses" class="def">CompiledClauses</a> <a href="src/Agda-TypeChecking-CompiledClause.html#CompiledClauses" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Case" class="def">Case</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a>)</td><td class="doc"><p><code>Case n bs</code> stands for a match on the <code>n</code>-th argument
(counting from zero) with <code>bs</code> as the case branches.
</p></td></tr><tr><td class="src"><a name="v:Done" class="def">Done</a> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>] <a href="Agda-Syntax-Internal.html#t:Term">Term</a></td><td class="doc"><p><code>Done xs b</code> stands for the body <code>b</code> where the <code>xs</code> contains hiding
and name suggestions for the free variables. This is needed to build
lambdas on the right hand side for partial applications which can
still reduce.
</p></td></tr><tr><td class="src"><a name="v:Fail" class="def">Fail</a></td><td class="doc"><p>Absurd case.
</p></td></tr></table></div><div class="subs instances"><p id="control.i:CompiledClauses" class="caption collapser" onclick="toggleSection('i:CompiledClauses')">Instances</p><div id="section.i:CompiledClauses" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable">Typeable</a> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-DropArgs.html#t:DropArgs">DropArgs</a> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a></td><td class="doc"><p>To drop the first <code>n</code> arguments in a compiled clause,
we reduce the split argument indices by <code>n</code> and
drop <code>n</code> arguments from the bodies.
NOTE: this only works for non-recursive functions, we
are not dropping arguments to recursive calls in bodies.
</p></td></tr><tr><td class="src"><a href="Agda-TypeChecking-Reduce.html#t:InstantiateFull">InstantiateFull</a> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:emptyBranches" class="def">emptyBranches</a> :: <a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> c<a href="src/Agda-TypeChecking-CompiledClause.html#emptyBranches" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:litCase" class="def">litCase</a> :: <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a> -> c -> <a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> c<a href="src/Agda-TypeChecking-CompiledClause.html#litCase" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:conCase" class="def">conCase</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-CompiledClause.html#t:WithArity">WithArity</a> c -> <a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> c<a href="src/Agda-TypeChecking-CompiledClause.html#conCase" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:catchAll" class="def">catchAll</a> :: c -> <a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> c<a href="src/Agda-TypeChecking-CompiledClause.html#catchAll" 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>
