```{-# LANGUAGE DeriveDataTypeable #-}
module Agda.Utils.Permutation where

import Data.Generics (Typeable, Data)
import Data.List
import Agda.Utils.Size

-- | @permute [2,3,1] [x,y,z] = [y,z,x]@
data Permutation = Perm Integer [Integer]
deriving (Show, Eq, Data, Typeable)

instance Sized Permutation where
size (Perm _ xs) = size xs

permute :: Permutation -> [a] -> [a]
permute (Perm _ is) xs = map ((xs !!) . fromIntegral) is

idP :: Integer -> Permutation
idP n = Perm n [0..n - 1]

-- | @permute (compose p1 p2) == permute p1 . permute p2@
composeP :: Permutation -> Permutation -> Permutation
composeP p1 (Perm n xs) = Perm n \$ permute p1 xs
{- proof:
permute (compose (Perm xs) (Perm ys)) zs
== permute (Perm (permute (Perm xs) ys)) zs
== map (zs !!) (permute (Perm xs) ys)
== map (zs !!) (map (ys !!) xs)
== map (zs !! . ys !!) xs
== map (\x -> zs !! (ys !! x)) xs
== map (\x -> map (zs !!) ys !! x) xs  {- map f xs !! n == f (xs !! n) -}
== map (map (zs !!) ys !!) xs
== permute (Perm xs) (permute (Perm ys) zs)
-}

invertP :: Permutation -> Permutation
invertP p@(Perm n xs) = Perm (size xs) \$ map inv [0..n - 1]
where
inv x = case findIndex (x ==) xs of
Just y  -> fromIntegral y
Nothing -> error \$ "invertP: non-surjective permutation " ++ show p

-- | Turn a possible non-surjective permutation into a surjective permutation.
compactP :: Permutation -> Permutation
compactP (Perm n xs) = Perm m \$ map adjust xs
where
m            = genericLength xs
missing      = [0..n - 1] \\ xs
holesBelow k = genericLength \$ filter (< k) missing
adjust k = k - holesBelow k

reverseP :: Permutation -> Permutation
reverseP (Perm n xs) = Perm n \$ map ((n - 1) -) \$ reverse xs

-- | @expandP i n π@ in the domain of @π@ replace the /i/th element by /n/ elements.
expandP :: Integer -> Integer -> Permutation -> Permutation
expandP i n (Perm m xs) = Perm (m + n - 1) \$ concatMap expand xs
where
expand j
| j == i	  = [i..i + n - 1]
| j < i	  = [j]
| otherwise = [j + n - 1]

-- | Stable topologic sort. The first argument decides whether its first
--   argument is an immediate parent to its second argument.
topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation
topoSort parent xs = fmap (Perm (size xs)) \$ topo g
where
nodes     = zip [0..] xs
g	      = [ (n, parents x) | (n, x) <- nodes ]
parents x = [ n | (n, y) <- nodes, parent y x ]

topo :: Eq node => [(node, [node])] -> Maybe [node]
topo [] = return []
topo g  = case xs of
[]    -> fail "cycle detected"
x : _ -> do
ys <- topo \$ remove x g
return \$ x : ys
where
xs = [ x | (x, []) <- g ]
remove x g = [ (y, filter (/= x) ys) | (y, ys) <- g, x /= y ]

```