{-
Computer Aided Formal Reasoning (G53CFR, G54CFR)
Thorsten Altenkirch

Lecture 2: A first taste of Agda

In this lecture we start to explore the Agda system, a functional
ordinary examples which we could have developed in Haskell as well.
-}

module l02 where

module myNat where

{- Agda has no automatically loaded prelude. Hence we can start from
scratch and define the natural numbers. Later we will use the
standard libray. -}

data ℕ : Set where -- to type ℕ we type \bn
zero : ℕ
suc : (m : ℕ) → ℕ -- \-> or \to

{- To process an Agda file we use C-c C-c from emacs. Once Agda has
checked the file the type checker also colours the different
symbols. -}

{- We define addition. Note Agda's syntax for mixfix operations. The
arguments are represented by _s -}

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

{- Try to evaluate: (suc (suc zero)) + (suc (suc zero))
by typing in C-c C-n -}

{- Better we import the library definition of ℕ
This way we can type 2 instead of (suc (suc zero))
-}

open import Data.Nat

{- We define Lists :  -}

data List (A : Set) : Set where
[] : List A
_∷_ : (a : A) → (as : List A) → List A

{- In future we'll use
open import Data.List -}

{- declare the fixity of ∷ (type \::) -}

infixr 5 _∷_

{- Two example lists -}

l1 : List ℕ
l1 = 1 ∷ 2 ∷ 3 ∷ []

l2 : List ℕ
l2 = 4 ∷ 5 ∷ []

{- implementing append (++) -}

_++_ : {A : Set} → List A → List A → List A
[] ++ bs = bs
(a ∷ as) ++ bs = a ∷ (as ++ bs)

{- Note that Agda checks wether a function is terminating.
If we type
(a ∷ as) ++ bs = (a ∷ as) ++ bs
in the 2nd line Agda will complain by coloring the offending
function calls in red.
-}

{- What does the following variant of ++ do ? -}

_++'_ : {A : Set} → List A → List A → List A
as ++' [] = as
as ++' (b ∷ bs) = (b ∷ as) ++' bs

{- Indeed it can be used to define reverse.  This way to implement
reverse is often called fast reverse because it is "tail recursive"
which leads to a more efficient execution than the naive
implementation. -}

rev : {A : Set} → List A → List A
rev as = [] ++' as

{- We tried to define a function which accesses the nth element of a list:

_!!_ : {A : Set} → List A → ℕ → A
[] !! n = {!!}
(a ∷ as) !! zero = a
(a ∷ as) !! suc n = as !! n

but there is no way to complete the first line (consider what happens
if A is the empty type!
-}

{- To fix this we handle errors explicitely, using Maybe -}

open import Data.Maybe

{- This version of the function can either return an element of the list
(just a) or an error (nothing).
-}
_!!_ : {A : Set} → List A → ℕ → Maybe A
[] !! n = nothing
(a ∷ as) !! zero = just a
(a ∷ as) !! suc n = as !! n