<!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.Utils.Permutation</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-Utils-Permutation.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Utils-Permutation.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>Safe-Infered</td></tr></table><p class="caption">Agda.Utils.Permutation</p></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">data</span> <a href="#t:Permutation">Permutation</a> = <a href="#v:Perm">Perm</a> {<ul class="subs"><li><a href="#v:permRange">permRange</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:permPicks">permPicks</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a>]</li></ul>}</li><li class="src short"><a href="#v:permute">permute</a> :: <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> [a] -> [a]</li><li class="src short"><a href="#v:idP">idP</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a></li><li class="src short"><a href="#v:takeP">takeP</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a></li><li class="src short"><a href="#v:liftP">liftP</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a></li><li class="src short"><a href="#v:composeP">composeP</a> :: <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a></li><li class="src short"><a href="#v:invertP">invertP</a> :: <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a></li><li class="src short"><a href="#v:compactP">compactP</a> :: <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a></li><li class="src short"><a href="#v:reverseP">reverseP</a> :: <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a></li><li class="src short"><a href="#v:expandP">expandP</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a></li><li class="src short"><a href="#v:topoSort">topoSort</a> :: (a -> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>) -> [a] -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a></li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Permutation" class="def">Permutation</a> <a href="src/Agda-Utils-Permutation.html#Permutation" class="link">Source</a></p><div class="doc"><pre>permute [1,2,0] [x0,x1,x2] = [x1,x2,x0]</pre><p>Agda typing would be:
<code>Perm : {m : Nat}(n : Nat) -> Vec (Fin n) m -> Permutation</code>
<code>m</code> is the <code><a href="Agda-Utils-Size.html#v:size">size</a></code> of the permutation.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Perm" class="def">Perm</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:permRange" class="def">permRange</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:permPicks" class="def">permPicks</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></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:Permutation" class="caption collapser" onclick="toggleSection('i:Permutation')">Instances</p><div id="section.i:Permutation" 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-Utils-Permutation.html#t:Permutation">Permutation</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-Utils-Permutation.html#t:Permutation">Permutation</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-Utils-Permutation.html#t:Permutation">Permutation</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Utils-Size.html#t:Sized">Sized</a> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-DropArgs.html#t:DropArgs">DropArgs</a> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</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-Utils-Permutation.html#t:Permutation">Permutation</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:permute" class="def">permute</a> :: <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> [a] -> [a]<a href="src/Agda-Utils-Permutation.html#permute" class="link">Source</a></p><div class="doc"><p><code>permute [1,2,0] [x0,x1,x2] = [x1,x2,x0]</code>
More precisely, <code>permute indices list = sublist</code>, generates <code>sublist</code>
from <code>list</code> by picking the elements of list as indicated by <code>indices</code>.
<code>permute [1,3,0] [x0,x1,x2,x3] = [x1,x3,x0]</code>
</p><p>Agda typing:
<code>permute (Perm {m} n is) : Vec A m -> Vec A n</code>
</p></div></div><div class="top"><p class="src"><a name="v:idP" class="def">idP</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a><a href="src/Agda-Utils-Permutation.html#idP" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:takeP" class="def">takeP</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a><a href="src/Agda-Utils-Permutation.html#takeP" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:liftP" class="def">liftP</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a><a href="src/Agda-Utils-Permutation.html#liftP" class="link">Source</a></p><div class="doc"><p><code>liftP k</code> takes a <code>Perm {m} n</code> to a <code>Perm {m+k} (n+k)</code>.
Analogous to <code><a href="Agda-TypeChecking-Substitution.html#v:liftS">liftS</a></code>,
but Permutations operate on de Bruijn LEVELS, not indices.
</p></div></div><div class="top"><p class="src"><a name="v:composeP" class="def">composeP</a> :: <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a><a href="src/Agda-Utils-Permutation.html#composeP" class="link">Source</a></p><div class="doc"><pre>permute (compose p1 p2) == permute p1 . permute p2</pre></div></div><div class="top"><p class="src"><a name="v:invertP" class="def">invertP</a> :: <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a><a href="src/Agda-Utils-Permutation.html#invertP" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:compactP" class="def">compactP</a> :: <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a><a href="src/Agda-Utils-Permutation.html#compactP" class="link">Source</a></p><div class="doc"><p>Turn a possible non-surjective permutation into a surjective permutation.
</p></div></div><div class="top"><p class="src"><a name="v:reverseP" class="def">reverseP</a> :: <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a><a href="src/Agda-Utils-Permutation.html#reverseP" class="link">Source</a></p><div class="doc"><pre>permute (reverseP p) xs ==
reverse $ permute p $ reverse xs</pre><p>Example:
<code>
permute (reverseP (Perm 4 [1,3,0])) [x0,x1,x2,x3]
== permute (Perm 4 $ map (3-) [0,3,1]) [x0,x1,x2,x3]
== permute (Perm 4 [3,0,2]) [x0,x1,x2,x3]
== [x3,x0,x2]
== reverse [x2,x0,x3]
== reverse $ permute (Perm 4 [1,3,0]) [x3,x2,x1,x0]
== reverse $ permute (Perm 4 [1,3,0]) $ reverse [x0,x1,x2,x3]
</code>
</p></div></div><div class="top"><p class="src"><a name="v:expandP" class="def">expandP</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a> -> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a><a href="src/Agda-Utils-Permutation.html#expandP" class="link">Source</a></p><div class="doc"><p><code>expandP i n π</code> in the domain of <code>π</code> replace the <em>i</em>th element by <em>n</em> elements.
</p></div></div><div class="top"><p class="src"><a name="v:topoSort" class="def">topoSort</a> :: (a -> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>) -> [a] -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a><a href="src/Agda-Utils-Permutation.html#topoSort" class="link">Source</a></p><div class="doc"><p>Stable topologic sort. The first argument decides whether its first
argument is an immediate parent to its second argument.
</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>
