{-# LANGUAGE ScopedTypeVariables #-}

module Vec0 (dotProduct, safeLookup) where

import Prelude hiding (length)
import Data.Vector
import Language.Haskell.Liquid.Prelude (liquidAssert)
    
{-@ predicate Lt X Y      = X < Y                         @-}
{-@ predicate Ge X Y      = not (Lt X Y)                  @-}
{-@ predicate InBound I A = ((Ge I 0) && (Lt I (vlen A))) @-}

{-@ invariant {v:Int | v >= 0} @-}
{-@ unsafeLookup :: vec:Vector a 
                 -> {v: Int | (0 <= v && v < (vlen vec)) } 
                 -> a @-}
unsafeLookup vec i = vec ! i

{-@ unsafeLookup' :: vec:Vector a -> {v: Int | (InBound v vec)} -> a @-}
unsafeLookup' vec i = vec ! i

safeLookup x i 
  | 0 <= i && i < length x = Just (x ! i)
  | otherwise              = Nothing 

{-@ absoluteSum   :: Vector Int -> {v: Int | 0 <= v}  @-}
absoluteSum       :: Vector Int -> Int 
absoluteSum vec   = if 0 < n then go n 0 0 else 0
  where
    go (d::Int) acc i 
      | i /= n    = go (d-1) (acc + abz (vec ! i)) (i + 1)
      | otherwise = acc 
    n             = length vec

abz n = if 0 <= n then n else (0 - n) 

loop :: Int -> Int -> a -> (Int -> a -> a) -> a 
loop lo hi base f = go (hi-lo) base lo
  where
    {-@ decrease go 1 @-}
    go (d::Int) acc i     
      | i /= hi   = go (d-1) (f i acc) (i + 1)
      | otherwise = acc

incr x = x + 1

zoo = incr 29

{-@ dotProduct :: x:(Vector Int) 
               -> y:{v: Vector Int | (vlen v) = (vlen x)} 
               -> Int 
  @-}
dotProduct     :: Vector Int -> Vector Int -> Int
dotProduct x y 
  | length x == length y
  = loop 0 (length x) 0 (\i -> (+ (x ! i) * (y ! i))) 
  | otherwise
  = error "dotProduct only on equal-sized vectors!"


{-@ type SparseVector a N = [({v: Int | (0 <= v && v < N)}, a)] @-}

{-@ sparseDotProduct :: (Num a) => x:(Vector a) -> (SparseVector a {(vlen x)}) -> a @-}
sparseDotProduct x y  = go 0 y
  where
    {-@ decrease go 2 @-}
    go sum ((i, v) : y') = go (sum + (x ! i) * v) y' 
    go sum []            = sum