<!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.LexActions</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-LexActions.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Syntax-Parser-LexActions.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.LexActions</p></div><div id="table-of-contents"><p class="caption">Contents</p><ul><li><a href="#g:1">Main function
</a></li><li><a href="#g:2">Lex actions
</a><ul><li><a href="#g:3">General actions
</a></li><li><a href="#g:4">Specialized actions
</a></li></ul></li><li><a href="#g:5">Lex predicates
</a></li></ul></div><div id="description"><p class="caption">Description</p><div class="doc"><p>This module contains the building blocks used to construct the lexer.
</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:lexToken">lexToken</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:Parser">Parser</a> <a href="Agda-Syntax-Parser-Tokens.html#t:Token">Token</a></li><li class="src short"><a href="#v:token">token</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-Parser-Monad.html#t:Parser">Parser</a> tok) -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> tok</li><li class="src short"><a href="#v:withInterval">withInterval</a> :: ((<a href="Agda-Syntax-Position.html#t:Interval">Interval</a>, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>) -> tok) -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> tok</li><li class="src short"><a href="#v:withInterval-39-">withInterval'</a> :: (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> a) -> ((<a href="Agda-Syntax-Position.html#t:Interval">Interval</a>, a) -> tok) -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> tok</li><li class="src short"><a href="#v:withInterval_">withInterval_</a> :: (<a href="Agda-Syntax-Position.html#t:Interval">Interval</a> -> r) -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> r</li><li class="src short"><a href="#v:withLayout">withLayout</a> :: <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> r -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> r</li><li class="src short"><a href="#v:begin">begin</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a> -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> <a href="Agda-Syntax-Parser-Tokens.html#t:Token">Token</a></li><li class="src short"><a href="#v:end">end</a> :: <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> <a href="Agda-Syntax-Parser-Tokens.html#t:Token">Token</a></li><li class="src short"><a href="#v:endWith">endWith</a> :: <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> a -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> a</li><li class="src short"><a href="#v:begin_">begin_</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a> -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> <a href="Agda-Syntax-Parser-Tokens.html#t:Token">Token</a></li><li class="src short"><a href="#v:end_">end_</a> :: <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> <a href="Agda-Syntax-Parser-Tokens.html#t:Token">Token</a></li><li class="src short"><a href="#v:lexError">lexError</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-Parser-Monad.html#t:Parser">Parser</a> a</li><li class="src short"><a href="#v:keyword">keyword</a> :: <a href="Agda-Syntax-Parser-Tokens.html#t:Keyword">Keyword</a> -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> <a href="Agda-Syntax-Parser-Tokens.html#t:Token">Token</a></li><li class="src short"><a href="#v:symbol">symbol</a> :: <a href="Agda-Syntax-Parser-Tokens.html#t:Symbol">Symbol</a> -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> <a href="Agda-Syntax-Parser-Tokens.html#t:Token">Token</a></li><li class="src short"><a href="#v:identifier">identifier</a> :: <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> <a href="Agda-Syntax-Parser-Tokens.html#t:Token">Token</a></li><li class="src short"><a href="#v:literal">literal</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Read.html#t:Read">Read</a> a => (<a href="Agda-Syntax-Position.html#t:Range">Range</a> -> a -> <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a>) -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> <a href="Agda-Syntax-Parser-Tokens.html#t:Token">Token</a></li><li class="src short"><a href="#v:followedBy">followedBy</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Char.html#t:Char">Char</a> -> <a href="Agda-Syntax-Parser-Alex.html#t:LexPredicate">LexPredicate</a></li><li class="src short"><a href="#v:eof">eof</a> :: <a href="Agda-Syntax-Parser-Alex.html#t:LexPredicate">LexPredicate</a></li><li class="src short"><a href="#v:inState">inState</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a> -> <a href="Agda-Syntax-Parser-Alex.html#t:LexPredicate">LexPredicate</a></li></ul></div><div id="interface"><h1 id="g:1">Main function
</h1><div class="top"><p class="src"><a name="v:lexToken" class="def">lexToken</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:Parser">Parser</a> <a href="Agda-Syntax-Parser-Tokens.html#t:Token">Token</a><a href="src/Agda-Syntax-Parser-LexActions.html#lexToken" class="link">Source</a></p><div class="doc"><p>Scan the input to find the next token. Calls
<code><a href="Agda-Syntax-Parser-Lexer.html#v:alexScanUser">alexScanUser</a></code>. This is the main lexing function
where all the work happens. The function <code><a href="Agda-Syntax-Parser-Lexer.html#v:lexer">lexer</a></code>,
used by the parser is the continuation version of this function.
</p></div></div><h1 id="g:2">Lex actions
</h1><h2 id="g:3">General actions
</h2><div class="top"><p class="src"><a name="v:token" class="def">token</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-Parser-Monad.html#t:Parser">Parser</a> tok) -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> tok<a href="src/Agda-Syntax-Parser-LexActions.html#token" class="link">Source</a></p><div class="doc"><p>The most general way of parsing a token.
</p></div></div><div class="top"><p class="src"><a name="v:withInterval" class="def">withInterval</a> :: ((<a href="Agda-Syntax-Position.html#t:Interval">Interval</a>, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>) -> tok) -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> tok<a href="src/Agda-Syntax-Parser-LexActions.html#withInterval" class="link">Source</a></p><div class="doc"><p>Parse a token from an <code><a href="Agda-Syntax-Position.html#t:Interval">Interval</a></code> and the lexed string.
</p></div></div><div class="top"><p class="src"><a name="v:withInterval-39-" class="def">withInterval'</a> :: (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> a) -> ((<a href="Agda-Syntax-Position.html#t:Interval">Interval</a>, a) -> tok) -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> tok<a href="src/Agda-Syntax-Parser-LexActions.html#withInterval%27" class="link">Source</a></p><div class="doc"><p>Like <code><a href="Agda-Syntax-Parser-LexActions.html#v:withInterval">withInterval</a></code>, but applies a function to the string.
</p></div></div><div class="top"><p class="src"><a name="v:withInterval_" class="def">withInterval_</a> :: (<a href="Agda-Syntax-Position.html#t:Interval">Interval</a> -> r) -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> r<a href="src/Agda-Syntax-Parser-LexActions.html#withInterval_" class="link">Source</a></p><div class="doc"><p>Return a token without looking at the lexed string.
</p></div></div><div class="top"><p class="src"><a name="v:withLayout" class="def">withLayout</a> :: <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> r -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> r<a href="src/Agda-Syntax-Parser-LexActions.html#withLayout" class="link">Source</a></p><div class="doc"><p>Executed for layout keywords. Enters the <code><a href="Agda-Syntax-Parser-Lexer.html#v:layout">layout</a></code>
state and performs the given action.
</p></div></div><div class="top"><p class="src"><a name="v:begin" class="def">begin</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</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-LexActions.html#begin" class="link">Source</a></p><div class="doc"><p>Enter a new state without consuming any input.
</p></div></div><div class="top"><p class="src"><a name="v:end" class="def">end</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-LexActions.html#end" class="link">Source</a></p><div class="doc"><p>Exit the current state without consuming any input
</p></div></div><div class="top"><p class="src"><a name="v:endWith" class="def">endWith</a> :: <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> a -> <a href="Agda-Syntax-Parser-Alex.html#t:LexAction">LexAction</a> a<a href="src/Agda-Syntax-Parser-LexActions.html#endWith" class="link">Source</a></p><div class="doc"><p>Exit the current state and perform the given action.
</p></div></div><div class="top"><p class="src"><a name="v:begin_" class="def">begin_</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</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-LexActions.html#begin_" class="link">Source</a></p><div class="doc"><p>Enter a new state throwing away the current lexeme.
</p></div></div><div class="top"><p class="src"><a name="v:end_" class="def">end_</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-LexActions.html#end_" class="link">Source</a></p><div class="doc"><p>Exit the current state throwing away the current lexeme.
</p></div></div><div class="top"><p class="src"><a name="v:lexError" class="def">lexError</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-Parser-Monad.html#t:Parser">Parser</a> a<a href="src/Agda-Syntax-Parser-Monad.html#lexError" class="link">Source</a></p><div class="doc"><p>For lexical errors we want to report the current position as the site of
the error, whereas for parse errors the previous position is the one
we're interested in (since this will be the position of the token we just
lexed). This function does <code><a href="Agda-Syntax-Parser-Monad.html#v:parseErrorAt">parseErrorAt</a></code> the current position.
</p></div></div><h2 id="g:4">Specialized actions
</h2><div class="top"><p class="src"><a name="v:keyword" class="def">keyword</a> :: <a href="Agda-Syntax-Parser-Tokens.html#t:Keyword">Keyword</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-LexActions.html#keyword" class="link">Source</a></p><div class="doc"><p>Parse a <code><a href="Agda-Syntax-Parser-Tokens.html#t:Keyword">Keyword</a></code> token, triggers layout for <code><a href="Agda-Syntax-Parser-Tokens.html#v:layoutKeywords">layoutKeywords</a></code>.
</p></div></div><div class="top"><p class="src"><a name="v:symbol" class="def">symbol</a> :: <a href="Agda-Syntax-Parser-Tokens.html#t:Symbol">Symbol</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-LexActions.html#symbol" class="link">Source</a></p><div class="doc"><p>Parse a <code><a href="Agda-Syntax-Parser-Tokens.html#t:Symbol">Symbol</a></code> token.
</p></div></div><div class="top"><p class="src"><a name="v:identifier" class="def">identifier</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-LexActions.html#identifier" class="link">Source</a></p><div class="doc"><p>Parse an identifier. Identifiers can be qualified (see <code><a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></code>).
Example: <code>Foo.Bar.f</code>
</p></div></div><div class="top"><p class="src"><a name="v:literal" class="def">literal</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Read.html#t:Read">Read</a> a => (<a href="Agda-Syntax-Position.html#t:Range">Range</a> -> a -> <a href="Agda-Syntax-Literal.html#t:Literal">Literal</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-LexActions.html#literal" class="link">Source</a></p><div class="doc"><p>Parse a literal.
</p></div></div><h1 id="g:5">Lex predicates
</h1><div class="top"><p class="src"><a name="v:followedBy" class="def">followedBy</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Char.html#t:Char">Char</a> -> <a href="Agda-Syntax-Parser-Alex.html#t:LexPredicate">LexPredicate</a><a href="src/Agda-Syntax-Parser-LexActions.html#followedBy" class="link">Source</a></p><div class="doc"><p>True when the given character is the next character of the input string.
</p></div></div><div class="top"><p class="src"><a name="v:eof" class="def">eof</a> :: <a href="Agda-Syntax-Parser-Alex.html#t:LexPredicate">LexPredicate</a><a href="src/Agda-Syntax-Parser-LexActions.html#eof" class="link">Source</a></p><div class="doc"><p>True if we are at the end of the file.
</p></div></div><div class="top"><p class="src"><a name="v:inState" class="def">inState</a> :: <a href="Agda-Syntax-Parser-Monad.html#t:LexState">LexState</a> -> <a href="Agda-Syntax-Parser-Alex.html#t:LexPredicate">LexPredicate</a><a href="src/Agda-Syntax-Parser-LexActions.html#inState" class="link">Source</a></p><div class="doc"><p>True if the given state appears somewhere on the state stack
</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>
