on master help sign in
Merge pull request #4586 from bossmc/master

`total` implementation for `List.transpose`

commit595cfb4795dd8e8c4e5cbdba32fe9081748e90e2 authorNiklas Larsson <metaniklas@gmail.com> dateMon 19 Nov 2018, 14:26 (8 years ago) parenta2440993c8f2d6
1 file changed+4−4
libs/prelude/Prelude/List.idr+4−4
libs/prelude/Prelude/List.idr+4−4
@@ -436,12 +436,12 @@ intercalate sep xss = concat $ intersperse sep xss
436436|||
437437||| transpose [[], [1, 2]] = [[1], [2]]
438438||| transpose (transpose [[], [1, 2]]) = [[1, 2]]
439−|||
440−||| TODO: Solution which satisfies the totality checker?
441439transpose : List (List a) -> List (List a)
442440transpose [] = []
443−transpose ([] :: xss) = transpose xss
444−transpose ((x::xs) :: xss) = assert_total $ (x :: (mapMaybe head' xss)) :: (transpose (xs :: (map (drop 1) xss)))
441+transpose (heads :: tails) = spreadHeads heads (transpose tails) where
442+ spreadHeads [] tails = tails
443+ spreadHeads (head :: heads) [] = [head] :: spreadHeads heads []
444+ spreadHeads (head :: heads) (tail :: tails) = (head :: tail) :: spreadHeads heads tails
445445
446446--------------------------------------------------------------------------------
447447-- Membership tests