{-# 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
import Agda.Utils.Impossible
data Permutation = Perm { Permutation -> Int
permRange :: Int, Permutation -> [Int]
permPicks :: [Int] }
deriving (Permutation -> Permutation -> Bool
(Permutation -> Permutation -> Bool)
-> (Permutation -> Permutation -> Bool) -> Eq Permutation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Permutation -> Permutation -> Bool
$c/= :: Permutation -> Permutation -> Bool
== :: Permutation -> Permutation -> Bool
$c== :: Permutation -> Permutation -> Bool
Eq, Typeable Permutation
Constr
DataType
Typeable Permutation =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Permutation -> c Permutation)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Permutation)
-> (Permutation -> Constr)
-> (Permutation -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Permutation))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Permutation))
-> ((forall b. Data b => b -> b) -> Permutation -> Permutation)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Permutation -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Permutation -> r)
-> (forall u. (forall d. Data d => d -> u) -> Permutation -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> Permutation -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Permutation -> m Permutation)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Permutation -> m Permutation)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Permutation -> m Permutation)
-> Data Permutation
Permutation -> Constr
Permutation -> DataType
(forall b. Data b => b -> b) -> Permutation -> Permutation
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Permutation -> c Permutation
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Permutation
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Permutation -> u
forall u. (forall d. Data d => d -> u) -> Permutation -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Permutation -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Permutation -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Permutation -> m Permutation
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Permutation -> m Permutation
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Permutation
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Permutation -> c Permutation
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Permutation)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Permutation)
$cPerm :: Constr
$tPermutation :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Permutation -> m Permutation
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Permutation -> m Permutation
gmapMp :: (forall d. Data d => d -> m d) -> Permutation -> m Permutation
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Permutation -> m Permutation
gmapM :: (forall d. Data d => d -> m d) -> Permutation -> m Permutation
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Permutation -> m Permutation
gmapQi :: Int -> (forall d. Data d => d -> u) -> Permutation -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Permutation -> u
gmapQ :: (forall d. Data d => d -> u) -> Permutation -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Permutation -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Permutation -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Permutation -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Permutation -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Permutation -> r
gmapT :: (forall b. Data b => b -> b) -> Permutation -> Permutation
$cgmapT :: (forall b. Data b => b -> b) -> Permutation -> Permutation
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Permutation)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Permutation)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Permutation)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Permutation)
dataTypeOf :: Permutation -> DataType
$cdataTypeOf :: Permutation -> DataType
toConstr :: Permutation -> Constr
$ctoConstr :: Permutation -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Permutation
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Permutation
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Permutation -> c Permutation
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Permutation -> c Permutation
$cp1Data :: Typeable Permutation
Data)
instance Show Permutation where
show :: Permutation -> String
show (Perm n :: Int
n xs :: [Int]
xs) = [Int] -> String
showx [0..Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1] String -> ShowS
forall a. [a] -> [a] -> [a]
++ " -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Int] -> String
showx [Int]
xs
where showx :: [Int] -> String
showx = String -> (Int -> String) -> [Int] -> String
forall a. String -> (a -> String) -> [a] -> String
showList "," (\ i :: Int
i -> "x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)
showList :: String -> (a -> String) -> [a] -> String
showList :: String -> (a -> String) -> [a] -> String
showList sep :: String
sep f :: a -> String
f [] = ""
showList sep :: String
sep f :: a -> String
f [e :: a
e] = a -> String
f a
e
showList sep :: String
sep f :: a -> String
f (e :: a
e:es :: [a]
es) = a -> String
f a
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
sep String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> (a -> String) -> [a] -> String
forall a. String -> (a -> String) -> [a] -> String
showList String
sep a -> String
f [a]
es
instance Sized Permutation where
size :: Permutation -> Int
size (Perm _ xs :: [Int]
xs) = [Int] -> Int
forall a. Sized a => a -> Int
size [Int]
xs
instance Null Permutation where
empty :: Permutation
empty = Int -> [Int] -> Permutation
Perm 0 []
null :: Permutation -> Bool
null (Perm _ picks :: [Int]
picks) = [Int] -> Bool
forall a. Null a => a -> Bool
null [Int]
picks
instance KillRange Permutation where
killRange :: Permutation -> Permutation
killRange = Permutation -> Permutation
forall a. a -> a
id
permute :: Permutation -> [a] -> [a]
permute :: Permutation -> [a] -> [a]
permute p :: Permutation
p xs :: [a]
xs = (Maybe a -> a) -> [Maybe a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
forall a. HasCallStack => a
__IMPOSSIBLE__) (Permutation -> [a] -> [Maybe a]
forall a. Permutation -> [a] -> [Maybe a]
safePermute Permutation
p [a]
xs)
safePermute :: Permutation -> [a] -> [Maybe a]
safePermute :: Permutation -> [a] -> [Maybe a]
safePermute (Perm _ is :: [Int]
is) xs :: [a]
xs = (Int -> Maybe a) -> [Int] -> [Maybe a]
forall a b. (a -> b) -> [a] -> [b]
map ([a]
xs [a] -> Int -> Maybe a
forall a. [a] -> Int -> Maybe a
!!!!) [Int]
is
where
xs :: [a]
xs !!!! :: [a] -> Int -> Maybe a
!!!! n :: Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = Maybe a
forall a. Maybe a
Nothing
| Bool
otherwise = [a]
xs [a] -> Int -> Maybe a
forall a. [a] -> Int -> Maybe a
!!! Int
n
class InversePermute a b where
inversePermute :: Permutation -> a -> b
instance InversePermute [Maybe a] [(Int,a)] where
inversePermute :: Permutation -> [Maybe a] -> [(Int, a)]
inversePermute (Perm n :: Int
n is :: [Int]
is) = [Maybe (Int, a)] -> [(Int, a)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Int, a)] -> [(Int, a)])
-> ([Maybe a] -> [Maybe (Int, a)]) -> [Maybe a] -> [(Int, a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Maybe a -> Maybe (Int, a))
-> [Int] -> [Maybe a] -> [Maybe (Int, a)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ i :: Int
i ma :: Maybe a
ma -> (Int
i,) (a -> (Int, a)) -> Maybe a -> Maybe (Int, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
ma) [Int]
is
instance InversePermute [Maybe a] (IntMap a) where
inversePermute :: Permutation -> [Maybe a] -> IntMap a
inversePermute p :: Permutation
p = [(Int, a)] -> IntMap a
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, a)] -> IntMap a)
-> ([Maybe a] -> [(Int, a)]) -> [Maybe a] -> IntMap a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Permutation -> [Maybe a] -> [(Int, a)]
forall a b. InversePermute a b => Permutation -> a -> b
inversePermute Permutation
p
instance InversePermute [Maybe a] [Maybe a] where
inversePermute :: Permutation -> [Maybe a] -> [Maybe a]
inversePermute p :: Permutation
p@(Perm n :: Int
n _) = IntMap a -> [Maybe a]
forall a. IntMap a -> [Maybe a]
tabulate (IntMap a -> [Maybe a])
-> ([Maybe a] -> IntMap a) -> [Maybe a] -> [Maybe a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Permutation -> [Maybe a] -> IntMap a
forall a b. InversePermute a b => Permutation -> a -> b
inversePermute Permutation
p
where tabulate :: IntMap a -> [Maybe a]
tabulate m :: IntMap a
m = [Int] -> (Int -> Maybe a) -> [Maybe a]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1] ((Int -> Maybe a) -> [Maybe a]) -> (Int -> Maybe a) -> [Maybe a]
forall a b. (a -> b) -> a -> b
$ \ i :: Int
i -> Int -> IntMap a -> Maybe a
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap a
m
instance InversePermute (Int -> a) [Maybe a] where
inversePermute :: Permutation -> (Int -> a) -> [Maybe a]
inversePermute (Perm n :: Int
n xs :: [Int]
xs) f :: Int -> a
f = [Int] -> (Int -> Maybe a) -> [Maybe a]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1] ((Int -> Maybe a) -> [Maybe a]) -> (Int -> Maybe a) -> [Maybe a]
forall a b. (a -> b) -> a -> b
$ \ x :: Int
x -> Int -> a
f (Int -> a) -> Maybe Int -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [Int] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
x [Int]
xs
idP :: Int -> Permutation
idP :: Int -> Permutation
idP n :: Int
n = Int -> [Int] -> Permutation
Perm Int
n [0..Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]
takeP :: Int -> Permutation -> Permutation
takeP :: Int -> Permutation -> Permutation
takeP n :: Int
n (Perm m :: Int
m xs :: [Int]
xs) = Int -> [Int] -> Permutation
Perm Int
n ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$ (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n) [Int]
xs
droppedP :: Permutation -> Permutation
droppedP :: Permutation -> Permutation
droppedP (Perm n :: Int
n xs :: [Int]
xs) = Int -> [Int] -> Permutation
Perm Int
n ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$ [0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1] [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ [Int]
xs
liftP :: Int -> Permutation -> Permutation
liftP :: Int -> Permutation -> Permutation
liftP n :: Int
n (Perm m :: Int
m xs :: [Int]
xs) = Int -> [Int] -> Permutation
Perm (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m) ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$ [Int]
xs [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
m..Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1]
composeP :: Permutation -> Permutation -> Permutation
composeP :: Permutation -> Permutation -> Permutation
composeP p1 :: Permutation
p1 (Perm n :: Int
n xs :: [Int]
xs) = Int -> [Int] -> Permutation
Perm Int
n ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$ Permutation -> [Int] -> [Int]
forall a. Permutation -> [a] -> [a]
permute Permutation
p1 [Int]
xs
invertP :: Int -> Permutation -> Permutation
invertP :: Int -> Permutation -> Permutation
invertP err :: Int
err p :: Permutation
p@(Perm n :: Int
n xs :: [Int]
xs) = Int -> [Int] -> Permutation
Perm ([Int] -> Int
forall a. Sized a => a -> Int
size [Int]
xs) ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$ Array Int Int -> [Int]
forall i e. Array i e -> [e]
elems Array Int Int
tmpArray
where tmpArray :: Array Int Int
tmpArray = (Int -> Int -> Int)
-> Int -> (Int, Int) -> [(Int, Int)] -> Array Int Int
forall i e a.
Ix i =>
(e -> a -> e) -> e -> (i, i) -> [(i, a)] -> Array i e
accumArray ((Int -> Int -> Int) -> Int -> Int -> Int
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Int -> Int
forall a b. a -> b -> a
const) Int
err (0, Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) ([(Int, Int)] -> Array Int Int) -> [(Int, Int)] -> Array Int Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
xs [0..]
compactP :: Permutation -> Permutation
compactP :: Permutation -> Permutation
compactP (Perm n :: Int
n xs :: [Int]
xs) = Int -> [Int] -> Permutation
Perm Int
m ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Int
adjust [Int]
xs
where
m :: Int
m = [Int] -> Int
forall i a. Num i => [a] -> i
List.genericLength [Int]
xs
missing :: [Int]
missing = [0..Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1] [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ [Int]
xs
holesBelow :: Int -> i
holesBelow k :: Int
k = [Int] -> i
forall i a. Num i => [a] -> i
List.genericLength ([Int] -> i) -> [Int] -> i
forall a b. (a -> b) -> a -> b
$ (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k) [Int]
missing
adjust :: Int -> Int
adjust k :: Int
k = Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int -> Int
forall i. Num i => Int -> i
holesBelow Int
k
reverseP :: Permutation -> Permutation
reverseP :: Permutation -> Permutation
reverseP (Perm n :: Int
n xs :: [Int]
xs) = Int -> [Int] -> Permutation
Perm Int
n ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map ((Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) Int -> Int -> Int
forall a. Num a => a -> a -> a
-) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int]
forall a. [a] -> [a]
reverse [Int]
xs
flipP :: Permutation -> Permutation
flipP :: Permutation -> Permutation
flipP (Perm n :: Int
n xs :: [Int]
xs) = Int -> [Int] -> Permutation
Perm Int
n ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
-) [Int]
xs
expandP :: Int -> Int -> Permutation -> Permutation
expandP :: Int -> Int -> Permutation -> Permutation
expandP i :: Int
i n :: Int
n (Perm m :: Int
m xs :: [Int]
xs) = Int -> [Int] -> Permutation
Perm (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$ (Int -> [Int]) -> [Int] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Int -> [Int]
expand [Int]
xs
where
expand :: Int -> [Int]
expand j :: Int
j
| Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i = [Int
i..Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]
| Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
i = [Int
j]
| Bool
otherwise = [Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]
topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation
topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation
topoSort parent :: a -> a -> Bool
parent xs :: [a]
xs = Int -> [Int] -> Permutation
Perm ([a] -> Int
forall a. Sized a => a -> Int
size [a]
xs) ([Int] -> Permutation) -> Maybe [Int] -> Maybe Permutation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, [Int])] -> Maybe [Int]
forall node. Eq node => [(node, [node])] -> Maybe [node]
topo [(Int, [Int])]
g
where
nodes :: [(Int, a)]
nodes = [Int] -> [a] -> [(Int, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] [a]
xs
g :: [(Int, [Int])]
g = [ (Int
n, a -> [Int]
parents a
x) | (n :: Int
n, x :: a
x) <- [(Int, a)]
nodes ]
parents :: a -> [Int]
parents x :: a
x = [ Int
n | (n :: Int
n, y :: a
y) <- [(Int, a)]
nodes, a -> a -> Bool
parent a
y a
x ]
topo :: Eq node => [(node, [node])] -> Maybe [node]
topo :: [(node, [node])] -> Maybe [node]
topo [] = [node] -> Maybe [node]
forall (m :: * -> *) a. Monad m => a -> m a
return []
topo g :: [(node, [node])]
g = case [node]
xs of
[] -> String -> Maybe [node]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "cycle detected"
x :: node
x : _ -> do
[node]
ys <- [(node, [node])] -> Maybe [node]
forall node. Eq node => [(node, [node])] -> Maybe [node]
topo ([(node, [node])] -> Maybe [node])
-> [(node, [node])] -> Maybe [node]
forall a b. (a -> b) -> a -> b
$ node -> [(node, [node])] -> [(node, [node])]
forall a. Eq a => a -> [(a, [a])] -> [(a, [a])]
remove node
x [(node, [node])]
g
[node] -> Maybe [node]
forall (m :: * -> *) a. Monad m => a -> m a
return ([node] -> Maybe [node]) -> [node] -> Maybe [node]
forall a b. (a -> b) -> a -> b
$ node
x node -> [node] -> [node]
forall a. a -> [a] -> [a]
: [node]
ys
where
xs :: [node]
xs = [ node
x | (x :: node
x, []) <- [(node, [node])]
g ]
remove :: a -> [(a, [a])] -> [(a, [a])]
remove x :: a
x g :: [(a, [a])]
g = [ (a
y, (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
x) [a]
ys) | (y :: a
y, ys :: [a]
ys) <- [(a, [a])]
g, a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y ]
data Drop a = Drop
{ Drop a -> Int
dropN :: Int
, Drop a -> a
dropFrom :: a
}
deriving (Drop a -> Drop a -> Bool
(Drop a -> Drop a -> Bool)
-> (Drop a -> Drop a -> Bool) -> Eq (Drop a)
forall a. Eq a => Drop a -> Drop a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Drop a -> Drop a -> Bool
$c/= :: forall a. Eq a => Drop a -> Drop a -> Bool
== :: Drop a -> Drop a -> Bool
$c== :: forall a. Eq a => Drop a -> Drop a -> Bool
Eq, Eq (Drop a)
Eq (Drop a) =>
(Drop a -> Drop a -> Ordering)
-> (Drop a -> Drop a -> Bool)
-> (Drop a -> Drop a -> Bool)
-> (Drop a -> Drop a -> Bool)
-> (Drop a -> Drop a -> Bool)
-> (Drop a -> Drop a -> Drop a)
-> (Drop a -> Drop a -> Drop a)
-> Ord (Drop a)
Drop a -> Drop a -> Bool
Drop a -> Drop a -> Ordering
Drop a -> Drop a -> Drop a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Drop a)
forall a. Ord a => Drop a -> Drop a -> Bool
forall a. Ord a => Drop a -> Drop a -> Ordering
forall a. Ord a => Drop a -> Drop a -> Drop a
min :: Drop a -> Drop a -> Drop a
$cmin :: forall a. Ord a => Drop a -> Drop a -> Drop a
max :: Drop a -> Drop a -> Drop a
$cmax :: forall a. Ord a => Drop a -> Drop a -> Drop a
>= :: Drop a -> Drop a -> Bool
$c>= :: forall a. Ord a => Drop a -> Drop a -> Bool
> :: Drop a -> Drop a -> Bool
$c> :: forall a. Ord a => Drop a -> Drop a -> Bool
<= :: Drop a -> Drop a -> Bool
$c<= :: forall a. Ord a => Drop a -> Drop a -> Bool
< :: Drop a -> Drop a -> Bool
$c< :: forall a. Ord a => Drop a -> Drop a -> Bool
compare :: Drop a -> Drop a -> Ordering
$ccompare :: forall a. Ord a => Drop a -> Drop a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Drop a)
Ord, Int -> Drop a -> ShowS
[Drop a] -> ShowS
Drop a -> String
(Int -> Drop a -> ShowS)
-> (Drop a -> String) -> ([Drop a] -> ShowS) -> Show (Drop a)
forall a. Show a => Int -> Drop a -> ShowS
forall a. Show a => [Drop a] -> ShowS
forall a. Show a => Drop a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Drop a] -> ShowS
$cshowList :: forall a. Show a => [Drop a] -> ShowS
show :: Drop a -> String
$cshow :: forall a. Show a => Drop a -> String
showsPrec :: Int -> Drop a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Drop a -> ShowS
Show, Typeable (Drop a)
Constr
DataType
Typeable (Drop a) =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Drop a -> c (Drop a))
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Drop a))
-> (Drop a -> Constr)
-> (Drop a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Drop a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Drop a)))
-> ((forall b. Data b => b -> b) -> Drop a -> Drop a)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Drop a -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Drop a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Drop a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Drop a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Drop a -> m (Drop a))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Drop a -> m (Drop a))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Drop a -> m (Drop a))
-> Data (Drop a)
Drop a -> Constr
Drop a -> DataType
(forall d. Data d => c (t d)) -> Maybe (c (Drop a))
(forall b. Data b => b -> b) -> Drop a -> Drop a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Drop a -> c (Drop a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Drop a)
forall a. Data a => Typeable (Drop a)
forall a. Data a => Drop a -> Constr
forall a. Data a => Drop a -> DataType
forall a.
Data a =>
(forall b. Data b => b -> b) -> Drop a -> Drop a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Drop a -> u
forall a u. Data a => (forall d. Data d => d -> u) -> Drop a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Drop a -> r
forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Drop a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Drop a -> m (Drop a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Drop a -> m (Drop a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Drop a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Drop a -> c (Drop a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Drop a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Drop a))
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Drop a -> u
forall u. (forall d. Data d => d -> u) -> Drop a -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Drop a -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Drop a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Drop a -> m (Drop a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Drop a -> m (Drop a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Drop a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Drop a -> c (Drop a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Drop a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Drop a))
$cDrop :: Constr
$tDrop :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Drop a -> m (Drop a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Drop a -> m (Drop a)
gmapMp :: (forall d. Data d => d -> m d) -> Drop a -> m (Drop a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Drop a -> m (Drop a)
gmapM :: (forall d. Data d => d -> m d) -> Drop a -> m (Drop a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Drop a -> m (Drop a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Drop a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Drop a -> u
gmapQ :: (forall d. Data d => d -> u) -> Drop a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Drop a -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Drop a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Drop a -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Drop a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Drop a -> r
gmapT :: (forall b. Data b => b -> b) -> Drop a -> Drop a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Drop a -> Drop a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Drop a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Drop a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Drop a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Drop a))
dataTypeOf :: Drop a -> DataType
$cdataTypeOf :: forall a. Data a => Drop a -> DataType
toConstr :: Drop a -> Constr
$ctoConstr :: forall a. Data a => Drop a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Drop a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Drop a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Drop a -> c (Drop a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Drop a -> c (Drop a)
$cp1Data :: forall a. Data a => Typeable (Drop a)
Data, a -> Drop b -> Drop a
(a -> b) -> Drop a -> Drop b
(forall a b. (a -> b) -> Drop a -> Drop b)
-> (forall a b. a -> Drop b -> Drop a) -> Functor Drop
forall a b. a -> Drop b -> Drop a
forall a b. (a -> b) -> Drop a -> Drop b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Drop b -> Drop a
$c<$ :: forall a b. a -> Drop b -> Drop a
fmap :: (a -> b) -> Drop a -> Drop b
$cfmap :: forall a b. (a -> b) -> Drop a -> Drop b
Functor, Drop a -> Bool
(a -> m) -> Drop a -> m
(a -> b -> b) -> b -> Drop a -> b
(forall m. Monoid m => Drop m -> m)
-> (forall m a. Monoid m => (a -> m) -> Drop a -> m)
-> (forall m a. Monoid m => (a -> m) -> Drop a -> m)
-> (forall a b. (a -> b -> b) -> b -> Drop a -> b)
-> (forall a b. (a -> b -> b) -> b -> Drop a -> b)
-> (forall b a. (b -> a -> b) -> b -> Drop a -> b)
-> (forall b a. (b -> a -> b) -> b -> Drop a -> b)
-> (forall a. (a -> a -> a) -> Drop a -> a)
-> (forall a. (a -> a -> a) -> Drop a -> a)
-> (forall a. Drop a -> [a])
-> (forall a. Drop a -> Bool)
-> (forall a. Drop a -> Int)
-> (forall a. Eq a => a -> Drop a -> Bool)
-> (forall a. Ord a => Drop a -> a)
-> (forall a. Ord a => Drop a -> a)
-> (forall a. Num a => Drop a -> a)
-> (forall a. Num a => Drop a -> a)
-> Foldable Drop
forall a. Eq a => a -> Drop a -> Bool
forall a. Num a => Drop a -> a
forall a. Ord a => Drop a -> a
forall m. Monoid m => Drop m -> m
forall a. Drop a -> Bool
forall a. Drop a -> Int
forall a. Drop a -> [a]
forall a. (a -> a -> a) -> Drop a -> a
forall m a. Monoid m => (a -> m) -> Drop a -> m
forall b a. (b -> a -> b) -> b -> Drop a -> b
forall a b. (a -> b -> b) -> b -> Drop a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Drop a -> a
$cproduct :: forall a. Num a => Drop a -> a
sum :: Drop a -> a
$csum :: forall a. Num a => Drop a -> a
minimum :: Drop a -> a
$cminimum :: forall a. Ord a => Drop a -> a
maximum :: Drop a -> a
$cmaximum :: forall a. Ord a => Drop a -> a
elem :: a -> Drop a -> Bool
$celem :: forall a. Eq a => a -> Drop a -> Bool
length :: Drop a -> Int
$clength :: forall a. Drop a -> Int
null :: Drop a -> Bool
$cnull :: forall a. Drop a -> Bool
toList :: Drop a -> [a]
$ctoList :: forall a. Drop a -> [a]
foldl1 :: (a -> a -> a) -> Drop a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Drop a -> a
foldr1 :: (a -> a -> a) -> Drop a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Drop a -> a
foldl' :: (b -> a -> b) -> b -> Drop a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Drop a -> b
foldl :: (b -> a -> b) -> b -> Drop a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Drop a -> b
foldr' :: (a -> b -> b) -> b -> Drop a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Drop a -> b
foldr :: (a -> b -> b) -> b -> Drop a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Drop a -> b
foldMap' :: (a -> m) -> Drop a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Drop a -> m
foldMap :: (a -> m) -> Drop a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Drop a -> m
fold :: Drop m -> m
$cfold :: forall m. Monoid m => Drop m -> m
Foldable, Functor Drop
Foldable Drop
(Functor Drop, Foldable Drop) =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Drop a -> f (Drop b))
-> (forall (f :: * -> *) a.
Applicative f =>
Drop (f a) -> f (Drop a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Drop a -> m (Drop b))
-> (forall (m :: * -> *) a. Monad m => Drop (m a) -> m (Drop a))
-> Traversable Drop
(a -> f b) -> Drop a -> f (Drop b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Drop (m a) -> m (Drop a)
forall (f :: * -> *) a. Applicative f => Drop (f a) -> f (Drop a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Drop a -> m (Drop b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Drop a -> f (Drop b)
sequence :: Drop (m a) -> m (Drop a)
$csequence :: forall (m :: * -> *) a. Monad m => Drop (m a) -> m (Drop a)
mapM :: (a -> m b) -> Drop a -> m (Drop b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Drop a -> m (Drop b)
sequenceA :: Drop (f a) -> f (Drop a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Drop (f a) -> f (Drop a)
traverse :: (a -> f b) -> Drop a -> f (Drop b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Drop a -> f (Drop b)
$cp2Traversable :: Foldable Drop
$cp1Traversable :: Functor Drop
Traversable)
instance KillRange a => KillRange (Drop a) where
killRange :: KillRangeT (Drop a)
killRange = (a -> a) -> KillRangeT (Drop a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
forall a. KillRange a => KillRangeT a
killRange
class DoDrop a where
doDrop :: Drop a -> a
dropMore :: Int -> Drop a -> Drop a
dropMore n :: Int
n (Drop m :: Int
m xs :: a
xs) = Int -> a -> Drop a
forall a. Int -> a -> Drop a
Drop (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) a
xs
unDrop :: Int -> Drop a -> Drop a
unDrop n :: Int
n (Drop m :: Int
m xs :: a
xs)
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
m = Int -> a -> Drop a
forall a. Int -> a -> Drop a
Drop (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) a
xs
| Bool
otherwise = Drop a
forall a. HasCallStack => a
__IMPOSSIBLE__
instance DoDrop [a] where
doDrop :: Drop [a] -> [a]
doDrop (Drop m :: Int
m xs :: [a]
xs) = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
List.drop Int
m [a]
xs
instance DoDrop Permutation where
doDrop :: Drop Permutation -> Permutation
doDrop (Drop k :: Int
k (Perm n :: Int
n xs :: [Int]
xs)) =
Int -> [Int] -> Permutation
Perm (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m) ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$ [0..Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-1] [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m) (Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
List.drop Int
k [Int]
xs)
where m :: Int
m = -Int
k
unDrop :: Int -> Drop Permutation -> Drop Permutation
unDrop m :: Int
m = Int -> Drop Permutation -> Drop Permutation
forall a. DoDrop a => Int -> Drop a -> Drop a
dropMore (-Int
m)