    {-# OPTIONS_GHC -Wunused-imports #-}

    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
    (Permutation -> Permutation -> Bool)
    -> (Permutation -> Permutation -> Bool) -> Eq Permutation
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Permutation -> Permutation -> Bool
    == :: Permutation -> Permutation -> Bool
    $c/= :: Permutation -> Permutation -> Bool
    /= :: Permutation -> Permutation -> Bool
    Eq, (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
    $cfrom :: forall x. Permutation -> Rep Permutation x
    from :: forall x. Permutation -> Rep Permutation x
    $cto :: forall x. Rep Permutation x -> Permutation
    to :: forall x. Rep Permutation x -> Permutation
    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
      natSize :: Permutation -> Peano
    natSize (Perm Int
    _ [Int]
    xs) = [Int] -> Peano
    forall a. Sized a => a -> Peano
    natSize [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@
    --
    -- 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 = IntMap a -> Int -> [a] -> [Int] -> [a]
    forall a. IntMap a -> Int -> [a] -> [Int] -> [a]
    go IntMap a
    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 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    n     = a -> Maybe a -> a
    forall a. a -> Maybe a -> a
    fromMaybe a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                        (Int -> IntMap a -> Maybe a
    forall a. Int -> IntMap a -> Maybe a
    IntMap.lookup Int
    i IntMap a
    seen) a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :
                      IntMap a -> Int -> [a] -> [Int] -> [a]
    forall a. IntMap a -> Int -> [a] -> [Int] -> [a]
    go IntMap a
    seen Int
    n [a]
    xs [Int]
    is
        | Bool
    otherwise = IntMap a -> Int -> [a] -> Int -> [Int] -> [a]
    forall a. IntMap a -> Int -> [a] -> Int -> [Int] -> [a]
    scan IntMap a
    seen Int
    n [a]
    xs (Int
    i Int -> Int -> Int
    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 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 = a
    x a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : (IntMap a -> Int -> [a] -> [Int] -> [a]
    forall a. IntMap a -> Int -> [a] -> [Int] -> [a]
    go (IntMap a -> Int -> [a] -> [Int] -> [a])
    -> IntMap a -> Int -> [a] -> [Int] -> [a]
    forall a b. (a -> b) -> a -> b
    $! IntMap a
    seen') Int
    n' [a]
    xs [Int]
    is
        | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0  = (IntMap a -> Int -> [a] -> Int -> [Int] -> [a]
    forall a. IntMap a -> Int -> [a] -> Int -> [Int] -> [a]
    scan (IntMap a -> Int -> [a] -> Int -> [Int] -> [a])
    -> IntMap a -> Int -> [a] -> Int -> [Int] -> [a]
    forall a b. (a -> b) -> a -> b
    $! IntMap a
    seen') Int
    n' [a]
    xs (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) [Int]
    is
        where
        seen' :: IntMap a
    seen' = Int -> a -> IntMap a -> IntMap a
    forall a. Int -> a -> IntMap a -> IntMap a
    IntMap.insert Int
    n a
    x IntMap a
    seen
        n' :: Int
    n'    = Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1
      scan IntMap a
    seen Int
    n [a]
    xs !Int
    _ [Int]
    is = a
    forall a. HasCallStack => a
    __IMPOSSIBLE__ a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : IntMap a -> Int -> [a] -> [Int] -> [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) = [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
    i -> Int -> a
    f (Int -> a) -> Maybe Int -> Maybe a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> IntMap Int -> Maybe Int
    forall a. Int -> IntMap a -> Maybe a
    IntMap.lookup Int
    i IntMap Int
    m
        where
        m :: IntMap Int
    m = (Int -> Int -> Int) -> [(Int, Int)] -> IntMap Int
    forall a. (a -> a -> a) -> [(Int, a)] -> IntMap a
    IntMapS.fromListWith ((Int -> Int -> Int) -> Int -> Int -> Int
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Int -> Int -> Int
    forall a b. a -> b -> a
    const) ([(Int, Int)] -> IntMap Int) -> [(Int, Int)] -> IntMap Int
    forall a b. (a -> b) -> a -> b
    $ [Int] -> [Int] -> [(Int, Int)]
    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 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 -> Bool) -> [Int] -> [Int]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (UArray Int Bool
    notInXs UArray Int Bool -> Int -> Bool
    forall (a :: * -> * -> *) e i.
    (IArray a e, Ix i) =>
    a i e -> i -> e
    !) [Int
    0 .. Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1]
      where
      notInXs :: UArray Int Bool
      notInXs :: UArray Int Bool
    notInXs =
        (Bool -> Bool -> Bool)
    -> Bool -> (Int, Int) -> [(Int, Bool)] -> UArray Int Bool
    forall (a :: * -> * -> *) e i e'.
    (IArray a e, Ix i) =>
    (e -> e' -> e) -> e -> (i, i) -> [(i, e')] -> a i e
    accumArray ((Bool -> Bool -> Bool) -> Bool -> Bool -> Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const) Bool
    True (Int
    0, Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) ([Int] -> [Bool] -> [(Int, Bool)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int]
    xs (Bool -> [Bool]
    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 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
    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]
    -- 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 (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 = (Int -> Int -> Int)
    -> Int -> (Int, Int) -> [(Int, Int)] -> Array Int Int
    forall (a :: * -> * -> *) e i e'.
    (IArray a e, Ix i) =>
    (e -> e' -> e) -> e -> (i, i) -> [(i, e')] -> a 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 p :: Permutation
    p@(Perm Int
    _ [Int]
    xs) = Int -> [Int] -> Permutation
    Perm ([Int] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Int]
    xs) ([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
      missing :: IntSet
    missing      = [Int] -> IntSet
    IntSet.fromList ([Int] -> IntSet) -> [Int] -> IntSet
    forall a b. (a -> b) -> a -> b
    $ Permutation -> [Int]
    permPicks (Permutation -> [Int]) -> Permutation -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Permutation -> Permutation
    droppedP Permutation
    p
      holesBelow :: Int -> Int
    holesBelow Int
    k = IntSet -> Int
    IntSet.size (IntSet -> Int) -> IntSet -> Int
    forall a b. (a -> b) -> a -> b
    $ (IntSet, IntSet) -> IntSet
    forall a b. (a, b) -> a
    fst ((IntSet, IntSet) -> IntSet) -> (IntSet, IntSet) -> IntSet
    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 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
      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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM ((a -> m [Int]) -> (Int, a) -> m (Int, [Int])
    forall (m :: * -> *) b d a.
    Functor m =>
    (b -> m d) -> (a, b) -> m (a, d)
    mapSndM a -> m [Int]
    parents) [(Int, a)]
    nodes
      return $ Perm (size xs) <$> topo g
      where

        topo :: Eq node => [(node, [node])] -> Maybe [node]
        topo :: forall node. Eq node => [(node, [node])] -> Maybe [node]
    topo [] = [node] -> Maybe [node]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        topo [(node, [node])]
    g  = case [node]
    xs of
          []    -> String -> Maybe [node]
    forall a. String -> Maybe a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail String
    "cycle detected"
          node
    x : [node]
    _ -> do
            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
            return $ x : 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
    $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
    /= :: 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
    $ccompare :: forall a. Ord a => Drop a -> Drop a -> Ordering
    compare :: Drop a -> Drop a -> Ordering
    $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
    >= :: Drop a -> Drop a -> Bool
    $cmax :: forall a. Ord a => Drop a -> Drop a -> Drop a
    max :: Drop a -> Drop a -> Drop a
    $cmin :: forall a. Ord a => Drop a -> Drop a -> Drop a
    min :: Drop a -> Drop a -> Drop a
    Ord, Int -> Drop a -> ShowS
    [Drop a] -> ShowS
    Drop a -> String
    (Int -> Drop a -> ShowS)
    -> (Drop a -> String) -> ([Drop a] -> ShowS) -> Show (Drop a)
    forall a. Show a => Int -> Drop a -> ShowS
    forall a. Show a => [Drop a] -> ShowS
    forall a. Show a => Drop a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Int -> Drop a -> ShowS
    showsPrec :: Int -> Drop a -> ShowS
    $cshow :: forall a. Show a => Drop a -> String
    show :: Drop a -> String
    $cshowList :: forall a. Show a => [Drop a] -> ShowS
    showList :: [Drop a] -> ShowS
    Show, (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
    $cfmap :: forall a b. (a -> b) -> Drop a -> Drop b
    fmap :: forall a b. (a -> b) -> Drop a -> Drop b
    $c<$ :: forall a b. a -> Drop b -> Drop a
    <$ :: forall a b. a -> Drop b -> Drop a
    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
    $cfold :: forall m. Monoid m => Drop m -> m
    fold :: forall m. Monoid m => Drop m -> 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
    foldMap' :: forall m a. Monoid m => (a -> m) -> Drop a -> m
    $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
    foldr' :: forall a b. (a -> b -> 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
    foldl' :: forall b a. (b -> a -> b) -> b -> Drop a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> Drop a -> a
    foldr1 :: forall a. (a -> a -> a) -> Drop a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Drop a -> a
    foldl1 :: forall a. (a -> a -> a) -> Drop a -> a
    $ctoList :: forall a. Drop a -> [a]
    toList :: forall a. Drop a -> [a]
    $cnull :: forall a. Drop a -> Bool
    null :: forall a. Drop a -> Bool
    $clength :: forall a. Drop a -> Int
    length :: forall a. Drop a -> Int
    $celem :: forall a. Eq a => a -> Drop a -> Bool
    elem :: forall a. Eq a => a -> Drop a -> Bool
    $cmaximum :: forall a. Ord a => Drop a -> a
    maximum :: forall a. Ord a => Drop a -> a
    $cminimum :: forall a. Ord a => Drop a -> a
    minimum :: forall a. Ord a => Drop a -> a
    $csum :: forall a. Num a => Drop a -> a
    sum :: forall a. Num a => Drop a -> a
    $cproduct :: forall a. Num a => Drop a -> a
    product :: forall a. Num a => Drop a -> a
    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)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Drop a -> f (Drop b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Drop a -> f (Drop b)
    $csequenceA :: forall (f :: * -> *) a. Applicative f => Drop (f a) -> f (Drop a)
    sequenceA :: forall (f :: * -> *) a. Applicative f => Drop (f a) -> f (Drop a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Drop a -> m (Drop b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Drop a -> m (Drop b)
    $csequence :: forall (m :: * -> *) a. Monad m => Drop (m a) -> m (Drop a)
    sequence :: forall (m :: * -> *) a. Monad m => Drop (m a) -> m (Drop a)
    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