{-# LANGUAGE CPP #-} {-# 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 #include "undefined.h" 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 { permRange :: Int, permPicks :: [Int] } deriving (Eq, Data) instance Show Permutation where show (Perm n xs) = showx [0..n - 1] ++ " -> " ++ showx xs where showx = showList "," (\ i -> "x" ++ show i) showList :: String -> (a -> String) -> [a] -> String showList sep f [] = "" showList sep f [e] = f e showList sep f (e:es) = f e ++ sep ++ showList sep f es instance Sized Permutation where size (Perm _ xs) = size xs instance Null Permutation where empty = Perm 0 [] null (Perm _ picks) = null picks instance KillRange Permutation where killRange = 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 p xs = map (fromMaybe __IMPOSSIBLE__) (safePermute p xs) safePermute :: Permutation -> [a] -> [Maybe a] safePermute (Perm _ is) xs = map (xs !!!!) is where xs !!!! n | n < 0 = Nothing | otherwise = xs !!! 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 (Perm n is) = catMaybes . zipWith (\ i ma -> (i,) <$> ma) is instance InversePermute [Maybe a] (IntMap a) where inversePermute p = IntMap.fromList . inversePermute p instance InversePermute [Maybe a] [Maybe a] where inversePermute p@(Perm n _) = tabulate . inversePermute p where tabulate m = for [0..n-1] $ \ i -> IntMap.lookup i m instance InversePermute (Int -> a) [Maybe a] where inversePermute (Perm n xs) f = for [0..n-1] $ \ x -> f <$> List.findIndex (x ==) xs -- | Identity permutation. idP :: Int -> Permutation idP n = Perm n [0..n - 1] -- | Restrict a permutation to work on @n@ elements, discarding picks @>=n@. takeP :: Int -> Permutation -> Permutation takeP n (Perm m xs) = Perm n $ filter (< n) xs -- | Pick the elements that are not picked by the permutation. droppedP :: Permutation -> Permutation droppedP (Perm n xs) = Perm n $ [0..n-1] List.\\ 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 n (Perm m xs) = Perm (n + m) $ xs ++ [m..m+n-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 p1 (Perm n xs) = Perm n $ permute p1 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 err p@(Perm n xs) = Perm (size xs) $ elems tmpArray where tmpArray = accumArray (flip const) err (0, n-1) $ zip xs [0..] -- | Turn a possible non-surjective permutation into a surjective permutation. compactP :: Permutation -> Permutation compactP (Perm n xs) = Perm m $ map adjust xs where m = List.genericLength xs missing = [0..n - 1] List.\\ xs holesBelow k = List.genericLength $ filter (< k) missing adjust k = k - holesBelow 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 (Perm n xs) = Perm n $ map ((n - 1) -) $ reverse 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 (Perm n xs) = Perm n $ map (n - 1 -) xs -- | @expandP i n π@ in the domain of @π@ replace the /i/th element by /n/ elements. expandP :: Int -> Int -> Permutation -> Permutation expandP i n (Perm m xs) = Perm (m + n - 1) $ concatMap expand xs where expand j | j == i = [i..i + n - 1] | j < i = [j] | otherwise = [j + n - 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 parent xs = fmap (Perm (size xs)) $ topo g where nodes = zip [0..] xs g = [ (n, parents x) | (n, x) <- nodes ] parents x = [ n | (n, y) <- nodes, parent y x ] topo :: Eq node => [(node, [node])] -> Maybe [node] topo [] = return [] topo g = case xs of [] -> fail "cycle detected" x : _ -> do ys <- topo $ remove x g return $ x : ys where xs = [ x | (x, []) <- g ] remove x g = [ (y, filter (/= x) ys) | (y, ys) <- g, x /= y ] ------------------------------------------------------------------------ -- * Drop (apply) and undrop (abstract) ------------------------------------------------------------------------ -- | Delayed dropping which allows undropping. data Drop a = Drop { dropN :: Int -- ^ Non-negative number of things to drop. , dropFrom :: a -- ^ Where to drop from. } deriving (Eq, Ord, Show, Data, Functor, Foldable, Traversable) instance KillRange a => KillRange (Drop a) where killRange = fmap 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 n (Drop m xs) = Drop (m + n) xs unDrop :: Int -> Drop a -> Drop a -- ^ Pick up dropped stuff. unDrop n (Drop m xs) | n <= m = Drop (m - n) xs | otherwise = __IMPOSSIBLE__ instance DoDrop [a] where doDrop (Drop m xs) = List.drop m xs instance DoDrop Permutation where doDrop (Drop k (Perm n xs)) = Perm (n + m) $ [0..m-1] ++ map (+ m) (List.drop k xs) where m = -k unDrop m = dropMore (-m) -- allow picking up more than dropped