    {-# 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 ]