{-# LANGUAGE DeriveDataTypeable    #-}

module Agda.Utils.Permutation where

import Prelude hiding (drop, null)

import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.List as List
import Data.Maybe
import Data.Array

import Data.Foldable (Foldable)
import Data.Traversable (Traversable)

import Data.Data (Data)

import Agda.Syntax.Position (KillRange(..))
import Agda.Utils.Functor
import Agda.Utils.List ((!!!))
import Agda.Utils.Null
import Agda.Utils.Size

import Agda.Utils.Impossible

-- | 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
DataType
Constr
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 d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Permutation -> c Permutation
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Permutation
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Permutation -> u
forall u. (forall d. Data d => d -> u) -> Permutation -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Permutation -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Permutation -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Permutation -> m Permutation
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Permutation -> m Permutation
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Permutation
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Permutation -> c Permutation
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Permutation)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Permutation)
$cPerm :: Constr
$tPermutation :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Permutation -> m Permutation
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Permutation -> m Permutation
gmapMp :: (forall d. Data d => d -> m d) -> Permutation -> m Permutation
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Permutation -> m Permutation
gmapM :: (forall d. Data d => d -> m d) -> Permutation -> m Permutation
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Permutation -> m Permutation
gmapQi :: Int -> (forall d. Data d => d -> u) -> Permutation -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Permutation -> u
gmapQ :: (forall d. Data d => d -> u) -> Permutation -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Permutation -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Permutation -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Permutation -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Permutation -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Permutation -> r
gmapT :: (forall b. Data b => b -> b) -> Permutation -> Permutation
$cgmapT :: (forall b. Data b => b -> b) -> Permutation -> Permutation
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Permutation)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Permutation)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Permutation)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Permutation)
dataTypeOf :: Permutation -> DataType
$cdataTypeOf :: Permutation -> DataType
toConstr :: Permutation -> Constr
$ctoConstr :: Permutation -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Permutation
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Permutation
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Permutation -> c Permutation
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Permutation -> c Permutation
$cp1Data :: Typeable Permutation
Data)

instance Show Permutation where
  show :: Permutation -> String
show (Perm 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 :: 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 KillRange Permutation where
  killRange :: Permutation -> Permutation
killRange = Permutation -> Permutation
forall a. a -> a
id

-- | @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 :: 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 :: 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]
forall a. IntMap a -> [Maybe a]
tabulate (IntMap a -> [Maybe a])
-> ([Maybe a] -> IntMap a) -> [Maybe a] -> [Maybe a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Permutation -> [Maybe a] -> IntMap a
forall a b. InversePermute a b => Permutation -> a -> b
inversePermute Permutation
p
    where tabulate :: IntMap a -> [Maybe a]
tabulate 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 -> Int
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Int -> Int
forall a b. a -> b -> a
const) 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 -> i
holesBelow Int
k = [Int] -> i
forall i a. Num i => [a] -> i
List.genericLength ([Int] -> i) -> [Int] -> i
forall a b. (a -> b) -> a -> b
$ (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k) [Int]
missing
    adjust :: Int -> Int
adjust Int
k = Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int -> Int
forall i. Num i => Int -> i
holesBelow Int
k

-- | @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 :: (a -> a -> Bool) -> [a] -> Maybe Permutation
topoSort a -> a -> Bool
parent [a]
xs = Int -> [Int] -> Permutation
Perm ([a] -> Int
forall a. Sized a => a -> Int
size [a]
xs) ([Int] -> Permutation) -> Maybe [Int] -> Maybe Permutation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, [Int])] -> Maybe [Int]
forall node. Eq node => [(node, [node])] -> Maybe [node]
topo [(Int, [Int])]
g
  where
    nodes :: [(Int, a)]
