<!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.Epic.Interface</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-Epic-Interface.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Compiler-Epic-Interface.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.Epic.Interface</p></div><div id="description"><p class="caption">Description</p><div class="doc"><p>Epic interface data structure, which is serialisable and stored for each
compiled file
</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:Var">Var</a> = <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:Tag">Tag</a> <ul class="subs"><li>= <a href="#v:Tag">Tag</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:PrimTag">PrimTag</a> <a href="Agda-Compiler-Epic-Interface.html#t:Var">Var</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:Forced">Forced</a> <ul class="subs"><li>= <a href="#v:NotForced">NotForced</a> </li><li>| <a href="#v:Forced">Forced</a> </li></ul></li><li class="src short"><a href="#v:pairwiseFilter">pairwiseFilter</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>] -> [a] -> [a]</li><li class="src short"><a href="#v:notForced">notForced</a> :: <a href="Agda-Compiler-Epic-Interface.html#t:ForcedArgs">ForcedArgs</a> -> [a] -> [a]</li><li class="src short"><a href="#v:forced">forced</a> :: <a href="Agda-Compiler-Epic-Interface.html#t:ForcedArgs">ForcedArgs</a> -> [a] -> [a]</li><li class="src short"><span class="keyword">data</span> <a href="#t:Relevance">Relevance</a> <ul class="subs"><li>= <a href="#v:Irr">Irr</a> </li><li>| <a href="#v:Rel">Rel</a> </li></ul></li><li class="src short"><span class="keyword">type</span> <a href="#t:ForcedArgs">ForcedArgs</a> = [<a href="Agda-Compiler-Epic-Interface.html#t:Forced">Forced</a>]</li><li class="src short"><span class="keyword">type</span> <a href="#t:RelevantArgs">RelevantArgs</a> = [<a href="Agda-Compiler-Epic-Interface.html#t:Relevance">Relevance</a>]</li><li class="src short"><span class="keyword">data</span> <a href="#t:InjectiveFun">InjectiveFun</a> = <a href="#v:InjectiveFun">InjectiveFun</a> {<ul class="subs"><li><a href="#v:injArg">injArg</a> :: <a href="Agda-Syntax-Common.html#t:Nat">Nat</a></li><li><a href="#v:injArity">injArity</a> :: <a href="Agda-Syntax-Common.html#t:Nat">Nat</a></li></ul>}</li><li class="src short"><span class="keyword">data</span> <a href="#t:EInterface">EInterface</a> = <a href="#v:EInterface">EInterface</a> {<ul class="subs"><li><a href="#v:constrTags">constrTags</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:QName">QName</a> <a href="Agda-Compiler-Epic-Interface.html#t:Tag">Tag</a></li><li><a href="#v:definitions">definitions</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-Epic-Interface.html#t:Var">Var</a></li><li><a href="#v:defDelayed">defDelayed</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:QName">QName</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:conArity">conArity</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:QName">QName</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:mainName">mainName</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></li><li><a href="#v:relevantArgs">relevantArgs</a> :: <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Compiler-Epic-Interface.html#t:Var">Var</a> <a href="Agda-Compiler-Epic-Interface.html#t:RelevantArgs">RelevantArgs</a></li><li><a href="#v:forcedArgs">forcedArgs</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:QName">QName</a> <a href="Agda-Compiler-Epic-Interface.html#t:ForcedArgs">ForcedArgs</a></li><li><a href="#v:injectiveFuns">injectiveFuns</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:QName">QName</a> <a href="Agda-Compiler-Epic-Interface.html#t:InjectiveFun">InjectiveFun</a></li></ul>}</li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Var" class="def">Var</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-Epic-Interface.html#Var" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Tag" class="def">Tag</a> <a href="src/Agda-Compiler-Epic-Interface.html#Tag" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Tag" class="def">Tag</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:PrimTag" class="def">PrimTag</a> <a href="Agda-Compiler-Epic-Interface.html#t:Var">Var</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:Tag" class="caption collapser" onclick="toggleSection('i:Tag')">Instances</p><div id="section.i:Tag" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-Compiler-Epic-Interface.html#t:Tag">Tag</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> <a href="Agda-Compiler-Epic-Interface.html#t:Tag">Tag</a></td><td class="doc empty"> </td></tr><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-Compiler-Epic-Interface.html#t:Tag">Tag</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable">Typeable</a> <a href="Agda-Compiler-Epic-Interface.html#t:Tag">Tag</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Compiler-Epic-Interface.html#t:Tag">Tag</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Forced" class="def">Forced</a> <a href="src/Agda-Compiler-Epic-Interface.html#Forced" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:NotForced" class="def">NotForced</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Forced" class="def">Forced</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:Forced" class="caption collapser" onclick="toggleSection('i:Forced')">Instances</p><div id="section.i:Forced" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-Compiler-Epic-Interface.html#t:Forced">Forced</a></td><td class="doc empty"> </td></tr><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-Compiler-Epic-Interface.html#t:Forced">Forced</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable">Typeable</a> <a href="Agda-Compiler-Epic-Interface.html#t:Forced">Forced</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Compiler-Epic-Interface.html#t:Forced">Forced</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:pairwiseFilter" class="def">pairwiseFilter</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>] -> [a] -> [a]<a href="src/Agda-Compiler-Epic-Interface.html#pairwiseFilter" class="link">Source</a></p><div class="doc"><p>Filter a list using a list of Bools specifying what to keep.
</p></div></div><div class="top"><p class="src"><a name="v:notForced" class="def">notForced</a> :: <a href="Agda-Compiler-Epic-Interface.html#t:ForcedArgs">ForcedArgs</a> -> [a] -> [a]<a href="src/Agda-Compiler-Epic-Interface.html#notForced" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:forced" class="def">forced</a> :: <a href="Agda-Compiler-Epic-Interface.html#t:ForcedArgs">ForcedArgs</a> -> [a] -> [a]<a href="src/Agda-Compiler-Epic-Interface.html#forced" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Relevance" class="def">Relevance</a> <a href="src/Agda-Compiler-Epic-Interface.html#Relevance" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Irr" class="def">Irr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Rel" class="def">Rel</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:Relevance" class="caption collapser" onclick="toggleSection('i:Relevance')">Instances</p><div id="section.i:Relevance" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-Compiler-Epic-Interface.html#t:Relevance">Relevance</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> <a href="Agda-Compiler-Epic-Interface.html#t:Relevance">Relevance</a></td><td class="doc empty"> </td></tr><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-Compiler-Epic-Interface.html#t:Relevance">Relevance</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable">Typeable</a> <a href="Agda-Compiler-Epic-Interface.html#t:Relevance">Relevance</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Compiler-Epic-Interface.html#t:Relevance">Relevance</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:ForcedArgs" class="def">ForcedArgs</a> = [<a href="Agda-Compiler-Epic-Interface.html#t:Forced">Forced</a>]<a href="src/Agda-Compiler-Epic-Interface.html#ForcedArgs" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:RelevantArgs" class="def">RelevantArgs</a> = [<a href="Agda-Compiler-Epic-Interface.html#t:Relevance">Relevance</a>]<a href="src/Agda-Compiler-Epic-Interface.html#RelevantArgs" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:InjectiveFun" class="def">InjectiveFun</a> <a href="src/Agda-Compiler-Epic-Interface.html#InjectiveFun" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:InjectiveFun" class="def">InjectiveFun</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:injArg" class="def">injArg</a> :: <a href="Agda-Syntax-Common.html#t:Nat">Nat</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:injArity" class="def">injArity</a> :: <a href="Agda-Syntax-Common.html#t:Nat">Nat</a></dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:InjectiveFun" class="caption collapser" onclick="toggleSection('i:InjectiveFun')">Instances</p><div id="section.i:InjectiveFun" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-Compiler-Epic-Interface.html#t:InjectiveFun">InjectiveFun</a></td><td class="doc empty"> </td></tr><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-Compiler-Epic-Interface.html#t:InjectiveFun">InjectiveFun</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable">Typeable</a> <a href="Agda-Compiler-Epic-Interface.html#t:InjectiveFun">InjectiveFun</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Compiler-Epic-Interface.html#t:InjectiveFun">InjectiveFun</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:EInterface" class="def">EInterface</a> <a href="src/Agda-Compiler-Epic-Interface.html#EInterface" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:EInterface" class="def">EInterface</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:constrTags" class="def">constrTags</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:QName">QName</a> <a href="Agda-Compiler-Epic-Interface.html#t:Tag">Tag</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:definitions" class="def">definitions</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-Epic-Interface.html#t:Var">Var</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:defDelayed" class="def">defDelayed</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:QName">QName</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:conArity" class="def">conArity</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:QName">QName</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:mainName" class="def">mainName</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></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:relevantArgs" class="def">relevantArgs</a> :: <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Compiler-Epic-Interface.html#t:Var">Var</a> <a href="Agda-Compiler-Epic-Interface.html#t:RelevantArgs">RelevantArgs</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:forcedArgs" class="def">forcedArgs</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:QName">QName</a> <a href="Agda-Compiler-Epic-Interface.html#t:ForcedArgs">ForcedArgs</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:injectiveFuns" class="def">injectiveFuns</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:QName">QName</a> <a href="Agda-Compiler-Epic-Interface.html#t:InjectiveFun">InjectiveFun</a></dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:EInterface" class="caption collapser" onclick="toggleSection('i:EInterface')">Instances</p><div id="section.i:EInterface" 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-Compiler-Epic-Interface.html#t:EInterface">EInterface</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable">Typeable</a> <a href="Agda-Compiler-Epic-Interface.html#t:EInterface">EInterface</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Monoid.html#t:Monoid">Monoid</a> <a href="Agda-Compiler-Epic-Interface.html#t:EInterface">EInterface</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Compiler-Epic-Interface.html#t:EInterface">EInterface</a></td><td class="doc empty"> </td></tr></table></div></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>
