{-@ LIQUID "--totality" @-} 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