module Language.Haskell.Liquid.List (transpose) where

{-@ lazy transpose @-}
transpose                  :: Int -> [[a]] -> [[a]]
transpose :: Int -> [[a]] -> [[a]]
transpose Int
_ []             = []
transpose Int
n ([]   : [[a]]
xss)   = Int -> [[a]] -> [[a]]
forall a. Int -> [[a]] -> [[a]]
transpose Int
n [[a]]
xss
transpose Int
n ((a
x:[a]
xs) : [[a]]
xss) = (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a
h | (a
h:[a]
_) <- [[a]]
xss]) [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: Int -> [[a]] -> [[a]]
forall a. Int -> [[a]] -> [[a]]
transpose (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) ([a]
xs [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [ [a]
t | (a
_:[a]
t) <- [[a]]
xss])