nodes     = [Int] -> [a] -> [(Int, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [a]
xs
    g :: [(Int, [Int])]
g         = [ (Int
n, a -> [Int]
parents a
x) | (Int
n, a
x) <- [(Int, a)]
nodes ]
    parents :: a -> [Int]
parents a
x = [ Int
n | (Int
n, a
y) <- [(Int, a)]
nodes, a -> a -> Bool
parent a
y a
x ]

    topo :: Eq node => [(node, [node])] -> Maybe [node]
    topo :: [(node, [node])] -> Maybe [node]
topo [] = [node] -> Maybe [node]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    topo [(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
  { Drop a -> Int
dropN    :: Int  -- ^ Non-negative number of things to drop.
  , 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
$cp1Ord :: forall a. Ord a => Eq (Drop a)
Ord, Int -> Drop a -> ShowS
[Drop a] -> ShowS
Drop a -> String
(Int -> Drop a -> ShowS)
-> (Drop a -> String) -> ([Drop a] -> ShowS) -> Show (Drop a)
forall a. Show a => Int -> Drop a -> ShowS
forall a. Show a => [Drop a] -> ShowS
forall a. Show a => Drop a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Drop a] -> ShowS
$cshowList :: forall a. Show a => [Drop a] -> ShowS
show :: Drop a -> String
$cshow :: forall a. Show a => Drop a -> String
showsPrec :: Int -> Drop a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Drop a -> ShowS
Show, Typeable (Drop a)
DataType
Constr
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 d. Data d => c (t d)) -> Maybe (c (Drop a))
(forall b. Data b => b -> b) -> Drop a -> Drop a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Drop a -> c (Drop a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Drop a)
forall a. Data a => Typeable (Drop a)
forall a. Data a => Drop a -> 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))
$cDrop :: Constr
$tDrop :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Drop a -> m (Drop a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Drop a -> m (Drop a)
gmapMp :: (forall d. Data d => d -> m d) -> Drop a -> m (Drop a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Drop a -> m (Drop a)
gmapM :: (forall d. Data d => d -> m d) -> Drop a -> m (Drop a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Drop a -> m (Drop a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Drop a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Drop a -> u
gmapQ :: (forall d. Data d => d -> u) -> Drop a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Drop a -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Drop a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Drop a -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Drop a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Drop a -> r
gmapT :: (forall b. Data b => b -> b) -> Drop a -> Drop a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Drop a -> Drop a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Drop a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Drop a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Drop a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Drop a))
dataTypeOf :: Drop a -> DataType
$cdataTypeOf :: forall a. Data a => Drop a -> DataType
toConstr :: Drop a -> Constr
$ctoConstr :: forall a. Data a => Drop a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Drop a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Drop a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Drop a -> c (Drop a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Drop a -> c (Drop a)
$cp1Data :: forall a. Data a => Typeable (Drop a)
Data, a -> Drop b -> Drop a
(a -> b) -> Drop a -> Drop b
(forall a b. (a -> b) -> Drop a -> Drop b)
-> (forall a b. a -> Drop b -> Drop a) -> Functor Drop
forall a b. a -> Drop b -> Drop a
forall a b. (a -> b) -> Drop a -> Drop b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Drop b -> Drop a
$c<$ :: forall a b. a -> Drop b -> Drop a
fmap :: (a -> b) -> Drop a -> Drop b
$cfmap :: forall a b. (a -> b) -> Drop a -> Drop b
Functor, Drop a -> Bool
(a -> m) -> Drop a -> m
(a -> b -> b) -> b -> Drop a -> b
(forall m. Monoid m => Drop m -> m)
-> (forall m a. Monoid m => (a -> m) -> Drop a -> m)
-> (forall m a. Monoid m => (a -> m) -> Drop a -> m)
-> (forall a b. (a -> b -> b) -> b -> Drop a -> b)
-> (forall a b. (a -> b -> b) -> b -> Drop a -> b)
-> (forall b a. (b -> a -> b) -> b -> Drop a -> b)
-> (forall b a. (b -> a -> b) -> b -> Drop a -> b)
-> (forall a. (a -> a -> a) -> Drop a -> a)
-> (forall a. (a -> a -> a) -> Drop a -> a)
-> (forall a. Drop a -> [a])
-> (forall a. Drop a -> Bool)
-> (forall a. Drop a -> Int)
-> (forall a. Eq a => a -> Drop a -> Bool)
-> (forall a. Ord a => Drop a -> a)
-> (forall a. Ord a => Drop a -> a)
-> (forall a. Num a => Drop a -> a)
-> (forall a. Num a => Drop a -> a)
-> Foldable Drop
forall a. Eq a => a -> Drop a -> Bool
forall a. Num a => Drop a -> a
forall a. Ord a => Drop a -> a
forall m. Monoid m => Drop m -> m
forall a. Drop a -> Bool
forall a. Drop a -> Int
forall a. Drop a -> [a]
forall a. (a -> a -> a) -> Drop a -> a
forall m a. Monoid m => (a -> m) -> Drop a -> m
forall b a. (b -> a -> b) -> b -> Drop a -> b
forall a b. (a -> b -> b) -> b -> Drop a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Drop a -> a
$cproduct :: forall a. Num a => Drop a -> a
sum :: Drop a -> a
$csum :: forall a. Num a => Drop a -> a
minimum :: Drop a -> a
$cminimum :: forall a. Ord a => Drop a -> a
maximum :: Drop a -> a
$cmaximum :: forall a. Ord a => Drop a -> a
elem :: a -> Drop a -> Bool
$celem :: forall a. Eq a => a -> Drop a -> Bool
length :: Drop a -> Int
$clength :: forall a. Drop a -> Int
null :: Drop a -> Bool
$cnull :: forall a. Drop a -> Bool
toList :: Drop a -> [a]
$ctoList :: forall a. Drop a -> [a]
foldl1 :: (a -> a -> a) -> Drop a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Drop a -> a
foldr1 :: (a -> a -> a) -> Drop a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Drop a -> a
foldl' :: (b -> a -> b) -> b -> Drop a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Drop a -> b
foldl :: (b -> a -> b) -> b -> Drop a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Drop a -> b
foldr' :: (a -> b -> b) -> b -> Drop a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Drop a -> b
foldr :: (a -> b -> b) -> b -> Drop a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Drop a -> b
foldMap' :: (a -> m) -> Drop a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Drop a -> m
foldMap :: (a -> m) -> Drop a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Drop a -> m
fold :: Drop m -> m
$cfold :: forall m. Monoid m => Drop m -> m
Foldable, Functor Drop
Foldable Drop
Functor Drop
-> Foldable Drop
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Drop a -> f (Drop b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Drop (f a) -> f (Drop a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Drop a -> m (Drop b))
-> (forall (m :: * -> *) a. Monad m => Drop (m a) -> m (Drop a))
-> Traversable Drop
(a -> f b) -> Drop a -> f (Drop b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Drop (m a) -> m (Drop a)
forall (f :: * -> *) a. Applicative f => Drop (f a) -> f (Drop a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Drop a -> m (Drop b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Drop a -> f (Drop b)
sequence :: Drop (m a) -> m (Drop a)
$csequence :: forall (m :: * -> *) a. Monad m => Drop (m a) -> m (Drop a)
mapM :: (a -> m b) -> Drop a -> m (Drop b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Drop a -> m (Drop b)
sequenceA :: Drop (f a) -> f (Drop a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Drop (f a) -> f (Drop a)
traverse :: (a -> f b) -> Drop a -> f (Drop b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Drop a -> f (Drop b)
$cp2Traversable :: Foldable Drop
$cp1Traversable :: Functor Drop
Traversable)

instance KillRange a => KillRange (Drop a) where
  killRange :: KillRangeT (Drop a)
killRange = (a -> a) -> KillRangeT (Drop a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
forall a. KillRange a => KillRangeT a
killRange

-- | 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