module Agda.Utils.Permutation where
import Prelude hiding (drop)
import Data.List hiding (drop)
import qualified Data.List as List
import Data.Maybe
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)
import Data.Typeable (Typeable)
import Agda.Utils.Size
import Agda.Utils.List ((!!!))
#include "../undefined.h"
import Agda.Utils.Impossible
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
xs !!!! n = fromMaybe __IMPOSSIBLE__ (xs !!! n)
idP :: Int -> Permutation
idP n = Perm n [0..n 1]
takeP :: Int -> Permutation -> Permutation
takeP n (Perm m xs) = Perm n $ filter (< n) xs
droppedP :: Permutation -> Permutation
droppedP (Perm n xs) = Perm n $ [0..n1] \\ 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 ]
data Drop a = Drop
{ dropN :: Int
, dropFrom :: a
}
deriving (Eq, Ord, Show, Typeable, Functor, Foldable, Traversable)
class DoDrop a where
doDrop :: Drop a -> a
dropMore :: Int -> Drop a -> Drop a
dropMore n (Drop m xs) = Drop (m + n) xs
unDrop :: Int -> Drop a -> Drop a
unDrop n (Drop m xs)
| n <= m = Drop (m n) xs
| otherwise = __IMPOSSIBLE__
instance DoDrop [a] where
doDrop (Drop m xs) = List.drop m xs
instance DoDrop Permutation where
doDrop (Drop k (Perm n xs)) =
Perm (n + m) $ [0..m1] ++ map (+ m) (List.drop k xs)
where m = k
unDrop m = dropMore (m)