module X2 where


----------------------------------------------------------------------
-- Exercise 2 : Vectors                                             --
----------------------------------------------------------------------

-- LIBRARY

data Nat : Set where
  zero  : Nat
  suc   : Nat -> Nat

data _^_ (X : Set) : Nat -> Set where
  [] : X ^ zero
  _::_ : {n : Nat} -> X -> X ^ n -> X ^ suc n

_+_ : Nat -> Nat -> Nat
zero + y = y
suc x + y = suc (x + y)

data Maybe (X : Set) : Set where
  just : X -> Maybe X
  nothing : Maybe X

vec : {n : Nat}{X : Set} -> X -> X ^ n
vec {zero} x = []
vec {suc n} x = x :: vec {n} x

_$s_ : {n : Nat}{S T : Set} -> (S -> T) ^ n -> S ^ n -> T ^ n
[]        $s []         = []
(f :: fs) $s (s :: ss)  = f s :: (fs $s ss)

infixl 90 _$s_


-- EXERCISES (usual hints apply)


-- Vector basics

{- (2.1) Implement vector concatenation. (Guess the length!) -}

_++_ : {m n : Nat}{X : Set} -> X ^ m -> X ^ n -> X ^ {! !}
xs ++ ys = {! !} 

{- (2.2) Show how to compute the sum a vector of numbers. -}

sum : {n : Nat} -> Nat ^ n -> Nat
sum xs = {! !}

{- (2.3) Compute the scalar product of two vectors (the sum of the
   products of corresponding elements). You'll need to define
   multiplication, of course. -}

_times_ : Nat -> Nat -> Nat
m times n = {! !}

_dot_ : {n : Nat} -> Nat ^ n -> Nat ^ n -> Nat
xs dot ys = {! !}

{- (2.4) Define Maybe-application, returning a value where possible. -}

_$m_ : {S T : Set} -> Maybe (S -> T) -> Maybe S -> Maybe T
fm $m sm = {! !}

{- Compare (vec, _$s_) with (just, _$m_). Do you see a pattern? -}

{- (2.5) Show how to construct a vector of values from a vector of
   maybe-values, provided they are all "just". -}

allJust : {n : Nat}{X : Set} -> Maybe X ^ n -> Maybe (X ^ n)
allJust xms = {! !}


-- Matrices: rows of columns

Matrix : Set -> Nat -> Nat -> Set
Matrix X m n = (X ^ m) ^ n

{- (2.6) Define the identity matrix of a given size
         (one on the diagonal, zero off) -}

identity : {n : Nat} -> Matrix Nat n n
identity {n} = {! !}

{- (2.7*) Define matrix transposition. -}

transpose : {m n : Nat}{X : Set} -> Matrix X m n -> Matrix X n m
transpose xmn = {! !}

{- (2.8) Define matrix multiplication. -}

_mmult_ : {l m n : Nat} -> Matrix Nat l m -> Matrix Nat m n -> Matrix Nat l n
xlm mmult xmn = {! !}