module Vectors where

import Prelude hiding (sum, product, zipWith)

flatten :: Int -> Int -> [[a]] -> [a]

-- | Lets reuse plain lists

type Vec a = [a]

-- | The `len` function is defined in the LH prelude as:
{-

   len        :: [a] -> Int
   len []     = 0
   len (_:xs) = 1 + len xs
-}

             
{-@ type VecN a N = {v : Vec a | len v = N} @-}

{-@ product   :: xs:Vec a -> ys:Vec a -> VecN a {len xs * len ys} @-}
product xs ys = flatten n m $ map (\y -> map (* y) xs) ys
  where
    m         = length xs
    n         = length ys

{-@ sum       :: xs:Vec a -> ys:VecN a {len xs}-> VecN a {len xs} @-}
sum xs ys     = zipWith (+) xs ys

{-@ sum'       :: xs:Vec a -> ys:Vec a -> VecN a {len xs + len ys} @-}
sum' [] ys     = ys
sum' (x:xs) ys = x : sum' xs ys

{-@ example1   :: b:VecN _ 3 -> VecN _ 6 @-}
example1 b     = ([1, 2] `product` b) `sum` [1, 2, 3, 4, 5, 6]
    
{-@ example2   :: a:Vec _ -> b:{Vec _ | len b * len a = 6} -> VecN _ 6 @-}
example2 a b   = (a `product` b) `sum` [1,2,3,4,5,6]


-- Helpers --


{-@ flatten          :: n:Nat -> m:Nat -> VecN (VecN a m) n -> VecN a {m * n} @-}
flatten n m []       = []
flatten n m (xs:xss) = xs ++ flatten (n-1) m xss 


{-@ zipWith             :: (a -> b -> c) -> xs:Vec a -> ys:VecN b {len xs} -> VecN c {len xs} @-}
zipWith f [] []         = []
zipWith f (x:xs) (y:ys) = f x y : zipWith f xs ys




{-@ lAssert :: TT -> a -> a@-}
lAssert True x = x