    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

    -- | 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
    (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
    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 -> DataType
    Permutation -> Constr
    (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. Permutation -> Rep Permutation x)
    -> (forall x. Rep Permutation x -> Permutation)
    -> Generic Permutation
    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 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1] String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " -> " 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 String
    "," (\ Int
    i -> String
    "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 :: 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 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 Int
    _ [Int]
    xs) = [Int] -> Int
    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) = [Int] -> Bool
    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@
    permute :: Permutation -> [a] -> [a]
    permute :: forall a. Permutation -> [a] -> [a]
    permute Permutation
    p [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 :: forall a. Permutation -> [a] -> [Maybe a]
    safePermute (Perm Int
    _ [Int]
    is) [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
        [a]
    xs !!!! :: [a] -> Int -> Maybe a
    !!!! Int
    n | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    0     = Maybe a
    forall a. Maybe a
    Nothing
                  | Bool
    otherwise = [a]
    xs [a] -> Int -> Maybe a
    forall {a}. [a] -> Int -> Maybe a
    !!! Int
    n

    -- |  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) = [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 (\ Int
    i 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 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 Int
    n [Int]
    _) = 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 IntMap a
    m = [Int] -> (Int -> Maybe a) -> [Maybe a]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [Int
    0..Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1] ((Int -> Maybe a) -> [Maybe a]) -> (Int -> Maybe a) -> [Maybe a]
    forall a b. (a -> b) -> a -> b
    $ \ 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 Int
    n [Int]
    xs) Int -> a
    f = [Int] -> (Int -> Maybe a) -> [Maybe a]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [Int
    0..Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1] ((Int -> Maybe a) -> [Maybe a]) -> (Int -> Maybe a) -> [Maybe a]
    forall a b. (a -> b) -> a -> b
    $ \ 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

    -- | Identity permutation.
    idP :: Int -> Permutation
    idP :: Int -> Permutation
    idP Int
    n = Int -> [Int] -> Permutation
    Perm Int
    n [Int
    0..Int
    n Int -> Int -> Int
    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 ([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

    -- | 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 ([Int] -> Permutation) -> [Int] -> Permutation
    forall a b. (a -> b) -> a -> b
    $ [Int
    0..Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1] [Int] -> [Int] -> [Int]
    forall a. Eq a => [a] -> [a] -> [a]
    List.\\ [Int]
    xs

    -- | @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 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
    -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 ([Int] -> Permutation) -> [Int] -> Permutation
    forall a b. (a -> b) -> a -> b
    $ Permutation -> [Int] -> [Int]
    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 ([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
    forall a b. a -> b -> a
    const Int -> Int
    forall a. a -> a
    id) Int
    err (Int
    0, Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    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 [Int
    0..]

    -- | Turn a possible non-surjective permutation into a surjective permutation.
    compactP :: Permutation -> Permutation
    compactP :: Permutation -> Permutation
    compactP (Perm Int
    n [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      = [Int
    0..Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1] [Int] -> [Int] -> [Int]
    forall a. Eq a => [a] -> [a] -> [a]
    List.\\ [Int]
    xs
        holesBelow :: Int -> Int
    holesBelow Int
    k = [Int] -> Int
    forall i a. Num i => [a] -> i
    List.genericLength ([Int] -> Int) -> [Int] -> Int
    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 Int
    k = Int
    k Int -> Int -> Int
    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 ([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
    - Int
    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 $ 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 ([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
    - Int
    1 Int -> Int -> Int
    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 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    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 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
    - Int
    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
    - 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 = Identity (Maybe Permutation) -> Maybe Permutation
    forall a. Identity a -> a
    runIdentity (Identity (Maybe Permutation) -> Maybe Permutation)
    -> Identity (Maybe Permutation) -> Maybe Permutation
    forall a b. (a -> b) -> a -> b
    $ (a -> a -> Identity Bool) -> [a] -> Identity (Maybe Permutation)
    forall (m :: * -> *) a.
    Monad m =>
    (a -> a -> m Bool) -> [a] -> m (Maybe Permutation)
    topoSortM (\a
    x a
    y -> Bool -> Identity Bool
    forall a. a -> Identity a
    Identity (Bool -> Identity Bool) -> Bool -> Identity Bool
    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     = [Int] -> [a] -> [(Int, a)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int
    0..] [a]
    xs
          parents :: a -> m [Int]
    parents a
    x = ((Int, a) -> Int) -> [(Int, a)] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, a) -> Int
    forall a b. (a, b) -> a
    fst ([(Int, a)] -> [Int]) -> m [(Int, a)] -> m [Int]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Int, a) -> m Bool) -> [(Int, a)] -> m [(Int, a)]
    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 <- ((Int, a) -> m (Int, [Int])) -> [(Int, a)] -> m [(Int, [Int])]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((a -> m [Int]) -> (Int, a) -> m (Int, [Int])
    forall (m :: * -> *) b d a.
    Applicative m =>
    (b -> m d) -> (a, b) -> m (a, d)
    mapSndM a -> m [Int]
    parents) [(Int, a)]
    nodes
      Maybe Permutation -> m (Maybe Permutation)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Permutation -> m (Maybe Permutation))
    -> Maybe Permutation -> m (Maybe Permutation)
    forall a b. (a -> b) -> a -> b
    $ 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

        topo :: Eq node => [(node, [node])] -> Maybe [node]
        topo :: forall node. Eq node => [(node, [node])] -> Maybe [node]
    topo [] = [node] -> Maybe [node]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        topo [(node, [node])]
    g  = case [node]
    xs of
          []    -> String -> Maybe [node]
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail String
    "cycle detected"
          node
    x : [node]
    _ -> 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 | (node
    x, []) <- [(node, [node])]
    g ]
            remove :: a -> [(a, [a])] -> [(a, [a])]
    remove a
    x [(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) | (a
    y, [a]
    ys) <- [(a, [a])]
    g, a
    x a -> a -> Bool
    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
    (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
    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)
    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 -> DataType
    Drop a -> Constr
    (forall b. Data b => b -> b) -> Drop a -> Drop a
    forall {a}. Data a => Typeable (Drop a)
    forall a. Data a => Drop a -> DataType
    forall a. Data a => Drop a -> Constr
    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))
    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 -> 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
    <$ :: 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 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 :: 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
    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
    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) = 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  -- ^ Pick up dropped stuff.
      unDrop Int
    n (Drop Int
    m 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 Int
    m [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 Int
    k (Perm Int
    n [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
    0..Int
    mInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    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 Int
    m = Int -> Drop Permutation -> Drop Permutation
    forall a. DoDrop a => Int -> Drop a -> Drop a
    dropMore (-Int
    m) -- allow picking up more than dropped