{-@ LIQUID "--no-termination" @-} {-@ LIQUID "--prune-unsorted" @-} module Tx (transpose, transpose', transpose'') where import Language.Haskell.Liquid.Prelude -- | Specifying a matrix {-@ type Matrix a = {m0:[{v:[a] | (len v) = (cols m0)}] | true } @-} {-@ type MatrixCR a C R = {m0:[{v:[a] | (len v) = C}] | (((len m0) = R) && (R > 0 => (cols m0) = C)) } @-} {-@ measure cols :: [[a]] -> Int cols ([]) = 0 cols (x:xs) = (len x) @-} -- | A Few Simple Examples (which run VERY slowly) {-@ predicate Dim V C R = (((len V) = R) && ((cols V) = C)) @-} {-@ mat_3_2 :: {v: Matrix Int | (Dim v 3 2)} @-} mat_3_2 :: [[Int]] mat_3_2 = [ [1,2,3] , [4,5,6] ] {-@ mat_2_4 :: {v: Matrix Int | (Dim v 2 4)} @-} mat_2_4 :: [[Int]] mat_2_4 = [ [1,2] , [3,4] , [5,6] , [7,8] ] -- | Old fashioned transpose with explicit dimensions {- transpose :: c:Nat -> r:{v:Nat | v > 0} -> {v:[{v:[a] | (len v) = c}] | (len v) = r} -> {v:[{v:[a] | (len v) = r}] | (len v) = c} -} {-@ transpose :: c:Nat -> r:{v:Nat | v > 0} -> (MatrixCR a c r) -> (MatrixCR a r c) @-} transpose :: Int -> Int -> [[a]] -> [[a]] transpose 0 _ _ = [] transpose n m ((x:xs) : xss) = (x : map head xss) : transpose (n - 1) m (xs : map tail xss) transpose n m ([] : _) = liquidError "transpose1" transpose n m [] = liquidError "transpose2" {-@ transpose' :: m:{v:(Matrix a) | ((len v) > 0)} -> (MatrixCR a (len m) (cols m)) @-} transpose' :: [[a]] -> [[a]] transpose' ([]:_) = [] transpose' ((x:xs) : xss) = (x : map head xss) : transpose' (xs : map tail xss) transpose' [] = liquidError "transpose'" -- | A wrapper implementing the explicit transpose using the implicit one {-@ transpose'' :: c:Nat -> r:{v:Nat | v > 0} -> (MatrixCR a c r) -> (MatrixCR a r c) @-} transpose'' :: Int -> Int -> [[a]] -> [[a]] transpose'' n m xss = transpose' xss