module KMeansHelper where

import Prelude hiding (zipWith)
import Data.List (sort, span, minimumBy)
import Data.Function (on)
import Data.Ord (comparing)
import Language.Haskell.Liquid.Prelude (liquidAssert, liquidError)


-- | Fixed-Length Lists

{-@ type List a N = {v : [a] | (len v) = N} @-}


-- | N Dimensional Points

{-@ type Point N = List Double N @-}

{-@ type NonEmptyList a = {v : [a] | (len v) > 0} @-}

-- | Clustering 

{-@ type Clustering a  = [(NonEmptyList a)] @-}

------------------------------------------------------------------
-- | Grouping By a Predicate -------------------------------------
------------------------------------------------------------------

{-@ groupBy       :: (a -> a -> Bool) -> [a] -> (Clustering a) @-}
groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy a -> a -> Bool
_  []     =  []
groupBy a -> a -> Bool
eq (a
x:[a]
xs) =  (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys) [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: (a -> a -> Bool) -> [a] -> [[a]]
groupBy a -> a -> Bool
eq [a]
zs
  where ([a]
ys,[a]
zs)   = (a -> Bool) -> [a] -> ([a], [a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (a -> a -> Bool
eq a
x) [a]
xs

------------------------------------------------------------------
-- | Partitioning By a Size --------------------------------------
------------------------------------------------------------------

{-@ type PosInt = {v: Int | v > 0 } @-}

{-@ partition           :: size:PosInt -> xs:[a] -> (Clustering a) / [len xs] @-}

partition :: Int -> [a] -> [[a]]
partition Int
size []       = []
partition Int
size ys :: [a]
ys@(a
_:[a]
_) = [a]
zs [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: Int -> [a] -> [[a]]
partition Int
size [a]
zs'
  where
    zs :: [a]
zs                  = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
size [a]
ys
    zs' :: [a]
zs'                 = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
size [a]
ys

-----------------------------------------------------------------------
-- | Safe Zipping -----------------------------------------------------
-----------------------------------------------------------------------

{-@ zipWith :: (a -> b -> c) -> xs:[a] -> (List b (len xs)) -> (List c (len xs)) @-}
zipWith :: (t -> t -> a) -> [t] -> [t] -> [a]
zipWith t -> t -> a
f (t
a:[t]
as) (t
b:[t]
bs) = t -> t -> a
f t
a t
b a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (t -> t -> a) -> [t] -> [t] -> [a]
zipWith t -> t -> a
f [t]
as [t]
bs
zipWith t -> t -> a
_ [] []         = []

-- Other cases only for exposition
zipWith t -> t -> a
_ (t
_:[t]
_) []      = String -> [a]
forall a. String -> a
liquidError String
"Dead Code"
zipWith t -> t -> a
_ [] (t
_:[t]
_)      = String -> [a]
forall a. String -> a
liquidError String
"Dead Code"

-----------------------------------------------------------------------
-- | "Matrix" Transposition -------------------------------------------
-----------------------------------------------------------------------

{-@ type Matrix a Rows Cols  = (List (List a Cols) Rows) @-}

{-@ transpose                :: c:Int -> r:PosInt -> Matrix a r c -> Matrix a c r @-}

transpose                    :: Int -> Int -> [[a]] -> [[a]]
transpose :: Int -> Int -> [[a]] -> [[a]]
transpose Int
0 Int
_ [[a]]
_              = []
transpose Int
c Int
r ((a
x:[a]
xs) : [[a]]
xss) = (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: ([a] -> a) -> [[a]] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> a
forall a. [a] -> a
head [[a]]
xss) [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: Int -> Int -> [[a]] -> [[a]]
forall a. Int -> Int -> [[a]] -> [[a]]
transpose (Int
cInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
r ([a]
xs [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: ([a] -> [a]) -> [[a]] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> [a]
forall a. [a] -> [a]
tail [[a]]
xss)

-- Or, with comprehensions
-- transpose c r ((x:xs):xss) = (x : [ xs' | (x':_) <- xss ]) : transpose (c-1) r (xs : [xs' | (_ : xs') <- xss])

-- Not needed, just for exposition
transpose Int
c Int
r ([] : [[a]]
_)       = String -> [[a]]
forall a. String -> a
liquidError String
"dead code"
transpose Int
c Int
r []             = String -> [[a]]
forall a. String -> a
liquidError String
"dead code"