<!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.Parser.Lexer</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-Parser-Lexer.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Syntax-Parser-Lexer.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.Parser.Lexer</p></div><div id="table-of-contents"><p class="caption">Contents</p><ul><li><a href="#g:1">The main function
</a></li><li><a href="#g:2">Lex states
</a></li><li><a href="#g:3">Alex generated functions
</a></li></ul></div><div id="description"><p class="caption">Description</p><div class="doc"><p>The lexer is generated by Alex (<a href="http://www.haskell.org/alex">http://www.haskell.org/alex</a>) and is an
adaptation of GHC's lexer. The main lexing function <code><a href="Agda-Syntax-Parser-Lexer.html#v:lexer">lexer</a></code> is called by
the <a href="Agda-Syntax-Parser-Parser.html">Agda.Syntax.Parser.Parser</a> to get the next token from the input.
</p></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"><a href="#v:lexer">lexer</a> :: (<a href="Agda-Syntax-Parser-Tokens.html#t:Token">Token</a> -> <a href="Agda-Syntax-Parser-Monad.html#t:Parser">Parser</a> a) -> <a href="Agda-Syntax-Parser-Monad.html#t:Parser">Parser</a> a</li><li class="src short"><a href="#v:normal">normal</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a></li><li class="src short"><a href="#v:literate">literate</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a></li><li class="src short"><a href="#v:code">code</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:layout">layout</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a></li><li class="src short"><a href="#v:empty_layout">empty_layout</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a></li><li class="src short"><a href="#v:bol">bol</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a></li><li class="src short"><a href="#v:imp_dir">imp_dir</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:AlexReturn">AlexReturn</a> a<ul class="subs"><li>= <a href="#v:AlexEOF">AlexEOF</a> </li><li>| <a href="#v:AlexError">AlexError</a> !<a href="Agda-Syntax-Parser-Alex.html#t:AlexInput">AlexInput</a> </li><li>| <a href="#v:AlexSkip">AlexSkip</a> !<a href="Agda-Syntax-Parser-Alex.html#t:AlexInput">AlexInput</a> !<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> </li><li>| <a href="#v:AlexToken">AlexToken</a> !<a href="Agda-Syntax-Parser-Alex.html#t:AlexInput">AlexInput</a> !<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> a </li></ul></li><li class="src short"><a href="#v:alexScanUser">alexScanUser</a> :: ([<a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a>], <a href="Agda-Syntax-Parser-Monad.html#t:ParseFlags">ParseFlags</a>) -> <a href="Agda-Syntax-Parser-Alex.html#t:AlexInput">AlexInput</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-Parser-Lexer.html#t:AlexReturn">AlexReturn</a> (<a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> <a href="Agda-Syntax-Parser-Tokens.html#t:Token">Token</a>)</li></ul></div><div id="interface"><h1 id="g:1">The main function
</h1><div class="top"><p class="src"><a name="v:lexer" class="def">lexer</a> :: (<a href="Agda-Syntax-Parser-Tokens.html#t:Token">Token</a> -> <a href="Agda-Syntax-Parser-Monad.html#t:Parser">Parser</a> a) -> <a href="Agda-Syntax-Parser-Monad.html#t:Parser">Parser</a> a<a href="src/Agda-Syntax-Parser-Lexer.html#lexer" class="link">Source</a></p><div class="doc"><p>Return the next token. This is the function used by Happy in the parser.
</p><pre>lexer k = <code><a href="Agda-Syntax-Parser-LexActions.html#v:lexToken">lexToken</a></code> >>= k</pre></div></div><h1 id="g:2">Lex states
</h1><div class="top"><p class="src"><a name="v:normal" class="def">normal</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a><a href="src/Agda-Syntax-Parser-Lexer.html#normal" class="link">Source</a></p><div class="doc"><p>This is the initial state for parsing a regular, non-literate file.
</p></div></div><div class="top"><p class="src"><a name="v:literate" class="def">literate</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a><a href="src/Agda-Syntax-Parser-Lexer.html#literate" class="link">Source</a></p><div class="doc"><p>This is the initial state for parsing a literate file. Code blocks
should be enclosed in <code>\begin{code}</code> <code>\end{code}</code> pairs.
</p></div></div><div class="top"><p class="src"><a name="v:code" class="def">code</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-Syntax-Parser-Lexer.html#code" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:layout" class="def">layout</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a><a href="src/Agda-Syntax-Parser-Lexer.html#layout" class="link">Source</a></p><div class="doc"><p>The layout state. Entered when we see a layout keyword (<code><a href="Agda-Syntax-Parser-LexActions.html#v:withLayout">withLayout</a></code>) and
exited either when seeing an open brace (<code>openBrace</code>) or at the next token
(<code><a href="Agda-Syntax-Parser-Layout.html#v:newLayoutContext">newLayoutContext</a></code>).
</p><p>Update: we don't use braces for layout anymore.
</p></div></div><div class="top"><p class="src"><a name="v:empty_layout" class="def">empty_layout</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a><a href="src/Agda-Syntax-Parser-Lexer.html#empty_layout" class="link">Source</a></p><div class="doc"><p>We enter this state from <code><a href="Agda-Syntax-Parser-Layout.html#v:newLayoutContext">newLayoutContext</a></code> when the token following a
layout keyword is to the left of (or at the same column as) the current
layout context. Example:
</p><pre> data Empty : Set where
foo : Empty -> Nat
</pre><p>Here the second line is not part of the <code>where</code> clause since it is has the
same indentation as the <code>data</code> definition. What we have to do is insert an
empty layout block <code>{}</code> after the <code>where</code>. The only thing that can happen
in this state is that <code><a href="Agda-Syntax-Parser-Layout.html#v:emptyLayout">emptyLayout</a></code> is executed, generating the closing
brace. The open brace is generated when entering by <code><a href="Agda-Syntax-Parser-Layout.html#v:newLayoutContext">newLayoutContext</a></code>.
</p></div></div><div class="top"><p class="src"><a name="v:bol" class="def">bol</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a><a href="src/Agda-Syntax-Parser-Lexer.html#bol" class="link">Source</a></p><div class="doc"><p>This state is entered at the beginning of each line. You can't lex
anything in this state, and to exit you have to check the layout rule.
Done with <code><a href="Agda-Syntax-Parser-Layout.html#v:offsideRule">offsideRule</a></code>.
</p></div></div><div class="top"><p class="src"><a name="v:imp_dir" class="def">imp_dir</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a><a href="src/Agda-Syntax-Parser-Lexer.html#imp_dir" class="link">Source</a></p><div class="doc"><p>This state can only be entered by the parser. In this state you can only
lex the keywords <code>using</code>, <code>hiding</code>, <code>renaming</code> and <code>to</code>. Moreover they are
only keywords in this particular state. The lexer will never enter this
state by itself, that has to be done in the parser.
</p></div></div><h1 id="g:3">Alex generated functions
</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:AlexReturn" class="def">AlexReturn</a> a <a href="src/Agda-Syntax-Parser-Lexer.html#AlexReturn" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:AlexEOF" class="def">AlexEOF</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:AlexError" class="def">AlexError</a> !<a href="Agda-Syntax-Parser-Alex.html#t:AlexInput">AlexInput</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:AlexSkip" class="def">AlexSkip</a> !<a href="Agda-Syntax-Parser-Alex.html#t:AlexInput">AlexInput</a> !<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:AlexToken" class="def">AlexToken</a> !<a href="Agda-Syntax-Parser-Alex.html#t:AlexInput">AlexInput</a> !<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> a</td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><a name="v:alexScanUser" class="def">alexScanUser</a> :: ([<a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a>], <a href="Agda-Syntax-Parser-Monad.html#t:ParseFlags">ParseFlags</a>) -> <a href="Agda-Syntax-Parser-Alex.html#t:AlexInput">AlexInput</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-Parser-Lexer.html#t:AlexReturn">AlexReturn</a> (<a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> <a href="Agda-Syntax-Parser-Tokens.html#t:Token">Token</a>)<a href="src/Agda-Syntax-Parser-Lexer.html#alexScanUser" class="link">Source</a></p><div class="doc"><p>This is the main lexing function generated by Alex.
</p></div></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>
