module Agda.Utils.Permutation where

import Prelude hiding (drop, null)

import Control.DeepSeq
import Control.Monad (filterM)

import Data.Array.Unboxed
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.IntMap.Strict as IntMapS
import qualified Data.IntSet as IntSet
import Data.Functor.Identity
import qualified Data.List as List
import Data.Maybe

import GHC.Generics (Generic)

import Agda.Utils.Functor
import Agda.Utils.Null
import Agda.Utils.Size
import Agda.Utils.Tuple

import Agda.Utils.Impossible

-- | Partial permutations. Examples:
--
--   @permute [1,2,0]   [x0,x1,x2] = [x1,x2,x0]@     (proper permutation).
--
--   @permute [1,0]     [x0,x1,x2] = [x1,x0]@        (partial permuation).
--
--   @permute [1,0,1,2] [x0,x1,x2] = [x1,x0,x1,x2]@  (not a permutation because not invertible).
--
--   Agda typing would be:
--   @Perm : {m : Nat}(n : Nat) -> Vec (Fin n) m -> Permutation@
--   @m@ is the 'size' of the permutation.
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, 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 [1,2,0] [x0,x1,x2] = [x1,x2,x0]@
--   More precisely, @permute indices list = sublist@, generates @sublist@
--   from @list@ by picking the elements of list as indicated by @indices@.
--   @permute [1,3,0] [x0,x1,x2,x3] = [x1,x3,x0]@
--
--   Agda typing:
--   @permute (Perm {m} n is) : Vec A m -> Vec A n@
--
-- Precondition for @'permute' ('Perm' _ is) xs@: Every index in @is@
-- must be non-negative and, if @xs@ is finite, then every index must
-- also be smaller than the length of @xs@.
--
-- The implementation is supposed to be extensionally equal to the
-- following one (if different exceptions are identified), but in some
-- cases more efficient:
-- @
--   permute ('Perm' _ is) xs = 'map' (xs 'Agda.Utils.List.!!') is
-- @
permute :: Permutation -> [a] -> [a]
permute :: forall a. Permutation -> [a] -> [a]
permute (Perm Int
_ [Int]
is) [a]
xs = forall a. IntMap a -> Int -> [a] -> [Int] -> [a]
go forall a. Monoid a => a
mempty Int
0 [a]
xs [Int]
is
  where
  -- Computes the list of permuted elements.
  go :: IntMap a  -- A map from positions to elements that have
                  -- already been seen.
     -> Int       -- The number of elements that have been seen (the
                  -- size of the map).
     -> [a]       -- Elements that have not yet been seen.
     -> [Int]     -- Indices to process.
     -> [a]
  go :: forall a. IntMap a -> Int -> [a] -> [Int] -> [a]
go IntMap a
seen !Int
n [a]
xs []       = []
  go IntMap a
seen  Int
n [a]
xs (Int
i : [Int]
is)
    | Int
i forall a. Ord a => a -> a -> Bool
< Int
n     = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__
                    (forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap a
seen) forall a. a -> [a] -> [a]
:
                  forall a. IntMap a -> Int -> [a] -> [Int] -> [a]
go IntMap a
seen Int
n [a]
xs [Int]
is
    | Bool
otherwise = forall a. IntMap a -> Int -> [a] -> Int -> [Int] -> [a]
scan IntMap a
seen Int
n [a]
xs (Int
i forall a. Num a => a -> a -> a
- Int
n) [Int]
is

  -- Finds the element at the given position and continues.
  scan :: IntMap a -> Int -> [a] -> Int -> [Int] -> [a]
  scan :: forall a. IntMap a -> Int -> [a] -> Int -> [Int] -> [a]
scan IntMap a
seen !Int
n (a
x : [a]
xs) !Int
i [Int]
is
    | Int
i forall a. Eq a => a -> a -> Bool
== Int
0 = a
x forall a. a -> [a] -> [a]
: (forall a. IntMap a -> Int -> [a] -> [Int] -> [a]
go forall a b. (a -> b) -> a -> b
$! IntMap a
seen') Int
n' [a]
xs [Int]
is
    | Int
i forall a. Ord a => a -> a -> Bool
> Int
0  = (forall a. IntMap a -> Int -> [a] -> Int -> [Int] -> [a]
scan forall a b. (a -> b) -> a -> b
$! IntMap a
seen') Int
n' [a]
xs (Int
i forall a. Num a => a -> a -> a
- Int
1) [Int]
is
    where
    seen' :: IntMap a
seen' = forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
n a
x IntMap a
seen
    n' :: Int
n'    = Int
n forall a. Num a => a -> a -> a
+ Int
1
  scan IntMap a
seen Int
n [a]
xs !Int
_ [Int]
is = forall a. HasCallStack => a
__IMPOSSIBLE__ forall a. a -> [a] -> [a]
: forall a. IntMap a -> Int -> [a] -> [Int] -> [a]
go IntMap a
seen Int
n [a]
xs [Int]
is

-- |  Invert a Permutation on a partial finite int map.
-- @inversePermute perm f = f'@
-- such that @permute perm f' = f@
--
-- Example, with map represented as @[Maybe a]@:
-- @
--   f    = [Nothing, Just a, Just b ]
--   perm = Perm 4 [3,0,2]
--   f'   = [ Just a , Nothing , Just b , Nothing ]
-- @
-- Zipping @perm@ with @f@ gives @[(0,a),(2,b)]@, after compression
-- with @catMaybes@.  This is an @IntMap@ which can easily
-- written out into a substitution again.

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
i -> Int -> a
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap Int
m
    where
    m :: IntMap Int
m = forall a. (a -> a -> a) -> [(Int, a)] -> IntMap a
IntMapS.fromListWith (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. a -> b -> a
const) forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
xs [Int
0..]

-- | Identity permutation.
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]

-- | Restrict a permutation to work on @n@ elements, discarding picks @>=n@.
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

-- | Pick the elements that are not picked by the permutation.
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
$ forall a. (a -> Bool) -> [a] -> [a]
filter (UArray Int Bool
notInXs forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
!) [Int
0 .. Int
n forall a. Num a => a -> a -> a
- Int
1]
  where
  notInXs :: UArray Int Bool
  notInXs :: UArray Int Bool
notInXs =
    forall (a :: * -> * -> *) e i e'.
(IArray a e, Ix i) =>
(e -> e' -> e) -> e -> (i, i) -> [(i, e')] -> a i e
accumArray (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. a -> b -> a
const) Bool
True (Int
0, Int
n forall a. Num a => a -> a -> a
- Int
1) (forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
xs (forall a. a -> [a]
repeat Bool
False))

