<!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.Concrete.Operators</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-Concrete-Operators.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Syntax-Concrete-Operators.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.Concrete.Operators</p></div><div id="description"><p class="caption">Description</p><div class="doc"><p>The parser doesn't know about operators and parses everything as normal
function application. This module contains the functions that parses the
operators properly. For a stand-alone implementation of this see
<code>src/prototyping/mixfix/old</code>.
</p><p>It also contains the function that puts parenthesis back given the
precedence of the context.
</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:parseApplication">parseApplication</a> :: [<a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>] -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></li><li class="src short"><a href="#v:parseLHS">parseLHS</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Concrete.html#t:LHSCore">LHSCore</a></li><li class="src short"><a href="#v:parsePattern">parsePattern</a> :: <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a></li><li class="src short"><a href="#v:parsePatternSyn">parsePatternSyn</a> :: <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a></li><li class="src short"><a href="#v:paren">paren</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Monad">Monad</a> m => (<a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> m <a href="Agda-Syntax-Fixity.html#t:Fixity">Fixity</a>) -> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> -> m (<a href="Agda-Syntax-Fixity.html#t:Precedence">Precedence</a> -> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>)</li><li class="src short"><a href="#v:mparen">mparen</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a> -> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> -> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></li><li class="src short"><a href="#v:validConPattern">validConPattern</a> :: [<a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a>] -> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:patternAppView">patternAppView</a> :: <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> [<a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>]</li><li class="src short"><a href="#v:fullParen">fullParen</a> :: <a href="Agda-Syntax-Concrete-Operators-Parser.html#t:IsExpr">IsExpr</a> e => e -> e</li><li class="src short"><a href="#v:buildParser">buildParser</a> :: <span class="keyword">forall</span> e. <a href="Agda-Syntax-Concrete-Operators-Parser.html#t:IsExpr">IsExpr</a> e => <a href="Agda-Syntax-Position.html#t:Range">Range</a> -> FlatScope -> <a href="Agda-Syntax-Concrete-Operators.html#t:UseBoundNames">UseBoundNames</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> (<a href="Agda-Utils-ReadP.html#t:ReadP">ReadP</a> e e)</li><li class="src short"><a href="#v:parsePat">parsePat</a> :: <a href="Agda-Utils-ReadP.html#t:ReadP">ReadP</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> [<a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>]</li><li class="src short"><a href="#v:getDefinedNames">getDefinedNames</a> :: [<a href="Agda-Syntax-Scope-Base.html#t:KindOfName">KindOfName</a>] -> FlatScope -> [(<a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a>, <a href="Agda-Syntax-Fixity.html#t:Fixity-39-">Fixity'</a>)]</li><li class="src short"><span class="keyword">data</span> <a href="#t:UseBoundNames">UseBoundNames</a> <ul class="subs"><li>= <a href="#v:UseBoundNames">UseBoundNames</a> </li><li>| <a href="#v:DontUseBoundNames">DontUseBoundNames</a> </li></ul></li><li class="src short"><a href="#v:qualifierModules">qualifierModules</a> :: [<a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a>] -> [[<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>]]</li><li class="src short"><a href="#v:patternQNames">patternQNames</a> :: <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> [<a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a>]</li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><a name="v:parseApplication" class="def">parseApplication</a> :: [<a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>] -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a><a href="src/Agda-Syntax-Concrete-Operators.html#parseApplication" class="link">Source</a></p><div class="doc"><p>Parse a list of expressions into an application.
</p></div></div><div class="top"><p class="src"><a name="v:parseLHS" class="def">parseLHS</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Concrete.html#t:LHSCore">LHSCore</a><a href="src/Agda-Syntax-Concrete-Operators.html#parseLHS" class="link">Source</a></p><div class="doc"><p>Parses a left-hand side, and makes sure that it defined the expected name.
TODO: check the arities of constructors. There is a possible ambiguity with
postfix constructors:
Assume _ * is a constructor. Then 'true *' can be parsed as either the
intended _* applied to true, or as true applied to a variable *. If we
check arities this problem won't appear.
</p></div></div><div class="top"><p class="src"><a name="v:parsePattern" class="def">parsePattern</a> :: <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a><a href="src/Agda-Syntax-Concrete-Operators.html#parsePattern" class="link">Source</a></p><div class="doc"><p>Parses a pattern.
TODO: check the arities of constructors. There is a possible ambiguity with
postfix constructors:
Assume _ * is a constructor. Then 'true *' can be parsed as either the
intended _* applied to true, or as true applied to a variable *. If we
check arities this problem won't appear.
</p></div></div><div class="top"><p class="src"><a name="v:parsePatternSyn" class="def">parsePatternSyn</a> :: <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a><a href="src/Agda-Syntax-Concrete-Operators.html#parsePatternSyn" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:paren" class="def">paren</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Monad">Monad</a> m => (<a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> m <a href="Agda-Syntax-Fixity.html#t:Fixity">Fixity</a>) -> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> -> m (<a href="Agda-Syntax-Fixity.html#t:Precedence">Precedence</a> -> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>)<a href="src/Agda-Syntax-Concrete-Operators.html#paren" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mparen" class="def">mparen</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a> -> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> -> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a><a href="src/Agda-Syntax-Concrete-Operators.html#mparen" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:validConPattern" class="def">validConPattern</a> :: [<a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a>] -> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-Syntax-Concrete-Operators.html#validConPattern" class="link">Source</a></p><div class="doc"><p>Helper function for <code><a href="Agda-Syntax-Concrete-Operators.html#v:parseLHS">parseLHS</a></code> and <code><a href="Agda-Syntax-Concrete-Operators.html#v:parsePattern">parsePattern</a></code>.
</p></div></div><div class="top"><p class="src"><a name="v:patternAppView" class="def">patternAppView</a> :: <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> [<a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>]<a href="src/Agda-Syntax-Concrete-Operators.html#patternAppView" class="link">Source</a></p><div class="doc"><p>View a pattern <code>p</code> as a list <code>p0 .. pn</code> where <code>p0</code> is the identifier
(in most cases a constructor).
</p><p>Pattern needs to be parsed already (operators resolved).
</p></div></div><div class="top"><p class="src"><a name="v:fullParen" class="def">fullParen</a> :: <a href="Agda-Syntax-Concrete-Operators-Parser.html#t:IsExpr">IsExpr</a> e => e -> e<a href="src/Agda-Syntax-Concrete-Operators.html#fullParen" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:buildParser" class="def">buildParser</a> :: <span class="keyword">forall</span> e. <a href="Agda-Syntax-Concrete-Operators-Parser.html#t:IsExpr">IsExpr</a> e => <a href="Agda-Syntax-Position.html#t:Range">Range</a> -> FlatScope -> <a href="Agda-Syntax-Concrete-Operators.html#t:UseBoundNames">UseBoundNames</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> (<a href="Agda-Utils-ReadP.html#t:ReadP">ReadP</a> e e)<a href="src/Agda-Syntax-Concrete-Operators.html#buildParser" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:parsePat" class="def">parsePat</a> :: <a href="Agda-Utils-ReadP.html#t:ReadP">ReadP</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> [<a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>]<a href="src/Agda-Syntax-Concrete-Operators.html#parsePat" class="link">Source</a></p><div class="doc"><p>Returns the list of possible parses.
</p></div></div><div class="top"><p class="src"><a name="v:getDefinedNames" class="def">getDefinedNames</a> :: [<a href="Agda-Syntax-Scope-Base.html#t:KindOfName">KindOfName</a>] -> FlatScope -> [(<a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a>, <a href="Agda-Syntax-Fixity.html#t:Fixity-39-">Fixity'</a>)]<a href="src/Agda-Syntax-Concrete-Operators.html#getDefinedNames" class="link">Source</a></p><div class="doc"><p>Compute all unqualified defined names in scope and their fixities.
</p></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:UseBoundNames" class="def">UseBoundNames</a> <a href="src/Agda-Syntax-Concrete-Operators.html#UseBoundNames" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:UseBoundNames" class="def">UseBoundNames</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:DontUseBoundNames" class="def">DontUseBoundNames</a></td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><a name="v:qualifierModules" class="def">qualifierModules</a> :: [<a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a>] -> [[<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>]]<a href="src/Agda-Syntax-Concrete-Operators.html#qualifierModules" class="link">Source</a></p><div class="doc"><p>Return all qualifiers occuring in a list of <code><a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></code>s.
Each qualifier is returned as a list of names, e.g.
for <code>Data.Nat._+_</code> we return the list <code>[Data,Nat]</code>.
</p></div></div><div class="top"><p class="src"><a name="v:patternQNames" class="def">patternQNames</a> :: <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> [<a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a>]<a href="src/Agda-Syntax-Concrete-Operators.html#patternQNames" class="link">Source</a></p><div class="doc"><p>Collect all names in a pattern into a list of qualified names.
</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>
