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

_+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