-- | @liftP k@ takes a @Perm {m} n@ to a @Perm {m+k} (n+k)@.
--   Analogous to 'Agda.TypeChecking.Substitution.liftS',
--   but Permutations operate on de Bruijn LEVELS, not indices.
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]
-- liftP n (Perm m xs) = Perm (n + m) $ [0..n-1] ++ map (n+) xs -- WRONG, works for indices, but not for levels

-- | @permute (compose p1 p2) == permute p1 . permute p2@
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
  {- proof:
      permute (compose (Perm xs) (Perm ys)) zs
      == permute (Perm (permute (Perm xs) ys)) zs
      == map (zs !!) (permute (Perm xs) ys)
      == map (zs !!) (map (ys !!) xs)
      == map (zs !! . ys !!) xs
      == map (\x -> zs !! (ys !! x)) xs
      == map (\x -> map (zs !!) ys !! x) xs  {- map f xs !! n == f (xs !! n) -}
      == map (map (zs !!) ys !!) xs
      == permute (Perm xs) (permute (Perm ys) zs)
  -}

-- | @invertP err p@ is the inverse of @p@ where defined,
--   otherwise defaults to @err@.
--   @composeP p (invertP err p) == p@
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 (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems Array Int Int
tmpArray
  where
  -- This array cannot be unboxed, because it should be possible to
  -- instantiate err with __IMPOSSIBLE__.
  tmpArray :: Array Int Int
  tmpArray :: Array Int Int
tmpArray = forall (a :: * -> * -> *) e i e'.
(IArray a e, Ix i) =>
(e -> e' -> e) -> e -> (i, i) -> [(i, e')] -> a 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..]

-- | Turn a possible non-surjective permutation into a surjective permutation.
compactP :: Permutation -> Permutation
compactP :: Permutation -> Permutation
compactP p :: Permutation
p@(Perm Int
_ [Int]
xs) = Int -> [Int] -> Permutation
Perm (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
xs) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Int -> Int
adjust [Int]
xs
  where
  missing :: IntSet
missing      = [Int] -> IntSet
IntSet.fromList forall a b. (a -> b) -> a -> b
$ Permutation -> [Int]
permPicks forall a b. (a -> b) -> a -> b
$ Permutation -> Permutation
droppedP Permutation
p
  holesBelow :: Int -> Int
holesBelow Int
k = IntSet -> Int
IntSet.size forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Int -> IntSet -> (IntSet, IntSet)
IntSet.split Int
k IntSet
missing
  adjust :: Int -> Int
adjust Int
k     = Int
k forall a. Num a => a -> a -> a
- Int -> Int
holesBelow Int
k

-- | @permute (reverseP p) xs ==
--    reverse $ permute p $ reverse xs@
--
--   Example:
--   @
--        permute (reverseP (Perm 4 [1,3,0])) [x0,x1,x2,x3]
--     == permute (Perm 4 $ map (3-) [0,3,1]) [x0,x1,x2,x3]
--     == permute (Perm 4 [3,0,2]) [x0,x1,x2,x3]
--     == [x3,x0,x2]
--     == reverse [x2,x0,x3]
--     == reverse $ permute (Perm 4 [1,3,0]) [x3,x2,x1,x0]
--     == reverse $ permute (Perm 4 [1,3,0]) $ reverse [x0,x1,x2,x3]
--   @
--
--   With @reverseP@, you can convert a permutation on de Bruijn indices
--   to one on de Bruijn levels, and vice versa.
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 $ Perm n $ reverse xs

-- | @permPicks (flipP p) = permute p (downFrom (permRange p))@
--   or
--   @permute (flipP (Perm n xs)) [0..n-1] = permute (Perm n xs) (downFrom n)@
--
--   Can be use to turn a permutation from (de Bruijn) levels to levels
--   to one from levels to indices.
--
--   See 'Agda.Syntax.Internal.Patterns.numberPatVars'.
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 i n π@ in the domain of @π@ replace the /i/th element by /n/ elements.
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]

-- | Stable topologic sort. The first argument decides whether its first
--   argument is an immediate parent to its second argument.
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 ]

------------------------------------------------------------------------
-- * Drop (apply) and undrop (abstract)
------------------------------------------------------------------------

-- | Delayed dropping which allows undropping.
data Drop a = Drop
  { forall a. Drop a -> Int
dropN    :: Int  -- ^ Non-negative number of things to drop.
  , forall a. Drop a -> a
dropFrom :: a    -- ^ Where to drop from.
  }
  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, 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)

-- | Things that support delayed dropping.
class DoDrop a where

  doDrop :: Drop a -> a              -- ^ Perform the dropping.

  dropMore :: Int -> Drop a -> Drop a  -- ^ Drop more.
  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  -- ^ Pick up dropped stuff.
  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) -- allow picking up more than dropped