{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
module Agda.Utils.Permutation where
import Prelude hiding (drop, null)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.List as List
import Data.Maybe
import Data.Array
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)
import Data.Data (Data)
import Agda.Syntax.Position (KillRange(..))
import Agda.Utils.Functor
import Agda.Utils.List ((!!!))
import Agda.Utils.Null
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
data Permutation = Perm { permRange :: Int, permPicks :: [Int] }
deriving (Eq, Data)
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
instance Null Permutation where
empty = Perm 0 []
null (Perm _ picks) = null picks
instance KillRange Permutation where
killRange = id
permute :: Permutation -> [a] -> [a]
permute p xs = map (fromMaybe __IMPOSSIBLE__) (safePermute p xs)
safePermute :: Permutation -> [a] -> [Maybe a]
safePermute (Perm _ is) xs = map (xs !!!!) is
where
xs !!!! n | n < 0 = Nothing
| otherwise = xs !!! n
class InversePermute a b where
inversePermute :: Permutation -> a -> b
instance InversePermute [Maybe a] [(Int,a)] where
inversePermute (Perm n is) = catMaybes . zipWith (\ i ma -> (i,) <$> ma) is
instance InversePermute [Maybe a] (IntMap a) where
inversePermute p = IntMap.fromList . inversePermute p
instance InversePermute [Maybe a] [Maybe a] where
inversePermute p@(Perm n _) = tabulate . inversePermute p
where tabulate m = for [0..n-1] $ \ i -> IntMap.lookup i m
instance InversePermute (Int -> a) [Maybe a] where
inversePermute (Perm n xs) f = for [0..n-1] $ \ x -> f <$> List.findIndex (x ==) xs
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..n-1] List.\\ xs
liftP :: Int -> Permutation -> Permutation
liftP n (Perm m xs) = Perm (n + m) $ xs ++ [m..m+n-1]
composeP :: Permutation -> Permutation -> Permutation
composeP p1 (Perm n xs) = Perm n $ permute p1 xs
invertP :: Int -> Permutation -> Permutation
invertP err p@(Perm n xs) = Perm (size xs) $ elems tmpArray
where tmpArray = accumArray (flip const) err (0, n-1) $ zip xs [0..]
compactP :: Permutation -> Permutation
compactP (Perm n xs) = Perm m $ map adjust xs
where
m = List.genericLength xs
missing = [0..n - 1] List.\\ xs
holesBelow k = List.genericLength $ filter (< k) missing
adjust k = k - holesBelow k
reverseP :: Permutation -> Permutation
reverseP (Perm n xs) = Perm n $ map ((n - 1) -) $ reverse xs
flipP :: Permutation -> Permutation
flipP (Perm n xs) = Perm n $ map (n - 1 -) 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, Data, Functor, Foldable, Traversable)
instance KillRange a => KillRange (Drop a) where
killRange = fmap killRange
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..m-1] ++ map (+ m) (List.drop k xs)
where m = -k
unDrop m = dropMore (-m)