<!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.Compile</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-Compile.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-TypeChecking-CompiledClause-Compile.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.Compile</p></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"><a href="#v:compileClauses">compileClauses</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>, <a href="Agda-Syntax-Internal.html#t:Type">Type</a>) -> [<a href="Agda-Syntax-Internal.html#t:Clause">Clause</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a></li><li class="src short"><span class="keyword">type</span> <a href="#t:Cl">Cl</a> = ([<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Pattern">Pattern</a>], <a href="Agda-Syntax-Internal.html#t:ClauseBody">ClauseBody</a>)</li><li class="src short"><span class="keyword">type</span> <a href="#t:Cls">Cls</a> = [<a href="Agda-TypeChecking-CompiledClause-Compile.html#t:Cl">Cl</a>]</li><li class="src short"><a href="#v:compileWithSplitTree">compileWithSplitTree</a> :: <a href="Agda-TypeChecking-Coverage-SplitTree.html#t:SplitTree">SplitTree</a> -> <a href="Agda-TypeChecking-CompiledClause-Compile.html#t:Cls">Cls</a> -> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a></li><li class="src short"><a href="#v:compile">compile</a> :: <a href="Agda-TypeChecking-CompiledClause-Compile.html#t:Cls">Cls</a> -> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a></li><li class="src short"><a href="#v:nextSplit">nextSplit</a> :: <a href="Agda-TypeChecking-CompiledClause-Compile.html#t:Cls">Cls</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a></li><li class="src short"><a href="#v:splitOn">splitOn</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-Compile.html#t:Cls">Cls</a> -> <a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> <a href="Agda-TypeChecking-CompiledClause-Compile.html#t:Cls">Cls</a></li><li class="src short"><a href="#v:splitC">splitC</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-Compile.html#t:Cl">Cl</a> -> <a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> <a href="Agda-TypeChecking-CompiledClause-Compile.html#t:Cl">Cl</a></li><li class="src short"><a href="#v:expandCatchAlls">expandCatchAlls</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-Compile.html#t:Cls">Cls</a> -> <a href="Agda-TypeChecking-CompiledClause-Compile.html#t:Cls">Cls</a></li><li class="src short"><a href="#v:substBody">substBody</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:ClauseBody">ClauseBody</a> -> <a href="Agda-Syntax-Internal.html#t:ClauseBody">ClauseBody</a></li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><a name="v:compileClauses" class="def">compileClauses</a><a href="src/Agda-TypeChecking-CompiledClause-Compile.html#compileClauses" class="link">Source</a></p><div class="subs arguments"><p class="caption">Arguments</p><table><tr><td class="src">:: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>, <a href="Agda-Syntax-Internal.html#t:Type">Type</a>)</td><td class="doc"><p>Translate record patterns and coverage check with given type?
</p></td></tr><tr><td class="src">-> [<a href="Agda-Syntax-Internal.html#t:Clause">Clause</a>]</td><td class="doc empty"> </td></tr><tr><td class="src">-> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a></td><td class="doc empty"> </td></tr></table></div><div class="doc"><p>Process function clauses into case tree.
This involves:
1. Coverage checking, generating a split tree.
2. Translation of lhs record patterns into rhs uses of projection.
Update the split tree.
3. Generating a case tree from the split tree.
Phases 1. and 2. are skipped if <code>Nothing</code>.
</p></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Cl" class="def">Cl</a> = ([<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Pattern">Pattern</a>], <a href="Agda-Syntax-Internal.html#t:ClauseBody">ClauseBody</a>)<a href="src/Agda-TypeChecking-CompiledClause-Compile.html#Cl" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Cls" class="def">Cls</a> = [<a href="Agda-TypeChecking-CompiledClause-Compile.html#t:Cl">Cl</a>]<a href="src/Agda-TypeChecking-CompiledClause-Compile.html#Cls" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:compileWithSplitTree" class="def">compileWithSplitTree</a> :: <a href="Agda-TypeChecking-Coverage-SplitTree.html#t:SplitTree">SplitTree</a> -> <a href="Agda-TypeChecking-CompiledClause-Compile.html#t:Cls">Cls</a> -> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a><a href="src/Agda-TypeChecking-CompiledClause-Compile.html#compileWithSplitTree" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:compile" class="def">compile</a> :: <a href="Agda-TypeChecking-CompiledClause-Compile.html#t:Cls">Cls</a> -> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a><a href="src/Agda-TypeChecking-CompiledClause-Compile.html#compile" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:nextSplit" class="def">nextSplit</a> :: <a href="Agda-TypeChecking-CompiledClause-Compile.html#t:Cls">Cls</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a><a href="src/Agda-TypeChecking-CompiledClause-Compile.html#nextSplit" class="link">Source</a></p><div class="doc"><p>Get the index of the next argument we need to split on.
This the number of the first pattern that does a match in the first clause.
</p></div></div><div class="top"><p class="src"><a name="v:splitOn" class="def">splitOn</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-Compile.html#t:Cls">Cls</a> -> <a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> <a href="Agda-TypeChecking-CompiledClause-Compile.html#t:Cls">Cls</a><a href="src/Agda-TypeChecking-CompiledClause-Compile.html#splitOn" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:splitC" class="def">splitC</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-Compile.html#t:Cl">Cl</a> -> <a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> <a href="Agda-TypeChecking-CompiledClause-Compile.html#t:Cl">Cl</a><a href="src/Agda-TypeChecking-CompiledClause-Compile.html#splitC" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:expandCatchAlls" class="def">expandCatchAlls</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-Compile.html#t:Cls">Cls</a> -> <a href="Agda-TypeChecking-CompiledClause-Compile.html#t:Cls">Cls</a><a href="src/Agda-TypeChecking-CompiledClause-Compile.html#expandCatchAlls" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:substBody" class="def">substBody</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:ClauseBody">ClauseBody</a> -> <a href="Agda-Syntax-Internal.html#t:ClauseBody">ClauseBody</a><a href="src/Agda-TypeChecking-CompiledClause-Compile.html#substBody" 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>
