{-# LANGUAGE ScopedTypeVariables #-}
module List () where
{-@ decrease go 3 4 5 @-}
{-@ decrease perms 4 5 6 @-}
{-@ foo :: xs:[a] -> ys:[a] -> {v:Int| v = (len xs)- (len ys)} -> Int @-}
foo :: [a] -> [a] -> Int -> Int
foo = undefined
permutations :: [a] -> [[a]]
permutations xs = go xs xs (length xs) (length xs) 1
where
go xs0 xs (d2 :: Int) d1 (d3::Int) = xs : perms xs0 xs [] d2 d1 0
perms _ [] _ _ _ _ = []
perms xs0 (t:ts) is (d2 :: Int) (d1::Int) (d3 :: Int) = (perms ts xs0 (t:is) d2 (length ts) d3) ++ (go xs0 is (length xs0 - length is) d1 1)
-- permutations :: [a] -> [[a]]
-- permutations xs = go xs xs (length xs) (0::Int) 1
-- where
-- go xs0 xs d1 (d2::Int) (d3::Int) = xs : perms xs0 xs [] d1 0 0
-- perms _ [] _ _ _ _ = []
-- perms xs0 (t:ts) is (d1::Int) (d2 :: Int) (d3 :: Int) = (perms ts xs0 (t:is) (length ts) 0 d3) ++ (go xs0 is (length is) 0 1)
--
--