<!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.Scope.Monad</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-Scope-Monad.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Syntax-Scope-Monad.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.Scope.Monad</p></div><div id="table-of-contents"><p class="caption">Contents</p><ul><li><a href="#g:1">The scope checking monad
</a></li><li><a href="#g:2">Errors
</a></li><li><a href="#g:3">General operations
</a></li><li><a href="#g:4">Names
</a></li><li><a href="#g:5">Resolving names
</a></li><li><a href="#g:6">Binding names
</a></li><li><a href="#g:7">Module manipulation operations
</a></li></ul></div><div id="description"><p class="caption">Description</p><div class="doc"><p>The scope monad with operations.
</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"><span class="keyword">type</span> <a href="#t:ScopeM">ScopeM</a> = <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a></li><li class="src short"><a href="#v:notInScope">notInScope</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a</li><li class="src short"><a href="#v:isDatatypeModule">isDatatypeModule</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</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:getCurrentModule">getCurrentModule</a> :: <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></li><li class="src short"><a href="#v:setCurrentModule">setCurrentModule</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:withCurrentModule">withCurrentModule</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a</li><li class="src short"><a href="#v:withCurrentModule-39-">withCurrentModule'</a> :: (<a href="/usr/share/doc/ghc/html/libraries/transformers-0.3.0.0/Control-Monad-Trans-Class.html#t:MonadTrans">MonadTrans</a> t, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Monad">Monad</a> (t <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a>)) => <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> t <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a -> t <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a</li><li class="src short"><a href="#v:getNamedScope">getNamedScope</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:getCurrentScope">getCurrentScope</a> :: <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:createModule">createModule</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-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:modifyScopeInfo">modifyScopeInfo</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a>) -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:modifyScopes">modifyScopes</a> :: (<a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a>) -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:modifyNamedScope">modifyNamedScope</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> (<a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a>) -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:modifyCurrentScope">modifyCurrentScope</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a>) -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:modifyNamedScopeM">modifyNamedScopeM</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> (<a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a>) -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:modifyCurrentScopeM">modifyCurrentScopeM</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a>) -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:modifyCurrentNameSpace">modifyCurrentNameSpace</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> (<a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a>) -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:setContextPrecedence">setContextPrecedence</a> :: <a href="Agda-Syntax-Fixity.html#t:Precedence">Precedence</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:getContextPrecedence">getContextPrecedence</a> :: <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Fixity.html#t:Precedence">Precedence</a></li><li class="src short"><a href="#v:withContextPrecedence">withContextPrecedence</a> :: <a href="Agda-Syntax-Fixity.html#t:Precedence">Precedence</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a</li><li class="src short"><a href="#v:getLocalVars">getLocalVars</a> :: <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Scope-Base.html#t:LocalVars">LocalVars</a></li><li class="src short"><a href="#v:setLocalVars">setLocalVars</a> :: <a href="Agda-Syntax-Scope-Base.html#t:LocalVars">LocalVars</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:withLocalVars">withLocalVars</a> :: <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a</li><li class="src short"><a href="#v:freshAbstractName">freshAbstractName</a> :: <a href="Agda-Syntax-Fixity.html#t:Fixity-39-">Fixity'</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></li><li class="src short"><a href="#v:freshAbstractName_">freshAbstractName_</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></li><li class="src short"><a href="#v:freshAbstractQName">freshAbstractQName</a> :: <a href="Agda-Syntax-Fixity.html#t:Fixity-39-">Fixity'</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:ResolvedName">ResolvedName</a> <ul class="subs"><li>= <a href="#v:VarName">VarName</a> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a> </li><li>| <a href="#v:DefinedName">DefinedName</a> <a href="Agda-Syntax-Common.html#t:Access">Access</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a> </li><li>| <a href="#v:FieldName">FieldName</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a> </li><li>| <a href="#v:ConstructorName">ConstructorName</a> [<a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a>] </li><li>| <a href="#v:PatternSynResName">PatternSynResName</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a> </li><li>| <a href="#v:UnknownName">UnknownName</a> </li></ul></li><li class="src short"><a href="#v:resolveName">resolveName</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Scope-Monad.html#t:ResolvedName">ResolvedName</a></li><li class="src short"><a href="#v:resolveModule">resolveModule</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">AbstractModule</a></li><li class="src short"><a href="#v:getFixity">getFixity</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Fixity.html#t:Fixity-39-">Fixity'</a></li><li class="src short"><a href="#v:bindVariable">bindVariable</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:bindName">bindName</a> :: <a href="Agda-Syntax-Common.html#t:Access">Access</a> -> <a href="Agda-Syntax-Scope-Base.html#t:KindOfName">KindOfName</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:bindModule">bindModule</a> :: <a href="Agda-Syntax-Common.html#t:Access">Access</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:bindQModule">bindQModule</a> :: <a href="Agda-Syntax-Common.html#t:Access">Access</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:stripNoNames">stripNoNames</a> :: <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><span class="keyword">type</span> <a href="#t:Ren">Ren</a> a = <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> a a</li><li class="src short"><span class="keyword">type</span> <a href="#t:Out">Out</a> = (<a href="Agda-Syntax-Scope-Monad.html#t:Ren">Ren</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a>, <a href="Agda-Syntax-Scope-Monad.html#t:Ren">Ren</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>)</li><li class="src short"><span class="keyword">type</span> <a href="#t:WSM">WSM</a> = <a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-State-Lazy.html#t:StateT">StateT</a> <a href="Agda-Syntax-Scope-Monad.html#t:Out">Out</a> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a></li><li class="src short"><a href="#v:copyScope">copyScope</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> (<a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a>, (<a href="Agda-Syntax-Scope-Monad.html#t:Ren">Ren</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a>, <a href="Agda-Syntax-Scope-Monad.html#t:Ren">Ren</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>))</li><li class="src short"><a href="#v:applyImportDirectiveM">applyImportDirectiveM</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Concrete.html#t:ImportDirective">ImportDirective</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:openModule_">openModule_</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Concrete.html#t:ImportDirective">ImportDirective</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li></ul></div><div id="interface"><h1 id="g:1">The scope checking monad
</h1><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:ScopeM" class="def">ScopeM</a> = <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a><a href="src/Agda-Syntax-Scope-Monad.html#ScopeM" class="link">Source</a></p><div class="doc"><p>To simplify interaction between scope checking and type checking (in
particular when chasing imports), we use the same monad.
</p></div></div><h1 id="g:2">Errors
</h1><div class="top"><p class="src"><a name="v:notInScope" class="def">notInScope</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a<a href="src/Agda-Syntax-Scope-Monad.html#notInScope" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:isDatatypeModule" class="def">isDatatypeModule</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</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-Scope-Monad.html#isDatatypeModule" class="link">Source</a></p></div><h1 id="g:3">General operations
</h1><div class="top"><p class="src"><a name="v:getCurrentModule" class="def">getCurrentModule</a> :: <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a><a href="src/Agda-Syntax-Scope-Monad.html#getCurrentModule" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:setCurrentModule" class="def">setCurrentModule</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#setCurrentModule" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:withCurrentModule" class="def">withCurrentModule</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a<a href="src/Agda-Syntax-Scope-Monad.html#withCurrentModule" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:withCurrentModule-39-" class="def">withCurrentModule'</a> :: (<a href="/usr/share/doc/ghc/html/libraries/transformers-0.3.0.0/Control-Monad-Trans-Class.html#t:MonadTrans">MonadTrans</a> t, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Monad">Monad</a> (t <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a>)) => <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> t <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a -> t <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a<a href="src/Agda-Syntax-Scope-Monad.html#withCurrentModule%27" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getNamedScope" class="def">getNamedScope</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Monad.html#getNamedScope" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getCurrentScope" class="def">getCurrentScope</a> :: <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Monad.html#getCurrentScope" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:createModule" class="def">createModule</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-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#createModule" class="link">Source</a></p><div class="doc"><p>Create a new module with an empty scope (Bool is True if it is a datatype module)
</p></div></div><div class="top"><p class="src"><a name="v:modifyScopeInfo" class="def">modifyScopeInfo</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a>) -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#modifyScopeInfo" class="link">Source</a></p><div class="doc"><p>Apply a function to the scope info.
</p></div></div><div class="top"><p class="src"><a name="v:modifyScopes" class="def">modifyScopes</a> :: (<a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a>) -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#modifyScopes" class="link">Source</a></p><div class="doc"><p>Apply a function to the scope map.
</p></div></div><div class="top"><p class="src"><a name="v:modifyNamedScope" class="def">modifyNamedScope</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> (<a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a>) -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#modifyNamedScope" class="link">Source</a></p><div class="doc"><p>Apply a function to the given scope.
</p></div></div><div class="top"><p class="src"><a name="v:modifyCurrentScope" class="def">modifyCurrentScope</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a>) -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#modifyCurrentScope" class="link">Source</a></p><div class="doc"><p>Apply a function to the current scope.
</p></div></div><div class="top"><p class="src"><a name="v:modifyNamedScopeM" class="def">modifyNamedScopeM</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> (<a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a>) -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#modifyNamedScopeM" class="link">Source</a></p><div class="doc"><p>Apply a monadic function to the top scope.
</p></div></div><div class="top"><p class="src"><a name="v:modifyCurrentScopeM" class="def">modifyCurrentScopeM</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a>) -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#modifyCurrentScopeM" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:modifyCurrentNameSpace" class="def">modifyCurrentNameSpace</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> (<a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a>) -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#modifyCurrentNameSpace" class="link">Source</a></p><div class="doc"><p>Apply a function to the public or private name space.
</p></div></div><div class="top"><p class="src"><a name="v:setContextPrecedence" class="def">setContextPrecedence</a> :: <a href="Agda-Syntax-Fixity.html#t:Precedence">Precedence</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#setContextPrecedence" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getContextPrecedence" class="def">getContextPrecedence</a> :: <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Fixity.html#t:Precedence">Precedence</a><a href="src/Agda-Syntax-Scope-Monad.html#getContextPrecedence" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:withContextPrecedence" class="def">withContextPrecedence</a> :: <a href="Agda-Syntax-Fixity.html#t:Precedence">Precedence</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a<a href="src/Agda-Syntax-Scope-Monad.html#withContextPrecedence" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getLocalVars" class="def">getLocalVars</a> :: <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Scope-Base.html#t:LocalVars">LocalVars</a><a href="src/Agda-Syntax-Scope-Monad.html#getLocalVars" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:setLocalVars" class="def">setLocalVars</a> :: <a href="Agda-Syntax-Scope-Base.html#t:LocalVars">LocalVars</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#setLocalVars" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:withLocalVars" class="def">withLocalVars</a> :: <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a<a href="src/Agda-Syntax-Scope-Monad.html#withLocalVars" class="link">Source</a></p><div class="doc"><p>Run a computation without changing the local variables.
</p></div></div><h1 id="g:4">Names
</h1><div class="top"><p class="src"><a name="v:freshAbstractName" class="def">freshAbstractName</a> :: <a href="Agda-Syntax-Fixity.html#t:Fixity-39-">Fixity'</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a><a href="src/Agda-Syntax-Scope-Monad.html#freshAbstractName" class="link">Source</a></p><div class="doc"><p>Create a fresh abstract name from a concrete name.
</p></div></div><div class="top"><p class="src"><a name="v:freshAbstractName_" class="def">freshAbstractName_</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a><a href="src/Agda-Syntax-Scope-Monad.html#freshAbstractName_" class="link">Source</a></p><div class="doc"><pre>freshAbstractName_ = freshAbstractName defaultFixity</pre></div></div><div class="top"><p class="src"><a name="v:freshAbstractQName" class="def">freshAbstractQName</a> :: <a href="Agda-Syntax-Fixity.html#t:Fixity-39-">Fixity'</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a><a href="src/Agda-Syntax-Scope-Monad.html#freshAbstractQName" class="link">Source</a></p><div class="doc"><p>Create a fresh abstract qualified name.
</p></div></div><h1 id="g:5">Resolving names
</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:ResolvedName" class="def">ResolvedName</a> <a href="src/Agda-Syntax-Scope-Monad.html#ResolvedName" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:VarName" class="def">VarName</a> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:DefinedName" class="def">DefinedName</a> <a href="Agda-Syntax-Common.html#t:Access">Access</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:FieldName" class="def">FieldName</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a></td><td class="doc"><p>record fields names need to be distinguished to parse copatterns
</p></td></tr><tr><td class="src"><a name="v:ConstructorName" class="def">ConstructorName</a> [<a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:PatternSynResName" class="def">PatternSynResName</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:UnknownName" class="def">UnknownName</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:ResolvedName" class="caption collapser" onclick="toggleSection('i:ResolvedName')">Instances</p><div id="section.i:ResolvedName" 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-Syntax-Scope-Monad.html#t:ResolvedName">ResolvedName</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:resolveName" class="def">resolveName</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Scope-Monad.html#t:ResolvedName">ResolvedName</a><a href="src/Agda-Syntax-Scope-Monad.html#resolveName" class="link">Source</a></p><div class="doc"><p>Look up the abstract name referred to by a given concrete name.
</p></div></div><div class="top"><p class="src"><a name="v:resolveModule" class="def">resolveModule</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">AbstractModule</a><a href="src/Agda-Syntax-Scope-Monad.html#resolveModule" class="link">Source</a></p><div class="doc"><p>Look up a module in the scope.
</p></div></div><div class="top"><p class="src"><a name="v:getFixity" class="def">getFixity</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Fixity.html#t:Fixity-39-">Fixity'</a><a href="src/Agda-Syntax-Scope-Monad.html#getFixity" class="link">Source</a></p><div class="doc"><p>Get the fixity of a name. The name is assumed to be in scope.
</p></div></div><h1 id="g:6">Binding names
</h1><div class="top"><p class="src"><a name="v:bindVariable" class="def">bindVariable</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#bindVariable" class="link">Source</a></p><div class="doc"><p>Bind a variable. The abstract name is supplied as the second argument.
</p></div></div><div class="top"><p class="src"><a name="v:bindName" class="def">bindName</a> :: <a href="Agda-Syntax-Common.html#t:Access">Access</a> -> <a href="Agda-Syntax-Scope-Base.html#t:KindOfName">KindOfName</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#bindName" class="link">Source</a></p><div class="doc"><p>Bind a defined name. Must not shadow anything.
</p></div></div><div class="top"><p class="src"><a name="v:bindModule" class="def">bindModule</a> :: <a href="Agda-Syntax-Common.html#t:Access">Access</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#bindModule" class="link">Source</a></p><div class="doc"><p>Bind a module name.
</p></div></div><div class="top"><p class="src"><a name="v:bindQModule" class="def">bindQModule</a> :: <a href="Agda-Syntax-Common.html#t:Access">Access</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#bindQModule" class="link">Source</a></p><div class="doc"><p>Bind a qualified module name. Adds it to the imports field of the scope.
</p></div></div><h1 id="g:7">Module manipulation operations
</h1><div class="top"><p class="src"><a name="v:stripNoNames" class="def">stripNoNames</a> :: <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#stripNoNames" class="link">Source</a></p><div class="doc"><p>Clear the scope of any no names.
</p></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Ren" class="def">Ren</a> a = <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> a a<a href="src/Agda-Syntax-Scope-Monad.html#Ren" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Out" class="def">Out</a> = (<a href="Agda-Syntax-Scope-Monad.html#t:Ren">Ren</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a>, <a href="Agda-Syntax-Scope-Monad.html#t:Ren">Ren</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>)<a href="src/Agda-Syntax-Scope-Monad.html#Out" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:WSM" class="def">WSM</a> = <a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-State-Lazy.html#t:StateT">StateT</a> <a href="Agda-Syntax-Scope-Monad.html#t:Out">Out</a> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a><a href="src/Agda-Syntax-Scope-Monad.html#WSM" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:copyScope" class="def">copyScope</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> (<a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a>, (<a href="Agda-Syntax-Scope-Monad.html#t:Ren">Ren</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a>, <a href="Agda-Syntax-Scope-Monad.html#t:Ren">Ren</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>))<a href="src/Agda-Syntax-Scope-Monad.html#copyScope" class="link">Source</a></p><div class="doc"><p>Create a new scope with the given name from an old scope. Renames
public names in the old scope to match the new name and returns the
renamings.
</p></div></div><div class="top"><p class="src"><a name="v:applyImportDirectiveM" class="def">applyImportDirectiveM</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Concrete.html#t:ImportDirective">ImportDirective</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Monad.html#applyImportDirectiveM" class="link">Source</a></p><div class="doc"><p>Apply an importdirective and check that all the names mentioned actually
exist.
</p></div></div><div class="top"><p class="src"><a name="v:openModule_" class="def">openModule_</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Concrete.html#t:ImportDirective">ImportDirective</a> -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Syntax-Scope-Monad.html#openModule_" class="link">Source</a></p><div class="doc"><p>Open a module.
</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>
