module Lunes where

{-
data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

{- C-c C-l runs the type checker. -}
{- ℕ = \bn, → = \to -}

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)
{- C-c C-c splits cases -}
{- C-c C-r refines the problem -}
-}

open import Data.Nat
{- look up using M-click -}
open import Data.Bool

{- evaluate using C-c C-n -}

{- Write a function to decide equality of natural numbers,
   eq m n = true, if m=n
   eq m n = false, otherwise
-}
eq :     Bool --EX
eq zero zero = true
eq zero (suc n) = false
eq (suc n) zero = false
eq (suc n) (suc n') = eq n n'

open import Data.List

snoc : {A : Set}  List A  A  List A
snoc [] a = a  []
snoc {A} (x  xs) a = x  snoc {A} xs a
{- C-c SPC to type check what I have written. -}

{- {A : Set} .. is an implicit parameter, it is inserted by the
   compiler. -}

rev : {A : Set}  List A  List A
rev [] = []
rev (x  xs) = snoc (rev xs) x

data  : Set where

open import Data.Maybe

{- return nth element of a list. -}
_!!_ : {A : Set}  List A    Maybe A
[] !! n = nothing
(a  as) !! zero = just a
(a  as) !! suc n = as !! n
-- write the function with three lines!

open import Data.Vec

snoc' : {A : Set}{n : }  Vec A n  A  Vec A (suc n)
snoc' [] a = a  []
snoc' (x  xs) a = x  (snoc' xs a)

rev' : {A : Set}{n : }  Vec A n  Vec A n
rev' [] = []
rev' (x  xs) = snoc' (rev' xs) x

open import Data.Fin hiding (_+_) 

enum : (n : )  Vec (Fin n) n
enum zero = []
enum (suc n) = zero  Data.Vec.map suc (enum n)

max : {n : }  Fin (suc n)
max {zero} = zero {0}
max {suc n} = suc (max {n})

emb : {n : }  Fin n  Fin (suc n)
emb zero = zero
emb (suc i) = suc (emb i)

inv : {n : }  Fin n  Fin n
inv zero = max
inv (suc i) = emb (inv i)

_!!'_ : {A : Set}{n : }  Vec A n  Fin n  A
[] !!' () -- impossible pattern
(x  xs) !!' zero = x
(x  xs) !!' suc i = xs !!' i

{- Es imposible hacer trampa en Agda. -}

Vector :   Set {- Vec n is an n-dimensional vector -}
Vector m = Vec  m

Matrix :     Set {- Matrix m n is an m x n Matrix -}
Matrix m n = Vec (Vector n) m

{- multiplication with a scalar -}
_*v_ : {n : }    Vector n  Vector n
k *v [] = []
k *v (x  xs) = k * x  k *v xs

v1 : Vector 3
v1 = 1  2  3  []

test1 : Vector 3
test1 = 2 *v v1

{- addition of vectors -}
_+v_ : {n : }  Vector n  Vector n  Vector n
[] +v [] = []
(x  xs) +v (y  ys) = x + y  xs +v ys

v2 : Vector 3
v2 = 2  3  0  []

test2 : Vector 3
test2 = v1 +v v2

zeros : {n : }  Vector n
zeros {zero} = []
zeros {suc n} = zero  zeros {n}

{- multiplication of a vector and a matrix -}
_*vm_ : {m n : }  Vector m  Matrix m n  Vector n
[] *vm [] = zeros
(x  xs) *vm (ys  yss) = (x *v ys) +v (xs *vm yss)

id3 : Matrix 3 3
id3 = (1  0  0  []) 
     (0  1  0  []) 
     (0  0  1  []) 
     []

test3 : Vector 3
test3 = v1 *vm id3

{- matrix multiplication -}
_*mm_ : {l m n : }  Matrix l m  Matrix m n  Matrix l n
[] *mm yss = []
(xs  xss) *mm yss = xs *vm yss  xss *mm yss

inv3 : Matrix 3 3
inv3 = (0  0  1  []) 
      (0  1  0  []) 
      (1  0  0  []) 
      []

test4 : Matrix 3 3
test4 = inv3 *mm inv3

{- implement matrix transposition, i.e. swap rows and columns. -}

vreturn : {A : Set}{n : }  A  Vec A n
vreturn {n = zero} a = []
vreturn {n = suc m} a = a  vreturn {n = m} a

vapp : {A B : Set}{n : }  Vec (A  B) n  Vec A n  Vec B n
vapp [] [] = []
vapp (f  fs) (a  as) = f a  vapp fs as

transpose : {m n : }  Matrix m n  Matrix n m
transpose [] = vreturn []
transpose (as  ass) = vapp (vapp (vreturn _∷_) as) (transpose ass)

rect : Matrix 2 3
rect = (1  2  3  [])
      (4  5  6  [])
      []

test5 : Matrix 3 2
test5 = transpose rect