<!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.Compiler.JS.Compiler</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-Compiler-JS-Compiler.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Compiler-JS-Compiler.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.Compiler.JS.Compiler</p></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><a name="v:compilerMain" class="def">compilerMain</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Interface">Interface</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-Compiler-JS-Compiler.html#compilerMain" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:compile" class="def">compile</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Interface">Interface</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-Compiler-JS-Compiler.html#compile" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:prefix" class="def">prefix</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Char.html#t:Char">Char</a>]<a href="src/Agda-Compiler-JS-Compiler.html#prefix" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:jsMod" class="def">jsMod</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Compiler-JS-Syntax.html#t:GlobalId">GlobalId</a><a href="src/Agda-Compiler-JS-Compiler.html#jsMod" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:jsFileName" class="def">jsFileName</a> :: <a href="Agda-Compiler-JS-Syntax.html#t:GlobalId">GlobalId</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a><a href="src/Agda-Compiler-JS-Compiler.html#jsFileName" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:jsMember" class="def">jsMember</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a> -> <a href="Agda-Compiler-JS-Syntax.html#t:MemberId">MemberId</a><a href="src/Agda-Compiler-JS-Compiler.html#jsMember" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:global-39-" class="def">global'</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-Compiler-JS-Syntax.html#t:Exp">Exp</a>, [<a href="Agda-Compiler-JS-Syntax.html#t:MemberId">MemberId</a>])<a href="src/Agda-Compiler-JS-Compiler.html#global%27" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:global" class="def">global</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-Compiler-JS-Syntax.html#t:Exp">Exp</a>, [<a href="Agda-Compiler-JS-Syntax.html#t:MemberId">MemberId</a>])<a href="src/Agda-Compiler-JS-Compiler.html#global" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:reorder" class="def">reorder</a> :: [<a href="Agda-Compiler-JS-Syntax.html#t:Export">Export</a>] -> [<a href="Agda-Compiler-JS-Syntax.html#t:Export">Export</a>]<a href="src/Agda-Compiler-JS-Compiler.html#reorder" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:reorder-39-" class="def">reorder'</a> :: <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Set.html#t:Set">Set</a> [<a href="Agda-Compiler-JS-Syntax.html#t:MemberId">MemberId</a>] -> [<a href="Agda-Compiler-JS-Syntax.html#t:Export">Export</a>] -> [<a href="Agda-Compiler-JS-Syntax.html#t:Export">Export</a>]<a href="src/Agda-Compiler-JS-Compiler.html#reorder%27" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:isTopLevelValue" class="def">isTopLevelValue</a> :: <a href="Agda-Compiler-JS-Syntax.html#t:Export">Export</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-Compiler-JS-Compiler.html#isTopLevelValue" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:isEmptyObject" class="def">isEmptyObject</a> :: <a href="Agda-Compiler-JS-Syntax.html#t:Export">Export</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-Compiler-JS-Compiler.html#isEmptyObject" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:insertAfter" class="def">insertAfter</a> :: <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Set.html#t:Set">Set</a> [<a href="Agda-Compiler-JS-Syntax.html#t:MemberId">MemberId</a>] -> <a href="Agda-Compiler-JS-Syntax.html#t:Export">Export</a> -> [<a href="Agda-Compiler-JS-Syntax.html#t:Export">Export</a>] -> [<a href="Agda-Compiler-JS-Syntax.html#t:Export">Export</a>]<a href="src/Agda-Compiler-JS-Compiler.html#insertAfter" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:curModule" class="def">curModule</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Compiler-JS-Syntax.html#t:Module">Module</a><a href="src/Agda-Compiler-JS-Compiler.html#curModule" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:definition" class="def">definition</a> :: (<a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>, <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Compiler-JS-Syntax.html#t:Export">Export</a><a href="src/Agda-Compiler-JS-Compiler.html#definition" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:defn" class="def">defn</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> [<a href="Agda-Compiler-JS-Syntax.html#t:MemberId">MemberId</a>] -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-TypeChecking-Monad-Base.html#t:JSCode">JSCode</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Defn">Defn</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Compiler-JS-Syntax.html#t:Exp">Exp</a><a href="src/Agda-Compiler-JS-Compiler.html#defn" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:numPars" class="def">numPars</a> :: [<a href="Agda-Syntax-Internal.html#t:Clause">Clause</a>] -> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a><a href="src/Agda-Compiler-JS-Compiler.html#numPars" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:clause" class="def">clause</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-Compiler-JS-Case.html#t:Case">Case</a><a href="src/Agda-Compiler-JS-Compiler.html#clause" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mapping" class="def">mapping</a> :: [<a href="Agda-Syntax-Internal.html#t:Pattern">Pattern</a>] -> (<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>, <a href="Agda-Syntax-Common.html#t:Nat">Nat</a>, [<a href="Agda-Compiler-JS-Syntax.html#t:Exp">Exp</a>])<a href="src/Agda-Compiler-JS-Compiler.html#mapping" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mapping-39-" class="def">mapping'</a> :: <a href="Agda-Syntax-Internal.html#t:Pattern">Pattern</a> -> (<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>, <a href="Agda-Syntax-Common.html#t:Nat">Nat</a>, [<a href="Agda-Compiler-JS-Syntax.html#t:Exp">Exp</a>]) -> (<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>, <a href="Agda-Syntax-Common.html#t:Nat">Nat</a>, [<a href="Agda-Compiler-JS-Syntax.html#t:Exp">Exp</a>])<a href="src/Agda-Compiler-JS-Compiler.html#mapping%27" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:pattern" class="def">pattern</a> :: <a href="Agda-Syntax-Internal.html#t:Pattern">Pattern</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Compiler-JS-Case.html#t:Patt">Patt</a><a href="src/Agda-Compiler-JS-Compiler.html#pattern" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:tag" class="def">tag</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Compiler-JS-Case.html#t:Tag">Tag</a><a href="src/Agda-Compiler-JS-Compiler.html#tag" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:visitorName" class="def">visitorName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Compiler-JS-Syntax.html#t:MemberId">MemberId</a><a href="src/Agda-Compiler-JS-Compiler.html#visitorName" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:body" class="def">body</a> :: <a href="Agda-Syntax-Internal.html#t:ClauseBody">ClauseBody</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Compiler-JS-Syntax.html#t:Exp">Exp</a><a href="src/Agda-Compiler-JS-Compiler.html#body" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:term" class="def">term</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Compiler-JS-Syntax.html#t:Exp">Exp</a><a href="src/Agda-Compiler-JS-Compiler.html#term" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:isSingleton" class="def">isSingleton</a> :: <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-Compiler-JS-Syntax.html#t:Exp">Exp</a>)<a href="src/Agda-Compiler-JS-Compiler.html#isSingleton" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:defProjection" class="def">defProjection</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</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="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a>)<a href="src/Agda-Compiler-JS-Compiler.html#defProjection" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:args" class="def">args</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="/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:Args">Args</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-Compiler-JS-Syntax.html#t:Exp">Exp</a>]<a href="src/Agda-Compiler-JS-Compiler.html#args" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:qname" class="def">qname</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Compiler-JS-Syntax.html#t:Exp">Exp</a><a href="src/Agda-Compiler-JS-Compiler.html#qname" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:literal" class="def">literal</a> :: <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a> -> <a href="Agda-Compiler-JS-Syntax.html#t:Exp">Exp</a><a href="src/Agda-Compiler-JS-Compiler.html#literal" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:dummyLambda" class="def">dummyLambda</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-Compiler-JS-Syntax.html#t:Exp">Exp</a> -> <a href="Agda-Compiler-JS-Syntax.html#t:Exp">Exp</a><a href="src/Agda-Compiler-JS-Compiler.html#dummyLambda" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:writeModule" class="def">writeModule</a> :: <a href="Agda-Compiler-JS-Syntax.html#t:Module">Module</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-Compiler-JS-Compiler.html#writeModule" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:compileDir" class="def">compileDir</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a><a href="src/Agda-Compiler-JS-Compiler.html#compileDir" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:outFile" class="def">outFile</a> :: <a href="Agda-Compiler-JS-Syntax.html#t:GlobalId">GlobalId</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a><a href="src/Agda-Compiler-JS-Compiler.html#outFile" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:outFile_" class="def">outFile_</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a><a href="src/Agda-Compiler-JS-Compiler.html#outFile_" 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>
