module Agda.Utils.Permutation where
import Data.Typeable (Typeable)
import Data.List
import Agda.Utils.Size
import Agda.Utils.Impossible
#include "../undefined.h"
data Permutation = Perm { permRange :: Int, permPicks :: [Int] }
deriving (Eq, Typeable)
instance Show Permutation where
show (Perm n xs) = showx [0..n 1] ++ " -> " ++ showx xs
where showx = showList "," (\ i -> "x" ++ show i)
showList :: String -> (a -> String) -> [a] -> String
showList sep f [] = ""
showList sep f [e] = f e
showList sep f (e:es) = f e ++ sep ++ showList sep f es
instance Sized Permutation where
size (Perm _ xs) = size xs
permute :: Permutation -> [a] -> [a]
permute (Perm _ is) xs = map (xs !!!) is
where
[] !!! _ = __IMPOSSIBLE__
(x:xs) !!! 0 = x
(x:xs) !!! n = xs !!! (n 1)
idP :: Int -> Permutation
idP n = Perm n [0..n 1]
takeP :: Int -> Permutation -> Permutation
takeP n (Perm m xs) = Perm n $ filter (< n) xs
liftP :: Int -> Permutation -> Permutation
liftP n (Perm m xs) = Perm (n + m) $ xs ++ [m..m+n1]
composeP :: Permutation -> Permutation -> Permutation
composeP p1 (Perm n xs) = Perm n $ permute p1 xs
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
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 :: Int -> Int -> 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]
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 ]