module Agda.Utils.Permutation where
import Prelude hiding (drop, null)
import Control.DeepSeq
import Control.Monad (filterM)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.Functor.Identity
import qualified Data.List as List
import Data.Maybe
import Data.Array
import Data.Data (Data)
import GHC.Generics (Generic)
import Agda.Utils.Functor
import Agda.Utils.List ((!!!))
import Agda.Utils.Null
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Impossible
data Permutation = Perm { Permutation -> Int
permRange :: Int, Permutation -> [Int]
permPicks :: [Int] }
deriving (Permutation -> Permutation -> Bool
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
Permutation -> Constr
Permutation -> DataType
(forall b. Data b => b -> b) -> Permutation -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Permutation -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Permutation -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Permutation -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Permutation -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, forall x. Rep Permutation x -> Permutation
forall x. Permutation -> Rep Permutation x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Permutation x -> Permutation
$cfrom :: forall x. Permutation -> Rep Permutation x
Generic)
instance Show Permutation where
show :: Permutation -> String
show (Perm Int
n [Int]
xs) = [Int] -> String
showx [Int
0..Int
n forall a. Num a => a -> a -> a
- Int
1] forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ [Int] -> String
showx [Int]
xs
where showx :: [Int] -> String
showx = forall a. String -> (a -> String) -> [a] -> String
showList String
"," (\ Int
i -> String
"x" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i)
showList :: String -> (a -> String) -> [a] -> String
showList :: forall a. String -> (a -> String) -> [a] -> String
showList String
sep a -> String
f [] = String
""
showList String
sep a -> String
f [a
e] = a -> String
f a
e
showList String
sep a -> String
f (a
e:[a]
es) = a -> String
f a
e forall a. [a] -> [a] -> [a]
++ String
sep forall a. [a] -> [a] -> [a]
++ forall a. String -> (a -> String) -> [a] -> String
showList String
sep a -> String
f [a]
es
instance Sized Permutation where
size :: Permutation -> Int
size (Perm Int
_ [Int]
xs) = forall a. Sized a => a -> Int
size [Int]
xs
instance Null Permutation where
empty :: Permutation
empty = Int -> [Int] -> Permutation
Perm Int
0 []
null :: Permutation -> Bool
null (Perm Int
_ [Int]
picks) = forall a. Null a => a -> Bool
null [Int]
picks
instance NFData Permutation
permute :: Permutation -> [a] -> [a]
permute :: forall a. Permutation -> [a] -> [a]
permute Permutation
p [a]
xs = forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__) (forall a. Permutation -> [a] -> [Maybe a]
safePermute Permutation
p [a]
xs)
safePermute :: Permutation -> [a] -> [Maybe a]
safePermute :: forall a. Permutation -> [a] -> [Maybe a]
safePermute (Perm Int
_ [Int]
is) [a]
xs = forall a b. (a -> b) -> [a] -> [b]
map ([a]
xs forall {a}. [a] -> Int -> Maybe a
!!!!) [Int]
is
where
[a]
xs !!!! :: [a] -> Int -> Maybe a
!!!! Int
n | Int
n forall a. Ord a => a -> a -> Bool
< Int
0 = forall a. Maybe a
Nothing
| Bool
otherwise = [a]
xs 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 Int
n [Int]
is) = forall a. [Maybe a] -> [a]
catMaybes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Int
i Maybe a
ma -> (Int
i,) 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 Permutation
p = forall a. [(Int, a)] -> IntMap a
IntMap.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 Int
n [Int]
_) = IntMap a -> [Maybe a]
tabulate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. InversePermute a b => Permutation -> a -> b
inversePermute Permutation
p
where tabulate :: IntMap a -> [Maybe a]
tabulate IntMap a
m = forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Int
0..Int
nforall a. Num a => a -> a -> a
-Int
1] forall a b. (a -> b) -> a -> b
$ \ Int
i -> 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 Int
n [Int]
xs) Int -> a
f = forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Int
0..Int
nforall a. Num a => a -> a -> a
-Int
1] forall a b. (a -> b) -> a -> b
$ \ Int
x -> Int -> a
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
x [Int]
xs
idP :: Int -> Permutation
idP :: Int -> Permutation
idP Int
n = Int -> [Int] -> Permutation
Perm Int
n [Int
0..Int
n forall a. Num a => a -> a -> a
- Int
1]
takeP :: Int -> Permutation -> Permutation
takeP :: Int -> Permutation -> Permutation
takeP Int
n (Perm Int
m [Int]
xs) = Int -> [Int] -> Permutation
Perm Int
n forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Ord a => a -> a -> Bool
< Int
n) [Int]
xs
droppedP :: Permutation -> Permutation
droppedP :: Permutation -> Permutation
droppedP (Perm Int
n [Int]
xs) = Int -> [Int] -> Permutation
Perm Int
n forall a b. (a -> b) -> a -> b
$ [Int
0..Int
nforall a. Num a => a -> a -> a
-Int
1] forall a. Eq a => [a] -> [a] -> [a]
List.\\ [Int]
xs
liftP :: Int -> Permutation -> Permutation
liftP :: Int -> Permutation -> Permutation
liftP Int
n (Perm Int
m [Int]
xs) = Int -> [Int] -> Permutation
Perm (Int
n forall a. Num a => a -> a -> a
+ Int
m) forall a b. (a -> b) -> a -> b
$ [Int]
xs forall a. [a] -> [a] -> [a]
++ [Int
m..Int
mforall a. Num a => a -> a -> a
+Int
nforall a. Num a => a -> a -> a
-Int
1]
composeP :: Permutation -> Permutation -> Permutation
composeP :: Permutation -> Permutation -> Permutation
composeP Permutation
p1 (Perm Int
n [Int]
xs) = Int -> [Int] -> Permutation
Perm Int
n forall a b. (a -> b) -> a -> b
$ forall a. Permutation -> [a] -> [a]
permute Permutation
p1 [Int]
xs
invertP :: Int -> Permutation -> Permutation
invertP :: Int -> Permutation -> Permutation
invertP Int
err p :: Permutation
p@(Perm Int
n [Int]
xs) = Int -> [Int] -> Permutation
Perm (forall a. Sized a => a -> Int
size [Int]
xs) forall a b. (a -> b) -> a -> b
$ forall i e. Array i e -> [e]
elems Array Int Int
tmpArray
where tmpArray :: Array Int Int
tmpArray = forall i e a.
Ix i =>
(e -> a -> e) -> e -> (i, i) -> [(i, a)] -> Array i e
accumArray (forall a b. a -> b -> a
const forall a. a -> a
id) Int
err (Int
0, Int
nforall a. Num a => a -> a -> a
-Int
1) forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
xs [Int
0..]
compactP :: Permutation -> Permutation
compactP :: Permutation -> Permutation
compactP (Perm Int
n [Int]
xs) = Int -> [Int] -> Permutation
Perm Int
m forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Int -> Int
adjust [Int]
xs
where
m :: Int
m = forall i a. Num i => [a] -> i
List.genericLength [Int]
xs
missing :: [Int]
missing = [Int
0..Int
n forall a. Num a => a -> a -> a
- Int
1] forall a. Eq a => [a] -> [a] -> [a]
List.\\ [Int]
xs
holesBelow :: Int -> Int
holesBelow Int
k = forall i a. Num i => [a] -> i
List.genericLength forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Ord a => a -> a -> Bool
< Int
k) [Int]
missing
adjust :: Int -> Int
adjust Int
k = Int
k forall a. Num a => a -> a -> a
- Int -> Int
holesBelow Int
k
reverseP :: Permutation -> Permutation
reverseP :: Permutation -> Permutation
reverseP (Perm Int
n [Int]
xs) = Int -> [Int] -> Permutation
Perm Int
n forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ((Int
n forall a. Num a => a -> a -> a
- Int
1) forall a. Num a => a -> a -> a
-) forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [Int]
xs
flipP :: Permutation -> Permutation
flipP :: Permutation -> Permutation
flipP (Perm Int
n [Int]
xs) = Int -> [Int] -> Permutation
Perm Int
n forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Int
n forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
-) [Int]
xs
expandP :: Int -> Int -> Permutation -> Permutation
expandP :: Int -> Int -> Permutation -> Permutation
expandP Int
i Int
n (Perm Int
m [Int]
xs) = Int -> [Int] -> Permutation
Perm (Int
m forall a. Num a => a -> a -> a
+ Int
n forall a. Num a => a -> a -> a
- Int
1) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Int -> [Int]
expand [Int]
xs
where
expand :: Int -> [Int]
expand Int
j
| Int
j forall a. Eq a => a -> a -> Bool
== Int
i = [Int
i..Int
i forall a. Num a => a -> a -> a
+ Int
n forall a. Num a => a -> a -> a
- Int
1]
| Int
j forall a. Ord a => a -> a -> Bool
< Int
i = [Int
j]
| Bool
otherwise = [Int
j forall a. Num a => a -> a -> a
+ Int
n forall a. Num a => a -> a -> a
- Int
1]
topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation
topoSort :: forall a. (a -> a -> Bool) -> [a] -> Maybe Permutation
topoSort a -> a -> Bool
parent [a]
xs = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
Monad m =>
(a -> a -> m Bool) -> [a] -> m (Maybe Permutation)
topoSortM (\a
x a
y -> forall a. a -> Identity a
Identity forall a b. (a -> b) -> a -> b
$ a -> a -> Bool
parent a
x a
y) [a]
xs
topoSortM :: Monad m => (a -> a -> m Bool) -> [a] -> m (Maybe Permutation)
topoSortM :: forall (m :: * -> *) a.
Monad m =>
(a -> a -> m Bool) -> [a] -> m (Maybe Permutation)
topoSortM a -> a -> m Bool
parent [a]
xs = do
let nodes :: [(Int, a)]
nodes = forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [a]
xs
parents :: a -> m [Int]
parents a
x = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (\(Int
_, a
y) -> a -> a -> m Bool
parent a
y a
x) [(Int, a)]
nodes
[(Int, [Int])]
g <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) b d a.
Applicative m =>
(b -> m d) -> (a, b) -> m (a, d)
mapSndM a -> m [Int]
parents) [(Int, a)]
nodes
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> [Int] -> Permutation
Perm (forall a. Sized a => a -> Int
size [a]
xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall node. Eq node => [(node, [node])] -> Maybe [node]
topo [(Int, [Int])]
g
where
topo :: Eq node => [(node, [node])] -> Maybe [node]
topo :: forall node. Eq node => [(node, [node])] -> Maybe [node]
topo [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
topo [(node, [node])]
g = case [node]
xs of
[] -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"cycle detected"
node
x : [node]
_ -> do
[node]
ys <- forall node. Eq node => [(node, [node])] -> Maybe [node]
topo forall a b. (a -> b) -> a -> b
$ forall {a}. Eq a => a -> [(a, [a])] -> [(a, [a])]
remove node
x [(node, [node])]
g
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ node
x forall a. a -> [a] -> [a]
: [node]
ys
where
xs :: [node]
xs = [ node
x | (node
x, []) <- [(node, [node])]
g ]
remove :: a -> [(a, [a])] -> [(a, [a])]
remove a
x [(a, [a])]
g = [ (a
y, forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= a
x) [a]
ys) | (a
y, [a]
ys) <- [(a, [a])]
g, a
x forall a. Eq a => a -> a -> Bool
/= a
y ]
data Drop a = Drop
{ forall a. Drop a -> Int
dropN :: Int
, forall a. Drop a -> a
dropFrom :: a
}
deriving (Drop a -> Drop a -> Bool
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, Drop a -> Drop a -> Bool
Drop a -> Drop a -> Ordering
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
Ord, Int -> Drop a -> ShowS
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, Drop a -> Constr
Drop a -> DataType
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 (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))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. 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 u. (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 :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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)
Data, 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
<$ :: forall a b. a -> Drop b -> Drop a
$c<$ :: forall a b. a -> Drop b -> Drop a
fmap :: forall a b. (a -> b) -> Drop a -> Drop b
$cfmap :: forall a b. (a -> b) -> Drop a -> Drop b
Functor, 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 :: forall a. Num a => Drop a -> a
$cproduct :: forall a. Num a => Drop a -> a
sum :: forall a. Num a => Drop a -> a
$csum :: forall a. Num a => Drop a -> a
minimum :: forall a. Ord a => Drop a -> a
$cminimum :: forall a. Ord a => Drop a -> a
maximum :: forall a. Ord a => Drop a -> a
$cmaximum :: forall a. Ord a => Drop a -> a
elem :: forall a. Eq a => a -> Drop a -> Bool
$celem :: forall a. Eq a => a -> Drop a -> Bool
length :: forall a. Drop a -> Int
$clength :: forall a. Drop a -> Int
null :: forall a. Drop a -> Bool
$cnull :: forall a. Drop a -> Bool
toList :: forall a. Drop a -> [a]
$ctoList :: forall a. Drop a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Drop a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Drop a -> a
foldr1 :: forall a. (a -> a -> a) -> Drop a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Drop a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Drop a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Drop a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Drop a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Drop a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Drop a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Drop a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Drop a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Drop a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Drop a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Drop a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Drop a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Drop a -> m
fold :: forall m. Monoid m => Drop m -> m
$cfold :: forall m. Monoid m => Drop m -> m
Foldable, Functor Drop
Foldable Drop
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 :: forall (m :: * -> *) a. Monad m => Drop (m a) -> m (Drop a)
$csequence :: forall (m :: * -> *) a. Monad m => Drop (m a) -> m (Drop a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Drop a -> m (Drop b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Drop a -> m (Drop b)
sequenceA :: forall (f :: * -> *) a. Applicative f => Drop (f a) -> f (Drop a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Drop (f a) -> f (Drop a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Drop a -> f (Drop b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Drop a -> f (Drop b)
Traversable)
class DoDrop a where
doDrop :: Drop a -> a
dropMore :: Int -> Drop a -> Drop a
dropMore Int
n (Drop Int
m a
xs) = forall a. Int -> a -> Drop a
Drop (Int
m forall a. Num a => a -> a -> a
+ Int
n) a
xs
unDrop :: Int -> Drop a -> Drop a
unDrop Int
n (Drop Int
m a
xs)
| Int
n forall a. Ord a => a -> a -> Bool
<= Int
m = forall a. Int -> a -> Drop a
Drop (Int
m forall a. Num a => a -> a -> a
- Int
n) a
xs
| Bool
otherwise = forall a. HasCallStack => a
__IMPOSSIBLE__
instance DoDrop [a] where
doDrop :: Drop [a] -> [a]
doDrop (Drop Int
m [a]
xs) = forall a. Int -> [a] -> [a]
List.drop Int
m [a]
xs
instance DoDrop Permutation where
doDrop :: Drop Permutation -> Permutation
doDrop (Drop Int
k (Perm Int
n [Int]
xs)) =
Int -> [Int] -> Permutation
Perm (Int
n forall a. Num a => a -> a -> a
+ Int
m) forall a b. (a -> b) -> a -> b
$ [Int
0..Int
mforall a. Num a => a -> a -> a
-Int
1] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Num a => a -> a -> a
+ Int
m) (forall a. Int -> [a] -> [a]
List.drop Int
k [Int]
xs)
where m :: Int
m = -Int
k
unDrop :: Int -> Drop Permutation -> Drop Permutation
unDrop Int
m = forall a. DoDrop a => Int -> Drop a -> Drop a
dropMore (-Int
m)